syntactic means to prevent accidental mixup of static and dynamic context

--- 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;

--- 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 **)

--- 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*)
 

--- 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;

--- 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 **)

--- 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;