--- a/src/Pure/Tools/class_package.ML Tue Dec 27 15:24:23 2005 +0100
+++ b/src/Pure/Tools/class_package.ML Tue Dec 27 15:24:40 2005 +0100
@@ -7,7 +7,11 @@
signature CLASS_PACKAGE =
sig
- val add_classentry: class -> string list -> string list -> theory -> theory
+ val add_class: bstring -> Locale.expr -> Element.context list -> theory
+ -> ProofContext.context * theory
+ val add_class_i: bstring -> Locale.expr -> Element.context_i list -> theory
+ -> ProofContext.context * theory
+ val add_classentry: class -> xstring list -> xstring list -> theory -> theory
val the_consts: theory -> class -> string list
val the_tycos: theory -> class -> (string * string) list
@@ -65,6 +69,8 @@
ClassesData.map (apfst (Symtab.update (class, data)));
fun add_const class const =
ClassesData.map (apsnd (Symtab.update (const, class)));
+val the_consts = #consts oo get_class_data;
+val the_tycos = #tycos oo get_class_data;
(* name mangling *)
@@ -76,67 +82,91 @@
#axclass_name (get_class_data thy class);
-(* assign consts to type classes *)
+(* classes *)
local
-fun gen_add_consts prep_class prep_const (raw_class, raw_consts_new) thy =
+open Element
+
+fun gen_add_class add_locale bname raw_import raw_body thy =
let
- val class = prep_class thy raw_class;
- val consts_new = map (prep_const thy) raw_consts_new;
- val {locale_name, axclass_name, consts, tycos} =
- get_class_data thy class;
+ fun extract_notes_consts thy elems =
+ elems
+ |> List.mapPartial
+ (fn (Notes notes) => SOME notes
+ | _ => NONE)
+ |> Library.flat
+ |> map (fn (_, facts) => map fst facts)
+ |> Library.flat o Library.flat
+ |> map prop_of
+ |> (fn ts => fold (curry add_term_consts) ts [])
+ |> tap (writeln o commas);
+ fun extract_tyvar_name thy tys =
+ fold (curry add_typ_tfrees) tys []
+ |> (fn [(v, [])] => v
+ | [(v, sort)] =>
+ if Sorts.sort_eq (Sign.classes_of thy) (Sign.defaultS thy, sort)
+ then v
+ else error ("sort constraint on class type variable: " ^ Sign.string_of_sort thy sort)
+ | [] => error ("no class type variable")
+ | vs => error ("more than one type variable: " ^ (commas o map (Sign.string_of_typ thy o TFree)) vs))
+ fun extract_tyvar_consts thy elems =
+ elems
+ |> List.mapPartial
+ (fn (Fixes consts) => SOME consts
+ | _ => NONE)
+ |> Library.flat
+ |> map (fn (c, ty, syn) => ((c, the ty), the syn))
+ |> `(fn consts => extract_tyvar_name thy (map (snd o fst) consts));
+ (* fun remove_local_syntax ((c, ty), _) thy =
+ thy
+ |> Sign.add_syntax_i [(c, ty, Syntax.NoSyn)]; *)
+ fun add_global_const ((c, ty), syn) thy =
+ thy
+ |> Sign.add_consts_i [(c, ty, syn)]
+ |> `(fn thy => Sign.intern_const thy c)
+ fun add_axclass bname_axiom locale_pred cs thy =
+ thy
+ |> AxClass.add_axclass_i (bname, Sign.defaultS thy)
+ [Thm.no_attributes (bname_axiom,
+ Const (ObjectLogic.judgment_name thy, dummyT) $
+ list_comb (Const (locale_pred, dummyT), map (fn c => Const (c, dummyT)) cs)
+ |> curry (inferT_axm thy) "locale_pred" |> snd)]
+ |-> (fn _ => `(fn thy => Sign.intern_class thy bname))
+ fun print_ctxt ctxt elem =
+ map Pretty.writeln (Element.pretty_ctxt ctxt elem)
in
thy
- |> put_class_data class {
- locale_name = locale_name,
- axclass_name = axclass_name,
- consts = consts @ consts_new,
- tycos = tycos
- }
- |> fold (add_const class) consts_new
+ |> add_locale bname raw_import raw_body
+ |-> (fn (elems : context_i list, ctxt) =>
+ tap (fn _ => map (print_ctxt ctxt) elems)
+ #> tap (fn thy => extract_notes_consts thy elems)
+ #> `(fn thy => Locale.intern thy bname)
+ #-> (fn name_locale =>
+ `(fn thy => extract_tyvar_consts thy elems)
+ #-> (fn (v, consts) =>
+ fold_map add_global_const consts
+ #-> (fn cs =>
+ add_axclass (bname ^ "_intro") name_locale cs
+ #-> (fn name_axclass =>
+ put_class_data name_locale {
+ locale_name = name_locale,
+ axclass_name = name_axclass,
+ consts = cs,
+ tycos = []
+ })
+ #> fold (add_const name_locale) cs
+ #> pair ctxt
+ ))))
end;
in
-val add_consts = gen_add_consts Sign.intern_class Sign.intern_const;
-val add_consts_i = gen_add_consts (K I) (K I);
+val add_class = gen_add_class (Locale.add_locale_context true);
+val add_class_i = gen_add_class (Locale.add_locale_context_i true);
end; (* local *)
-val the_consts = #consts oo get_class_data;
-
-
-(* assign type constructors to type classes *)
-
-local
-
-fun gen_add_tycos prep_class prep_type (raw_class, raw_tycos_new) thy =
- let
- val class = prep_class thy raw_class
- val tycos_new = map (prep_type thy) raw_tycos_new
- val {locale_name, axclass_name, consts, tycos} =
- get_class_data thy class
- in
- thy
- |> put_class_data class {
- locale_name = locale_name,
- axclass_name = axclass_name,
- consts = consts,
- tycos = tycos @ tycos_new
- }
- end;
-
-in
-
-fun add_tycos xs thy =
- gen_add_tycos Sign.intern_class (rpair (Context.theory_name thy) oo Sign.intern_type) xs thy;
-val add_tycos_i = gen_add_tycos (K I) (K I);
-
-end; (* local *)
-
-val the_tycos = #tycos oo get_class_data;
-
(* class queries *)
@@ -156,12 +186,16 @@
end;
fun get_arities thy sort tycon =
- Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort
+ Sorts.mg_domain (Sign.classes_arities_of thy) tycon (syntactic_sort_of thy sort)
|> map (syntactic_sort_of thy);
fun get_superclasses thy class =
- Sorts.superclasses (Sign.classes_of thy) class
- |> syntactic_sort_of thy;
+ if is_class thy class
+ then
+ Sorts.superclasses (Sign.classes_of thy) class
+ |> syntactic_sort_of thy
+ else
+ error ("no syntactic class: " ^ class);
(* instance queries *)
@@ -227,7 +261,8 @@
) subclasses;
fun mk_class_deriv thy subclasses superclass =
case get_superclass_derivation (subclasses, superclass)
- of (subclass::deriv) => ((rev o filter (is_class thy)) deriv, find_index_eq subclass subclasses);
+ of (subclass::deriv) =>
+ ((rev o filter (is_class thy)) deriv, find_index_eq subclass subclasses);
fun mk_lookup (sort_def, (Type (tycon, tys))) =
let
val arity_lookup = map2 (curry mk_lookup)
@@ -236,7 +271,7 @@
| mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
let
fun mk_look class =
- let val (deriv, classindex) = mk_class_deriv thy sort_use class
+ let val (deriv, classindex) = mk_class_deriv thy (syntactic_sort_of thy sort_use) class
in Lookup (deriv, (vname, classindex)) end;
in map mk_look sort_def end;
in
@@ -250,21 +285,49 @@
(* intermediate auxiliary *)
-fun add_classentry raw_class raw_consts raw_tycos thy =
+fun add_classentry raw_class raw_cs raw_tycos thy =
let
val class = Sign.intern_class thy raw_class;
+ val cs = map (Sign.intern_const thy) raw_cs;
+ val tycos = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_tycos;
in
thy
|> put_class_data class {
locale_name = "",
axclass_name = class,
- consts = [],
- tycos = []
+ consts = cs,
+ tycos = tycos
}
- |> add_consts (class, raw_consts)
- |> add_tycos (class, raw_tycos)
+ |> fold (add_const class) cs
end;
-
+
+
+(* toplevel interface *)
+
+local
+
+structure P = OuterParse
+and K = OuterKeyword
+
+in
+
+val classK = "class_class"
+
+val locale_val =
+ (P.locale_expr --
+ Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] ||
+ Scan.repeat1 P.context_element >> pair Locale.empty);
+
+val classP =
+ OuterSyntax.command classK "operational type classes" K.thy_decl
+ (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
+ >> (Toplevel.theory_context
+ o (fn f => swap o f) o (fn (name, (expr, elems)) => add_class name expr elems)));
+
+val _ = OuterSyntax.add_parsers [classP];
+
+end; (* local *)
+
(* setup *)
--- a/src/Pure/Tools/codegen_package.ML Tue Dec 27 15:24:23 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML Tue Dec 27 15:24:40 2005 +0100
@@ -63,12 +63,16 @@
val print_codegen_generated: theory -> unit;
val rename_inconsistent: theory -> theory;
+
+ (*debugging purpose only*)
structure InstNameMangler: NAME_MANGLER;
structure ConstNameMangler: NAME_MANGLER;
structure DatatypeconsNameMangler: NAME_MANGLER;
structure CodegenData: THEORY_DATA;
val mk_tabs: theory -> auxtab;
val alias_get: theory -> string -> string;
+ val idf_of_name: theory -> string -> string -> string;
+ val idf_of_const: theory -> auxtab -> string * typ -> string;
end;
structure CodegenPackage : CODEGEN_PACKAGE =
@@ -590,18 +594,27 @@
fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) (c, ty) =
let
- val coty = case (snd o strip_type) ty
- of Type (tyco, _) => tyco
- | _ => "";
- val c' = case Symtab.lookup overltab1 c
- of SOME (ty_decl, tys) => ConstNameMangler.get thy overltab2
- (idf_of_name thy nsp_overl c, (ty_decl, (the oo find_first) (fn ty' => Sign.typ_instance thy (ty', ty)) tys))
- | NONE => case try (DatatypeconsNameMangler.get thy dtcontab) (c, coty)
- of SOME c' => idf_of_name thy nsp_dtcon c'
- | NONE => case Symtab.lookup clsmemtab c
- of SOME _ => idf_of_name thy nsp_mem c
- | NONE => idf_of_name thy nsp_const c;
- in c' end;
+ fun get_overloaded (c, ty) =
+ case Symtab.lookup overltab1 c
+ of SOME (ty_decl, tys) =>
+ (case find_first (curry (Sign.typ_instance thy) ty) tys
+ of SOME ty' => ConstNameMangler.get thy overltab2
+ (idf_of_name thy nsp_overl c, (ty_decl, ty')) |> SOME
+ | _ => NONE)
+ | _ => NONE
+ fun get_datatypecons (c, ty) =
+ case (snd o strip_type) ty
+ of Type (tyco, _) =>
+ try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco)
+ | _ => NONE;
+ in case get_overloaded (c, ty)
+ of SOME idf => idf
+ | NONE => case get_datatypecons (c, ty)
+ of SOME c' => idf_of_name thy nsp_dtcon c'
+ | NONE => case Symtab.lookup clsmemtab c
+ of SOME _ => idf_of_name thy nsp_mem c
+ | NONE => idf_of_name thy nsp_const c
+ end;
fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf =
case name_of_idf thy nsp_const idf
@@ -637,13 +650,14 @@
val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco;
val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco;
val idf_eqpred = idf_of_name thy nsp_eq_pred name_dtco;
+ val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity;
fun mk_eq_pred _ trns =
trns
|> succeed (eqpred, [])
fun mk_eq_inst _ trns =
trns
|> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred
- |> succeed (Classinst (class_eq, (dtco, arity), [(fun_eq, idf_eqpred)]), []);
+ |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))])), []);
in
trns
|> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst
@@ -757,31 +771,33 @@
(* application generators *)
+fun mk_lookup thy tabs (ClassPackage.Instance (inst as (cls, tyco), ls)) trns =
+ trns
+ |> ensure_def_class thy tabs cls
+ ||>> ensure_def_inst thy tabs inst
+ ||>> (fold_map o fold_map) (mk_lookup thy tabs) ls
+ |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls)))
+ | mk_lookup thy tabs (ClassPackage.Lookup (clss, (v, i))) trns =
+ trns
+ |> fold_map (ensure_def_class thy tabs) clss
+ |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i))));
+
+fun mk_itapp e [] = e
+ | mk_itapp e lookup = IInst (e, lookup);
+
fun appgen_default thy tabs ((f, ty), ts) trns =
let
val _ = debug 5 (fn _ => "making application of " ^ quote f) ();
val ty_def = Sign.the_const_constraint thy f;
- fun mk_lookup (ClassPackage.Instance (inst as (cls, tyco), ls)) trns =
- trns
- |> ensure_def_class thy tabs cls
- ||>> ensure_def_inst thy tabs inst
- ||>> (fold_map o fold_map) mk_lookup ls
- |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls)))
- | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns =
- trns
- |> fold_map (ensure_def_class thy tabs) clss
- |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i))));
- fun mk_itapp e [] = e
- | mk_itapp e lookup = IInst (e, lookup);
in
trns
|> ensure_def_const thy tabs (f, ty)
- ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty))
+ ||>> (fold_map o fold_map) (mk_lookup thy tabs) (ClassPackage.extract_sortlookup thy (ty_def, ty))
||>> invoke_cg_type thy tabs ty
||>> fold_map (invoke_cg_expr thy tabs) ts
|-> (fn (((f, lookup), ty), es) =>
succeed (mk_itapp (IConst (f, ty)) lookup `$$ es))
- end
+ end;
fun appgen_neg thy tabs (f as ("neg", Type ("fun", [ty, _])), ts) trns =
let
@@ -887,26 +903,46 @@
val arity = ClassPackage.get_arities thy [cls] tyco;
val ms = map (fn m => (m, Sign.the_const_constraint thy m)) (ClassPackage.the_consts thy cls);
val instmem_idfs = ClassPackage.get_inst_consts_sign thy (tyco, cls);
+ val supclss = ClassPackage.get_superclasses thy cls;
fun add_vars arity clsmems (trns as (_, modl)) =
case get_def modl (idf_of_name thy nsp_class cls)
of Class (_, _, members, _) => ((Term.invent_names
(tvars_of_itypes ((map (snd o snd)) members)) "a" (length arity) ~~ arity, clsmems), trns)
+ val ad_hoc_arity = map (fn (v, sort) => map_index (fn (i, _) => (ClassPackage.Lookup ([], (v, i)))) sort);
+ (*! THIS IS ACTUALLY VERY AD-HOC... !*)
in
- trns
+ (trns
|> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
|> (fold_map o fold_map) (ensure_def_class thy tabs) arity
||>> fold_map (ensure_def_const thy tabs) ms
|-> (fn (arity, ms) => add_vars arity ms)
||>> ensure_def_class thy tabs cls
||>> ensure_def_tyco thy tabs tyco
- ||>> fold_map (ensure_def_const thy tabs) instmem_idfs
- |-> (fn ((((arity, ms), cls), tyco), instmem_idfs) =>
- succeed (Classinst (cls, (tyco, arity), ms ~~ instmem_idfs), []))
+ ||>> fold_map (fn supcls => ensure_def_inst thy tabs (supcls, tyco)) supclss
+ ||>> fold_map (fn supcls => (fold_map o fold_map) (mk_lookup thy tabs)
+ (ClassPackage.extract_sortlookup thy
+ (Type (tyco, map_index (fn (i, _) => TVar (("'a", i), [])) (ClassPackage.get_arities thy [supcls] tyco)),
+ Type (tyco, map_index (fn (i, sort) => TFree (string_of_int i, sort)) arity)))) supclss
+ ||>> fold_map (ensure_def_const thy tabs) instmem_idfs)
+ |-> (fn ((((((arity, ms), cls), tyco), supinsts), supinstlookup), instmem_idfs)
+ : ((((((string * string list) list * string list) * string) * string)
+ * string list) * ClassPackage.sortlookup list list list) * string list
+ =>
+ succeed (Classinst ((cls, (tyco, arity)), (supclss ~~ (supinsts ~~ supinstlookup), ms ~~ map (rpair (ad_hoc_arity arity)) instmem_idfs)), []))
end
| _ =>
trns |> fail ("no class instance found for " ^ quote inst);
+(* trns
+ |> ensure_def_const thy tabs (f, ty)
+
+ ||>> invoke_cg_type thy tabs ty
+ ||>> fold_map (invoke_cg_expr thy tabs) ts
+ |-> (fn (((f, lookup), ty), es) =>
+ succeed (mk_itapp (IConst (f, ty)) lookup `$$ es))*)
+
+
(* parametrized generators, for instantiation in HOL *)
fun appgen_let strip_abs thy tabs (f as ("Let", _), ts) trns =
--- a/src/Pure/Tools/codegen_serializer.ML Tue Dec 27 15:24:23 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Dec 27 15:24:40 2005 +0100
@@ -143,15 +143,27 @@
local
-fun ml_from_defs tyco_syntax const_syntax is_dicttype resolv ds =
+fun ml_from_defs tyco_syntax const_syntax is_dicttyco resolv ds =
let
+ fun is_dicttype (IType (tyco, _)) =
+ is_dicttyco tyco
+ | is_dicttype (IDictT _) =
+ true
+ | is_dicttype _ =
+ false;
fun chunk_defs ps =
let
val (p_init, p_last) = split_last ps
in
Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])])
end;
- val ml_label_uniq = translate_string (fn "_" => "__" | "." => "_" | c => c);
+ fun ml_from_label s =
+ let
+ val s' = NameSpace.unpack s;
+ in
+ NameSpace.pack (Library.drop (length s' - 2, s'))
+ |> translate_string (fn "_" => "__" | "." => "_" | c => c)
+ end;
fun ml_from_type br (IType ("Pair", [t1, t2])) =
brackify (eval_br_postfix br (INFX (2, L))) [
ml_from_type (INFX (2, X)) t1,
@@ -191,7 +203,7 @@
| ml_from_type _ (IDictT fs) =
Pretty.gen_list "," "{" "}" (
map (fn (f, ty) =>
- Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_type NOBR ty]) fs
+ Pretty.block [Pretty.str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs
);
fun ml_from_pat br (ICons (("True", []), _)) =
Pretty.str "true"
@@ -239,8 +251,16 @@
Pretty.str ":",
Pretty.str "IntInf.int"
]
- | ml_from_pat br (IVarP (v, _)) =
- Pretty.str v
+ | ml_from_pat br (IVarP (v, ty)) =
+ if is_dicttype ty
+ then
+ brackify (eval_br br BR) [
+ Pretty.str v,
+ Pretty.str ":",
+ ml_from_type NOBR ty
+ ]
+ else
+ Pretty.str v
and ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) =
let
fun dest_cons (IApp (IConst ("Cons", _),
@@ -313,19 +333,19 @@
| ml_from_expr br (IDictE fs) =
Pretty.gen_list "," "{" "}" (
map (fn (f, e) =>
- Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_expr NOBR e]) fs
+ Pretty.block [Pretty.str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs
)
| ml_from_expr br (ILookup ([], v)) =
Pretty.str v
| ml_from_expr br (ILookup ([l], v)) =
brackify (eval_br br BR) [
- Pretty.str ("#" ^ (ml_label_uniq l)),
+ Pretty.str ("#" ^ (ml_from_label l)),
Pretty.str v
]
| ml_from_expr br (ILookup (ls, v)) =
brackify (eval_br br BR) [
Pretty.str ("("
- ^ (ls |> map ((fn s => "#" ^ s) o ml_label_uniq) |> foldr1 (fn (l, e) => l ^ " o " ^ e))
+ ^ (ls |> map ((fn s => "#" ^ s) o ml_from_label) |> foldr1 (fn (l, e) => l ^ " o " ^ e))
^ ")"),
Pretty.str v
]
@@ -422,23 +442,10 @@
val definer = the (fold check_args ds NONE);
fun mk_eq definer f ty (pats, expr) =
let
- fun mk_pat_arg p =
- case itype_of_ipat p
- of ty as IType (tyco, _) =>
- if is_dicttype tyco
- then Pretty.block [
- Pretty.str "(",
- ml_from_pat NOBR p,
- Pretty.str ":",
- ml_from_type NOBR ty,
- Pretty.str ")"
- ]
- else ml_from_pat BR p
- | _ => ml_from_pat BR p;
val lhs = [Pretty.str (definer ^ " " ^ f)]
@ (if null pats
then [Pretty.str ":", ml_from_type NOBR ty]
- else map mk_pat_arg pats)
+ else map (ml_from_pat BR) pats)
val rhs = [Pretty.str "=", ml_from_expr NOBR expr]
in
Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
@@ -551,9 +558,10 @@
Pretty.str "",
Pretty.str ("end; (* struct " ^ name ^ " *)")
]);
- fun is_dicttype tyco =
+ fun is_dicttyco module tyco =
NameSpace.is_qualified tyco andalso case get_def module tyco
of Typesyn (_, IDictT _) => true
+ | Typesyn _ => false
| _ => false;
fun eta_expander "Pair" = 2
| eta_expander "Cons" = 2
@@ -590,7 +598,8 @@
|> debug 3 (fn _ => "eliminating classes...")
|> eliminate_classes
|> debug 3 (fn _ => "serializing...")
- |> serialize (ml_from_defs tyco_syntax const_syntax is_dicttype) ml_from_module ml_validator nspgrp name_root
+ |> `(is_dicttyco)
+ |-> (fn is_dicttyco => serialize (ml_from_defs tyco_syntax const_syntax is_dicttyco) ml_from_module ml_validator nspgrp name_root)
|> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
end;
@@ -952,7 +961,7 @@
end
| haskell_from_def (name, Classmember _) =
NONE
- | haskell_from_def (_, Classinst ("Eq", (tyco, arity), [(_, eqpred)])) =
+ | haskell_from_def (_, Classinst (("Eq", (tyco, arity)), (_, [(_, (eqpred, _))]))) =
Pretty.block [
Pretty.str "instance ",
haskell_from_sctxt arity,
@@ -963,7 +972,7 @@
Pretty.fbrk,
Pretty.str ("(==) = " ^ (lower_first o resolv) eqpred)
] |> SOME
- | haskell_from_def (_, Classinst (clsname, (tyco, arity), instmems)) =
+ | haskell_from_def (_, Classinst ((clsname, (tyco, arity)), (_, instmems))) =
Pretty.block [
Pretty.str "instance ",
haskell_from_sctxt arity,
@@ -972,14 +981,14 @@
haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)),
Pretty.str " where",
Pretty.fbrk,
- Pretty.chunks (map (fn (member, const) =>
+ Pretty.chunks (map (fn (member, (const, _)) =>
Pretty.str ((lower_first o resolv) member ^ " = " ^ (lower_first o resolv) const)
) instmems)
] |> SOME
in
case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs
of [] => NONE
- | l => (SOME o Pretty.block) l
+ | l => (SOME o Pretty.chunks o separate (Pretty.str "")) l
end;
in
--- a/src/Pure/Tools/codegen_thingol.ML Tue Dec 27 15:24:23 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Dec 27 15:24:40 2005 +0100
@@ -53,7 +53,9 @@
| Datatypecons of string
| Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list
| Classmember of class
- | Classinst of class * (string * (vname * string list) list) * (string * string) list;
+ | Classinst of (class * (string * (vname * sort) list))
+ * ((string * (string * ClassPackage.sortlookup list list)) list
+ * (string * (string * ClassPackage.sortlookup list list)) list);
type module;
type transact;
type 'dst transact_fin;
@@ -488,7 +490,9 @@
| Datatypecons of string
| Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list
| Classmember of class
- | Classinst of class * (string * (vname * string list) list) * (string * string) list;
+ | Classinst of (class * (string * (vname * sort) list))
+ * ((string * (string * ClassPackage.sortlookup list list)) list
+ * (string * (string * ClassPackage.sortlookup list list)) list);
datatype node = Def of def | Module of node Graph.T;
type module = node Graph.T;
@@ -549,7 +553,7 @@
Pretty.str "class member belonging to ",
Pretty.str clsname
]
- | pretty_def (Classinst (clsname, (tyco, arity), mems)) =
+ | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
Pretty.block [
Pretty.str "class instance (",
Pretty.str clsname,
@@ -557,8 +561,7 @@
Pretty.str tyco,
Pretty.str ", ",
Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str o snd) arity),
- Pretty.str ")) with ",
- Pretty.gen_list "," "[" "]" (map (fn (m1, m2) => Pretty.str (m1 ^ " => " ^ m2)) mems)
+ Pretty.str "))"
];
fun pretty_module modl =
@@ -777,10 +780,10 @@
| def => "attempted to add class member to non-class"
^ (Pretty.output o pretty_def) def |> error)])
end
- | *) add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) =
+ | *) add_check_transform (name, Classinst ((clsname, (tyco, arity)), (_, memdefs))) =
let
val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco
- ^ " of class " ^ quote clsname ^ " with " ^ (commas o map (fn (m1, m2) => m1 ^ " => " ^ m2)) memdefs) ();
+ ^ " of class " ^ quote clsname) ();
(* fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
let
val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c;
@@ -1197,41 +1200,6 @@
in transform_iexpr vname_alist e `$$ (snd o transform_lookups) ls end
| transform_iexpr vname_alist e =
map_iexpr transform_itype transform_ipat (transform_iexpr vname_alist) e;
- fun mk_cls_typ_map v membrs ty_inst =
- map (fn (m, (mctxt, ty)) =>
- (m, ty |> instant_itype (v, ty_inst))) membrs;
- fun extract_members (cls, Class (supclss, v, membrs, _)) =
- let
- val ty_cls = cls `%% [IVarT (v, [])];
- val w = "d";
- val add_supclss = if null supclss then I else cons (v, supclss);
- fun mk_fun (m, (mctxt, ty)) = (m, Fun ([([IVarP (w, ty_cls)], ILookup ([m], w))],
- (add_supclss mctxt, ty `-> ty_cls)));
- in fold (cons o mk_fun) membrs end
- | extract_members _ = I;
- fun introduce_dicts (Class (supcls, v, membrs, insts)) =
- let
- val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) membrs)) "a" 1 |> hd
- in
- Typesyn ([(varname_cls, supcls)], IDictT (mk_cls_typ_map v membrs (IVarT (varname_cls, []))))
- end
- | introduce_dicts (Classinst (clsname, (tyco, arity), memdefs)) =
- let
- val Class (_, v, members, _) =
- if clsname = class_eq
- then
- Class ([], "a", [(fun_eq, ([], IVarT ("a", []) `-> IVarT ("a", []) `-> Type_bool))], [])
- else
- get_def module clsname;
- val ty = tyco `%% map IVarT arity;
- val inst_typ_map = mk_cls_typ_map v members ty;
- val memdefs_ty = map (fn (memname, memprim) =>
- (memname, (memprim, (the o AList.lookup (op =) inst_typ_map) memname))) memdefs;
- in
- Fun ([([], IDictE (map (apsnd IConst) memdefs_ty))],
- ([], IType (clsname, [ty])))
- end
- | introduce_dicts d = d;
fun elim_sorts (Fun (eqs, ([], ty))) =
Fun (map (fn (ps, rhs) => (map transform_ipat ps, transform_iexpr [] rhs)) eqs,
([], transform_itype ty))
@@ -1255,6 +1223,56 @@
| elim_sorts (Typesyn (vars, ty)) =
Typesyn (map (fn (v, _) => (v, [])) vars, transform_itype ty)
| elim_sorts d = d;
+ fun mk_cls_typ_map v (supclss, membrs) ty_inst =
+ (map (fn class => (class, IType (class, [ty_inst]))) supclss,
+ map (fn (m, (mctxt, ty)) =>
+ (m, ty |> instant_itype (v, ty_inst))) membrs);
+ fun extract_members (cls, Class (supclss, v, membrs, _)) =
+ let
+ val ty_cls = cls `%% [IVarT (v, [])];
+ val w = "d";
+ val add_supclss = if null supclss then I else cons (v, supclss);
+ fun mk_fun (m, (mctxt, ty)) = (m, Fun ([([IVarP (w, ty_cls)], ILookup ([m], w))],
+ (add_supclss mctxt, ty `-> ty_cls)));
+ in fold (cons o mk_fun) membrs end
+ | extract_members _ = I;
+ fun introduce_dicts (Class (supclss, v, membrs, insts)) =
+ let
+ val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) membrs)) "a" 1 |> hd
+ in
+ Typesyn ([(varname_cls, supclss)], IDictT ((op @) (mk_cls_typ_map v (supclss, membrs) (IVarT (varname_cls, [])))))
+ end
+ | introduce_dicts (Classinst ((clsname, (tyco, arity)), (supinsts, memdefs))) =
+ let
+ val Class (supclss, v, members, _) =
+ if clsname = class_eq
+ then
+ Class ([], "a", [(fun_eq, ([], IVarT ("a", []) `-> IVarT ("a", []) `-> Type_bool))], [])
+ else
+ get_def module clsname;
+ val ty = tyco `%% map IVarT arity;
+ val (supinst_typ_map, mem_typ_map) = mk_cls_typ_map v (supclss, members) ty;
+ fun mk_meminst (m, ty) =
+ let
+ val (instname, instlookup) = (the o AList.lookup (op =) memdefs) m;
+ in
+ IInst (IConst (instname, ty), instlookup)
+ |> pair m
+ end;
+ val memdefs_ty = map mk_meminst mem_typ_map;
+ fun mk_supinst (supcls, dictty) =
+ let
+ val (instname, instlookup) = (the o AList.lookup (op =) supinsts) supcls;
+ in
+ IInst (IConst (instname, dictty), instlookup)
+ |> pair supcls
+ end;
+ val instdefs_ty = map mk_supinst supinst_typ_map;
+ in
+ Fun ([([], IDictE (instdefs_ty @ memdefs_ty))],
+ (arity, IType (clsname, [ty])))
+ end
+ | introduce_dicts d = d;
in
module
|> `(fn module => fold_defs extract_members module [])