1structure lazyTools :> lazyTools = 2 3struct 4 5local 6 7 open Globals HolKernel Parse Splaymap PrimitiveBddRules DerivedBddRules 8 9 datatype lazy_thm = LazyThm of (term HOLset.set) * (term list) * (unit -> thm) | Thm of thm 10 11 val lthms = ref (Splaymap.mkDict (Term.compare) : (term,lazy_thm)Splaymap.dict) 12 val lzmode = ref true 13 val _ = register_btrace("HolCheckLZ",lzmode); 14 val dbglz = ref false 15 val _ = Feedback.register_btrace("HolCheckDBGLZ",dbglz) 16 17 fun SPECL tml th = rev_itlist Specialize tml th handle HOL_ERR _ => raise ERR"lzSPECL" "" 18 19 val dpfx = "lzt_" 20 21 val mp_thm = bossLib.DECIDE ``!x y. x ==> (x==>y=y)`` 22in 23 24(*FIXME: if tm has free type vars, they are also free in the tm in the hyp after ASSUME and this may stump the rewriter *) 25(* this is harder than it looks because we can't bind them like we do normal free_vars by doing a list_mk_forall *) 26(* and really it can't be fixed directly because type vars also cannot be instantiated in the concl if they are free in the hyp*) 27(* so how do we "fix" this? 28 ANS: it is possible to instantiate a tyvar in the hyp *and* the concl, so this is only a practical rather 29 than theoretical obstacle *) 30(*NOTE: lthm does not need assums (except the one from ASSUME of course). See tphols2005 submission for proof and explanation *) 31(* FIXME: however, add pointer_eq checks so that if I have A |- t and B|-t, then I store two jf's and fire the right one *) 32(*FIXME: should I be using Susp to handle closures? No need, since a given jf fires at most once, but it might be cleaner to do so*) 33fun mk_lthm ljf ejf = 34 let val _ = profTools.bgt "lt_ml"(*PRF*) 35 val res = if not (!lzmode) 36 then let val _ = profTools.bgt "lt_ml_eager"(*PRF*) 37 val eres = ejf() 38 val _ = profTools.ent "lt_ml_eager"(*PRF*) 39 in eres end 40 else let val _ = profTools.bgt "lt_ml_lazy"(*PRF*) 41 val (tm,jf) = ljf() 42 val _ = profTools.ent "lt_ml_lazy"(*PRF*) 43 val _ = profTools.bgt "lt_ml_admin"(*PRF*) 44 val fv = FVL [tm] empty_varset 45 val fvl = HOLset.listItems fv 46 val lt = boolSyntax.list_mk_forall (fvl,tm) 47 val _ = (lthms := Splaymap.insert(!lthms,lt,LazyThm(fv,fvl,jf))) 48 val res = (SPECL fvl (ASSUME lt)) 49 val _ = profTools.ent "lt_ml_admin"(*PRF*) 50 in res end 51 val _ = profTools.ent "lt_ml"(*PRF*) 52 in res end 53 54fun get_thm (LazyThm (fv,fvl,jf)) = 55 let val th'' = jf() 56 val _ = profTools.bgt "lt_gt_genl"(*PRF*) 57 (*val (asl,cn) = dest_thm th'' (* the commented code shows how inefficient GENL is *) 58 val _ = HOLset.isEmpty(HOLset.intersection(hyp_frees th'',fv)) 59 val th' = mk_thm(asl,boolSyntax.list_mk_forall (fvl,cn))*) 60 val th' = (GENL fvl (th'')) (* FIXME: this will fail if any fv is free in the hyp of th'' *) 61 val _ = profTools.ent "lt_gt_genl"(*PRF*) 62 val th = prove_lthm th' 63 val _ = profTools.bgt "lt_gt_sm"(*PRF*) 64 val _ = (lthms:=Splaymap.insert(!lthms,concl th',Thm th)) 65 val _ = profTools.ent "lt_gt_sm"(*PRF*) 66 in th end 67 | get_thm (Thm th) = th 68 69and prove_lthm lthm = 70 let val _ = dbgTools.DEN (dpfx^"_pl") (*DBG*) 71 val res = List.foldl (fn (ass,lth) => 72 let val _ = profTools.bgt "lt_pl_sm"(*PRF*) 73 val asslth = Splaymap.peek(!lthms,ass) 74 val _ = profTools.ent "lt_pl_sm"(*PRF*) 75 in if isSome asslth 76 then let val th = (get_thm (valOf asslth)) 77 val _ = profTools.bgt "lt_pl_mpd"(*PRF*) 78 val th' = MP (DISCH ass lth) th 79 val _ = profTools.ent "lt_pl_mpd"(*PRF*) 80 in th' end 81 else lth 82 end) lthm (hyp lthm) 83 (*FIXME: if failure is caused by justifiers of some assum failing, this does not tell us which justifier failed*) 84 handle ex => (print "\n>>>lazyTools.prove_lthm failure\n"; print_thm lthm; failwith ("\n<<<lazyTools.prove_lthm failure\n")) 85 val _ = dbgTools.DEX (dpfx^"_pl") (*DBG*) 86 in res end 87 88(*term_bdd analog for prove_lthm*) 89fun prove_ltb ltb = 90 let val _ = dbgTools.DEN (dpfx^"_pt") (*DBG*) 91 val res = List.foldl (fn (ass,ltb) => 92 let val _ = profTools.bgt "lt_pt_sm"(*PRF*) 93 val asslth = Splaymap.peek(!lthms,ass) 94 val _ = profTools.ent "lt_pt_sm"(*PRF*) 95 in if isSome asslth 96 then let val th = (get_thm (valOf asslth)) 97 val _ = profTools.bgt "lt_pt_mpd"(*PRF*) 98 val tb = BddEqMp (MP (Drule.ISPECL [concl th,getTerm ltb] mp_thm) th) 99 (BddDisch (BddExtendVarmap (getVarmap ltb) (thmToTermBdd th)) ltb) 100 val _ = profTools.ent "lt_pt_mpd"(*PRF*) 101 in tb end 102 else ltb 103 end) ltb (HOLset.listItems (getAssums ltb)) 104 handle ex => (print "\n>>>lazyTools.prove_ltb failure\n"; print_term (getTerm ltb); 105 failwith ("\n<<<lazyTools.prove_ltb failure\n")) 106 val _ = dbgTools.DEX (dpfx^"_pt") (*DBG*) 107 in res end 108 109(* quick check that lazification works *) 110fun testlz s (jf:unit->Thm.thm) lt = 111 if (!dbglz) 112 then let val th = prove_lthm lt (* just calling jf may fail if jf uses tactics and lt has lazy lemmas *) 113 handle ex => (dbgTools.CBTH (s^"_lz") lt;dbgTools.DTH (s^"_lz") lt; 114 failwith("dbgTools.testlz failure 1:"^s)) 115 in if (Term.compare(concl th,concl lt)=EQUAL) 116 then () 117 else (dbgTools.CBTH s th; dbgTools.CBTH (s^"_lz") lt;dbgTools.DTH s th;dbgTools.DTH (s^"_lz") lt; 118 failwith ("dbgTools.testlz failure 2:"^s)) end 119 else () 120 121end 122end 123