# HG changeset patch # User haftmann # Date 1133276710 -3600 # Node ID 98431741bda3c54d824da1b0b799f0a5535a8447 # Parent 591e8cdea6f78b9a15747b0615a99f727d7bba7b added haskell serializer diff -r 591e8cdea6f7 -r 98431741bda3 src/Pure/Tools/codegen_package.ML --- 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), diff -r 591e8cdea6f7 -r 98431741bda3 src/Pure/Tools/codegen_serializer.ML --- 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 *) diff -r 591e8cdea6f7 -r 98431741bda3 src/Pure/Tools/codegen_thingol.ML --- 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 ""; 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 "" + | pretty_iexpr (ILookup _) = + Pretty.str ""; (* 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