1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory FP_Eval 8imports 9 HOL.HOL 10 TermPatternAntiquote 11begin 12 13text \<open> 14 FP_Eval: efficient evaluator for functional programs. 15 16 The algorithm is similar to @{method simp}, but streamlined somewhat. 17 Poorly-scaling simplifier features are omitted, e.g.: 18 conditional rules, eta normalisation, rewriting under lambdas, etc. 19 20 See FP_Eval_Tests for examples and tests. Currently, only 21 ML conversions and tactics are provided. 22 23 Features: 24 \<bullet> Low overhead (usually lower than @{method simp}) 25 \<bullet> Applicative-order evaluation to WHNF (doesn't rewrite under lambdas) 26 \<bullet> Manual specification of rewrite rules, no global context 27 \<bullet> Cong rules supported for controlling evaluation (if, let, case, etc.) 28 \<bullet> Finer control than simp: explicit skeletons, debugging callbacks, 29 perf counters (see signature for FP_Eval.eval') 30 31 Major TODOs: 32 \<bullet> Preprocess rewrite rules for speed 33 \<bullet> Optimize eval_rec more 34 \<bullet> Support for simprocs (ideally with static checks) 35 \<bullet> Simple tactical and Isar method wrappers 36 \<bullet> Automatic ruleset builders 37 \<bullet> Static analysis for rules: 38 \<bullet> Confluence, termination 39 \<bullet> Completeness 40 \<bullet> Running time? 41 \<bullet> Dynamic analysis e.g. unused rules 42 43 Work in progress. 44\<close> 45 46locale FP_Eval begin 47lemma bool_prop_eq_True: 48 "Trueprop P \<equiv> (P \<equiv> True)" 49 by (simp add: atomize_eq) 50 51lemma bool_prop_eq_False: 52 "Trueprop (\<not>P) \<equiv> (P \<equiv> False)" 53 by (simp add: atomize_eq) 54end 55 56ML \<open> 57structure FP_Eval = struct 58 59(*** Utils ***) 60 61(* O(1) version of thm RS @{thm eq_reflection} *) 62fun then_eq_reflection thm = let 63 val (x, y) = Thm.dest_binop (Thm.dest_arg (Thm.cprop_of thm)); 64 val cT = Thm.ctyp_of_cterm x; 65 val rule = @{thm eq_reflection} |> Thm.instantiate' [SOME cT] [SOME x, SOME y]; 66 in Thm.implies_elim rule thm end; 67 68fun bool_conv_True thm = 69 Thm.instantiate ([], [((("P", 0), @{typ bool}), 70 Thm.dest_arg (Thm.cprop_of thm))]) 71 @{thm FP_Eval.bool_prop_eq_True} 72 |> (fn conv => Thm.equal_elim conv thm); 73 74fun bool_conv_False thm = 75 Thm.instantiate ([], [((("P", 0), @{typ bool}), 76 Thm.dest_arg (Thm.dest_arg (Thm.cprop_of thm)))]) 77 @{thm FP_Eval.bool_prop_eq_False} 78 |> (fn conv => Thm.equal_elim conv thm); 79 80(* Emulate simp's conversion of non-equational rules to "P \<equiv> True", etc. *) 81fun maybe_convert_eqn thm = 82 (* HACK: special case to transform @{thm refl} to "(HOL.eq ?t ?t) \<equiv> True", 83 as the default result of "?t \<equiv> ?t" isn't what we want *) 84 if Thm.eq_thm_prop (thm, @{thm refl}) then SOME (bool_conv_True thm) else 85 (case Thm.prop_of thm of 86 @{term_pat "Trueprop (_ = _)"} => 87 SOME (then_eq_reflection thm) 88 | @{term_pat "Trueprop (\<not> _)"} => 89 SOME (bool_conv_False thm) 90 | @{term_pat "_ \<equiv> _"} => SOME thm 91 | @{term_pat "Trueprop _"} => 92 SOME (bool_conv_True thm) 93 | _ => NONE); 94 95(* FIXME: turn into Config. 96 NB: low-level eval' ignores this global setting *) 97(* 0: none; 1: summary details; 2+: everything *) 98val trace = Unsynchronized.ref 0; 99 100 101(*** Data structures ***) 102 103(* TODOs: 104 - cond rules? 105 - simprocs? 106 - skeleton optimisation? 107*) 108type eqns_for_const = 109 int * (* arity of const (we require it to be equal in all rules) *) 110 (int list * thm) option * (* possible cong rule skeleton (list of which args to evaluate) *) 111 thm Net.net; (* eval equations *) 112(* NB: the cong thm is never actually used; it only tells 113 fp_eval how to perform the rewriting. *) 114 115(* Main fp_eval context *) 116type rules = eqns_for_const Symtab.table; 117 118(* For completeness, though make_rules is preferred *) 119val empty_rules : rules = Symtab.empty; 120 121 122(*** Data structure operations ***) 123 124(* Must be simple Pure.eq equations *) 125val net_from_eqns : thm list -> thm Net.net = fn eqns => 126 let fun lift_eqn eqn = (case Thm.prop_of eqn of 127 @{term_pat "_ \<equiv> _"} => eqn 128 | _ => raise THM ("net_from_eqns: not a simple equation", 0, [eqn])); 129 val eqns' = map lift_eqn eqns; 130 fun insert eqn = Net.insert_term (K false) (Thm.term_of (Thm.lhs_of eqn), eqn); 131 in fold_rev insert eqns' Net.empty end; 132 133(* Must be a simple Pure.eq equation, or convertible to one *) 134fun add_eqn raw_eqn : rules -> rules = 135 let val eqn = case maybe_convert_eqn raw_eqn of 136 NONE => raise THM ("add_eqn: can't use this as equation", 0, [raw_eqn]) 137 | SOME eqn => eqn; 138 val eqn_lhs = Thm.term_of (Thm.lhs_of eqn); 139 val (cname, args) = case strip_comb eqn_lhs of 140 (* This should be OK because Const names are qualified *) 141 (Const (cname, _), args) => (cname, args) 142 | (Free (cname, _), args) => (cname, args) 143 | _ => raise THM ("add_eqn: head of LHS is not a constant", 0, [eqn]); 144 val arity = length args; 145 val empty_entry = (cname, (arity, NONE, Net.empty)); 146 fun update_entry (arity', cong, net) = 147 if arity <> arity' 148 then raise THM ("add_eqn: arity mismatch for " ^ cname ^ 149 " (existing=" ^ string_of_int arity' ^ 150 ", new=" ^ string_of_int arity ^ ")", 0, [raw_eqn]) 151 else (arity, cong, Net.insert_term (K false) (eqn_lhs, eqn) net); 152 in Symtab.map_default empty_entry update_entry end 153 154(* Helper for add_cong. cong_thm must be a weak cong rule of the form 155 156 "\<lbrakk> ?x_i = ?y_i; 157 ?x_j = ?y_j \<rbrakk> \<Longrightarrow> 158 my_const ?x_1 ?x_2 ... ?x_i ... = my_const ?x_1 ... ?y_i ..." 159 160 Returns indices of ?x_i in the LHS of the conclusion. 161 *) 162fun process_cong cong_thm : string * int * int list = 163 let fun die msg terms = raise TERM ("add_cong: " ^ msg, terms @ [Thm.prop_of cong_thm]); 164 (* LHS vars in premises tell us which order to use for rewriting *) 165 fun dest_prem (Const (@{const_name Pure.eq}, _) $ Var (vl, _) $ Var (vr, _)) = (vl, vr) 166 | dest_prem (@{const Trueprop} $ 167 (Const (@{const_name HOL.eq}, _) $ Var (vl, _) $ Var (vr, _))) = (vl, vr) 168 | dest_prem t = die "premise not a simple equality" [t]; 169 val prem_pairs = Logic.strip_imp_prems (Thm.prop_of cong_thm) 170 |> map dest_prem; 171 (* check concl and get LHS argument list *) 172 val (concl_lhs, concl_rhs) = 173 case Logic.strip_imp_concl (Thm.prop_of cong_thm) of 174 @{term_pat "?lhs \<equiv> ?rhs"} => (lhs, rhs) 175 | @{term_pat "Trueprop (?lhs = ?rhs)"} => (lhs, rhs) 176 | concl => die "concl not a simple equality" [concl]; 177 val (cname, arg_pairs) = case apply2 strip_comb (concl_lhs, concl_rhs) of 178 ((head as Const (cname, _), args1), (head' as Const (cname', _), args2)) => 179 if cname <> cname' 180 then die "different consts" [head, head'] 181 else if length args1 <> length args2 182 then die "different arities" [concl_lhs, concl_rhs] 183 else if not (forall is_Var (args1 @ args2)) 184 then die "args not schematic vars" [concl_lhs, concl_rhs] 185 else (cname, map (apply2 (dest_Var #> fst)) (args1 ~~ args2)) 186 | _ => die "equation heads are not constants" [concl_lhs, concl_rhs]; 187 (* for each prem LHS, find its argument position in the concl *) 188 fun prem_index var = case find_index (fn v => v = var) (map fst arg_pairs) of 189 ~1 => die "var in prems but not conclusion" [Var (var, dummyT)] 190 | n => n; 191 val prem_indices = map prem_index (map fst prem_pairs); 192 (* ensure no duplicates, otherwise fp_eval would do multiple evaluations *) 193 val _ = case duplicates (op=) prem_indices of 194 [] => () 195 | (n::_) => die "var appears twice in prems" [Var (fst (nth prem_pairs n), dummyT)]; 196 (* TODO: we could do even more checking here, but most other errors would 197 cause fp_eval to fail-fast *) 198 val const_arity = length arg_pairs; 199 in (cname, const_arity, prem_indices) end; 200 201fun add_cong cong_thm : rules -> rules = 202 let val (cname, arity, cong_spec) = process_cong cong_thm; 203 val empty_entry = (cname, (arity, NONE, Net.empty)); 204 fun update_entry (arity', opt_cong, net) = 205 if arity <> arity' 206 then raise THM ("add_cong: arity mismatch for " ^ cname ^ 207 " (existing=" ^ string_of_int arity' ^ 208 ", new=" ^ string_of_int arity ^ ")", 0, [cong_thm]) 209 else case opt_cong of 210 NONE => (arity, SOME (cong_spec, cong_thm), net) 211 | SOME (cong_spec', cong_thm') => 212 if cong_spec = cong_spec' 213 then (warning ("add_cong: adding duplicate for " ^ cname); 214 (arity, opt_cong, net)) 215 else raise THM ("add_cong: different cong rule already exists for " ^ cname, 216 0, [cong_thm', cong_thm]); 217 in Symtab.map_default empty_entry update_entry end; 218 219(* Simple builder *) 220fun make_rules eqns congs = fold_rev add_eqn eqns (fold add_cong congs empty_rules); 221 222fun merge_rules (r1, r2) = 223 let fun merge_const cname (r as (arity, cong, net), r' as (arity', cong', net')) = 224 if pointer_eq (r, r') then r else 225 let val _ = if arity = arity' then () else 226 error ("merge_rules: different arity for " ^ cname ^ ": " ^ 227 string_of_int arity ^ ", " ^ string_of_int arity'); 228 val cong'' = case (cong, cong') of 229 (NONE, NONE) => NONE 230 | (SOME _, NONE) => cong 231 | (NONE, SOME _) => cong' 232 | (SOME (_, thm), SOME (_, thm')) => 233 if Thm.eq_thm_prop (thm, thm') then cong else 234 raise THM ("merge_rules: different cong rules for " ^ cname, 0, 235 [thm, thm']); 236 in (arity, cong'', Net.merge Thm.eq_thm_prop (net, net')) end; 237 in if pointer_eq (r1, r2) then r1 else 238 Symtab.join merge_const (r1, r2) 239 end; 240 241fun dest_rules rules = 242 let val const_rules = Symtab.dest rules |> map snd; 243 val eqnss = map (fn (_, _, net) => Net.content net) const_rules; 244 val congs = map_filter (fn (_, cong, _) => Option.map snd cong) const_rules; 245 in (List.concat eqnss, congs) end; 246 247 248(*** Evaluator ***) 249 250(* Skeleton terms track which subterms have already been fully 251 evaluated and can be skipped. This follows the same method as 252 Raw_Simplifier.bottomc. *) 253val skel0 = Bound 0; (* always descend and rewrite *) 254val skel_skip = Var (("", 0), dummyT); (* always skip *) 255 256(* Full interface *) 257fun eval' (ctxt: Proof.context) 258 (debug_trace: int -> (unit -> string) -> unit) (* debug callback: level, message *) 259 (breakpoint: cterm -> bool) (* if true, stop rewriting and return *) 260 (eval_under_var: bool) (* if true, expand partially applied funcs under Var skeletons *) 261 (rules: rules) 262 (ct0: cterm, ct0_skel: term) 263 (* eqn, final skeleton, perf counters *) 264 : (thm * term) * (string * int) list = let 265 (* Performance counters *) 266 val counter_eval_rec = Unsynchronized.ref 0; 267 val counter_try_rewr = Unsynchronized.ref 0; 268 val counter_rewrite1 = Unsynchronized.ref 0; 269 val counter_rewrites = Unsynchronized.ref 0; 270 val counter_rewr_skel = Unsynchronized.ref 0; 271 val counter_beta_redc = Unsynchronized.ref 0; 272 val counter_transitive = Unsynchronized.ref 0; 273 val counter_combination = Unsynchronized.ref 0; 274 val counter_dest_comb = Unsynchronized.ref 0; 275 val counter_congs = Unsynchronized.ref 0; 276 fun increment c = (c := !c + 1); 277 278 (* Debug output *) 279 val print_term = Syntax.string_of_term ctxt; 280 val print_cterm = print_term o Thm.term_of; 281 fun print_maybe_thm t = Option.getOpt (Option.map (print_term o Thm.prop_of) t, "<none>"); 282 283 (* Utils *) 284 fun my_transitive t1 t2 = 285 (increment counter_transitive; 286 Thm.transitive t1 t2); 287 fun my_combination t1 t2 = 288 (increment counter_combination; 289 Thm.combination t1 t2); 290 291 fun transitive1 NONE NONE = NONE 292 | transitive1 (t1 as SOME _) NONE = t1 293 | transitive1 NONE (t2 as SOME _) = t2 294 | transitive1 (SOME t1) (SOME t2) = SOME (my_transitive t1 t2); 295 296 fun maybe_rewr_result NONE ct = ct 297 | maybe_rewr_result (SOME rewr) _ = Thm.rhs_of rewr; 298 299 fun maybe_eqn (SOME eqn) _ = eqn 300 | maybe_eqn _ ct = Thm.reflexive ct; 301 302 fun combination1 _ NONE _ NONE = NONE 303 | combination1 cf cf_rewr cx cx_rewr = 304 SOME (my_combination (maybe_eqn cf_rewr cf) (maybe_eqn cx_rewr cx)); 305 306 (* strip_comb; invent skeleton to same depth if required *) 307 val strip_comb_skel = let 308 fun strip (f $ x, fK $ xK, ts) = strip (f, fK, (x, xK)::ts) 309 | strip (f $ x, skel as Var _, ts) = 310 (* if a sub-comb is normalized, expand it for matching purposes, 311 but don't expand children *) 312 if eval_under_var then strip (f, skel, (x, skel)::ts) 313 else (f $ x, skel, ts) 314 (* skeleton doesn't match; be conservative and expand all *) 315 | strip (f $ x, _, ts) = strip (f, skel0, (x, skel0)::ts) 316 | strip (f, fK, ts) = (f, fK, ts) (* finish *); 317 in fn (t, skel) => strip (t, skel, []) end; 318 319 (* strip_comb for cterms *) 320 val strip_ccomb : cterm -> int -> cterm * cterm list = let 321 fun strip ts t n = if n = 0 then (t, ts) else 322 case Thm.term_of t of 323 _ $ _ => let val (f, x) = Thm.dest_comb t; 324 (* yes, even dest_comb is nontrivial *) 325 val _ = increment counter_dest_comb; 326 in strip (x::ts) f (n-1) end 327 | _ => (t, ts); 328 in strip [] end; 329 330 (* find the first matching eqn and use it *) 331 fun rewrite1 _ [] = NONE 332 | rewrite1 ct (eqn::eqns) = let 333 val _ = increment counter_rewrite1; 334 in 335 SOME (Thm.instantiate (Thm.first_order_match (Thm.lhs_of eqn, ct)) eqn, eqn) 336 |> tap (fn _ => increment counter_rewrites) 337 handle Pattern.MATCH => rewrite1 ct eqns 338 end; 339 340 (* Apply rewrite step to skeleton. 341 FIXME: traverses whole RHS. If the RHS is large and the rest of the 342 evaluation ignores most of it, then this is wasted work. 343 Either preprocess eqn or somehow update skel lazily *) 344 fun rewrite_skel eqn skel = 345 let val _ = debug_trace 2 (fn () => "rewrite_skel: " ^ print_maybe_thm (SOME eqn) ^ " on " ^ print_term skel); 346 (* FIXME: may be wrong wrt. first_order_match--eta conversions? *) 347 fun match (Var (v, _)) t = Vartab.map_default (v, t) I 348 | match (pf $ px) (f $ x) = match pf f #> match px x 349 | match (pf $ px) (t as Var _) = match pf t #> match px t 350 | match (Abs (_, _, pt)) (Abs (_, _, t)) = match pt t 351 | match (Abs (_, _, pt)) (t as Var _) = match pt t 352 | match _ _ = I; 353 val inst = match (Thm.term_of (Thm.lhs_of eqn)) skel Vartab.empty; 354 fun subst (t as Var (v, _)) = Option.getOpt (Vartab.lookup inst v, t) 355 | subst t = t; 356 (* Consts in the RHS that don't appear in our rewrite rules, are also normalised *) 357 fun norm_consts (t as Var _) = t 358 | norm_consts (t as Bound _) = t 359 | norm_consts (Abs (v, T, t)) = Abs (v, T, norm_consts t) 360 | norm_consts (t as Const (cname, _)) = 361 if Symtab.defined rules cname then t else Var ((cname, 0), dummyT) 362 | norm_consts (t as Free (cname, _)) = 363 if Symtab.defined rules cname then t else Var ((cname, 0), dummyT) 364 | norm_consts (f $ x) = 365 let val f' = norm_consts f; 366 val x' = norm_consts x; 367 in case (f', x') of 368 (Var _, Var _) => f' 369 | _ => f' $ x' 370 end; 371 in map_aterms subst (Thm.term_of (Thm.rhs_of eqn)) 372 |> tap (fn t' => counter_rewr_skel := !counter_rewr_skel + size_of_term t') 373 |> norm_consts 374 |> tap (fn t' => debug_trace 2 (fn () => "rewrite_skel: ==> " ^ print_term t')) end; 375 376 fun apply_skel (f as Var _) (Var _) = f 377 | apply_skel (f as Abs _) x = betapply (f, x) 378 | apply_skel f x = f $ x; 379 380 (* Main structure. 381 We just rewrite all combinations inside-out, and ignore everything else. 382 Special cases: 383 - Combinations may have no arguments; this expands a single Const or Free. 384 - A combination may have more args than the arity of its head, e.g. 385 "If c t f x y z ...". In this case, we rewrite "If c t f" only, 386 then recurse on the new combination. 387 - If the head is a lambda abs, its arity is considered to be the number of 388 bound vars; they are evaluated first and then beta redc is performed. 389 *) 390 val reached_breakpoint = Unsynchronized.ref false; 391 fun eval_rec (ct, skel) = 392 ((if !reached_breakpoint then () else reached_breakpoint := breakpoint ct); 393 if !reached_breakpoint 394 then (debug_trace 1 (fn () => "eval_rec: triggered breakpoint on: " ^ print_cterm ct); 395 (NONE, skel)) 396 else 397 (increment counter_eval_rec; 398 debug_trace 2 (fn () => "eval_rec: " ^ print_cterm ct ^ " (skel: " ^ print_term skel ^ ")"); 399 case skel of 400 Var _ => (NONE, skel) 401 | Abs _ => (NONE, skel) 402 | _ => let 403 val (head, head_skel, args) = strip_comb_skel (Thm.term_of ct, skel); 404 val (chead, cargs) = strip_ccomb ct (length args); 405 (* rules for head, if any *) 406 val maybe_head_rules = 407 case head of 408 Const (cname, _) => Symtab.lookup rules cname 409 | Free (cname, _) => Symtab.lookup rules cname 410 | _ => NONE; 411 412 val beta_depth = let 413 fun f (Abs (_, _, t)) = 1 + f t 414 | f _ = 0; 415 in Int.min (length args, f head) end; 416 417 (* Emulating call by value. First, we find the equation arity of the head. 418 We evaluate a number of args up to the arity, except if the head has a 419 cong specification, we follow the cong spec. *) 420 val (eval_args, effective_arity) = 421 case maybe_head_rules of 422 SOME (arity, maybe_cong, _) => 423 if length args < arity 424 then (List.tabulate (length args, I), length args) 425 else (case maybe_cong of 426 NONE => (List.tabulate (arity, I), arity) 427 | SOME (indices, cong_thm) => 428 (increment counter_congs; 429 debug_trace 2 (fn () => "eval_rec: will use cong skeleton: " ^ print_maybe_thm (SOME cong_thm)); 430 (indices, arity))) 431 (* If head has no equations, just evaluate all arguments. *) 432 | NONE => let val d = if beta_depth = 0 then length args else beta_depth; 433 in (List.tabulate (d, I), d) end; 434 val skip_args = subtract op= eval_args (List.tabulate (length args, I)); 435 436 (* evaluate args *) 437 fun eval_arg i = (i, (nth cargs i, eval_rec (nth cargs i, snd (nth args i)))); 438 fun skip_arg i = (i, (nth cargs i, (NONE, snd (nth args i)))); 439 val arg_convs = map eval_arg eval_args @ map skip_arg skip_args 440 |> sort (int_ord o apply2 fst) |> map snd; 441 442 (* substitute results up to arity of head *) 443 (* TODO: avoid unnecessary cterm ops? *) 444 fun recombine beta_redc = 445 fold (fn (arg, (arg_conv, arg_skel)) => fn (f, (f_conv, f_skel)) => 446 let val comb_thm = combination1 f f_conv arg arg_conv; 447 val result = maybe_rewr_result comb_thm (Thm.apply f arg); 448 (* respect breakpoint, if set *) 449 in case (if not beta_redc orelse !reached_breakpoint then Bound 0 450 else Thm.term_of f) of 451 Abs _ => let 452 val _ = debug_trace 2 (fn () => 453 "eval_rec: beta redc: " ^ print_cterm result); 454 val _ = increment counter_beta_redc; 455 val beta_thm = Thm.beta_conversion false result; 456 (* f_skel must be Abs, for apply_skel to do what we want *) 457 val f_skel' = case f_skel of Abs _ => f_skel 458 | _ => Thm.term_of f; 459 in (Thm.rhs_of beta_thm, 460 (transitive1 comb_thm (SOME beta_thm), 461 apply_skel f_skel' arg_skel)) end 462 | _ => (result, (comb_thm, apply_skel f_skel arg_skel)) 463 end); 464 465 val (ct', (arg_conv, skel')) = 466 recombine true 467 (take effective_arity arg_convs) 468 (chead, (NONE, head_skel)); 469 470 (* Now rewrite the application of head to args *) 471 val _ = debug_trace 2 (fn () => "eval_rec: head is " ^ print_term head ^ 472 ", (effective) arity " ^ string_of_int effective_arity); 473 in case maybe_head_rules of (* TODO: refactor the following *) 474 NONE => 475 if beta_depth = 0 476 then let (* No equation and not Abs head, so mark as normalised. 477 We also know effective_arity = length args, so arg_convs 478 is complete *) 479 val _ = @{assert} (effective_arity = length args); 480 val skel'' = case head of Abs _ => skel' | _ => 481 fold (fn x => fn f => apply_skel f x) 482 (map (snd o snd) arg_convs) skel_skip; 483 in (arg_conv, skel'') end 484 else let (* Add remaining args and continue rewriting *) 485 val (ct'', (conv'', skel'')) = 486 recombine false 487 (drop effective_arity arg_convs) 488 (maybe_rewr_result arg_conv ct', (arg_conv, skel')); 489 val (final_conv, final_skel) = eval_rec (ct'', skel''); 490 in (transitive1 conv'' final_conv, final_skel) end 491 | SOME (arity, _, net) => 492 if effective_arity < arity then (arg_conv, skel') else 493 let val rewr_result = 494 if !reached_breakpoint then NONE else 495 (debug_trace 2 (fn () => "eval_rec: now rewrite head from: " ^ print_cterm ct'); 496 rewrite1 ct' (Net.match_term net (Thm.term_of ct'))); 497 in case rewr_result of 498 NONE => 499 (* No equations; add remaining args and mark head as normalised *) 500 let val (_, (conv'', _)) = 501 recombine false 502 (drop effective_arity arg_convs) 503 (ct', (arg_conv, skel')); 504 val skel'' = fold (fn x => fn f => apply_skel f x) 505 (map (snd o snd) arg_convs) skel_skip; 506 in (conv'', skel'') end 507 | SOME (conv, rule) => 508 let val _ = debug_trace 2 (fn () => "eval: " 509 ^ print_maybe_thm (SOME conv) ^ "\n using: " 510 ^ print_maybe_thm (SOME rule)); 511 val _ = increment counter_try_rewr; 512 val rhs_skel = rewrite_skel rule skel'; 513 val conv' = case arg_conv of NONE => conv 514 | SOME t => my_transitive t conv; 515 val _ = debug_trace 2 (fn () => 516 "eval_rec: after rewrite: " ^ print_maybe_thm (SOME conv')); 517 (* Add remaining args and continue rewriting *) 518 val (ct'', (conv'', skel'')) = 519 recombine false 520 (drop effective_arity arg_convs) 521 (Thm.rhs_of conv', (SOME conv', rhs_skel)); 522 val (final_conv, final_skel) = eval_rec (ct'', skel''); 523 in (transitive1 conv'' final_conv, final_skel) end 524 end 525 end 526 |> tap (fn (conv, skel) => debug_trace 2 (fn () => 527 "result: " ^ print_maybe_thm (SOME (maybe_eqn conv ct)) ^ "\n skel: " ^ print_term skel)) 528 )); 529 530 (* Final result *) 531 val (ct_rewr, final_skel) = eval_rec (ct0, ct0_skel); 532 val counters = [ 533 ("eval_rec", !counter_eval_rec), 534 ("try_rewr", !counter_try_rewr), 535 ("rewrite1", !counter_rewrite1), 536 ("rewrites", !counter_rewrites), 537 ("rewr_skel", !counter_rewr_skel), 538 ("beta_redc", !counter_beta_redc), 539 ("transitive", !counter_transitive), 540 ("combination", !counter_combination), 541 ("dest_comb", !counter_dest_comb), 542 ("congs", !counter_congs) 543 ]; 544 in ((maybe_eqn ct_rewr ct0, final_skel), counters) end; 545 546 547(* Simplified interface with common defaults *) 548fun eval (ctxt: Proof.context) 549 (rules: rules) 550 : (cterm * term) -> ((thm * term) * (string * int) list) = 551 let fun debug_trace level msg = if level <= !trace then tracing (msg ()) else (); 552 fun breakpoint _ = false; 553 val eval_under_var = false; 554 in eval' ctxt debug_trace breakpoint eval_under_var rules end; 555 556(* Even simpler interface; uses default skel *) 557fun eval_conv ctxt rules: conv = 558 rpair skel0 #> eval ctxt rules #> fst #> fst; 559 560(* FIXME: eval doesn't rewrite under binders, we should add some forall_conv here *) 561fun eval_tac ctxt rules n: tactic = 562 Conv.gconv_rule (eval_conv ctxt rules) n 563 #> Seq.succeed; 564 565end; 566\<close> 567 568text \<open>See FP_Eval_Tests for explanation\<close> 569lemma (in FP_Eval) let_weak_cong': 570 "a = b \<Longrightarrow> Let a t = Let b t" 571 by simp 572 573end