src/Tools/Code/code_thingol.ML
changeset 34895 19fd499cddff
parent 34891 99b9a6290446
child 35226 b987b803616d
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jan 13 10:18:45 2010 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jan 13 12:20:37 2010 +0100
     1.3 @@ -86,8 +86,6 @@
     1.4      -> ((string * stmt) list * (string * stmt) list
     1.5        * ((string * stmt) list * (string * stmt) list)) list
     1.6  
     1.7 -  val expand_eta: theory -> int -> thm -> thm
     1.8 -  val canonize_thms: theory -> thm list -> thm list
     1.9    val read_const_exprs: theory -> string list -> string list * string list
    1.10    val consts_program: theory -> string list -> string list * (naming * program)
    1.11    val eval_conv: theory
    1.12 @@ -397,60 +395,6 @@
    1.13  end; (* local *)
    1.14  
    1.15  
    1.16 -(** technical transformations of code equations **)
    1.17 -
    1.18 -fun expand_eta thy k thm =
    1.19 -  let
    1.20 -    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
    1.21 -    val (_, args) = strip_comb lhs;
    1.22 -    val l = if k = ~1
    1.23 -      then (length o fst o strip_abs) rhs
    1.24 -      else Int.max (0, k - length args);
    1.25 -    val (raw_vars, _) = Term.strip_abs_eta l rhs;
    1.26 -    val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs [])))
    1.27 -      raw_vars;
    1.28 -    fun expand (v, ty) thm = Drule.fun_cong_rule thm
    1.29 -      (Thm.cterm_of thy (Var ((v, 0), ty)));
    1.30 -  in
    1.31 -    thm
    1.32 -    |> fold expand vars
    1.33 -    |> Conv.fconv_rule Drule.beta_eta_conversion
    1.34 -  end;
    1.35 -
    1.36 -fun same_arity thy thms =
    1.37 -  let
    1.38 -    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
    1.39 -    val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0;
    1.40 -  in map (expand_eta thy k) thms end;
    1.41 -
    1.42 -fun mk_desymbolization pre post mk vs =
    1.43 -  let
    1.44 -    val names = map (pre o fst o fst) vs
    1.45 -      |> map (Name.desymbolize false)
    1.46 -      |> Name.variant_list []
    1.47 -      |> map post;
    1.48 -  in map_filter (fn (((v, i), x), v') =>
    1.49 -    if v = v' andalso i = 0 then NONE
    1.50 -    else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
    1.51 -  end;
    1.52 -
    1.53 -fun desymbolize_tvars thy thms =
    1.54 -  let
    1.55 -    val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
    1.56 -    val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
    1.57 -  in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
    1.58 -
    1.59 -fun desymbolize_vars thy thm =
    1.60 -  let
    1.61 -    val vs = Term.add_vars (Thm.prop_of thm) [];
    1.62 -    val var_subst = mk_desymbolization I I Var vs;
    1.63 -  in Thm.certify_instantiate ([], var_subst) thm end;
    1.64 -
    1.65 -fun canonize_thms thy = map (Thm.transfer thy)
    1.66 -  #> desymbolize_tvars thy
    1.67 -  #> same_arity thy #> map (desymbolize_vars thy);
    1.68 -
    1.69 -
    1.70  (** statements, abstract programs **)
    1.71  
    1.72  type typscheme = (vname * sort) list * itype;
    1.73 @@ -614,8 +558,8 @@
    1.74        #>> (fn class => Classparam (c, class));
    1.75      fun stmt_fun cert =
    1.76        let
    1.77 -        val ((vs, ty), raw_eqns) = Code.dest_cert thy cert;
    1.78 -        val eqns = burrow_fst (canonize_thms thy) (map snd raw_eqns);
    1.79 +        val ((vs, ty), raw_eqns) = Code.equations_thms_cert thy cert;
    1.80 +        val eqns = map snd raw_eqns;
    1.81        in
    1.82          fold_map (translate_tyvar_sort thy algbr eqngr) vs
    1.83          ##>> translate_typ thy algbr eqngr ty