48 upon parsing/printing. Thus every pointer program needs to have a |
47 upon parsing/printing. Thus every pointer program needs to have a |
49 program variable H, and assertions should not contain any locally |
48 program variable H, and assertions should not contain any locally |
50 bound Hs - otherwise they may bind the implicit H. *} |
49 bound Hs - otherwise they may bind the implicit H. *} |
51 |
50 |
52 syntax |
51 syntax |
53 "@emp" :: "bool" ("emp") |
52 "_emp" :: "bool" ("emp") |
54 "@singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]") |
53 "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]") |
55 "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60) |
54 "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60) |
56 "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60) |
55 "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60) |
57 |
56 |
58 (* FIXME does not handle "_idtdummy" *) |
57 (* FIXME does not handle "_idtdummy" *) |
59 ML{* |
58 ML{* |
60 (* free_tr takes care of free vars in the scope of sep. logic connectives: |
59 (* free_tr takes care of free vars in the scope of sep. logic connectives: |
61 they are implicitly applied to the heap *) |
60 they are implicitly applied to the heap *) |
77 absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H" |
76 absfree("H",dummyT,P) $ absfree("H",dummyT,Q) $ Syntax.free "H" |
78 | wand_tr ts = raise TERM ("wand_tr", ts); |
77 | wand_tr ts = raise TERM ("wand_tr", ts); |
79 *} |
78 *} |
80 |
79 |
81 parse_translation |
80 parse_translation |
82 {* [("@emp", emp_tr), ("@singl", singl_tr), |
81 {* [("_emp", emp_tr), ("_singl", singl_tr), |
83 ("@star", star_tr), ("@wand", wand_tr)] *} |
82 ("_star", star_tr), ("_wand", wand_tr)] *} |
84 |
83 |
85 text{* Now it looks much better: *} |
84 text{* Now it looks much better: *} |
86 |
85 |
87 lemma "VARS H x y z w |
86 lemma "VARS H x y z w |
88 {[x\<mapsto>y] ** [z\<mapsto>w]} |
87 {[x\<mapsto>y] ** [z\<mapsto>w]} |
119 (* |
118 (* |
120 | strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps |
119 | strip (Abs(_,_,((list as Const("List",_))$ Bound 0 $ p $ ps))) = list$p$ps |
121 *) |
120 *) |
122 | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t |
121 | strip (Abs(_,_,(t as Const("_var",_) $ Var _) $ Bound 0)) = t |
123 | strip (Abs(_,_,P)) = P |
122 | strip (Abs(_,_,P)) = P |
124 | strip (Const("is_empty",_)) = Syntax.const "@emp" |
123 | strip (Const("is_empty",_)) = Syntax.const "_emp" |
125 | strip t = t; |
124 | strip t = t; |
126 in |
125 in |
127 fun is_empty_tr' [_] = Syntax.const "@emp" |
126 fun is_empty_tr' [_] = Syntax.const "_emp" |
128 fun singl_tr' [_,p,q] = Syntax.const "@singl" $ p $ q |
127 fun singl_tr' [_,p,q] = Syntax.const "_singl" $ p $ q |
129 fun star_tr' [P,Q,_] = Syntax.const "@star" $ strip P $ strip Q |
128 fun star_tr' [P,Q,_] = Syntax.const "_star" $ strip P $ strip Q |
130 fun wand_tr' [P,Q,_] = Syntax.const "@wand" $ strip P $ strip Q |
129 fun wand_tr' [P,Q,_] = Syntax.const "_wand" $ strip P $ strip Q |
131 end |
130 end |
132 *} |
131 *} |
133 |
132 |
134 print_translation |
133 print_translation |
135 {* [("is_empty", is_empty_tr'),("singl", singl_tr'), |
134 {* [("is_empty", is_empty_tr'),("singl", singl_tr'), |