# HG changeset patch # User haftmann # Date 1141831747 -3600 # Node ID ee83040c3c849d6900888bc2bc09dedabea5ad43 # Parent ec53c138277a2a2d8a9c2ddcdd1e08927a2d2e81 first running version of type classes diff -r ec53c138277a -r ee83040c3c84 src/Pure/Tools/class_package.ML --- 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) = diff -r ec53c138277a -r ee83040c3c84 src/Pure/Tools/codegen_package.ML --- 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 diff -r ec53c138277a -r ee83040c3c84 src/Pure/Tools/codegen_serializer.ML --- 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 diff -r ec53c138277a -r ee83040c3c84 src/Pure/Tools/codegen_thingol.ML --- 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;