1(*--------------------------------------------------------------------------- 2 * A bunch of functions that fold quotation parsing in, sometimes to good 3 * effect. 4 *---------------------------------------------------------------------------*) 5structure Q :> Q = 6struct 7 8open HolKernel boolLib; 9 10type tmquote = term quotation 11type tyquote = hol_type quotation 12 13val ERR = mk_HOL_ERR "Q"; 14 15val ptm = Parse.Term 16val pty = Parse.Type; 17val ty_antiq = Parse.ty_antiq; 18 19fun normalise_quotation frags = 20 case frags of 21 [] => [] 22 | [x] => [x] 23 | (QUOTE s1::QUOTE s2::rest) => normalise_quotation (QUOTE (s1^s2) :: rest) 24 | x::xs => x :: normalise_quotation xs 25 26fun contextTerm ctxt q = Parse.parse_in_context ctxt (normalise_quotation q); 27 28fun ptm_with_ctxtty ctxt ty q = Parse.typed_parse_in_context ty ctxt q 29 30fun TC_OFF f x = trace ("show_typecheck_errors", 0) f x 31fun ptm_with_ctxtty' ctxt ty = TC_OFF (ptm_with_ctxtty ctxt ty) 32 33 34fun ptm_with_ty q ty = ptm_with_ctxtty [] ty q; 35fun btm q = ptm_with_ty q Type.bool 36 37fun mk_term_rsubst ctxt = let 38 (* rely on the fact that the ctxt will be the free variables of the term/thm 39 that is going to be worked over by the subst *) 40 fun f {redex,residue} = let 41 val redex' = contextTerm ctxt redex 42 in 43 if op_mem aconv redex' ctxt then let 44 val residue' = ptm_with_ctxtty ctxt (type_of redex') residue 45 in 46 SOME (redex' |-> residue') 47 end 48 else NONE 49 50 end 51in 52 List.mapPartial f 53end 54 55val mk_type_rsubst = map (fn {redex,residue} => (pty redex |-> pty residue)); 56 57fun store_thm(s,q,t) = boolLib.store_thm(s,btm q,t); 58fun prove (q, t) = Tactical.prove(btm q,t); 59fun new_definition(s,q) = Definition.new_definition(s,btm q); 60fun new_infixl_definition(s,q,f) = boolLib.new_infixl_definition(s,btm q,f); 61fun new_infixr_definition(s,q,f) = boolLib.new_infixr_definition(s,btm q,f); 62 63val ABS = Thm.ABS o ptm; 64val BETA_CONV = Thm.BETA_CONV o ptm; 65val REFL = Thm.REFL o ptm; 66 67fun DISJ1 th = Thm.DISJ1 th o btm; 68val DISJ2 = Thm.DISJ2 o btm; 69 70fun GEN [QUOTE s] th = 71 let val V = free_vars (concl th) 72 in case Lib.assoc2 (Lib.deinitcomment s) 73 (Lib.zip V (map (fst o Term.dest_var) V)) 74 of NONE => raise ERR "GEN" "variable not found" 75 | SOME (v,_) => Thm.GEN v th 76 end 77 | GEN _ _ = raise ERR "GEN" "unexpected quote format" 78 79fun GENL qs th = List.foldr (fn (q,th) => GEN q th) th qs 80 81fun SPEC q = 82 W(Thm.SPEC o ptm_with_ty q o (type_of o fst o dest_forall o concl)); 83 84val SPECL = rev_itlist SPEC; 85val ISPEC = Drule.ISPEC o ptm; 86val ISPECL = Drule.ISPECL o map ptm; 87val ID_SPEC = W(Thm.SPEC o (fst o dest_forall o concl)) 88 89fun em_getState s = errormonad.Some((s,s)) 90fun sm_getState s = seq.result(s,s) 91 92fun SPEC_THEN q ttac thm (g as (asl,w)) = let 93 infix >>- >>~ 94 fun em >>- f = let open errormonad in em >- f end 95 fun sm >>~ f = let open seqmonad in sm >- f end 96 val a = Parse.Absyn q 97 val ctxt = HOLset.listItems (hyp_frees thm) @ free_varsl(w::asl) 98 val (Bvar,_) = dest_forall (concl thm) 99 val bty = type_of Bvar 100 val pbty0 = Pretype.fromType bty 101 val fixed_tyvars = hyp_tyvars thm |> HOLset.listItems 102 val pbty = Pretype.rename_typevars (List.map dest_vartype fixed_tyvars) pbty0 103 val fixup_map0 = 104 let open errormonad 105 in 106 pbty >>- (fn pty => 107 Pretype.unify pbty0 pty >> 108 em_getState >>- (return o Pretype.Env.toList)) 109 end Pretype.Env.empty 110 val fixup_map = 111 case fixup_map0 of 112 errormonad.Some(_, alist) => 113 List.map (fn (i,v) => (Pretype.toType (valOf v) |-> i)) alist 114 | _ => raise Fail "SPEC_THEN invariant failure" 115 fun parse_with_unify_check a = 116 let 117 val ptmm = TermParse.absyn_to_preterm (Parse.term_grammar()) a 118 open Preterm seqmonad 119 val printers = SOME (term_to_string, type_to_string) 120 in 121 fromErr pbty >>~ (fn pty => 122 fromErr ptmm >>~ (fn ptm => 123 fromErr 124 (TermParse.ctxt_preterm_to_term printers NONE ctxt 125 (Constrained{Locn = locn.Loc_None,Ptm = ptm, Ty = pty})))) 126 end 127 fun Ecompose theta0 E = 128 List.mapPartial 129 (fn {redex,residue} => 130 case Pretype.toTypeM (Pretype.UVar residue) E of 131 errormonad.Some(_, ty) => SOME{redex=redex, residue = ty} 132 | _ => NONE) 133 theta0 134 fun inst_spec_n_ttac t = 135 let 136 open seqmonad 137 in 138 sm_getState >>~ (fn env => 139 let val theta = Ecompose fixup_map env 140 in 141 case Lib.total ttac (Thm.SPEC t (INST_TYPE theta thm)) of 142 NONE => fail 143 | SOME tac => (case Lib.total tac g of 144 NONE => fail 145 | SOME result => return result) 146 end) 147 end 148 val sm = parse_with_unify_check a >>~ inst_spec_n_ttac 149in 150 case seq.cases (sm Pretype.Env.empty) of 151 NONE => raise ERR "SPEC_THEN" "No parse succeeds" 152 | SOME ((_, res),_) => res 153end 154 155val SPEC_THEN : term quotation -> thm_tactic -> thm_tactic = SPEC_THEN; 156 157fun SPECL_THEN ql = 158 case ql of 159 [] => ALL_THEN 160 | q::qs => SPEC_THEN q THEN_TCL SPECL_THEN qs 161 162fun ISPEC_THEN q ttac thm g = Q_TAC (fn t => ttac (Drule.ISPEC t thm)) q g 163 164fun goal_ctxt (asl,w) = free_varsl (w::asl) 165 166fun seq_mmap mf list = 167 case list of 168 [] => seq.result [] 169 | x::xs => seq.bind (mf x) 170 (fn x' => 171 seq.bind (seq_mmap mf xs) 172 (fn xs' => seq.result (x'::xs'))) 173 174fun ISPECL_THEN ql ttac thm g = 175 let 176 open Parse TermParse 177 val ctxt = goal_ctxt g 178 fun tf q = prim_ctxt_termS Absyn (term_grammar()) ctxt q 179 val tl_s = seq_mmap tf ql 180 in 181 case seq.cases tl_s of 182 NONE => raise ERR "ISPECL_THEN" "No parse for quotation list" 183 | SOME _ => 184 let 185 fun f tl = SOME (ttac (Drule.ISPECL tl thm) g) 186 handle HOL_ERR _ => NONE 187 in 188 case seq.cases (seq.mapPartial f tl_s) of 189 NONE => raise ERR "ISPECL_THEN" "No parse leads to success" 190 | SOME (res, _) => res 191 end 192 end 193 194fun SPEC_TAC (q1,q2) (g as (asl,w)) = let 195 val ctxt = free_varsl (w::asl) 196 val T1 = Parse.parse_in_context ctxt q1 197 val T2 = ptm_with_ctxtty' ctxt (type_of T1) q2 198in 199 Tactic.SPEC_TAC(T1, T2) g 200end; 201 202(* Generalizes first free variable with given name to itself. *) 203 204fun ID_SPEC_TAC q (g as (asl,w)) = 205 let val ctxt = free_varsl (w::asl) 206 val tm = Parse.parse_in_context ctxt q 207 in 208 Tactic.SPEC_TAC (tm, tm) g 209 end 210 211fun EXISTS(q1,q2) thm = 212 let val tm1 = btm q1 213 val exvartype = type_of (fst (dest_exists tm1)) 214 handle HOL_ERR _ => raise ERR "EXISTS" "first quotation not an exists" 215 val tm2 = ptm_with_ty q2 exvartype 216 in 217 Thm.EXISTS (tm1,tm2) thm 218 end; 219 220fun EXISTS_TAC q (g as (asl, w)) = 221 let 222 val exvartype = type_of (fst (dest_exists w)) 223 handle HOL_ERR _ => raise ERR "EXISTS_TAC" "goal not an exists" 224 in 225 QTY_TAC exvartype (fn t => Tactic.EXISTS_TAC t) q g 226 end 227 228fun LIST_EXISTS_TAC qL = EVERY (map EXISTS_TAC qL) 229 230fun REFINE_EXISTS_TAC q (asl, w) = let 231 val (qvar, body) = dest_exists w 232 val ctxt = free_varsl (w::asl) 233 val t = ptm_with_ctxtty' ctxt (type_of qvar) q 234 val qvars = op_set_diff aconv (free_vars t) ctxt 235 val newgoal = subst [qvar |-> t] body 236 fun chl [] ttac = ttac 237 | chl (h::t) ttac = X_CHOOSE_THEN h (chl t ttac) 238in 239 SUBGOAL_THEN 240 (list_mk_exists(rev qvars, newgoal)) 241 (chl (rev qvars) (fn th => Tactic.EXISTS_TAC t THEN ACCEPT_TAC th)) 242 (asl, w) 243end 244 245fun X_CHOOSE_THEN q ttac thm (g as (asl,w)) = 246 let val ty = type_of (fst (dest_exists (concl thm))) 247 handle HOL_ERR _ => 248 raise ERR "X_CHOOSE_THEN" "provided thm not an exists" 249 in 250 QTY_TAC ty (fn t => Thm_cont.X_CHOOSE_THEN t ttac thm) q g 251 end 252 253val X_CHOOSE_TAC = C X_CHOOSE_THEN Tactic.ASSUME_TAC; 254 255fun DISCH q th = 256 let val (asl,c) = dest_thm th 257 val V = free_varsl (c::asl) 258 val tm = ptm_with_ctxtty V Type.bool q 259 in Thm.DISCH tm th 260 end; 261 262fun PAT_UNDISCH_TAC q (g as (asl,w)) = 263let val ctxt = free_varsl (w::asl) 264 val pat = ptm_with_ctxtty' ctxt Type.bool q 265 val asm = 266 first (can (ho_match_term [] Term.empty_tmset pat)) asl 267in Tactic.UNDISCH_TAC asm g 268end; 269 270fun PAT_ASSUM q ttac = 271 Q_TAC0 {traces = [("notify type variable guesses", 0)]} (SOME bool) 272 (fn t => Tactical.PAT_ASSUM t ttac) 273 q 274fun PAT_X_ASSUM q ttac = 275 Q_TAC0 {traces = [("notify type variable guesses", 0)]} (SOME bool) 276 (fn t => Tactical.PAT_X_ASSUM t ttac) 277 q 278 279fun SUBGOAL_THEN q ttac = 280 QTY_TAC Type.bool (fn t => Tactical.SUBGOAL_THEN t ttac) q 281 282val UNDISCH_TAC = QTY_TAC Type.bool Tactic.UNDISCH_TAC 283 284fun UNDISCH_THEN q ttac = 285 QTY_TAC Type.bool (fn t => Tactic.UNDISCH_TAC t THEN DISCH_THEN ttac) q 286 287fun hdtm_assum q ttac = Q_TAC (C Tactical.hdtm_assum ttac) q 288fun hdtm_x_assum q ttac = Q_TAC (C Tactical.hdtm_x_assum ttac) q 289 290val ASSUME = ASSUME o btm 291 292fun X_GEN_TAC q (g as (asl, w)) = 293 let 294 val ty = type_of (fst(dest_forall w)) 295 in 296 QTY_TAC ty Tactic.X_GEN_TAC q g 297 end 298 299fun X_FUN_EQ_CONV q tm = 300 let val ctxt = free_vars tm 301 val ty = #1 (dom_rng (type_of (lhs tm))) 302 in 303 Conv.X_FUN_EQ_CONV (ptm_with_ctxtty' ctxt ty q) tm 304 end 305 306fun skolem_ty tm = 307 let val (V,tm') = strip_forall tm 308 in if not (null V) 309 then list_mk_fun (map type_of V, type_of(fst(dest_exists tm'))) 310 else raise ERR"XSKOLEM_CONV" "no universal prefix" 311 end; 312 313fun X_SKOLEM_CONV q tm = 314 let val ctxt = free_vars tm 315 val ty = skolem_ty tm 316 in 317 Conv.X_SKOLEM_CONV (ptm_with_ctxtty ctxt ty q) tm 318 end 319 320fun AP_TERM q th = 321 let val ctxt = free_vars(concl th) 322 val tm = contextTerm ctxt q 323 val (ty,_) = dom_rng (type_of tm) 324 val (lhs,rhs) = dest_eq(concl th) 325 val theta = match_type ty (type_of lhs) 326 in 327 Thm.AP_TERM (Term.inst theta tm) th 328 end; 329 330fun AP_THM th q = 331 let val (lhs,rhs) = dest_eq(concl th) 332 val ty = fst (dom_rng (type_of lhs)) 333 val ctxt = free_vars (concl th) 334 in 335 Thm.AP_THM th (ptm_with_ctxtty ctxt ty q) 336 end; 337 338val ASM_CASES_TAC = QTY_TAC bool Tactic.ASM_CASES_TAC 339 340fun AC_CONV p = Conv.AC_CONV p o ptm; 341 342(* Could be smarter *) 343 344fun INST subst th = let 345 val ctxt = thm_frees th 346in 347 Thm.INST (mk_term_rsubst ctxt subst) th 348end 349val INST_TYPE = Thm.INST_TYPE o mk_type_rsubst; 350 351 352(*---------------------------------------------------------------------------*) 353(* Abbreviation tactics *) 354(*---------------------------------------------------------------------------*) 355 356fun ABBREV_TAC q (gl as (asl,w)) = 357 let val ctxt = free_varsl(w::asl) 358 val eq = Parse.parse_in_context ctxt q 359 in 360 markerLib.ABBREV_TAC eq 361 end gl; 362 363fun PAT_ABBREV_TAC q (gl as (asl,w)) = 364 let val fv_set = FVL (w::asl) empty_tmset 365 val ctxt = HOLset.listItems fv_set 366 val eq = Parse.parse_in_context ctxt q 367 in 368 markerLib.PAT_ABBREV_TAC fv_set eq 369 end gl; 370 371fun MATCH_ABBREV_TAC q (gl as (asl,w)) = 372 let val fv_set = FVL (w::asl) empty_tmset 373 val ctxt = HOLset.listItems fv_set 374 val pattern = ptm_with_ctxtty' ctxt bool q 375 in 376 markerLib.MATCH_ABBREV_TAC fv_set pattern 377 end gl; 378 379fun HO_MATCH_ABBREV_TAC q (gl as (asl,w)) = 380 let val fv_set = FVL (w::asl) empty_tmset 381 val ctxt = HOLset.listItems fv_set 382 val pattern = ptm_with_ctxtty' ctxt bool q 383in 384 markerLib.HO_MATCH_ABBREV_TAC fv_set pattern 385end gl; 386 387fun UNABBREV_TAC q (gl as (asl,w)) = 388 let val v = Parse.parse_in_context (free_varsl (w::asl)) q 389 in 390 markerLib.UNABBREV_TAC (fst(dest_var v)) 391 end gl; 392 393fun RM_ABBREV_TAC q (gl as (asl,w)) = 394 let val v = Parse.parse_in_context (free_varsl (w::asl)) q 395 in 396 markerLib.RM_ABBREV_TAC (fst(dest_var v)) 397 end gl; 398 399fun MATCH_ASSUM_ABBREV_TAC q (gl as (asl,w)) = 400 let val fv_set = FVL (w::asl) empty_tmset 401 val ctxt = HOLset.listItems fv_set 402 val pattern = ptm_with_ctxtty' ctxt bool q 403 in 404 markerLib.MATCH_ASSUM_ABBREV_TAC fv_set pattern 405 end gl; 406 407fun make_abbrev_tac s = 408 MAP_EVERY markerLib.ABB' (markerLib.safe_inst_sort s) 409 410(*---------------------------------------------------------------------------*) 411(* Renaming tactics *) 412(*---------------------------------------------------------------------------*) 413 414fun make_rename_tac s = 415 MAP_EVERY 416 (fn {redex=l,residue=r} => 417 CHOOSE_THEN SUBST_ALL_TAC 418 (Thm.EXISTS(mk_exists(l, mk_eq(r, l)), r) (Thm.REFL r))) 419 (Listsort.sort markerLib.safe_inst_cmp s) 420 421fun isnt_uscore_var v = let 422 val (s, _) = dest_var v 423in 424 size s <> 0 andalso String.sub(s, 0) <> #"_" 425end 426val strip_uscore_bindings = filter (fn {redex,residue} => isnt_uscore_var redex) 427fun redex_map f {redex,residue} = {redex = f redex, residue = residue} 428 429fun PQ (* parser quiet *) f = 430 f |> trace ("notify type variable guesses", 0) 431 |> trace ("show_typecheck_errors", 0) 432 433(* needs to be eta-expanded so that the possible HOL_ERRs are raised 434 when applied to a goal, not before, thereby letting FIRST_ASSUM catch 435 the exception *) 436fun wholeterm_rename_helper {pats,fvs_set,ERR,kont} tm g = let 437 fun do_one_pat pat = 438 let 439 val ((tmtheta0, _), (tytheta, _)) = 440 raw_match [] fvs_set pat tm ([],[]) 441 handle HOL_ERR _ => raise ERR "No match" 442 val rename_tac = 443 tmtheta0 |> strip_uscore_bindings |> map (redex_map (inst tytheta)) 444 |> make_rename_tac 445 in 446 rename_tac THEN kont 447 end g 448 fun test_parses patseq = 449 case PQ seq.cases patseq of 450 NONE => raise ERR "No match" 451 | SOME (pat, rest) => do_one_pat pat handle HOL_ERR _ => test_parses rest 452in 453 test_parses pats 454end 455 456val Absyn = Parse.Absyn 457val term_grammar = Parse.term_grammar 458 459 460fun kMATCH_RENAME_TAC q k (g as (_, t)) = let 461 val ctxt = goal_ctxt g 462 fun mkA q = Absyn.TYPED(locn.Loc_None, Absyn q, Pretype.fromType bool) 463 val pat_parses = TermParse.prim_ctxt_termS mkA (term_grammar()) ctxt q 464in 465 wholeterm_rename_helper 466 {pats=pat_parses, ERR = ERR "MATCH_RENAME_TAC", kont = k, 467 fvs_set = HOLset.fromList Term.compare ctxt} 468 t 469end g 470 471fun MATCH_RENAME_TAC q = kMATCH_RENAME_TAC q ALL_TAC 472 473fun kMATCH_ASSUM_RENAME_TAC q k (g as (asl,t)) = let 474 val ctxt = free_varsl(t::asl) 475 val pats = TermParse.prim_ctxt_termS Absyn (term_grammar()) ctxt q 476in 477 FIRST_ASSUM (fn th => 478 wholeterm_rename_helper 479 {pats=pats, ERR = ERR "MATCH_ASSUM_RENAME_TAC", kont = k, 480 fvs_set = HOLset.fromList Term.compare ctxt} 481 (concl th)) 482end g 483 484fun MATCH_ASSUM_RENAME_TAC q = kMATCH_ASSUM_RENAME_TAC q ALL_TAC 485 486(* needs to be eta-expanded so that the possible HOL_ERRs are raised 487 when applied to a goal, not before, thereby letting FIRST_ASSUM catch 488 the exception *) 489fun subterm_helper make_tac k {ERR,pats,fvs_set} t g = let 490 fun test (pat, thetasz) (bvs, subt) = 491 case Lib.total (fn t => raw_match [] fvs_set pat t ([],[])) subt of 492 SOME ((theta0, _), (tytheta,_)) => 493 let 494 fun filt {residue, ...} = 495 List.all (fn bv => not (free_in bv residue)) bvs 496 val theta0 = 497 filter (fn s => isnt_uscore_var (#redex s) andalso filt s) 498 theta0 499 val theta = map (redex_map (inst tytheta)) theta0 500 in 501 if length theta <> thetasz then NONE 502 else Lib.total (make_tac theta THEN k) g 503 end 504 | NONE => NONE 505 fun find_pats patseq = 506 case PQ seq.cases patseq of 507 NONE => raise ERR "No matching sub-term found" 508 | SOME (patsz, rest) => 509 (case gen_find_term (test patsz) t of 510 SOME tacresult => tacresult 511 | NONE => find_pats rest) 512in 513 find_pats pats 514end 515 516fun prep_rename q nm (asl, t) = let 517 val ERR = ERR nm 518 val fvs = free_varsl (t::asl) 519 val pats = TermParse.prim_ctxt_termS Absyn (term_grammar()) fvs q 520 val fvs_set = HOLset.fromList Term.compare fvs 521 fun mapthis pat = let 522 val patfvs = free_vars pat 523 val pat_binds = 524 filter (fn v => not (op_mem aconv v fvs) andalso isnt_uscore_var v) 525 patfvs 526 in 527 (pat, length pat_binds) 528 end 529in 530 {ERR = ERR, pats = seq.map mapthis pats, fvs_set = fvs_set} 531end 532 533fun kMATCH_GOALSUB_RENAME_TAC q k (g as (asl, t)) = 534 subterm_helper make_rename_tac k 535 (prep_rename q "MATCH_GOALSUB_RENAME_TAC" g) t g 536 537fun MATCH_GOALSUB_RENAME_TAC q = kMATCH_GOALSUB_RENAME_TAC q ALL_TAC 538 539fun kMATCH_ASMSUB_RENAME_TAC q k (g as (asl, t)) = let 540 val args = prep_rename q "MATCH_ASMSUB_RENAME_TAC" g 541in 542 FIRST_ASSUM (subterm_helper make_rename_tac k args o concl) g 543end 544 545fun MATCH_GOALSUB_ABBREV_TAC q (g as (asl, t)) = 546 subterm_helper make_abbrev_tac ALL_TAC 547 (prep_rename q "MATCH_GOALSUB_ABBREV_TAC" g) t g 548 549fun MATCH_ASMSUB_ABBREV_TAC q (g as (asl, t)) = let 550 val args = prep_rename q "MATCH_ASMSUB_ABBREV_TAC" g 551in 552 FIRST_ASSUM (subterm_helper make_abbrev_tac ALL_TAC args o concl) g 553end 554 555fun MATCH_ASMSUB_RENAME_TAC q = kMATCH_ASMSUB_RENAME_TAC q ALL_TAC 556 557fun RENAME1_TAC q = 558 MATCH_RENAME_TAC q ORELSE MATCH_ASSUM_RENAME_TAC q ORELSE 559 MATCH_GOALSUB_RENAME_TAC q ORELSE MATCH_ASMSUB_RENAME_TAC q 560 561fun coreRENAME_TAC qs k = 562 let 563 fun kRENAME1 q k = 564 kMATCH_RENAME_TAC q k ORELSE kMATCH_ASSUM_RENAME_TAC q k ORELSE 565 kMATCH_GOALSUB_RENAME_TAC q k ORELSE kMATCH_ASMSUB_RENAME_TAC q k 566 fun recurse qs = 567 case qs of 568 [] => k 569 | q::rest => kRENAME1 q (recurse rest) 570 in 571 recurse qs 572 end 573 574fun flip_inst s = map (fn {redex,residue} => {redex=residue,residue=redex}) s 575 576fun gvarify (goal as (asl,w)) = 577 let 578 fun gentheta (v, acc) = {residue = v, redex = genvar (type_of v)} :: acc 579 in 580 HOLset.foldl gentheta [] (FVL (w::asl) empty_tmset) 581 end 582 583fun kRENAME_TAC qs k g = 584 let 585 val gsig = gvarify g 586 val gsig_inv = flip_inst gsig 587 in 588 make_rename_tac gsig THEN 589 coreRENAME_TAC qs (make_rename_tac gsig_inv THEN k) 590 end g 591 592fun RENAME_TAC qs = kRENAME_TAC qs ALL_TAC 593 594end (* Q *) 595