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 mem 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 SPEC_THEN q ttac thm (g as (asl,w)) = let 90 val (Bvar,_) = dest_forall (concl thm) 91in 92 QTY_TAC (type_of Bvar) (fn t => ttac (Thm.SPEC t thm)) q g 93end 94 95fun SPECL_THEN ql = 96 case ql of 97 [] => ALL_THEN 98 | q::qs => SPEC_THEN q THEN_TCL SPECL_THEN qs 99 100fun ISPEC_THEN q ttac thm g = Q_TAC (fn t => ttac (Drule.ISPEC t thm)) q g 101 102fun goal_ctxt (asl,w) = free_varsl (w::asl) 103 104fun seq_mmap mf list = 105 case list of 106 [] => seq.result [] 107 | x::xs => seq.bind (mf x) 108 (fn x' => 109 seq.bind (seq_mmap mf xs) 110 (fn xs' => seq.result (x'::xs'))) 111 112fun ISPECL_THEN ql ttac thm g = 113 let 114 open Parse TermParse 115 val ctxt = goal_ctxt g 116 fun tf q = prim_ctxt_termS Absyn (term_grammar()) ctxt q 117 val tl_s = seq_mmap tf ql 118 in 119 case seq.cases tl_s of 120 NONE => raise ERR "ISPECL_THEN" "No parse for quotation list" 121 | SOME _ => 122 let 123 fun f tl = SOME (ttac (Drule.ISPECL tl thm) g) 124 handle HOL_ERR _ => NONE 125 in 126 case seq.cases (seq.mapPartial f tl_s) of 127 NONE => raise ERR "ISPECL_THEN" "No parse leads to success" 128 | SOME (res, _) => res 129 end 130 end 131 132fun SPEC_TAC (q1,q2) (g as (asl,w)) = let 133 val ctxt = free_varsl (w::asl) 134 val T1 = Parse.parse_in_context ctxt q1 135 val T2 = ptm_with_ctxtty' ctxt (type_of T1) q2 136in 137 Tactic.SPEC_TAC(T1, T2) g 138end; 139 140(* Generalizes first free variable with given name to itself. *) 141 142fun ID_SPEC_TAC q (g as (asl,w)) = 143 let val ctxt = free_varsl (w::asl) 144 val tm = Parse.parse_in_context ctxt q 145 in 146 Tactic.SPEC_TAC (tm, tm) g 147 end 148 149fun EXISTS(q1,q2) thm = 150 let val tm1 = btm q1 151 val exvartype = type_of (fst (dest_exists tm1)) 152 handle HOL_ERR _ => raise ERR "EXISTS" "first quotation not an exists" 153 val tm2 = ptm_with_ty q2 exvartype 154 in 155 Thm.EXISTS (tm1,tm2) thm 156 end; 157 158fun EXISTS_TAC q (g as (asl, w)) = 159 let 160 val exvartype = type_of (fst (dest_exists w)) 161 handle HOL_ERR _ => raise ERR "EXISTS_TAC" "goal not an exists" 162 in 163 QTY_TAC exvartype (fn t => Tactic.EXISTS_TAC t) q g 164 end 165 166fun LIST_EXISTS_TAC qL = EVERY (map EXISTS_TAC qL) 167 168fun REFINE_EXISTS_TAC q (asl, w) = let 169 val (qvar, body) = dest_exists w 170 val ctxt = free_varsl (w::asl) 171 val t = ptm_with_ctxtty' ctxt (type_of qvar) q 172 val qvars = set_diff (free_vars t) ctxt 173 val newgoal = subst [qvar |-> t] body 174 fun chl [] ttac = ttac 175 | chl (h::t) ttac = X_CHOOSE_THEN h (chl t ttac) 176in 177 SUBGOAL_THEN 178 (list_mk_exists(rev qvars, newgoal)) 179 (chl (rev qvars) (fn th => Tactic.EXISTS_TAC t THEN ACCEPT_TAC th)) 180 (asl, w) 181end 182 183fun X_CHOOSE_THEN q ttac thm (g as (asl,w)) = 184 let val ty = type_of (fst (dest_exists (concl thm))) 185 handle HOL_ERR _ => 186 raise ERR "X_CHOOSE_THEN" "provided thm not an exists" 187 in 188 QTY_TAC ty (fn t => Thm_cont.X_CHOOSE_THEN t ttac thm) q g 189 end 190 191val X_CHOOSE_TAC = C X_CHOOSE_THEN Tactic.ASSUME_TAC; 192 193fun DISCH q th = 194 let val (asl,c) = dest_thm th 195 val V = free_varsl (c::asl) 196 val tm = ptm_with_ctxtty V Type.bool q 197 in Thm.DISCH tm th 198 end; 199 200fun PAT_UNDISCH_TAC q (g as (asl,w)) = 201let val ctxt = free_varsl (w::asl) 202 val pat = ptm_with_ctxtty' ctxt Type.bool q 203 val asm = 204 first (can (ho_match_term [] Term.empty_tmset pat)) asl 205in Tactic.UNDISCH_TAC asm g 206end; 207 208fun PAT_ASSUM q ttac = 209 Q_TAC0 {traces = [("notify type variable guesses", 0)]} (SOME bool) 210 (fn t => Tactical.PAT_ASSUM t ttac) 211 q 212fun PAT_X_ASSUM q ttac = 213 Q_TAC0 {traces = [("notify type variable guesses", 0)]} (SOME bool) 214 (fn t => Tactical.PAT_X_ASSUM t ttac) 215 q 216 217fun SUBGOAL_THEN q ttac = 218 QTY_TAC Type.bool (fn t => Tactical.SUBGOAL_THEN t ttac) q 219 220val UNDISCH_TAC = QTY_TAC Type.bool Tactic.UNDISCH_TAC 221 222fun UNDISCH_THEN q ttac = 223 QTY_TAC Type.bool (fn t => Tactic.UNDISCH_TAC t THEN DISCH_THEN ttac) q 224 225fun hdtm_assum q ttac = Q_TAC (C Tactical.hdtm_assum ttac) q 226fun hdtm_x_assum q ttac = Q_TAC (C Tactical.hdtm_x_assum ttac) q 227 228val ASSUME = ASSUME o btm 229 230fun X_GEN_TAC q (g as (asl, w)) = 231 let 232 val ty = type_of (fst(dest_forall w)) 233 in 234 QTY_TAC ty Tactic.X_GEN_TAC q g 235 end 236 237fun X_FUN_EQ_CONV q tm = 238 let val ctxt = free_vars tm 239 val ty = #1 (dom_rng (type_of (lhs tm))) 240 in 241 Conv.X_FUN_EQ_CONV (ptm_with_ctxtty' ctxt ty q) tm 242 end 243 244fun skolem_ty tm = 245 let val (V,tm') = strip_forall tm 246 in if V<>[] 247 then list_mk_fun (map type_of V, type_of(fst(dest_exists tm'))) 248 else raise ERR"XSKOLEM_CONV" "no universal prefix" 249 end; 250 251fun X_SKOLEM_CONV q tm = 252 let val ctxt = free_vars tm 253 val ty = skolem_ty tm 254 in 255 Conv.X_SKOLEM_CONV (ptm_with_ctxtty ctxt ty q) tm 256 end 257 258fun AP_TERM q th = 259 let val ctxt = free_vars(concl th) 260 val tm = contextTerm ctxt q 261 val (ty,_) = dom_rng (type_of tm) 262 val (lhs,rhs) = dest_eq(concl th) 263 val theta = match_type ty (type_of lhs) 264 in 265 Thm.AP_TERM (Term.inst theta tm) th 266 end; 267 268fun AP_THM th q = 269 let val (lhs,rhs) = dest_eq(concl th) 270 val ty = fst (dom_rng (type_of lhs)) 271 val ctxt = free_vars (concl th) 272 in 273 Thm.AP_THM th (ptm_with_ctxtty ctxt ty q) 274 end; 275 276val ASM_CASES_TAC = QTY_TAC bool Tactic.ASM_CASES_TAC 277 278fun AC_CONV p = Conv.AC_CONV p o ptm; 279 280(* Could be smarter *) 281 282fun INST subst th = let 283 val ctxt = thm_frees th 284in 285 Thm.INST (mk_term_rsubst ctxt subst) th 286end 287val INST_TYPE = Thm.INST_TYPE o mk_type_rsubst; 288 289 290(*---------------------------------------------------------------------------*) 291(* Abbreviation tactics *) 292(*---------------------------------------------------------------------------*) 293 294fun ABBREV_TAC q (gl as (asl,w)) = 295 let val ctxt = free_varsl(w::asl) 296 val eq = Parse.parse_in_context ctxt q 297 in 298 markerLib.ABBREV_TAC eq 299 end gl; 300 301fun PAT_ABBREV_TAC q (gl as (asl,w)) = 302 let val fv_set = FVL (w::asl) empty_tmset 303 val ctxt = HOLset.listItems fv_set 304 val eq = Parse.parse_in_context ctxt q 305 in 306 markerLib.PAT_ABBREV_TAC fv_set eq 307 end gl; 308 309fun MATCH_ABBREV_TAC q (gl as (asl,w)) = 310 let val fv_set = FVL (w::asl) empty_tmset 311 val ctxt = HOLset.listItems fv_set 312 val pattern = ptm_with_ctxtty' ctxt bool q 313 in 314 markerLib.MATCH_ABBREV_TAC fv_set pattern 315 end gl; 316 317fun HO_MATCH_ABBREV_TAC q (gl as (asl,w)) = 318 let val fv_set = FVL (w::asl) empty_tmset 319 val ctxt = HOLset.listItems fv_set 320 val pattern = ptm_with_ctxtty' ctxt bool q 321in 322 markerLib.HO_MATCH_ABBREV_TAC fv_set pattern 323end gl; 324 325fun UNABBREV_TAC q (gl as (asl,w)) = 326 let val v = Parse.parse_in_context (free_varsl (w::asl)) q 327 in 328 markerLib.UNABBREV_TAC (fst(dest_var v)) 329 end gl; 330 331fun RM_ABBREV_TAC q (gl as (asl,w)) = 332 let val v = Parse.parse_in_context (free_varsl (w::asl)) q 333 in 334 markerLib.RM_ABBREV_TAC (fst(dest_var v)) 335 end gl; 336 337fun MATCH_ASSUM_ABBREV_TAC q (gl as (asl,w)) = 338 let val fv_set = FVL (w::asl) empty_tmset 339 val ctxt = HOLset.listItems fv_set 340 val pattern = ptm_with_ctxtty' ctxt bool q 341 in 342 markerLib.MATCH_ASSUM_ABBREV_TAC fv_set pattern 343 end gl; 344 345fun make_abbrev_tac s = 346 MAP_EVERY markerLib.ABB' (markerLib.safe_inst_sort s) 347 348(*---------------------------------------------------------------------------*) 349(* Renaming tactics *) 350(*---------------------------------------------------------------------------*) 351 352fun make_rename_tac s = 353 MAP_EVERY 354 (fn {redex=l,residue=r} => 355 CHOOSE_THEN SUBST_ALL_TAC 356 (Thm.EXISTS(mk_exists(l, mk_eq(r, l)), r) (Thm.REFL r))) 357 (Listsort.sort markerLib.safe_inst_cmp s) 358 359fun isnt_uscore_var v = let 360 val (s, _) = dest_var v 361in 362 size s <> 0 andalso String.sub(s, 0) <> #"_" 363end 364val strip_uscore_bindings = filter (fn {redex,residue} => isnt_uscore_var redex) 365fun redex_map f {redex,residue} = {redex = f redex, residue = residue} 366 367fun PQ (* parser quiet *) f = 368 f |> trace ("notify type variable guesses", 0) 369 |> trace ("show_typecheck_errors", 0) 370 371(* needs to be eta-expanded so that the possible HOL_ERRs are raised 372 when applied to a goal, not before, thereby letting FIRST_ASSUM catch 373 the exception *) 374fun wholeterm_rename_helper {pats,fvs_set,ERR,kont} tm g = let 375 fun do_one_pat pat = 376 let 377 val ((tmtheta0, _), (tytheta, _)) = 378 raw_match [] fvs_set pat tm ([],[]) 379 handle HOL_ERR _ => raise ERR "No match" 380 val rename_tac = 381 tmtheta0 |> strip_uscore_bindings |> map (redex_map (inst tytheta)) 382 |> make_rename_tac 383 in 384 rename_tac THEN kont 385 end g 386 fun test_parses patseq = 387 case PQ seq.cases patseq of 388 NONE => raise ERR "No match" 389 | SOME (pat, rest) => do_one_pat pat handle HOL_ERR _ => test_parses rest 390in 391 test_parses pats 392end 393 394val Absyn = Parse.Absyn 395val term_grammar = Parse.term_grammar 396 397 398fun kMATCH_RENAME_TAC q k (g as (_, t)) = let 399 val ctxt = goal_ctxt g 400 fun mkA q = Absyn.TYPED(locn.Loc_None, Absyn q, Pretype.fromType bool) 401 val pat_parses = TermParse.prim_ctxt_termS mkA (term_grammar()) ctxt q 402in 403 wholeterm_rename_helper 404 {pats=pat_parses, ERR = ERR "MATCH_RENAME_TAC", kont = k, 405 fvs_set = HOLset.fromList Term.compare ctxt} 406 t 407end g 408 409fun MATCH_RENAME_TAC q = kMATCH_RENAME_TAC q ALL_TAC 410 411fun kMATCH_ASSUM_RENAME_TAC q k (g as (asl,t)) = let 412 val ctxt = free_varsl(t::asl) 413 val pats = TermParse.prim_ctxt_termS Absyn (term_grammar()) ctxt q 414in 415 FIRST_ASSUM (fn th => 416 wholeterm_rename_helper 417 {pats=pats, ERR = ERR "MATCH_ASSUM_RENAME_TAC", kont = k, 418 fvs_set = HOLset.fromList Term.compare ctxt} 419 (concl th)) 420end g 421 422fun MATCH_ASSUM_RENAME_TAC q = kMATCH_ASSUM_RENAME_TAC q ALL_TAC 423 424(* needs to be eta-expanded so that the possible HOL_ERRs are raised 425 when applied to a goal, not before, thereby letting FIRST_ASSUM catch 426 the exception *) 427fun subterm_helper make_tac k {ERR,pats,fvs_set} t g = let 428 fun test (pat, thetasz) (bvs, subt) = 429 case Lib.total (fn t => raw_match [] fvs_set pat t ([],[])) subt of 430 SOME ((theta0, _), (tytheta,_)) => 431 let 432 fun filt {residue, ...} = 433 List.all (fn bv => not (free_in bv residue)) bvs 434 val theta0 = 435 filter (fn s => isnt_uscore_var (#redex s) andalso filt s) 436 theta0 437 val theta = map (redex_map (inst tytheta)) theta0 438 in 439 if length theta <> thetasz then NONE 440 else Lib.total (make_tac theta THEN k) g 441 end 442 | NONE => NONE 443 fun find_pats patseq = 444 case PQ seq.cases patseq of 445 NONE => raise ERR "No matching sub-term found" 446 | SOME (patsz, rest) => 447 (case gen_find_term (test patsz) t of 448 SOME tacresult => tacresult 449 | NONE => find_pats rest) 450in 451 find_pats pats 452end 453 454fun prep_rename q nm (asl, t) = let 455 val ERR = ERR nm 456 val fvs = free_varsl (t::asl) 457 val pats = TermParse.prim_ctxt_termS Absyn (term_grammar()) fvs q 458 val fvs_set = HOLset.fromList Term.compare fvs 459 fun mapthis pat = let 460 val patfvs = free_vars pat 461 val pat_binds = 462 filter (fn v => not (mem v fvs) andalso isnt_uscore_var v) patfvs 463 in 464 (pat, length pat_binds) 465 end 466in 467 {ERR = ERR, pats = seq.map mapthis pats, fvs_set = fvs_set} 468end 469 470fun kMATCH_GOALSUB_RENAME_TAC q k (g as (asl, t)) = 471 subterm_helper make_rename_tac k 472 (prep_rename q "MATCH_GOALSUB_RENAME_TAC" g) t g 473 474fun MATCH_GOALSUB_RENAME_TAC q = kMATCH_GOALSUB_RENAME_TAC q ALL_TAC 475 476fun kMATCH_ASMSUB_RENAME_TAC q k (g as (asl, t)) = let 477 val args = prep_rename q "MATCH_ASMSUB_RENAME_TAC" g 478in 479 FIRST_ASSUM (subterm_helper make_rename_tac k args o concl) g 480end 481 482fun MATCH_GOALSUB_ABBREV_TAC q (g as (asl, t)) = 483 subterm_helper make_abbrev_tac ALL_TAC 484 (prep_rename q "MATCH_GOALSUB_ABBREV_TAC" g) t g 485 486fun MATCH_ASMSUB_ABBREV_TAC q (g as (asl, t)) = let 487 val args = prep_rename q "MATCH_ASMSUB_ABBREV_TAC" g 488in 489 FIRST_ASSUM (subterm_helper make_abbrev_tac ALL_TAC args o concl) g 490end 491 492fun MATCH_ASMSUB_RENAME_TAC q = kMATCH_ASMSUB_RENAME_TAC q ALL_TAC 493 494fun RENAME1_TAC q = 495 MATCH_RENAME_TAC q ORELSE MATCH_ASSUM_RENAME_TAC q ORELSE 496 MATCH_GOALSUB_RENAME_TAC q ORELSE MATCH_ASMSUB_RENAME_TAC q 497 498fun coreRENAME_TAC qs k = 499 let 500 fun kRENAME1 q k = 501 kMATCH_RENAME_TAC q k ORELSE kMATCH_ASSUM_RENAME_TAC q k ORELSE 502 kMATCH_GOALSUB_RENAME_TAC q k ORELSE kMATCH_ASMSUB_RENAME_TAC q k 503 fun recurse qs = 504 case qs of 505 [] => k 506 | q::rest => kRENAME1 q (recurse rest) 507 in 508 recurse qs 509 end 510 511fun flip_inst s = map (fn {redex,residue} => {redex=residue,residue=redex}) s 512 513fun gvarify (goal as (asl,w)) = 514 let 515 fun gentheta (v, acc) = {residue = v, redex = genvar (type_of v)} :: acc 516 in 517 HOLset.foldl gentheta [] (FVL (w::asl) empty_tmset) 518 end 519 520fun kRENAME_TAC qs k g = 521 let 522 val gsig = gvarify g 523 val gsig_inv = flip_inst gsig 524 in 525 make_rename_tac gsig THEN 526 coreRENAME_TAC qs (make_rename_tac gsig_inv THEN k) 527 end g 528 529fun RENAME_TAC qs = kRENAME_TAC qs ALL_TAC 530 531end (* Q *) 532