dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
authorhaftmann
Thu May 15 16:38:29 2014 +0200 (2014-05-15)
changeset 569697491932da574
parent 56968 d2b1d95eb722
child 56970 a3f911785efa
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu May 15 16:38:28 2014 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu May 15 16:38:29 2014 +0200
     1.3 @@ -181,7 +181,7 @@
     1.4  in
     1.5  
     1.6  fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
     1.7 -  (fn program => fn _ => fn vs_t => fn deps =>
     1.8 +  (fn program => fn vs_t => fn deps =>
     1.9      check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t)
    1.10        o reject_vars ctxt;
    1.11  
    1.12 @@ -190,7 +190,7 @@
    1.13      let
    1.14        val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts')
    1.15      in
    1.16 -      fn ctxt' => fn _ => fn vs_t => fn _ => check_holds_oracle ctxt' evaluator' vs_t o reject_vars ctxt'
    1.17 +      fn ctxt' => fn vs_t => fn _ => check_holds_oracle ctxt' evaluator' vs_t o reject_vars ctxt'
    1.18      end);
    1.19  
    1.20  (* o reject_vars ctxt'*)
     2.1 --- a/src/Tools/Code/code_simp.ML	Thu May 15 16:38:28 2014 +0200
     2.2 +++ b/src/Tools/Code/code_simp.ML	Thu May 15 16:38:29 2014 +0200
     2.3 @@ -76,7 +76,7 @@
     2.4  (* evaluation with dynamic code context *)
     2.5  
     2.6  fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt
     2.7 -  (fn program => fn _ => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
     2.8 +  (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
     2.9  
    2.10  fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt)
    2.11    THEN' conclude_tac ctxt NONE ctxt;
     3.1 --- a/src/Tools/Code/code_thingol.ML	Thu May 15 16:38:28 2014 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Thu May 15 16:38:29 2014 +0200
     3.3 @@ -86,20 +86,20 @@
     3.4    val read_const_exprs: Proof.context -> string list -> string list
     3.5    val consts_program: theory -> string list -> program
     3.6    val dynamic_conv: Proof.context -> (program
     3.7 -    -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv)
     3.8 +    -> typscheme * iterm -> Code_Symbol.T list -> conv)
     3.9      -> conv
    3.10    val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
    3.11 -    -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a)
    3.12 +    -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
    3.13      -> term -> 'a
    3.14    val static_conv: Proof.context -> string list -> (program -> string list
    3.15 -    -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> conv)
    3.16 +    -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
    3.17      -> Proof.context -> conv
    3.18    val static_conv_simple: Proof.context -> string list
    3.19      -> (program -> Proof.context -> term -> conv)
    3.20      -> Proof.context -> conv
    3.21    val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list ->
    3.22      (program -> string list
    3.23 -      -> Proof.context -> (string -> (string * sort)) -> typscheme * iterm -> Code_Symbol.T list -> 'a)
    3.24 +      -> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
    3.25      -> Proof.context -> term -> 'a
    3.26  end;
    3.27  
    3.28 @@ -795,18 +795,11 @@
    3.29  
    3.30  (* value evaluation *)
    3.31  
    3.32 -fun normalize_tvars t = 
    3.33 +fun ensure_value ctxt algbr eqngr t =
    3.34    let
    3.35      val ty = fastype_of t;
    3.36 -    val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
    3.37 +    val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
    3.38        o dest_TFree))) t [];
    3.39 -    val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
    3.40 -    val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
    3.41 -  in ((vs_original, (vs_normalized, normalize ty)), map_types normalize t) end;
    3.42 -
    3.43 -fun ensure_value ctxt algbr eqngr t_original =
    3.44 -  let
    3.45 -    val ((vs_original, (vs, ty)), t) = normalize_tvars t_original;
    3.46      val t' = annotate ctxt algbr eqngr (@{const_name Pure.dummy_pattern}, ty) [] t;
    3.47      val dummy_constant = Constant @{const_name Pure.dummy_pattern};
    3.48      val stmt_value =
    3.49 @@ -817,14 +810,13 @@
    3.50          (((vs, ty), [(([], t), (NONE, true))]), NONE));
    3.51      fun term_value (_, program1) =
    3.52        let
    3.53 -        val Fun ((vs_ty as (vs, _), [(([], t), _)]), _) =
    3.54 +        val Fun ((vs_ty, [(([], t), _)]), _) =
    3.55            Code_Symbol.Graph.get_node program1 dummy_constant;
    3.56          val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
    3.57          val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
    3.58          val deps_all = Code_Symbol.Graph.all_succs program2 deps';
    3.59          val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
    3.60 -        val vs_mapping = map fst vs ~~ vs_original;
    3.61 -      in (((the o AList.lookup (op =) vs_mapping), (program3, ((vs_ty, t), deps'))), (deps', program2)) end;
    3.62 +       in ((program3, ((vs_ty, t), deps')), (deps', program2)) end;
    3.63    in
    3.64      ensure_stmt Constant stmt_value @{const_name Pure.dummy_pattern}
    3.65      #> snd
    3.66 @@ -833,21 +825,21 @@
    3.67  
    3.68  fun dynamic_evaluator ctxt evaluator algebra eqngr t =
    3.69    let
    3.70 -    val ((resubst_tvar, (program, ((vs_ty', t'), deps))), _) =
    3.71 +    val ((program, (vs_ty_t', deps)), _) =
    3.72        invoke_generation false (Proof_Context.theory_of ctxt) (algebra, eqngr) ensure_value t;
    3.73 -  in evaluator program resubst_tvar (vs_ty', t') deps end;
    3.74 +  in evaluator program t vs_ty_t' deps end;
    3.75  
    3.76  fun dynamic_conv ctxt conv =
    3.77 -  Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt conv);
    3.78 +  Code_Preproc.dynamic_conv ctxt (dynamic_evaluator ctxt (fn program => fn _ => conv program));
    3.79  
    3.80  fun dynamic_value ctxt postproc evaluator =
    3.81    Code_Preproc.dynamic_value ctxt postproc (dynamic_evaluator ctxt evaluator);
    3.82  
    3.83  fun static_subevaluator ctxt subevaluator algebra eqngr program t =
    3.84    let
    3.85 -    val ((resubst_tvar, (_, ((vs_ty', t'), deps))), _) =
    3.86 +    val ((_, ((vs_ty', t'), deps)), _) =
    3.87        ensure_value ctxt algebra eqngr t ([], program);
    3.88 -  in subevaluator ctxt resubst_tvar (vs_ty', t') deps end;
    3.89 +  in subevaluator ctxt t (vs_ty', t') deps end;
    3.90  
    3.91  fun static_evaluator ctxt evaluator consts algebra eqngr =
    3.92    let
    3.93 @@ -867,7 +859,8 @@
    3.94    in evaluator program end;
    3.95  
    3.96  fun static_conv ctxt consts conv =
    3.97 -  Code_Preproc.static_conv ctxt consts (static_evaluator ctxt conv consts);
    3.98 +  Code_Preproc.static_conv ctxt consts (static_evaluator ctxt (fn program => fn deps =>
    3.99 +    let val conv' = conv program deps in fn ctxt => fn _ => conv' ctxt end) consts);
   3.100  
   3.101  fun static_conv_simple ctxt consts conv =
   3.102    Code_Preproc.static_conv ctxt consts (static_evaluator_simple ctxt conv consts);
     4.1 --- a/src/Tools/nbe.ML	Thu May 15 16:38:28 2014 +0200
     4.2 +++ b/src/Tools/nbe.ML	Thu May 15 16:38:29 2014 +0200
     4.3 @@ -501,12 +501,6 @@
     4.4  
     4.5  (* reconstruction *)
     4.6  
     4.7 -fun typ_of_itype resubst_tvar =
     4.8 -  let
     4.9 -    fun typ_of (tyco `%% itys) = Type (tyco, map typ_of itys)
    4.10 -      | typ_of (ITyVar v) = TFree (resubst_tvar v);
    4.11 -  in typ_of end;
    4.12 -
    4.13  fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t =
    4.14    let
    4.15      fun take_until f [] = []
    4.16 @@ -542,17 +536,16 @@
    4.17  
    4.18  (* evaluation with type reconstruction *)
    4.19  
    4.20 -fun eval_term raw_ctxt (nbe_program, idx_tab) resubst_tvar ((vs, ty), t) deps =
    4.21 +fun eval_term raw_ctxt (nbe_program, idx_tab) t_original ((vs, ty), t) deps =
    4.22    let
    4.23      val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
    4.24      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
    4.25 -    val ty' = typ_of_itype resubst_tvar ty;
    4.26 -    fun type_infer t =
    4.27 +    fun type_infer t' =
    4.28        Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
    4.29 -        (Type.constraint ty' t);
    4.30 -    fun check_tvars t =
    4.31 -      if null (Term.add_tvars t []) then t
    4.32 -      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
    4.33 +        (Type.constraint (fastype_of t_original) t');
    4.34 +    fun check_tvars t' =
    4.35 +      if null (Term.add_tvars t' []) then t'
    4.36 +      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t');
    4.37    in
    4.38      compile_term ctxt nbe_program deps (vs, t)
    4.39      |> term_of_univ ctxt idx_tab
    4.40 @@ -592,11 +585,11 @@
    4.41  
    4.42  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
    4.43    (Thm.add_oracle (@{binding normalization_by_evaluation},
    4.44 -    fn (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct) =>
    4.45 -      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps))));
    4.46 +    fn (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct) =>
    4.47 +      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab (term_of ct) vs_ty_t deps))));
    4.48  
    4.49 -fun oracle ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps ct =
    4.50 -  raw_oracle (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct);
    4.51 +fun oracle ctxt nbe_program_idx_tab vs_ty_t deps ct =
    4.52 +  raw_oracle (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct);
    4.53  
    4.54  fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
    4.55    (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));
    4.56 @@ -613,7 +606,7 @@
    4.57  fun static_value ctxt consts =
    4.58    let
    4.59      val evaluator = Code_Thingol.static_value ctxt I consts
    4.60 -      (fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
    4.61 +      (fn program => fn _ => K (eval_term ctxt (compile false ctxt program)));
    4.62    in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
    4.63  
    4.64  end;