1structure holfoot_pp_print :> holfoot_pp_print = 2struct 3 4(* 5quietdec := true; 6loadPath := 7 (concat [Globals.HOLDIR, "/examples/separationLogic/src"]) :: 8 (concat [Globals.HOLDIR, "/examples/separationLogic/src/holfoot"]) :: 9 !loadPath; 10show_assums := true; 11*) 12 13open HolKernel boolLib bossLib PPBackEnd Parse 14open separationLogicSyntax 15open vars_as_resourceSyntax 16open holfootSyntax 17open Unicode 18 19(* 20quietdec := false; 21*) 22val holfoot_pretty_printer_block_indent = ref 3; 23 24fun unicode_choice snu su = 25 if (current_trace "Unicode" = 1) then su else snu 26 27val _ = register_UserStyle NONE "holfoot_comment" [FG LightGrey] 28val _ = register_UserStyle NONE "holfoot_spec" [FG OrangeRed] 29val _ = register_UserStyle NONE "holfoot_alert_0" [Bold, Underline] 30val _ = register_UserStyle NONE "holfoot_alert_1" [Bold] 31val _ = register_UserStyle NONE "holfoot_alert_2" [Underline] 32val _ = register_UserStyle NONE "holfoot_frame_split___context" [FG LightGrey] 33val _ = register_UserStyle NONE "holfoot_frame_split___imp" [FG OrangeRed] 34val _ = register_UserStyle NONE "holfoot_frame_split___split" [FG Green] 35 36fun holfoot_var_printer GS backend (sys : term_pp_types.sysprinter) (ppfns:term_pp_types.ppstream_funs) gravs d t = let 37 open Portable term_pp_types 38 val v_term = dest_holfoot_var t; 39 in 40 (#add_string ppfns) (stringLib.fromHOLstring v_term) 41 end 42 43 44 45fun holfoot_tag_printer GS backend (sys : term_pp_types.sysprinter) (ppfns:term_pp_types.ppstream_funs) gravs d t = let 46 open Portable term_pp_types 47 val t_term = dest_holfoot_tag t; 48 in 49 (#add_string ppfns) (stringLib.fromHOLstring t_term) 50 end 51 52 53fun pretty_print_list not_last oper list = 54 smpp.pr_list oper not_last list; 55 56 57fun pretty_print_list_sep sep (sys,strn,brk) d = 58 let 59 open Portable term_pp_types smpp; 60 infix >>; 61 in 62 pretty_print_list (strn sep >> brk (1,0)) 63 (fn arg => sys (Top, Top, Top) (d - 1) arg) 64 end; 65 66 67fun holfoot_proccall_args_printer backend (sys_raw : term_pp_types.sysprinter) (ppfns:term_pp_types.ppstream_funs) gravs d args_term = 68 let 69 open Portable term_pp_types smpp; 70 val {add_string,add_break,add_newline,...} = ppfns 71 val (refArgs_term, valArgs_term) = pairLib.dest_pair args_term; 72 val (refArgsL, _) = listSyntax.dest_list refArgs_term; 73 val (valArgsL, _) = listSyntax.dest_list valArgs_term; 74 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 75 val pretty_print_arg_list = pretty_print_list_sep "," (sys, add_string, add_break) d; 76 in 77 if (null valArgsL) andalso (null refArgsL) then (add_string "()") else 78 (add_string "(" >> 79 pretty_print_arg_list refArgsL >> 80 (if (null valArgsL) then nothing else ( 81 add_string ";" >> add_break (1,0) >> 82 pretty_print_arg_list valArgsL 83 )) >> 84 add_string ")") 85 end; 86 87fun prefix_var_name prefix v = 88let 89 val (v_name, v_type) = dest_var v; 90 val v' = mk_var (prefix^v_name, v_type); 91in 92 v' 93end; 94 95 96fun add_loc_add_string (i:int) add_string add_break loc_add_strings = 97let 98 open smpp; 99 fun add_pps [] = nothing 100 | add_pps [s1] = (add_string s1) 101 | add_pps (s1::l) = ( 102 add_string s1 >> 103 add_string " " >> 104 add_string "-" >> 105 add_break (1, i) >> 106 add_pps l) 107in 108 add_pps loc_add_strings 109end; 110 111fun label_list2ML t = rev (map (fst o dest_var) (fst (listSyntax.dest_list t))); 112 113fun holfoot_prog_printer GS backend (sys_raw : term_pp_types.sysprinter) (ppfns:term_pp_types.ppstream_funs) gravs d t = let 114 open Portable term_pp_types smpp 115 infix >> 116 val {add_string,add_break,ublock,add_newline,ustyle,...} = ppfns 117 val (op_term,args) = strip_comb t; 118 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 119 in 120 if (same_const op_term holfoot_prog_field_lookup_term) then ( 121 let 122 val v_term = el 1 args; 123 val exp_term = el 2 args; 124 val tag_term = el 3 args; 125 in 126 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 127 sys (Top, Top, Top) (d - 1) v_term >> 128 add_string " =" >> 129 add_break (1,1) >> 130 sys (Top, Top, Top) (d - 1) exp_term >> 131 add_string (unicode_choice "->" UChar.rightarrow) >> 132 sys (Top, Top, Top) (d - 1) tag_term 133 ) 134 end 135 ) else if (same_const op_term holfoot_prog_field_assign_term) then ( 136 let 137 val exp_term = el 1 args; 138 val tag_term = el 2 args; 139 val exp2_term = el 3 args; 140 in 141 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 142 sys (Top, Top, Top) (d - 1) exp_term >> 143 add_string (unicode_choice "->" UChar.rightarrow) >> 144 sys (Top, Top, Top) (d - 1) tag_term >> 145 add_string " =" >> 146 add_break (1,1) >> 147 sys (Top, Top, Top) (d - 1) exp2_term 148 ) 149 end 150 ) else if (same_const op_term holfoot_prog_procedure_call_term) then ( 151 let 152 val name_term = el 1 args; 153 val args_term = el 2 args; 154 in 155 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 156 add_string (stringLib.fromHOLstring name_term) >> 157 holfoot_proccall_args_printer backend sys_raw ppfns gravs (d - 1) args_term 158 ) 159 end 160 ) else if (same_const op_term holfoot_prog_parallel_procedure_call_term) then ( 161 let 162 val name1_term = el 1 args; 163 val args1_term = el 2 args; 164 val name2_term = el 3 args; 165 val args2_term = el 4 args; 166 in 167 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 168 add_string (stringLib.fromHOLstring name1_term) >> 169 holfoot_proccall_args_printer backend sys_raw ppfns gravs (d - 1) args1_term >> 170 add_string " ||" >> 171 add_string " " >> 172 add_string (stringLib.fromHOLstring name2_term) >> 173 holfoot_proccall_args_printer backend sys_raw ppfns gravs (d - 1) args2_term 174 ) 175 end 176 ) else if (same_const op_term holfoot_prog_assign_term) then ( 177 let 178 val v_term = el 1 args; 179 val exp_term = el 2 args; 180 in 181 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 182 sys (Top, Top, Top) (d - 1) v_term >> 183 add_string " =" >> 184 add_break (1,1) >> 185 sys (Top, Top, Top) (d - 1) exp_term 186 ) 187 end 188 ) else if (same_const op_term holfoot_prog_dispose_term) then ( 189 let 190 val n_term = el 1 args; 191 val e_term = el 2 args; 192 val simple = is_holfoot_exp_one n_term; 193 in 194 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 195 if (simple) then ( 196 add_string "dispose" >> 197 add_string " " >> 198 sys (Top, Top, Top) (d - 1) e_term 199 ) else ( 200 add_string "dispose-block" >> 201 add_string "(" >> 202 sys (Top, Top, Top) (d - 1) e_term >> 203 add_string "," >> 204 sys (Top, Top, Top) (d - 1) n_term >> 205 add_string ")" 206 )) 207 end 208 ) else if (same_const op_term holfoot_prog_new_term) then ( 209 let 210 val n_term = el 1 args; 211 val v_term = el 2 args; 212 val (l, _) = listSyntax.dest_list (el 3 args); 213 val simple = is_holfoot_exp_one n_term; 214 in 215 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 216 sys (Top, Top, Top) (d - 1) v_term >> 217 add_string " =" >> 218 add_break (1,!holfoot_pretty_printer_block_indent) >> 219 (if simple then ( 220 add_string "new()" 221 ) else ( 222 add_string "new-block" >> 223 add_string "(" >> 224 sys (Top, Top, Top) (d - 1) n_term >> 225 add_string ")" 226 )) >> 227 (if (null l) then nothing else ( 228 add_string " " >> 229 add_string "[" >> 230 ustyle [UserStyle "holfoot_spec"] ( 231 pretty_print_list_sep "," (sys, add_string, add_break) d l 232 ) >> 233 add_string "]" 234 )) 235 ) 236 end 237 ) else if (same_const op_term asl_prog_assume_term) then ( 238 let 239 val prop_term = el 1 args; 240 in 241 ublock CONSISTENT 0 ( 242 add_string "assume" >> 243 sys (Top, Top, Top) (d - 1) prop_term 244 ) 245 end 246 ) else if (same_const op_term asl_prog_diverge_term) then ( 247 ublock CONSISTENT 0 ( 248 add_string "diverge" 249 ) 250 ) else if (same_const op_term asl_prog_fail_term) then ( 251 ublock CONSISTENT 0 ( 252 add_string "fail" 253 ) 254 ) else if (same_const op_term asl_prog_cond_term) then ( 255 let 256 val prop_term = el 1 args; 257 val prog1_term = el 2 args; 258 val prog2_term = el 3 args; 259 in 260 ublock CONSISTENT 0 ( 261 add_string "if" >> 262 add_string " " >> 263 sys (Top, Top, Top) (d - 1) prop_term >> 264 add_string " {" >> 265 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 266 ublock INCONSISTENT 0 ( 267 sys (Top, Top, Top) (d - 1) prog1_term 268 ) >> 269 add_break (1,0) >> 270 add_string "} else {" >> 271 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 272 ublock INCONSISTENT 0 ( 273 sys (Top, Top, Top) (d - 1) prog2_term 274 ) >> 275 add_break (1,0) >> 276 add_string "}" 277 ) 278 end 279 ) else if (same_const op_term asl_prog_choice_term) then ( 280 let 281 val prog1_term = el 1 args; 282 val prog2_term = el 2 args; 283 in 284 ublock CONSISTENT 0 ( 285 add_string "if (*) {" >> 286 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 287 ublock INCONSISTENT 0 ( 288 sys (Top, Top, Top) (d - 1) prog1_term 289 ) >> 290 add_break (1,0) >> 291 add_string "} else {" >> 292 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 293 ublock INCONSISTENT 0 ( 294 sys (Top, Top, Top) (d - 1) prog2_term 295 ) >> 296 add_break (1,0) >> 297 add_string "}" 298 ) 299 end 300 ) else if (same_const op_term asl_prog_while_term) then ( 301 let 302 val prop_term = el 1 args; 303 val prog_term = el 2 args; 304 in 305 ublock CONSISTENT 0 ( 306 add_string "while" >> 307 add_string " " >> 308 sys (Top, Top, Top) (d - 1) prop_term >> 309 add_string " " >> 310 add_string "{" >> 311 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 312 ublock INCONSISTENT 0 ( 313 sys (Top, Top, Top) (d - 1) prog_term 314 ) >> 315 add_break (1,0) >> 316 add_string "}" 317 ) 318 end 319 ) else if (same_const op_term asl_comment_block_spec_term) orelse 320 (same_const op_term asl_comment_loop_spec_term) then ( 321 let 322 val (pre_term, post_term) = pairSyntax.dest_pair (el 1 args); 323 val prog_term = el 2 args; 324 val loop = same_const op_term asl_comment_loop_spec_term; 325 326 val (v,pre_body) = pairSyntax.dest_pabs pre_term; 327 val (_,post_body) = pairSyntax.dest_pabs post_term; 328 val vL = free_vars v; 329 val vL' = map (prefix_var_name "!") vL; 330 val su = map (op |->) (zip vL vL'); 331 val pre_body' = subst su pre_body; 332 val post_body' = subst su post_body; 333 in 334 ublock CONSISTENT 0 ( 335 ustyle [UserStyle "holfoot_comment"] ( 336 add_string (if loop then "loop-specification" else "block-specification") >> 337 add_string " " >> 338 add_string "[" >> 339 sys (Top, Top, Top) (d - 1) pre_body' >> 340 add_string "]" 341 ) >> 342 add_string " " >> 343 add_string "{" >> 344 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 345 ublock INCONSISTENT 0 ( 346 sys (Top, Top, Top) (d - 1) prog_term 347 ) >> 348 add_break (1,0) >> 349 add_string "}" >> 350 add_string " " >> 351 ustyle [UserStyle "holfoot_comment"] ( 352 add_string "[" >> 353 sys (Top, Top, Top) (d - 1) post_body' >> 354 add_string "]" 355 ) 356 ) 357 end 358 ) else if (same_const op_term asl_comment_loop_unroll_term) then ( 359 let 360 val unroll_term = el 1 args; 361 val prog_term = el 2 args; 362 in 363 ublock CONSISTENT 0 ( 364 ustyle [UserStyle "holfoot_comment"] ( 365 add_string ("loop-unroll") >> 366 add_string " " >> 367 sys (Top, Top, Top) (d - 1) unroll_term 368 ) >> 369 add_string " " >> 370 add_string "{" >> 371 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 372 ublock INCONSISTENT 0 ( 373 sys (Top, Top, Top) (d - 1) prog_term 374 ) >> 375 add_break (1,0) >> 376 add_string "}" 377 ) 378 end 379 ) else if (same_const op_term asl_comment_assert_term) then ( 380 let 381 val p_term = el 1 args; 382 val (v,p_body) = pairSyntax.dest_pabs p_term; 383 val vL = free_vars v; 384 val vL' = map (prefix_var_name "!") vL; 385 val su = map (op |->) (zip vL vL'); 386 val p_body' = subst su p_body; 387 in 388 ustyle [UserStyle "holfoot_comment"] ( 389 add_string ("assert") >> 390 add_string " " >> 391 add_string "[" >> 392 ublock CONSISTENT 0 ( 393 sys (Top, Top, Top) (d - 1) p_body' 394 ) >> 395 add_string "]" 396 ) 397 end 398 ) else if (same_const op_term asl_prog_cond_critical_section_term) then ( 399 let 400 val res_term = el 1 args; 401 val cond_term = el 2 args; 402 val prog_term = el 3 args; 403 in 404 ublock CONSISTENT 0 ( 405 add_string "with" >> 406 add_string " " >> 407 add_string (stringLib.fromHOLstring res_term) >> 408 add_string " " >> 409 add_string "when" >> 410 add_string " " >> 411 sys (Top, Top, Top) (d - 1) cond_term >> 412 add_string " {" >> 413 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 414 ublock INCONSISTENT 0 ( 415 sys (Top, Top, Top) (d - 1) prog_term 416 ) >> 417 add_break (1,0) >> 418 add_string "}" 419 ) 420 end 421 ) else if (same_const op_term var_res_prog_local_var_term) orelse 422 (same_const op_term var_res_prog_call_by_value_arg_term) then ( 423 let 424 val (l, t') = var_res_strip_local_vars t; 425 val _ = if (l = []) then raise term_pp_types.UserPP_Failed else (); 426 in 427 ublock INCONSISTENT 0 ( 428 add_string "local" >> 429 add_break (1,!holfoot_pretty_printer_block_indent) >> 430 pretty_print_list 431 (add_string "," >> add_break (1, !holfoot_pretty_printer_block_indent)) 432 (fn (v,vt) => ( 433 ublock CONSISTENT (!holfoot_pretty_printer_block_indent) ( 434 if (isSome vt) then ( 435 add_string "(" >> 436 sys (Top, Top, Top) (d - 1) v >> 437 add_string " " >> 438 add_string "=" >> 439 add_string " " >> 440 sys (Top, Top, Top) (d - 1) (valOf vt) >> 441 add_string ")" 442 ) else ( 443 sys (Top, Top, Top) (d - 1) v 444 )))) l>> 445 add_string ";" >> 446 add_break (1,0) >> 447 sys (Top, Top, Top) (d - 1) t' 448 ) 449 end 450 ) else if (same_const op_term asl_prog_block_term) then ( 451 let 452 val (argL_term, rest_term) = listSyntax.strip_cons (el 1 args); 453 val (argL_term, rest_term) = let 454 val (c, rest_term') = dest_asl_comment_location rest_term 455 val nc = mk_asl_comment_location (c, mk_comb (op_term, rest_term')) 456 in 457 (argL_term@[nc], rest_term') 458 end handle HOL_ERR _ => (argL_term, rest_term); 459 val _ = if listSyntax.is_nil rest_term then () else Feedback.fail() 460 in 461 if argL_term = [] then nothing else 462 if length argL_term = 1 then sys (Top, Top, Top) (d - 1) (hd argL_term) else 463 ( 464 ublock CONSISTENT 0 ( 465 pretty_print_list (add_break (1,0)) 466 (fn stm => 467 (ublock CONSISTENT (!holfoot_pretty_printer_block_indent) ( 468 sys (Top, Top, Top) (d - 1) stm >> 469 add_string ";" 470 ))) argL_term 471 ) 472 ) 473 end 474 ) else if (same_const op_term asl_comment_location_term) then ( 475 let 476 val loc_add_strings = label_list2ML (el 1 args); 477 in 478 ublock CONSISTENT 0 ( 479 ublock INCONSISTENT 0 ( 480 ustyle [UserStyle "holfoot_comment"] ( 481 add_string "/*" >> 482 add_break (1,3) >> 483 add_loc_add_string 3 add_string add_break loc_add_strings >> 484 add_break (1,0) >> 485 add_string "*/" 486 ) 487 ) >> 488 add_break (1,0) >> 489 sys (Top, Top, Top) (d - 1) (el 2 args) 490 ) 491 end 492 ) else if (same_const op_term asl_comment_location2_term) then ( 493 let 494 val loc_add_strings = label_list2ML (el 1 args); 495 in 496 ublock CONSISTENT 0 ( 497 ublock INCONSISTENT 0 ( 498 ustyle [UserStyle "holfoot_comment"] ( 499 add_string "/**" >> 500 add_break (1,3) >> 501 add_loc_add_string 3 add_string add_break loc_add_strings >> 502 add_break (1,0) >> 503 add_string "**/" 504 ) 505 ) >> 506 add_break (1,0) >> 507 sys (Top, Top, Top) (d - 1) (el 2 args) 508 ) 509 end 510 ) else if (same_const op_term asl_comment_loop_invariant_term) then ( 511 let 512 val (v,body) = pairSyntax.dest_pabs (el 1 args); 513 val vL = free_vars v; 514 val vL' = map (prefix_var_name "!") vL; 515 val su = map (op |->) (zip vL vL'); 516 val body' = subst su body; 517 in 518 ublock CONSISTENT 0 ( 519 ublock INCONSISTENT 0 ( 520 ustyle [UserStyle "holfoot_comment"] ( 521 add_string "/*" >> 522 add_string " " >> 523 ustyle [UserStyle "holfoot_alert_2"] ( 524 add_string "Loop Invariant:" 525 ) >> 526 add_break (1,3) >> 527 add_string "[" >> 528 sys (Top, Top, Top) (d - 1) body' >> 529 add_string "] */" 530 ) 531 ) >> 532 add_break (1,0) >> 533 sys (Top, Top, Top) (d - 1) (el 2 args) 534 ) 535 end 536 ) else if (same_const op_term asl_comment_abstraction_term) then ( 537 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 538 add_string "abstracted" >> 539 add_string " " >> 540 add_string (fst (dest_var (el 1 args))) 541 ) 542 ) else if (same_const op_term asl_comment_location_string_term) then ( 543 let 544 val loc_add_strings = [stringLib.fromHOLstring (el 1 args)]; 545 in 546 ublock CONSISTENT 0 ( 547 ublock INCONSISTENT 0 ( 548 ustyle [UserStyle "holfoot_comment"] ( 549 add_string "/***" >> 550 add_break (1,3) >> 551 add_loc_add_string 3 add_string add_break loc_add_strings >> 552 add_break (1,0) >> 553 add_string "***/" 554 ) 555 ) >> 556 add_break (1,0) >> 557 sys (Top, Top, Top) (d - 1) (el 2 args) 558 ) 559 end 560 ) else( 561 raise term_pp_types.UserPP_Failed 562 ) 563 end 564 565 566 567 568fun coded_expression_to_term e1 e2 p = 569 let 570 val arg1 = Parse.term_to_string e1; 571 val arg2 = Parse.term_to_string e2; 572 val v1 = mk_var (arg1, numSyntax.num); 573 val v2 = mk_var (arg2, numSyntax.num); 574 val tt0 = list_mk_comb(p, [v1,v2]) 575 val tt1 = rhs (concl (LIST_BETA_CONV tt0)) handle HOL_ERR _ => tt0; 576 in 577 tt1 578 end; 579 580fun gencoded_expression_to_term p eL_t = 581 let 582 val (eL,_) = listSyntax.dest_list eL_t; 583 val esL = map Parse.term_to_string eL; 584 val evL = map (fn n => mk_var (n, numSyntax.num)) esL; 585 val evL_t = listSyntax.mk_list (evL, numSyntax.num); 586 val tt0 = mk_comb(p, evL_t) 587 val tt1 = rhs (concl ((BETA_CONV THENC SIMP_CONV list_ss []) tt0)) handle HOL_ERR _ => tt0; 588 in 589 tt1 590 end; 591 592fun holfoot_expression_printer GS backend (sys_raw : term_pp_types.sysprinter) (ppfns:term_pp_types.ppstream_funs) gravs d t = 593 let 594 open Portable term_pp_types smpp 595 infix >> 596 val {add_string,add_break,ublock,add_newline,ustyle,...} = ppfns 597 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 598 val (op_term,args) = strip_comb t; 599 in 600 if (same_const op_term var_res_exp_var_term) then ( 601 sys (Top, Top, Top) (d - 1) (hd args) 602 ) else if (same_const op_term var_res_exp_const_term) then ( 603 (if (is_var (hd args)) then add_string "#" else nothing) >> 604 sys (Top, Top, Top) (d - 1) (hd args) 605 ) else if (same_const op_term var_res_exp_binop_term) then ( 606 add_string "(" >> 607 sys (Top, Top, Top) (d - 1) (coded_expression_to_term (el 2 args) (el 3 args) (el 1 args)) >> 608 add_string ")" 609 ) else if (same_const op_term var_res_exp_op_term) then ( 610 add_string "(" >> 611 sys (Top, Top, Top) (d - 1) (gencoded_expression_to_term 612 (el 1 args) (el 2 args)) >> 613 add_string ")" 614 ) else ( 615 raise term_pp_types.UserPP_Failed 616 ) 617 end 618 619fun holfoot_pred_printer GS backend sys_raw (ppfns:term_pp_types.ppstream_funs) gravs d t = 620 let 621 open Portable term_pp_types smpp 622 infix >> 623 val {add_string,add_break,ublock,add_newline,ustyle,...} = ppfns 624 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 625 val (op_term,args) = strip_comb t; 626 in 627 if (same_const op_term asl_pred_false_term) then ( 628 add_string "false" 629 ) else if (same_const op_term asl_pred_true_term) then ( 630 add_string "true" 631 ) else if (same_const op_term asl_pred_neg_term) then ( 632 add_string "(not" >> 633 add_string " " >> 634 sys (Top, Top, Top) (d - 1) (el 1 args) >> 635 add_string ")" 636 ) else if (same_const op_term asl_pred_and_term) then ( 637 add_string "(" >> 638 sys (Top, Top, Top) (d - 1) (el 1 args) >> 639 add_string " " >> 640 add_string "and" >> 641 add_string " " >> 642 sys (Top, Top, Top) (d - 1) (el 2 args) >> 643 add_string (")") 644 ) else if (same_const op_term asl_pred_or_term) then ( 645 add_string ("(") >> 646 sys (Top, Top, Top) (d - 1) (el 1 args) >> 647 add_string (" or") >> 648 add_string " " >> 649 sys (Top, Top, Top) (d - 1) (el 2 args) >> 650 add_string (")") 651 ) else if (same_const op_term var_res_pred_bin_term) then ( 652 add_string ("(") >> 653 sys (Top, Top, Top) (d - 1) (coded_expression_to_term (el 2 args) (el 3 args) (el 1 args)) >> 654 add_string (")") 655 ) else if (same_const op_term var_res_pred_term) then ( 656 add_string "(" >> 657 sys (Top, Top, Top) (d - 1) (gencoded_expression_to_term 658 (el 1 args) (el 2 args)) >> 659 add_string ")" 660 ) else ( 661 raise term_pp_types.UserPP_Failed 662 ) 663 end 664 665 666 667fun finite_map_printer (sys, strn, brk) gravs d t = 668 let 669 open Portable term_pp_types smpp 670 infix >> 671 val (plist,rest) = strip_finite_map t; 672 in 673 (if ((length plist) = 1) then nothing else strn "[") >> 674 (pretty_print_list (strn ", ") 675 (fn (tag,exp) => 676 (sys (Top, Top, Top) (d - 1) tag >> 677 strn ":" >> 678 sys (Top, Top, Top) (d - 1) exp 679 )) plist) >> 680 (if (isSome rest) then ( 681 (if (length plist = 0) then nothing else strn (", ")) >> 682 strn ("...")) 683 else nothing) >> 684 (if (length plist = 1) then nothing else strn "]") 685 end 686 687fun tag_list_printer (sys, strn, brk) gravs d t = 688 let 689 open Portable term_pp_types smpp 690 infix >> 691 val (plist,_) = listSyntax.dest_list t; 692 val plist = map pairSyntax.dest_pair plist; 693 in 694 (if ((length plist) = 1) then nothing else strn "[") >> 695 (pretty_print_list (strn ", ") 696 (fn (tag,exp) => 697 (sys (Top, Top, Top) (d - 1) tag >> 698 strn ":" >> 699 sys (Top, Top, Top) (d - 1) exp 700 )) plist) >> 701 (if (length plist = 1) then nothing else strn "]") 702 end 703 704 705fun COND_PROP___STRONG_EXISTS_term_rewrite tt = 706let 707 val (v, body) = dest_COND_PROP___STRONG_EXISTS tt; 708 val vL = pairSyntax.strip_pair v; 709 val vL' = map (prefix_var_name "_") vL; 710 val body' = subst (map op|-> (zip vL vL')) body; 711in 712 COND_PROP___STRONG_EXISTS_term_rewrite body' 713end handle HOL_ERR _ => tt; 714 715 716fun holfoot_a_prop_printer Gs backend (sys_raw:term_pp_types.sysprinter) (ppfns:term_pp_types.ppstream_funs) gravs d t = let 717 open Portable term_pp_types smpp 718 infix >> 719 val {add_string,add_break,ublock,add_newline,ustyle,...} = ppfns 720 val (op_term,args) = strip_comb t; 721 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 722 in 723 if (same_const op_term asl_star_term) orelse 724 (same_const op_term fasl_star_term) then ( 725 sys (Top, Top, Top) (d - 1) (el 2 args) >> 726 add_string " " >> 727 add_string (unicode_choice "-*-" UChar.blackstar) >> 728 add_break (1,0) >> 729 sys (Top, Top, Top) (d - 1) (el 3 args) 730 ) else if (same_const op_term asl_bigstar_list_term) then ( 731 add_string (unicode_choice "-**-" UChar.circlestar) >> 732 add_break (1,0) >> 733 sys (Top, Top, Top) (d - 1) (el 2 args) 734 ) else if (same_const op_term var_res_prop_equal_term) then ( 735 ublock INCONSISTENT 0 ( 736 add_string "(" >> 737 sys (Top, Top, Top) (d - 1) (el 2 args) >> 738 add_string (" "^(unicode_choice "==" "=")) >> 739 add_break (1,!holfoot_pretty_printer_block_indent) >> 740 sys (Top, Top, Top) (d - 1) (el 3 args) >> 741 add_string ")" 742 ) 743 ) else if (same_const op_term var_res_prop_unequal_term) then ( 744 ublock INCONSISTENT 0 ( 745 add_string "(" >> 746 sys (Top, Top, Top) (d - 1) (el 2 args) >> 747 add_string (" "^(unicode_choice "!=" UChar.neq)) >> 748 add_break (1,!holfoot_pretty_printer_block_indent) >> 749 sys (Top, Top, Top) (d - 1) (el 3 args) >> 750 add_string ")" 751 ) 752 ) else if (same_const op_term var_res_prop_binexpression_term) then ( 753 ublock INCONSISTENT 0 ( 754 add_string "(" >> 755 sys (Top, Top, Top) (d - 1) (coded_expression_to_term (el 4 args) (el 5 args) (el 3 args)) >> 756 add_string ")" 757 ) 758 ) else if (same_const op_term asl_emp_term) then ( 759 add_string "emp" 760 ) else if (same_const op_term holfoot_ap_data_list_term) then ( 761 ublock INCONSISTENT 0 ( 762 add_string (if (same_const (el 3 args) listSyntax.nil_tm) then 763 "list" else "data_list") >> 764 add_string "(" >> 765 add_break (0,!holfoot_pretty_printer_block_indent) >> 766 sys (Top, Top, Top) (d - 1) (el 1 args) >> 767 add_string ";" >> 768 add_break (1,!holfoot_pretty_printer_block_indent) >> 769 sys (Top, Top, Top) (d - 1) (el 2 args) >> 770 (if not (same_const (el 3 args) listSyntax.nil_tm) then 771 (add_string "," >> add_break (1,!holfoot_pretty_printer_block_indent) >> 772 tag_list_printer (sys, add_string, add_break) (Top,Top,Top) (d-1) (el 3 args) 773 ) else nothing) >> 774 add_string ")" 775 ) 776 ) else if (same_const op_term holfoot_ap_data_list_seg_term) then ( 777 let 778 val end_is_null = is_holfoot_exp_null (el 4 args); 779 val has_data = not (same_const (el 3 args) listSyntax.nil_tm); 780 val desc = if has_data then 781 (if end_is_null then "data_list" else "data_lseg") else 782 (if end_is_null then "list" else "lseg") 783 in 784 ublock INCONSISTENT 0 ( 785 add_string desc >> 786 add_string "(" >> 787 add_break (0,!holfoot_pretty_printer_block_indent) >> 788 sys (Top, Top, Top) (d - 1) (el 1 args) >> 789 add_string ";" >> 790 add_break (1,!holfoot_pretty_printer_block_indent) >> 791 sys (Top, Top, Top) (d - 1) (el 2 args) >> 792 (if has_data then 793 (add_string "," >> add_break (1,!holfoot_pretty_printer_block_indent) >> 794 tag_list_printer (sys, add_string, add_break) (Top,Top,Top) (d-1) (el 3 args) 795 ) else nothing) >> 796 (if (end_is_null) then nothing else ( 797 add_string "," >> 798 add_break (1,!holfoot_pretty_printer_block_indent) >> 799 sys (Top, Top, Top) (d - 1) (el 4 args) 800 )) >> 801 add_string ")" 802 ) 803 end 804 ) else if (same_const op_term holfoot_ap_data_queue_term) then ( 805 let 806 val has_data = not (same_const (el 3 args) listSyntax.nil_tm); 807 val desc = if has_data then "data_queue" else "queue"; 808 in 809 ublock INCONSISTENT 0 ( 810 add_string desc >> 811 add_string "(" >> 812 add_break (0,!holfoot_pretty_printer_block_indent) >> 813 sys (Top, Top, Top) (d - 1) (el 1 args) >> 814 add_string ";" >> 815 add_break (1,!holfoot_pretty_printer_block_indent) >> 816 sys (Top, Top, Top) (d - 1) (el 2 args) >> 817 (if has_data then 818 (add_string "," >> add_break (1,!holfoot_pretty_printer_block_indent) >> 819 tag_list_printer (sys, add_string, add_break) (Top,Top,Top) (d-1) (el 3 args) 820 ) else nothing) >> 821 add_string "," >> 822 add_break (1,!holfoot_pretty_printer_block_indent) >> 823 sys (Top, Top, Top) (d - 1) (el 4 args) >> 824 add_string ")" 825 ) 826 end 827 ) else if ((same_const op_term holfoot_ap_data_array_term) orelse 828 (same_const op_term holfoot_ap_data_interval_term)) then ( 829 let 830 val has_data = not (same_const (el 3 args) listSyntax.nil_tm); 831 val is_interval = same_const op_term holfoot_ap_data_interval_term; 832 val desc = if is_interval then 833 (if has_data then "data_interval" else "interval") 834 else 835 (if has_data then "data_array" else "array"); 836 in 837 ublock INCONSISTENT 0 ( 838 add_string desc >> 839 add_string "(" >> 840 add_break (0,!holfoot_pretty_printer_block_indent) >> 841 sys (Top, Top, Top) (d - 1) (el 1 args) >> 842 add_string "," >> 843 add_break (1,!holfoot_pretty_printer_block_indent) >> 844 sys (Top, Top, Top) (d - 1) (el 2 args) >> 845 (if has_data then 846 (add_string "," >> add_break (1,!holfoot_pretty_printer_block_indent) >> 847 tag_list_printer (sys, add_string, add_break) (Top,Top,Top) (d-1) (el 3 args) 848 ) else nothing) >> 849 add_string ")" 850 ) 851 end 852 ) else if (same_const op_term holfoot_ap_bintree_term) then ( 853 ublock INCONSISTENT 0 ( 854 add_string "bin_tree" >> 855 add_string "(" >> 856 sys (Top, Top, Top) (d - 1) (fst (pairSyntax.dest_pair (el 1 args))) >> 857 add_string "," >> 858 add_string " " >> 859 sys (Top, Top, Top) (d - 1) (snd (pairSyntax.dest_pair (el 1 args))) >> 860 add_string ";" >> 861 add_break(1, !holfoot_pretty_printer_block_indent) >> 862 sys (Top, Top, Top) (d - 1) (el 2 args) >> 863 add_string ")" 864 ) 865 ) else if (same_const op_term holfoot_ap_tree_term) then ( 866 ublock INCONSISTENT 0 ( 867 add_string "tree" >> 868 add_string "(" >> 869 sys (Top, Top, Top) (d - 1) (el 1 args) >> 870 add_string ";" >> 871 add_break(1, !holfoot_pretty_printer_block_indent) >> 872 sys (Top, Top, Top) (d - 1) (el 2 args) >> 873 add_string ")" 874 ) 875 ) else if (same_const op_term holfoot_ap_data_tree_term) then ( 876 let 877 val (dtag_t, data_t) = pairSyntax.dest_pair (el 3 args); 878 in 879 ublock INCONSISTENT 0 ( 880 add_string "data_tree" >> 881 add_string "(" >> 882 sys (Top, Top, Top) (d - 1) (el 1 args) >> 883 add_string ";" >> 884 add_break(1, !holfoot_pretty_printer_block_indent) >> 885 sys (Top, Top, Top) (d - 1) (el 2 args) >> 886 add_string "," >> 887 add_break(1, !holfoot_pretty_printer_block_indent) >> 888 sys (Top, Top, Top) (d - 1) dtag_t >> 889 add_string ":" >> 890 sys (Top, Top, Top) (d - 1) data_t >> 891 add_string ")" 892 ) 893 end 894 ) else if (same_const op_term holfoot_ap_points_to_term) then ( 895 ublock INCONSISTENT 0 ( 896 sys (Top, Top, Top) (d - 1) (el 1 args) >> 897 add_string " " >> 898 add_string (unicode_choice "|->" UChar.longmapsto) >> 899 add_break(1, !holfoot_pretty_printer_block_indent) >> 900 finite_map_printer (sys,add_string,add_break) (Top,Top,Top) (d-1) (el 2 args) 901 ) 902 ) else if (same_const op_term var_res_map_term) then ( 903 let 904 val (vc, b) = pairSyntax.dest_pabs (el 2 args); 905 val vl = pairSyntax.strip_pair vc; 906 in 907 ublock INCONSISTENT 0 ( 908 add_string "map" >> 909 add_string " " >> 910 add_string "(\\" >> 911 pretty_print_list_sep "" (sys, add_string, add_break) d vl >> 912 add_string "." >> 913 add_break (1,!holfoot_pretty_printer_block_indent) >> 914 sys (Top, Top, Top) (d - 1) b >> 915 add_string ")" >> 916 add_break (1,!holfoot_pretty_printer_block_indent) >> 917 add_string "(" >> 918 sys (Top, Top, Top) (d - 1) (el 3 args) >> 919 add_string ")" 920 ) 921 end 922 ) else if (same_const op_term var_res_prop_binexpression_cond_term) then ( 923 ublock CONSISTENT 0 ( 924 add_string "if" >> 925 add_string " " >> 926 add_string "(" >> 927 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 928 sys (Top, Top, Top) (d - 1) (coded_expression_to_term (el 3 args) (el 4 args) (el 2 args)) >> 929 add_string ")" 930 ) >> 931 add_string(" ") >> 932 add_string("then (") >> 933 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 934 ublock INCONSISTENT 0 ( 935 sys (Top, Top, Top) (d - 1) (el 5 args) 936 ) >> 937 add_break (1, 0) >> 938 add_string ") else (" >> 939 add_break (1,(!holfoot_pretty_printer_block_indent)) >> 940 ublock INCONSISTENT 0 ( 941 sys (Top, Top, Top) (d - 1) (el 6 args) 942 ) >> 943 add_break (1, 0) >> 944 add_string ") end" 945 ) 946 ) else if (same_const op_term var_res_bool_proposition_term) then ( 947 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 948 add_string "pure" >> 949 add_string "(" >> 950 sys (Top, Top, Top) (d - 1) (el 2 args) >> 951 add_string ")" 952 ) 953 ) else if (same_const op_term var_res_prop_expression_term) then ( 954 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 955 add_string "pure" >> 956 add_string "(" >> 957 sys (Top, Top, Top) (d - 1) (gencoded_expression_to_term 958 (el 3 args) (el 4 args)) >> 959 add_string ")" 960 ) 961 ) else if (same_const op_term var_res_prop_stack_true_term) then ( 962 add_string "pure(T)" 963 ) else if (same_const op_term asl_false_term) then ( 964 add_string "false" 965 ) else if (same_const op_term var_res_prop_input_ap_distinct_term) then ( 966 let 967 val (w,r) = pairSyntax.dest_pair (el 2 args); 968 val wL = pred_setSyntax.strip_set w; 969 val rL = pred_setSyntax.strip_set r; 970 in 971 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 972 add_string "w/r:" >> 973 add_break (1,0) >> 974 pretty_print_list_sep "," (sys, add_string, add_break) d wL >> 975 add_string ";" >> 976 add_break (1,0) >> 977 pretty_print_list_sep "," (sys, add_string, add_break) d rL >> 978 add_string " " >> 979 add_string "|" >> 980 add_break (1,0) >> 981 sys (Top, Top, Top) (d - 1) (el 4 args) 982 ) 983 end 984 ) else if (same_const op_term var_res_prop_input_ap_term) then ( 985 let 986 val (w,r) = pairSyntax.dest_pair (el 2 args); 987 val wL = pred_setSyntax.strip_set w; 988 val rL = pred_setSyntax.strip_set r; 989 in 990 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 991 add_string "w/r:" >> 992 add_break (1,0) >> 993 pretty_print_list_sep "," (sys, add_string, add_break) d wL >> 994 add_string ";" >> 995 add_break (1,0) >> 996 pretty_print_list_sep "," (sys, add_string, add_break) d rL >> 997 add_string " " >> 998 add_string "|" >> 999 add_break (1,0) >> 1000 sys (Top, Top, Top) (d - 1) (el 3 args) >> 1001 add_string "" 1002 ) 1003 end 1004 ) else if (same_const op_term COND_PROP___STRONG_EXISTS_term) then ( 1005 let 1006 val body' = COND_PROP___STRONG_EXISTS_term_rewrite t 1007 in 1008 sys (Top, Top, Top) (d - 1) body' 1009 end 1010 ) else if (same_const op_term asl_exists_term) then ( 1011 let 1012 val (v,body) = dest_abs (el 1 args); 1013 val v' = prefix_var_name "_" v; 1014 val body' = subst [v |-> v'] body; 1015 in 1016 sys (Top, Top, Top) (d - 1) body' 1017 end 1018 ) else ( 1019 raise term_pp_types.UserPP_Failed 1020 ) 1021 end 1022 1023 1024 1025 1026fun holfoot_specification_printer GS backend (sys_raw:term_pp_types.sysprinter) (ppfns:term_pp_types.ppstream_funs) gravs d t = let 1027 open Portable term_pp_types smpp 1028 infix >> 1029 val {add_string,add_break,ublock,add_newline,ustyle,...} = ppfns 1030 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 1031 val (_, resL,funL) = dest_ASL_SPECIFICATION t; 1032 val resL = rand resL; 1033 1034 fun rest_preprocess rest = 1035 let 1036 val argL = pairLib.strip_pair rest; 1037 in 1038 (el 1 argL, el 2 argL, el 3 argL) 1039 end; 1040 1041 val restL = map rest_preprocess (fst (listSyntax.dest_list resL)); 1042 1043 fun funt_preprocess funt = 1044 let 1045 val argL = pairLib.strip_pair funt; 1046 val (assume_opt_term, fun_name,abs_body,abs_spec) = 1047 (el 1 argL, el 2 argL, el 3 argL, el 4 argL); 1048 1049 1050 val (pv, spec) = pairSyntax.dest_pabs abs_spec; 1051 val x_pre_wrapper = rand (rator spec); 1052 val pre_wrapper = (snd (pairSyntax.dest_pabs x_pre_wrapper)) handle HOL_ERR _ => x_pre_wrapper 1053 1054 val x_post = rand spec; 1055 val post = (snd (pairSyntax.dest_pabs x_post)) handle HOL_ERR _ => x_post 1056 val abs_post = pairSyntax.mk_pabs (pv, post) 1057 1058 val wrapper_argL = snd (strip_comb pre_wrapper); 1059 val (argL1_term,_) = listSyntax.dest_list (el 1 wrapper_argL); 1060 val (argL2_term,_) = listSyntax.dest_list (el 2 wrapper_argL); 1061 val argL1_string = map (fst o dest_var) argL1_term; 1062 val argL2_string = map (fst o dest_var) argL2_term; 1063 1064 val argL1_const = map (fn n => mk_comb (holfoot_var_term, stringLib.fromMLstring n)) argL1_string; 1065 val argL2_const = map (fn n => mk_var (n, numSyntax.num)) argL2_string 1066 1067 val argL_term = pairLib.mk_pair 1068 (listSyntax.mk_list (argL1_const, ``:holfoot_var``), 1069 listSyntax.mk_list (argL2_const, numSyntax.num)); 1070 1071 val body_term = mk_comb (abs_body, argL_term); 1072 1073 val pre_term = mk_comb (el 3 wrapper_argL, argL_term); 1074 val post_term = mk_comb (abs_post, argL_term); 1075 1076 1077 fun term_simp t = (rhs o concl) (SIMP_CONV list_ss [bagTheory.BAG_UNION_INSERT, bagTheory.BAG_UNION_EMPTY] t) 1078 val body_term' = term_simp body_term; 1079 val pre_term' = term_simp pre_term; 1080 val post_term' = term_simp post_term; 1081 1082 val assume_opt = if same_const assume_opt_term T then true else false; 1083 in 1084 (assume_opt, fun_name, argL_term, pre_term', body_term', post_term') 1085 end 1086 1087 val funtL_term = (fst (listSyntax.dest_list funL)); 1088 val funtL = map funt_preprocess funtL_term; 1089 1090 fun umap f [] = nothing 1091 | umap f (x::xs) = (f x) >> (umap f xs); 1092 in 1093 ublock CONSISTENT 0 ( 1094 ustyle [UserStyle "holfoot_alert_0"] ( 1095 add_string ("HOLFOOT_SPECIFICATION") 1096 ) >> 1097 add_string " " >> 1098 add_string "(" >> 1099 add_newline >> 1100 ublock CONSISTENT (!holfoot_pretty_printer_block_indent) ( 1101 add_newline >> 1102 (umap (fn (s,vars,prop) => ( 1103 ublock INCONSISTENT 0 ( 1104 add_string "resource" >> 1105 add_string " " >> 1106 ustyle [UserStyle "holfoot_alert_1"] ( 1107 add_string (stringLib.fromHOLstring s) 1108 ) >> 1109 add_break (1, (!holfoot_pretty_printer_block_indent)) >> 1110 sys (Top, Top, Top) (d - 1) vars >> 1111 add_break (1, (!holfoot_pretty_printer_block_indent)) >> 1112 add_string "{" >> 1113 sys (Top, Top, Top) (d - 1) prop >> 1114 add_string "}" >> 1115 add_newline >> 1116 add_newline 1117 ))) restL) >> 1118 (umap (fn (assume_opt, fun_name, argL_term, pre_term, body_term, post_term) => ( 1119 ublock INCONSISTENT 0 ( 1120 (if (not assume_opt) then (add_string "assume") else nothing) >> 1121 ustyle [UserStyle "holfoot_alert_1"] ( 1122 add_string (stringLib.fromHOLstring fun_name) 1123 ) >> 1124 holfoot_proccall_args_printer backend sys_raw (ppfns:term_pp_types.ppstream_funs) gravs (d - 1) argL_term >> 1125 (if (not assume_opt) then (add_newline >> add_string " ") 1126 else (add_break (1,2))) >> 1127 add_string "[" >> 1128 1129 ustyle [UserStyle "holfoot_spec"] ( 1130 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 1131 sys (Top, Top, Top) (d - 1) pre_term 1132 )) >> 1133 1134 add_string "]" >> 1135 (if assume_opt then ( 1136 add_string " " >> 1137 add_string "{" >> 1138 add_newline >> 1139 add_string " " >> 1140 1141 ublock INCONSISTENT 0 ( 1142 sys (Top, Top, Top) (d - 1) body_term 1143 ) >> 1144 1145 add_newline >> 1146 add_string "}") 1147 else nothing) >> 1148 (if (not assume_opt) then (add_newline >> add_string " ") 1149 else (add_string " ")) >> 1150 add_string "[" >> 1151 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 1152 ustyle [UserStyle "holfoot_spec"] ( 1153 sys (Top, Top, Top) (d - 1) post_term 1154 ) >> 1155 add_string "]" 1156 ) >> 1157 add_newline >> 1158 add_newline 1159 ))) funtL ) 1160 ) >> 1161 add_newline >> 1162 add_string ")" 1163 ) 1164 end; 1165 1166 1167 1168(* 1169val t = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 1170*) 1171fun holfoot_prop_is_equiv_false_printer GS backend (sys_raw : term_pp_types.sysprinter) (ppfns:term_pp_types.ppstream_funs) gravs d t = let 1172 open Portable term_pp_types smpp 1173 infix >> 1174 val {add_string,add_break,ublock,add_newline,ustyle,...} = ppfns 1175in 1176 if (is_VAR_RES_PROP_IS_EQUIV_FALSE t) orelse 1177 ((is_neg t) andalso (is_VAR_RES_PROP_IS_EQUIV_FALSE (dest_neg t))) then 1178 add_string "..." 1179 else 1180 raise term_pp_types.UserPP_Failed 1181end 1182 1183 1184(* 1185val t = find_term is_VAR_RES_FRAME_SPLIT (snd (top_goal ())) 1186*) 1187fun holfoot_frame_split_printer GS backend (sys_raw : term_pp_types.sysprinter) (ppfns:term_pp_types.ppstream_funs) gravs d t = let 1188 open Portable term_pp_types smpp 1189 infix >> 1190 val {add_string,add_break,ublock,add_newline,ustyle,...} = ppfns 1191 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 1192 val (f, rfc, wr, w', context, split, imp, restP) = dest_VAR_RES_FRAME_SPLIT t; 1193 val (mode, comment_opt) = pairSyntax.dest_pair rfc; 1194 val _ = if (aconv f holfoot_disjoint_fmap_union_term) then () else Feedback.fail(); 1195 1196 1197 fun fst_dest_bag t = (fst o bagSyntax.dest_bag) t handle HOL_ERR _ => [t]; 1198 val (wL, rL) = ((fn f => f ## f) fst_dest_bag) 1199 (pairSyntax.dest_pair wr) 1200 val wL' = fst_dest_bag w'; 1201 1202 fun wL_sys a b v = 1203 if not (mem v wL') then sys a b v else 1204 (add_string "!" >> (sys a b v)); 1205in 1206 ublock CONSISTENT 0 ( 1207 (if (optionSyntax.is_some comment_opt) then 1208 (ublock INCONSISTENT 0 ( 1209 ustyle [UserStyle "holfoot_comment"] ( 1210 add_string "/*" >> 1211 add_break (1,3) >> 1212 add_loc_add_string 3 add_string add_break 1213 (label_list2ML (optionSyntax.dest_some comment_opt)) >> 1214 add_break (1,0) >> 1215 add_string "*/" 1216 ) 1217 ) >> 1218 add_break (1,0)) else nothing) >> 1219 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 1220 add_string "[[w/r:" >> 1221 add_string " " >> 1222 pretty_print_list_sep "," (wL_sys, add_string, add_break) d wL >> 1223 add_string ";" >> 1224 add_break (1,0) >> 1225 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 1226 pretty_print_list_sep "," (sys, add_string, add_break) d rL >> 1227 add_string " " >> 1228 add_string "|" 1229 ) >> 1230 add_break (1,0) >> 1231 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 1232 ustyle [UserStyle "holfoot_frame_split___context"] ( 1233 pretty_print_list_sep " *" (sys, add_string, add_break) d (fst_dest_bag context) 1234 ) >> 1235 add_string " " >> 1236 add_string "|" 1237 ) >> 1238 add_break (1,0) >> 1239 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 1240 ustyle [UserStyle "holfoot_frame_split___split"] ( 1241 pretty_print_list_sep " *" (sys, add_string, add_break) d (fst_dest_bag split) 1242 ) >> 1243 add_string " " >> 1244 add_string "-->" 1245 ) >> 1246 add_break (1,0) >> 1247 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 1248 ustyle [UserStyle "holfoot_frame_split___imp"] ( 1249 pretty_print_list_sep " *" (sys, add_string, add_break) d (fst_dest_bag imp) 1250 ) >> 1251 (if (aconv mode T) then 1252 (add_string " " >> 1253 add_string "|" >> 1254 add_break (1,2) >> 1255 add_string "...") else nothing) >> 1256 add_string "]]" 1257 ) 1258 )) 1259end 1260 1261fun holfoot_cond_triple_printer GS backend sys_raw (ppfns:term_pp_types.ppstream_funs) gravs d t = let 1262 open Portable term_pp_types smpp 1263 infix >> 1264 val {add_string,add_break,ublock,add_newline,ustyle,...} = ppfns 1265 fun sys gravs d' = sys_raw {gravs = gravs, depth = d', binderp = false} 1266 1267 val (f, pre, prog, post) = dest_VAR_RES_COND_HOARE_TRIPLE t; 1268 val _ = if (aconv f holfoot_disjoint_fmap_union_term) then () else Feedback.fail(); 1269 1270 fun my_dest_var_res_prop p = let 1271 val (f', wr, re, b) = dest_var_res_prop (COND_PROP___STRONG_EXISTS_term_rewrite p); 1272 val _ = if (aconv f' holfoot_disjoint_fmap_union_term) then () else Feedback.fail(); 1273 val (wL, _) = bagSyntax.dest_bag wr 1274 val (rL, _) = bagSyntax.dest_bag re 1275 val (bL, _) = bagSyntax.dest_bag b 1276 in 1277 (rL, wL, bL) 1278 end; 1279 1280 val (pre_readL, pre_writeL, pre_condL ) = my_dest_var_res_prop pre; 1281 val (post_readL, post_writeL, post_condL) = my_dest_var_res_prop post; 1282 1283 fun print_condition (wL, rL, cL) = ( 1284 ublock INCONSISTENT (!holfoot_pretty_printer_block_indent) ( 1285 ustyle [UserStyle "holfoot_spec"] ( 1286 add_string "[[w/r:" >> 1287 add_string " " >> 1288 pretty_print_list_sep "," (sys, add_string, add_break) d wL >> 1289 add_string ";" >> 1290 (if (null rL) then nothing else ( 1291 add_break (1,0) >> 1292 pretty_print_list_sep "," (sys, add_string, add_break) d rL 1293 )) >> 1294 add_string " " >> 1295 add_string "|" >> 1296 add_break (1,0) >> 1297 pretty_print_list_sep " *" (sys, add_string, add_break) d cL >> 1298 add_string "]]" 1299 ) 1300 )); 1301in 1302 ublock CONSISTENT (0) ( 1303 print_condition (pre_writeL, pre_readL, pre_condL) >> 1304 add_break (1,!holfoot_pretty_printer_block_indent) >> 1305 ublock CONSISTENT (!holfoot_pretty_printer_block_indent) ( 1306 sys (Top, Top, Top) (d - 1) prog 1307 ) >> 1308 add_newline >> 1309 print_condition (post_writeL, post_readL, post_condL) 1310 ) 1311end 1312 1313 1314val pretty_printer_list = 1315 [("holfoot_prop_is_equiv_false", ``VAR_RES_PROP_IS_EQUIV_FALSE c f wrb (sfb:holfoot_a_proposition -> num)``, holfoot_prop_is_equiv_false_printer), 1316 ("holfoot_prop_is_equiv_false", ``~(VAR_RES_PROP_IS_EQUIV_FALSE c f wrb (sfb:holfoot_a_proposition -> num))``, holfoot_prop_is_equiv_false_printer), 1317 ("holfoot_specification", ``ASL_SPECIFICATION holfoot_separation_combinator locks 1318 (procs : (bool # 'b # ('c -> ('c, 'a, 'b, holfoot_state) asl_program) # 1319 ('c -> ('c, 'a, 'b, holfoot_state) asl_program)) list)``, holfoot_specification_printer), 1320 ("holfoot_prog", ``prog:holfoot_program``, holfoot_prog_printer), 1321 ("holfoot_var", ``holfoot_var v``, holfoot_var_printer), 1322 ("holfoot_tag", ``holfoot_tag t``, holfoot_tag_printer), 1323 ("holfoot_expression", ``e:('a,'b,'c) var_res_expression``, holfoot_expression_printer), 1324 ("holfoot_pred", ``p:'a asl_predicate``, holfoot_pred_printer), 1325 ("holfoot_a_prop", ``x:'a set``, holfoot_a_prop_printer), 1326 ("holfoot_triple", ``VAR_RES_COND_HOARE_TRIPLE DISJOINT_FMAP_UNION pre (prog:holfoot_program) post``, holfoot_cond_triple_printer), 1327 ("holfoot_entails", ``VAR_RES_FRAME_SPLIT DISJOINT_FMAP_UNION mode wr w' 1328 frame split (imp:holfoot_a_proposition -> num) pred``, holfoot_frame_split_printer) 1329 ]:(string * Parse.term * term_grammar.userprinter) list; 1330 1331val use_holfoot_pp = ref true 1332val _ = Feedback.register_btrace ("use holfoot_pp", use_holfoot_pp); 1333 1334fun trace_user_printer (up:term_grammar.userprinter) = 1335 (fn GS => fn sys => fn ppfns => fn gravs => fn d => fn pps => fn t => 1336 if (!use_holfoot_pp) then 1337 (up GS sys ppfns gravs d pps t) 1338 handle Interrupt => raise Interrupt 1339 | _ => raise term_pp_types.UserPP_Failed 1340 else 1341 raise term_pp_types.UserPP_Failed):term_grammar.userprinter 1342 1343 1344val pretty_printer_list_trace = map (fn (s, t, p) => 1345 (s, t, trace_user_printer p)) pretty_printer_list 1346val _ = app (fn (s,_,c) => term_grammar.userSyntaxFns.register_userPP 1347 {name = s, code = c}) 1348 pretty_printer_list_trace 1349 1350fun aup (s,pat,code) = 1351 (add_ML_dependency "holfoot_pp_print"; add_user_printer(s,pat)) 1352 1353fun temp_add_holfoot_pp () = 1354 (map temp_add_user_printer pretty_printer_list_trace; 1355 print "HOLFOOT pretty printing activated!\n"); 1356 1357fun temp_remove_holfoot_pp () = 1358 (map (temp_remove_user_printer o #1) pretty_printer_list_trace; 1359 print "HOLFOOT pretty printing deactivated!\n"); 1360 1361fun add_holfoot_pp_quiet () = 1362 (map aup pretty_printer_list_trace;()); 1363 1364fun add_holfoot_pp () = 1365 (add_holfoot_pp_quiet(); 1366 print "HOLFOOT pretty printing activated!\n"); 1367 1368fun remove_holfoot_pp_quiet () = 1369 (map (remove_user_printer o #1) pretty_printer_list_trace;()); 1370 1371fun remove_holfoot_pp () = 1372 (remove_holfoot_pp_quiet (); 1373 print "HOLFOOT pretty printing deactivated!\n"); 1374 1375 1376(* 1377open holfootParser 1378open holfoot_pp_print 1379val file = concat [examplesDir, "/automatic/list.sf"]; 1380val t = parse_holfoot_file file 1381 1382temp_remove_holfoot_pp ();temp_add_holfoot_pp ();t 1383temp_remove_holfoot_pp ();t 1384*) 1385 1386val _ = Feedback.set_trace "PPBackEnd use annotations" 0 1387val _ = add_holfoot_pp_quiet(); 1388 1389end 1390