src/Tools/nbe.ML
changeset 56969 7491932da574
parent 56925 601edd9a6859
child 56972 f64730f667b9
     1.1 --- a/src/Tools/nbe.ML	Thu May 15 16:38:28 2014 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu May 15 16:38:29 2014 +0200
     1.3 @@ -501,12 +501,6 @@
     1.4  
     1.5  (* reconstruction *)
     1.6  
     1.7 -fun typ_of_itype resubst_tvar =
     1.8 -  let
     1.9 -    fun typ_of (tyco `%% itys) = Type (tyco, map typ_of itys)
    1.10 -      | typ_of (ITyVar v) = TFree (resubst_tvar v);
    1.11 -  in typ_of end;
    1.12 -
    1.13  fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t =
    1.14    let
    1.15      fun take_until f [] = []
    1.16 @@ -542,17 +536,16 @@
    1.17  
    1.18  (* evaluation with type reconstruction *)
    1.19  
    1.20 -fun eval_term raw_ctxt (nbe_program, idx_tab) resubst_tvar ((vs, ty), t) deps =
    1.21 +fun eval_term raw_ctxt (nbe_program, idx_tab) t_original ((vs, ty), t) deps =
    1.22    let
    1.23      val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
    1.24      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
    1.25 -    val ty' = typ_of_itype resubst_tvar ty;
    1.26 -    fun type_infer t =
    1.27 +    fun type_infer t' =
    1.28        Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
    1.29 -        (Type.constraint ty' t);
    1.30 -    fun check_tvars t =
    1.31 -      if null (Term.add_tvars t []) then t
    1.32 -      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
    1.33 +        (Type.constraint (fastype_of t_original) t');
    1.34 +    fun check_tvars t' =
    1.35 +      if null (Term.add_tvars t' []) then t'
    1.36 +      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t');
    1.37    in
    1.38      compile_term ctxt nbe_program deps (vs, t)
    1.39      |> term_of_univ ctxt idx_tab
    1.40 @@ -592,11 +585,11 @@
    1.41  
    1.42  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
    1.43    (Thm.add_oracle (@{binding normalization_by_evaluation},
    1.44 -    fn (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct) =>
    1.45 -      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps))));
    1.46 +    fn (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct) =>
    1.47 +      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab (term_of ct) vs_ty_t deps))));
    1.48  
    1.49 -fun oracle ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps ct =
    1.50 -  raw_oracle (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct);
    1.51 +fun oracle ctxt nbe_program_idx_tab vs_ty_t deps ct =
    1.52 +  raw_oracle (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct);
    1.53  
    1.54  fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
    1.55    (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));
    1.56 @@ -613,7 +606,7 @@
    1.57  fun static_value ctxt consts =
    1.58    let
    1.59      val evaluator = Code_Thingol.static_value ctxt I consts
    1.60 -      (fn program => fn _ => K (eval_term ctxt (compile true ctxt program)));
    1.61 +      (fn program => fn _ => K (eval_term ctxt (compile false ctxt program)));
    1.62    in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
    1.63  
    1.64  end;