--- a/src/Pure/Tools/codegen_package.ML Tue Nov 29 16:04:57 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML Tue Nov 29 16:05:10 2005 +0100
@@ -6,7 +6,7 @@
intermediate language ("Thin-gol").
*)
-(*NOTE: for simplifying development, this package contains
+(*NOTE: for simplifying developement, this package contains
some stuff which will finally be moved upwards to HOL*)
signature CODEGEN_PACKAGE =
@@ -120,13 +120,18 @@
val serializer_ml =
let
val name_root = "Generated";
- val nsp_conn_ml = [
+ val nsp_conn = [
[nsp_class, nsp_type, nsp_eq_class], [nsp_const, nsp_inst, nsp_mem, nsp_eq]
];
- in CodegenSerializer.ml_from_thingol nsp_conn_ml name_root end;
+ in CodegenSerializer.ml_from_thingol nsp_conn name_root end;
-fun serializer_hs _ _ _ _ =
- error ("haskell serialization not implemented yet");
+val serializer_hs =
+ let
+ val name_root = "Generated";
+ val nsp_conn = [
+ [nsp_class, nsp_eq_class], [nsp_type], [nsp_const], [nsp_inst], [nsp_mem], [nsp_eq]
+ ];
+ in CodegenSerializer.haskell_from_thingol nsp_conn name_root end;
(* theory data for codegen *)
@@ -223,7 +228,7 @@
fun merge_serialize_data
({ serializer = serializer, primitives = primitives1,
syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
- { serializer = _, primitives = primitives2,
+ {serializer = _, primitives = primitives2,
syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) =
{ serializer = serializer,
primitives = CodegenSerializer.merge_prims (primitives1, primitives2) : CodegenSerializer.primitives,
@@ -315,7 +320,7 @@
gens |> map_gens
(fn (codegens_sort, codegens_type, codegens_expr, defgens) =>
(codegens_sort, codegens_type,
- codegens_expr
+ codegens_expr
|> Output.update_warn (op =) ("overwriting existing expression code generator " ^ name) (name, (cg, stamp ())),
defgens)),
lookups, serialize_data, logic_data));
@@ -340,7 +345,7 @@
lookups |> map_lookups
(fn (lookups_tyco, lookups_const) =>
(lookups_tyco |> Symtab.update_new (src, dst),
- lookups_const)),
+ lookups_const)),
serialize_data, logic_data));
fun add_lookup_const ((src, ty), dst) =
@@ -350,7 +355,7 @@
lookups |> map_lookups
(fn (lookups_tyco, lookups_const) =>
(lookups_tyco,
- lookups_const |> Symtab.update_multi (src, (ty, dst)))),
+ lookups_const |> Symtab.update_multi (src, (ty, dst)))),
serialize_data, logic_data));
fun set_is_datatype f =
@@ -436,9 +441,9 @@
fun cname_of_idf thy ((_, overl_rev), _, _) idf =
case Symtab.lookup overl_rev idf
- of NONE =>
+ of NONE =>
(case name_of_idf thy nsp_const idf
- of NONE => (case name_of_idf thy nsp_mem idf
+ of NONE => (case name_of_idf thy nsp_mem idf
of NONE => NONE
| SOME n => SOME (n, Sign.the_const_constraint thy n))
| SOME n => SOME (n, Sign.the_const_constraint thy n))
@@ -509,7 +514,7 @@
|> pair f
else (f, trns);
-fun mk_fun thy defs eqs ty trns =
+fun mk_fun thy defs eqs ty trns =
let
val sortctxt = ClassPackage.extract_sortctxt thy ty;
fun mk_sortvar (v, sort) trns =
@@ -561,7 +566,7 @@
(sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class))
|-> (fn sort => succeed sort)
-fun codegen_type_default thy defs (v as TVar (_, sort)) trns =
+fun codegen_type_default thy defs(v as TVar (_, sort)) trns =
trns
|> invoke_cg_sort thy defs sort
|-> (fn sort => succeed (IVarT (name_of_tvar v, sort)))
@@ -598,7 +603,7 @@
val _ = debug 10 (fn _ => "making application (3)") ();
fun mk_itapp e [] = e
| mk_itapp e lookup = IInst (e, lookup);
- in
+ in
trns
|> debug 10 (fn _ => "making application (4): " ^ f ^ "::" ^ Sign.string_of_typ thy ty ^ " <~> " ^ Sign.string_of_typ thy ty_def)
|> ensure_def_const thy defs (idf_of_cname thy defs (f, ty))
@@ -662,7 +667,7 @@
fun defgen_tyco_fallback thy defs tyco trns =
if Symtab.fold (fn (_, { syntax_tyco, ... }) => fn b => b orelse Symtab.defined syntax_tyco tyco)
- ((#serialize_data o CodegenData.get) thy) false
+ ((#serialize_data o CodegenData.get) thy) false
then
trns
|> debug 5 (fn _ => "trying defgen tyco fallback for " ^ quote tyco)
@@ -673,7 +678,7 @@
fun defgen_const_fallback thy defs f trns =
if Symtab.fold (fn (_, { syntax_const, ... }) => fn b => b orelse Symtab.defined syntax_const f)
- ((#serialize_data o CodegenData.get) thy) false
+ ((#serialize_data o CodegenData.get) thy) false
then
trns
|> debug 5 (fn _ => "trying defgen const fallback for " ^ quote f)
@@ -709,6 +714,8 @@
case name_of_idf thy nsp_mem f
of SOME clsmem =>
let
+ val _ = debug 10 (fn _ => "CLSMEM " ^ quote clsmem) ();
+ val _ = debug 10 (fn _ => (the o ClassPackage.lookup_const_class thy) clsmem) ();
val cls = idf_of_name thy nsp_class ((the o ClassPackage.lookup_const_class thy) clsmem);
val (tvar, ty) = ClassPackage.get_const_sign thy clsmem;
in
@@ -725,20 +732,25 @@
of SOME (cls, tyco) =>
let
val arity = (map o map) (idf_of_name thy nsp_class)
- (ClassPackage.get_arities thy [cls] tyco)
+ (ClassPackage.get_arities thy [cls] tyco);
val clsmems = map (idf_of_name thy nsp_mem)
(ClassPackage.the_consts thy cls);
val instmem_idfs = map (idf_of_cname thy defs)
(ClassPackage.get_inst_consts_sign thy (tyco, cls));
+ fun add_vars arity clsmems (trns as (_, univ)) =
+ ((invent_var_t_names
+ (map ((fn Classmember (_, _, ty) => ty) o get_def univ)
+ clsmems) (length arity) [] "a" ~~ arity, clsmems), trns)
in
trns
|> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
- |> ensure_def_class thy defs (idf_of_name thy nsp_class cls)
+ |> (fold_map o fold_map) (ensure_def_class thy defs) arity
+ ||>> fold_map (ensure_def_const thy defs) clsmems
+ |-> (fn (arity, clsmems) => add_vars arity clsmems)
+ ||>> ensure_def_class thy defs (idf_of_name thy nsp_class cls)
||>> ensure_def_tyco thy defs (idf_of_tname thy tyco)
- ||>> (fold_map o fold_map) (ensure_def_class thy defs) arity
- ||>> fold_map (ensure_def_const thy defs) clsmems
||>> fold_map (ensure_def_const thy defs) instmem_idfs
- |-> (fn ((((cls, tyco), arity), clsmems), instmem_idfs) =>
+ |-> (fn ((((arity, clsmems), cls), tyco), instmem_idfs) =>
succeed (Classinst (cls, (tyco, arity), clsmems ~~ instmem_idfs), []))
end
| _ =>
@@ -859,7 +871,7 @@
)
| _ =>
trns
- |> fail ("not a case constant expression: " ^ Sign.string_of_term thy t)
+ |> fail ("not a caseconstant expression: " ^ Sign.string_of_term thy t)
end;
fun defgen_datatype get_datatype thy defs tyco trns =
@@ -952,29 +964,7 @@
|> null ? K ["x"]
|> space_implode "_"
end;
- fun add_def (name, [(ty, (_, (args, rhs)))]) (overl, defs, clstab) =
- (overl,
- defs |> Symtab.update_new (idf_of_name thy nsp_const name, (args, rhs, ty)),
- clstab)
- | add_def (name, ds) ((overl, overl_rev), defs, clstab) =
- let
- val ty_decl = Sign.the_const_constraint thy name;
- fun mk_idf ("0", Type ("nat", [])) = "const.Zero"
- | mk_idf ("1", Type ("nat", [])) = "."
- | mk_idf (nm, ty) =
- if is_number nm
- then nm
- else idf_of_name thy nsp_const nm
- ^ "_" ^ mangle_tyname (ty_decl, ty)
- val overl_lookups = map
- (fn (ty, (_, (args, rhs))) => (ty, mk_idf (name, ty), args, rhs)) ds;
- in
- ((overl |> Symtab.update_new (name, map (fn (ty, idf, _, _) => (ty, idf)) overl_lookups),
- overl_rev |> fold Symtab.update_new (map (fn (ty, idf, _, _) => (idf, (name, ty))) overl_lookups)),
- defs |> fold Symtab.update_new (map (fn (ty, idf, args, rhs) => (idf, (args, rhs, ty))) overl_lookups),
- clstab)
- end;
- fun mk_instname thyname (cls, tyco) =
+ fun mangle_instname thyname (cls, tyco) =
idf_of_name thy nsp_inst
(NameSpace.append thyname (NameSpace.base cls ^ "_" ^ NameSpace.base tyco))
fun add_clsmems classtab ((overl, overl_rev), defs, (clstab, clstab_rev, clsmems)) =
@@ -1001,19 +991,43 @@
(clstab
|> Symtab.fold
(fn (cls, (_, clsinsts)) => fold
- (fn (tyco, thyname) => Insttab.update ((cls, tyco), mk_instname thyname (cls, tyco))) clsinsts)
+ (fn (tyco, thyname) => Insttab.update ((cls, tyco), mangle_instname thyname (cls, tyco))) clsinsts)
classtab,
clstab_rev
|> Symtab.fold
(fn (cls, (_, clsinsts)) => fold
- (fn (tyco, thyname) => Symtab.update (mk_instname thyname (cls, tyco), (cls, tyco))) clsinsts)
+ (fn (tyco, thyname) => Symtab.update (mangle_instname thyname (cls, tyco), (cls, tyco))) clsinsts)
classtab,
clsmems
|> Symtab.fold
(fn (class, (clsmems, _)) => fold
(fn clsmem => Symtab.update (clsmem, class)) clsmems)
classtab))
- in
+ fun add_def (name, [(ty, (_, (args, rhs)))]) (overl, defs, clstab) =
+ (overl,
+ defs |> Symtab.update_new (idf_of_name thy nsp_const name, (args, rhs, ty)),
+ clstab)
+ | add_def (name, ds) ((overl, overl_rev), defs, clstab) =
+ let
+ val ty_decl = Sign.the_const_constraint thy name;
+ fun mk_idf ("0", Type ("nat", [])) = "const.Zero"
+ | mk_idf ("1", Type ("nat", [])) = "."
+ | mk_idf (nm, ty) =
+ if is_number nm
+ then nm
+ else idf_of_name thy nsp_const nm
+ ^ "_" ^ mangle_tyname (ty_decl, ty)
+ val overl_lookups = map
+ (fn (ty, (_, (args, rhs))) => (ty, mk_idf (name, ty), args, rhs)) ds;
+ in
+ ((overl
+ |> Symtab.default (name, [])
+ |> Symtab.map_entry name (append (map (fn (ty, idf, _, _) => (ty, idf)) overl_lookups)),
+ overl_rev
+ |> fold Symtab.update_new (map (fn (ty, idf, _, _) => (idf, (name, ty))) overl_lookups)),
+ defs
+ |> fold Symtab.update_new (map (fn (ty, idf, args, rhs) => (idf, (args, rhs, ty))) overl_lookups), clstab)
+ end; in
((Symtab.empty, Symtab.empty), Symtab.empty, (Insttab.empty, Symtab.empty, Symtab.empty))
|> add_clsmems (ClassPackage.get_classtab thy)
|> fold add_def (Codegen.mk_deftab thy |> Symtab.dest)
@@ -1174,9 +1188,13 @@
fun serialize_code serial_name filename consts thy =
let
- fun mk_sfun tab name args f =
- Symtab.lookup tab name
- |> Option.map (fn ms => Codegen.fillin_mixfix ms args (f : 'a -> Pretty.T))
+ fun mk_sfun tab =
+ let
+ fun na name =
+ Option.map Codegen.num_args_of (Symtab.lookup tab name)
+ fun stx name =
+ Codegen.fillin_mixfix ((the o Symtab.lookup tab) name)
+ in (na, stx) end;
val serialize_data =
thy
|> CodegenData.get
@@ -1188,7 +1206,7 @@
(#primitives serialize_data);
val _ = serializer' : string list option -> module -> Pretty.T;
val compile_it = serial_name = "ml" andalso filename = "-";
- fun use_code code =
+ fun use_code code =
if compile_it
then use_text Context.ml_output false code
else File.write (Path.unpack filename) (code ^ "\n");
@@ -1197,7 +1215,7 @@
|> (if is_some consts then generate_code (the consts) else pair [])
|-> (fn [] => `(serializer' NONE o #modl o CodegenData.get)
| consts => `(serializer' (SOME consts) o #modl o CodegenData.get))
- |-> (fn code => ((use_code o Pretty.output) code; I))
+ |-> (fn code => (setmp print_mode [] (use_code o Pretty.output) code; I))
end;
@@ -1214,14 +1232,14 @@
("code_generate", "code_serialize", "extracting", "defined_by", "depending_on", "code_alias", "code_syntax_tyco", "code_syntax_const");
val generateP =
- OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
+ OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
>> (fn consts =>
Toplevel.theory (generate_code consts #> snd))
);
val serializeP =
- OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl (
+ OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl (
P.name
-- P.name
-- Scan.option (
@@ -1233,7 +1251,7 @@
);
val aliasP =
- OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
+ OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
P.name
-- P.name
>> (fn (src, dst) => Toplevel.theory (add_alias (src, dst)))
@@ -1300,15 +1318,15 @@
add_defgen ("defs", defgen_defs),
add_defgen ("clsmem", defgen_clsmem),
add_defgen ("clsinst", defgen_clsinst),
- add_alias ("op <>", "neq"),
- add_alias ("op >=", "ge"),
- add_alias ("op >", "gt"),
- add_alias ("op <=", "le"),
- add_alias ("op <", "lt"),
- add_alias ("op +", "add"),
- add_alias ("op -", "minus"),
- add_alias ("op *", "times"),
- add_alias ("op @", "append"),
+ add_alias ("op <>", "op_neq"),
+ add_alias ("op >=", "op_ge"),
+ add_alias ("op >", "op_gt"),
+ add_alias ("op <=", "op_le"),
+ add_alias ("op <", "op_lt"),
+ add_alias ("op +", "op_add"),
+ add_alias ("op -", "op_minus"),
+ add_alias ("op *", "op_times"),
+ add_alias ("op @", "op_append"),
add_lookup_tyco ("bool", type_bool),
add_lookup_tyco ("IntDef.int", type_integer),
add_lookup_tyco ("List.list", type_list),
--- a/src/Pure/Tools/codegen_serializer.ML Tue Nov 29 16:04:57 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Nov 29 16:05:10 2005 +0100
@@ -15,13 +15,16 @@
val has_prim: primitives -> string -> bool;
val mk_prims: primitives -> string;
+ type num_args_syntax = string -> int option;
type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
- -> (string list * Pretty.T) option;
- type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
+ -> Pretty.T;
+ type serializer = num_args_syntax * CodegenThingol.itype pretty_syntax
+ -> num_args_syntax * CodegenThingol.iexpr pretty_syntax
-> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;
val ml_from_thingol: string list list -> string -> serializer;
+ val haskell_from_thingol: string list list -> string -> serializer;
end;
structure CodegenSerializer: CODEGEN_SERIALIZER =
@@ -64,9 +67,11 @@
(** generic serialization **)
+type num_args_syntax = string -> int option;
type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
- -> (string list * Pretty.T) option;
-type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
+ -> Pretty.T;
+type serializer = num_args_syntax * CodegenThingol.itype pretty_syntax
+ -> num_args_syntax * CodegenThingol.iexpr pretty_syntax
-> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;
@@ -105,94 +110,121 @@
| postify [p] f = [p, Pretty.brk 1, f]
| postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f];
-fun praetify [] f = [f]
- | praetify [p] f = [f, Pretty.str " of ", p]
+fun upper_first s =
+ let val (c :: cs) = String.explode s
+ in String.implode (Char.toUpper c :: cs) end;
+
+fun lower_first s =
+ let val (c :: cs) = String.explode s
+ in String.implode (Char.toLower c :: cs) end;
+
+
+(** grouping functions **)
+
+fun group_datatypes one_arg defs =
+ let
+ fun check_typ_dup dtname xs =
+ if AList.defined (op =) xs dtname
+ then error ("double datatype definition: " ^ quote dtname)
+ else xs
+ fun check_typ_miss dtname xs =
+ if AList.defined (op =) xs dtname
+ then xs
+ 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;
(** ML serializer **)
local
-fun ml_validator prims name =
+fun ml_from_defs (tyco_na, tyco_stx) (const_na, const_stx) resolv ds =
let
- fun replace_invalid c =
- if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
- andalso not (NameSpace.separator = c)
- then c
- else "_"
- fun suffix_it name =
- name
- |> member (op =) ThmDatabase.ml_reserved ? suffix "'"
- |> member (op =) CodegenThingol.prims ? suffix "'"
- |> has_prim prims ? suffix "'"
- |> (fn name' => if name = name' then name else suffix_it name')
- in
- name
- |> translate_string replace_invalid
- |> suffix_it
- |> (fn name' => if name = name' then NONE else SOME name')
- end;
-
-val ml_label_uniq = translate_string (fn "'" => "''" | "." => "'" | c => c);
-
-fun ml_from_defs styco sconst resolv ds =
- let
- fun chunk_defs ps =
+ 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;
- fun ml_from_typ br (IType ("Pair", [t1, t2])) =
+ 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_typ (INFX (2, X)) t1,
+ ml_from_type (INFX (2, X)) t1,
Pretty.str "*",
- ml_from_typ (INFX (2, X)) t2
+ ml_from_type (INFX (2, X)) t2
]
- | ml_from_typ br (IType ("Bool", [])) =
+ | ml_from_type br (IType ("Bool", [])) =
Pretty.str "bool"
- | ml_from_typ br (IType ("Integer", [])) =
+ | ml_from_type br (IType ("Integer", [])) =
Pretty.str "IntInf.int"
- | ml_from_typ br (IType ("List", [ty])) =
- postify ([ml_from_typ BR ty]) (Pretty.str "list")
+ | ml_from_type br (IType ("List", [ty])) =
+ postify ([ml_from_type BR ty]) (Pretty.str "list")
|> Pretty.block
- | ml_from_typ br (IType (tyco, typs)) =
+ | ml_from_type br (IType (tyco, typs)) =
let
- val tyargs = (map (ml_from_typ BR) typs)
+ val tyargs = (map (ml_from_type BR) typs)
in
- case styco tyco tyargs (ml_from_typ BR)
+ case tyco_na tyco
of NONE =>
postify tyargs ((Pretty.str o resolv) tyco)
|> Pretty.block
- | SOME ([], p) =>
- p
- | SOME (_, p) =>
- error ("cannot serialize partial type application to ML, while serializing "
- ^ quote (tyco ^ " " ^ Pretty.output (Pretty.list "(" ")" tyargs)))
+ | SOME i =>
+ if i <> length (typs)
+ then error "can only serialize strictly complete type applications to ML"
+ else tyco_stx tyco tyargs (ml_from_type BR)
end
- | ml_from_typ br (IFun (t1, t2)) =
+ | ml_from_type br (IFun (t1, t2)) =
brackify (eval_br_postfix br (INFX (1, R))) [
- ml_from_typ (INFX (1, X)) t1,
+ ml_from_type (INFX (1, X)) t1,
Pretty.str "->",
- ml_from_typ (INFX (1, R)) t2
+ ml_from_type (INFX (1, R)) t2
]
- | ml_from_typ _ (IVarT (v, [])) =
+ | ml_from_type _ (IVarT (v, [])) =
Pretty.str ("'" ^ v)
- | ml_from_typ _ (IVarT (_, sort)) =
+ | ml_from_type _ (IVarT (_, sort)) =
"cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
- | ml_from_typ _ (IDictT fs) =
+ | ml_from_type _ (IDictT fs) =
(Pretty.enclose "{" "}" o Pretty.breaks) (
map (fn (f, ty) =>
- Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_typ NOBR ty]) fs
+ Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_type NOBR ty]) fs
);
fun ml_from_pat br (ICons (("True", []), _)) =
Pretty.str "true"
| ml_from_pat br (ICons (("False", []), _)) =
Pretty.str "false"
- | ml_from_pat br (ICons (("Pair", ps), _)) =
- ps
- |> map (ml_from_pat NOBR)
- |> Pretty.list "(" ")"
+ | ml_from_pat br (ICons (("Pair", [p1, p2]), _)) =
+ Pretty.list "(" ")" [
+ ml_from_pat NOBR p1,
+ ml_from_pat NOBR p2
+ ]
| ml_from_pat br (ICons (("Nil", []), _)) =
Pretty.str "[]"
| ml_from_pat br (p as ICons (("Cons", _), _)) =
@@ -217,10 +249,14 @@
|> cons ((Pretty.str o resolv) f)
|> brackify (eval_br br BR)
| ml_from_pat br (IVarP (v, IType ("Integer", []))) =
- Pretty.str ("(" ^ v ^ ":IntInf.int)")
+ brackify (eval_br br BR) [
+ Pretty.str v,
+ Pretty.str ":",
+ Pretty.str "IntInf.int"
+ ]
| ml_from_pat br (IVarP (v, _)) =
Pretty.str v;
- fun ml_from_iexpr br (e as (IApp (IConst ("Cons", _), _))) =
+ fun ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) =
let
fun dest_cons (IApp (IConst ("Cons", _),
IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2)
@@ -229,33 +265,33 @@
case unfoldr dest_cons e
of (es, (IConst ("Nil", _))) =>
es
- |> map (ml_from_iexpr NOBR)
+ |> map (ml_from_expr NOBR)
|> Pretty.list "[" "]"
| (es, e) =>
(es @ [e])
- |> map (ml_from_iexpr (INFX (5, X)))
+ |> map (ml_from_expr (INFX (5, X)))
|> separate (Pretty.str "::")
|> brackify (eval_br br (INFX (5, R)))
end
- | ml_from_iexpr br (e as IApp (e1, e2)) =
+ | ml_from_expr br (e as IApp (e1, e2)) =
(case (unfold_app e)
of (e as (IConst (f, _)), es) =>
ml_from_app br (f, es)
- | _ =>
+ | _ =>
brackify (eval_br br BR) [
- ml_from_iexpr NOBR e1,
- ml_from_iexpr BR e2
+ ml_from_expr NOBR e1,
+ ml_from_expr BR e2
])
- | ml_from_iexpr br (e as IConst (f, _)) =
+ | ml_from_expr br (e as IConst (f, _)) =
ml_from_app br (f, [])
- | ml_from_iexpr br (IVarE (v, _)) =
+ | ml_from_expr br (IVarE (v, _)) =
Pretty.str v
- | ml_from_iexpr br (IAbs ((v, _), e)) =
+ | ml_from_expr br (IAbs ((v, _), e)) =
brackify (eval_br br BR) [
Pretty.str ("fn " ^ v ^ " =>"),
- ml_from_iexpr BR e
+ ml_from_expr NOBR e
]
- | ml_from_iexpr br (e as ICase (_, [_])) =
+ | ml_from_expr br (e as ICase (_, [_])) =
let
val (ps, e) = unfold_let e;
fun mk_val (p, e) = Pretty.block [
@@ -263,15 +299,15 @@
ml_from_pat BR p,
Pretty.str " =",
Pretty.brk 1,
- ml_from_iexpr NOBR e,
+ ml_from_expr NOBR e,
Pretty.str ";"
]
in Pretty.chunks [
[Pretty.str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
- [Pretty.str ("in"), Pretty.fbrk, ml_from_iexpr NOBR e] |> Pretty.block,
+ [Pretty.str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
Pretty.str ("end")
] end
- | ml_from_iexpr br (ICase (e, c::cs)) =
+ | ml_from_expr br (ICase (e, c::cs)) =
let
fun mk_clause definer (p, e) =
Pretty.block [
@@ -279,22 +315,22 @@
ml_from_pat NOBR p,
Pretty.str " =>",
Pretty.brk 1,
- ml_from_iexpr NOBR e
+ ml_from_expr NOBR e
]
in brackify (eval_br br BR) (
Pretty.str "case"
- :: ml_from_iexpr NOBR e
+ :: ml_from_expr NOBR e
:: mk_clause "of " c
:: map (mk_clause "| ") cs
) end
- | ml_from_iexpr br (IInst _) =
+ | ml_from_expr br (IInst _) =
error "cannot serialize poly instant to ML"
- | ml_from_iexpr br (IDictE fs) =
+ | ml_from_expr br (IDictE fs) =
(Pretty.enclose "{" "}" o Pretty.breaks) (
map (fn (f, e) =>
- Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_iexpr NOBR e]) fs
+ Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_expr NOBR e]) fs
)
- | ml_from_iexpr br (ILookup (ls, 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,
@@ -304,7 +340,7 @@
]
and mk_app_p br p args =
brackify (eval_br br BR)
- (p :: map (ml_from_iexpr BR) args)
+ (p :: map (ml_from_expr BR) args)
and ml_from_app br ("Nil", []) =
Pretty.str "[]"
| ml_from_app br ("True", []) =
@@ -313,75 +349,76 @@
Pretty.str "false"
| ml_from_app br ("primeq", [e1, e2]) =
brackify (eval_br br (INFX (4, L))) [
- ml_from_iexpr (INFX (4, L)) e1,
+ ml_from_expr (INFX (4, L)) e1,
Pretty.str "=",
- ml_from_iexpr (INFX (4, X)) e2
+ ml_from_expr (INFX (4, X)) e2
]
| ml_from_app br ("Pair", [e1, e2]) =
Pretty.list "(" ")" [
- ml_from_iexpr NOBR e1,
- ml_from_iexpr NOBR e2
+ ml_from_expr NOBR e1,
+ ml_from_expr NOBR e2
]
| ml_from_app br ("and", [e1, e2]) =
brackify (eval_br br (INFX (~1, L))) [
- ml_from_iexpr (INFX (~1, L)) e1,
+ ml_from_expr (INFX (~1, L)) e1,
Pretty.str "andalso",
- ml_from_iexpr (INFX (~1, X)) e2
+ ml_from_expr (INFX (~1, X)) e2
]
| ml_from_app br ("or", [e1, e2]) =
brackify (eval_br br (INFX (~2, L))) [
- ml_from_iexpr (INFX (~2, L)) e1,
+ ml_from_expr (INFX (~2, L)) e1,
Pretty.str "orelse",
- ml_from_iexpr (INFX (~2, X)) e2
+ ml_from_expr (INFX (~2, X)) e2
]
| ml_from_app br ("if", [b, e1, e2]) =
brackify (eval_br br BR) [
Pretty.str "if",
- ml_from_iexpr BR b,
+ ml_from_expr NOBR b,
Pretty.str "then",
- ml_from_iexpr BR e1,
+ ml_from_expr NOBR e1,
Pretty.str "else",
- ml_from_iexpr BR e2
+ ml_from_expr NOBR e2
]
| ml_from_app br ("add", [e1, e2]) =
brackify (eval_br br (INFX (6, L))) [
- ml_from_iexpr (INFX (6, L)) e1,
+ ml_from_expr (INFX (6, L)) e1,
Pretty.str "+",
- ml_from_iexpr (INFX (6, X)) e2
+ ml_from_expr (INFX (6, X)) e2
]
| ml_from_app br ("mult", [e1, e2]) =
brackify (eval_br br (INFX (7, L))) [
- ml_from_iexpr (INFX (7, L)) e1,
+ ml_from_expr (INFX (7, L)) e1,
Pretty.str "+",
- ml_from_iexpr (INFX (7, X)) e2
+ ml_from_expr (INFX (7, X)) e2
]
| ml_from_app br ("lt", [e1, e2]) =
brackify (eval_br br (INFX (4, L))) [
- ml_from_iexpr (INFX (4, L)) e1,
+ ml_from_expr (INFX (4, L)) e1,
Pretty.str "<",
- ml_from_iexpr (INFX (4, X)) e2
+ ml_from_expr (INFX (4, X)) e2
]
| ml_from_app br ("le", [e1, e2]) =
brackify (eval_br br (INFX (7, L))) [
- ml_from_iexpr (INFX (4, L)) e1,
+ ml_from_expr (INFX (4, L)) e1,
Pretty.str "<=",
- ml_from_iexpr (INFX (4, X)) e2
+ ml_from_expr (INFX (4, X)) e2
]
| ml_from_app br ("minus", es) =
mk_app_p br (Pretty.str "~") es
| ml_from_app br ("wfrec", es) =
mk_app_p br (Pretty.str "wfrec") es
+ | ml_from_app br (f, []) =
+ Pretty.str (resolv f)
| ml_from_app br (f, es) =
- let
- val args = map (ml_from_iexpr BR) es
- val brackify' = K (eval_br br BR) ? (single #> Pretty.enclose "(" ")")
- in
- case sconst f args (ml_from_iexpr BR)
- of NONE =>
- brackify (eval_br br BR) (Pretty.str (resolv f) :: args)
- | SOME (_, p) =>
- brackify' p
- end;
+ case const_na f
+ of NONE =>
+ let
+ val (es', e) = split_last es;
+ in mk_app_p br (ml_from_app NOBR (f, es')) [e] end
+ | SOME i =>
+ let
+ val (es1, es2) = splitAt (i, es);
+ in mk_app_p br (const_stx f (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end;
fun ml_from_funs (ds as d::ds_tl) =
let
fun mk_definer [] = "val"
@@ -399,9 +436,9 @@
let
val lhs = [Pretty.str (definer ^ " " ^ f)]
@ (if null pats
- then [Pretty.str ":", ml_from_typ NOBR ty]
+ then [Pretty.str ":", ml_from_type NOBR ty]
else map (ml_from_pat BR) pats)
- val rhs = [Pretty.str "=", ml_from_iexpr NOBR expr]
+ val rhs = [Pretty.str "=", ml_from_expr NOBR expr]
in
Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
end
@@ -422,44 +459,21 @@
:: map (mk_fun "and") ds_tl
)
end;
- fun ml_from_datatypes ds =
+ fun ml_from_datatypes defs =
let
- fun check_typ_dup ty xs =
- if AList.defined (op =) xs ty
- then error ("double datatype definition: " ^ quote ty)
- else xs
- fun check_typ_miss ty xs =
- if AList.defined (op =) xs ty
- then xs
- else error ("missing datatype definition: " ^ quote ty)
- fun group (name, Datatype (vs, _, _)) ts =
- (map (fn (_, []) => () | _ => error "can't serialize sort constrained datatype declaration to ML") vs;
- ts
- |> apsnd (check_typ_dup name)
- |> apsnd (AList.update (op =) (name, (vs, []))))
- | group (_, Datatypecons (_, _::_::_)) _ =
- error ("Datatype constructor containing more than one parameter")
- | group (name, Datatypecons (ty, tys)) ts =
- ts
- |> apfst (AList.default (op =) (resolv ty, []))
- |> apfst (AList.map_entry (op =) (resolv ty) (cons (name, tys)))
- | group _ _ =
- error ("Datatype block containing other statements than datatype or constructor definitions")
- fun group_cons (ty, co) ts =
- ts
- |> check_typ_miss ty
- |> AList.map_entry (op =) ty (rpair co o fst)
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_typ NOBR) typs)
+ (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_typ BR o IVarT) vs)
- (Pretty.str t)
+ @ 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)
@@ -471,10 +485,7 @@
)
end;
in
- ([], [])
- |> fold group ds
- |-> (fn cons => fold group_cons cons)
- |> mk_datatypes
+ (mk_datatypes o group_datatypes true) defs
end;
fun ml_from_def (name, Typesyn (vs, ty)) =
(map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
@@ -483,30 +494,50 @@
:: postify (map (Pretty.str o fst) vs) (Pretty.str name)
@ [Pretty.str " =",
Pretty.brk 1,
- ml_from_typ NOBR ty,
+ ml_from_type NOBR ty,
Pretty.str ";"
]))
| ml_from_def (name, Nop) =
if exists (fn query => (is_some o query) name)
- [(fn name => styco name [] (ml_from_typ NOBR)),
- (fn name => sconst name [] (ml_from_iexpr NOBR))]
+ [(fn name => tyco_na name),
+ (fn name => const_na name)]
then Pretty.str ""
else error ("empty statement during serialization: " ^ quote name)
| ml_from_def (name, Class _) =
error ("can't serialize class declaration " ^ quote name ^ " to ML")
| ml_from_def (name, Classinst _) =
error ("can't serialize instance declaration " ^ quote name ^ " to ML")
- in case (snd o hd) ds
+ in (writeln "******************"; (*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)
+ | _ => (case ds of [d] => ml_from_def d))
end;
in
-fun ml_from_thingol nspgrp name_root styco sconst prims select module =
+fun ml_from_thingol nspgrp name_root (tyco_syntax) (const_syntax as (const_na, _)) prims select module =
let
+ fun ml_validator name =
+ let
+ fun replace_invalid c =
+ if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
+ andalso not (NameSpace.separator = c)
+ then c
+ else "_"
+ fun suffix_it name =
+ name
+ |> member (op =) ThmDatabase.ml_reserved ? suffix "'"
+ |> member (op =) CodegenThingol.prims ? suffix "'"
+ |> has_prim prims ? suffix "'"
+ |> (fn name' => if name = name' then name else suffix_it name')
+ in
+ name
+ |> translate_string replace_invalid
+ |> suffix_it
+ |> (fn name' => if name = name' then NONE else SOME name')
+ end;
fun ml_from_module (name, ps) =
Pretty.chunks ([
Pretty.str ("structure " ^ name ^ " = "),
@@ -532,11 +563,10 @@
of Datatypecons (_ , tys) =>
if length tys >= 2 then length tys else 0
| _ =>
- (case sconst s [] (K (Pretty.str ""))
- of NONE => 0
- | SOME (xs, _) => length xs)
+ const_na s
+ |> the_default 0
else 0
- in
+ in
module
|> debug 12 (Pretty.output o pretty_module)
|> debug 3 (fn _ => "connecting datatypes and classdecls...")
@@ -553,7 +583,7 @@
|> debug 3 (fn _ => "eliminating classes...")
|> eliminate_classes
|> debug 3 (fn _ => "generating...")
- |> serialize (ml_from_defs styco sconst) ml_from_module (ml_validator prims) nspgrp name_root
+ |> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root
end;
fun ml_from_thingol' nspgrp name_root =
@@ -571,5 +601,396 @@
end; (* local *)
+local
+
+val bslash = "\\";
+
+fun haskell_from_defs (tyco_na, tyco_stx) (const_na, const_stx) is_cons resolv defs =
+ let
+ val resolv = fn s =>
+ let
+ val (prfix, base) = (split_last o NameSpace.unpack o resolv) s
+ in
+ NameSpace.pack (map upper_first prfix @ [base])
+ end;
+ fun resolv_const f =
+ if is_cons f
+ then (upper_first o resolv) f
+ else (lower_first o resolv) f
+ fun haskell_from_sctxt vs =
+ let
+ fun from_sctxt [] = Pretty.str ""
+ | from_sctxt vs =
+ vs
+ |> map (fn (v, cls) => Pretty.str ((upper_first o resolv) cls ^ " " ^ lower_first v))
+ |> Pretty.gen_list "," "(" ")"
+ |> (fn p => Pretty.block [p, Pretty.str " => "])
+ in
+ vs
+ |> map (fn (v, sort) => map (pair v) sort)
+ |> Library.flat
+ |> from_sctxt
+ end;
+ fun haskell_from_type br ty =
+ let
+ fun from_itype br (IType ("Pair", [t1, t2])) sctxt =
+ sctxt
+ |> from_itype NOBR t1
+ ||>> from_itype NOBR t2
+ |-> (fn (p1, p2) => pair (Pretty.gen_list "," "(" ")" [p1, p2]))
+ | from_itype br (IType ("List", [ty])) sctxt =
+ sctxt
+ |> from_itype NOBR ty
+ |-> (fn p => pair (Pretty.enclose "[" "]" [p]))
+ | from_itype br (IType (tyco, tys)) sctxt =
+ let
+ fun mk_itype NONE tyargs sctxt =
+ sctxt
+ |> pair (brackify (eval_br br BR) ((Pretty.str o upper_first o resolv) tyco :: tyargs))
+ | mk_itype (SOME i) tyargs sctxt =
+ if i <> length (tys)
+ then error "can only serialize strictly complete type applications to haskell"
+ else
+ sctxt
+ |> pair (tyco_stx tyco tyargs (haskell_from_type BR))
+ in
+ sctxt
+ |> fold_map (from_itype BR) tys
+ |-> mk_itype (tyco_na tyco)
+ end
+ | from_itype br (IFun (t1, t2)) sctxt =
+ sctxt
+ |> from_itype (INFX (1, X)) t1
+ ||>> from_itype (INFX (1, R)) t2
+ |-> (fn (p1, p2) => pair (
+ brackify (eval_br br (INFX (1, R))) [
+ p1,
+ Pretty.str "->",
+ p2
+ ]
+ ))
+ | from_itype br (IVarT (v, [])) sctxt =
+ sctxt
+ |> pair ((Pretty.str o lower_first) v)
+ | from_itype br (IVarT (v, sort)) sctxt =
+ sctxt
+ |> AList.default (op =) (v, [])
+ |> AList.map_entry (op =) v (fold (insert (op =)) sort)
+ |> pair ((Pretty.str o lower_first) v)
+ | from_itype br (IDictT _) _ =
+ error "cannot serialize dictionary type to haskell"
+ in
+ []
+ |> from_itype br ty
+ ||> haskell_from_sctxt
+ |> (fn (pty, pctxt) => Pretty.block [pctxt, pty])
+ end;
+ fun haskell_from_pat br (ICons (("Pair", [p1, p2]), _)) =
+ Pretty.list "(" ")" [
+ haskell_from_pat NOBR p1,
+ haskell_from_pat NOBR p2
+ ]
+ | haskell_from_pat br (ICons (("Nil", []), _)) =
+ Pretty.str "[]"
+ | haskell_from_pat br (p as ICons (("Cons", _), _)) =
+ let
+ fun dest_cons (ICons (("Cons", [p1, p2]), ty)) = SOME (p1, p2)
+ | dest_cons p = NONE
+ in
+ case unfoldr dest_cons p
+ of (ps, (ICons (("Nil", []), _))) =>
+ ps
+ |> map (haskell_from_pat NOBR)
+ |> Pretty.list "[" "]"
+ | (ps, p) =>
+ (ps @ [p])
+ |> map (haskell_from_pat (INFX (5, X)))
+ |> separate (Pretty.str ":")
+ |> brackify (eval_br br (INFX (5, R)))
+ end
+ | haskell_from_pat br (ICons ((f, ps), _)) =
+ ps
+ |> map (haskell_from_pat BR)
+ |> cons ((Pretty.str o upper_first o resolv) f)
+ |> brackify (eval_br br BR)
+ | haskell_from_pat br (IVarP (v, _)) =
+ (Pretty.str o lower_first) v;
+ fun haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) =
+ let
+ fun dest_cons (IApp (IApp (IConst ("Cons", _), e1), e2)) = SOME (e1, e2)
+ | dest_cons p = NONE
+ in
+ case unfoldr dest_cons e
+ of (es, (IConst ("Nil", _))) =>
+ es
+ |> map (haskell_from_expr NOBR)
+ |> Pretty.list "[" "]"
+ | (es, e) =>
+ (es @ [e])
+ |> map (haskell_from_expr (INFX (5, X)))
+ |> separate (Pretty.str ":")
+ |> brackify (eval_br br (INFX (5, R)))
+ end
+ | haskell_from_expr br (e as IApp (e1, e2)) =
+ (case (unfold_app e)
+ of (e as (IConst (f, _)), es) =>
+ haskell_from_app br (f, es)
+ | _ =>
+ brackify (eval_br br BR) [
+ haskell_from_expr NOBR e1,
+ haskell_from_expr BR e2
+ ])
+ | haskell_from_expr br (e as IConst (f, _)) =
+ haskell_from_app br (f, [])
+ | haskell_from_expr br (IVarE (v, _)) =
+ (Pretty.str o lower_first) v
+ | haskell_from_expr br (e as IAbs _) =
+ let
+ val (vs, body) = unfold_abs e
+ in
+ brackify (eval_br br BR) (
+ Pretty.str bslash
+ :: map (Pretty.str o lower_first o fst) vs @ [
+ Pretty.str "->",
+ haskell_from_expr NOBR body
+ ])
+ end
+ | haskell_from_expr br (e as ICase (_, [_])) =
+ let
+ val (ps, body) = unfold_let e;
+ fun mk_bind (p, e) = Pretty.block [
+ haskell_from_pat BR p,
+ Pretty.str " =",
+ Pretty.brk 1,
+ haskell_from_expr NOBR e
+ ];
+ in Pretty.chunks [
+ [Pretty.str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
+ [Pretty.str ("in "), haskell_from_expr NOBR body] |> Pretty.block
+ ] end
+ | haskell_from_expr br (ICase (e, c::cs)) =
+ let
+ fun mk_clause (p, e) =
+ Pretty.block [
+ haskell_from_pat NOBR p,
+ Pretty.str " ->",
+ Pretty.brk 1,
+ haskell_from_expr NOBR e
+ ]
+ in (Pretty.block o Pretty.fbreaks) (
+ Pretty.block [Pretty.str "case ", haskell_from_expr NOBR e, Pretty.str " of"]
+ :: map (mk_clause) cs
+ )end
+ | haskell_from_expr br (IInst (e, _)) =
+ haskell_from_expr br e
+ | haskell_from_expr br (IDictE _) =
+ error "cannot serialize dictionary expression to haskell"
+ | haskell_from_expr br (ILookup _) =
+ error "cannot serialize lookup expression to haskell"
+ and mk_app_p br p args =
+ brackify (eval_br br BR)
+ (p :: map (haskell_from_expr BR) args)
+ and haskell_from_app br ("Nil", []) =
+ Pretty.str "[]"
+ | haskell_from_app br ("Cons", es) =
+ mk_app_p br (Pretty.str "(:)") es
+ | haskell_from_app br ("primeq", [e1, e2]) =
+ brackify (eval_br br (INFX (4, L))) [
+ haskell_from_expr (INFX (4, L)) e1,
+ Pretty.str "==",
+ haskell_from_expr (INFX (4, X)) e2
+ ]
+ | haskell_from_app br ("Pair", [e1, e2]) =
+ Pretty.list "(" ")" [
+ haskell_from_expr NOBR e1,
+ haskell_from_expr NOBR e2
+ ]
+ | haskell_from_app br ("and", [e1, e2]) =
+ brackify (eval_br br (INFX (3, R))) [
+ haskell_from_expr (INFX (3, X)) e1,
+ Pretty.str "&&",
+ haskell_from_expr (INFX (3, R)) e2
+ ]
+ | haskell_from_app br ("or", [e1, e2]) =
+ brackify (eval_br br (INFX (2, L))) [
+ haskell_from_expr (INFX (2, L)) e1,
+ Pretty.str "||",
+ haskell_from_expr (INFX (2, X)) e2
+ ]
+ | haskell_from_app br ("if", [b, e1, e2]) =
+ brackify (eval_br br BR) [
+ Pretty.str "if",
+ haskell_from_expr NOBR b,
+ Pretty.str "then",
+ haskell_from_expr NOBR e1,
+ Pretty.str "else",
+ haskell_from_expr NOBR e2
+ ]
+ | haskell_from_app br ("add", [e1, e2]) =
+ brackify (eval_br br (INFX (6, L))) [
+ haskell_from_expr (INFX (6, L)) e1,
+ Pretty.str "+",
+ haskell_from_expr (INFX (6, X)) e2
+ ]
+ | haskell_from_app br ("mult", [e1, e2]) =
+ brackify (eval_br br (INFX (7, L))) [
+ haskell_from_expr (INFX (7, L)) e1,
+ Pretty.str "*",
+ haskell_from_expr (INFX (7, X)) e2
+ ]
+ | haskell_from_app br ("lt", [e1, e2]) =
+ brackify (eval_br br (INFX (4, L))) [
+ haskell_from_expr (INFX (4, L)) e1,
+ Pretty.str "<",
+ haskell_from_expr (INFX (4, X)) e2
+ ]
+ | haskell_from_app br ("le", [e1, e2]) =
+ brackify (eval_br br (INFX (7, L))) [
+ haskell_from_expr (INFX (4, L)) e1,
+ Pretty.str "<=",
+ haskell_from_expr (INFX (4, X)) e2
+ ]
+ | haskell_from_app br ("minus", es) =
+ mk_app_p br (Pretty.str "negate") es
+ | haskell_from_app br ("wfrec", es) =
+ mk_app_p br (Pretty.str "wfrec") es
+ | haskell_from_app br (f, []) =
+ Pretty.str (resolv_const f)
+ | haskell_from_app br (f, es) =
+ case const_na f
+ of NONE =>
+ let
+ val (es', e) = split_last es;
+ in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end
+ | SOME i =>
+ let
+ val (es1, es2) = splitAt (i, es);
+ in mk_app_p br (const_stx f (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end;
+ 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 = Pretty.str "";
+(*
+ | haskell_from_def (name, Class (supclsnames, members, insts)) = Pretty.str ""
+ | haskell_from_def (name, Classmember (clsname, v, ty)) = Pretty.str ""
+*)
+ fun haskell_from_def (name, Nop) =
+ if exists (fn query => (is_some o query) name)
+ [(fn name => tyco_na name),
+ (fn name => const_na name)]
+ then Pretty.str ""
+ else error ("empty statement during serialization: " ^ quote name)
+ | haskell_from_def (name, Fun (eqs, (_, ty))) =
+ let
+ fun from_eq name (args, rhs) =
+ Pretty.block [
+ Pretty.str (lower_first name),
+ Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args),
+ Pretty.brk 1,
+ Pretty.str ("="),
+ Pretty.brk 1,
+ haskell_from_expr NOBR rhs
+ ]
+ in
+ Pretty.chunks [
+ Pretty.block [
+ Pretty.str (name ^ " ::"),
+ Pretty.brk 1,
+ haskell_from_type NOBR ty
+ ],
+ Pretty.chunks (map (from_eq name) eqs)
+ ]
+ end
+ | haskell_from_def (name, Typesyn (vs, ty)) =
+ Pretty.block [
+ Pretty.str "type ",
+ haskell_from_sctxt vs,
+ Pretty.str (upper_first name),
+ Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vs),
+ Pretty.str " =",
+ Pretty.brk 1,
+ haskell_from_type NOBR ty
+ ]
+ | haskell_from_def (_, Classinst (clsname, (tyco, arity), instmems)) =
+ Pretty.block [
+ Pretty.str "instance ",
+ haskell_from_sctxt arity,
+ Pretty.str ((upper_first o resolv) clsname),
+ Pretty.str " ",
+ Pretty.str ((upper_first o resolv) tyco),
+ Pretty.str " where",
+ Pretty.fbrk,
+ 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 ""))
+ end;
+
+in
+
+fun haskell_from_thingol nspgrp name_root tyco_syntax (const_syntax as (const_na, _)) prims select module =
+ let
+ fun haskell_from_module (name, ps) =
+ Pretty.block [
+ Pretty.str ("module " ^ (upper_first name) ^ " where"),
+ Pretty.fbrk,
+ Pretty.fbrk,
+ Pretty.chunks (separate (Pretty.str "") ps)
+ ];
+ fun haskell_validator s = NONE;
+ fun eta_expander "Pair" = 2
+ | eta_expander "if" = 3
+ | 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
+ | _ =>
+ const_na s
+ |> the_default 0
+ else 0;
+ fun is_cons f =
+ NameSpace.is_qualified f
+ andalso case get_def module f
+ of Datatypecons _ => true
+ | _ => false;
+ 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 _ => "generating...")
+ |> serialize (haskell_from_defs tyco_syntax const_syntax is_cons) haskell_from_module haskell_validator nspgrp name_root
+ end;
+
+end; (* local *)
+
end; (* struct *)
--- a/src/Pure/Tools/codegen_thingol.ML Tue Nov 29 16:04:57 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Nov 29 16:05:10 2005 +0100
@@ -25,9 +25,6 @@
| ICase of iexpr * (ipat * iexpr) list
| IDictE of (string * iexpr) list
| ILookup of (string list * vname);
- val eq_itype: itype * itype -> bool
- val eq_ipat: ipat * ipat -> bool
- val eq_iexpr: iexpr * iexpr -> bool
val mk_funs: itype list * itype -> itype;
val mk_apps: iexpr * iexpr list -> iexpr;
val mk_abss: (vname * itype) list * iexpr -> iexpr;
@@ -38,9 +35,11 @@
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
val unfold_fun: itype -> itype list * itype;
val unfold_app: iexpr -> iexpr * iexpr list;
+ val unfold_abs: iexpr -> (vname * itype) list * iexpr;
val unfold_let: iexpr -> (ipat * iexpr) list * iexpr;
val itype_of_iexpr: iexpr -> itype;
val ipat_of_iexpr: iexpr -> ipat;
+ val eq_itype: itype * itype -> bool;
val invent_var_t_names: itype list -> int -> vname list -> vname -> vname list;
val invent_var_e_names: iexpr list -> int -> vname list -> vname -> vname list;
@@ -52,15 +51,14 @@
| Datatypecons of string * itype list
| Class of string list * string list * string list
| Classmember of string * vname * itype
- | Classinst of string * (string * string list list) * (string * string) list;
+ | Classinst of string * (string * (vname * string list) list) * (string * string) list;
type module;
type transact;
type 'dst transact_fin;
type ('src, 'dst) gen_codegen = 'src -> transact -> 'dst transact_fin;
type gen_defgen = string -> transact -> (def * string list) transact_fin;
- val eq_def: def * def -> bool;
val pretty_def: def -> Pretty.T;
- val pretty_module: module -> Pretty.T;
+ val pretty_module: module -> Pretty.T;
val empty_module: module;
val get_def: module -> string -> def;
val merge_module: module * module -> module;
@@ -222,10 +220,6 @@
| IDictE of (string * iexpr) list
| ILookup of (string list * vname);
-val eq_itype = (op =);
-val eq_ipat = (op =);
-val eq_iexpr = (op =);
-
val mk_funs = Library.foldr IFun;
val mk_apps = Library.foldl IApp;
val mk_abss = Library.foldr IAbs;
@@ -246,6 +240,10 @@
(fn IApp e => SOME e
| _ => NONE);
+val unfold_abs = unfoldr
+ (fn IAbs b => SOME b
+ | _ => NONE)
+
val unfold_let = unfoldr
(fn ICase (e, [(p, e')]) => SOME ((p, e), e')
| _ => NONE);
@@ -273,7 +271,10 @@
| map_iexpr _ _ _ (e as IConst _) =
e
| map_iexpr _ _ _ (e as IVarE _) =
- e;
+ e
+ | map_iexpr f_itype f_ipat f_iexpr (IDictE ms) =
+ IDictE (map (apsnd f_iexpr) ms)
+ | map_iexpr _ _ _ (ILookup _) = error "ILOOKUP";
fun fold_itype f_itype (IFun (t1, t2)) =
f_itype t1 #> f_itype t2
@@ -294,13 +295,41 @@
| fold_iexpr f_itype f_ipat f_iexpr (IAbs (v, e)) =
f_iexpr e
| fold_iexpr f_itype f_ipat f_iexpr (ICase (e, ps)) =
- f_iexpr e #> fold (fn (p, e) => f_ipat p #> f_iexpr e) ps
+ f_iexpr e #> fold (fn (p, e) => f_ipat p #> f_iexpr e) ps
| fold_iexpr _ _ _ (e as IConst _) =
I
| fold_iexpr _ _ _ (e as IVarE _) =
I;
+(* simple type matching *)
+
+fun eq_itype (ty1, ty2) =
+ let
+ exception NO_MATCH;
+ fun eq (IVarT (v1, sort1)) (IVarT (v2, sort2)) subs =
+ if sort1 <> sort2
+ then raise NO_MATCH
+ else
+ (case AList.lookup (op =) subs v1
+ of NONE => subs |> AList.update (op =) (v1, v2)
+ | (SOME v1') =>
+ if v1' <> v2
+ then raise NO_MATCH
+ else subs)
+ | eq (IType (tyco1, tys1)) (IType (tyco2, tys2)) subs =
+ if tyco1 <> tyco2
+ then raise NO_MATCH
+ else subs |> fold2 eq tys1 tys2
+ | eq (IFun (ty11, ty12)) (IFun (ty21, ty22)) subs =
+ subs |> eq ty11 ty21 |> eq ty12 ty22
+ | eq _ _ _ = raise NO_MATCH;
+ in
+ (eq ty1 ty2 []; true)
+ handle NO_MATCH => false
+ end;
+
+
(* simple diagnosis *)
fun pretty_itype (IType (tyco, tys)) =
@@ -309,12 +338,14 @@
Pretty.gen_list "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
| pretty_itype (IVarT (v, sort)) =
Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort))
+ | pretty_itype (IDictT _) =
+ Pretty.str "<DictT>";
fun pretty_ipat (ICons ((cons, ps), ty)) =
Pretty.gen_list " " "(" ")"
(Pretty.str cons :: map pretty_ipat ps @ [Pretty.str ":: ", pretty_itype ty])
| pretty_ipat (IVarP (v, ty)) =
- Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
+ Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty];
fun pretty_iexpr (IConst (f, ty)) =
Pretty.block [Pretty.str (f ^ "::"), pretty_itype ty]
@@ -338,6 +369,10 @@
]
) cs)
]
+ | pretty_iexpr (IDictE _) =
+ Pretty.str "<DictE>"
+ | pretty_iexpr (ILookup _) =
+ Pretty.str "<Lookup>";
(* language auxiliary *)
@@ -351,7 +386,7 @@
else error ("inconsistent application: in " ^ Pretty.output (pretty_iexpr e)
^ ", " ^ (Pretty.output o pretty_itype) ty2 ^ " vs. " ^ (Pretty.output o pretty_itype o itype_of_iexpr) e2)
| _ => error ("expression is not a function: " ^ Pretty.output (pretty_iexpr e1)))
- | itype_of_iexpr (IInst (e, cs)) = error ""
+ | itype_of_iexpr (IInst (e, cs)) = itype_of_iexpr e
| itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
| itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
@@ -402,22 +437,25 @@
fun invent (IConst (f, _)) =
I
| invent (IVarE (v, _)) =
- cons v
+ insert (op =) v
| invent (IApp (e1, e2)) =
invent e1 #> invent e2
| invent (IAbs ((v, _), e)) =
- cons v #> invent e
+ insert (op =) v #> invent e
| invent (ICase (e, cs)) =
invent e
- #>
- fold (fn (p, e) => append (vars_of_ipats [p]) #> invent e) cs
+ #> fold (fn (p, e) => fold (insert (op =)) (vars_of_ipats [p]) #> invent e) cs
+ | invent (IInst (e, lookup)) =
+ invent e
+ | invent (IDictE ms) =
+ fold (invent o snd) ms
+ | invent (ILookup (ls, v)) = error "ILOOKUP"
in Term.invent_names (fold invent es used) a n end;
+
(** language module system - definitions, modules, transactions **)
-
-
(* type definitions *)
datatype def =
@@ -428,7 +466,7 @@
| Datatypecons of string * itype list
| Class of string list * string list * string list
| Classmember of string * string * itype
- | Classinst of string * (string * string list list) * (string * string) list;
+ | Classinst of string * (string * (vname * string list) list) * (string * string) list;
datatype node = Def of def | Module of node Graph.T;
type module = node Graph.T;
@@ -478,26 +516,26 @@
]
| pretty_def (Class (supcls, mems, insts)) =
Pretty.block [
- Pretty.str "class extending",
+ Pretty.str "class extending ",
Pretty.gen_list "," "[" "]" (map Pretty.str supcls),
- Pretty.str "with ",
+ Pretty.str " with ",
Pretty.gen_list "," "[" "]" (map Pretty.str mems),
- Pretty.str "instances ",
+ Pretty.str " instances ",
Pretty.gen_list "," "[" "]" (map Pretty.str insts)
]
- | pretty_def (Classmember (cls, v, ty)) =
+ | pretty_def (Classmember (clsname, v, ty)) =
Pretty.block [
Pretty.str "class member belonging to ",
- Pretty.str cls
+ Pretty.str clsname
]
- | pretty_def (Classinst (cls, (tyco, arity), mems)) =
+ | pretty_def (Classinst (clsname, (tyco, arity), mems)) =
Pretty.block [
Pretty.str "class instance (",
- Pretty.str cls,
+ Pretty.str clsname,
Pretty.str ", (",
Pretty.str tyco,
Pretty.str ", ",
- Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str) arity),
+ Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str o snd) arity),
Pretty.str "))"
];
@@ -658,7 +696,8 @@
(debug 7 (fn _ => "transformation for datatype constructor " ^ quote name
^ " of datatype " ^ quote dtname) ();
([([dtname],
- fn [Datatype (_, _, [])] => NONE | _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
+ fn [Datatype (_, _, [])] => NONE
+ | _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
[(dtname,
fn Datatype (vs, cs, clss) => Datatype (vs, name::cs, clss)
| def => "attempted to add datatype constructor to non-datatype: "
@@ -692,20 +731,16 @@
| add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) =
let
val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco
- ^ " of class " ^ quote clsname) ();
+ ^ " of class " ^ quote clsname) ();
fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
let
- val _ = writeln "CHECK RUNNING (1)";
- val mtyp_i' = instant_itype (v, tyco `%%
- map2 IVarT ((invent_var_t_names [mtyp_c] (length arity) [] "a"), arity)) mtyp_c;
- val _ = writeln "CHECK RUNNING (2)";
- in let val XXX = (
- if eq_itype (mtyp_i', mtyp_i) (*! PERHAPS TOO STRICT !*)
- then NONE
- else "wrong type signature for class member: "
- ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected,"
- ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME
- ) in (writeln "CHECK RUNNING (3)"; XXX) end end
+ val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c;
+ in if eq_itype (mtyp_i', mtyp_i)
+ then NONE
+ else "wrong type signature for class member: "
+ ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected, "
+ ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME
+ end
| check defs =
"non-well-formed definitions encountered for classmembers: "
^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME
@@ -735,16 +770,15 @@
let
fun handle_fail msgs f =
let
- fun handl trns =
- trns |> f
- handle FAIL exc => (Fail exc, ([], modl))
in
if ! soft_exc
then
- ([], modl) |> handl
- handle e => (Fail (msgs, SOME e), ([], modl))
+ ([], modl) |> f
+ handle FAIL exc => (Fail exc, ([], modl))
+ | e => (Fail (msgs, SOME e), ([], modl))
else
- ([], modl) |> handl
+ ([], modl) |> f
+ handle FAIL exc => (Fail exc, ([], modl))
end;
fun select msgs [(gname, gen)] =
handle_fail (msgs @ [mk_msg gname]) (gen src)
@@ -773,7 +807,6 @@
val (checks, trans) = add_check_transform (name, def);
fun check (check_defs, checker) modl =
let
- val _ = writeln ("CHECK (1): " ^ commas check_defs)
fun get_def' s =
if NameSpace.is_qualified s
then get_def modl s
@@ -781,12 +814,10 @@
val defs =
check_defs
|> map get_def';
- val _ = writeln ("CHECK (2): " ^ commas check_defs)
in
- let val XXX = case checker defs
+ case checker defs
of NONE => modl
- | SOME e => raise FAIL ([e], NONE)
- in (writeln "CHECK (3)"; XXX) end
+ | SOME msg => raise FAIL ([msg], NONE)
end;
fun transform (name, f) modl =
modl
@@ -957,8 +988,12 @@
let
val delta = query f - length es;
val add_n = if delta < 0 then 0 else delta;
+ val tys =
+ (fst o unfold_fun) ty
+ |> curry Library.drop (length es)
+ |> curry Library.take add_n
val add_vars =
- invent_var_e_names es add_n [] "x" ~~ Library.drop (length es, (fst o unfold_fun) ty);
+ invent_var_e_names es add_n [] "x" ~~ tys;
in
Library.foldr IAbs (add_vars, IConst (f, ty) `$$ es `$$ (map IVarE add_vars))
end;
@@ -988,7 +1023,7 @@
fun connect_datatypes_clsdecls module =
let
- fun extract_dep (name, Datatypecons (dtname, _)) =
+ fun extract_dep (name, Datatypecons (dtname, _)) =
[(dtname, name)]
| extract_dep (name, Classmember (cls, _, _)) =
[(cls, name)]
@@ -1033,7 +1068,7 @@
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, members, insts)) =
+ fun transform_dicts (Class (supcls, members, _)) =
let
val memberdecls = AList.make
((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
@@ -1041,13 +1076,12 @@
in
Typesyn ([(varname_cls, [])], IDictT (mk_cls_typ_map memberdecls (IVarT (varname_cls, []))))
end
- | transform_dicts (Classinst (tyco, (cls, arity), memdefs)) =
+ | transform_dicts (Classinst (clsname, (tyco, arity), memdefs)) =
let
- val Class (_, members, _) = get_def module cls;
+ 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 (invent_var_t_names (map (snd o snd) memberdecls)
- (length arity) [] "a" ~~ arity);
+ 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;
@@ -1059,45 +1093,57 @@
fun transform_defs (Fun (ds, (sortctxt, ty))) =
let
fun reduce f xs = foldl' f (NONE, xs);
+ val _ = writeln ("class 1");
val varnames_ctxt =
sortctxt
|> length o Library.flat o map snd
|> (fn used => invent_var_e_names (map snd ds) used ((vars_of_ipats o fst o hd) ds) "d")
|> unflat (map snd sortctxt);
+ val _ = writeln ("class 2");
val vname_alist = map2 (fn ((vt, sort), vs) => (vt, vs ~~ sort)) (sortctxt, varnames_ctxt);
+ val _ = writeln ("class 3");
fun add_typarms ty =
map (reduce (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 (reduce (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;
- fun transform_lookup (ClassPackage.Instance ((cdict, idict), ls)) =
+ val _ = writeln ("class 7");
+ fun transform_lookup (ClassPackage.Instance ((cdict, idict), ls)) =
ls
|> transform_lookups
- |-> (fn ty =>
- curry mk_apps (IConst (idict, cdict `%% ty))
- #> pair (cdict `%% ty))
+ |-> (fn tys =>
+ curry mk_apps (IConst (idict, cdict `%% tys))
+ #> pair (cdict `%% tys))
| transform_lookup (ClassPackage.Lookup (deriv, (v, i))) =
let
val (v', cls) =
(nth o the oo AList.lookup (op =)) vname_alist v i;
fun mk_parm tyco = tyco `%% [IVarT (v, [])];
- in (mk_parm (hd (deriv)), ILookup (rev deriv, v')) end
+ in (mk_parm cls, ILookup (rev deriv, v')) end
and transform_lookups lss =
map_yield (map_yield transform_lookup
#> apfst (reduce (op xx))
#> apsnd (reduce (op **))) lss;
+ val _ = writeln ("class 8");
fun transform_iexpr (IInst (e, ls)) =
- transform_iexpr e `$$ (snd o transform_lookups) ls
- | transform_iexpr e =
- map_iexpr transform_itype transform_ipat transform_iexpr e;
- fun transform_rhs (ps, rhs) = (add_parms ps, transform_iexpr rhs)
+ (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
in
@@ -1174,7 +1220,7 @@
|> fill_in [] [] module
end;
-fun mk_resolv tab =
+fun mk_resolv tab =
let
fun resolver modl name =
if NameSpace.is_qualified name then