Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] syntax


view this post on Zulip Email Gateway (Aug 18 2022 at 18:50):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,

I have a programming construct construct of the following form:

update (% (x::'a, y::'b, z::'c): {(x'::', y'::'b, z::'c) . x' = x+1 /\
y'=y / 2 /\ z' = z + x + y})

Is it possible to introduce the syntax:

[: x::'a, y::'b, z::'c := x'::'a, y'::'b, z::'c . x' = x+1 /\ y'=y / 2
/\ z' = z + x + y :]

or

[: x, y, z := x', y', z . (x'::'a) = x+1 /\ (y'::'b)=y / 2 /\ (z'::'c) =
z + x + y :]

Best regards,

Viorel

view this post on Zulip Email Gateway (Aug 18 2022 at 18:50):

From: Brian Huffman <huffman@in.tum.de>
Here's something that's close to what you want. It does require
parentheses around the tuples of variable bindings, though. (The
nonterminal "pttrn" is what is used for the binders in lambda
abstractions and set comprehensions.)

syntax "_foo" :: "pttrn => pttrn => logic => logic" ("[: _ := _ . _:]")
translations "_foo x y t" == "CONST update (_abs x (_Coll y t))"
term "[: (x::'a, y::'b) := (x'::'a, y'::'b) . P x y x' y' :]"

And here's another variant where the parentheses are not required.
It's a little more awkward to define because the syntax translation
needs to convert from nonterminal "patterns" (defined in
HOL/Product_Type.thy, used for tuple binders) to nonterminal "pttrn".

syntax "_foo" :: "patterns => patterns => logic => logic" ("[: _ := _ . _:]")
translations
"_foo (_patterns x xs) (_patterns y ys) t" == "CONST update (_abs
(_pattern x xs) (_Coll (_pattern y ys) t))"
"_foo x y t" == "CONST update (_abs x (_Coll y t))"

term "[: x::'a, y::'b := x'::'a, y'::'b . P x y x' y' :]"

view this post on Zulip Email Gateway (Aug 18 2022 at 18:51):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Brian,

Thank you very much. It works nicely. It seems
that the syntax [: x, y := x', y' . ... :] works together
with the syntax [: R :] = update R when R has the
type 'a => ('a set).

Viorel


Last updated: Mar 29 2024 at 08:18 UTC