# HG changeset patch # User haftmann # Date 1285076766 -7200 # Node ID 7af0441a3a477c9abf7e21e0612ac4ec760d3385 # Parent 6dc866b9c548b7230316c6309ea2b73123a81ff3 no_frees_* is subsumed by new framework mechanisms in Code_Preproc diff -r 6dc866b9c548 -r 7af0441a3a47 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Tue Sep 21 15:46:06 2010 +0200 +++ b/src/Tools/Code/code_simp.ML Tue Sep 21 15:46:06 2010 +0200 @@ -6,7 +6,6 @@ signature CODE_SIMP = sig - val no_frees_conv: conv -> conv val map_ss: (simpset -> simpset) -> theory -> theory val dynamic_eval_conv: conv val dynamic_eval_tac: theory -> int -> tactic @@ -19,22 +18,6 @@ structure Code_Simp : CODE_SIMP = struct -(* avoid free variables during conversion *) - -fun no_frees_conv conv ct = - let - val frees = Thm.add_cterm_frees ct []; - fun apply_beta free thm = Thm.combination thm (Thm.reflexive free) - |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false))) - |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false)); - in - ct - |> fold_rev Thm.cabs frees - |> conv - |> fold apply_beta frees - end; - - (* dedicated simpset *) structure Simpset = Theory_Data @@ -68,8 +51,8 @@ (* evaluation with dynamic code context *) -val dynamic_eval_conv = Conv.tap_thy (fn thy => no_frees_conv (Code_Thingol.dynamic_eval_conv thy - (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program))); +val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy + (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)); fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE; @@ -83,9 +66,9 @@ (* evaluation with static code context *) -fun static_eval_conv thy some_ss consts = no_frees_conv - (Code_Thingol.static_eval_conv_simple thy consts - (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program)); +fun static_eval_conv thy some_ss consts = + Code_Thingol.static_eval_conv_simple thy consts + (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program); fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts) THEN' conclude_tac thy some_ss; diff -r 6dc866b9c548 -r 7af0441a3a47 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Sep 21 15:46:06 2010 +0200 +++ b/src/Tools/nbe.ML Tue Sep 21 15:46:06 2010 +0200 @@ -589,28 +589,18 @@ fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct = raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct); -fun no_frees_rew rew t = - let - val frees = map Free (Term.add_frees t []); - in - t - |> fold_rev lambda frees - |> rew - |> curry (Term.betapplys o swap) frees - end; - -val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Simp.no_frees_conv - (lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy - (K (fn program => oracle thy program (compile false thy program)))))); +val dynamic_eval_conv = Conv.tap_thy (fn thy => + lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy + (K (fn program => oracle thy program (compile false thy program))))); fun dynamic_eval_value thy = lift_triv_classes_rew thy - (no_frees_rew (Code_Thingol.dynamic_eval_value thy I - (K (fn program => eval_term thy program (compile false thy program))))); + (Code_Thingol.dynamic_eval_value thy I + (K (fn program => eval_term thy program (compile false thy program)))); -fun static_eval_conv thy consts = Code_Simp.no_frees_conv - (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts +fun static_eval_conv thy consts = + lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts (K (fn program => let val nbe_program = compile true thy program - in fn thy => oracle thy program nbe_program end)))); + in fn thy => oracle thy program nbe_program end))); (** setup **)