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