1(*--------------------------------------------------------------------------- 2 Proving that definitions terminate. 3 ---------------------------------------------------------------------------*) 4 5structure TotalDefn :> TotalDefn = 6struct 7 8open HolKernel Parse boolLib pairLib basicSize DefnBase numSyntax 9 arithmeticTheory; 10 11structure Parse = struct 12 open Parse 13 val (Type,Term) = parse_from_grammars arithmeticTheory.arithmetic_grammars 14end 15open Parse 16 17val ERR = mk_HOL_ERR "TotalDefn"; 18val ERRloc = mk_HOL_ERRloc "TotalDefn"; 19val WARN = HOL_WARNING "TotalDefn"; 20 21(*---------------------------------------------------------------------------*) 22(* Misc. stuff that should be in Lib probably *) 23(*---------------------------------------------------------------------------*) 24 25fun max [] m = m 26 | max (h::t) m = max t (if h>m then h else m); 27 28fun take 0 L = [] 29 | take n (h::t) = h::take (n-1) t 30 | take n [] = raise ERR "take" "not enough elements"; 31 32fun copies x = 33 let fun repl 0 = [] 34 | repl n = x::repl (n-1) 35 in repl 36 end; 37 38(*---------------------------------------------------------------------------*) 39(* perms delivers all permutations of a list. By Peter Sestoft. *) 40(* Pinched from MoscowML distribution (examples/small/perms.sml). *) 41(*---------------------------------------------------------------------------*) 42 43local 44 fun accuperms [] tail res = tail :: res 45 | accuperms (x::xr) tail res = cycle [] x xr tail res 46 and cycle left mid [] tail res = accuperms left (mid::tail) res 47 | cycle left mid (right as r::rr) tail res = 48 cycle (mid::left) r rr tail (accuperms (left @ right) (mid::tail) res) 49in 50 fun perms xs = accuperms xs [] [] 51 fun permsn n = perms (List.tabulate(n, fn x => x+1)) 52end; 53 54(*---------------------------------------------------------------------------*) 55(* Remove duplicates in a set of terms, while keeping original order *) 56(*---------------------------------------------------------------------------*) 57 58fun rm x [] = [] 59 | rm x (h::t) = if aconv x h then rm x t else h::rm x t; 60 61fun mk_term_set [] = [] 62 | mk_term_set (h::t) = h::mk_set (rm h t); 63 64fun imk_var(i,ty) = mk_var("v"^Int.toString i,ty); 65 66(*---------------------------------------------------------------------------*) 67(* Basic syntax for WF relations *) 68(*---------------------------------------------------------------------------*) 69 70val inv_image_tm = prim_mk_const{Thy="relation",Name="inv_image"}; 71 72fun mk_inv_image(R,f) = 73 let val ty1 = fst(dom_rng(type_of R)) 74 val ty2 = fst(dom_rng(type_of f)) 75 in 76 list_mk_comb(inst[beta |-> ty1, alpha |-> ty2] inv_image_tm,[R,f]) 77 end; 78 79val WF_tm = prim_mk_const{Name = "WF", Thy="relation"}; 80 81val isWFR = same_const WF_tm o fst o strip_comb; 82 83fun get_WF tmlist = 84 pluck isWFR tmlist 85 handle HOL_ERR _ => raise ERR "get_WF" "unexpected termination condition"; 86 87fun K0 ty = mk_abs(mk_var("v",ty), numSyntax.zero_tm); 88 89(*---------------------------------------------------------------------------*) 90(* Takes [v1,...,vn] [i_j,...,i_m], where 1 <= i_j <= i_m <= n and returns *) 91(* *) 92(* inv_image ($< LEX ... LEX $<) *) 93(* (\(v1:ty1,...,vn:tyn). *) 94(* (size_of(tyi)(vi), ..., size_of(tym)(vm))) *) 95(*---------------------------------------------------------------------------*) 96 97fun list_mk_lex [] = raise ERR "list_mk_lex" "empty list" 98 | list_mk_lex [x] = x 99 | list_mk_lex L = end_itlist (curry pairSyntax.mk_lex) L; 100 101val nless_lex = list_mk_lex o copies numSyntax.less_tm; 102 103fun mk_lex_reln argvars sizedlist arrangement = 104 let val lex_comb = nless_lex (length sizedlist) 105 val pargvars = list_mk_pair argvars 106 in 107 mk_inv_image (lex_comb, mk_pabs(pargvars,list_mk_pair arrangement)) 108 end; 109 110 111(*---------------------------------------------------------------------------*) 112(* proper_subterm t1 t2 iff t1 is a proper subterm of t2. A record projn *) 113(* x.fld is a proper subterm of x. *) 114(*---------------------------------------------------------------------------*) 115 116fun is_recd_proj tm1 tm2 = 117 let val (proj,a) = dest_comb tm1 118 val aty = type_of a 119 val projlist = mapfilter 120 (fst o dest_comb o boolSyntax.lhs o snd o strip_forall o concl) 121 (TypeBase.accessors_of aty) 122 in TypeBase.is_record_type aty andalso mem proj projlist 123 end 124 handle HOL_ERR _ => false; 125 126fun proper_subterm tm1 tm2 = 127 not(aconv tm1 tm2) 128 andalso (Lib.can (find_term (aconv tm1)) tm2 129 orelse 130 is_recd_proj tm1 tm2); 131 132 133(*---------------------------------------------------------------------------*) 134(* Adjustable set of rewrites for doing termination proof. *) 135(*---------------------------------------------------------------------------*) 136 137val DIV_LESS_I = prove 138(``!n d. 0n < n /\ 1 < d ==> I(n DIV d) < I(n)``, 139 REWRITE_TAC[DIV_LESS,combinTheory.I_THM]); 140 141val MOD_LESS_I = prove 142(``!m n. 0n < n ==> I(m MOD n) < I(n)``, 143 REWRITE_TAC [MOD_LESS,combinTheory.I_THM]); 144 145val SUB_LESS_I = prove 146(``!m n. 0n < n /\ n <= m ==> I(m - n) < I(m)``, 147 REWRITE_TAC[SUB_LESS,combinTheory.I_THM]); 148 149val termination_simps = 150 ref [combinTheory.o_DEF, 151 combinTheory.I_THM, 152 prim_recTheory.measure_def, 153 relationTheory.inv_image_def, 154 pairTheory.LEX_DEF, 155 pairTheory.RPROD_DEF, 156 SUB_LESS_I,DIV_LESS_I,MOD_LESS_I]; 157 158(*---------------------------------------------------------------------------*) 159(* Adjustable set of WF theorems for doing WF proofs. *) 160(*---------------------------------------------------------------------------*) 161 162val WF_thms = 163 let open relationTheory prim_recTheory pairTheory 164 in 165 ref [WF_inv_image, WF_measure, WF_LESS, 166 WF_EMPTY_REL, WF_PRED, WF_RPROD, WF_LEX, WF_TC] 167 end; 168 169 170(*---------------------------------------------------------------------------*) 171(* Same as pairSimps.PAIR_ss, except more eager to force paired *) 172(* beta-reductions. For example, should reduce "(\(x,y). M x y) N" to *) 173(* "M (FST N) (SND N)" *) 174(*---------------------------------------------------------------------------*) 175 176val term_ss = 177 let open simpLib infix ++ 178 in boolSimps.bool_ss 179 ++ pairSimps.PAIR_ss 180 ++ pairSimps.paired_forall_ss 181 ++ pairSimps.paired_exists_ss 182 ++ pairSimps.gen_beta_ss 183 ++ rewrites [pairTheory.FORALL_PROD] 184 ++ numSimps.REDUCE_ss 185 ++ numSimps.ARITH_RWTS_ss 186 end; 187 188val term_dp_ss = 189 let open simpLib infix ++ 190 in term_ss ++ numSimps.ARITH_DP_ss 191 end; 192 193 194(*---------------------------------------------------------------------------*) 195(* Destruct R (x1,...,xn) (y1,...ym) into [(x1,y1), ... , (xn,yn)], *) 196(* where n and m need not be equal. *) 197(*---------------------------------------------------------------------------*) 198 199local 200fun foo [] _ = raise ERR "foo" "empty arg." 201 | foo _ [] = raise ERR "foo" "empty arg." 202 | foo [x] Y = [(x,pairSyntax.list_mk_pair Y)] 203 | foo X [y] = [(pairSyntax.list_mk_pair X, y)] 204 | foo (x::rst) (y::rst1) = (x,y)::foo rst rst1 205in 206fun dest tm = 207 let val Ryx = (snd o strip_imp o snd o strip_forall) tm 208 val (Ry, x) = dest_comb Ryx 209 val y = rand Ry 210 open pairSyntax 211 in 212 foo (spine_pair y) (spine_pair x) 213 end 214end; 215 216(*---------------------------------------------------------------------------*) 217(* Is a list-of-lists rectangular, filling in with false on short rows *) 218(*---------------------------------------------------------------------------*) 219 220fun fill n [] = copies false n 221 | fill n (h::t) = h::fill (n-1) t; 222 223fun rectangular L = 224 let val lens = map length L 225 in case Lib.mk_set lens 226 of [] => raise ERR "rectangular" "impossible" 227 | [x] => L 228 | _ => map (fill (max lens 0)) L 229 end; 230 231(*---------------------------------------------------------------------------*) 232(* For each column, return true if every element is true. *) 233(*---------------------------------------------------------------------------*) 234 235fun apply_pred_to_cols P L = 236 if all null L then [] 237 else P (map (Lib.trye hd) L)::apply_pred_to_cols P (map (Lib.trye tl) L); 238 239(*---------------------------------------------------------------------------*) 240(* For each column, return true if every element is true. *) 241(* For each column, if any entry in the column is true, then return true. *) 242(*---------------------------------------------------------------------------*) 243 244val all_true_in_cols = apply_pred_to_cols (all I); 245val some_true_in_cols = apply_pred_to_cols (exists I); 246 247(*---------------------------------------------------------------------------*) 248(* After first true in a list, turn everything false. *) 249(*---------------------------------------------------------------------------*) 250 251fun fix [] = [] 252 | fix (true::t) = true::map (K false) t 253 | fix (false::t) = false::fix t; 254 255(*---------------------------------------------------------------------------*) 256(* Make L0 rectangular then try to find and mark first column where *) 257(* predicate holds. If there is such, mark all later cols false. Otherwise, *) 258(* collect all columns where predicate holds at least once. *) 259(*---------------------------------------------------------------------------*) 260 261fun projects L0 = 262 let val L = rectangular L0 263 val col_trues = all_true_in_cols L 264 in 265 if exists I col_trues then fix col_trues else some_true_in_cols L 266 end; 267 268(*---------------------------------------------------------------------------*) 269(* Collect all columns where some change happens. *) 270(*---------------------------------------------------------------------------*) 271 272fun column_summaries L = some_true_in_cols (rectangular L); 273 274(*---------------------------------------------------------------------------*) 275(* Identify columns where P holds *) 276(*---------------------------------------------------------------------------*) 277 278fun nth P [] _ N = rev N 279 | nth P (h::t) n N = nth P t (n+1) (if P h then n::N else N); 280 281(*---------------------------------------------------------------------------*) 282(* Take apart a product type with respect to a list of terms *) 283(*---------------------------------------------------------------------------*) 284 285fun strip_prod_ty [] _ = raise ERR "strip_prod_ty" "" 286 | strip_prod_ty [x] ty = [(x,ty)] 287 | strip_prod_ty (h::t) ty = 288 let val (x,y) = with_exn pairSyntax.dest_prod ty 289 (ERR "strip_prod_ty" "expected a product type") 290 in (h,x)::strip_prod_ty t y 291 end 292 293fun list_mk_prod_tyl L = 294 let val (front,(b,last)) = front_last L 295 val tysize = TypeBasePure.type_size (TypeBase.theTypeBase()) 296 val last' = (if b then tysize else K0) last 297 handle e => Raise (wrap_exn "TotalDefn" "last'" e) 298 in 299 itlist (fn (b,ty1) => fn M => 300 let val x = mk_var("x",ty1) 301 val y = mk_var("y",fst(dom_rng (type_of M))) 302 val blagga = (if b then tysize else K0) ty1 303 in 304 mk_pabs(mk_pair(x,y), 305 numSyntax.mk_plus(mk_comb(blagga,x),mk_comb(M,y))) 306 end) front last' 307 end 308 309(*---------------------------------------------------------------------------*) 310(* Construct all lex combos corresponding to permutations of list *) 311(*---------------------------------------------------------------------------*) 312 313fun mk_sized_subsets argvars sizedlist = 314 let val permutations = 315 if length sizedlist > 4 316 then (WARN "mk_sized_subsets" 317 "too many permutations (more than 24): chopping some"; 318 perms (take 4 sizedlist)) 319 else perms sizedlist 320 in 321 map (mk_lex_reln argvars sizedlist) permutations 322 handle HOL_ERR _ => [] 323 end; 324 325(*---------------------------------------------------------------------------*) 326(* Simplify guessed relations *) 327(*---------------------------------------------------------------------------*) 328 329val simplifyR = 330 let open prim_recTheory basicSizeTheory reduceLib simpLib 331 val expand = QCONV (SIMP_CONV term_ss 332 [measure_def,pair_size_def,bool_size_def,one_size_def]) 333 in 334 rhs o concl o expand 335 end; 336 337(*---------------------------------------------------------------------------*) 338(* "guessR" guesses a list of termination measures. Quite ad hoc. *) 339(* First guess covers recursions on proper subterms, e.g. prim. recs. Next *) 340(* guess measure sum of sizes of all arguments. Next guess generates *) 341(* lex-combos for Ackermann-style iterated prim. rec. defs. Finally, *) 342(* generate all lex combinations of arguments that get changed by known *) 343(* functions, i.e., ones that have corresponding theorems in ref variable *) 344(* "termination_simps". *) 345(* Finally, all generated termination relations are simplified and *) 346(* duplicates are weeded out. *) 347(*---------------------------------------------------------------------------*) 348 349fun known_fun tm = 350 let fun dest_order x = dest_less x handle HOL_ERR _ => dest_leq x 351 fun get_lhs th = 352 rand (fst(dest_order(snd(strip_imp 353 (snd(strip_forall(concl th))))))) 354 val pats = mapfilter get_lhs (!termination_simps) 355 in 356 0 < length (mapfilter (C match_term tm) pats) 357 end; 358 359fun relevant (tm,_) = known_fun tm; 360 361fun guessR defn = 362 let open Defn numSyntax simpLib boolSimps 363 fun tysize ty = TypeBasePure.type_size (TypeBase.theTypeBase()) ty 364 fun size_app v = mk_comb(tysize (type_of v),v) 365 in 366 if null (tcs_of defn) then [] 367 else 368 case reln_of defn 369 of NONE => [] 370 | SOME R => 371 let val domty = fst(dom_rng(type_of R)) 372 val (_,tcs0) = Lib.pluck isWFR (tcs_of defn) 373 val tcs = map (rhs o concl o QCONV (SIMP_CONV bool_ss [])) tcs0 374 val tcs = filter (not o equal T) tcs 375 val matrix = map dest tcs 376 val check1 = map (map (uncurry proper_subterm)) matrix 377 val chf1 = projects check1 378 val domtyl_1 = strip_prod_ty chf1 domty 379 val domty0 = list_mk_prod_tyl domtyl_1 380 (* deal with possible iterated prim_rec *) 381 val indices_1 = Lib.upto 1 (length domtyl_1) 382 val (argvars_1,subset_1) = 383 itlist2 (fn i => fn (b,ty) => fn (alist,slist) => 384 let val v = imk_var(i,ty) 385 in (v::alist, if b then size_app v::slist else slist) 386 end) indices_1 domtyl_1 ([],[]) 387 val it_prim_rec = [mk_lex_reln argvars_1 subset_1 subset_1] 388 handle HOL_ERR _ => [] 389 (* deal with other lex. combos *) 390 val check2 = map (map relevant) matrix 391 val chf2 = column_summaries check2 392 val domtyl_2 = strip_prod_ty chf2 domty 393 val indices = Lib.upto 1 (length domtyl_2) 394 val (argvars,subset) = 395 itlist2 (fn i => fn (b,ty) => fn (alist,slist) => 396 let val v = imk_var(i,ty) 397 in (v::alist, if b then size_app v::slist else slist) 398 end) indices domtyl_2 ([],[]) 399 val lex_combs = mk_sized_subsets argvars subset 400 val allrels = [mk_cmeasure domty0, mk_cmeasure (tysize domty)] 401 @ it_prim_rec @ lex_combs 402 val allrels' = mk_term_set (map simplifyR allrels) 403 in 404 allrels' 405 end 406end 407 handle e => raise wrap_exn "TotalDefn" "guessR" e; 408 409(*---------------------------------------------------------------------------*) 410(* Wellfoundedness and termination provers (parameterized by theorems). *) 411(* The default TC simplifier and prover is terribly terribly naive, but *) 412(* still useful. It knows all about the sizes of types. *) 413(*---------------------------------------------------------------------------*) 414 415(*---------------------------------------------------------------------------*) 416(* Wellfoundedness prover for combinations of wellfounded relations. *) 417(*---------------------------------------------------------------------------*) 418 419fun BC_TAC th = 420 if is_imp (#2 (strip_forall (concl th))) 421 then MATCH_ACCEPT_TAC th ORELSE MATCH_MP_TAC th 422 else MATCH_ACCEPT_TAC th; 423 424fun PRIM_WF_TAC thl = REPEAT (MAP_FIRST BC_TAC thl ORELSE CONJ_TAC); 425fun WF_TAC g = PRIM_WF_TAC (!WF_thms) g; 426 427(*--------------------------------------------------------------------------*) 428(* Basic simplification and proof for remaining termination conditions. *) 429(*--------------------------------------------------------------------------*) 430 431fun get_orig (TypeBasePure.ORIG th) = th 432 | get_orig _ = raise ERR "get_orig" "not the original" 433 434fun PRIM_TC_SIMP_CONV simps = 435 let val els = TypeBasePure.listItems (TypeBase.theTypeBase()) 436 val size_defs = 437 mapfilter (get_orig o #2 o valOf o TypeBasePure.size_of0) els 438 val case_defs = mapfilter TypeBasePure.case_def_of els 439 in 440 simpLib.SIMP_CONV term_ss (simps@size_defs@case_defs) 441 end; 442 443fun TC_SIMP_CONV tm = PRIM_TC_SIMP_CONV (!termination_simps) tm; 444 445val ASM_ARITH_TAC = 446 REPEAT STRIP_TAC 447 THEN REPEAT (POP_ASSUM 448 (fn th => if numSimps.is_arith (concl th) 449 then MP_TAC th else ALL_TAC)) 450 THEN CONV_TAC Arith.ARITH_CONV; 451 452fun PRIM_TC_SIMP_TAC thl = 453 CONV_TAC (PRIM_TC_SIMP_CONV thl) THEN TRY ASM_ARITH_TAC; 454 455fun TC_SIMP_TAC g = PRIM_TC_SIMP_TAC (!termination_simps) g; 456 457fun PRIM_TERM_TAC wftac tctac = CONJ_TAC THENL [wftac,tctac] 458 459val STD_TERM_TAC = PRIM_TERM_TAC WF_TAC TC_SIMP_TAC; 460 461local 462 fun mesg tac (g as (_,tm)) = 463 (if !Defn.monitoring then 464 print(String.concat["\nCalling ARITH on\n",term_to_string tm,"\n"]) 465 else () ; 466 tac g) 467in 468fun PROVE_TERM_TAC g = 469 let open combinTheory simpLib 470 val simps = map (PURE_REWRITE_RULE [I_THM]) (!termination_simps) 471 val ss = term_dp_ss ++ rewrites simps 472 in 473 PRIM_TERM_TAC WF_TAC 474 (CONV_TAC TC_SIMP_CONV THEN BasicProvers.PRIM_STP_TAC ss NO_TAC) 475 end g 476end; 477 478 479(*---------------------------------------------------------------------------*) 480(* Instantiate the termination relation with q and then try to prove *) 481(* wellfoundedness and remaining termination conditions. *) 482(*---------------------------------------------------------------------------*) 483 484fun PRIM_WF_REL_TAC q WFthms simps g = 485 (Q.EXISTS_TAC q THEN CONJ_TAC THENL 486 [PRIM_WF_TAC WFthms, PRIM_TC_SIMP_TAC simps]) g; 487 488fun WF_REL_TAC q = Q.EXISTS_TAC q THEN STD_TERM_TAC; 489 490 491(*--------------------------------------------------------------------------- 492 Definition principles that automatically attempt 493 to prove termination. If the termination proof 494 fails, the definition attempt fails. 495 ---------------------------------------------------------------------------*) 496 497fun reln_is_not_set defn = 498 case Defn.reln_of defn 499 of NONE => false 500 | SOME R => is_var R; 501 502fun proveTotal tac defn = 503 let val (WFR,rest) = get_WF (Defn.tcs_of defn) 504 val form = list_mk_conj(WFR::rest) 505 val thm = Tactical.default_prover(form,tac) 506 in 507 (Defn.elim_tcs defn (CONJUNCTS thm), SOME thm) 508 end; 509 510local open Defn 511 val auto_tgoal = ref true 512 val () = Feedback.register_btrace("auto Defn.tgoal", auto_tgoal) 513 514 fun should_try_to_prove_termination defn rhs_frees = 515 let 516 val tcs = tcs_of defn 517 in 518 not(null tcs) andalso null (intersect (free_varsl tcs) rhs_frees) 519 end 520 fun fvs_on_rhs V = 521 let 522 val Vstr = 523 String.concat (Lib.commafy (map (Lib.quote o #1 o dest_var) V)) 524 in 525 if !allow_schema_definition 526 then () 527 else raise ERR "defnDefine" 528 (" The following variables are free in the \n right hand side of\ 529 \ the proposed definition: " ^ Vstr) 530 end 531 val msg1 = "\nUnable to prove termination!\n\n\ 532 \Try using \"TotalDefn.tDefine <name> <quotation> <tac>\".\n" 533 val msg2 = "\nThe termination goal has been set up using Defn.tgoal <defn>.\n" 534 fun termination_proof_failed defn = 535 let 536 val s = 537 if !auto_tgoal 538 then (Defn.tgoal defn 539 ; PP.prettyPrint 540 (TextIO.print, !Globals.linewidth) 541 (proofManagerLib.pp_proof (proofManagerLib.p())) 542 ; if !Globals.interactive then msg2 else "") 543 else "" 544 in 545 raise ERR "defnDefine" (msg1 ^ s) 546 end 547in 548 fun defnDefine term_tac defn = 549 let 550 val V = params_of defn 551 val _ = if not (null V) then fvs_on_rhs V else () (* can fail *) 552 val tprover = proveTotal term_tac 553 fun try_proof defn Rcand = tprover (set_reln defn Rcand) 554 val (defn',opt) = 555 if should_try_to_prove_termination defn V 556 then ((if reln_is_not_set defn 557 then Lib.tryfind (try_proof defn) (guessR defn) 558 else tprover defn) 559 handle HOL_ERR _ => termination_proof_failed defn) 560 else (defn,NONE) 561 in 562 save_defn defn' 563 ; (LIST_CONJ (map GEN_ALL (eqns_of defn')), ind_of defn', opt) 564 end 565end 566 567val primDefine = defnDefine PROVE_TERM_TAC; 568 569(*---------------------------------------------------------------------------*) 570(* Make a definition, giving the name to store things under. If anything *) 571(* fails in the process, remove any constants introduced by the definition. *) 572(*---------------------------------------------------------------------------*) 573 574fun xDefine stem q = 575 Parse.try_grammar_extension 576 (Theory.try_theory_extension 577 (#1 o primDefine o Defn.Hol_defn stem)) q 578 handle e => Raise (wrap_exn "TotalDefn" "xDefine" e); 579 580(*--------------------------------------------------------------------------- 581 Define 582 ---------------------------------------------------------------------------*) 583 584local 585 fun msg alist invoc = 586 String.concat 587 ["Definition failed! Can't make name for storing definition\n", 588 "because there is no alphanumeric identifier in: \n\n ", 589 wfrecUtils.list_to_string Lib.quote "," alist, 590 ".\n\nTry \"",invoc, "\" instead.\n\n"] 591 fun mk_bindstem exn invoc alist = 592 Lib.first Lexis.ok_identifier alist 593 handle HOL_ERR _ => (Lib.say (msg alist invoc); raise exn) 594in 595 fun define q = 596 let 597 val absyn0 = Parse.Absyn q 598 val locn = Absyn.locn_of_absyn absyn0 599 val (tm,names) = Defn.parse_absyn absyn0 600 val bindstem = 601 mk_bindstem (ERRloc "Define" locn "") "Define <quotation>" names 602 in 603 #1 (primDefine (Defn.mk_defn bindstem tm)) 604 handle e => raise (wrap_exn_loc "TotalDefn" "Define" locn e) 605 end 606 607 (* Use of Raise means that typecheck error exceptions will get printed 608 anyway; no need to also have the code in Preterm etc print them out 609 as well. *) 610 611 fun Define q = 612 trace ("show_typecheck_errors", 0) 613 (Parse.try_grammar_extension (Theory.try_theory_extension define)) 614 q 615 handle e => Raise e 616end 617 618(*---------------------------------------------------------------------------*) 619(* Version of Define where the termination tactic is explicitly supplied. *) 620(*---------------------------------------------------------------------------*) 621 622fun tDefine stem q tac = 623 let open Defn 624 fun thunk() = 625 let val defn = Hol_defn stem q 626 in 627 if triv_defn defn 628 then let val def = fetch_eqns defn 629 val bind = stem ^ !Defn.def_suffix 630 in been_stored (bind,def); def 631 end 632 else let val (def,ind) = with_flag (proofManagerLib.chatting,false) 633 Defn.tprove0(defn,tac) 634 val def = def |> CONJUNCTS |> map GEN_ALL |> LIST_CONJ 635 in Defn.store(stem,def,ind) ; def 636 end 637 end 638 in 639 Parse.try_grammar_extension 640 (Theory.try_theory_extension thunk) () 641 handle e => Raise (wrap_exn "TotalDefn" "tDefine" e) 642 end; 643 644(*---------------------------------------------------------------------------*) 645(* Version of Define that supports multiple definitions, failing if any do. *) 646(*---------------------------------------------------------------------------*) 647 648fun multidefine q = List.map (#1 o primDefine) (Defn.Hol_multi_defns q) 649 650fun multiDefine q = 651 Parse.try_grammar_extension (Theory.try_theory_extension multidefine) q 652 handle e => Raise e; 653 654(*---------------------------------------------------------------------------*) 655(* API for Define *) 656(*---------------------------------------------------------------------------*) 657 658datatype phase 659 = PARSE of term quotation 660 | BUILD of term 661 | TERMINATION of defn; 662 663type apidefn = (defn * thm option, phase * exn) Lib.verdict 664 665 666(*---------------------------------------------------------------------------*) 667(* Turn off printing of messages by the HOL system for the duration of the *) 668(* invocation of f. *) 669(*---------------------------------------------------------------------------*) 670 671fun silent f = 672 Lib.with_flag(Lib.saying,false) 673 (Lib.with_flag(Feedback.emit_WARNING,false) 674 (Lib.with_flag(Feedback.emit_MESG,false) f)); 675 676(*---------------------------------------------------------------------------*) 677(* Instantiate the termination conditions of a defn with a relation and *) 678(* attempt to prove termination. Note that this includes having to prove *) 679(* that the supplied relation is well-founded. *) 680(*---------------------------------------------------------------------------*) 681 682fun tryR tac defn = proveTotal tac o Defn.set_reln defn; 683 684(*---------------------------------------------------------------------------*) 685(* Given a guesser of termination relations and a prover for termination *) 686(* conditions, try the guesses until the prover succeeds. Return the proved *) 687(* termination conditions as a theorem, along with the tc-free defn. *) 688(*---------------------------------------------------------------------------*) 689 690fun elimTCs guessR tac defn = 691 case guessR defn 692 of [] => (defn,NONE) (* prim. rec. or non-rec. defn *) 693 | guesses => Lib.tryfind (tryR tac defn) guesses; 694 695(*---------------------------------------------------------------------------*) 696(* Sequence the phases of definition, starting from a stem and a term *) 697(*---------------------------------------------------------------------------*) 698 699fun apiDefine guessR tprover (stem,tm) = 700 PASS tm ?> verdict (Defn.mk_defn stem) BUILD 701 ?> verdict (elimTCs guessR tprover) TERMINATION; 702 703(*---------------------------------------------------------------------------*) 704(* Sequence the phases of definition, starting from a quotation *) 705(*---------------------------------------------------------------------------*) 706 707fun stem eqn = (fst (dest_const (fst (strip_comb (lhs eqn)))),eqn) 708 709fun apiDefineq guessR tprover q = 710 PASS q ?> verdict (silent (stem o hd o Defn.parse_quote)) PARSE 711 ?> apiDefine guessR tprover; 712 713(*---------------------------------------------------------------------------*) 714(* Instantiate to the current guesser and terminator *) 715(*---------------------------------------------------------------------------*) 716 717val std_apiDefine = apiDefine guessR PROVE_TERM_TAC; 718val std_apiDefineq = apiDefineq guessR PROVE_TERM_TAC; 719 720(*--------------------------------------------------------------------------- 721 Special entrypoints for defining schemas 722 ---------------------------------------------------------------------------*) 723 724fun xDefineSchema stem = 725 with_flag(allow_schema_definition,true) (xDefine stem); 726 727val DefineSchema = 728 with_flag(allow_schema_definition,true) Define; 729 730end 731