# HG changeset patch
# User haftmann
# Date 1464269270 -7200
# Node ID 80a91e0e236e556858aebe2950af531f8e0605bb
# Parent  84c6dd947b751ff6213d1abbbcc5d0da6af09b3d
corrected closure scope of static_conv_thingol;
clarified implementation and names

diff -r 84c6dd947b75 -r 80a91e0e236e src/Doc/more_antiquote.ML
--- a/src/Doc/more_antiquote.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Doc/more_antiquote.ML	Thu May 26 15:27:50 2016 +0200
@@ -43,7 +43,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val const = Code.check_const thy raw_const;
-    val (_, eqngr) = Code_Preproc.obtain true ctxt [const] [];
+    val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
     val thms = Code_Preproc.cert eqngr const
       |> Code.equations_of_cert thy
diff -r 84c6dd947b75 -r 80a91e0e236e src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu May 26 15:27:50 2016 +0200
@@ -21,7 +21,8 @@
   val sortargs: code_graph -> string -> sort list
   val all: code_graph -> string list
   val pretty: Proof.context -> code_graph -> Pretty.T
-  val obtain: bool -> Proof.context -> string list -> term list -> code_algebra * code_graph
+  val obtain: bool -> Proof.context -> string list -> term list ->
+    { algebra: code_algebra, eqngr: code_graph }
   val dynamic_conv: Proof.context
     -> (code_algebra -> code_graph -> term -> conv) -> conv
   val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'b)
@@ -123,20 +124,20 @@
 fun trans_conv_rule conv eq = trans_comb eq (conv (Thm.rhs_of eq));
 
 structure Sandwich : sig
-  type T = Proof.context -> cterm -> (thm -> thm) * cterm;
+  type T = Proof.context -> cterm -> (Proof.context -> thm -> thm) * cterm;
   val chain: T -> T -> T
