src/Pure/Isar/code.ML
changeset 32873 333945c9ac6a
parent 32872 019201eb7e07
child 32928 6bcc35f7ff6d
     1.1 --- a/src/Pure/Isar/code.ML	Mon Oct 05 08:36:33 2009 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Mon Oct 05 15:04:45 2009 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4    val read_const: theory -> string -> string
     1.5    val string_of_const: theory -> string -> string
     1.6    val args_number: theory -> string -> int
     1.7 -  val typscheme: theory -> string * typ -> (string * sort) list * typ
     1.8  
     1.9    (*constructor sets*)
    1.10    val constrset_of_consts: theory -> (string * typ) list
    1.11 @@ -28,8 +27,7 @@
    1.12      -> (thm * bool) list -> (thm * bool) list
    1.13    val const_typ_eqn: theory -> thm -> string * typ
    1.14    val typscheme_eqn: theory -> thm -> (string * sort) list * typ
    1.15 -  val typscheme_rhss_eqns: theory -> string -> thm list
    1.16 -    -> ((string * sort) list * typ) * (string * typ list) list
    1.17 +  val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ
    1.18  
    1.19    (*executable code*)
    1.20    val add_datatype: (string * typ) list -> theory -> theory
    1.21 @@ -114,19 +112,6 @@
    1.22  
    1.23  fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
    1.24  
    1.25 -fun typscheme thy (c, ty) =
    1.26 -  let
    1.27 -    val ty' = Logic.unvarifyT ty;
    1.28 -  in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end;
    1.29 -
    1.30 -fun default_typscheme thy c =
    1.31 -  let
    1.32 -    val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
    1.33 -      o Type.strip_sorts o Sign.the_const_type thy) c;
    1.34 -  in case AxClass.class_of_param thy c
    1.35 -   of SOME class => ([(Name.aT, [class])], ty)
    1.36 -    | NONE => typscheme thy (c, ty)
    1.37 -  end;
    1.38  
    1.39  
    1.40  (** data store **)
    1.41 @@ -522,18 +507,22 @@
    1.42      val (c, ty) = head_eqn thm;
    1.43      val c' = AxClass.unoverload_const thy (c, ty);
    1.44    in (c', ty) end;
    1.45 -
    1.46 -fun typscheme_eqn thy = typscheme thy o const_typ_eqn thy;
    1.47  fun const_eqn thy = fst o const_typ_eqn thy;
    1.48  
    1.49 -fun consts_of thy thms = [] |> (fold o fold o fold_aterms)
    1.50 -  (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
    1.51 -    (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of) thms);
    1.52 -
    1.53 -fun typscheme_rhss_eqns thy c [] =
    1.54 -      (default_typscheme thy c, [])
    1.55 -  | typscheme_rhss_eqns thy c (thms as thm :: _) =
    1.56 -      (typscheme_eqn thy thm, consts_of thy thms);
    1.57 +fun typscheme thy (c, ty) =
    1.58 +  (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
    1.59 +fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy;
    1.60 +fun typscheme_eqns thy c [] = 
    1.61 +      let
    1.62 +        val raw_ty = Sign.the_const_type thy c;
    1.63 +        val tvars = Term.add_tvar_namesT raw_ty [];
    1.64 +        val tvars' = case AxClass.class_of_param thy c
    1.65 +         of SOME class => [TFree (Name.aT, [class])]
    1.66 +          | NONE => Name.invent_list [] Name.aT (length tvars)
    1.67 +              |> map (fn v => TFree (v, []));
    1.68 +        val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
    1.69 +      in typscheme thy (c, ty) end
    1.70 +  | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm;
    1.71  
    1.72  fun assert_eqns_const thy c eqns =
    1.73    let
    1.74 @@ -549,7 +538,7 @@
    1.75      fun inter_sorts vs =
    1.76        fold (curry (Sorts.inter_sort (Sign.classes_of thy)) o snd) vs [];
    1.77      val sorts = map_transpose inter_sorts vss;
    1.78 -    val vts = Name.names Name.context "'X" sorts
    1.79 +    val vts = Name.names Name.context Name.aT sorts
    1.80        |> map (fn (v, sort) => TVar ((v, 0), sort));
    1.81    in map2 (fn vs => Thm.certify_instantiate (vs ~~ vts, [])) vss thms end;
    1.82