src/Tools/Code/code_thingol.ML
changeset 32353 0ac26087464b
parent 32350 5ef633275b15
child 32358 98c00ee9e786
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Aug 10 12:24:47 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Aug 10 12:24:49 2009 +0200
     1.3 @@ -79,6 +79,7 @@
     1.4    val is_cons: program -> string -> bool
     1.5    val contr_classparam_typs: program -> string -> itype option list
     1.6  
     1.7 +  val clean_thms: theory -> typ -> thm list -> thm list
     1.8    val read_const_exprs: theory -> string list -> string list * string list
     1.9    val consts_program: theory -> string list -> string list * (naming * program)
    1.10    val cached_program: theory -> naming * program
    1.11 @@ -376,6 +377,67 @@
    1.12  end; (* local *)
    1.13  
    1.14  
    1.15 +(** technical transformations of code equations **)
    1.16 +
    1.17 +fun expand_eta thy k thm =
    1.18 +  let
    1.19 +    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
    1.20 +    val (head, args) = strip_comb lhs;
    1.21 +    val l = if k = ~1
    1.22 +      then (length o fst o strip_abs) rhs
    1.23 +      else Int.max (0, k - length args);
    1.24 +    val (raw_vars, _) = Term.strip_abs_eta l rhs;
    1.25 +    val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs [])))
    1.26 +      raw_vars;
    1.27 +    fun expand (v, ty) thm = Drule.fun_cong_rule thm
    1.28 +      (Thm.cterm_of thy (Var ((v, 0), ty)));
    1.29 +  in
    1.30 +    thm
    1.31 +    |> fold expand vars
    1.32 +    |> Conv.fconv_rule Drule.beta_eta_conversion
    1.33 +  end;
    1.34 +
    1.35 +fun same_arity thy thms =
    1.36 +  let
    1.37 +    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
    1.38 +    val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
    1.39 +  in map (expand_eta thy k) thms end;
    1.40 +
    1.41 +fun avoid_value thy ty [thm] =
    1.42 +      if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
    1.43 +      then [thm]
    1.44 +      else [expand_eta thy 1 thm]
    1.45 +  | avoid_value thy _ thms = thms;
    1.46 +
    1.47 +fun mk_desymbolization pre post mk vs =
    1.48 +  let
    1.49 +    val names = map (pre o fst o fst) vs
    1.50 +      |> map (Name.desymbolize false)
    1.51 +      |> Name.variant_list []
    1.52 +      |> map post;
    1.53 +  in map_filter (fn (((v, i), x), v') =>
    1.54 +    if v = v' andalso i = 0 then NONE
    1.55 +    else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
    1.56 +  end;
    1.57 +
    1.58 +fun desymbolize_tvars thy thms =
    1.59 +  let
    1.60 +    val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
    1.61 +    val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
    1.62 +  in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
    1.63 +
    1.64 +fun desymbolize_vars thy thm =
    1.65 +  let
    1.66 +    val vs = Term.add_vars (Thm.prop_of thm) [];
    1.67 +    val var_subst = mk_desymbolization I I Var vs;
    1.68 +  in Thm.certify_instantiate ([], var_subst) thm end;
    1.69 +
    1.70 +fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy);
    1.71 +
    1.72 +fun clean_thms thy ty =
    1.73 +  same_arity thy #> avoid_value thy ty #> desymbolize_all_vars thy;
    1.74 +
    1.75 +
    1.76  (** statements, abstract programs **)
    1.77  
    1.78  type typscheme = (vname * sort) list * itype;
    1.79 @@ -498,17 +560,11 @@
    1.80      fun stmt_classparam class =
    1.81        ensure_class thy algbr funcgr class
    1.82        #>> (fn class => Classparam (c, class));
    1.83 -    fun stmt_fun ((vs, ty), raw_eqns) =
    1.84 -      let
    1.85 -        val eqns = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
    1.86 -          then raw_eqns
    1.87 -          else (map o apfst) (Code.expand_eta thy 1) raw_eqns;
    1.88 -      in
    1.89 -        fold_map (translate_tyvar_sort thy algbr funcgr) vs
    1.90 -        ##>> translate_typ thy algbr funcgr ty
    1.91 -        ##>> translate_eqns thy algbr funcgr eqns
    1.92 -        #>> (fn info => Fun (c, info))
    1.93 -      end;
    1.94 +    fun stmt_fun ((vs, ty), eqns) =
    1.95 +      fold_map (translate_tyvar_sort thy algbr funcgr) vs
    1.96 +      ##>> translate_typ thy algbr funcgr ty
    1.97 +      ##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy ty) eqns)
    1.98 +      #>> (fn info => Fun (c, info));
    1.99      val stmt_const = case Code.get_datatype_of_constr thy c
   1.100       of SOME tyco => stmt_datatypecons tyco
   1.101        | NONE => (case AxClass.class_of_param thy c
   1.102 @@ -597,9 +653,6 @@
   1.103              translate_term thy algbr funcgr thm t'
   1.104              ##>> fold_map (translate_term thy algbr funcgr thm) ts
   1.105              #>> (fn (t, ts) => t `$$ ts)
   1.106 -and translate_eqns thy algbr funcgr eqns =
   1.107 -  fold_map (translate_eqn thy algbr funcgr)
   1.108 -    (burrow_fst (Code.desymbolize_all_vars thy) eqns)
   1.109  and translate_eqn thy algbr funcgr (thm, proper) =
   1.110    let
   1.111      val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals