1signature LAZY_EVAL = sig 2 3datatype pat = AnyPat of indexname | ConsPat of (string * pat list) 4 5type constructor = string * int 6 7type equation = { 8 function : term, 9 thm : thm, 10 rhs : term, 11 pats : pat list 12 } 13 14type eval_ctxt' = { 15 equations : equation list, 16 constructors : constructor list, 17 pctxt : Proof.context, 18 facts : thm Net.net, 19 verbose : bool 20 } 21 22type eval_hook = eval_ctxt' -> term -> (term * conv) option 23 24type eval_ctxt = { 25 ctxt : eval_ctxt', 26 hooks : eval_hook list 27 } 28 29val is_constructor_name : constructor list -> string -> bool 30val constructor_arity : constructor list -> string -> int option 31 32val mk_eval_ctxt : Proof.context -> constructor list -> thm list -> eval_ctxt 33val add_facts : thm list -> eval_ctxt -> eval_ctxt 34val get_facts : eval_ctxt -> thm list 35val get_ctxt : eval_ctxt -> Proof.context 36val add_hook : eval_hook -> eval_ctxt -> eval_ctxt 37val get_verbose : eval_ctxt -> bool 38val set_verbose : bool -> eval_ctxt -> eval_ctxt 39val get_constructors : eval_ctxt -> constructor list 40val set_constructors : constructor list -> eval_ctxt -> eval_ctxt 41 42val whnf : eval_ctxt -> term -> term * conv 43val match : eval_ctxt -> pat -> term -> 44 (indexname * term) list option -> (indexname * term) list option * term * conv 45val match_all : eval_ctxt -> pat list -> term list -> 46 (indexname * term) list option -> (indexname * term) list option * term list * conv 47 48end 49 50structure Lazy_Eval : LAZY_EVAL = struct 51 52datatype pat = AnyPat of indexname | ConsPat of (string * pat list) 53 54type constructor = string * int 55 56type equation = { 57 function : term, 58 thm : thm, 59 rhs : term, 60 pats : pat list 61 } 62 63type eval_ctxt' = { 64 equations : equation list, 65 constructors : constructor list, 66 pctxt : Proof.context, 67 facts : thm Net.net, 68 verbose : bool 69 } 70 71type eval_hook = eval_ctxt' -> term -> (term * conv) option 72 73type eval_ctxt = { 74 ctxt : eval_ctxt', 75 hooks : eval_hook list 76 } 77 78fun add_hook h ({hooks, ctxt} : eval_ctxt) = 79 {hooks = h :: hooks, ctxt = ctxt} : eval_ctxt 80 81fun get_verbose {ctxt = {verbose, ...}, ...} = verbose 82 83fun set_verbose b ({ctxt = {equations, pctxt, facts, constructors, ...}, hooks} : eval_ctxt) = 84 {ctxt = {equations = equations, pctxt = pctxt, facts = facts, 85 constructors = constructors, verbose = b}, hooks = hooks} 86 87fun get_constructors ({ctxt = {constructors, ...}, ...} : eval_ctxt) = constructors 88 89fun set_constructors cs ({ctxt = {equations, pctxt, facts, verbose, ...}, hooks} : eval_ctxt) = 90 {ctxt = {equations = equations, pctxt = pctxt, facts = facts, 91 verbose = verbose, constructors = cs}, hooks = hooks} 92 93type constructor = string * int 94 95val is_constructor_name = member (op = o apsnd fst) 96 97val constructor_arity = AList.lookup op = 98 99fun stream_pat_of_term _ (Var v) = AnyPat (fst v) 100 | stream_pat_of_term constructors t = 101 case strip_comb t of 102 (Const (c, _), args) => 103 (case constructor_arity constructors c of 104 NONE => raise TERM ("Not a valid pattern.", [t]) 105 | SOME n => 106 if length args = n then 107 ConsPat (c, map (stream_pat_of_term constructors) args) 108 else 109 raise TERM ("Not a valid pattern.", [t])) 110 | _ => raise TERM ("Not a valid pattern.", [t]) 111 112fun analyze_eq constructors thm = 113 let 114 val ((f, pats), rhs) = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> 115 apfst (strip_comb #> apsnd (map (stream_pat_of_term constructors))) 116 handle TERM _ => raise THM ("Not a valid function equation.", 0, [thm]) 117 in 118 {function = f, thm = thm RS @{thm eq_reflection}, rhs = rhs, pats = pats} : equation 119 end 120 121fun mk_eval_ctxt ctxt (constructors : constructor list) thms : eval_ctxt = { 122 ctxt = { 123 equations = map (analyze_eq constructors) thms, 124 facts = Net.empty, 125 verbose = false, 126 pctxt = ctxt, 127 constructors = constructors 128 }, 129 hooks = [] 130 } 131 132fun add_facts facts' {ctxt = {equations, pctxt, facts, verbose, constructors}, hooks} = 133 let 134 val eq = op = o apply2 Thm.prop_of 135 val facts' = 136 fold (fn thm => fn net => Net.insert_term eq (Thm.prop_of thm, thm) net 137 handle Net.INSERT => net) facts' facts 138 in 139 {ctxt = {equations = equations, pctxt = pctxt, facts = facts', 140 verbose = verbose, constructors = constructors}, 141 hooks = hooks} 142 end 143 144val get_facts = Net.content o #facts o #ctxt 145 146val get_ctxt = (#pctxt o #ctxt : eval_ctxt -> Proof.context) 147 148fun find_eqs (eval_ctxt : eval_ctxt) f = 149 let 150 fun eq_const (Const (c, _)) (Const (c', _)) = c = c' 151 | eq_const _ _ = false 152 in 153 map_filter (fn eq => if eq_const f (#function eq) then SOME eq else NONE) 154 (#equations (#ctxt eval_ctxt)) 155 end 156 157datatype ('a, 'b) either = Inl of 'a | Inr of 'b 158 159fun whnf (ctxt : eval_ctxt) t = 160 case whnf_aux1 ctxt (Envir.beta_norm t) of 161 (t', conv) => 162 if t aconv t' then 163 (t', conv) 164 else 165 case whnf ctxt t' of 166 (t'', conv') => (t'', conv then_conv conv') 167 168and whnf_aux1 (ctxt as {hooks, ctxt = ctxt'}) t = 169 case get_first (fn h => h ctxt' t) hooks of 170 NONE => whnf_aux2 ctxt t 171 | SOME (t', conv) => case whnf ctxt t' of (t'', conv') => 172 (t'', conv then_conv conv') 173and whnf_aux2 ctxt t = 174 let 175 val (f, args) = strip_comb t 176 177 fun instantiate table (Var (x, _)) = the (AList.lookup op = table x) 178 | instantiate table (s $ t) = instantiate table s $ instantiate table t 179 | instantiate _ t = t 180 fun apply_eq {thm, rhs, pats, ...} conv args = 181 let 182 val (table, args', conv') = match_all ctxt pats args (SOME []) 183 in ( 184 case table of 185 SOME _ => ( 186 let 187 val thy = Proof_Context.theory_of (get_ctxt ctxt) 188 val t' = list_comb (f, args') 189 val lhs = Thm.term_of (Thm.lhs_of thm) 190 val env = Pattern.match thy (lhs, t') (Vartab.empty, Vartab.empty) 191 val rhs = Thm.term_of (Thm.rhs_of thm) 192 val rhs = Envir.subst_term env rhs |> Envir.beta_norm 193 in 194 Inr (rhs, conv then_conv conv' then_conv Conv.rewr_conv thm) 195 end 196 handle Pattern.MATCH => Inl (args', conv then_conv conv')) 197 | NONE => Inl (args', conv then_conv conv')) 198 end 199 200 fun apply_eqs [] args conv = (list_comb (f, args), conv) 201 | apply_eqs (eq :: ctxt) args conv = 202 (case apply_eq eq conv args of 203 Inr res => res 204 | Inl (args', conv) => apply_eqs ctxt args' conv) 205 206 in 207 case f of 208 Const (f', _) => 209 if is_constructor_name (get_constructors ctxt) f' then 210 (t, Conv.all_conv) 211 else 212 apply_eqs (find_eqs ctxt f) args Conv.all_conv 213 | _ => (t, Conv.all_conv) 214 end 215and match_all ctxt pats args table = 216 let 217 fun match_all' [] [] acc conv table = (table, rev acc, conv) 218 | match_all' (_ :: pats) (arg :: args) acc conv NONE = 219 match_all' pats args (arg :: acc) (Conv.fun_conv conv) NONE 220 | match_all' (pat :: pats) (arg :: args) acc conv (SOME table) = 221 let 222 val (table', arg', conv') = match ctxt pat arg (SOME table) 223 val conv = Conv.combination_conv conv conv' 224 val acc = arg' :: acc 225 in 226 match_all' pats args acc conv table' 227 end 228 | match_all' _ _ _ _ _ = raise Match 229 in 230 if length pats = length args then 231 match_all' pats args [] Conv.all_conv table 232 else 233 (NONE, args, Conv.all_conv) 234 end 235and match _ _ t NONE = (NONE, t, Conv.all_conv) 236 | match _ (AnyPat v) t (SOME table) = (SOME ((v, t) :: table), t, Conv.all_conv) 237 | match ctxt (ConsPat (c, pats)) t (SOME table) = 238 let 239 val (t', conv) = whnf ctxt t 240 val (f, args) = strip_comb t' 241 in 242 case f of 243 Const (c', _) => 244 if c = c' then 245 case match_all ctxt pats args (SOME table) of 246 (table, args', conv') => (table, list_comb (f, args'), conv then_conv conv') 247 else 248 (NONE, t', conv) 249 | _ => (NONE, t', conv) 250 end 251 252end