1structure holfootParserGenpreds :> holfootParserGenpreds =
2struct
3
4(*
5quietdec := true;
6loadPath :=
7            (concat [Globals.HOLDIR, "/examples/separationLogic/src"]) ::
8            (concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot"]) ::
9            !loadPath;
10
11map load ["finite_mapTheory", "holfootTheory",
12     "Parsetree", "AssembleHolfootParser"];
13show_assums := true;
14*)
15
16open HolKernel Parse boolLib finite_mapTheory
17open Parsetree;
18open separationLogicSyntax
19open vars_as_resourceSyntax
20open holfootSyntax
21open holfootParser
22
23(*
24quietdec := false;
25*)
26
27
28val reset_genpreds = holfootParser.reset_genpreds;
29
30fun add_default_genpreds () =
31let
32   fun mk_list [] = Absyn.mk_ident "NIL"
33     | mk_list (e::es) =
34       Absyn.mk_app (Absyn.mk_app (Absyn.mk_ident "CONS", e), mk_list es)
35
36   val holfoot_data_list___EMPTY_tm = ``[]:(holfoot_tag # num list) list``;
37
38   fun mk_holfoot_ap_list_seg_absyn (tag, exp1, exp2) =
39      Absyn.list_mk_app (Absyn.mk_AQ holfoot_ap_data_list_seg_term, [
40          tag, exp1, Absyn.mk_AQ holfoot_data_list___EMPTY_tm, exp2]);
41
42   (* list(x) *)
43   val _ = add_genpred ("list", [Aspred_arg_ty_exp],
44                 fn [exp1] => mk_holfoot_ap_list_seg_absyn (
45                     Absyn.mk_AQ (string2holfoot_tag (!list_link_tag)),
46                     exp1,
47                     Absyn.mk_AQ (holfoot_exp_null_term)));
48   (* lseg(x,y) *)
49   val _ = add_genpred ("lseg", [Aspred_arg_ty_exp,Aspred_arg_ty_comma,Aspred_arg_ty_exp],
50                 fn [exp1,exp2] => mk_holfoot_ap_list_seg_absyn (
51                     Absyn.mk_AQ (string2holfoot_tag (!list_link_tag)),
52                     exp1,
53                     exp2));
54
55   (* lseg(tag;x,y) *)
56   val _ = add_genpred ("lseg", [Aspred_arg_ty_tag, Aspred_arg_ty_semi, Aspred_arg_ty_exp, Aspred_arg_ty_comma, Aspred_arg_ty_exp],
57                 fn [tag,exp1,exp2] => mk_holfoot_ap_list_seg_absyn (
58                     tag,
59                     exp1,
60                     exp2));
61
62
63   fun mk_holfoot_ap_data_list_seg_absyn (tag, exp1, dtag, data, exp2) =
64      Absyn.list_mk_app (Absyn.mk_AQ holfoot_ap_data_list_seg_term, [
65          tag, exp1, mk_list [Absyn.mk_pair (dtag, data)], exp2]);
66
67
68   (* data_list(x,data) *)
69   val _ = add_genpred ("data_list", [Aspred_arg_ty_exp, Aspred_arg_ty_comma, Aspred_arg_ty_hol],
70                 fn [exp1,data] => mk_holfoot_ap_data_list_seg_absyn (
71                     Absyn.mk_AQ (string2holfoot_tag (!list_link_tag)),
72                     exp1,
73                     Absyn.mk_AQ (string2holfoot_tag (!data_list_tag)),
74                     data,
75                     Absyn.mk_AQ (holfoot_exp_null_term)));
76
77
78   (* data_lseg(x,data,y) *)
79   val _ = add_genpred ("data_lseg", [Aspred_arg_ty_exp,Aspred_arg_ty_comma,Aspred_arg_ty_hol,Aspred_arg_ty_comma,Aspred_arg_ty_exp],
80                 fn [exp1,data,exp2] => mk_holfoot_ap_data_list_seg_absyn (
81                     Absyn.mk_AQ (string2holfoot_tag (!list_link_tag)),
82                     exp1,
83                     Absyn.mk_AQ (string2holfoot_tag (!data_list_tag)),
84                     data,
85                     exp2));
86
87   (* data_lseg(tag;x,dtag:data,y) *)
88   val _ = add_genpred ("data_lseg", [Aspred_arg_ty_tag, Aspred_arg_ty_semi,
89                                      Aspred_arg_ty_exp, Aspred_arg_ty_comma,
90                                      Aspred_arg_ty_tag, Aspred_arg_ty_colon,
91                                      Aspred_arg_ty_hol, Aspred_arg_ty_comma,
92                                      Aspred_arg_ty_exp],
93                 fn [tag,exp1,dtag,data,exp2] => mk_holfoot_ap_data_list_seg_absyn (
94                     tag,
95                     exp1, dtag,data,
96                     exp2));
97
98
99   fun mk_holfoot_ap_tree_absyn (tagL, tagR, exp) =
100      Absyn.list_mk_app(Absyn.mk_AQ holfoot_ap_bintree_term, [
101                      Absyn.mk_pair (tagL, tagR), exp])
102
103   (* tree(x) *)
104   val _ = add_genpred ("tree", [Aspred_arg_ty_exp],
105                 fn [exp] => mk_holfoot_ap_tree_absyn (
106                     Absyn.mk_AQ (string2holfoot_tag (#1 (!tree_link_tags))),
107                     Absyn.mk_AQ (string2holfoot_tag (#2 (!tree_link_tags))),
108                     exp));
109
110   (* tree(tagL,tagR,x) *)
111   val _ = add_genpred ("tree", [Aspred_arg_ty_tag, Aspred_arg_ty_comma, Aspred_arg_ty_tag, Aspred_arg_ty_comma, Aspred_arg_ty_exp],
112                 fn [tagL, tagR, exp] => mk_holfoot_ap_tree_absyn (
113                     tagL,tagR,exp));
114
115
116   fun mk_holfoot_ap_data_tree_absyn (tagL, exp, dtagL, data) =
117      Absyn.list_mk_app(Absyn.mk_AQ holfoot_ap_data_tree_term, [
118                tagL, exp,
119                Absyn.mk_pair (dtagL, data)]);
120
121   (* data_tree(x,data) *)
122   val _ = add_genpred ("data_tree", [Aspred_arg_ty_exp, Aspred_arg_ty_comma, Aspred_arg_ty_hol],
123                 fn [exp,data] => mk_holfoot_ap_data_tree_absyn (
124                     mk_list [Absyn.mk_AQ (string2holfoot_tag (#1 (!tree_link_tags))),
125                      Absyn.mk_AQ (string2holfoot_tag (#2 (!tree_link_tags)))],
126                     exp,
127                     mk_list [Absyn.mk_AQ (string2holfoot_tag (!tree_data_tag))],
128                     data))
129
130   (* data_tree(x,dtagL:data) *)
131   val _ = add_genpred ("data_tree", [Aspred_arg_ty_exp, Aspred_arg_ty_comma, Aspred_arg_ty_list Aspred_arg_ty_tag, Aspred_arg_ty_colon, Aspred_arg_ty_hol],
132                 fn [exp,dtagL,data] => mk_holfoot_ap_data_tree_absyn (
133                     mk_list [Absyn.mk_AQ (string2holfoot_tag (#1 (!tree_link_tags))),
134                      Absyn.mk_AQ (string2holfoot_tag (#2 (!tree_link_tags)))],
135                     exp,
136                     dtagL,
137                     data))
138
139   (* data_tree(tagL;x,dtagL:data) *)
140   val _ = add_genpred ("data_tree", [
141              Aspred_arg_ty_list Aspred_arg_ty_tag, Aspred_arg_ty_semi,
142              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
143              Aspred_arg_ty_list Aspred_arg_ty_tag, Aspred_arg_ty_colon,
144              Aspred_arg_ty_hol],
145                 fn [tagL,exp,dtagL,data] => mk_holfoot_ap_data_tree_absyn (
146                     tagL,
147                     exp,
148                     dtagL,
149                     data))
150
151
152   fun mk_holfoot_ap_array_absyn (exp1, exp2) =
153        Absyn.list_mk_app (Absyn.mk_AQ holfoot_ap_data_array_term, [
154                 exp1, exp2, Absyn.mk_AQ holfoot_data_list___EMPTY_tm]);
155
156   (* array(b,n) *)
157   val _ = add_genpred ("array", [
158              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
159              Aspred_arg_ty_exp],
160                 fn [exp1,exp2] => mk_holfoot_ap_array_absyn (
161                     exp1,
162                     exp2))
163
164
165   fun mk_holfoot_ap_data_array_absyn (exp1, exp2, dtag, data) =
166        Absyn.list_mk_app (Absyn.mk_AQ holfoot_ap_data_array_term, [
167                 exp1, exp2, mk_list [Absyn.mk_pair (dtag, data)]]);
168
169
170   (* data_array(b,n,data) *)
171   val _ = add_genpred ("data_array", [
172              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
173              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
174              Aspred_arg_ty_hol],
175                 fn [exp1,exp2,data] => mk_holfoot_ap_data_array_absyn (
176                     exp1,
177                     exp2,
178                     Absyn.mk_AQ (string2holfoot_tag (!array_data_tag)),
179                     data))
180
181   (* data_array(b,n,dtag:data) *)
182   val _ = add_genpred ("data_array", [
183              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
184              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
185              Aspred_arg_ty_tag, Aspred_arg_ty_colon,
186              Aspred_arg_ty_hol],
187                 fn [exp1,exp2,dtag,data] => mk_holfoot_ap_data_array_absyn (
188                     exp1,
189                     exp2,
190                     dtag,
191                     data))
192
193   fun mk_holfoot_ap_interval_absyn (exp1, exp2) =
194        Absyn.list_mk_app (Absyn.mk_AQ holfoot_ap_data_interval_term, [
195                 exp1, exp2, Absyn.mk_AQ holfoot_data_list___EMPTY_tm]);
196
197   (* interval(b,e) *)
198   val _ = add_genpred ("interval", [
199              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
200              Aspred_arg_ty_exp],
201                 fn [exp1,exp2] => mk_holfoot_ap_interval_absyn (
202                     exp1,
203                     exp2))
204
205   fun mk_holfoot_ap_data_interval_absyn (exp1, exp2, dtag, data) =
206        Absyn.list_mk_app (Absyn.mk_AQ holfoot_ap_data_interval_term, [
207                 exp1, exp2, mk_list [Absyn.mk_pair (dtag, data)]]);
208
209
210   (* data_interval(b,e,data) *)
211   val _ = add_genpred ("data_interval", [
212              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
213              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
214              Aspred_arg_ty_hol],
215                 fn [exp1,exp2,data] => mk_holfoot_ap_data_interval_absyn (
216                     exp1,
217                     exp2,
218                     Absyn.mk_AQ (string2holfoot_tag (!array_data_tag)),
219                     data))
220
221   (* data_interval(b,n,dtag:data) *)
222   val _ = add_genpred ("data_interval", [
223              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
224              Aspred_arg_ty_exp, Aspred_arg_ty_comma,
225              Aspred_arg_ty_tag, Aspred_arg_ty_colon,
226              Aspred_arg_ty_hol],
227                 fn [exp1,exp2,dtag,data] => mk_holfoot_ap_data_interval_absyn (
228                     exp1,
229                     exp2,
230                     dtag,
231                     data))
232
233
234
235   fun mk_holfoot_ap_queue_absyn (tag, exp1, exp2) =
236      Absyn.list_mk_app (Absyn.mk_AQ holfoot_ap_data_queue_term, [
237          tag, exp1, Absyn.mk_AQ holfoot_data_list___EMPTY_tm, exp2]);
238
239   (* queue(f,r) *)
240   val _ = add_genpred ("queue", [Aspred_arg_ty_exp, Aspred_arg_ty_comma, Aspred_arg_ty_exp],
241                 fn [exp1,exp2] => mk_holfoot_ap_queue_absyn (
242                     Absyn.mk_AQ (string2holfoot_tag (!list_link_tag)),
243                     exp1, exp2));
244
245
246   fun mk_holfoot_ap_data_queue_absyn (tag, exp1, dtag, data, exp2) =
247      Absyn.list_mk_app (Absyn.mk_AQ holfoot_ap_data_queue_term, [
248          tag, exp1, mk_list [Absyn.mk_pair (dtag, data)], exp2]);
249
250
251   (* data_queue(x,data,r) *)
252   val _ = add_genpred ("data_queue", [Aspred_arg_ty_exp, Aspred_arg_ty_comma, Aspred_arg_ty_hol, Aspred_arg_ty_comma, Aspred_arg_ty_exp],
253                 fn [exp1,data,exp2] => mk_holfoot_ap_data_queue_absyn (
254                     Absyn.mk_AQ (string2holfoot_tag (!list_link_tag)),
255                     exp1,
256                     Absyn.mk_AQ (string2holfoot_tag (!data_list_tag)),
257                     data,
258                     exp2));
259
260
261   (* data_queue(tl;x,dta:data,r) *)
262   val _ = add_genpred ("data_queue", [
263                 Aspred_arg_ty_tag, Aspred_arg_ty_semi,
264                 Aspred_arg_ty_exp, Aspred_arg_ty_comma,
265                 Aspred_arg_ty_tag, Aspred_arg_ty_colon,
266                 Aspred_arg_ty_hol, Aspred_arg_ty_comma,
267                 Aspred_arg_ty_exp],
268                 fn [tag,exp1,dtag,data,exp2] => mk_holfoot_ap_data_queue_absyn (
269                     tag,
270                     exp1,
271                     dtag,
272                     data,
273                     exp2));
274in
275   ()
276end;
277
278fun init_genpreds () =
279let
280   val _ = reset_genpreds ();
281   val _ = add_default_genpreds ();
282in
283   ()
284end;
285
286
287val _ = init_genpreds ();
288
289
290(*
291val file = "/home/tt291/hol98/examples/separationLogic/src/holfoot/EXAMPLES/automatic/list.sf"
292val file = "/home/tt291/hol98/examples/separationLogic/src/holfoot/EXAMPLES/interactive/mergesort.dsf"
293val file = "/home/tt291/hol98/examples/separationLogic/src/holfoot/EXAMPLES/automatic/tree.sf"
294val file = "/home/tt291/hol98/examples/separationLogic/src/holfoot/EXAMPLES/automatic/tree_copy.dsf"
295val file = "/home/tt291/hol98/examples/separationLogic/src/holfoot/EXAMPLES/automatic/array_copy-shape.dsf"
296val file = "/home/tt291/hol98/examples/separationLogic/src/holfoot/EXAMPLES/interactive/array-inc.dsf"
297val file = "/home/tt291/hol98/examples/separationLogic/src/holfoot/EXAMPLES/automatic/quicksort-shape.dsf"
298val file = "/home/tt291/hol98/examples/separationLogic/src/holfoot/EXAMPLES/interactive/queue.dsf2"
299
300
301val _ = parse_holfoot_file file
302
303*)
304
305end
306