# HG changeset patch # User haftmann # Date 1134138352 -3600 # Node ID 9668764224a787e8db8f556aec3657905bffc252 # Parent 87cb7e641ba5d52421d2885d350169c5aafeeaea substantial improvements for class code generation diff -r 87cb7e641ba5 -r 9668764224a7 etc/isar-keywords-ZF.el --- 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" diff -r 87cb7e641ba5 -r 9668764224a7 etc/isar-keywords.el --- 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" diff -r 87cb7e641ba5 -r 9668764224a7 src/Pure/Tools/class_package.ML --- 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) diff -r 87cb7e641ba5 -r 9668764224a7 src/Pure/Tools/codegen_package.ML --- 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 ["\\", "=>", extractingK, definedK, dependingK]; +val _ = OuterSyntax.add_keywords ["\\", "=>", constantsK, definedK, dependingK]; (* setup *) diff -r 87cb7e641ba5 -r 9668764224a7 src/Pure/Tools/codegen_serializer.ML --- 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...") diff -r 87cb7e641ba5 -r 9668764224a7 src/Pure/Tools/codegen_thingol.ML --- 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 "" - | pretty_iexpr (ILookup _) = - Pretty.str ""; + | pretty_iexpr (ILookup (ls, v)) = + Pretty.str (""); (* 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;