--- a/src/Pure/Tools/codegen_package.ML Mon Jan 30 08:19:30 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Mon Jan 30 08:20:06 2006 +0100
@@ -76,7 +76,7 @@
structure CodegenPackage : CODEGEN_PACKAGE =
struct
-open CodegenThingolOp;
+open CodegenThingol;
infix 8 `%%;
infixr 6 `->;
infixr 6 `-->;
@@ -673,10 +673,14 @@
let
val sortctxt = ClassPackage.extract_sortctxt thy ty;
fun dest_eqthm eq_thm =
- eq_thm
- |> prop_of
- |> Logic.dest_equals
- |> apfst (strip_comb #> snd);
+ let
+ val ((t, args), rhs) = (apfst strip_comb o Logic.dest_equals o prop_of) eq_thm;
+ in case t
+ of Const (c', _) => if c' = c then (args, rhs)
+ else error ("illegal function equation for " ^ quote c
+ ^ ", actually defining " ^ quote c')
+ | _ => error ("illegal function equation for " ^ quote c)
+ end;
fun mk_eq (args, rhs) trns =
trns
|> fold_map (exprgen_term thy tabs o devarify_term) args
@@ -1179,7 +1183,7 @@
in (seri (
(Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
(Option.map fst oo Symtab.lookup o #syntax_const) target_data
- ) "Generated" cs module : unit; thy) end;
+ ) cs module : unit; thy) end;
in
thy
|> generate_code raw_consts
@@ -1191,28 +1195,18 @@
in
-val (classK, generateK, serializeK,
+val (generateK, serializeK,
primclassK, primtycoK, primconstK,
syntax_tycoK, syntax_constK, aliasK) =
- ("code_class", "code_generate", "code_serialize",
+ ("code_generate", "code_serialize",
"code_primclass", "code_primtyco", "code_primconst",
"code_syntax_tyco", "code_syntax_const", "code_alias");
val dependingK =
("depending_on");
-val classP =
- OuterSyntax.command classK "codegen data for classes" K.thy_decl (
- P.xname
- -- ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name))
- -- (Scan.optional ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) [])
- >> (fn ((name, tycos), consts) => (Toplevel.theory (ClassPackage.add_classentry name consts tycos)))
- )
-
val generateP =
OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
- P.$$$ "("
- |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
- --| P.$$$ ")"
+ Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
>> (fn raw_consts =>
Toplevel.theory (generate_code (SOME raw_consts) #> snd))
);
@@ -1220,13 +1214,11 @@
val serializeP =
OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl (
P.name
- -- Scan.option (
- P.$$$ "("
- |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
- --| P.$$$ ")"
- )
+ -- Scan.option (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)))
#-> (fn (target, raw_consts) =>
- get_serializer target
+ P.$$$ "("
+ |-- get_serializer target
+ --| P.$$$ ")"
>> (fn seri =>
Toplevel.theory (serialize_code target seri raw_consts)
))
@@ -1268,9 +1260,6 @@
(Toplevel.theory oo fold) (add_prim_const raw_const depends) primdefs)
);
-val _ : OuterParse.token list -> (string -> string -> theory -> theory) * OuterParse.token list
- = parse_syntax_tyco;
-
val syntax_tycoP =
OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
Scan.repeat1 (
@@ -1295,23 +1284,23 @@
fold (fn (target, modifier) => modifier raw_c target) syns)
);
-val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP,
+val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP,
primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP];
-val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", dependingK];
+val _ = OuterSyntax.add_keywords [dependingK];
(** theory setup **)
-val _ = Context.add_setup
- (add_eqextr ("defs", eqextr_defs) #>
- add_defgen ("clsdecl", defgen_clsdecl) #>
- add_defgen ("funs", defgen_funs) #>
- add_defgen ("clsmem", defgen_clsmem) #>
- add_defgen ("datatypecons", defgen_datatypecons));
-
+val _ = Context.add_setup (
+ add_eqextr ("defs", eqextr_defs)
+ #> add_defgen ("funs", defgen_funs)
+ #> add_defgen ("clsdecl", defgen_clsdecl)
+ #> add_defgen ("clsmem", defgen_clsmem)
+ #> add_defgen ("clsinst", defgen_clsinst)
+ #> add_defgen ("datatypecons", defgen_datatypecons)
(* add_appconst_i ("op =", ((2, 2), appgen_eq)) *)
-(* add_defgen ("clsinst", defgen_clsinst) *)
+);
end; (* local *)
--- a/src/Pure/Tools/codegen_serializer.ML Mon Jan 30 08:19:30 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Mon Jan 30 08:20:06 2006 +0100
@@ -14,7 +14,6 @@
-> OuterParse.token list ->
((string -> CodegenThingol.itype pretty_syntax option)
* (string -> CodegenThingol.iexpr pretty_syntax option)
- -> string
-> string list option
-> CodegenThingol.module -> unit)
* OuterParse.token list;
@@ -31,7 +30,7 @@
structure CodegenSerializer: CODEGEN_SERIALIZER =
struct
-open CodegenThingolOp;
+open CodegenThingol;
infix 8 `%%;
infixr 6 `->;
infixr 6 `-->;
@@ -40,6 +39,7 @@
infixr 5 `|->;
infixr 5 `|-->;
+
(** generic serialization **)
(* precedences *)
@@ -155,7 +155,7 @@
fun parse_nonatomic_mixfix reader s ctxt =
case parse_mixfix reader s ctxt
- of ([Pretty _], _) => error ("mixfix contains just one pretty element; either declare as " ^ quote "atom" ^ " or consider adding a break")
+ of ([Pretty _], _) => error ("mixfix contains just one pretty element; either declare as " ^ quote atomK ^ " or consider adding a break")
| x => x;
fun parse_syntax_proto reader = OuterParse.$$$ "(" |-- (
@@ -212,18 +212,28 @@
-> OuterParse.token list ->
((string -> CodegenThingol.itype pretty_syntax option)
* (string -> CodegenThingol.iexpr pretty_syntax option)
- -> string
-> string list option
-> CodegenThingol.module -> unit)
* OuterParse.token list;
-fun abstract_serializer (target, nspgrp) (from_defs, from_module, validator)
- postprocess preprocess (tyco_syntax, const_syntax) name_root select module =
+fun pretty_of_prim target resolv (name, primdef) =
+ let
+ fun pr (CodegenThingol.Pretty p) = p
+ | pr (CodegenThingol.Name s) = resolv s;
+ in case AList.lookup (op = : string * string -> bool) primdef target
+ of NONE => error ("no primitive definition for " ^ quote name)
+ | SOME ps => (Pretty.block o map pr) ps
+ end;
+
+fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator)
+ postprocess preprocess (tyco_syntax, const_syntax) select module =
let
fun from_prim (name, prim) =
case AList.lookup (op = : string * string -> bool) prim target
of NONE => error ("no primitive definition for " ^ quote name)
| SOME p => p;
+ fun from_module' imps ((name_qual, name), defs) =
+ from_module imps ((name_qual, name), defs) |> postprocess name_qual;
in
module
|> debug 3 (fn _ => "selecting submodule...")
@@ -233,8 +243,8 @@
|> preprocess
|> debug 3 (fn _ => "serializing...")
|> serialize (from_defs (from_prim, (tyco_syntax, const_syntax)))
- from_module validator nspgrp name_root
- |> postprocess
+ from_module' validator nspgrp name_root
+ |> K ()
end;
fun abstract_validator keywords name =
@@ -255,13 +265,42 @@
|> (fn name' => if name = name' then NONE else SOME name')
end;
+fun write_file mkdir path p = (
+ if mkdir
+ then
+ File.mkdir (Path.dir path)
+ else ();
+ File.write path (Pretty.output p ^ "\n");
+ p
+ );
+
+fun mk_module_file postprocess_module ext path name p =
+ let
+ val prfx = Path.dir path;
+ val name' = case name
+ of "" => Path.base path
+ | _ => (Path.ext ext o Path.unpack o implode o separate "/" o NameSpace.unpack) name;
+ in
+ p
+ |> write_file true (Path.append prfx name')
+ |> postprocess_module name
+ end;
+
fun parse_single_file serializer =
- OuterParse.name
- >> (fn path => serializer (fn p => File.write (Path.unpack path) (Pretty.output p ^ "\n")));
+ OuterParse.path
+ >> (fn path => serializer
+ (fn "" => write_file false path #> K NONE
+ | _ => SOME));
+
+fun parse_multi_file postprocess_module ext serializer =
+ OuterParse.path
+ >> (fn path => (serializer o mk_module_file postprocess_module ext) path);
fun parse_internal serializer =
OuterParse.name
- >> (fn "-" => serializer (fn p => use_text Context.ml_output false (Pretty.output p))
+ >> (fn "-" => serializer
+ (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
+ | _ => SOME)
| _ => Scan.fail ());
@@ -270,7 +309,7 @@
fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) =
let
fun dest_cons (IApp (IApp (IConst (c, _), e1), e2)) =
- if (writeln (c ^ " - " ^ thingol_cons); c = thingol_cons)
+ if c = thingol_cons
then SOME (e1, e2)
else NONE
| dest_cons _ = NONE;
@@ -282,7 +321,7 @@
];
fun pretty_compact fxy pr [e1, e2] =
case unfoldr dest_cons e2
- of (es, IConst (c, _)) => (writeln (string_of_int (length es));
+ of (es, IConst (c, _)) =>
if c = thingol_nil
then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es))
else pretty_default fxy pr e1 e2)
@@ -553,11 +592,11 @@
NONE
| ml_from_def (name, Classinst _) =
error ("can't serialize instance declaration " ^ quote name ^ " to ML")
- in (writeln ("ML defs " ^ (commas o map fst) defs); case defs
+ in case defs
of (_, Fun _)::_ => ml_from_funs defs
| (_, Datatypecons _)::_ => ml_from_datatypes defs
| (_, Datatype _)::_ => ml_from_datatypes defs
- | [def] => ml_from_def def)
+ | [def] => ml_from_def def
end;
in
@@ -567,7 +606,7 @@
val reserved_ml = ThmDatabase.ml_reserved @ [
"bool", "int", "list", "true", "false"
];
- fun ml_from_module _ (name, ps) =
+ fun ml_from_module _ ((_, name), ps) =
Pretty.chunks ([
str ("structure " ^ name ^ " = "),
str "struct",
@@ -585,7 +624,7 @@
false;
fun is_cons c = has_nsp c nsp_dtcon;
val serializer = abstract_serializer (target, nspgrp)
- (ml_from_defs (is_cons, needs_type), ml_from_module, abstract_validator reserved_ml);
+ "ROOT" (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
@@ -605,9 +644,17 @@
|> eta_expand_poly
|> debug 3 (fn _ => "eliminating classes...")
|> eliminate_classes;
+ val parse_multi =
+ OuterParse.name
+ #-> (fn "dir" =>
+ parse_multi_file
+ (K o SOME o str o suffix ";" o prefix "val _ = use "
+ o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer
+ | _ => Scan.fail ());
in
- (parse_single_file serializer
- || parse_internal serializer)
+ (parse_multi
+ || parse_internal serializer
+ || parse_single_file serializer)
>> (fn seri => fn (tyco_syntax, const_syntax) => seri
(preprocess const_syntax) (tyco_syntax, const_syntax))
end;
@@ -749,22 +796,24 @@
[str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
[str ("in "), hs_from_expr NOBR body] |> Pretty.block
] end
- | hs_from_expr fxy (ICase (e, c::cs)) =
+ | hs_from_expr fxy (ICase (e, cs)) =
let
- fun mk_clause definer (p, e) =
+ fun mk_clause (p, e) =
Pretty.block [
- str definer,
hs_from_pat NOBR p,
str " ->",
Pretty.brk 1,
hs_from_expr NOBR e
]
- in brackify fxy (
- str "case"
- :: hs_from_expr NOBR e
- :: mk_clause "of " c
- :: map (mk_clause "| ") cs
- ) end
+ in Pretty.block [
+ str "case",
+ Pretty.brk 1,
+ hs_from_expr NOBR e,
+ Pretty.brk 1,
+ str "of",
+ Pretty.fbrk,
+ (Pretty.chunks o map mk_clause) cs
+ ] end
| hs_from_expr fxy (IInst (e, _)) =
hs_from_expr fxy e
| hs_from_expr fxy (IDictE _) =
@@ -883,16 +932,16 @@
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 [
- str ("module " ^ (upper_first name) ^ " where"),
- Pretty.fbrk,
- Pretty.fbrk,
+ fun hs_from_module imps ((_, name), ps) =
+ (Pretty.block o Pretty.fbreaks) (
+ str ("module " ^ (upper_first name) ^ " where")
+ :: map (str o prefix "import ") imps @ [
+ str "",
Pretty.chunks (separate (str "") ps)
- ];
+ ]);
fun is_cons c = has_nsp c nsp_dtcon;
val serializer = abstract_serializer (target, nspgrp)
- (hs_from_defs is_cons, hs_from_module, abstract_validator reserved_hs);
+ "Main" (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)
@@ -903,7 +952,7 @@
|> debug 3 (fn _ => "eta-expanding...")
|> eta_expand (eta_expander const_syntax);
in
- parse_single_file serializer
+ parse_multi_file ((K o K) NONE) "hs" serializer
>> (fn seri => fn (tyco_syntax, const_syntax) => seri
(preprocess const_syntax) (tyco_syntax, const_syntax))
end;
--- a/src/Pure/Tools/codegen_thingol.ML Mon Jan 30 08:19:30 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Mon Jan 30 08:20:06 2006 +0100
@@ -46,15 +46,28 @@
val vars_of_ipats: ipat list -> string list;
val vars_of_iexprs: iexpr list -> string list;
+ val `%% : string * itype list -> itype;
+ val `-> : itype * itype -> itype;
+ val `--> : itype list * itype -> itype;
+ val `$ : iexpr * iexpr -> iexpr;
+ val `$$ : iexpr * iexpr list -> iexpr;
+ val `|-> : (vname * itype) * iexpr -> iexpr;
+ val `|--> : (vname * itype) list * iexpr -> iexpr;
+
type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype);
+ datatype prim =
+ Pretty of Pretty.T
+ | Name of string;
datatype def =
Undef
| Prim of (string * Pretty.T option) list
| Fun of funn
| Typesyn of (vname * string list) list * itype
- | Datatype of ((vname * string list) list * (string * itype list) list) * string list
+ | Datatype of ((vname * string list) list * (string * itype list) list)
+ * string list
| Datatypecons of string
- | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list
+ | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list))
+ * string list
| Classmember of class
| Classinst of (class * (string * (vname * sort) list)) * (string * funn) list;
type module;
@@ -88,25 +101,12 @@
val serialize:
((string -> string) -> (string * def) list -> 'a option)
- -> (string list -> string * 'a list -> 'a)
+ -> (string list -> (string * string) * 'a list -> 'a option)
-> (string -> string option)
- -> string list list -> string -> module -> 'a;
+ -> string list list -> string -> module -> 'a option;
end;
-signature CODEGEN_THINGOL_OP =
-sig
- include CODEGEN_THINGOL;
- val `%% : string * itype list -> itype;
- val `-> : itype * itype -> itype;
- val `--> : itype list * itype -> itype;
- val `$ : iexpr * iexpr -> iexpr;
- val `$$ : iexpr * iexpr list -> iexpr;
- val `|-> : (vname * itype) * iexpr -> iexpr;
- val `|--> : (vname * itype) list * iexpr -> iexpr;
-end;
-
-
-structure CodegenThingolOp: CODEGEN_THINGOL_OP =
+structure CodegenThingol: CODEGEN_THINGOL =
struct
(** auxiliary **)
@@ -368,7 +368,8 @@
if ty2 = itype_of_iexpr e2
then ty'
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)
+ ^ ", " ^ (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)) = itype_of_iexpr e
| itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
@@ -451,14 +452,20 @@
type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype);
+datatype prim =
+ Pretty of Pretty.T
+ | Name of string;
+
datatype def =
Undef
| Prim of (string * Pretty.T option) list
| Fun of funn
| Typesyn of (vname * string list) list * itype
- | Datatype of ((vname * string list) list * (string * itype list) list) * string list
+ | Datatype of ((vname * string list) list * (string * itype list) list)
+ * string list
| Datatypecons of string
- | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list
+ | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list))
+ * string list
| Classmember of class
| Classinst of (class * (string * (vname * sort) list)) * (string * funn) list;
@@ -500,8 +507,9 @@
Pretty.block [
Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
Pretty.str " |=> ",
- Pretty.enum " |" "" ""
- (map (fn (c, tys) => (Pretty.block o Pretty.breaks) (Pretty.str c :: map pretty_itype tys)) cs),
+ Pretty.gen_list " |" "" ""
+ (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
+ (Pretty.str c :: map pretty_itype tys)) cs),
Pretty.str ", instances ",
Pretty.enum "," "[" "]" (map Pretty.str insts)
]
@@ -512,8 +520,9 @@
Pretty.str ("class var " ^ v ^ "extending "),
Pretty.enum "," "[" "]" (map Pretty.str supcls),
Pretty.str " with ",
- Pretty.enum "," "[" "]"
- (map (fn (m, (_, ty)) => Pretty.block [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
+ Pretty.gen_list "," "[" "]"
+ (map (fn (m, (_, ty)) => Pretty.block
+ [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
Pretty.str " instances ",
Pretty.enum "," "[" "]" (map Pretty.str insts)
]
@@ -529,7 +538,8 @@
Pretty.str ", (",
Pretty.str tyco,
Pretty.str ", ",
- Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o map Pretty.str o snd) arity),
+ Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o
+ map Pretty.str o snd) arity),
Pretty.str "))"
];
@@ -562,7 +572,9 @@
:: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
@ map (fn s => Pretty.str ("<-- " ^ s)) preds
@ map (fn s => Pretty.str ("--> " ^ s)) succs
- @ (the_list oo Option.mapPartial) ((fn Module modl' => SOME (pretty_deps modl') | _ => NONE) o Graph.get_node modl) (SOME key)
+ @ (the_list oo Option.mapPartial)
+ ((fn Module modl' => SOME (pretty_deps modl')
+ | _ => NONE) o Graph.get_node modl) (SOME key)
)
end
in
@@ -673,10 +685,12 @@
|> Graph.new_node (base, (Def o Prim) [(target, SOME primdef)])
| SOME (Def (Prim prim)) =>
if AList.defined (op =) prim target
- then error ("already primitive definition (" ^ target ^ ") present for " ^ name)
+ then error ("already primitive definition (" ^ target
+ ^ ") present for " ^ name)
else
module
- |> Graph.map_node base ((K o Def o Prim) (AList.update (op =) (target, SOME primdef) prim))
+ |> Graph.map_node base ((K o Def o Prim) (AList.update (op =)
+ (target, SOME primdef) prim))
| _ => error ("already non-primitive definition present for " ^ name))
| add (m::ms) module =
module
@@ -697,8 +711,9 @@
|> Graph.new_node (base, (Def o Prim) [(target, NONE)])
| SOME (Def (Prim prim)) =>
module
- |> Graph.map_node base ((K o Def o Prim) (AList.default (op =) (target, NONE) prim))
- | _ => error ("already non-primitive definition present for " ^ name))
+ |> Graph.map_node base ((K o Def o Prim) (AList.default (op =)
+ (target, NONE) prim))
+ | _ => module)
| ensure (m::ms) module =
module
|> Graph.default_node (m, Module empty_module)
@@ -772,19 +787,21 @@
|> Module;
in
Module modl
- |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], [])))
+ |> select (fold (mk_ipath o dest_name)
+ (filter NameSpace.is_qualified names) (PN ([], [])))
|> dest_modl
end;
-fun imports_of modl name_root name =
+fun imports_of modl name =
let
fun imports prfx [] modl =
[]
| imports prfx (m::ms) modl =
map (cons m) (imports (prfx @ [m]) ms ((dest_modl oo Graph.get_node) modl m))
- @ map single (Graph.imm_preds modl m);
+ @ map single (Graph.imm_succs modl m);
in
- map (cons name_root) (imports [] name modl)
+ modl
+ |> imports [] name
|> map NameSpace.pack
end;
@@ -794,7 +811,8 @@
val modn = (fst o dest_name) name
in
fn NONE => SOME modn
- | SOME mod' => if modn = mod' then SOME modn else error "inconsistent name prefix for simultanous names"
+ | SOME mod' => if modn = mod' then SOME modn
+ else error "inconsistent name prefix for simultanous names"
end
) names NONE;
@@ -804,7 +822,8 @@
val l = length pats
in
fn NONE => SOME l
- | SOME l' => if l = l' then SOME l else error "function definition with different number of arguments"
+ | SOME l' => if l = l' then SOME l
+ else error "function definition with different number of arguments"
end
) eqs NONE; eqs);
@@ -925,8 +944,8 @@
#> add_def (name, Undef)
#> add_dp dep
#> debug 9 (fn _ => "creating node " ^ quote name)
- #> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name)
- name defgens
+ #> select_generator (fn gname => "trying code generator "
+ ^ gname ^ " for definition of " ^ quote name) name defgens
#> debug 9 (fn _ => "checking creation of node " ^ quote name)
#> check_fail msg'
#-> (fn def => prep_def def)
@@ -1229,12 +1248,15 @@
fun resolver modl name =
if NameSpace.is_qualified name then
let
- val _ = debug 12 (fn name' => "resolving " ^ quote name ^ " in " ^ (quote o NameSpace.pack) modl) ();
- val modl' = if null modl then [] else (NameSpace.unpack o the o Symtab.lookup tab o NameSpace.pack) modl;
+ val _ = debug 12 (fn name' => "resolving " ^ quote name ^ " in "
+ ^ (quote o NameSpace.pack) modl) ();
+ val modl' = if null modl then [] else
+ (NameSpace.unpack o the o Symtab.lookup tab o NameSpace.pack) modl;
val name' = (NameSpace.unpack o the o Symtab.lookup tab) name
in
(NameSpace.pack o snd o snd o get_prefix (op =)) (modl', name')
- |> debug 12 (fn name' => "resolving " ^ quote name ^ " to " ^ quote name' ^ " in " ^ (quote o NameSpace.pack) modl)
+ |> debug 12 (fn name' => "resolving " ^ quote name ^ " to "
+ ^ quote name' ^ " in " ^ (quote o NameSpace.pack) modl)
end
else name
in resolver end;
@@ -1247,28 +1269,21 @@
val resolvtab = mk_resolvtab nsp_conn validate module;
val resolver = mk_resolv resolvtab;
fun mk_name prfx name =
- resolver prfx (NameSpace.pack (prfx @ [name]));
+ let
+ val name_qual = NameSpace.pack (prfx @ [name])
+ in (name_qual, resolver prfx name_qual) end;
fun mk_contents prfx module =
- List.mapPartial (seri prfx) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) 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_module (map (resolver []) (imports_of module (prfx @ [name])))
+ (mk_name prfx name, mk_contents (prfx @ [name]) modl)
| seri prfx ds =
- ds
- |> map (fn (name, Def def) => (mk_name prfx name, def))
- |> seri_defs (resolver prfx)
+ seri_defs (resolver prfx)
+ (map (fn (name, Def def) => (snd (mk_name prfx name), def)) ds)
in
- seri_module [] (name_root, (mk_contents [] module))
+ seri_module (map (resolver []) (Graph.strong_conn module |> List.concat |> rev))
+ (("", name_root), (mk_contents [] module))
end;
end; (* struct *)
-
-
-structure CodegenThingol : CODEGEN_THINGOL =
-struct
-
-open CodegenThingolOp;
-
-end; (* struct *)