Email Gateway (Aug 18 2022 at 18:50): 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
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' :]"
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: Nov 21 2024 at 12:39 UTC