# HG changeset patch # User haftmann # Date 1400164711 -7200 # Node ID 62da80041afdaccde3b4ac972e95db8422c44eb5 # Parent f64730f667b96c78e3475a66d3ec0dcd3f9f8e73 syntactic means to prevent accidental mixup of static and dynamic context diff -r f64730f667b9 -r 62da80041afd src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Thu May 15 16:38:31 2014 +0200 +++ b/src/HOL/Tools/code_evaluation.ML Thu May 15 16:38:31 2014 +0200 @@ -9,11 +9,15 @@ val dynamic_value: Proof.context -> term -> term option val dynamic_value_strict: Proof.context -> term -> term val dynamic_value_exn: Proof.context -> term -> term Exn.result - val static_value: Proof.context -> string list -> typ list -> Proof.context -> term -> term option - val static_value_strict: Proof.context -> string list -> typ list -> Proof.context -> term -> term - val static_value_exn: Proof.context -> string list -> typ list -> Proof.context -> term -> term Exn.result + val static_value: { ctxt: Proof.context, consts: string list, Ts: typ list } + -> Proof.context -> term -> term option + val static_value_strict: { ctxt: Proof.context, consts: string list, Ts: typ list } + -> Proof.context -> term -> term + val static_value_exn: { ctxt: Proof.context, consts: string list, Ts: typ list } + -> Proof.context -> term -> term Exn.result val dynamic_conv: Proof.context -> conv - val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv + val static_conv: { ctxt: Proof.context, consts: string list, Ts: typ list } + -> Proof.context -> conv val put_term: (unit -> term) -> Proof.context -> Proof.context val tracing: string -> 'a -> 'a end; @@ -160,8 +164,7 @@ | NONE => NONE) | subst_termify t = subst_termify_app (strip_comb t) -fun check_termify ctxt ts = - the_default ts (map_default subst_termify ts); +fun check_termify _ ts = the_default ts (map_default subst_termify ts); val _ = Context.>> (Syntax_Phases.term_check 0 "termify" check_termify); @@ -188,10 +191,11 @@ val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict; val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn; -fun gen_static_value static_value ctxt consts Ts = +fun gen_static_value static_value { ctxt, consts, Ts } = let - val static_value' = static_value cookie ctxt NONE I - (union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts) + val static_value' = static_value cookie + { ctxt = ctxt, target = NONE, lift_postproc = I, consts = + union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts } in fn ctxt' => fn t => static_value' ctxt' (mk_term_of t) end; val static_value = gen_static_value Code_Runtime.static_value; @@ -214,13 +218,13 @@ fun dynamic_conv ctxt = certify_eval ctxt dynamic_value Code_Runtime.dynamic_holds_conv; -fun static_conv ctxt consts Ts = +fun static_conv { ctxt, consts, Ts } = let val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} :: map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt) (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*) - val value = static_value ctxt consts Ts; - val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts); + val value = static_value { ctxt = ctxt, consts = consts, Ts = Ts }; + val holds = Code_Runtime.static_holds_conv { ctxt = ctxt, consts = union (op =) eqs consts }; in fn ctxt' => certify_eval ctxt' value holds end; diff -r f64730f667b9 -r 62da80041afd src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Thu May 15 16:38:31 2014 +0200 +++ b/src/Tools/Code/code_preproc.ML Thu May 15 16:38:31 2014 +0200 @@ -26,11 +26,11 @@ -> (code_algebra -> code_graph -> term -> conv) -> conv val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'b) -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'b - val static_conv: Proof.context -> string list - -> (code_algebra -> code_graph -> Proof.context -> term -> conv) + val static_conv: { ctxt: Proof.context, consts: string list } + -> ({ algebra: code_algebra, eqngr: code_graph } -> Proof.context -> term -> conv) -> Proof.context -> conv - val static_value: Proof.context -> ((term -> term) -> 'a -> 'b) -> string list - -> (code_algebra -> code_graph -> Proof.context -> term -> 'a) + val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'b), consts: string list } + -> ({ algebra: code_algebra, eqngr: code_graph } -> Proof.context -> term -> 'a) -> Proof.context -> term -> 'b end @@ -498,15 +498,15 @@ fun dynamic_value ctxt lift_postproc evaluator = evaluation (value_sandwich ctxt) lift_postproc (dynamic_evaluator evaluator) ctxt; -fun static_conv ctxt consts conv = +fun static_conv { ctxt, consts } conv = let val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts []; - in finalize (value_sandwich ctxt) (conv algebra eqngr) end; + in finalize (value_sandwich ctxt) (conv { algebra = algebra, eqngr = eqngr }) end; -fun static_value ctxt lift_postproc consts evaluator = +fun static_value { ctxt, lift_postproc, consts } evaluator = let val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts []; - in evaluation (value_sandwich ctxt) lift_postproc (evaluator algebra eqngr) end; + in evaluation (value_sandwich ctxt) lift_postproc (evaluator { algebra = algebra, eqngr = eqngr }) end; (** setup **) diff -r f64730f667b9 -r 62da80041afd src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Thu May 15 16:38:31 2014 +0200 +++ b/src/Tools/Code/code_runtime.ML Thu May 15 16:38:31 2014 +0200 @@ -17,14 +17,17 @@ -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a val dynamic_value_exn: 'a cookie -> Proof.context -> string option -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result - val static_value: 'a cookie -> Proof.context -> string option - -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a option - val static_value_strict: 'a cookie -> Proof.context -> string option - -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a - val static_value_exn: 'a cookie -> Proof.context -> string option - -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a Exn.result + val static_value: 'a cookie -> { ctxt: Proof.context, target: string option, + lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } + -> Proof.context -> term -> 'a option + val static_value_strict: 'a cookie -> { ctxt: Proof.context, target: string option, + lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } + -> Proof.context -> term -> 'a + val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option, + lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } + -> Proof.context -> term -> 'a Exn.result val dynamic_holds_conv: Proof.context -> conv - val static_holds_conv: Proof.context -> string list -> Proof.context -> conv + val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv val code_reflect: (string * string list option) list -> string list -> string -> string option -> theory -> theory datatype truth = Holds @@ -122,23 +125,22 @@ fun dynamic_value cookie ctxt some_target postproc t args = partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args); -fun static_evaluator cookie ctxt some_target program consts' = +fun static_evaluator cookie ctxt some_target { program, deps } = let - val evaluator = obtain_evaluator ctxt some_target program (map Constant consts'); + val evaluator = obtain_evaluator ctxt some_target program (map Constant deps); val evaluation' = evaluation cookie ctxt evaluator; in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end; -fun static_value_exn cookie ctxt some_target postproc consts = +fun static_value_exn cookie { ctxt, target, lift_postproc, consts } = let - val evaluator = Code_Thingol.static_value ctxt (Exn.map_result o postproc) consts - (static_evaluator cookie ctxt some_target); + val evaluator = Code_Thingol.static_value { ctxt = ctxt, + lift_postproc = Exn.map_result o lift_postproc, consts = consts } + (static_evaluator cookie ctxt target); in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end; -fun static_value_strict cookie ctxt some_target postproc consts = - Exn.release oo static_value_exn cookie ctxt some_target postproc consts; +fun static_value_strict cookie = Exn.release ooo static_value_exn cookie; -fun static_value cookie thy some_target postproc consts = - partiality_as_none oo static_value_exn cookie thy some_target postproc consts; +fun static_value cookie = partiality_as_none ooo static_value_exn cookie; (* evaluation for truth or nothing *) @@ -185,15 +187,9 @@ check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t) o reject_vars ctxt; -fun static_holds_conv ctxt consts = - Code_Thingol.static_conv ctxt consts (fn program => fn consts' => - let - val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts') - in - fn ctxt' => fn vs_t => fn _ => check_holds_oracle ctxt' evaluator' vs_t o reject_vars ctxt' - end); - -(* o reject_vars ctxt'*) +fun static_holds_conv (ctxt_consts as { ctxt, ... }) = + Code_Thingol.static_conv ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t => + K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt')); end; (*local*) diff -r f64730f667b9 -r 62da80041afd src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Thu May 15 16:38:31 2014 +0200 +++ b/src/Tools/Code/code_simp.ML Thu May 15 16:38:31 2014 +0200 @@ -10,8 +10,10 @@ val dynamic_conv: Proof.context -> conv val dynamic_tac: Proof.context -> int -> tactic val dynamic_value: Proof.context -> term -> term - val static_conv: Proof.context -> simpset option -> string list -> Proof.context -> conv - val static_tac: Proof.context -> simpset option -> string list -> Proof.context -> int -> tactic + val static_conv: { ctxt: Proof.context, simpset: simpset option, consts: string list } + -> Proof.context -> conv + val static_tac: { ctxt: Proof.context, simpset: simpset option, consts: string list } + -> Proof.context -> int -> tactic val setup: theory -> theory val trace: bool Config.T end; @@ -92,15 +94,14 @@ (* evaluation with static code context *) -fun static_conv ctxt some_ss consts = - Code_Thingol.static_conv_simple ctxt consts - (fn program => let val conv' = rewrite_modulo ctxt some_ss program - in fn ctxt' => fn _ => conv' ctxt' end); +fun static_conv { ctxt, simpset, consts } = + Code_Thingol.static_conv_simple { ctxt = ctxt, consts = consts } + (K oo rewrite_modulo ctxt simpset); -fun static_tac ctxt some_ss consts = +fun static_tac { ctxt, simpset, consts } = let - val conv = static_conv ctxt some_ss consts; - val tac = conclude_tac ctxt some_ss; + val conv = static_conv { ctxt = ctxt, simpset = simpset, consts = consts }; + val tac = conclude_tac ctxt simpset; in fn ctxt' => CONVERSION (conv ctxt') THEN' (tac ctxt') end; end; diff -r f64730f667b9 -r 62da80041afd src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Thu May 15 16:38:31 2014 +0200 +++ b/src/Tools/Code/code_thingol.ML Thu May 15 16:38:31 2014 +0200 @@ -91,14 +91,15 @@ val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> term -> 'a - val static_conv: Proof.context -> string list -> (program -> string list - -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv) + val static_conv: { ctxt: Proof.context, consts: string list } + -> ({ program: program, deps: string list } + -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv) -> Proof.context -> conv - val static_conv_simple: Proof.context -> string list + val static_conv_simple: { ctxt: Proof.context, consts: string list } -> (program -> Proof.context -> term -> conv) -> Proof.context -> conv - val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list -> - (program -> string list + val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list } + -> ({ program: program, deps: string list } -> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a) -> Proof.context -> term -> 'a end; @@ -841,32 +842,31 @@ ensure_value ctxt algebra eqngr t ([], program); in subevaluator ctxt t (vs_ty', t') deps end; -fun static_evaluator ctxt evaluator consts algebra eqngr = +fun static_evaluator ctxt evaluator consts { algebra, eqngr } = let fun generate_consts ctxt algebra eqngr = fold_map (ensure_const ctxt algebra eqngr false); - val (consts', program) = + val (deps, program) = invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts; - val subevaluator = evaluator program consts'; + val subevaluator = evaluator { program = program, deps = deps }; in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end; -fun static_evaluator_simple ctxt evaluator consts algebra eqngr = +fun static_evaluator_simple ctxt evaluator consts { algebra, eqngr } = let fun generate_consts ctxt algebra eqngr = fold_map (ensure_const ctxt algebra eqngr false); val (_, program) = invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts; - in evaluator program end; + in evaluator (program: program) end; -fun static_conv ctxt consts conv = - Code_Preproc.static_conv ctxt consts (static_evaluator ctxt (fn program => fn deps => - let val conv' = conv program deps in fn ctxt => fn _ => conv' ctxt end) consts); +fun static_conv (ctxt_consts as { ctxt, consts }) conv = + Code_Preproc.static_conv ctxt_consts (static_evaluator ctxt (K oo conv) consts); -fun static_conv_simple ctxt consts conv = - Code_Preproc.static_conv ctxt consts (static_evaluator_simple ctxt conv consts); +fun static_conv_simple (ctxt_consts as { ctxt, consts }) conv = + Code_Preproc.static_conv ctxt_consts (static_evaluator_simple ctxt conv consts); -fun static_value ctxt postproc consts evaluator = - Code_Preproc.static_value ctxt postproc consts (static_evaluator ctxt evaluator consts); +fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) evaluator = + Code_Preproc.static_value ctxt_postproc_consts (static_evaluator ctxt evaluator consts); (** constant expressions **) diff -r f64730f667b9 -r 62da80041afd src/Tools/nbe.ML --- a/src/Tools/nbe.ML Thu May 15 16:38:31 2014 +0200 +++ b/src/Tools/nbe.ML Thu May 15 16:38:31 2014 +0200 @@ -8,8 +8,8 @@ sig val dynamic_conv: Proof.context -> conv val dynamic_value: Proof.context -> term -> term - val static_conv: Proof.context -> string list -> Proof.context -> conv - val static_value: Proof.context -> string list -> Proof.context -> term -> term + val static_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv + val static_value: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term datatype Univ = Const of int * Univ list (*named (uninterpreted) constants*) @@ -597,16 +597,16 @@ fun dynamic_value ctxt = lift_triv_classes_rew ctxt (Code_Thingol.dynamic_value ctxt I (eval_term ctxt o compile false ctxt)); -fun static_conv ctxt consts = +fun static_conv (ctxt_consts as { ctxt, ... }) = let - val evaluator = Code_Thingol.static_conv ctxt consts - (fn program => fn _ => fn ctxt' => oracle ctxt' (compile true ctxt program)); + val evaluator = Code_Thingol.static_conv ctxt_consts + (fn { program, ... } => fn ctxt' => oracle ctxt' (compile true ctxt program)); in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end; -fun static_value ctxt consts = +fun static_value { ctxt, consts } = let - val evaluator = Code_Thingol.static_value ctxt I consts - (fn program => fn _ => fn ctxt' => eval_term ctxt' (compile false ctxt program)); + val evaluator = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts } + (fn { program, ... } => fn ctxt' => eval_term ctxt' (compile false ctxt program)); in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end; end;