1structure separationLogicSyntax :> separationLogicSyntax = 2struct 3 4(* 5quietdec := true; 6loadPath := (Globals.HOLDIR ^ "/examples/separationLogic/src") :: 7 (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot") :: 8 !loadPath; 9 10map load ["finite_mapTheory", "separationLogicTheory"]; 11show_assums := true; 12*) 13 14open HolKernel Parse boolLib separationLogicTheory 15 16 17(* 18quietdec := false; 19*) 20 21 22 23fun safe_dest_pair t = 24 pairLib.dest_pair t handle HOL_ERR _ => 25 (pairLib.mk_fst t, pairLib.mk_snd t); 26 27 28(***************************************************************** 29 Finite Maps 30 ****************************************************************) 31 32(*val t = ``FEMPTY |+ (v1,1) |+ (v2,2)``*) 33 34val FEMPTY_tm = ``FEMPTY:'a |-> 'b``; 35val FUPDATE_tm = ``$FUPDATE:('a |-> 'b) -> 'a # 'b -> ('a |-> 'b)``; 36 37fun strip_finite_map t = 38 let 39 val (op_term, args) = strip_comb t; 40 in 41 if (same_const op_term FUPDATE_tm) then 42 let 43 val (slist, rest) = (strip_finite_map (el 1 args)); 44 in 45 ((pairLib.dest_pair (el 2 args))::slist, rest) 46 end 47 else if (same_const op_term FEMPTY_tm) then ([], NONE) 48 else ([], SOME t) 49 end handle HOL_ERR _ => ([], SOME t); 50 51 52 53(***************************************************************** 54 Destructors Constructors 55 ****************************************************************) 56 57(*val l = [1,2,3,4,5,6,7,8,9]*) 58 59fun list2tuple1 l = (el 1 l); 60fun list2tuple2 l = (el 1 l, el 2 l); 61fun list2tuple3 l = (el 1 l, el 2 l, el 3 l); 62fun list2tuple4 l = (el 1 l, el 2 l, el 3 l, el 4 l); 63fun list2tuple5 l = (el 1 l, el 2 l, el 3 l, el 4 l, el 5 l); 64fun list2tuple6 l = (el 1 l, el 2 l, el 3 l, el 4 l, el 5 l, el 6 l); 65fun list2tuple7 l = (el 1 l, el 2 l, el 3 l, el 4 l, el 5 l, el 6 l, el 7 l); 66fun list2tuple8 l = (el 1 l, el 2 l, el 3 l, el 4 l, el 5 l, el 6 l, el 7 l, el 8 l); 67fun list2tuple9 l = (el 1 l, el 2 l, el 3 l, el 4 l, el 5 l, el 6 l, el 7 l, el 8 l, el 9 l); 68 69 70fun strip_comb_num n ff t = 71 let 72 val (f, args) = strip_comb t; 73 val _ = if (same_const f ff) andalso (length args = n) then () else Feedback.fail () 74 in 75 args 76 end; 77 78fun strip_comb_1 ff = list2tuple1 o (strip_comb_num 1 ff); 79fun strip_comb_2 ff = list2tuple2 o (strip_comb_num 2 ff); 80fun strip_comb_3 ff = list2tuple3 o (strip_comb_num 3 ff); 81fun strip_comb_4 ff = list2tuple4 o (strip_comb_num 4 ff); 82fun strip_comb_5 ff = list2tuple5 o (strip_comb_num 5 ff); 83fun strip_comb_6 ff = list2tuple6 o (strip_comb_num 6 ff); 84fun strip_comb_7 ff = list2tuple7 o (strip_comb_num 7 ff); 85fun strip_comb_8 ff = list2tuple8 o (strip_comb_num 8 ff); 86fun strip_comb_9 ff = list2tuple9 o (strip_comb_num 9 ff); 87 88 89 90 91 92 93 94fun asl_mk_const n = 95 prim_mk_const {Name = n, Thy = "separationLogic"} 96 97val asl_prog_parallel_term = asl_mk_const "asl_prog_parallel"; 98val dest_asl_prog_parallel = strip_comb_2 asl_prog_parallel_term; 99val is_asl_prog_parallel = (can dest_asl_prog_parallel); 100 101val asl_prog_diverge_term = asl_mk_const "asl_prog_diverge"; 102val asl_prog_fail_term = asl_mk_const "asl_prog_fail"; 103 104val asl_prog_seq_term = asl_mk_const "asl_prog_seq"; 105val dest_asl_prog_seq = strip_comb_2 asl_prog_seq_term; 106val is_asl_prog_seq = (can dest_asl_prog_seq); 107 108 109val asl_prog_block_term = asl_mk_const "asl_prog_block"; 110val dest_asl_prog_block = strip_comb_1 asl_prog_block_term; 111val is_asl_prog_block = (can dest_asl_prog_block); 112fun mk_asl_prog_block t = mk_icomb (asl_prog_block_term, t); 113 114val asl_prog_cond_term = asl_mk_const "asl_prog_cond"; 115val dest_asl_prog_cond = strip_comb_3 asl_prog_cond_term; 116val is_asl_prog_cond = (can dest_asl_prog_cond); 117fun mk_asl_prog_cond (c,p1,p2) = 118 list_mk_icomb(asl_prog_cond_term, [c,p1,p2]); 119 120val asl_prog_choice_term = asl_mk_const "asl_prog_choice"; 121val dest_asl_prog_choice = strip_comb_2 asl_prog_choice_term; 122val is_asl_prog_choice = (can dest_asl_prog_choice); 123 124 125 126val asl_prog_while_term = asl_mk_const "asl_prog_while"; 127val dest_asl_prog_while = strip_comb_2 asl_prog_while_term; 128val is_asl_prog_while = (can dest_asl_prog_while); 129fun mk_asl_prog_while (c,p) = 130 list_mk_icomb(asl_prog_while_term, [c,p]); 131 132val asl_prog_assume_term = asl_mk_const "asl_prog_assume"; 133val dest_asl_prog_assume = strip_comb_1 asl_prog_assume_term; 134val is_asl_prog_assume = (can dest_asl_prog_assume); 135 136 137val asl_prog_cond_critical_section_term = asl_mk_const "asl_prog_cond_critical_section"; 138val dest_asl_prog_cond_critical_section = strip_comb_3 asl_prog_cond_critical_section_term; 139val is_asl_prog_cond_critical_section = (can dest_asl_prog_cond_critical_section); 140 141 142val asl_prog_best_local_action_term = asl_mk_const "asl_prog_best_local_action"; 143val dest_asl_prog_best_local_action = strip_comb_2 asl_prog_best_local_action_term; 144val is_asl_prog_best_local_action = (can dest_asl_prog_best_local_action); 145 146 147val ASL_PROGRAM_HOARE_TRIPLE_term = asl_mk_const "ASL_PROGRAM_HOARE_TRIPLE"; 148val dest_ASL_PROGRAM_HOARE_TRIPLE = strip_comb_5 ASL_PROGRAM_HOARE_TRIPLE_term; 149val is_ASL_PROGRAM_HOARE_TRIPLE = (can dest_ASL_PROGRAM_HOARE_TRIPLE); 150 151 152 153val ASL_PROGRAM_IS_ABSTRACTION_term = asl_mk_const "ASL_PROGRAM_IS_ABSTRACTION"; 154val dest_ASL_PROGRAM_IS_ABSTRACTION = strip_comb_4 ASL_PROGRAM_IS_ABSTRACTION_term; 155val is_ASL_PROGRAM_IS_ABSTRACTION = (can dest_ASL_PROGRAM_IS_ABSTRACTION); 156fun mk_ASL_PROGRAM_IS_ABSTRACTION (xenv,penv,x,y) = 157 list_mk_icomb(ASL_PROGRAM_IS_ABSTRACTION_term, [xenv,penv,x,y]); 158 159 160val ASL_SPECIFICATION_term = asl_mk_const "ASL_SPECIFICATION" 161val dest_ASL_SPECIFICATION = strip_comb_3 ASL_SPECIFICATION_term; 162val is_ASL_SPECIFICATION = can dest_ASL_SPECIFICATION; 163 164 165val COND_PROP___IMP_term = asl_mk_const "COND_PROP___IMP"; 166val dest_COND_PROP___IMP = strip_comb_2 COND_PROP___IMP_term; 167val is_COND_PROP___IMP = (can dest_COND_PROP___IMP); 168 169val COND_PROP___EQUIV_term = asl_mk_const "COND_PROP___EQUIV"; 170val dest_COND_PROP___EQUIV = strip_comb_2 COND_PROP___EQUIV_term; 171val is_COND_PROP___EQUIV = (can dest_COND_PROP___EQUIV); 172 173 174val COND_PROP___STRONG_EXISTS_term = asl_mk_const "COND_PROP___STRONG_EXISTS"; 175fun dest_COND_PROP___STRONG_EXISTS tt = 176 let 177 val arg = strip_comb_1 COND_PROP___STRONG_EXISTS_term tt; 178 val (v, body) = pairSyntax.dest_pabs arg 179 in 180 (v, body) 181 end; 182val is_COND_PROP___STRONG_EXISTS = can dest_COND_PROP___STRONG_EXISTS; 183 184 185 186val COND_PROP___EXISTS_term = asl_mk_const "COND_PROP___EXISTS"; 187fun dest_COND_PROP___EXISTS tt = 188 let 189 val arg = strip_comb_1 COND_PROP___EXISTS_term tt; 190 val (v,b) = dest_abs arg 191 in 192 (v,b) 193 end; 194val is_COND_PROP___EXISTS = (can dest_COND_PROP___EXISTS); 195 196 197 198val COND_PROP___ADD_COND_term = asl_mk_const "COND_PROP___ADD_COND"; 199val dest_COND_PROP___ADD_COND = strip_comb_2 COND_PROP___ADD_COND_term; 200val is_COND_PROP___ADD_COND = (can dest_COND_PROP___ADD_COND); 201 202 203val asl_cond_star_term = asl_mk_const "asl_cond_star"; 204val dest_asl_cond_star = strip_comb_3 asl_cond_star_term 205val is_asl_cond_star = (can dest_asl_cond_star); 206 207 208val asl_pred_false_term = asl_mk_const "asl_pred_false"; 209val asl_pred_true_term = asl_mk_const "asl_pred_true"; 210val asl_pred_neg_term = asl_mk_const "asl_pred_neg"; 211val asl_pred_and_term = asl_mk_const "asl_pred_and"; 212val asl_pred_or_term = asl_mk_const "asl_pred_or"; 213val asl_pred_prim_term = asl_mk_const "asl_pred_prim"; 214 215val asl_exists_term = asl_mk_const "asl_exists" 216val asl_exists_list_term = asl_mk_const "asl_exists_list" 217val fasl_star_term = asl_mk_const "fasl_star"; 218val asl_star_term = asl_mk_const "asl_star"; 219val asl_bigstar_list_term = asl_mk_const "asl_bigstar_list"; 220val asl_trivial_cond_term = asl_mk_const "asl_trivial_cond"; 221val asl_emp_term = asl_mk_const "asl_emp"; 222val asl_false_term = asl_mk_const "asl_false"; 223val is_asl_false = same_const asl_false_term 224 225 226val dest_asl_trival_cond = strip_comb_2 asl_trivial_cond_term; 227val is_asl_trivial_cond = (can dest_asl_trival_cond); 228 229val dest_asl_star = strip_comb_3 asl_star_term; 230val is_asl_star = (can dest_asl_star); 231fun strip_asl_star t = 232let 233 val (_, p1, p2) = dest_asl_star t; 234 val p1L = strip_asl_star p1; 235 val p2L = strip_asl_star p2; 236in 237 (p1L @ p2L) 238end handle HOL_ERR _ => [t]; 239 240 241fun dest_asl_exists tt = 242 let 243 val arg = strip_comb_1 asl_exists_term tt; 244 val (v,b) = dest_abs arg 245 in 246 (v,b) 247 end; 248val is_asl_exists = (can dest_asl_exists); 249 250fun dest_asl_exists_list tt = 251 let 252 val (arg1, arg2) = strip_comb_2 asl_exists_list_term tt; 253 in 254 (arg1,arg2) 255 end; 256val is_asl_exists_list = (can dest_asl_exists_list); 257 258 259 260val asl_comment_loop_invariant_term = asl_mk_const "asl_comment_loop_invariant" 261val dest_asl_comment_loop_invariant = strip_comb_2 asl_comment_loop_invariant_term; 262val is_asl_comment_loop_invariant = (can dest_asl_comment_loop_invariant); 263 264val asl_comment_block_spec_term = asl_mk_const "asl_comment_block_spec" 265val dest_asl_comment_block_spec = strip_comb_2 asl_comment_block_spec_term; 266val is_asl_comment_block_spec = (can dest_asl_comment_block_spec); 267 268val asl_comment_loop_spec_term = asl_mk_const "asl_comment_loop_spec" 269val dest_asl_comment_loop_spec = strip_comb_2 asl_comment_loop_spec_term; 270val is_asl_comment_loop_spec = (can dest_asl_comment_loop_spec); 271 272val asl_comment_loop_unroll_term = asl_mk_const "asl_comment_loop_unroll" 273val dest_asl_comment_loop_unroll = strip_comb_2 asl_comment_loop_unroll_term; 274val is_asl_comment_loop_unroll = (can dest_asl_comment_loop_unroll); 275 276val asl_comment_location_string_term = asl_mk_const "asl_comment_location_string" 277val dest_asl_comment_location_string = strip_comb_2 asl_comment_location_string_term; 278val is_asl_comment_location_string = (can dest_asl_comment_location_string); 279 280val asl_comment_location_term = asl_mk_const "asl_comment_location" 281val dest_asl_comment_location = strip_comb_2 asl_comment_location_term; 282val is_asl_comment_location = (can dest_asl_comment_location); 283fun mk_asl_comment_location (c, tt) = list_mk_icomb (asl_comment_location_term, [c, tt]) 284 285val empty_label_list = listSyntax.mk_list ([], markerSyntax.label_ty) 286fun save_dest_asl_comment_location tt = 287let 288 val (c, p) = dest_asl_comment_location tt; 289in 290 (c, p, fn () => ISPECL [c, p] asl_comment_location_def) 291end handle HOL_ERR _ => (empty_label_list, tt, fn () => REFL tt) 292 293 294fun dest_list_asl_comment_location tt = 295dest_asl_comment_location tt handle HOL_ERR _ => 296dest_asl_comment_location (rand (rator tt)) 297 298 299fun save_dest_list_asl_comment_location tt = 300 if (is_asl_comment_location tt) then 301 save_dest_asl_comment_location tt 302 else 303 let 304 val (c, p, f) = save_dest_asl_comment_location (rand (rator tt)) 305 in 306 (c, p, fn () => (RATOR_CONV (RAND_CONV (K (f ()))) tt)) 307 end; 308 309val asl_comment_location2_term = asl_mk_const "asl_comment_location2" 310val dest_asl_comment_location2 = strip_comb_2 asl_comment_location2_term; 311val is_asl_comment_location2 = (can dest_asl_comment_location2); 312fun mk_asl_comment_location2 (c, tt) = list_mk_icomb (asl_comment_location2_term, [c, tt]) 313 314fun save_dest_asl_comment_location2 tt = 315let 316 val (c, p) = dest_asl_comment_location2 tt; 317in 318 (c, p, fn () => ISPECL [c, p] asl_comment_location2_def) 319end handle HOL_ERR _ => (empty_label_list, tt, fn () => REFL tt) 320 321 322val asl_comment_abstraction_term = asl_mk_const "asl_comment_abstraction" 323val dest_asl_comment_abstraction = strip_comb_2 asl_comment_abstraction_term; 324val is_asl_comment_abstraction = (can dest_asl_comment_abstraction); 325 326fun dest_asl_comment t = 327 let 328 val (op_term, args) = strip_comb t; 329 val _ = if (length args = 2) then () else (Feedback.fail ()); 330 val (arg1, arg2) = (el 1 args, el 2 args); 331 332 val def_thm = 333 if (same_const op_term asl_comment_location_term) then 334 asl_comment_location_def 335 else if (same_const op_term asl_comment_location_string_term) then 336 asl_comment_location_string_def 337 else if (same_const op_term asl_comment_location2_term) then 338 asl_comment_location2_def 339 else if (same_const op_term asl_comment_loop_invariant_term) then 340 asl_comment_loop_invariant_def 341 else if (same_const op_term asl_comment_abstraction_term) then 342 asl_comment_abstraction_def 343 else if (same_const op_term asl_comment_loop_spec_term) then 344 asl_comment_loop_spec_def 345 else if (same_const op_term asl_comment_loop_unroll_term) then 346 asl_comment_loop_unroll_def 347 else if (same_const op_term asl_comment_block_spec_term) then 348 asl_comment_block_spec_def 349 else Feedback.fail(); 350 in 351 (op_term, arg1, arg2, def_thm) 352 end; 353 354val asl_comment_assert_term = asl_mk_const "asl_comment_assert" 355val dest_asl_comment_assert = strip_comb_1 asl_comment_assert_term; 356val is_asl_comment_assert = (can dest_asl_comment_assert); 357 358 359val asl_procedure_call_preserve_names_wrapper_term = asl_mk_const "asl_procedure_call_preserve_names_wrapper" 360val dest_asl_procedure_call_preserve_names_wrapper = strip_comb_4 asl_procedure_call_preserve_names_wrapper_term 361val is_asl_procedure_call_preserve_names_wrapper = can dest_asl_procedure_call_preserve_names_wrapper 362 363 364 365 366 367end; 368