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