--- a/etc/isar-keywords-ZF.el Fri Dec 09 15:25:29 2005 +0100
+++ b/etc/isar-keywords-ZF.el Fri Dec 09 15:25:52 2005 +0100
@@ -201,6 +201,7 @@
"case_eqns"
"con_defs"
"concl"
+ "constants"
"constrains"
"contains"
"defined_by"
@@ -208,7 +209,6 @@
"depending_on"
"domains"
"elimination"
- "extracting"
"file"
"files"
"fixes"
--- a/etc/isar-keywords.el Fri Dec 09 15:25:29 2005 +0100
+++ b/etc/isar-keywords.el Fri Dec 09 15:25:52 2005 +0100
@@ -216,13 +216,13 @@
"compose"
"concl"
"congs"
+ "constants"
"constrains"
"contains"
"defined_by"
"defines"
"depending_on"
"distinct"
- "extracting"
"file"
"files"
"fixes"
--- a/src/Pure/Tools/class_package.ML Fri Dec 09 15:25:29 2005 +0100
+++ b/src/Pure/Tools/class_package.ML Fri Dec 09 15:25:52 2005 +0100
@@ -227,7 +227,7 @@
) subclasses;
fun mk_class_deriv thy subclasses superclass =
case get_superclass_derivation (subclasses, superclass)
- of (subclass::deriv) => (rev 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)
--- a/src/Pure/Tools/codegen_package.ML Fri Dec 09 15:25:29 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML Fri Dec 09 15:25:52 2005 +0100
@@ -60,14 +60,14 @@
-> appgen;
val appgen_case: (theory -> string -> (string * int) list option)
-> appgen;
- val defgen_datatype: (theory -> string -> (string list * string list) option)
+ val defgen_datatype: (theory -> string -> ((string * sort) list * string list) option)
-> (theory -> string * string -> typ list option)
-> defgen;
val defgen_datacons: (theory -> string * string -> typ list option)
-> defgen;
- val defgen_datatype_eq: (theory -> string -> (string list * string list) option)
+ val defgen_datatype_eq: (theory -> string -> ((string * sort) list * string list) option)
-> defgen;
- val defgen_datatype_eqinst: (theory -> string -> (string list * string list) option)
+ val defgen_datatype_eqinst: (theory -> string -> ((string * sort) list * string list) option)
-> defgen;
val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ)
-> defgen;
@@ -122,6 +122,7 @@
val nsp_class = "class";
val nsp_type = "type";
val nsp_const = "const";
+val nsp_dtcon = "dtcon"; (*NOT OPERATIONAL YET*)
val nsp_mem = "mem";
val nsp_inst = "inst";
val nsp_eq_class = "eq_class";
@@ -134,7 +135,7 @@
let
val name_root = "Generated";
val nsp_conn = [
- [nsp_class, nsp_type, nsp_eq_class], [nsp_const, nsp_inst, nsp_mem, nsp_eq]
+ [nsp_class, nsp_type, nsp_eq_class], [nsp_const, nsp_dtcon, nsp_inst, nsp_mem, nsp_eq]
];
in CodegenSerializer.ml_from_thingol nsp_conn name_root end;
@@ -142,7 +143,7 @@
let
val name_root = "Generated";
val nsp_conn = [
- [nsp_class, nsp_eq_class], [nsp_type], [nsp_const, nsp_eq], [nsp_inst], [nsp_mem]
+ [nsp_class, nsp_eq_class], [nsp_type], [nsp_const, nsp_mem, nsp_eq], [nsp_dtcon], [nsp_inst]
];
in CodegenSerializer.haskell_from_thingol nsp_conn name_root end;
@@ -756,13 +757,21 @@
fun defgen_clsdecl thy defs cls trns =
case name_of_idf thy nsp_class cls
of SOME cls =>
- trns
- |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
- |> fold_map (ensure_def_class thy defs)
- (map (idf_of_name thy nsp_class) (ClassPackage.get_superclasses thy cls))
- |-> (fn supcls => succeed (Class (supcls, "a", [], []),
- map (idf_of_name thy nsp_mem) (ClassPackage.the_consts thy cls)
- @ map (curry (idf_of_inst thy defs) cls) ((map fst o ClassPackage.the_tycos thy) cls)))
+ let
+ val memnames = ClassPackage.the_consts thy cls;
+ val memtypes = map (devarify_type o ClassPackage.get_const_sign thy "'a") memnames;
+ val memctxt = map (ClassPackage.extract_sortctxt thy) memtypes;
+ val memidfs = map (idf_of_name thy nsp_mem) memnames;
+ val instnames = map (curry (idf_of_inst thy defs) cls) ((map fst o ClassPackage.the_tycos thy) cls);
+ in
+ trns
+ |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
+ |> fold_map (ensure_def_class thy defs)
+ (map (idf_of_name thy nsp_class) (ClassPackage.get_superclasses thy cls))
+ ||>> fold_map (invoke_cg_type thy defs) memtypes
+ |-> (fn (supcls, memtypes) => succeed (Class (supcls, "a", memidfs ~~ (memctxt ~~ memtypes), []),
+ memidfs @ instnames))
+ end
| _ =>
trns
|> fail ("no class definition found for " ^ quote cls);
@@ -773,8 +782,7 @@
trns
|> debug 5 (fn _ => "trying defgen class member for " ^ quote f)
|> ensure_def_class thy defs (idf_of_name thy nsp_class ((the o ClassPackage.lookup_const_class thy) clsmem))
- ||>> (invoke_cg_type thy defs o devarify_type) (ClassPackage.get_const_sign thy "'a" clsmem)
- |-> (fn (cls, ty) => succeed (Classmember (cls, "a", ty), []))
+ |-> (fn cls => succeed (Classmember cls, []))
| _ =>
trns |> fail ("no class member found for " ^ quote f)
@@ -794,9 +802,9 @@
(ClassPackage.get_inst_consts_sign thy (tyco, cls));
val _ = debug 10 (fn _ => "(4) CLSINST " ^ cls ^ " - " ^ tyco) ()
fun add_vars arity clsmems (trns as (_, modl)) =
- ((Term.invent_names
- (map ((fn Classmember (_, _, ty) => ty) o get_def modl)
- clsmems |> tvars_of_itypes) "a" (length arity) ~~ arity, clsmems), trns)
+ 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 _ = debug 10 (fn _ => "(5) CLSINST " ^ cls ^ " - " ^ tyco) ()
in
trns
@@ -948,25 +956,33 @@
in
-fun defgen_datatype get_datatype get_datacons thy defs tyco trns =
- case tname_of_idf thy tyco
- of SOME dtname =>
- (case get_datatype thy dtname
- of SOME (vs, cnames) =>
- trns
- |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtname)
- |> succeed (Datatype (map (rpair [] o unprefix "'") vs, [], []),
- cnames
- |> map (idf_of_name thy nsp_const)
- |> map (fn "0" => "const.Zero" | c => c)
- (* |> add_eqinst get_datacons thy (snd trns) dtname cnames *))
- (*! VARIABLEN, EQTYPE !*)
+fun defgen_datatype get_datatype get_datacons thy defs idf trns =
+ case tname_of_idf thy idf
+ of SOME dtco =>
+ (case get_datatype thy dtco
+ of SOME (vars, cos) =>
+ let
+ val cotys = map (the o get_datacons thy o rpair dtco) cos;
+ val coidfs = cos
+ |> map (idf_of_name thy nsp_const)
+ |> map (fn "0" => "const.Zero" | c => c);
+ in
+ trns
+ |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
+ |> fold_map (invoke_cg_sort thy defs) (map snd vars)
+ ||>> (fold_map o fold_map) (invoke_cg_type thy defs o devarify_type) cotys
+ |-> (fn (sorts, tys) => succeed (Datatype
+ (map2 (fn (v, _) => fn sort => (unprefix "'" v, sort)) vars sorts, coidfs ~~ tys, []),
+ coidfs
+ (* |> add_eqinst get_datacons thy (snd trns) dtname cnames *)))
+ (*! VARIABLEN, EQTYPE !*)
+ end
| NONE =>
trns
- |> fail ("no datatype found for " ^ quote tyco))
+ |> fail ("no datatype found for " ^ quote dtco))
| NONE =>
trns
- |> fail ("not a type constructor: " ^ quote tyco)
+ |> fail ("not a type constructor: " ^ quote idf)
end;
end; (* local *)
@@ -984,12 +1000,11 @@
(case the_type c
of SOME dtname =>
(case get_datacons thy (c, dtname)
- of SOME tyargs =>
+ of SOME _ =>
trns
|> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote c)
|> ensure_def_tyco thy defs (idf_of_tname thy dtname)
- ||>> fold_map (invoke_cg_type thy defs o devarify_type) tyargs
- |-> (fn (dtname, tys) => succeed (Datatypecons (dtname, tys), []))
+ |-> (fn dtname => succeed (Datatypecons dtname, []))
| NONE =>
trns
|> fail ("no datatype constructor found for " ^ quote f))
@@ -1025,11 +1040,12 @@
case name_of_idf thy nsp_eq_class f
of SOME dtname =>
(case get_datatype thy dtname
- of SOME (vs, _) =>
+ of SOME (vars, _) =>
trns
|> debug 5 (fn _ => "trying defgen datatype_eqinst for " ^ quote dtname)
|> ensure_def_const thy defs (idf_of_name thy nsp_eq dtname)
- |-> (fn pred_eq => succeed (Classinst (class_eq, (dtname, vs ~~ replicate (length vs) [class_eq]), [(fun_eq, pred_eq)]), []))
+ |-> (fn pred_eq => succeed (Classinst (class_eq, (dtname,
+ map (fn (v, _) => (v, [class_eq])) vars), [(fun_eq, pred_eq)]), []))
| NONE =>
trns
|> fail ("no datatype found for " ^ quote dtname))
@@ -1348,8 +1364,8 @@
val (classK, generateK, serializeK, syntax_tycoK, syntax_constK, aliasK) =
("code_class", "code_generate", "code_serialize", "code_syntax_tyco", "code_syntax_const", "code_alias");
-val (extractingK, definedK, dependingK) =
- ("extracting", "defined_by", "depending_on");
+val (constantsK, definedK, dependingK) =
+ ("constants", "defined_by", "depending_on");
val classP =
OuterSyntax.command classK "codegen data for classes" K.thy_decl (
@@ -1371,7 +1387,7 @@
P.name
-- P.name
-- Scan.option (
- P.$$$ extractingK
+ P.$$$ constantsK
|-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
)
>> (fn ((serial_name, filename), consts) =>
@@ -1420,7 +1436,7 @@
);
val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP, syntax_tycoP, syntax_constP];
-val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", extractingK, definedK, dependingK];
+val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", constantsK, definedK, dependingK];
(* setup *)
--- a/src/Pure/Tools/codegen_serializer.ML Fri Dec 09 15:25:29 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Fri Dec 09 15:25:52 2005 +0100
@@ -138,77 +138,6 @@
in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end;
-(** grouping functions **)
-
-fun group_datatypes one_arg defs =
- let
- fun check_typ_dup dtname ts =
- if AList.defined (op =) ts dtname
- then error ("double datatype definition: " ^ quote dtname)
- else ts
- fun check_typ_miss dtname ts =
- if AList.defined (op =) ts dtname
- then ts
- else error ("missing datatype definition: " ^ quote dtname)
- fun group (name, Datatype (vs, _, _)) ts =
- (if one_arg
- then map (fn (_, []) => () | _ => error "can't serialize sort constrained datatype declaration to ML") vs
- else [];
- ts
- |> apsnd (check_typ_dup name)
- |> apsnd (AList.update (op =) (name, (vs, []))))
- | group (name, Datatypecons (dtname, tys as _::_::_)) ts =
- if one_arg
- then error ("datatype constructor containing more than one parameter")
- else
- ts
- |> apfst (AList.default (op =) (NameSpace.base dtname, []))
- |> apfst (AList.map_entry (op =) (NameSpace.base dtname) (cons (name, tys)))
- | group (name, Datatypecons (dtname, tys)) ts =
- ts
- |> apfst (AList.default (op =) (NameSpace.base dtname, []))
- |> apfst (AList.map_entry (op =) (NameSpace.base dtname) (cons (name, tys)))
- | group _ _ =
- error ("Datatype block containing other statements than datatype or constructor definitions")
- fun group_cons (dtname, co) ts =
- ts
- |> check_typ_miss dtname
- |> AList.map_entry (op =) dtname (rpair co o fst)
- in
- ([], [])
- |> fold group defs
- |-> (fn cons => fold group_cons cons)
- end;
-
-fun group_classes defs =
- let
- fun check_class_dup clsname ts =
- if AList.defined (op =) ts clsname
- then error ("double class definition: " ^ quote clsname)
- else ts
- fun check_clsname_miss clsname ts =
- if AList.defined (op =) ts clsname
- then ts
- else error ("missing class definition: " ^ quote clsname)
- fun group (name, Class (supercls, v, _, _)) ts =
- ts
- |> apsnd (check_class_dup name)
- |> apsnd (AList.update (op =) (name, ((supercls, v), [])))
- | group (name, Classmember (clsname, _, ty)) ts =
- ts
- |> apfst (AList.default (op =) (NameSpace.base clsname, []))
- |> apfst (AList.map_entry (op =) (NameSpace.base clsname) (cons (name, ty)))
- | group _ _ =
- error ("Datatype block containing other statements than datatype or constructor definitions")
- fun group_members (clsname, member) ts =
- ts
- |> check_clsname_miss clsname
- |> AList.map_entry (op =) clsname (rpair member o fst)
- in
- ([], [])
- |> fold group defs
- |-> (fn members => fold group_members members)
- end;
(** ML serializer **)
@@ -222,7 +151,7 @@
in
Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])])
end;
- val ml_label_uniq = translate_string (fn "'" => "''" | "." => "'" | c => c);
+ val ml_label_uniq = translate_string (fn "_" => "__" | "." => "_" | c => c);
fun ml_from_type br (IType ("Pair", [t1, t2])) =
brackify (eval_br_postfix br (INFX (2, L))) [
ml_from_type (INFX (2, X)) t1,
@@ -260,7 +189,7 @@
| ml_from_type _ (IVarT (_, sort)) =
"cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
| ml_from_type _ (IDictT fs) =
- (Pretty.enclose "{" "}" o Pretty.breaks) (
+ Pretty.gen_list "," "{" "}" (
map (fn (f, ty) =>
Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_type NOBR ty]) fs
);
@@ -382,18 +311,26 @@
| ml_from_expr br (IInst _) =
error "cannot serialize poly instant to ML"
| ml_from_expr br (IDictE fs) =
- (Pretty.enclose "{" "}" o Pretty.breaks) (
+ Pretty.gen_list "," "{" "}" (
map (fn (f, e) =>
Pretty.block [Pretty.str (ml_label_uniq 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 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) |> Pretty.str,
- Pretty.str ")",
- Pretty.str " ",
+ Pretty.str ("("
+ ^ (ls |> map ((fn s => "#" ^ s) o ml_label_uniq) |> foldr1 (fn (l, e) => l ^ " o " ^ e))
+ ^ ")"),
Pretty.str v
]
+ | ml_from_expr _ e =
+ error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
and mk_app_p br p args =
brackify (eval_br br BR)
(p :: map (ml_from_expr BR) args)
@@ -504,74 +441,78 @@
fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) =
let
val (pats_hd::pats_tl) = (fst o split_list) eqs;
- val _ = fold (fn x => fn y => (x ~~ y; y)) pats_tl pats_hd;
- (*check for equal length of argument lists*)
val shift = if null eq_tl then I else map (Pretty.block o single);
in (Pretty.block o Pretty.fbreaks o shift) (
mk_eq definer f ty eq
:: map (mk_eq "|" f ty) eq_tl
)
- end
+ end;
in
chunk_defs (
mk_fun definer d
:: map (mk_fun "and") ds_tl
- )
+ ) |> SOME
end;
fun ml_from_datatypes defs =
let
- fun mk_datatypes (ds as d::ds_tl) =
- let
- fun praetify [] f = [f]
- | praetify [p] f = [f, Pretty.str " of ", p]
- fun mk_cons (co, typs) =
- (Pretty.block oo praetify)
- (map (ml_from_type NOBR) typs)
- (Pretty.str (resolv co))
- fun mk_datatype definer (t, (vs, cs)) =
- Pretty.block (
- [Pretty.str definer]
- @ postify (map (ml_from_type BR o IVarT) vs)
- (Pretty.str (resolv t))
- @ [Pretty.str " =",
- Pretty.brk 1]
- @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
- )
- in
+ val defs' = List.mapPartial
+ (fn (name, Datatype info) => SOME (name, info)
+ | (name, Datatypecons _) => NONE
+ | (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o pretty_def) def)
+ ) ds
+ fun praetify [] f = [f]
+ | praetify [p] f = [f, Pretty.str " of ", p]
+ fun mk_cons (co, typs) =
+ (Pretty.block oo praetify)
+ (map (ml_from_type NOBR) typs)
+ (Pretty.str (resolv co))
+ fun mk_datatype definer (t, (vs, cs, _)) =
+ Pretty.block (
+ [Pretty.str definer]
+ @ postify (map (ml_from_type BR o IVarT) vs)
+ (Pretty.str (resolv t))
+ @ [Pretty.str " =",
+ Pretty.brk 1]
+ @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
+ )
+ in
+ case defs'
+ of d::ds_tl =>
chunk_defs (
mk_datatype "datatype " d
:: map (mk_datatype "and ") ds_tl
- )
- end;
- in
- (mk_datatypes o group_datatypes true) defs
+ ) |> SOME
+ | _ => NONE
end;
- fun ml_from_def (name, Typesyn (vs, ty)) =
- (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
- Pretty.block (
- Pretty.str "type "
- :: postify (map (Pretty.str o fst) vs) (Pretty.str name)
- @ [Pretty.str " =",
- Pretty.brk 1,
- ml_from_type NOBR ty,
- Pretty.str ";"
- ]))
- | ml_from_def (name, Nop) =
+ fun ml_from_def (name, Nop) =
if exists (fn query => query name)
[(fn name => (is_some o tyco_syntax) name),
(fn name => (is_some o const_syntax) name)]
- then Pretty.str ""
+ then NONE
else error ("empty statement during serialization: " ^ quote name)
+ | ml_from_def (name, Typesyn (vs, ty)) =
+ (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
+ Pretty.block (
+ Pretty.str "type "
+ :: postify (map (ml_from_type BR o IVarT) vs) (Pretty.str name)
+ @ [Pretty.str " =",
+ Pretty.brk 1,
+ ml_from_type NOBR ty,
+ Pretty.str ";"
+ ]
+ )) |> SOME
| ml_from_def (name, Class _) =
error ("can't serialize class declaration " ^ quote name ^ " to ML")
+ | ml_from_def (_, Classmember _) =
+ NONE
| ml_from_def (name, Classinst _) =
error ("can't serialize instance declaration " ^ quote name ^ " to ML")
- in (debug 10 (fn _ => "******************") (); (*map (writeln o Pretty.o)*)
- case (snd o hd) ds
- of Fun _ => ml_from_funs ds
- | Datatypecons _ => ml_from_datatypes ds
- | Datatype _ => ml_from_datatypes ds
- | _ => (case ds of [d] => ml_from_def d))
+ in (debug 10 (fn _ => "*** defs " ^ commas (map fst ds)) ();
+ case ds
+ of (_, Fun _)::_ => ml_from_funs ds
+ | (_, Datatypecons _)::_ => ml_from_datatypes ds
+ | (_, Datatype _)::_ => ml_from_datatypes ds
+ | [d] => ml_from_def d)
end;
in
@@ -619,8 +560,11 @@
| eta_expander s =
if NameSpace.is_qualified s
then case get_def module s
- of Datatypecons (_ , tys) =>
- if length tys >= 2 then length tys else 0
+ of Datatypecons dtname =>
+ (case get_def module dtname
+ of Datatype (_, cs, _) =>
+ let val l = AList.lookup (op =) cs s |> the |> length
+ in if l >= 2 then l else 0 end)
| _ =>
const_syntax s
|> Option.map fst
@@ -629,19 +573,17 @@
in
module
|> debug 12 (Pretty.output o pretty_module)
- |> debug 3 (fn _ => "connecting datatypes and classdecls...")
- |> connect_datatypes_clsdecls
|> debug 3 (fn _ => "selecting submodule...")
|> (if is_some select then (partof o the) select else I)
|> debug 3 (fn _ => "eta-expanding...")
|> eta_expand eta_expander
|> debug 3 (fn _ => "eta-expanding polydefs...")
|> eta_expand_poly
- |> debug 12 (Pretty.output o pretty_module)
|> debug 3 (fn _ => "tupelizing datatypes...")
|> tupelize_cons
|> debug 3 (fn _ => "eliminating classes...")
|> eliminate_classes
+ |> debug 12 (Pretty.output o pretty_module)
|> debug 3 (fn _ => "generating...")
|> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root
|> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
@@ -934,51 +876,11 @@
]
| haskell_from_binop br pr ass f args =
mk_app_p br (Pretty.str ("(" ^ f ^ ")")) args
- fun haskell_from_datatypes defs =
- let
- fun mk_cons (co, typs) =
- (Pretty.block o Pretty.breaks) (
- Pretty.str ((upper_first o resolv) co)
- :: map (haskell_from_type NOBR) typs
- )
- fun mk_datatype (t, (vs, cs)) =
- Pretty.block (
- Pretty.str "data "
- :: haskell_from_sctxt vs
- :: Pretty.str (upper_first t)
- :: Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vs)
- :: Pretty.str " ="
- :: Pretty.brk 1
- :: separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
- )
- in
- Pretty.chunks ((separate (Pretty.str "") o map mk_datatype o group_datatypes false) defs)
- end;
- fun haskell_from_classes defs =
- let
- fun mk_member (f, ty) =
- Pretty.block [
- Pretty.str (f ^ " ::"),
- Pretty.brk 1,
- haskell_from_type NOBR ty
- ];
- fun mk_class (clsname, ((supclsnames, v), members)) =
- Pretty.block [
- Pretty.str "class ",
- haskell_from_sctxt (map (fn class => (v, [class])) supclsnames),
- Pretty.str ((upper_first clsname) ^ " " ^ v),
- Pretty.str " where",
- Pretty.fbrk,
- Pretty.chunks (map mk_member members)
- ];
- in
- Pretty.chunks ((separate (Pretty.str "") o map mk_class o group_classes) defs)
- end;
fun haskell_from_def (name, Nop) =
if exists (fn query => query name)
[(fn name => (is_some o tyco_syntax) name),
(fn name => (is_some o const_syntax) name)]
- then Pretty.str ""
+ then NONE
else error ("empty statement during serialization: " ^ quote name)
| haskell_from_def (name, Fun (eqs, (_, ty))) =
let
@@ -999,7 +901,7 @@
haskell_from_type NOBR ty
],
Pretty.chunks (map (from_eq name) eqs)
- ]
+ ] |> SOME
end
| haskell_from_def (name, Typesyn (vs, ty)) =
Pretty.block [
@@ -1010,7 +912,47 @@
Pretty.str " =",
Pretty.brk 1,
haskell_from_type NOBR ty
- ]
+ ] |> SOME
+ | haskell_from_def (name, Datatype (vars, constrs, _)) =
+ let
+ fun mk_cons (co, tys) =
+ (Pretty.block o Pretty.breaks) (
+ Pretty.str ((upper_first o resolv) co)
+ :: map (haskell_from_type NOBR) tys
+ )
+ in
+ Pretty.block (
+ Pretty.str "data "
+ :: haskell_from_sctxt vars
+ :: Pretty.str (upper_first name)
+ :: Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vars)
+ :: Pretty.str " ="
+ :: Pretty.brk 1
+ :: separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons constrs)
+ )
+ end |> SOME
+ | haskell_from_def (_, Datatypecons _) =
+ NONE
+ | haskell_from_def (name, Class (supclasss, v, membrs, _)) =
+ let
+ fun mk_member (m, (_, ty)) =
+ Pretty.block [
+ Pretty.str (resolv m ^ " ::"),
+ Pretty.brk 1,
+ haskell_from_type NOBR ty
+ ]
+ in
+ Pretty.block [
+ Pretty.str "class ",
+ haskell_from_sctxt (map (fn class => (v, [class])) supclasss),
+ Pretty.str ((upper_first name) ^ " " ^ v),
+ Pretty.str " where",
+ Pretty.fbrk,
+ Pretty.chunks (map mk_member membrs)
+ ] |> SOME
+ end
+ | haskell_from_def (name, Classmember _) =
+ NONE
| haskell_from_def (_, Classinst (clsname, (tyco, arity), instmems)) =
Pretty.block [
Pretty.str "instance ",
@@ -1023,13 +965,11 @@
Pretty.chunks (map (fn (member, const) =>
Pretty.str ((lower_first o resolv) member ^ " = " ^ (lower_first o resolv) const)
) instmems)
- ];
- in case (snd o hd) defs
- of Datatypecons _ => haskell_from_datatypes defs
- | Datatype _ => haskell_from_datatypes defs
- | Class _ => haskell_from_classes defs
- | Classmember _ => haskell_from_classes defs
- | _ => Pretty.block (map haskell_from_def defs |> separate (Pretty.str ""))
+ ] |> SOME
+ in
+ case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs
+ of [] => NONE
+ | l => (SOME o Pretty.block) l
end;
in
@@ -1066,8 +1006,11 @@
| eta_expander s =
if NameSpace.is_qualified s
then case get_def module s
- of Datatypecons (_ , tys) =>
- if length tys >= 2 then length tys else 0
+ of Datatypecons dtname =>
+ (case get_def module dtname
+ of Datatype (_, cs, _) =>
+ let val l = AList.lookup (op =) cs s |> the |> length
+ in if l >= 2 then l else 0 end)
| _ =>
const_syntax s
|> Option.map fst
@@ -1081,8 +1024,6 @@
in
module
|> debug 12 (Pretty.output o pretty_module)
- |> debug 3 (fn _ => "connecting datatypes and classdecls...")
- |> connect_datatypes_clsdecls
|> debug 3 (fn _ => "selecting submodule...")
|> (if is_some select then (partof o the) select else I)
|> debug 3 (fn _ => "eta-expanding...")
--- a/src/Pure/Tools/codegen_thingol.ML Fri Dec 09 15:25:29 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Fri Dec 09 15:25:52 2005 +0100
@@ -1,4 +1,4 @@
- (* Title: Pure/Tools/codegen_thingol.ML
+(* Title: Pure/Tools/codegen_thingol.ML
ID: $Id$
Author: Florian Haftmann, TU Muenchen
@@ -48,10 +48,10 @@
Nop
| Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
| Typesyn of (vname * string list) list * itype
- | Datatype of (vname * string list) list * string list * string list
- | Datatypecons of string * itype list
- | Class of class list * vname * string list * string list
- | Classmember of class * vname * itype
+ | Datatype of (vname * string list) list * (string * itype list) list * string list
+ | 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;
type module;
type transact;
@@ -111,7 +111,6 @@
val extract_defs: iexpr -> string list;
val eta_expand: (string -> int) -> module -> module;
val eta_expand_poly: module -> module;
- val connect_datatypes_clsdecls: module -> module;
val tupelize_cons: module -> module;
val eliminate_classes: module -> module;
@@ -120,7 +119,7 @@
val soft_exc: bool ref;
val serialize:
- ((string -> string) -> (string * def) list -> Pretty.T)
+ ((string -> string) -> (string * def) list -> Pretty.T option)
-> (string * Pretty.T list -> Pretty.T)
-> (string -> string option)
-> string list list -> string -> module -> Pretty.T
@@ -212,6 +211,30 @@
| IDictE of (string * iexpr) list
| ILookup of (string list * vname);
+(*
+ variable naming conventions
+
+ bare names:
+ variable names v
+ class names cls
+ type constructor names tyco
+ datatype names dtco
+ const names (general) c
+ constructor names co
+ class member names m
+ arbitrary name s
+
+ constructs:
+ sort sort
+ type ty
+ expression e
+ pattern p
+ instance (cls, tyco) inst
+ variable (v, ty) var
+ class member (m, ty) membr
+ constructors (co, tys) constr
+ *)
+
val mk_funs = Library.foldr IFun;
val mk_apps = Library.foldl IApp;
val mk_abss = Library.foldr IAbs;
@@ -266,7 +289,8 @@
e
| map_iexpr f_itype f_ipat f_iexpr (IDictE ms) =
IDictE (map (apsnd f_iexpr) ms)
- | map_iexpr _ _ _ (ILookup _) = error "ILOOKUP";
+ | map_iexpr _ _ _ (e as ILookup _) =
+ e ;
fun fold_itype f_itype (IFun (t1, t2)) =
f_itype t1 #> f_itype t2
@@ -363,8 +387,8 @@
]
| pretty_iexpr (IDictE _) =
Pretty.str "<DictE>"
- | pretty_iexpr (ILookup _) =
- Pretty.str "<Lookup>";
+ | pretty_iexpr (ILookup (ls, v)) =
+ Pretty.str ("<Lookup: " ^ commas ls ^ " in " ^ v ^ ">");
(* language auxiliary *)
@@ -383,13 +407,19 @@
| itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
fun itype_of_ipat (ICons (_, ty)) = ty
- | itype_of_ipat (IVarP (_, ty)) = ty
+ | itype_of_ipat (IVarP (_, ty)) = ty;
fun ipat_of_iexpr (IConst (f, ty)) = ICons ((f, []), ty)
| ipat_of_iexpr (IVarE v) = IVarP v
| ipat_of_iexpr (e as IApp _) =
- case unfold_app e of (IConst (f, ty), es) =>
- ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty);
+ (case unfold_app e
+ of (IConst (f, ty), es) =>
+ ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty)
+ | (IInst (IConst (f, ty), _), es) =>
+ ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty)
+ | _ => error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e))
+ | ipat_of_iexpr e =
+ error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e);
fun tvars_of_itypes tys =
let
@@ -427,6 +457,8 @@
vars e
| vars (IDictE ms) =
fold (vars o snd) ms
+ | vars (ILookup (_, v)) =
+ cons v
in fold vars es [] end;
fun instant_itype (v, sty) ty =
@@ -449,10 +481,10 @@
Nop
| Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
| Typesyn of (vname * string list) list * itype
- | Datatype of (vname * string list) list * string list * string list
- | Datatypecons of string * itype list
- | Class of class list * vname * string list * string list
- | Classmember of class * vname * itype
+ | Datatype of (vname * string list) list * (string * itype list) list * string list
+ | 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;
datatype node = Def of def | Module of node Graph.T;
@@ -492,25 +524,24 @@
Pretty.block [
Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
Pretty.str " |=> ",
- Pretty.gen_list " |" "" "" (map Pretty.str cs),
+ Pretty.gen_list " |" "" ""
+ (map (fn (c, tys) => (Pretty.block o Pretty.breaks) (Pretty.str c :: map pretty_itype tys)) cs),
Pretty.str ", instances ",
Pretty.gen_list "," "[" "]" (map Pretty.str insts)
]
- | pretty_def (Datatypecons (dtname, tys)) =
+ | pretty_def (Datatypecons dtname) =
+ Pretty.str ("cons " ^ dtname)
+ | pretty_def (Class (supcls, v, mems, insts)) =
Pretty.block [
- Pretty.str "cons ",
- Pretty.gen_list " ->" "" "" (map pretty_itype tys @ [Pretty.str dtname])
- ]
- | pretty_def (Class (supcls, _, mems, insts)) =
- Pretty.block [
- Pretty.str "class extending ",
+ Pretty.str ("class var " ^ v ^ "extending "),
Pretty.gen_list "," "[" "]" (map Pretty.str supcls),
Pretty.str " with ",
- Pretty.gen_list "," "[" "]" (map Pretty.str mems),
+ Pretty.gen_list "," "[" "]"
+ (map (fn (m, (_, ty)) => Pretty.block [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
Pretty.str " instances ",
Pretty.gen_list "," "[" "]" (map Pretty.str insts)
]
- | pretty_def (Classmember (clsname, v, ty)) =
+ | pretty_def (Classmember clsname) =
Pretty.block [
Pretty.str "class member belonging to ",
Pretty.str clsname
@@ -543,12 +574,21 @@
fun pretty_deps modl =
let
fun one_node key =
- (Pretty.block o Pretty.fbreaks) (
- Pretty.str key
- :: (map (fn s => Pretty.str ("<- " ^ s)) o Graph.imm_preds modl) key
- @ (map (fn s => Pretty.str ("-> " ^ s)) o Graph.imm_succs modl) key
- @ (the_list oo Option.mapPartial) ((fn Module modl' => SOME (pretty_deps modl') | _ => NONE) o Graph.get_node modl) (SOME key)
- );
+ let
+ val preds_ = Graph.imm_preds modl key;
+ val succs_ = Graph.imm_succs modl key;
+ val mutbs = gen_inter (op =) (preds_, succs_);
+ val preds = fold (remove (op =)) mutbs preds_;
+ val succs = fold (remove (op =)) mutbs succs_;
+ in
+ (Pretty.block o Pretty.fbreaks) (
+ Pretty.str key
+ :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
+ @ map (fn s => Pretty.str ("<-- " ^ s)) preds
+ @ map (fn s => Pretty.str ("--> " ^ s)) succs
+ @ (the_list oo Option.mapPartial) ((fn Module modl' => SOME (pretty_deps modl') | _ => NONE) o Graph.get_node modl) (SOME key)
+ )
+ end
in
modl
|> Graph.strong_conn
@@ -697,7 +737,7 @@
|> dest_modl
end;
-fun add_check_transform (name, (Datatypecons (dtname, _))) =
+fun (*add_check_transform (name, (Datatypecons dtname)) =
(debug 7 (fn _ => "transformation for datatype constructor " ^ quote name
^ " of datatype " ^ quote dtname) ();
([([dtname],
@@ -733,11 +773,11 @@
| 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) ();
- fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
+ (* fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
let
val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c;
in if eq_itype (mtyp_i', mtyp_i)
@@ -748,9 +788,9 @@
end
| check defs =
"non-well-formed definitions encountered for classmembers: "
- ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME
+ ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME *)
in
- (map (fn (memname, memprim) => ([memname, memprim], check)) memdefs,
+ ((* map (fn (memname, memprim) => ([memname, memprim], check)) memdefs*) [],
[(clsname,
fn Class (supcs, v, mems, insts) => Class (supcs, v, mems, name::insts)
| def => "attempted to add class instance to non-class"
@@ -763,6 +803,13 @@
end
| add_check_transform _ = ([], []);
+(* checks to be implemented here lateron:
+ - well-formedness of function equations
+ - only possible to add defined constructors and class members
+ - right type abstraction with class members
+ - correct typing of instance definitions
+*)
+
fun succeed some = pair (Succeed some);
fun fail msg = pair (Fail ([msg], NONE));
@@ -945,21 +992,19 @@
val Fun_le = IConst (fun_le, Type_integer `-> Type_integer `-> Type_bool);
val Fun_wfrec = IConst (fun_wfrec, ((A `-> B) `-> A `-> B) `-> A `-> B);
-infix 7 xx;
-infix 5 **;
-infix 5 &&;
-
-fun a xx b = Type_pair a b;
-fun a ** b =
+fun foldl1 f (x::xs) =
+ Library.foldl f (x, xs);
+val ** = foldl1 (uncurry Type_pair);
+val XXp = foldl1 (fn (a, b) =>
+ let
+ val ty_a = itype_of_ipat a;
+ val ty_b = itype_of_ipat b;
+ in ICons ((cons_pair, [a, b]), Type_pair ty_a ty_b) end);
+val XXe = foldl1 (fn (a, b) =>
let
val ty_a = itype_of_iexpr a;
val ty_b = itype_of_iexpr b;
- in IConst (cons_pair, ty_a `-> ty_b `-> ty_a xx ty_b) `$ a `$ b end;
-fun a && b =
- let
- val ty_a = itype_of_ipat a;
- val ty_b = itype_of_ipat b;
- in ICons ((cons_pair, [a, b]), ty_a xx ty_b) end;
+ in IConst (cons_pair, ty_a `-> ty_b `-> Type_pair ty_a ty_b) `$ a `$ b end);
end; (* local *)
@@ -1000,12 +1045,8 @@
fun build_eqpred modl dtname =
let
- val cons =
- map ((fn Datatypecons c => c) o get_def modl)
- (case get_def modl dtname of Datatype (_, cs, _) => cs);
- val sortctxt =
- map (rpair [class_eq])
- (case get_def modl dtname of Datatype (_, vs, _) => vs);
+ val (vs, cons, _) = case get_def modl dtname of Datatype info => info;
+ val sortctxt = map (rpair [class_eq] o fst) vs
val ty = IType (dtname, map IVarT sortctxt);
fun mk_eq (c, []) =
([ICons ((c, []), ty), ICons ((c, []), ty)], Cons_true)
@@ -1085,31 +1126,26 @@
| map_def_fun def = def;
in map_defs map_def_fun end;
-fun connect_datatypes_clsdecls module =
- let
- fun extract_dep (name, Datatypecons (dtname, _)) =
- [(dtname, name)]
- | extract_dep (name, Classmember (cls, _, _)) =
- [(cls, name)]
- | extract_dep (name, def) = []
- in add_deps extract_dep module end;
-
fun tupelize_cons module =
let
- fun replace_def (_, (def as Datatypecons (_, []))) acc =
- (def, acc)
- | replace_def (_, (def as Datatypecons (_, [_]))) acc =
- (def, acc)
- | replace_def (name, (Datatypecons (tyco, tys))) acc =
- (Datatypecons (tyco,
- [foldr1 (op xx) tys]), name::acc)
- | replace_def (_, def) acc = (def, acc);
+ fun replace_cons (cons as (_, [])) =
+ pair cons
+ | replace_cons (cons as (_, [_])) =
+ pair cons
+ | replace_cons (con, tys) =
+ cons con
+ #> pair (con, [** tys])
+ fun replace_def (_, (def as Datatype (vs, cs, insts))) =
+ fold_map replace_cons cs
+ #-> (fn cs => pair (Datatype (vs, cs, insts)))
+ | replace_def (_, def) =
+ pair def
fun replace_app cs ((f, ty), es) =
if member (op =) cs f
then
let
val (tys, ty') = unfold_fun ty
- in IConst (f, foldr1 (op xx) tys `-> ty') `$ foldr1 (op **) es end
+ in IConst (f, ** tys `-> ty') `$ XXe es end
else IConst (f, ty) `$$ es;
fun replace_iexpr cs (IConst (f, ty)) =
replace_app cs ((f, ty), [])
@@ -1120,7 +1156,7 @@
| replace_iexpr cs e = map_iexpr I I (replace_iexpr cs) e;
fun replace_ipat cs (p as ICons ((c, ps), ty)) =
if member (op =) cs c then
- ICons ((c, [(foldr1 (op &&) (map (replace_ipat cs) ps))]), ty)
+ ICons ((c, [XXp (map (replace_ipat cs) ps)]), ty)
else map_ipat I (replace_ipat cs) p
| replace_ipat cs p = map_ipat I (replace_ipat cs) p;
in
@@ -1129,57 +1165,16 @@
fun eliminate_classes module =
let
- fun mk_cls_typ_map memberdecls ty_inst =
- map (fn (memname, (v, ty)) =>
- (memname, ty |> instant_itype (v, ty_inst))) memberdecls;
- fun transform_dicts (Class (supcls, v, members, _)) =
- let
- val memberdecls = AList.make
- ((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
- val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) memberdecls)) "a" 1 |> hd
- in
- Typesyn ([(varname_cls, [])], IDictT (mk_cls_typ_map memberdecls (IVarT (varname_cls, []))))
- end
- | transform_dicts (Classinst (clsname, (tyco, arity), memdefs)) =
+ fun transform_itype (IVarT (v, s)) =
+ IVarT (v, [])
+ | transform_itype (ty as IDictT _) =
+ ty
+ | transform_itype ty =
+ map_itype transform_itype ty;
+ fun transform_ipat p =
+ map_ipat transform_itype transform_ipat p;
+ fun transform_iexpr vname_alist (IInst (e, ls)) =
let
- val Class (_, _, members, _) = get_def module clsname;
- val memberdecls = AList.make
- ((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
- val ty_arity = tyco `%% map IVarT arity;
- val inst_typ_map = mk_cls_typ_map memberdecls ty_arity;
- 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))],
- ([], IDictT inst_typ_map))
- end
- | transform_dicts d = d
- fun transform_defs (Fun (ds, (sortctxt, ty))) =
- let
- val _ = writeln ("class 1");
- val varnames_ctxt =
- dig
- (Term.invent_names ((vars_of_iexprs o map snd) ds @ (vars_of_ipats o Library.flat o map fst) ds) "d" o length)
- (map snd sortctxt);
- val _ = writeln ("class 2");
- val vname_alist = map2 (fn (vt, sort) => fn vs => (vt, vs ~~ sort)) sortctxt varnames_ctxt;
- val _ = writeln ("class 3");
- fun add_typarms ty =
- map (foldr1 (op xx) o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist
- `--> ty;
- val _ = writeln ("class 4");
- fun add_parms ps =
- map (foldr1 (op &&) o (fn (vt, vss) => map (fn (v, cls) => IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist
- @ ps;
- val _ = writeln ("class 5");
- fun transform_itype (IVarT (v, s)) =
- IVarT (v, [])
- | transform_itype ty =
- map_itype transform_itype ty;
- val _ = writeln ("class 6");
- fun transform_ipat p =
- map_ipat transform_itype transform_ipat p;
- val _ = writeln ("class 7");
fun transform_lookup (ClassPackage.Instance ((cdict, idict), ls)) =
ls
|> transform_lookups
@@ -1191,27 +1186,87 @@
val (v', cls) =
(nth o the oo AList.lookup (op =)) vname_alist v i;
fun mk_parm tyco = tyco `%% [IVarT (v, [])];
- in (mk_parm cls, ILookup (rev deriv, v')) end
+ in (mk_parm cls, ILookup (deriv, v')) end
and transform_lookups lss =
map_yield (map_yield transform_lookup
- #> apfst (foldr1 (op xx))
- #> apsnd (foldr1 (op **))) lss;
- val _ = writeln ("class 8");
- fun transform_iexpr (IInst (e, ls)) =
- (writeln "A"; transform_iexpr e `$$ (snd o transform_lookups) ls)
- | transform_iexpr e =
- (writeln "B"; map_iexpr transform_itype transform_ipat transform_iexpr e);
- fun transform_rhs (ps, rhs) =
- (writeln ("LHS: " ^ (commas o map (Pretty.output o pretty_ipat)) ps);
- writeln ("RHS: " ^ ((Pretty.output o pretty_iexpr) rhs));
- (add_parms ps, writeln "---", transform_iexpr rhs) |> (fn (a, _, b) => (writeln "***"; (a, b))))
- val _ = writeln ("class 9");
- in Fun (map transform_rhs ds, ([], add_typarms ty)) end
- | transform_defs d = d
+ #> apfst **
+ #> apsnd XXe) lss
+ 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 _ = writeln "TRANSFORMING CLASS";
+ val _ = PolyML.print (Class (supcls, v, membrs, insts));
+ 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 _ = writeln "TRANSFORMING CLASSINST";
+ val _ = PolyML.print (Classinst (clsname, (tyco, arity), memdefs));
+ val Class (_, v, members, _) = 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))) =
+ (writeln "TRANSFORMING FUN ()";
+ Fun (map (fn (ps, rhs) => (map transform_ipat ps, transform_iexpr [] rhs)) eqs,
+ ([], transform_itype ty)))
+ | elim_sorts (Fun (eqs, (sortctxt, ty))) =
+ let
+ val _ = writeln "TRANSFORMING FUN (1)";
+ val varnames_ctxt =
+ dig
+ (Term.invent_names ((vars_of_iexprs o map snd) eqs @
+ (vars_of_ipats o Library.flat o map fst) eqs) "d" o length)
+ (map snd sortctxt);
+ val _ = writeln "TRANSFORMING FUN (2)";
+ val vname_alist = map2 (fn (vt, sort) => fn vs => (vt, vs ~~ sort))
+ sortctxt varnames_ctxt |> PolyML.print;
+ val _ = writeln "TRANSFORMING FUN (3)";
+ val ty' = map (op ** o (fn (vt, vss) => map (fn (_, cls) =>
+ cls `%% [IVarT (vt, [])]) vss)) vname_alist
+ `--> transform_itype ty;
+ val _ = writeln "TRANSFORMING FUN (4)";
+ val ps_add = map (XXp o (fn (vt, vss) => map (fn (v, cls) =>
+ IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist;
+ val _ = writeln "TRANSFORMING FUN (5)";
+ in Fun (map (fn (ps, rhs) => (ps_add @ map transform_ipat ps, transform_iexpr vname_alist rhs)) eqs, ([], ty')) before writeln "TRANSFORMING FUN (6)" end
+ | elim_sorts (Datatype (vars, constrs, insts)) =
+ (writeln "TRANSFORMING DATATYPE (1)";
+ Datatype (map (fn (v, _) => (v, [])) vars, map (apsnd (map transform_itype)) constrs, insts)
+ before writeln "TRANSFORMING DATATYPE (2)")
+ | elim_sorts (Typesyn (vars, ty)) =
+ (writeln "TRANSFORMING TYPESYN (1)";
+ Typesyn (map (fn (v, _) => (v, [])) vars, transform_itype ty)
+ before writeln "TRANSFORMING TYPESYN (2)")
+ | elim_sorts d = d;
in
module
- |> map_defs transform_dicts
- |> map_defs transform_defs
+ |> `(fn module => fold_defs extract_members module [])
+ |-> (fn membrs => fold (fn (name, f) => map_def name (K f)) membrs)
+ |> map_defs introduce_dicts
+ |> map_defs elim_sorts
end;
@@ -1302,16 +1357,23 @@
fun serialize s_def s_module validate nspgrp name_root module =
let
+ val _ = debug 15 (fn _ => "serialize 1") ();
val resolvtab = mk_resolvtab nspgrp validate module;
+ val _ = debug 15 (fn _ => "serialize 2") ();
val resolver = mk_resolv resolvtab;
+ val _ = debug 15 (fn _ => "serialize 3") ();
fun seri prfx ([(name, Module module)]) =
+ (debug 15 (fn _ => "serializing module " ^ quote name) ();
s_module (resolver prfx (prfx @ [name] |> NameSpace.pack),
- (map (seri (prfx @ [name]))
- ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))
+ List.mapPartial (seri (prfx @ [name]))
+ ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module))
+ |> SOME)
| seri prfx ds =
- s_def (resolver prfx) (map (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds)
+ (debug 15 (fn _ => "serializing definitions " ^ (commas o map fst) ds) ();
+ s_def (resolver prfx) (map
+ (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds))
in
- setmp print_mode [] (fn _ => s_module (name_root, (map (seri [])
+ setmp print_mode [] (fn _ => s_module (name_root, (List.mapPartial (seri [])
((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))) ()
end;