src/Tools/nbe.ML
changeset 56920 d651b944c67e
parent 56245 84fc7dfa3cd4
child 56925 601edd9a6859
     1.1 --- a/src/Tools/nbe.ML	Thu May 08 21:17:23 2014 +0200
     1.2 +++ b/src/Tools/nbe.ML	Fri May 09 08:13:26 2014 +0200
     1.3 @@ -502,10 +502,11 @@
     1.4  
     1.5  (* reconstruction *)
     1.6  
     1.7 -fun typ_of_itype vs (tyco `%% itys) =
     1.8 -      Type (tyco, map (typ_of_itype vs) itys)
     1.9 -  | typ_of_itype vs (ITyVar v) =
    1.10 -      TFree ("'" ^ v, (the o AList.lookup (op =) vs) v);
    1.11 +fun typ_of_itype resubst_tvar =
    1.12 +  let
    1.13 +    fun typ_of (tyco `%% itys) = Type (tyco, map typ_of itys)
    1.14 +      | typ_of (ITyVar v) = TFree (resubst_tvar v);
    1.15 +  in typ_of end;
    1.16  
    1.17  fun term_of_univ ctxt (idx_tab : Code_Symbol.T Inttab.table) t =
    1.18    let
    1.19 @@ -542,11 +543,11 @@
    1.20  
    1.21  (* evaluation with type reconstruction *)
    1.22  
    1.23 -fun eval_term raw_ctxt (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
    1.24 +fun eval_term raw_ctxt (nbe_program, idx_tab) resubst_tvar ((vs, ty), t) deps =
    1.25    let
    1.26      val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
    1.27      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
    1.28 -    val ty' = typ_of_itype vs0 ty;
    1.29 +    val ty' = typ_of_itype resubst_tvar ty;
    1.30      fun type_infer t =
    1.31        Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
    1.32          (Type.constraint ty' t);
    1.33 @@ -592,11 +593,11 @@
    1.34  
    1.35  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
    1.36    (Thm.add_oracle (@{binding normalization_by_evaluation},
    1.37 -    fn (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
    1.38 -      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab vsp_ty_t deps))));
    1.39 +    fn (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct) =>
    1.40 +      mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps))));
    1.41  
    1.42 -fun oracle ctxt nbe_program_idx_tab vsp_ty_t deps ct =
    1.43 -  raw_oracle (ctxt, nbe_program_idx_tab, vsp_ty_t, deps, ct);
    1.44 +fun oracle ctxt nbe_program_idx_tab resubst_tvars vs_ty_t deps ct =
    1.45 +  raw_oracle (ctxt, nbe_program_idx_tab, resubst_tvars, vs_ty_t, deps, ct);
    1.46  
    1.47  fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
    1.48    (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt));