optimization for trivial cases
authorhaftmann
Thu May 15 16:38:30 2014 +0200 (2014-05-15)
changeset 56971f4942eb3bb03
parent 56970 a3f911785efa
child 56972 f64730f667b9
optimization for trivial cases
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:29 2014 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:30 2014 +0200
     1.3 @@ -156,7 +156,9 @@
     1.4      val normalization =
     1.5        map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), TFree (v, sort))) vs_original vs_normalized;
     1.6    in
     1.7 -    (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global, cert (map_types normalize t))
     1.8 +    if eq_list (eq_fst (op =)) (vs_normalized, vs_original)
     1.9 +    then (I, ct)
    1.10 +    else (Thm.certify_instantiate (normalization, []) o Thm.varifyT_global, cert (map_types normalize t))
    1.11    end;
    1.12  
    1.13  fun no_variables_sandwich ctxt ct =
    1.14 @@ -169,7 +171,11 @@
    1.15      fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
    1.16        |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
    1.17        |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
    1.18 -  in (fold apply_beta all_vars, fold_rev Thm.lambda all_vars ct) end;
    1.19 +  in
    1.20 +    if null all_vars
    1.21 +    then (I, ct)
    1.22 +    else (fold apply_beta all_vars, fold_rev Thm.lambda all_vars ct)
    1.23 +  end;
    1.24  
    1.25  fun simplifier_conv_sandwich ctxt =
    1.26    let