-  val lift: (Proof.context -> cterm -> (cterm -> thm) * thm) -> T
+  val lift: (Proof.context -> cterm -> (Proof.context -> cterm -> thm) * thm) -> T
   val conversion: T -> (Proof.context -> term -> conv) -> Proof.context -> conv;
   val computation: T -> ((term -> term) -> 'a -> 'b) ->
     (Proof.context -> term -> 'a) -> Proof.context -> term -> 'b;
 end = struct
 
-type T = Proof.context -> cterm -> (thm -> thm) * cterm;
+type T = Proof.context -> cterm -> (Proof.context -> thm -> thm) * cterm;
 
 fun chain sandwich2 sandwich1 ctxt =
   sandwich1 ctxt
   ##>> sandwich2 ctxt
-  #>> (op o);
+  #>> (fn (f, g) => fn ctxt => f ctxt o g ctxt);
 
 fun lift conv_sandwhich ctxt ct =
   let
@@ -144,21 +145,23 @@
     fun potentail_trans_comb eq1 eq2 =
       if matches_transitive eq1 eq2 then trans_comb eq1 eq2 else eq2;
         (*weakened protocol for plain term evaluation*)
-  in (trans_conv_rule postproc_conv o potentail_trans_comb eq, Thm.rhs_of eq) end;
+  in (fn ctxt => trans_conv_rule (postproc_conv ctxt) o potentail_trans_comb eq, Thm.rhs_of eq) end;
 
 fun conversion sandwich conv ctxt ct =
   let
     val (postproc, ct') = sandwich ctxt ct;
-  in postproc (conv ctxt (Thm.term_of ct') ct') end;
+    val thm = conv ctxt (Thm.term_of ct') ct';
+    val thm' = postproc ctxt thm;
+  in thm' end;
 
 fun computation sandwich lift_postproc eval ctxt t =
   let
     val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t);
-  in
-    Thm.term_of ct'
-    |> eval ctxt
-    |> lift_postproc (Thm.term_of o Thm.rhs_of o postproc o Thm.reflexive o Thm.cterm_of ctxt)
-  end;
+    val result = eval ctxt (Thm.term_of ct');
+    val result' = lift_postproc
+      (Thm.term_of o Thm.rhs_of o postproc ctxt o Thm.reflexive o Thm.cterm_of ctxt)
+      result
+  in result' end;
 
 end;
 
@@ -178,9 +181,9 @@
         vs_original vs_normalized;
   in
     if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
-    then (I, ct)
+    then (K I, ct)
     else
-     (Thm.instantiate (normalization, []) o Thm.varifyT_global,
+     (K (Thm.instantiate (normalization, []) o Thm.varifyT_global),
       Thm.cterm_of ctxt (map_types normalize t))
   end;
 
@@ -194,8 +197,8 @@
       |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
   in
     if null all_vars
-    then (I, ct)
-    else (fold apply_beta all_vars, fold_rev Thm.lambda all_vars ct)
+    then (K I, ct)
+    else (K (fold apply_beta all_vars), fold_rev Thm.lambda all_vars ct)
   end;
 
 fun simplifier_conv_sandwich ctxt =
@@ -206,12 +209,13 @@
     fun pre_conv ctxt' =
       Simplifier.rewrite (put_simpset pre ctxt')
       #> trans_conv_rule (Axclass.unoverload_conv ctxt')
-    fun post_conv ctxt' =
-      Axclass.overload_conv ctxt'
-      #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt'))
-  in fn ctxt' => pre_conv ctxt' #> pair (post_conv ctxt') end;
+    fun post_conv ctxt'' =
+      Axclass.overload_conv ctxt''
+      #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt''))
+  in fn ctxt' => pre_conv ctxt' #> pair post_conv end;
 
-fun simplifier_sandwich ctxt = Sandwich.lift (simplifier_conv_sandwich ctxt);
+fun simplifier_sandwich ctxt =
+  Sandwich.lift (simplifier_conv_sandwich ctxt);
 
 fun value_sandwich ctxt =
   normalized_tfrees_sandwich
@@ -548,19 +552,18 @@
 
 fun obtain ignore_cache ctxt consts ts = apsnd snd
   (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
-    (extend_arities_eqngr ctxt consts ts));
+    (extend_arities_eqngr ctxt consts ts))
+  |> (fn (algebra, eqngr) => { algebra = algebra, eqngr = eqngr });
 
 fun dynamic_evaluation eval ctxt t =
   let
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t [];
-    val (algebra, eqngr) = obtain false ctxt consts [t];
+    val { algebra, eqngr } = obtain false ctxt consts [t];
   in eval algebra eqngr t end;
 
 fun static_evaluation ctxt consts eval =
-  let
-    val (algebra, eqngr) = obtain true ctxt consts [];
-  in eval { algebra = algebra, eqngr = eqngr } end;
+  eval (obtain true ctxt consts []);
 
 fun dynamic_conv ctxt conv =
   Sandwich.conversion (value_sandwich ctxt)
diff -r 84c6dd947b75 -r 80a91e0e236e src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
@@ -28,15 +28,15 @@
     -> Proof.context -> term -> 'a Exn.result
   val dynamic_holds_conv: Proof.context -> conv
   val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
-  val static_value': (Proof.context -> term -> 'a) cookie
+  val fully_static_value: (Proof.context -> term -> 'a) cookie
     -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
            consts: (string * typ) list, T: typ }
     -> Proof.context -> term -> 'a option (*EXPERIMENTAL!*)
-  val static_value_strict': (Proof.context -> term -> 'a) cookie
+  val fully_static_value_strict: (Proof.context -> term -> 'a) cookie
     -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
            consts: (string * typ) list, T: typ }
     -> Proof.context -> term -> 'a (*EXPERIMENTAL!*)
-  val static_value_exn': (Proof.context -> term -> 'a) cookie
+  val fully_static_value_exn: (Proof.context -> term -> 'a) cookie
     -> { ctxt: Proof.context, lift_postproc: (term -> term) -> 'a -> 'a,
            consts: (string * typ) list, T: typ }
     -> Proof.context -> term -> 'a Exn.result (*EXPERIMENTAL!*)
@@ -201,7 +201,7 @@
 end; (*local*)
 
 
-(** full static evaluation -- still with limited coverage! **)
+(** fully static evaluation -- still with limited coverage! **)
 
 fun evaluation_code ctxt module_name program tycos consts =
   let
@@ -293,7 +293,7 @@
       ml_name_for_typ = ml_name_for_typ } Ts
   end;
 
-fun compile_evaluator cookie ctxt cs_code cTs T { program, deps } =
+fun compile_computation cookie ctxt cs_code cTs T { program, deps } =
   let
     val (context_code, (_, const_map)) =
       evaluation_code ctxt structure_generated program [] cs_code;
@@ -302,21 +302,21 @@
     val of_term = value ctxt cookie (context_code ^ "\n" ^ of_term_code, List.last ml_names);
   in fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t end;
 
-fun static_value_exn' cookie { ctxt, lift_postproc, consts, T } =
+fun fully_static_value_exn cookie { ctxt, lift_postproc, consts, T } =
   let
     val thy = Proof_Context.theory_of ctxt;
     val cs_code = map (Axclass.unoverload_const thy) consts;
     val cTs = map2 (fn (_, T) => fn c => (c, T)) consts cs_code;
-    val evaluator = Code_Thingol.static_value { ctxt = ctxt,
+    val computation = Code_Thingol.static_value { ctxt = ctxt,
       lift_postproc = Exn.map_res o lift_postproc, consts = cs_code }
-      (compile_evaluator cookie ctxt cs_code cTs T);
+      (compile_computation cookie ctxt cs_code cTs T);
   in fn ctxt' =>
-    evaluator ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T
+    computation ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T
   end;
 
-fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie;
+fun fully_static_value_strict cookie = Exn.release ooo fully_static_value_exn cookie;
 
-fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
+fun fully_static_value cookie = partiality_as_none ooo fully_static_value_exn cookie;
 
 
 (** code antiquotation **)
diff -r 84c6dd947b75 -r 80a91e0e236e src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu May 26 15:27:50 2016 +0200
@@ -95,7 +95,7 @@
 
 fun static_conv { ctxt, simpset, consts } =
   Code_Thingol.static_conv_isa { ctxt = ctxt, consts = consts }
-    (K oo rewrite_modulo ctxt simpset);
+    (fn program => K o rewrite_modulo ctxt simpset program);
 
 fun static_tac { ctxt, simpset, consts } =
   let
diff -r 84c6dd947b75 -r 80a91e0e236e src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
@@ -104,7 +104,7 @@
     -> Proof.context -> term -> 'a
 end;
 
-structure Code_Thingol: CODE_THINGOL =
+structure Code_Thingol : CODE_THINGOL =
 struct
 
 open Basic_Code_Symbol;
@@ -776,36 +776,43 @@
   val empty = Code_Symbol.Graph.empty;
 );
 
-fun invoke_generation ignore_cache ctxt (algebra, eqngr) generate thing =
+fun invoke_generation ignore_cache ctxt generate thing =
   Program.change_yield
     (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
     (fn program => ([], program)
-      |> generate ctxt algebra eqngr thing
+      |> generate thing
       |-> (fn thing => fn (_, program) => (thing, program)));
 
 
 (* program generation *)
 
-fun consts_program_internal ctxt permissive consts =
-  let
-    fun generate_consts ctxt algebra eqngr =
-      fold_map (ensure_const ctxt algebra eqngr permissive);
-  in
-    invoke_generation permissive ctxt
-      (Code_Preproc.obtain false ctxt consts [])
-      generate_consts consts
-    |> snd
-  end;
+fun invoke_generation_for_consts ctxt { ignore_cache, permissive }
+  { algebra, eqngr } consts =
+  invoke_generation ignore_cache ctxt
+    (fold_map (ensure_const ctxt algebra eqngr permissive)) consts;
+
+fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts =
+  invoke_generation_for_consts ctxt
+    { ignore_cache = ignore_cache_and_permissive, permissive = ignore_cache_and_permissive }
+    (Code_Preproc.obtain ignore_cache_and_permissive ctxt consts []) consts
+  |> snd;
 
-fun consts_program_permissive thy = consts_program_internal thy true;
+fun invoke_generation_for_consts'' ctxt algebra_eqngr =
+  invoke_generation_for_consts ctxt
+    { ignore_cache = true, permissive = false }
+    algebra_eqngr
+  #> (fn (deps, program) => { deps = deps, program = program });
 
-fun consts_program thy consts =
+fun consts_program_permissive ctxt =
+  invoke_generation_for_consts' ctxt true;
+
+fun consts_program ctxt consts =
   let
     fun project program = Code_Symbol.Graph.restrict
       (member (op =) (Code_Symbol.Graph.all_succs program
         (map Constant consts))) program;
   in
-    consts_program_internal thy false consts
+    invoke_generation_for_consts' ctxt false consts
     |> project
   end;
 
@@ -843,8 +850,7 @@
 fun dynamic_evaluation eval ctxt algebra eqngr t =
   let
     val ((program, (vs_ty_t', deps)), _) =
-      invoke_generation false ctxt
-        (algebra, eqngr) ensure_value t;
+      invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t;
   in eval program t vs_ty_t' deps end;
 
 fun dynamic_conv ctxt conv =
@@ -855,44 +861,42 @@
   Code_Preproc.dynamic_value ctxt postproc
     (dynamic_evaluation comp ctxt);
 
-fun static_evaluation ctxt consts algebra eqngr static_eval =
+fun static_evaluation ctxt consts algebra_eqngr static_eval =
+  static_eval (invoke_generation_for_consts'' ctxt algebra_eqngr consts);
+
+fun static_evaluation_thingol ctxt consts (algebra_eqngr as { algebra, eqngr }) static_eval =
   let
-    fun generate_consts ctxt algebra eqngr =
-      fold_map (ensure_const ctxt algebra eqngr false);
-    val (deps, program) =
-      invoke_generation true ctxt
-        (algebra, eqngr) generate_consts consts;
-  in static_eval { program = program, deps = deps } end;
-
-fun static_evaluation_thingol ctxt consts algebra eqngr static_eval =
-  let
-    fun evaluation' program dynamic_eval ctxt t =
+    fun evaluation program dynamic_eval ctxt t =
       let
         val ((_, ((vs_ty', t'), deps)), _) =
           ensure_value ctxt algebra eqngr t ([], program);
       in dynamic_eval ctxt t (vs_ty', t') deps end;
-    fun evaluation static_eval { program, deps } =
-      evaluation' program (static_eval { program = program, deps = deps });
   in
-    static_evaluation ctxt consts algebra eqngr
-      (evaluation static_eval)
+    static_evaluation ctxt consts algebra_eqngr (fn program_deps =>
+      evaluation (#program program_deps) (static_eval program_deps))
   end;
 
-fun static_evaluation_isa ctxt consts algebra eqngr static_eval =
-  static_evaluation ctxt consts algebra eqngr
-    (fn { program, ... } => static_eval (program: program));
+fun static_evaluation_isa ctxt consts algebra_eqngr static_eval =
+  static_evaluation ctxt consts algebra_eqngr (fn program_deps =>
+    (static_eval (#program program_deps)));
 
 fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv =
-  Code_Preproc.static_conv ctxt_consts (fn { algebra, eqngr } =>
-    static_evaluation_thingol ctxt consts algebra eqngr (K oo conv));
+  Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr =>
+    static_evaluation_thingol ctxt consts algebra_eqngr
+      (fn program_deps =>
+        let
+          val static_conv = conv program_deps;
+        in 
+          fn ctxt => fn _ => fn vs_ty => fn deps => static_conv ctxt vs_ty deps
+        end));
 
 fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv =
-  Code_Preproc.static_conv ctxt_consts (fn { algebra, eqngr } =>
-    static_evaluation_isa ctxt consts algebra eqngr conv);
+  Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr =>
+    static_evaluation_isa ctxt consts algebra_eqngr conv);
 
 fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) comp =
-  Code_Preproc.static_value ctxt_postproc_consts (fn { algebra, eqngr } =>
-    static_evaluation_thingol ctxt consts algebra eqngr comp);
+  Code_Preproc.static_value ctxt_postproc_consts (fn algebra_eqngr =>
+    static_evaluation_thingol ctxt consts algebra_eqngr comp);
 
 
 (** constant expressions **)
@@ -931,7 +935,7 @@
 
 fun code_depgr ctxt consts =
   let
-    val (_, eqngr) = Code_Preproc.obtain true ctxt consts [];
+    val { eqngr, ... } = Code_Preproc.obtain true ctxt consts [];
     val all_consts = Graph.all_succs eqngr consts;
   in Graph.restrict (member (op =) all_consts) eqngr end;