# HG changeset patch # User haftmann # Date 1138605606 -3600 # Node ID 92ef83e5eaea28521cf605aab6b6812c27846d18 # Parent 05a16861d3a5d00db1bb4bdd8159e80e4c7712f2 various improvements diff -r 05a16861d3a5 -r 92ef83e5eaea src/Pure/Tools/codegen_package.ML --- 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.$$$ "\\" || P.$$$ "=>") |-- (P.list1 P.name)) - -- (Scan.optional ((P.$$$ "\\" || 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 ["\\", "=>", 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 *) diff -r 05a16861d3a5 -r 92ef83e5eaea src/Pure/Tools/codegen_serializer.ML --- 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; diff -r 05a16861d3a5 -r 92ef83e5eaea src/Pure/Tools/codegen_thingol.ML --- 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 *)