# HG changeset patch # User haftmann # Date 1138021600 -3600 # Node ID 5eb3df798405f678471f55ab725312e5fbb1c5a3 # Parent eb3733779aa8eab58ce050ed8805b79bf5442dfa more general serializer diff -r eb3733779aa8 -r 5eb3df798405 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Mon Jan 23 14:06:28 2006 +0100 +++ b/src/Pure/Tools/codegen_package.ML Mon Jan 23 14:06:40 2006 +0100 @@ -6,9 +6,6 @@ intermediate language ("Thin-gol"). *) -(*NOTE: for simplifying developement, this package contains -some stuff which will finally be moved upwards to HOL*) - signature CODEGEN_PACKAGE = sig type auxtab; @@ -16,7 +13,8 @@ -> (string * typ) -> (thm list * typ) option; type defgen; type appgen = theory -> auxtab - -> (string * typ) * term list -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact; + -> (string * typ) * term list -> CodegenThingol.transact + -> CodegenThingol.iexpr * CodegenThingol.transact; val add_appconst: string * ((int * int) * appgen) -> theory -> theory; val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory; @@ -937,7 +935,8 @@ overltab1 |> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)), overltab2 - |> fold (fn (ty, _) => ConstNameMangler.declare thy (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab + |> fold (fn (ty, _) => ConstNameMangler.declare thy + (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab ))) deftab; fun mk_dtcontab thy = DatatypeconsNameMangler.empty @@ -962,10 +961,10 @@ val clsmemtab = mk_clsmemtab thy; in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end; -fun check_for_target thy target = - if (Symtab.defined o #target_data o CodegenData.get) thy target - then () - else error ("unknown code target language: " ^ quote target); +fun get_serializer target = + case Symtab.lookup (!serializers) target + of SOME seri => seri + | NONE => error ("unknown code target language: " ^ quote target); fun map_module f = map_codegen_data (fn (modl, gens, target_data, logic_data) => @@ -1070,7 +1069,7 @@ let fun mk reader raw_tyco target thy = let - val _ = check_for_target thy target; + val _ = get_serializer target; fun check_tyco tyco = if Sign.declared_tyname thy tyco then tyco @@ -1118,7 +1117,7 @@ let fun mk reader raw_const target thy = let - val _ = check_for_target thy target; + val _ = get_serializer target; val tabs = mk_tabs thy; val c = idf_of_const thy tabs (read_const thy raw_const); in @@ -1134,7 +1133,7 @@ fun add_pretty_list raw_nil raw_cons (target, seri) thy = let - val _ = check_for_target thy target; + val _ = get_serializer target; val tabs = mk_tabs thy; fun mk_const raw_name = let @@ -1151,58 +1150,42 @@ -(** code generation **) +(** toplevel interface **) + +local -fun generate_code raw_consts thy = +fun generate_code (SOME raw_consts) thy = + let + val consts = map (read_const thy) raw_consts; + fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts + in + thy + |> expand_module generate + |-> (fn cs => pair (SOME cs)) + end + | generate_code NONE thy = + (NONE, thy); + +fun serialize_code target seri raw_consts thy = let - val consts = map (read_const thy) raw_consts; - fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts - in - thy - |> expand_module generate - end; - -fun serialize_code target filename raw_consts thy = - let - fun get_serializer thy target = + fun serialize cs thy = let - val _ = check_for_target thy target; + val module = (#modl o CodegenData.get) thy; val target_data = thy |> CodegenData.get |> #target_data |> (fn data => (the oo Symtab.lookup) data target); - in - (the o Symtab.lookup (! serializers)) target ( + in (seri ( (Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, (Option.map fst oo Symtab.lookup o #syntax_const) target_data - ) - end; - fun use_code code = - if target = "ml" andalso filename = "-" - then use_text Context.ml_output false code - else File.write (Path.unpack filename) (code ^ "\n"); - fun serialize thy cs = - let - val module = (#modl o CodegenData.get) thy; - val seri = get_serializer thy target "Generated"; - in case cs - of [] => seri NONE module () |> fst |> Pretty.output |> use_code - | cs => seri (SOME cs) module () |> fst |> Pretty.output |> use_code - end; + ) "Generated" cs module : unit; thy) end; in thy - |> (if is_some raw_consts then generate_code (the raw_consts) else pair []) - |-> (fn cs => `(fn thy => serialize thy cs)) - |-> (fn _ => I) + |> generate_code raw_consts + |-> (fn cs => serialize cs) end; - - -(** toplevel interface **) - -local - structure P = OuterParse and K = OuterKeyword @@ -1214,8 +1197,8 @@ ("code_class", "code_generate", "code_serialize", "code_primclass", "code_primtyco", "code_primconst", "code_syntax_tyco", "code_syntax_const", "code_alias"); -val (constantsK, dependingK) = - ("constants", "depending_on"); +val dependingK = + ("depending_on"); val classP = OuterSyntax.command classK "codegen data for classes" K.thy_decl ( @@ -1227,21 +1210,26 @@ val generateP = 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)) + P.$$$ "(" + |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) + --| P.$$$ ")" + >> (fn raw_consts => + Toplevel.theory (generate_code (SOME raw_consts) #> snd)) ); val serializeP = OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl ( P.name - -- P.name -- Scan.option ( - P.$$$ constantsK + P.$$$ "(" |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) + --| P.$$$ ")" ) - >> (fn ((target, filename), raw_consts) => - Toplevel.theory (serialize_code target filename raw_consts)) + #-> (fn (target, raw_consts) => + get_serializer target + >> (fn seri => + Toplevel.theory (serialize_code target seri raw_consts) + )) ); val aliasP = @@ -1309,7 +1297,7 @@ val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP, primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP]; -val _ = OuterSyntax.add_keywords ["\\", "=>", constantsK, dependingK]; +val _ = OuterSyntax.add_keywords ["\\", "=>", dependingK]; diff -r eb3733779aa8 -r 5eb3df798405 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Mon Jan 23 14:06:28 2006 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Mon Jan 23 14:06:40 2006 +0100 @@ -11,12 +11,13 @@ type 'a pretty_syntax; type serializer = string list list - -> (string -> CodegenThingol.itype pretty_syntax option) + -> OuterParse.token list -> + ((string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iexpr pretty_syntax option) -> string -> string list option - -> CodegenThingol.module - -> unit -> Pretty.T * unit; + -> CodegenThingol.module -> unit) + * OuterParse.token list; val parse_syntax: (string -> 'b -> 'a * 'b) -> OuterParse.token list -> ('b -> 'a pretty_syntax * 'b) * OuterParse.token list; val parse_targetdef: (string -> string) -> string -> string; @@ -113,8 +114,8 @@ (* user-defined syntax *) val (atomK, infixK, infixlK, infixrK) = - ("atom", "infix", "infixl", "infixr"); -val _ = OuterSyntax.add_keywords ["atom", "infix", "infixl", "infixr"]; + ("target_atom", "infix", "infixl", "infixr"); +val _ = OuterSyntax.add_keywords [atomK, infixK, infixlK, infixrK]; fun parse_infix (fixity as INFX (i, x)) s = let @@ -208,18 +209,19 @@ type serializer = string list list - -> (string -> CodegenThingol.itype pretty_syntax option) + -> OuterParse.token list -> + ((string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iexpr pretty_syntax option) -> string -> string list option - -> CodegenThingol.module - -> unit -> Pretty.T * unit; + -> CodegenThingol.module -> unit) + * OuterParse.token list; -fun abstract_serializer preprocess (from_defs, from_module, validator) - (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) postprocess select module = +fun abstract_serializer (target, nspgrp) (from_defs, from_module, validator) + postprocess preprocess (tyco_syntax, const_syntax) name_root select module = let fun from_prim (name, prim) = - case AList.lookup (op =) prim target + case AList.lookup (op = : string * string -> bool) prim target of NONE => error ("no primitive definition for " ^ quote name) | SOME p => p; in @@ -253,11 +255,14 @@ |> (fn name' => if name = name' then NONE else SOME name') end; -fun postprocess_single_file path p = - File.write (Path.unpack path) (Pretty.output p ^ "\n"); +fun parse_single_file serializer = + OuterParse.name + >> (fn path => serializer (fn p => File.write (Path.unpack path) (Pretty.output p ^ "\n"))); -fun parse_single_file serializer = - OuterParse.name >> (fn path => serializer (postprocess_single_file path)); +fun parse_internal serializer = + OuterParse.name + >> (fn "-" => serializer (fn p => use_text Context.ml_output false (Pretty.output p)) + | _ => Scan.fail ()); (* list serializer *) @@ -557,21 +562,20 @@ in -fun ml_from_thingol target (nsp_dtcon, nsp_class, int_tyco) - nspgrp (tyco_syntax, const_syntax) name_root select module = +fun ml_from_thingol target (nsp_dtcon, nsp_class, int_tyco) nspgrp = let val reserved_ml = ThmDatabase.ml_reserved @ [ "bool", "int", "list", "true", "false" ]; - fun ml_from_module _ (name, ps) () = - (Pretty.chunks ([ + fun ml_from_module _ (name, ps) = + Pretty.chunks ([ str ("structure " ^ name ^ " = "), str "struct", str "" ] @ separate (str "") ps @ [ str "", str ("end; (* struct " ^ name ^ " *)") - ]), ()); + ]); fun needs_type (IType (tyco, _)) = has_nsp tyco nsp_class orelse tyco = int_tyco @@ -580,7 +584,9 @@ | needs_type _ = false; fun is_cons c = has_nsp c nsp_dtcon; - fun eta_expander s = + val serializer = abstract_serializer (target, nspgrp) + (ml_from_defs (is_cons, needs_type), ml_from_module, abstract_validator reserved_ml); + fun eta_expander module const_syntax s = case const_syntax s of SOME ((i, _), _) => i | _ => if has_nsp s nsp_dtcon @@ -590,18 +596,20 @@ let val l = AList.lookup (op =) cs s |> the |> length in if l >= 2 then l else 0 end else 0; - fun preprocess module = + fun preprocess const_syntax module = module |> tap (Pretty.writeln o pretty_deps) |> debug 3 (fn _ => "eta-expanding...") - |> eta_expand eta_expander + |> eta_expand (eta_expander module const_syntax) |> debug 3 (fn _ => "eta-expanding polydefs...") |> eta_expand_poly |> debug 3 (fn _ => "eliminating classes...") - |> eliminate_classes + |> eliminate_classes; in - abstract_serializer preprocess (ml_from_defs (is_cons, needs_type), ml_from_module, abstract_validator reserved_ml) - (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module + (parse_single_file serializer + || parse_internal serializer) + >> (fn seri => fn (tyco_syntax, const_syntax) => seri + (preprocess const_syntax) (tyco_syntax, const_syntax)) end; end; (* local *) @@ -861,8 +869,7 @@ in -fun hs_from_thingol target nsp_dtcon - nspgrp (tyco_syntax, const_syntax) name_root select module = +fun hs_from_thingol target nsp_dtcon nspgrp = let val reserved_hs = [ "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", @@ -876,26 +883,29 @@ val (pr, b) = split_last (NameSpace.unpack s); val (c::cs) = String.explode b; in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end; - fun hs_from_module _ (name, ps) () = - (Pretty.block [ + fun hs_from_module _ (name, ps) = + Pretty.block [ str ("module " ^ (upper_first name) ^ " where"), Pretty.fbrk, Pretty.fbrk, Pretty.chunks (separate (str "") ps) - ], ()); + ]; fun is_cons c = has_nsp c nsp_dtcon; - fun eta_expander c = + val serializer = abstract_serializer (target, nspgrp) + (hs_from_defs is_cons, hs_from_module, abstract_validator reserved_hs); + fun eta_expander const_syntax c = const_syntax c |> Option.map (fst o fst) |> the_default 0; - fun preprocess module = + fun preprocess const_syntax module = module |> tap (Pretty.writeln o pretty_deps) |> debug 3 (fn _ => "eta-expanding...") - |> eta_expand eta_expander + |> eta_expand (eta_expander const_syntax); in - abstract_serializer preprocess (hs_from_defs is_cons, hs_from_module, abstract_validator reserved_hs) - (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module + parse_single_file serializer + >> (fn seri => fn (tyco_syntax, const_syntax) => seri + (preprocess const_syntax) (tyco_syntax, const_syntax)) end; end; (* local *) diff -r eb3733779aa8 -r 5eb3df798405 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Mon Jan 23 14:06:28 2006 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Mon Jan 23 14:06:40 2006 +0100 @@ -88,9 +88,9 @@ val serialize: ((string -> string) -> (string * def) list -> 'a option) - -> (string list -> string * 'a list -> 'b -> 'a * 'b) + -> (string list -> string * 'a list -> 'a) -> (string -> string option) - -> string list list -> string -> module -> 'b -> 'a * 'b; + -> string list list -> string -> module -> 'a; end; signature CODEGEN_THINGOL_OP = @@ -1242,32 +1242,25 @@ (* serialization *) -fun serialize seri_defs seri_module validate nsp_conn name_root module ctxt = +fun serialize seri_defs seri_module validate nsp_conn name_root module = let val resolvtab = mk_resolvtab nsp_conn validate module; val resolver = mk_resolv resolvtab; fun mk_name prfx name = resolver prfx (NameSpace.pack (prfx @ [name])); - fun mk_contents prfx module ctxt = - ctxt - |> fold_map (seri prfx) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module) - |-> (fn xs => pair (List.mapPartial I xs)) - and seri prfx ([(name, Module modl)]) ctxt = - ctxt - |> mk_contents (prfx @ [name]) modl - |-> (fn [] => pair NONE - | xs => - seri_module (imports_of module name_root (prfx @ [name])) (mk_name prfx name, xs) - #-> (fn x => pair (SOME x))) - | seri prfx ds ctxt = + fun mk_contents prfx module = + List.mapPartial (seri prfx) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module) + and seri prfx ([(name, Module modl)]) = + (case mk_contents (prfx @ [name]) modl + of [] => NONE + | xs => + SOME (seri_module (imports_of module name_root (prfx @ [name])) (mk_name prfx name, xs))) + | seri prfx ds = ds |> map (fn (name, Def def) => (mk_name prfx name, def)) |> seri_defs (resolver prfx) - |> rpair ctxt in - ctxt - |> mk_contents [] module - |-> (fn xs => seri_module [] (name_root, xs)) + seri_module [] (name_root, (mk_contents [] module)) end; end; (* struct *)