Re: [isabelle] syntax



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

On 12/20/2011 12:04 PM, Brian Huffman wrote:
On Tue, Dec 20, 2011 at 10:44 AM, Viorel Preoteasa
<viorel.preoteasa at abo.fi>  wrote:
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 :]
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' :]"

- Brian








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.