# HG changeset patch
# User haftmann
# Date 1400164709 -7200
# Node ID 7491932da5743dfde2b7e461ec48f14e5eedb3a4
# Parent  d2b1d95eb7227049f07c78f6666b63f551e52178
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor

diff -r d2b1d95eb722 -r 7491932da574 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu May 15 16:38:28 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu May 15 16:38:29 2014 +0200
@@ -181,7 +181,7 @@
 in
 
 fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
-  (fn program => fn _ => fn vs_t => fn deps =>
+  (fn program => fn vs_t => fn deps =>
     check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t)
       o reject_vars ctxt;
 
@@ -190,7 +190,7 @@
     let
       val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts')
     in
-      fn ctxt' => fn _ => fn vs_t => fn _ => check_holds_oracle ctxt' evaluator' vs_t o reject_vars ctxt'
+      fn ctxt' => fn vs_t => fn _ => check_holds_oracle ctxt' evaluator' vs_t o reject_vars ctxt'
     end);
 
 (* o reject_vars ctxt'*)
diff -r d2b1d95eb722 -r 7491932da574 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Thu May 15 16:38:28 2014 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu May 15 16:38:29 2014 +0200
@@ -76,7 +76,7 @@
 (* evaluation with dynamic code context *)
 
 fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt
-  (fn program => fn _ => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
+  (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
 
 fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt)
   THEN' conclude_tac ctxt NONE ctxt;
diff -r d2b1d95eb722 -r 7491932da574 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu May 15 16:38:28 2014 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu May 15 16:38:29 2014 +0200
@@ -86,20 +86,20 @@
   val read_const_exprs: Proof.context -> string list -> string list
   val consts_program: theory -> string list -> program
   val dynamic_conv: Proof.context -> (program
-    -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv)
+    -> typscheme * iterm -> Code_Symbol.T list -> conv)
     -> conv
   val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
-    -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a)
+    -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     -> term -> 'a
   val static_conv: Proof.context -> string list -> (program -> string list
-    -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv)
+    -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
     -> Proof.context -> conv
   val static_conv_simple: Proof.context -> string list
     -> (program -> Proof.context -> term -> conv)
     -> Proof.context -> conv
   val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list ->
     (program -> string list
-      -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a)
+      -> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     -> Proof.context -> term -> 'a
 end;
 
@@ -795,18 +795,11 @@
 
 (* value evaluation *)
 
-fun normalize_tvars t = 
+fun ensure_value ctxt algbr eqngr t =
   let
     val ty = fastype_of t;
-    val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
+    val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
-    val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
-    val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
-  in ((vs_original, (vs_normalized, normalize ty)), map_types normalize t) end;
-
-fun ensure_value ctxt algbr eqngr t_original =
-  let
-    val ((vs_original, (vs, ty)), t) = normalize_tvars t_original;
     val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t;
     val dummy_constant = Constant @{const_name Pure.dummy_pattern};
     val stmt_value =
@@ -817,14 +810,13 @@
         (((vs, ty), [(([], t), (NONE, true))]), NONE));
     fun term_value (_, program1) =
       let
-        val Fun ((vs_ty as (vs, _), [(([], t), _)]), _) =
+        val Fun ((vs_ty, [(([], t), _)]), _) =
           Code_Symbol.Graph.get_node program1 dummy_constant;
         val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
         val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
         val deps_all = Code_Symbol.Graph.all_succs program2 deps';
         val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
-        val vs_mapping = map fst vs ~~ vs_original;
-      in (((the o AList.lookup (op =) vs_mapping), (program3, ((vs_ty, t), deps'))), (deps', program2)) end;
+       in ((program3, ((vs_ty, t), deps')), (deps', program2)) end;
   in
     ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern}
     #> snd
@@ -833,21 +825,21 @@
 
 fun dynamic_evaluator ctxt evaluator algebra eqngr t =
   let
-    val ((resubst_tvar, (program, ((vs_ty', t'), deps))), _) =
+    val ((program, (vs_ty_t', deps)), _) =
       invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
-  in evaluator program resubst_tvar (vs_ty', t') deps end;
+  in evaluator program t vs_ty_t' deps end;
 
 fun dynamic_conv ctxt conv =
-  Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt conv);
+  Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt (fn program => fn _ => conv program));
 
 fun dynamic_value ctxt postproc evaluator =
   Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
 
 fun static_subevaluator ctxt subevaluator algebra eqngr program t =
   let
-    val ((resubst_tvar, (_, ((vs_ty', t'), deps))), _) =
+    val ((_, ((vs_ty', t'), deps)), _) =
       ensure_value ctxt algebra eqngr t ([], program);
-  in subevaluator ctxt resubst_tvar (vs_ty', t') deps end;
+  in subevaluator ctxt t (vs_ty', t') deps end;
 
 fun static_evaluator ctxt evaluator consts algebra eqngr =
   let
@@ -867,7 +859,8 @@
   in evaluator program end;
 
 fun static_conv ctxt consts conv =
-  Code_Preproc.static_conv ctxt consts (static_evaluator ctxt conv consts);
+  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_simple ctxt consts conv =
   Code_Preproc.static_conv ctxt consts (static_evaluator_simple ctxt conv consts);
diff -r d2b1d95eb722 -r 7491932da574 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu May 15 16:38:28 2014 +0200
+++ b/src/Tools/nbe.ML	Thu May 15 16:38:29 2014 +0200
@@ -501,12 +501,6 @@
 
 (* reconstruction *)
 
-fun typ_of_itype resubst_tvar =
-  let
-    fun typ_of (tyco `%% itys) = Type (tyco, map typ_of itys)
-      | typ_of (ITyVar v) = TFree (resubst_tvar v);
-  in typ_of end;
-
 fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t =
   let
     fun take_until f [] = []
@@ -542,17 +536,16 @@
 
 (* evaluation with type reconstruction *)
 
-fun eval_term raw_ctxt (nbe_program, idx_tab) resubst_tvar ((vs, ty), t) deps =
+fun eval_term raw_ctxt (nbe_program, idx_tab) t_original ((vs, ty), t) deps =
   let
     val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
     val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
-    val ty' = typ_of_itype resubst_tvar ty;
-    fun type_infer t =
+    fun type_infer t' =
       Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
-        (Type.constraint ty' t);
-    fun check_tvars t =
-      if null (Term.add_tvars t []) then t
-      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
+        (Type.constraint (fastype_of t_original) t');
+    fun check_tvars t' =
+      if null (Term.add_tvars t' []) then t'
+      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t');
   in
     compile_term ctxt nbe_program deps (vs, t)
     |> term_of_univ ctxt idx_tab
@@ -592,11 +585,11 @@
 
 val (_, raw_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (@{binding normalization_by_evaluation},
-    fn (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct) =>
-      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps))));
+    fn (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct) =>
+      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab (term_of ct) vs_ty_t deps))));
 
-fun oracle ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps ct =
-  raw_oracle (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct);
+fun oracle ctxt nbe_program_idx_tab vs_ty_t deps ct =
+  raw_oracle (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct);
 
 fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
   (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));
@@ -613,7 +606,7 @@
 fun static_value ctxt consts =
   let
     val evaluator = Code_Thingol.static_value ctxt I consts
-      (fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
+      (fn program => fn _ => K (eval_term ctxt (compile false ctxt program)));
   in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
 
 end;