src/Tools/Code/code_preproc.ML
changeset 31957 a9742afd403e
parent 31775 2b04504fcb69
child 31962 baa8dce5bc45
     1.1 --- a/src/Tools/Code/code_preproc.ML	Tue Jul 07 17:21:26 2009 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Jul 07 17:21:27 2009 +0200
     1.3 @@ -102,6 +102,15 @@
     1.4  
     1.5  fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
     1.6  
     1.7 +fun eqn_conv conv =
     1.8 +  let
     1.9 +    fun lhs_conv ct = if can Thm.dest_comb ct
    1.10 +      then Conv.combination_conv lhs_conv conv ct
    1.11 +      else Conv.all_conv ct;
    1.12 +  in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end;
    1.13 +
    1.14 +val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite;
    1.15 +
    1.16  fun term_of_conv thy f =
    1.17    Thm.cterm_of thy
    1.18    #> f
    1.19 @@ -117,7 +126,7 @@
    1.20    in
    1.21      eqns
    1.22      |> apply_functrans thy c functrans
    1.23 -    |> (map o apfst) (Code.rewrite_eqn pre)
    1.24 +    |> (map o apfst) (rewrite_eqn pre)
    1.25      |> (map o apfst) (AxClass.unoverload thy)
    1.26      |> map (Code.assert_eqn thy)
    1.27      |> burrow_fst (Code.norm_args thy)
    1.28 @@ -213,9 +222,19 @@
    1.29    (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
    1.30      (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
    1.31  
    1.32 +fun default_typscheme_of thy c =
    1.33 +  let
    1.34 +    val ty = (snd o dest_Const o TermSubst.zero_var_indexes o curry Const c
    1.35 +      o Type.strip_sorts o Sign.the_const_type thy) c;
    1.36 +  in case AxClass.class_of_param thy c
    1.37 +   of SOME class => ([(Name.aT, [class])], ty)
    1.38 +    | NONE => Code.typscheme thy (c, ty)
    1.39 +  end;
    1.40 +
    1.41  fun tyscm_rhss_of thy c eqns =
    1.42    let
    1.43 -    val tyscm = case eqns of [] => Code.default_typscheme thy c
    1.44 +    val tyscm = case eqns
    1.45 +     of [] => default_typscheme_of thy c
    1.46        | ((thm, _) :: _) => Code.typscheme_eqn thy thm;
    1.47      val rhss = consts_of thy eqns;
    1.48    in (tyscm, rhss) end;
    1.49 @@ -381,6 +400,17 @@
    1.50         handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
    1.51    end;
    1.52  
    1.53 +fun inst_thm thy tvars' thm =
    1.54 +  let
    1.55 +    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
    1.56 +    val inter_sort = Sorts.inter_sort (Sign.classes_of thy);
    1.57 +    fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v
    1.58 +     of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar)
    1.59 +          (tvar, (v, inter_sort (sort, sort'))))
    1.60 +      | NONE => NONE;
    1.61 +    val insts = map_filter mk_inst tvars;
    1.62 +  in Thm.instantiate (insts, []) thm end;
    1.63 +
    1.64  fun add_arity thy vardeps (class, tyco) =
    1.65    AList.default (op =)
    1.66      ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
    1.67 @@ -394,7 +424,7 @@
    1.68      val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
    1.69        Vartab.update ((v, 0), sort)) lhs;
    1.70      val eqns = proto_eqns
    1.71 -      |> (map o apfst) (Code.inst_thm thy inst_tab);
    1.72 +      |> (map o apfst) (inst_thm thy inst_tab);
    1.73      val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
    1.74      val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
    1.75    in (map (pair c) rhss' @ rhss, eqngr') end;