--- a/src/Pure/Tools/class_package.ML Wed Mar 08 10:19:57 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Wed Mar 08 16:29:07 2006 +0100
@@ -35,9 +35,9 @@
val the_superclasses: theory -> class -> class list
val the_consts_sign: theory -> class -> string * (string * typ) list
val lookup_const_class: theory -> string -> class option
- val the_instances: theory -> class -> (string * string) list
+ val the_instances: theory -> class -> (string * ((sort list) * string)) list
val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
- val get_classtab: theory -> (string list * (string * string) list) Symtab.table
+ val get_classtab: theory -> (string * string) list Symtab.table
val print_classes: theory -> unit
val intro_classes_tac: thm list -> tactic
@@ -62,23 +62,25 @@
name_axclass: string,
intro: thm option,
var: string,
- consts: (string * typ) list,
- insts: (string * string) list (* [type constructor ~> theory name] *)
+ consts: (string * typ) list
};
structure ClassData = TheoryDataFun (
struct
val name = "Pure/classes";
- type T = class_data Graph.T * (class Symtab.table * string Symtab.table);
- val empty = (Graph.empty, (Symtab.empty, Symtab.empty));
+ type T = (class_data Graph.T
+ * (string * (sort list * string)) list Symtab.table)
+ (* class ~> tyco ~> (arity, thyname) *)
+ * class Symtab.table;
+ val empty = ((Graph.empty, Symtab.empty), Symtab.empty);
val copy = I;
val extend = I;
- fun merge _ ((t1, (c1, l1)), (t2, (c2, l2)))=
- (Graph.merge (op =) (t1, t2),
- (Symtab.merge (op =) (c1, c2), Symtab.merge (op =) (l1, l2)));
- fun print thy (gr, _) =
+ fun merge _ (((g1, c1), f1), ((g2, c2), f2)) =
+ ((Graph.merge (op =) (g1, g2), Symtab.join (fn _ => AList.merge (op =) (K false)) (c1, c2)),
+ Symtab.merge (op =) (f1, f2));
+ fun print thy ((gr, _), _) =
let
- fun pretty_class gr (name, {name_locale, name_axclass, intro, var, consts, insts}) =
+ fun pretty_class gr (name, {name_locale, name_axclass, intro, var, consts}) =
(Pretty.block o Pretty.fbreaks) [
Pretty.str ("class " ^ name ^ ":"),
(Pretty.block o Pretty.fbreaks) (
@@ -91,10 +93,6 @@
(Pretty.block o Pretty.fbreaks) (
Pretty.str "constants: "
:: map (fn (c, ty) => Pretty.str (c ^ " :: " ^ Sign.string_of_typ thy ty)) consts
- ),
- (Pretty.block o Pretty.fbreaks) (
- Pretty.str "instances: "
- :: map (fn (tyco, thyname) => Pretty.str (tyco ^ ", in theory " ^ thyname)) insts
)
]
in
@@ -110,9 +108,9 @@
(* queries *)
-val lookup_class_data = try o Graph.get_node o fst o ClassData.get;
-val lookup_const_class = Symtab.lookup o fst o snd o ClassData.get;
-val lookup_locale_class = Symtab.lookup o snd o snd o ClassData.get;
+val lookup_class_data = try o Graph.get_node o fst o fst o ClassData.get;
+val the_instances = these oo Symtab.lookup o snd o fst o ClassData.get;
+val lookup_const_class = Symtab.lookup o snd o ClassData.get;
fun the_class_data thy class =
case lookup_class_data thy class
@@ -148,7 +146,7 @@
fun get_superclass_derivation thy (subclass, superclass) =
if subclass = superclass
then SOME [subclass]
- else case Graph.find_paths ((fst o ClassData.get) thy) (subclass, superclass)
+ else case Graph.find_paths ((fst o fst o ClassData.get) thy) (subclass, superclass)
of [] => NONE
| (p::_) => (SOME o filter (is_class thy)) p;
@@ -162,7 +160,7 @@
fun the_intros thy =
let
- val gr = (fst o ClassData.get) thy;
+ val gr = (fst o fst o ClassData.get) thy;
in (List.mapPartial (#intro o Graph.get_node gr) o Graph.keys) gr end;
fun subst_clsvar v ty_subst =
@@ -174,15 +172,11 @@
val data = the_class_data thy class
in (#var data, #consts data) end;
-val the_instances =
- #insts oo the_class_data;
-
fun the_inst_sign thy (class, tyco) =
let
val _ = if is_class thy class then () else error ("no syntactic class: " ^ class);
val arity =
- Sorts.mg_domain (Sign.classes_arities_of thy) tyco [class]
- |> map (operational_sort_of thy);
+ (fst o the o AList.lookup (op =) (the_instances thy class)) tyco
val clsvar = (#var o the_class_data thy) class;
val const_sign = (snd o the_consts_sign thy) class;
fun add_var sort used =
@@ -190,7 +184,7 @@
val v = hd (Term.invent_names used "'a" 1)
in ((v, sort), v::used) end;
val (vsorts, _) =
- []
+ [clsvar]
|> fold (fn (_, ty) => curry (gen_union (op =))
((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign
|> fold_map add_var arity;
@@ -199,43 +193,33 @@
in (vsorts, inst_signs) end;
fun get_classtab thy =
- Graph.fold_nodes
- (fn (class, { consts = consts, insts = insts, ... }) =>
- Symtab.update_new (class, (map fst consts, insts)))
- ((fst o ClassData.get) thy) Symtab.empty;
+ (Symtab.map o map)
+ (fn (tyco, (_, thyname)) => (tyco, thyname)) ((snd o fst o ClassData.get) thy);
(* updaters *)
fun add_class_data (class, (superclasses, name_locale, name_axclass, intro, var, consts)) =
- ClassData.map (fn (classtab, (consttab, loctab)) => (
- classtab
+ ClassData.map (fn ((gr, tab), consttab) => ((
+ gr
|> Graph.new_node (class, {
name_locale = name_locale,
name_axclass = name_axclass,
intro = intro,
var = var,
- consts = consts,
- insts = []
+ consts = consts
})
|> fold (curry Graph.add_edge_acyclic class) superclasses,
- (consttab
- |> fold (fn (c, _) => Symtab.update (c, class)) consts,
- loctab
- |> Symtab.update (name_locale, class))
+ tab
+ |> Symtab.update (class, [])),
+ consttab
+ |> fold (fn (c, _) => Symtab.update (c, class)) consts
));
fun add_inst_data (class, inst) =
- (ClassData.map o apfst o Graph.map_node class)
- (fn {name_locale, name_axclass, intro, var, consts, insts}
- => {
- name_locale = name_locale,
- name_axclass = name_axclass,
- intro = intro,
- var = var,
- consts = consts,
- insts = insts @ [inst]
- });
+ ClassData.map (fn ((gr, tab), consttab) =>
+ ((gr, tab |>
+ (Symtab.map_entry class (AList.update (op =) inst))), consttab));
(* name handling *)
@@ -468,7 +452,7 @@
fun get_classes thy tyco sort =
let
fun get class classes =
- if AList.defined (op =) ((#insts o the_class_data thy) class) tyco
+ if AList.defined (op =) ((the_instances thy) class) tyco
then classes
else classes
|> cons class
@@ -524,7 +508,7 @@
fun after_qed cs thy =
thy
|> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
- |> fold (fn class => add_inst_data (class, (tyco, Context.theory_name thy))) sort;
+ |> fold (fn class => add_inst_data (class, (tyco, (asorts, Context.theory_name thy)))) sort;
in
theory
|> check_defs raw_defs cs
@@ -623,7 +607,16 @@
|> filter (not o null o snd);
datatype classlookup = Instance of (class * string) * classlookup list list
- | Lookup of class list * (string * int)
+ | Lookup of class list * (string * int)
+
+fun pretty_lookup' (Instance ((class, tyco), lss)) =
+ (Pretty.block o Pretty.breaks) (
+ Pretty.enum "," "{" "}" [Pretty.str class, Pretty.str tyco]
+ :: map pretty_lookup lss
+ )
+ | pretty_lookup' (Lookup (classes, (v, i))) =
+ Pretty.enum " <" "[" "]" (map Pretty.str classes @ [Pretty.str (v ^ "!" ^ string_of_int i)])
+and pretty_lookup ls = (Pretty.enum "," "(" ")" o map pretty_lookup') ls;
fun extract_lookup thy sortctxt raw_typ_def raw_typ_use =
let
@@ -646,11 +639,12 @@
) subclasses;
val i' = if length subclasses = 1 then ~1 else i;
in (rev deriv, i') end;
- fun mk_lookup (sort_def, (Type (tycon, tys))) =
- let
- val arity_lookup = map2 (curry mk_lookup)
- (map (operational_sort_of thy) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def)) tys
- in map (fn class => Instance ((class, tycon), arity_lookup)) sort_def end
+ fun mk_lookup (sort_def, (Type (tyco, tys))) =
+ map (fn class => Instance ((class, tyco),
+ map2 (curry mk_lookup)
+ ((fst o the o AList.lookup (op =) (the_instances thy class)) tyco)
+ tys)
+ ) sort_def
| mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
let
fun mk_look class =
@@ -659,15 +653,10 @@
in map mk_look sort_def end;
in
sortctxt
-(* |> print *)
|> map (tab_lookup o fst)
-(* |> print *)
|> map (apfst (operational_sort_of thy))
-(* |> print *)
|> filter (not o null o fst)
-(* |> print *)
|> map mk_lookup
-(* |> print *)
end;
fun extract_classlookup thy (c, raw_typ_use) =
--- a/src/Pure/Tools/codegen_package.ML Wed Mar 08 10:19:57 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Wed Mar 08 16:29:07 2006 +0100
@@ -98,6 +98,7 @@
val nsp_dtcon = "dtcon";
val nsp_mem = "mem";
val nsp_inst = "inst";
+val nsp_instmem = "instmem";
fun add_nsp shallow name =
name
@@ -224,7 +225,7 @@
fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst);
);
-type auxtab = (deftab * string Symtab.table)
+type auxtab = deftab
* (InstNameMangler.T * (typ list Symtab.table * ConstNameMangler.T)
* DatatypeconsNameMangler.T);
type eqextr = theory -> auxtab
@@ -240,14 +241,14 @@
#ml CodegenSerializer.serializers
|> apsnd (fn seri => seri
(nsp_dtcon, nsp_class, K false)
- [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst]]
+ [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
)
)
|> Symtab.update (
#haskell CodegenSerializer.serializers
|> apsnd (fn seri => seri
[nsp_module, nsp_class, nsp_tyco, nsp_dtcon]
- [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]]
+ [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst], [nsp_instmem]]
)
)
);
@@ -402,7 +403,7 @@
val _ = alias_ref := (perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get,
perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get);
-fun idf_of_const thy (tabs as ((deftab, clsmemtab), (_, (overltab1, overltab2), dtcontab)))
+fun idf_of_const thy (tabs as (deftab, (_, (overltab1, overltab2), dtcontab)))
(c, ty) =
let
fun get_overloaded (c, ty) =
@@ -422,7 +423,7 @@
of SOME c' => idf_of_name thy nsp_dtcon c'
| NONE => case get_overloaded (c, ty)
of SOME idf => idf
- | NONE => case Symtab.lookup clsmemtab c
+ | NONE => case ClassPackage.lookup_const_class thy c
of SOME _ => idf_of_name thy nsp_mem c
| NONE => idf_of_name thy nsp_const c
end;
@@ -526,7 +527,7 @@
#ml CodegenSerializer.serializers
|> apsnd (fn seri => seri
(nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco)
- [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
+ [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst, nsp_instmem]]
)
)
); thy);
@@ -694,15 +695,24 @@
trns
|> fold_map (ensure_def_class thy tabs) clss
|-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", i))))
-and mk_fun thy tabs (c, ty) trns =
- case get_first (fn (name, eqx) => (eqx (c, ty))) (get_eqextrs thy tabs)
- of SOME ((eq_thms, default), ty) =>
+and mk_fun thy tabs restrict (c, ty1) trns =
+ case get_first (fn (name, eqx) => (eqx (c, ty1))) (get_eqextrs thy tabs)
+ of SOME ((eq_thms, default), ty2) =>
let
- val sortctxt = ClassPackage.extract_sortctxt thy ty;
+ val ty3 = if restrict then ty1 else ty2;
+ val sortctxt = ClassPackage.extract_sortctxt thy ty3;
+ val instantiate = if restrict
+ then
+ let
+ val tab_lookup = snd o the o Vartab.lookup (Sign.typ_match thy (ty2, ty1) Vartab.empty);
+ in map_term_types (map_atyps (fn (TVar (vi, _)) => tab_lookup vi
+ | ty => ty)) end
+ else I
fun dest_eqthm eq_thm =
let
val ((t, args), rhs) =
- (apfst strip_comb o Logic.dest_equals o prop_of o Drule.zero_var_indexes) eq_thm;
+ (apfst strip_comb o Logic.dest_equals o instantiate
+ o prop_of o Drule.zero_var_indexes) eq_thm;
in case t
of Const (c', _) => if c' = c then (args, rhs)
else error ("illegal function equation for " ^ quote c
@@ -711,7 +721,7 @@
end;
fun mk_default t =
let
- val (tys, ty') = strip_type ty;
+ val (tys, ty') = strip_type ty3;
val vs = Term.invent_names (add_term_names (t, [])) "x" (length tys);
in
if (not o eq_typ thy) (type_of t, ty')
@@ -722,7 +732,7 @@
trns
|> (exprsgen_eqs thy tabs o map dest_eqthm) eq_thms
||>> (exprsgen_eqs thy tabs o the_list o Option.map mk_default) default
- ||>> exprsgen_type thy tabs [ty]
+ ||>> exprsgen_type thy tabs [ty3]
||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
|-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) (eqs @ eq_default, (sortctxt, ty)))
end
@@ -739,12 +749,12 @@
|> ensure_def_class thy tabs supclass
||>> ensure_def_inst thy tabs (supclass, tyco)
||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
- (ClassPackage.extract_classlookup_inst thy (supclass, tyco) supclass)
+ (ClassPackage.extract_classlookup_inst thy (class, tyco) supclass)
|-> (fn ((supclass, inst), lss) => pair (supclass, (inst, lss)));
fun gen_membr (m, ty) trns =
trns
- |> mk_fun thy tabs (m, ty)
- |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, (idf_of_name thy nsp_mem m ^ "'", funn))
+ |> mk_fun thy tabs true (m, ty)
+ |-> (fn SOME funn => pair (idf_of_name thy nsp_mem m, (idf_of_name thy nsp_instmem m, funn))
| NONE => error ("could not derive definition for member " ^ quote m));
in
trns
@@ -760,7 +770,7 @@
end
| _ =>
trns |> fail ("no class instance found for " ^ quote inst);
- val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco;
+ val (_, thyname) = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco;
val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco)));
in
trns
@@ -769,13 +779,13 @@
("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
|> pair inst
end
-and ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns =
+and ensure_def_const thy (tabs as (_, (_, overltab, dtcontab))) (c, ty) trns =
let
fun defgen_funs thy tabs c trns =
case recconst_of_idf thy tabs c
of SOME (c, ty) =>
trns
- |> mk_fun thy tabs (c, ty)
+ |> mk_fun thy tabs false (c, ty)
|-> (fn (SOME funn) => succeed (Fun funn)
| NONE => fail ("no defining equations found for " ^ quote c))
| NONE =>
@@ -897,7 +907,7 @@
(* function extractors *)
-fun eqextr_defs thy ((deftab, _), _) (c, ty) =
+fun eqextr_defs thy (deftab, _) (c, ty) =
Option.mapPartial (get_first (fn (ty', (thm, _)) => if eq_typ thy (ty, ty')
then SOME ([thm], ty')
else NONE
@@ -906,8 +916,8 @@
(* parametrized generators, for instantiation in HOL *)
-fun appgen_split strip_abs thy tabs (app as (c, [t])) trns =
- case strip_abs 1 (Const c $ t)
+fun appgen_split strip_abs thy tabs (app as (c_ty, [t])) trns =
+ case strip_abs 1 (Const c_ty $ t)
of ([vt], bt) =>
trns
|> exprgen_term thy tabs vt
@@ -1054,7 +1064,7 @@
fun mk_insttab thy =
InstNameMangler.empty
|> Symtab.fold_map
- (fn (cls, (clsmems, clsinsts)) => fold_map
+ (fn (cls, clsinsts) => fold_map
(fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts)
(ClassPackage.get_classtab thy)
|-> (fn _ => I);
@@ -1101,18 +1111,11 @@
in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end
) (get_all_datatype_cons thy) [])
|-> (fn _ => I);
- fun mk_clsmemtab thy =
- Symtab.empty
- |> Symtab.fold
- (fn (class, (clsmems, _)) => fold
- (fn clsmem => Symtab.update (clsmem, class)) clsmems)
- (ClassPackage.get_classtab thy);
val deftab = extract_defs thy;
val insttab = mk_insttab thy;
val overltabs = mk_overltabs thy;
val dtcontab = mk_dtcontab thy;
- val clsmemtab = mk_clsmemtab thy;
- in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end;
+ in (deftab, (insttab, overltabs, dtcontab)) end;
fun get_serializer target =
case Symtab.lookup (!serializers) target
--- a/src/Pure/Tools/codegen_serializer.ML Wed Mar 08 10:19:57 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Wed Mar 08 16:29:07 2006 +0100
@@ -397,6 +397,21 @@
val ml_from_label =
str o translate_string (fn "_" => "__" | "." => "_" | c => c)
o NameSpace.base o resolv;
+ fun ml_from_tyvar (v, sort) =
+ let
+ fun mk_class v class =
+ str (prefix "'" v ^ " " ^ resolv class);
+ in
+ Pretty.block [
+ str "(",
+ str v,
+ str ":",
+ case sort
+ of [class] => mk_class v class
+ | _ => Pretty.enum " *" "" "" (map (mk_class v) sort),
+ str ")"
+ ]
+ end;
fun ml_from_sortlookup fxy ls =
let
fun from_label l =
@@ -496,7 +511,7 @@
ml_from_expr NOBR e
]
| ml_from_expr fxy (INum ((n, ty), _)) =
- Pretty.enclose "(" ")" [
+ brackify BR [
(str o IntInf.toString) n,
str ":",
ml_from_type NOBR ty
@@ -557,11 +572,11 @@
:: (lss
@ map (ml_from_expr BR) es)
);
- in (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) end;
+ in (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) end;
fun ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv =
let
- val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
+ val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
fun chunk_defs ps =
let
@@ -571,26 +586,14 @@
end;
fun ml_from_funs (defs as def::defs_tl) =
let
- fun mk_definer [] = "val"
- | mk_definer _ = "fun";
- fun check_args (_, ((pats, _)::_, _)) NONE =
- SOME (mk_definer pats)
- | check_args (_, ((pats, _)::_, _)) (SOME definer) =
- if mk_definer pats = definer
+ fun mk_definer [] [] = "val"
+ | mk_definer _ _ = "fun";
+ fun check_args (_, ((pats, _)::_, (sortctxt, _))) NONE =
+ SOME (mk_definer pats sortctxt)
+ | check_args (_, ((pats, _)::_, (sortctxt, _))) (SOME definer) =
+ if mk_definer pats sortctxt = definer
then SOME definer
- else error ("mixing simultaneous vals and funs not implemented")
- fun mk_class v class =
- str (prefix "'" v ^ " " ^ resolv class)
- fun from_tyvar (v, sort) =
- Pretty.block [
- str "(",
- str v,
- str ":",
- case sort
- of [class] => mk_class v class
- | _ => Pretty.enum " *" "" "" (map (mk_class v) sort),
- str ")"
- ];
+ else error ("mixing simultaneous vals and funs not implemented");
fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) =
let
val shift = if null eq_tl then I else
@@ -601,10 +604,10 @@
fun mk_eq definer (pats, expr) =
(Pretty.block o Pretty.breaks) (
[str definer, (str o resolv) name]
- @ (if null pats
+ @ (if null pats andalso null sortctxt
then [str ":", ml_from_type NOBR ty]
else
- map from_tyvar sortctxt
+ map ml_from_tyvar sortctxt
@ map2 mk_arg pats
((curry Library.take (length pats) o fst o CodegenThingol.unfold_fun) ty))
@ [str "=", ml_from_expr NOBR expr]
@@ -651,7 +654,7 @@
(from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs =
let
val resolv = resolver prefix;
- val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
+ val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
val (ml_from_funs, ml_from_datatypes) =
ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
@@ -735,11 +738,11 @@
:: (str o resolv) supinst
:: map (ml_from_sortlookup NOBR) lss
);
- fun from_memdef (m, (_, def)) =
- (ml_from_funs [(m, def)], (Pretty.block o Pretty.breaks) (
+ fun from_memdef (m, (m', def)) =
+ (ml_from_funs [(m', def)], (Pretty.block o Pretty.breaks) (
ml_from_label m
:: str "="
- :: (str o resolv) m
+ :: (str o resolv) m'
:: map (str o fst) arity
));
fun mk_memdefs supclassexprs [] =
@@ -762,14 +765,15 @@
(Pretty.block o Pretty.breaks) (
str definer
:: (str o resolv) name
- :: map (str o fst) arity
+ :: map ml_from_tyvar arity
),
Pretty.brk 1,
str "=",
Pretty.brk 1,
mk_memdefs (map from_supclass suparities) memdefs
] |> SOME
- end;
+ end
+ | ml_from_def (name, CodegenThingol.Classinstmember) = NONE;
in case defs
of (_, CodegenThingol.Fun _)::_ => (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs
| (_, CodegenThingol.Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
@@ -928,8 +932,12 @@
hs_from_expr NOBR e
])
end
- | hs_from_expr fxy (INum ((n, _), _)) =
- (str o IntInf.toString) n
+ | hs_from_expr fxy (INum ((n, ty), _)) =
+ brackify BR [
+ (str o IntInf.toString) n,
+ str "::",
+ hs_from_type NOBR ty
+ ]
| hs_from_expr fxy (e as IAbs _) =
let
val (es, e) = CodegenThingol.unfold_abs e
@@ -1043,25 +1051,27 @@
in
Pretty.block [
str "class ",
- hs_from_sctxt (map (fn class => (v, [class])) supclasss),
+ hs_from_sctxt [(v, supclasss)],
str (resolv_here name ^ " " ^ v),
str " where",
Pretty.fbrk,
Pretty.chunks (map mk_member membrs)
] |> SOME
end
- | hs_from_def (name, CodegenThingol.Classmember _) =
+ | hs_from_def (_, CodegenThingol.Classmember _) =
NONE
| hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) =
Pretty.block [
str "instance ",
- hs_from_sctxt_tycoexpr (arity, (clsname, map (ITyVar o fst) arity)),
- str " ",
- hs_from_sctxt_tycoexpr (arity, (tyco, map (ITyVar o fst) arity)),
+ hs_from_sctxt arity,
+ str (resolv clsname ^ " "),
+ hs_from_type BR (tyco `%% map (ITyVar o fst) arity),
str " where",
Pretty.fbrk,
Pretty.chunks (map (fn (m, (_, (eqs, ty))) => hs_from_funeqs (m, (eqs, ty))) memdefs)
] |> SOME
+ | hs_from_def (_, CodegenThingol.Classinstmember) =
+ NONE
in
case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs
of [] => NONE
--- a/src/Pure/Tools/codegen_thingol.ML Wed Mar 08 10:19:57 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Wed Mar 08 16:29:07 2006 +0100
@@ -75,7 +75,8 @@
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
* (class * (string * iclasslookup list list)) list)
- * (string * (string * funn)) list;
+ * (string * (string * funn)) list
+ | Classinstmember;
type module;
type transact;
type 'dst transact_fin;
@@ -418,7 +419,8 @@
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
* (class * (string * iclasslookup list list)) list)
- * (string * (string * funn)) list;
+ * (string * (string * funn)) list
+ | Classinstmember;
datatype node = Def of def | Module of node Graph.T;
type module = node Graph.T;
@@ -487,7 +489,9 @@
Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
map Pretty.str o snd) arity),
Pretty.str "))"
- ];
+ ]
+ | pretty_def Classinstmember =
+ Pretty.str "class instance member";
fun pretty_module modl =
let
@@ -802,7 +806,9 @@
(sortctxt', ty'))
then (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
else error ("inconsistent type for member definition " ^ quote m)
- in Classinst (d, map mk_memdef membrs) end;
+ in Classinst (d, map mk_memdef membrs) end
+ | check_prep_def modl Classinstmember =
+ error "attempted to add bare class instance member";
fun postprocess_def (name, Datatype (_, constrs)) =
(check_samemodule (name :: map fst constrs);
@@ -820,6 +826,12 @@
#> add_dep (name, m)
) membrs
)
+ | postprocess_def (name, Classinst (_, memdefs)) =
+ (check_samemodule (name :: map (fst o snd) memdefs);
+ fold (fn (_, (m', _)) =>
+ add_def_incr (m', Classinstmember)
+ ) memdefs
+ )
| postprocess_def _ =
I;