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