--- 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 ["\\<Rightarrow>", "=>", constantsK, dependingK];
+val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", dependingK];
--- 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 *)
--- 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 *)