normalize type variables of evaluation term by conversion
authorhaftmann
Thu May 15 16:38:17 2014 +0200 (2014-05-15)
changeset 56967c3746e999805
parent 56966 01637dd1260c
child 56968 d2b1d95eb722
normalize type variables of evaluation term by conversion
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/Tools/Code/code_preproc.ML	Thu May 15 20:48:14 2014 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:17 2014 +0200
     1.3 @@ -126,6 +126,24 @@
     1.4      |> fold apply_beta all_vars
     1.5    end;
     1.6  
     1.7 +fun normalized_tfrees ctxt conv ct =
     1.8 +  let
     1.9 +    val cert = cterm_of (Proof_Context.theory_of ctxt);
    1.10 +    val t = term_of ct;
    1.11 +    val vs_original = fold_term_types (K (fold_atyps (insert (eq_fst op =)
    1.12 +      o dest_TFree))) t [];
    1.13 +    val vs_normalized = Name.invent_names Name.context Name.aT (map snd vs_original);
    1.14 +    val normalize = map_type_tfree (TFree o the o AList.lookup (op =) (vs_original ~~ vs_normalized));
    1.15 +    val normalization =
    1.16 +      map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), TFree (v, sort))) vs_original vs_normalized;
    1.17 +    val ct_normalized = cert (map_types normalize t);
    1.18 +  in
    1.19 +    ct_normalized
    1.20 +    |> conv
    1.21 +    |> Thm.varifyT_global
    1.22 +    |> Thm.certify_instantiate (normalization, [])
    1.23 +  end;
    1.24 +
    1.25  fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
    1.26  
    1.27  fun term_of_conv ctxt conv =
    1.28 @@ -459,7 +477,7 @@
    1.29    (Wellsorted.change_yield (if ignore_cache then NONE else SOME thy)
    1.30      (extend_arities_eqngr (Proof_Context.init_global thy) consts ts));
    1.31  
    1.32 -fun dynamic_conv ctxt conv = no_variables_conv ctxt (fn ct =>
    1.33 +fun dynamic_conv ctxt conv = normalized_tfrees ctxt (no_variables_conv ctxt (fn ct =>
    1.34    let
    1.35      val thm1 = preprocess_conv ctxt ctxt ct;
    1.36      val ct' = Thm.rhs_of thm1;
    1.37 @@ -473,7 +491,7 @@
    1.38      Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
    1.39        error ("could not construct evaluation proof:\n"
    1.40        ^ (cat_lines o map (Display.string_of_thm ctxt)) [thm1, thm2, thm3])
    1.41 -  end);
    1.42 +  end));
    1.43  
    1.44  fun dynamic_value ctxt postproc evaluator t =
    1.45    let
    1.46 @@ -493,9 +511,9 @@
    1.47      val pre_conv = preprocess_conv ctxt;
    1.48      val conv' = conv algebra eqngr;
    1.49      val post_conv = postprocess_conv ctxt;
    1.50 -  in fn ctxt' => no_variables_conv ctxt' ((pre_conv ctxt')
    1.51 +  in fn ctxt' => normalized_tfrees ctxt' (no_variables_conv ctxt' ((pre_conv ctxt')
    1.52      then_conv (fn ct => conv' ctxt' (Thm.term_of ct) ct)
    1.53 -    then_conv (post_conv ctxt'))
    1.54 +    then_conv (post_conv ctxt')))
    1.55    end;
    1.56  
    1.57  fun static_value ctxt postproc consts evaluator =