--- a/src/HOL/Tools/datatype_codegen.ML Wed Aug 16 16:44:41 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Aug 17 09:24:47 2006 +0200
@@ -9,7 +9,7 @@
sig
val get_datatype_spec_thms: theory -> string
-> (((string * sort) list * (string * typ list) list) * tactic) option
- val get_all_datatype_cons: theory -> (string * string) list
+ val datatype_tac: theory -> string -> tactic
val dest_case_expr: theory -> term
-> ((string * typ) list * ((term * typ) * (term * term) list)) option
val add_datatype_case_const: string -> theory -> theory
@@ -21,7 +21,7 @@
val get_datatype_arities: theory -> string list -> sort
-> (string * (((string * sort list) * sort) * term list)) list option
val prove_arities: (thm list -> tactic) -> string list -> sort
- -> (((string * sort list) * sort) list -> (string * term list) list
+ -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
-> ((bstring * attribute list) * term) list) -> theory -> theory
val setup: theory -> theory
end;
@@ -392,7 +392,7 @@
in
thy
|> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
- arities ("", []) (f arities css)
+ arities ("", []) (f thy arities css)
end;
fun dtyp_of_case_const thy c =
@@ -444,12 +444,6 @@
SOME (vs_cos, datatype_tac thy dtco)
| NONE => NONE;
-fun get_all_datatype_cons thy =
- Symtab.fold (fn (dtco, _) => fold
- (fn (co, _) => cons (co, dtco))
- ((snd o the oo DatatypePackage.get_datatype_spec) thy dtco))
- (DatatypePackage.get_datatypes thy) [];
-
fun add_datatype_case_const dtco thy =
let
val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
--- a/src/Pure/Tools/codegen_consts.ML Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_consts.ML Thu Aug 17 09:24:47 2006 +0200
@@ -14,10 +14,13 @@
structure Consttab: TABLE
val typinst_of_typ: theory -> string * typ -> const
val typ_of_typinst: theory -> const -> string * typ
- val find_norminst: theory -> const -> (string (*theory name*) * typ list) option
+ val find_def: theory -> const
+ -> ((string (*theory name*) * string (*definition name*)) * typ list) option
+ val sortinsts: theory -> typ * typ -> (typ * sort) list
val norminst_of_typ: theory -> string * typ -> const
val class_of_classop: theory -> const -> class option
val insts_of_classop: theory -> const -> const list
+ val typ_of_classop: theory -> const -> typ
val read_const: theory -> string -> const
val read_const_typ: theory -> string -> string * typ
val string_of_const: theory -> const -> string
@@ -44,54 +47,98 @@
(* type instantiations and overloading *)
fun typinst_of_typ thy (c_ty as (c, ty)) =
- (*FIXME: better shift to defs.ML?*)
(c, Consts.typargs (Sign.consts_of thy) c_ty);
fun typ_of_typinst thy (c_tys as (c, tys)) =
- (*FIXME: better shift to defs.ML?*)
(c, Consts.instance (Sign.consts_of thy) c_tys);
-fun find_norminst thy (c, tys) =
- (*FIXME: better shift to defs.ML?*)
+fun find_def thy (c, tys) =
let
val specs = Defs.specifications_of (Theory.defs_of thy) c;
+ val typ_instance = case AxClass.class_of_param thy c
+ of SOME _ => let
+ fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2
+ | instance_tycos (_ , TVar _) = true
+ | instance_tycos ty_ty = Sign.typ_instance thy ty_ty;
+ in instance_tycos end
+ | NONE => Sign.typ_instance thy
in
- get_first (fn (_, { lhs, module, ... }) => if forall (Sign.typ_instance thy)
- (tys ~~ lhs) then SOME (module, lhs) else NONE) specs
+ get_first (fn (_, { is_def, thyname, name, lhs, ... }) => if is_def
+ andalso forall typ_instance (tys ~~ lhs)
+ then SOME ((thyname, name), lhs) else NONE) specs
end;
+fun sortinsts thy (ty, ty_decl) =
+ Vartab.empty
+ |> Sign.typ_match thy (ty_decl, ty)
+ |> Vartab.dest
+ |> map (fn (_, (sort, ty)) => (ty, sort));
+
+fun mk_classop_typinst thy (c, tyco) =
+ (c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*)))
+ (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]);
+
fun norminst_of_typ thy (c, ty) =
let
fun disciplined _ [(Type (tyco, _))] =
- [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy))
- (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]
+ mk_classop_typinst thy (c, tyco)
| disciplined sort _ =
- [TVar (("'a", 0), sort)];
+ (c, [TVar (("'a", 0), sort)]);
fun ad_hoc c tys =
- case find_norminst thy (c, tys)
+ case find_def thy (c, tys)
of SOME (_, tys) => (c, tys)
| NONE => typinst_of_typ thy (c, Sign.the_const_type thy c);
val tyinsts = Consts.typargs (Sign.consts_of thy) (c, ty);
- in if c = "op =" then (c, disciplined (Sign.defaultS thy) tyinsts)
+ in if c = "op =" then disciplined (Sign.defaultS thy) tyinsts
(*the distinction on op = will finally disappear!*)
else case AxClass.class_of_param thy c
- of SOME class => (c, disciplined [class] tyinsts)
+ of SOME class => disciplined [class] tyinsts
| _ => ad_hoc c tyinsts
end;
-fun class_of_classop thy (c_tys as (c, _)) =
- case AxClass.class_of_param thy c
- of NONE => NONE
- | SOME class => if is_some (find_norminst thy c_tys)
- then NONE
- else SOME class;
+fun class_of_classop thy (c, [TVar _]) =
+ AxClass.class_of_param thy c
+ | class_of_classop thy (c, [TFree _]) =
+ AxClass.class_of_param thy c
+ | class_of_classop thy (c, _) = NONE;
fun insts_of_classop thy (c_tys as (c, tys)) =
case AxClass.class_of_param thy c
of NONE => [c_tys]
- | SOME _ =>
- map (fn (_, { lhs, ... }) => (c, lhs))
- (Defs.specifications_of (Theory.defs_of thy) c);
+ | SOME class => let
+ val cs = maps (AxClass.params_of thy)
+ (Sorts.all_super_classes (Sign.classes_of thy) class)
+ fun add_tyco (tyco, classes) =
+ if member (op = o apsnd fst) classes class
+ then cons tyco else I;
+ val tycos =
+ Symtab.fold add_tyco
+ ((#arities o Sorts.rep_algebra o Sign.classes_of) thy) [];
+ in maps (fn c => map (fn tyco => mk_classop_typinst thy (c, tyco)) tycos) cs end;
+
+fun typ_of_classop thy (c, [TVar _]) =
+ let
+ val class = (the o AxClass.class_of_param thy) c;
+ val (v, cs) = ClassPackage.the_consts_sign thy class
+ in
+ (Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
+ ((the o AList.lookup (op =) cs) c)
+ end
+ | typ_of_classop thy (c, [TFree _]) =
+ let
+ val class = (the o AxClass.class_of_param thy) c;
+ val (v, cs) = ClassPackage.the_consts_sign thy class
+ in
+ (Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
+ ((the o AList.lookup (op =) cs) c)
+ end
+ | typ_of_classop thy (c, [Type (tyco, _)]) =
+ let
+ val class = (the o AxClass.class_of_param thy) c;
+ val (_, cs) = ClassPackage.the_inst_sign thy (class, tyco);
+ in
+ Logic.varifyT ((the o AList.lookup (op =) cs) c)
+ end;
(* reading constants as terms *)
@@ -101,7 +148,7 @@
val t = Sign.read_term thy raw_t
in case try dest_Const t
of SOME c_ty => c_ty
- | NONE => error ("not a constant: " ^ Sign.string_of_term thy t)
+ | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
end;
fun read_const thy =
--- a/src/Pure/Tools/codegen_names.ML Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_names.ML Thu Aug 17 09:24:47 2006 +0200
@@ -140,7 +140,7 @@
val tab = (snd o get_tabs) names;
in case Symtab.lookup tab name
of SOME x => x
- | NONE => error ("no such " ^ errname ^ ": " ^ quote name)
+ | NONE => error ("No such " ^ errname ^ ": " ^ quote name)
end;
@@ -213,10 +213,11 @@
val purify_lower = explode #> nth_map 0 Symbol.to_ascii_lower #> implode;
val purify_upper = explode #> nth_map 0 Symbol.to_ascii_upper #> implode;
-fun purify_var v =
- if nth (explode v) 0 = "'"
- then (unprefix "'" #> purify_name #> purify_lower #> prefix "'") v
- else (purify_name #> purify_lower) v;
+fun purify_var "" = "x"
+ | purify_var v =
+ if nth (explode v) 0 = "'"
+ then (unprefix "'" #> purify_name #> purify_lower #> prefix "'") v
+ else (purify_name #> purify_lower) v;
val purify_idf = purify_op #> purify_name;
val purify_prefix = map (purify_idf #> purify_upper);
@@ -234,16 +235,16 @@
val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
then ()
else
- error ("name violates naming conventions: " ^ quote name
+ error ("Name violates naming conventions: " ^ quote name
^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
val names_ref = CodegenNamesData.get thy;
val (Names names) = ! names_ref;
val (tycotab, tycorev) = #tyco names;
val _ = if Symtab.defined tycotab tyco
- then error ("type constructor already named: " ^ quote tyco)
+ then error ("Type constructor already named: " ^ quote tyco)
else ();
val _ = if Symtab.defined tycorev name
- then error ("name already given to type constructor: " ^ quote name)
+ then error ("Name already given to type constructor: " ^ quote name)
else ();
val _ = names_ref := map_tyco (K (Symtab.update_new (tyco, name) tycotab,
Symtab.update_new (name, tyco) tycorev)) (Names names);
@@ -260,17 +261,17 @@
val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
then ()
else
- error ("name violates naming conventions: " ^ quote name
+ error ("Name violates naming conventions: " ^ quote name
^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
val names_ref = CodegenNamesData.get thy;
val (Names names) = ! names_ref;
val (const, constrev) = #const names;
val c_tys as (c, _) = CodegenConsts.norminst_of_typ thy c_ty;
val _ = if Consttab.defined const c_tys
- then error ("constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))
+ then error ("Constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))
else ();
val _ = if Symtab.defined constrev name
- then error ("name already given to constant: " ^ quote name)
+ then error ("Name already given to constant: " ^ quote name)
else ();
val _ = names_ref := map_const (K (Consttab.update_new (c_tys, name) const,
Symtab.update_new (name, c_tys) constrev)) (Names names);
@@ -293,15 +294,16 @@
NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
fun force_thyname thy ("op =", [Type (tyco, _)]) =
+ (*will disappear finally*)
SOME (thyname_of_tyco thy tyco)
| force_thyname thy (c, tys) =
- case CodegenConsts.find_norminst thy (c, tys)
- of SOME (module, tys) => (case AxClass.class_of_param thy c
- of SOME class => (case tys
- of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
- | _ => SOME module)
- | NONE => SOME module)
- | NONE => NONE;
+ case AxClass.class_of_param thy c
+ of SOME class => (case tys
+ of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
+ | _ => NONE)
+ | NONE => (case CodegenConsts.find_def thy (c, tys)
+ of SOME ((thyname, _), tys) => SOME thyname
+ | NONE => NONE);
fun const_policy thy (c, tys) =
case force_thyname thy (c, tys)
@@ -331,20 +333,6 @@
fun const_rev thy = rev thy #const "constant" #> CodegenConsts.typ_of_typinst thy;
-(* reading constants as terms *)
-
-fun read_const_typ thy raw_t =
- let
- val t = Sign.read_term thy raw_t
- in case try dest_Const t
- of SOME c_ty => c_ty
- | NONE => error ("not a constant: " ^ Sign.string_of_term thy t)
- end;
-
-fun read_const thy =
- const thy o read_const_typ thy;
-
-
(* outer syntax *)
local
@@ -353,7 +341,7 @@
and K = OuterKeyword
fun const_force_e (raw_c, name) thy =
- const_force (read_const_typ thy raw_c, name) thy;
+ const_force (CodegenConsts.read_const_typ thy raw_c, name) thy;
fun tyco_force_e (raw_tyco, name) thy =
tyco_force (Sign.intern_type thy raw_tyco, name) thy;
--- a/src/Pure/Tools/codegen_package.ML Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Thu Aug 17 09:24:47 2006 +0200
@@ -9,7 +9,8 @@
signature CODEGEN_PACKAGE =
sig
val codegen_term: term -> theory -> CodegenThingol.iterm * theory;
- val eval_term: (string (*reference name!*) * 'a ref) * term -> theory -> 'a * theory;
+ val eval_term: (string (*reference name!*) * 'a ref) * term
+ -> theory -> 'a * theory;
val is_dtcon: string -> bool;
val consts_of_idfs: theory -> string list -> (string * typ) list;
val idfs_of_consts: theory -> (string * typ) list -> string list;
@@ -93,14 +94,16 @@
#ml CodegenSerializer.serializers
|> apsnd (fn seri => seri
nsp_dtcon
- [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
+ [[nsp_module], [nsp_class, nsp_tyco],
+ [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
)
)
|> Symtab.update (
#haskell CodegenSerializer.serializers
|> apsnd (fn seri => seri
(nsp_dtcon, [nsp_module, nsp_class, nsp_tyco, nsp_dtcon])
- [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_mem], [nsp_dtcon], [nsp_inst], [nsp_instmem]]
+ [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const, nsp_mem],
+ [nsp_dtcon], [nsp_inst], [nsp_instmem]]
)
)
);
@@ -108,11 +111,6 @@
(* theory data for code generator *)
-fun merge_opt _ (x1, NONE) = x1
- | merge_opt _ (NONE, x2) = x2
- | merge_opt eq (SOME x1, SOME x2) =
- if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
-
type appgens = (int * (appgen * stamp)) Symtab.table
fun merge_appgens (x : appgens * appgens) =
@@ -260,7 +258,8 @@
false
| check_strict thy f x ((_, SOME targets), _) =
exists (
- is_none o (fn tab => Symtab.lookup tab x) o f o the o (Symtab.lookup ((#target_data o CodegenData.get) thy))
+ is_none o (fn tab => Symtab.lookup tab x) o f o the
+ o (Symtab.lookup ((#target_data o CodegenData.get) thy))
) targets
| check_strict thy f x ((true, _), _) =
true;
@@ -281,8 +280,7 @@
Vartab.empty
|> Sign.typ_match thy (typ_decl, typ_ctxt)
|> Vartab.dest
- |> map_filter (fn (_, ([], _)) => NONE
- | (_, (sort, ty)) => SOME (ClassPackage.sortlookup thy (ty, sort)))
+ |> map (fn (_, (sort, ty)) => ClassPackage.sortlookup thy (ty, sort))
|> filter_out null
end;
@@ -306,7 +304,7 @@
end
| _ =>
trns
- |> fail ("no class definition found for " ^ quote cls);
+ |> fail ("No class definition found for " ^ quote cls);
val cls' = idf_of_class thy cls;
in
trns
@@ -333,14 +331,15 @@
(vars, cos)))
| NONE =>
trns
- |> fail ("no datatype found for " ^ quote dtco))
+ |> fail ("No datatype found for " ^ quote dtco))
| NONE =>
trns
- |> fail ("not a type constructor: " ^ quote dtco)
+ |> fail ("Not a type constructor: " ^ quote dtco)
in
trns
|> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
- |> ensure_def (defgen_datatype thy tabs) strict ("generating type constructor " ^ quote tyco) tyco'
+ |> ensure_def (defgen_datatype thy tabs) strict
+ ("generating type constructor " ^ quote tyco) tyco'
|> pair tyco'
end
and exprgen_tyvar_sort thy tabs (v, sort) trns =
@@ -348,7 +347,7 @@
|> fold_map (ensure_def_class thy tabs) (ClassPackage.operational_sort_of thy sort)
|-> (fn sort => pair (unprefix "'" v, sort))
and exprgen_type thy tabs (TVar _) trns =
- error "TVar encountered during code generation"
+ error "TVar encountered in typ during code generation"
| exprgen_type thy tabs (TFree v_s) trns =
trns
|> exprgen_tyvar_sort thy tabs v_s
@@ -386,9 +385,9 @@
(apfst strip_comb o Logic.dest_equals o Logic.legacy_unvarify 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
+ else error ("Illegal function equation for " ^ quote c
^ ", actually defining " ^ quote c')
- | _ => error ("illegal function equation for " ^ quote c)
+ | _ => error ("Illegal function equation for " ^ quote c)
end;
fun exprgen_eq (args, rhs) trns =
trns
@@ -396,7 +395,7 @@
||>> exprgen_term thy tabs rhs;
fun checkvars (args, rhs) =
if CodegenThingol.vars_distinct args then (args, rhs)
- else error ("repeated variables on left hand side of function")
+ else error ("Repeated variables on left hand side of function")
in
trns
|> message msg (fn trns => trns
@@ -404,7 +403,8 @@
|-> (fn eqs => pair (map checkvars eqs))
||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext
||>> exprgen_type thy tabs ty
- |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), map snd sortcontext)))
+ |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)),
+ map snd sortcontext)))
end
| [] => (NONE, trns)
and ensure_def_inst thy tabs (cls, tyco) trns =
@@ -414,11 +414,12 @@
of SOME (class, tyco) =>
let
val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
- val (_, memnames) = ClassPackage.the_consts_sign thy class;
+ val (_, members) = ClassPackage.the_consts_sign thy class;
val arity_typ = Type (tyco, (map TFree arity));
- val operational_arity = map_filter (fn (v, sort) => case ClassPackage.operational_sort_of thy sort
- of [] => NONE
- | sort => SOME (v, sort)) arity;
+ val operational_arity = map_filter (fn (v, sort) =>
+ case ClassPackage.operational_sort_of thy sort
+ of [] => NONE
+ | sort => SOME (v, sort)) arity;
fun mk_instmemname (m, ty) =
NameSpace.append (NameSpace.append ((NameSpace.drop_base o NameSpace.drop_base)
inst) nsp_instmem) (NameSpace.base (idf_of_const thy thmtab (m, ty)));
@@ -429,16 +430,8 @@
(ClassPackage.sortlookup thy (arity_typ, [supclass]));
fun gen_membr ((m0, ty0), (m, ty)) trns =
trns
- |> mk_fun thy tabs (m, ty)
- |-> (fn NONE => error ("could not derive definition for member "
- ^ quote m ^ " :: " ^ Sign.string_of_typ thy ty)
- | SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
- fold_map (exprgen_classlookup thy tabs)
- (ClassPackage.sortlookup thy (TFree sort_ctxt, sort)))
- (sorts ~~ operational_arity)
- #-> (fn lss =>
- pair (idf_of_const thy thmtab (m0, ty0),
- ((mk_instmemname (m0, ty0), funn), lss))));
+ |> ensure_def_const thy tabs (m0, ty0)
+ ||>> exprgen_term thy tabs (Const (m, ty));
in
trns
|> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls
@@ -447,12 +440,12 @@
||>> ensure_def_tyco thy tabs tyco
||>> fold_map (exprgen_tyvar_sort thy tabs) arity
||>> fold_map gen_suparity (ClassPackage.the_superclasses thy class)
- ||>> fold_map gen_membr (memnames ~~ memdefs)
+ ||>> fold_map gen_membr (members ~~ memdefs)
|-> (fn ((((class, tyco), arity), suparities), memdefs) =>
- succeed (Classinst (((class, (tyco, arity)), suparities), memdefs)))
+ succeed (Classinst ((class, (tyco, arity)), (suparities, memdefs))))
end
| _ =>
- trns |> fail ("no class instance found for " ^ quote inst);
+ trns |> fail ("No class instance found for " ^ quote inst);
val inst = idf_of_inst thy (cls, tyco);
in
trns
@@ -472,7 +465,8 @@
|-> (fn _ => succeed Bot)
| _ =>
trns
- |> fail ("not a datatype constructor: " ^ quote co);
+ |> fail ("Not a datatype constructor: "
+ ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty));
fun defgen_clsmem thy (tabs as (_, thmtab)) m trns =
case CodegenConsts.class_of_classop thy
((CodegenConsts.typinst_of_typ thy o the o const_of_idf thy) m)
@@ -482,13 +476,13 @@
|> ensure_def_class thy tabs class
|-> (fn _ => succeed Bot)
| _ =>
- trns |> fail ("no class found for " ^ quote m)
+ trns |> fail ("No class found for " ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))
fun defgen_funs thy (tabs as (_, thmtab)) c' trns =
trns
|> mk_fun thy tabs ((the o const_of_idf thy) c')
|-> (fn SOME (funn, _) => succeed (Fun funn)
- | NONE => fail ("no defining equations found for " ^
- (quote (c ^ " :: " ^ Sign.string_of_typ thy ty))))
+ | NONE => fail ("No defining equations found for "
+ ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)))
fun get_defgen tabs idf strict =
if (is_some oo dest_nsp) nsp_const idf
then defgen_funs thy tabs strict
@@ -496,13 +490,15 @@
then defgen_clsmem thy tabs strict
else if (is_some oo dest_nsp) nsp_dtcon idf
then defgen_datatypecons thy tabs strict
- else error ("illegal shallow name space for constant: " ^ quote idf);
+ else error ("Illegal shallow name space for constant: " ^ quote idf);
val idf = idf_of_const thy thmtab (c, ty);
val strict = check_strict thy #syntax_const idf tabs;
in
trns
- |> debug_msg (fn _ => "generating constant " ^ (quote (c ^ " :: " ^ Sign.string_of_typ thy ty)))
- |> ensure_def (get_defgen tabs idf) strict ("generating constant " ^ quote c) idf
+ |> debug_msg (fn _ => "generating constant "
+ ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))
+ |> ensure_def (get_defgen tabs idf) strict ("generating constant "
+ ^ CodegenConsts.string_of_const_typ thy (c, ty)) idf
|> pair idf
end
and exprgen_term thy tabs (Const (f, ty)) trns =
@@ -510,7 +506,7 @@
|> appgen thy tabs ((f, ty), [])
|-> (fn e => pair e)
| exprgen_term thy tabs (Var _) trns =
- error "Var encountered during code generation"
+ error "Var encountered in term during code generation"
| exprgen_term thy tabs (Free (v, ty)) trns =
trns
|> exprgen_type thy tabs ty
@@ -655,7 +651,7 @@
fun get_serializer target =
case Symtab.lookup (!serializers) target
of SOME seri => seri
- | NONE => Scan.fail_with (fn _ => "unknown code target language: " ^ quote target) ();
+ | NONE => Scan.fail_with (fn _ => "Unknown code target language: " ^ quote target) ();
fun map_module f =
map_codegen_data (fn (modl, gens, target_data) =>
@@ -712,6 +708,17 @@
fun eval_term (ref_spec, t) thy =
let
+ fun preprocess_term t =
+ let
+ val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
+ (* fake definition *)
+ val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
+ (Logic.mk_equals (x, t));
+ fun err () = error "preprocess_term: bad preprocessor"
+ in case map prop_of (CodegenTheorems.preprocess thy [eq])
+ of [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
+ | _ => err ()
+ end;
val target_data =
((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem], [nsp_eval]]
@@ -720,7 +727,7 @@
(Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data))
in
thy
- |> codegen_term t
+ |> codegen_term (preprocess_term t)
||>> `(#modl o CodegenData.get)
|-> (fn (t', modl) => `(fn _ => eval (ref_spec, t') modl))
end;
--- a/src/Pure/Tools/codegen_serializer.ML Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Thu Aug 17 09:24:47 2006 +0200
@@ -32,6 +32,7 @@
-> string list
-> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module
-> 'a;
+ val eval_verbose: bool ref;
val ml_fun_datatype: string
-> ((string -> CodegenThingol.itype pretty_syntax option)
* (string -> CodegenThingol.iterm pretty_syntax option))
@@ -113,9 +114,9 @@
| fillin (Quote q :: ms) args =
pr BR q :: fillin ms args
| fillin [] _ =
- error ("inconsistent mixfix: too many arguments")
+ error ("Inconsistent mixfix: too many arguments")
| fillin _ [] =
- error ("inconsistent mixfix: too less arguments");
+ error ("Inconsistent mixfix: too less arguments");
in gen_brackify (eval_fxy fxy_this fxy_ctxt) (fillin ms args) end;
@@ -164,7 +165,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 "
+ error ("Mixfix contains just one pretty element; either declare as "
^ quote atomK ^ " or consider adding a break")
| x => x;
@@ -187,7 +188,7 @@
fun mk fixity mfx ctxt =
let
val i = (length o List.filter is_arg) mfx;
- val _ = if i > no_args ctxt then error "too many arguments in codegen syntax" else ();
+ val _ = if i > no_args ctxt then error "Too many arguments in codegen syntax" else ();
in (((i, i), fillin_mixfix fixity mfx), ctxt) end;
in
parse_syntax_proto reader
@@ -272,10 +273,10 @@
fun check_eq (eq as (lhs, rhs)) =
if forall (CodegenThingol.is_pat is_cons) lhs
then SOME eq
- else (warning ("in function " ^ quote name ^ ", throwing away one "
+ else (warning ("In function " ^ quote name ^ ", throwing away one "
^ "non-executable function clause"); NONE)
in case map_filter check_eq eqs
- of [] => error ("in function " ^ quote name ^ ", no "
+ of [] => error ("In function " ^ quote name ^ ", no "
^ "executable function clauses found")
| eqs => (name, (eqs, ty))
end;
@@ -346,7 +347,7 @@
(Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'";
fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
fun maybe_unique _ _ = NONE;
- fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
+ fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
);
fun ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv =
@@ -420,7 +421,7 @@
of NONE => ml_from_tycoexpr fxy (tyco, tys)
| SOME ((i, k), pr) =>
if not (i <= length tys andalso length tys <= k)
- then error ("number of argument mismatch in customary serialization: "
+ then error ("Number of argument mismatch in customary serialization: "
^ (string_of_int o length) tys ^ " given, "
^ string_of_int i ^ " to " ^ string_of_int k
^ " expected")
@@ -508,7 +509,7 @@
@ [str ")"]
) end
| ml_from_expr _ e =
- error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
+ error ("Dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
and ml_mk_app f es =
if is_cons f andalso length es > 1 then
[(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
@@ -564,7 +565,7 @@
| check_args (_, ((pats, _)::_, (sortctxt, _))) (SOME definer) =
if mk_definer pats sortctxt = definer
then SOME definer
- else error ("mixing simultaneous vals and funs not implemented");
+ else error ("Mixing simultaneous vals and funs not implemented");
fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) =
let
val shift = if null eq_tl then I else
@@ -633,16 +634,16 @@
map_filter
(fn (name, CodegenThingol.Datatype info) => SOME (name, info)
| (name, CodegenThingol.Datatypecons _) => NONE
- | (name, def) => error ("datatype block containing illegal def: "
+ | (name, def) => error ("Datatype block containing illegal def: "
^ (Pretty.output o CodegenThingol.pretty_def) def));
fun filter_class defs =
case map_filter
(fn (name, CodegenThingol.Class info) => SOME (name, info)
| (name, CodegenThingol.Classmember _) => NONE
- | (name, def) => error ("class block containing illegal def: "
+ | (name, def) => error ("Class block containing illegal def: "
^ (Pretty.output o CodegenThingol.pretty_def) def)) defs
of [class] => class
- | _ => error ("class block without class: " ^ (commas o map (quote o fst)) defs)
+ | _ => error ("Class block without class: " ^ (commas o map (quote o fst)) defs)
fun ml_from_class (name, (supclasses, (v, membrs))) =
let
val w = (Char.toString o Char.toUpper o the o Char.fromString) v;
@@ -686,7 +687,7 @@
end
fun ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
(map (fn (vname, []) => () | _ =>
- error "can't serialize sort constrained type declaration to ML") vs;
+ error "Can't serialize sort constrained type declaration to ML") vs;
Pretty.block [
str "type ",
ml_from_tycoexpr NOBR (name, map (ITyVar o fst) vs),
@@ -696,7 +697,7 @@
str ";"
]
) |> SOME
- | ml_from_def (name, CodegenThingol.Classinst (((class, (tyco, arity)), suparities), memdefs)) =
+ | ml_from_def (name, CodegenThingol.Classinst ((class, (tyco, arity)), (suparities, memdefs))) =
let
val definer = if null arity then "val" else "fun"
fun from_supclass (supclass, ls) =
@@ -705,13 +706,12 @@
str "=",
ml_from_sortlookup NOBR ls
];
- fun from_memdef (m, ((m', def), lss)) =
- (ml_from_funs [(m', def)], (Pretty.block o Pretty.breaks) (
- ml_from_label m
- :: str "="
- :: (str o resolv) m'
- :: map (ml_from_sortlookup NOBR) lss
- ));
+ fun from_memdef (m, e) =
+ (Pretty.block o Pretty.breaks) [
+ ml_from_label m,
+ str "=",
+ ml_from_expr NOBR e
+ ];
fun mk_corp rhs =
(Pretty.block o Pretty.breaks) (
str definer
@@ -719,35 +719,16 @@
:: map ml_from_tyvar arity
@ [str "=", rhs]
);
- fun mk_memdefs supclassexprs [] =
- Pretty.enum "," "{" "};" (
- supclassexprs
- ) |> mk_corp
- | mk_memdefs supclassexprs memdefs =
- let
- val (defs, assigns) = (split_list o map from_memdef) memdefs;
- in
- Pretty.chunks [
- Pretty.block [
- str "local",
- Pretty.fbrk,
- Pretty.chunks defs
- ],
- Pretty.block [str "in", Pretty.brk 1,
- (mk_corp o Pretty.block o Pretty.breaks) [
- Pretty.enum "," "{" "}" (supclassexprs @ assigns),
- str ":",
- ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
- ]
- ],
- str "end; (* instance *)"
- ]
- end;
+ fun mk_memdefs supclassexprs memdefs =
+ (mk_corp o Pretty.block o Pretty.breaks) [
+ Pretty.enum "," "{" "}" (supclassexprs @ memdefs),
+ str ":",
+ ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+ ];
in
- mk_memdefs (map from_supclass suparities) memdefs |> SOME
+ mk_memdefs (map from_supclass suparities) (map from_memdef memdefs) |> SOME
end
- | ml_from_def (name, CodegenThingol.Classinstmember) = NONE
- | ml_from_def (name, def) = error ("illegal definition for " ^ quote name ^ ": " ^
+ | ml_from_def (name, def) = error ("Illegal definition for " ^ quote name ^ ": " ^
(Pretty.output o CodegenThingol.pretty_def) def);
in case defs
of (_, CodegenThingol.Fun _)::_ => ((*writeln "FUN";*) (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs)
@@ -756,7 +737,7 @@
| (_, CodegenThingol.Class _)::_ => (SOME o ml_from_class o filter_class) defs
| (_, CodegenThingol.Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
| [def] => ml_from_def def
- | defs => error ("illegal mutual dependencies: " ^ (commas o map fst) defs)
+ | defs => error ("Illegal mutual dependencies: " ^ (commas o map fst) defs)
end;
fun ml_annotators nsp_dtcon =
@@ -799,16 +780,18 @@
|| parse_single_file serializer
end;
+val eval_verbose = ref false;
+
fun eval_term nsp_eval nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl =
let
val (val_name, modl') = CodegenThingol.add_eval_def (nsp_eval, e) modl;
val struct_name = "EVAL";
val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
- (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
+ (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (Pretty.output p); NONE))
| _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
val _ = serializer modl';
val val_name_struct = NameSpace.append struct_name val_name;
- val _ = use_text Context.ml_output false ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())");
+ val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())");
val value = ! reff;
in value end;
@@ -860,7 +843,7 @@
hs_from_tycoexpr fxy (resolv tyco, tys)
| SOME ((i, k), pr) =>
if not (i <= length tys andalso length tys <= k)
- then error ("number of argument mismatch in customary serialization: "
+ then error ("Number of argument mismatch in customary serialization: "
^ (string_of_int o length) tys ^ " given, "
^ string_of_int i ^ " to " ^ string_of_int k
^ " expected")
@@ -1022,7 +1005,7 @@
end
| hs_from_def (_, CodegenThingol.Classmember _) =
NONE
- | hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) =
+ | hs_from_def (_, CodegenThingol.Classinst ((clsname, (tyco, arity)), (_, memdefs))) =
Pretty.block [
str "instance ",
hs_from_sctxt arity,
@@ -1030,10 +1013,14 @@
hs_from_type BR (tyco `%% map (ITyVar o fst) arity),
str " where",
Pretty.fbrk,
- Pretty.chunks (map (fn (m, ((_, (eqs, ty)), _)) => hs_from_funeqs (m, (eqs, ty))) memdefs)
+ Pretty.chunks (map (fn (m, e) =>
+ (Pretty.block o Pretty.breaks) [
+ (str o NameSpace.base o resolv) m,
+ str "=",
+ hs_from_expr NOBR e
+ ]
+ ) memdefs)
] |> SOME
- | hs_from_def (_, CodegenThingol.Classinstmember) =
- NONE
in
case map_filter (fn (name, def) => hs_from_def (name, def)) defs
of [] => NONE
--- a/src/Pure/Tools/codegen_thingol.ML Wed Aug 16 16:44:41 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Thu Aug 17 09:24:47 2006 +0200
@@ -72,10 +72,9 @@
| Datatypecons of string
| Class of class list * (vname * (string * (sortcontext * itype)) list)
| Classmember of class
- | Classinst of ((class * (string * (vname * sort) list))
- * (class * iclasslookup list) list)
- * (string * ((string * funn) * iclasslookup list list)) list
- | Classinstmember;
+ | Classinst of (class * (string * (vname * sort) list))
+ * ((class * iclasslookup list) list
+ * (string * iterm) list);
type module;
type transact;
type 'dst transact_fin;
@@ -97,6 +96,7 @@
val fail: string -> transact -> 'a transact_fin;
val message: string -> (transact -> 'a) -> transact -> 'a;
val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
+ val elim_classes: module -> funn -> (iterm list * iterm) list * itype;
val debug: bool ref;
val debug_msg: ('a -> string) -> 'a -> 'a;
@@ -388,12 +388,11 @@
| Typesyn of sortcontext * itype
| Datatype of datatyp
| Datatypecons of string
-| Class of class list * (vname * (string * (sortcontext * itype)) list)
+ | Class of class list * (vname * (string * (sortcontext * itype)) list)
| Classmember of class
- | Classinst of ((class * (string * (vname * sort) list))
- * (class * iclasslookup list) list)
- * (string * ((string * funn) * iclasslookup list list)) list
- | Classinstmember;
+ | Classinst of (class * (string * (vname * sort) list))
+ * ((class * iclasslookup list) list
+ * (string * iterm) list);
datatype node = Def of def | Module of node Graph.T;
type module = node Graph.T;
@@ -451,7 +450,7 @@
Pretty.str "class member belonging to ",
Pretty.str clsname
]
- | pretty_def (Classinst (((clsname, (tyco, arity)), _), _)) =
+ | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
Pretty.block [
Pretty.str "class instance (",
Pretty.str clsname,
@@ -461,9 +460,7 @@
Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
map Pretty.str o snd) arity),
Pretty.str "))"
- ]
- | pretty_def Classinstmember =
- Pretty.str "class instance member";
+ ];
fun pretty_module modl =
let
@@ -517,7 +514,7 @@
val (name'', name_base) = split_last name'
val (modl, shallow) = split_last name''
in (modl, NameSpace.pack [shallow, name_base]) end
- handle Empty => error ("not a qualified name: " ^ quote name);
+ handle Empty => error ("Not a qualified name: " ^ quote name);
fun has_nsp name shallow =
NameSpace.is_qualified name
@@ -578,7 +575,7 @@
of NONE =>
module
|> Graph.new_node (base, Def Bot)
- | SOME (Module _) => error ("module already present: " ^ quote name)
+ | SOME (Module _) => error ("Module already present: " ^ quote name)
| _ => module)
| ensure (m::ms) module =
module
@@ -588,9 +585,9 @@
fun add_def_incr strict (name, Bot) module =
(case try (get_def module) name
- of NONE => if strict then error "attempted to add Bot to module"
+ of NONE => if strict then error "Attempted to add Bot to module"
else map_def name (K Bot) module
- | SOME Bot => if strict then error "attempted to add Bot to module"
+ | SOME Bot => if strict then error "Attempted to add Bot to module"
else map_def name (K Bot) module
| SOME _ => module)
| add_def_incr _ (name, def) module =
@@ -599,7 +596,7 @@
| SOME Bot => map_def name (K def) module
| SOME def' => if eq_def (def, def')
then module
- else error ("tried to overwrite definition " ^ quote name));
+ else error ("Tried to overwrite definition " ^ quote name));
fun add_dep (name1, name2) modl =
if name1 = name2 then modl
@@ -614,7 +611,7 @@
then Graph.add_edge
else fn edge => fn gr => (Graph.add_edge_acyclic edge gr
handle Graph.CYCLES _ =>
- error ("adding dependency "
+ error ("Adding dependency "
^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))
fun add [] node =
node
@@ -760,7 +757,7 @@
) memdecls
| deps_of (Classmember class) =
[class]
- | deps_of (Classinst (((class, (tyco, sctxt)), suparities), memdefs)) =
+ | deps_of (Classinst ((class, (tyco, sctxt)), (suparities, memdefs))) =
[]
|> insert (op =) class
|> insert (op =) tyco
@@ -769,15 +766,10 @@
insert (op =) supclass
#> fold add_deps_of_classlookup ls
) suparities
- |> fold (fn (name, ((_, (eqs, (sctxt, ty))), lss)) =>
+ |> fold (fn (name, e) =>
insert (op =) name
- #> add_deps_of_sortctxt sctxt
- #> add_deps_of_type ty
- #> fold (fn (lhs, rhs) => fold add_deps_of_term lhs #> add_deps_of_term rhs) eqs
- #> (fold o fold) add_deps_of_classlookup lss
- ) memdefs
- | deps_of Classinstmember =
- [];
+ #> add_deps_of_term e
+ ) memdefs;
fun delete_garbage hidden modl =
let
@@ -876,7 +868,7 @@
in
fn NONE => SOME l
| SOME l' => if l = l' then SOME l
- else error "function definition with different number of arguments"
+ else error "Function definition with different number of arguments"
end
) eqs NONE; eqs);
@@ -889,44 +881,24 @@
| check_prep_def modl (d as Datatype _) =
d
| check_prep_def modl (Datatypecons dtco) =
- error "attempted to add bare datatype constructor"
+ error "Attempted to add bare datatype constructor"
| check_prep_def modl (d as Class _) =
d
| check_prep_def modl (Classmember _) =
- error "attempted to add bare class member"
- | check_prep_def modl (Classinst ((d as ((class, (tyco, arity)), _), memdefs))) =
+ error "Attempted to add bare class member"
+ | check_prep_def modl (d as Classinst ((class, (tyco, arity)), (_, memdefs))) =
let
val Class (_, (v, membrs)) = get_def modl class;
val _ = if length memdefs > length memdefs
- then error "too many member definitions given"
+ then error "Too many member definitions given"
else ();
- fun instant (w, ty) v =
- if v = w then ty else ITyVar v;
- fun mk_memdef (m, (sortctxt, ty)) =
- case AList.lookup (op =) memdefs m
- of NONE => error ("missing definition for member " ^ quote m)
- | SOME ((m', (eqs, (sortctxt', ty'))), lss) =>
- let
- val sortctxt'' = sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity;
- val ty'' = instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty;
- in if eq_ityp ((sortctxt'', ty''), (sortctxt', ty'))
- then (m, ((m', (check_funeqs eqs, (sortctxt', ty'))), lss))
- else
- error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: "
- ^ (Pretty.output o Pretty.block o Pretty.breaks) [
- pretty_sortcontext sortctxt'',
- Pretty.str "|=>",
- pretty_itype ty''
- ] ^ " vs. " ^ (Pretty.output o Pretty.block o Pretty.breaks) [
- pretty_sortcontext sortctxt',
- Pretty.str "|=>",
- pretty_itype ty'
- ]
- )
- end
- in Classinst (d, map mk_memdef membrs) end
+ fun check_memdef (m, _) =
+ if AList.defined (op =) memdefs m
+ then () else error ("Missing definition for member " ^ quote m);
+ val _ = map check_memdef memdefs;
+ in d end
| check_prep_def modl Classinstmember =
- error "attempted to add bare class instance member";
+ error "Attempted to add bare class instance member";
fun postprocess_def (name, Datatype (_, constrs)) =
(check_samemodule (name :: map fst constrs);
@@ -944,12 +916,6 @@
#> add_dep (name, m)
) membrs
)
- | postprocess_def (name, Classinst (_, memdefs)) =
- (check_samemodule (name :: map (fst o fst o snd) memdefs);
- fold (fn (_, ((m', _), _)) =>
- add_def_incr true (m', Classinstmember)
- ) memdefs
- )
| postprocess_def _ =
I;
@@ -958,6 +924,7 @@
fun ensure_def defgen strict msg name (dep, modl) =
let
+ (*FIXME represent dependencies as tuple (name, name -> string), for better error msgs*)
val msg' = (case dep
of NONE => msg
| SOME dep => msg ^ ", required for " ^ quote dep)
@@ -1017,9 +984,9 @@
fun handle_fail f x =
(f x
handle FAIL (msgs, NONE) =>
- (error o cat_lines) ("code generation failed, while:" :: msgs))
+ (error o cat_lines) ("Code generation failed, while:" :: msgs))
handle FAIL (msgs, SOME e) =>
- ((Output.error_msg o cat_lines) ("code generation failed, while:" :: msgs); raise e);
+ ((Output.error_msg o cat_lines) ("Code generation failed, while:" :: msgs); raise e);
in
modl
|> (if is_some init then ensure_bot (the init) else I)
@@ -1040,6 +1007,13 @@
end;
+(** eliminating classes in definitions **)
+
+fun elim_classes modl (eqs, (sortctxt, ty)) =
+ let
+ fun elim_expr _ = ();
+ in (error ""; (eqs, ty)) end;
+
(** generic serialization **)
(* resolving *)
@@ -1066,7 +1040,7 @@
|> perhaps validate;
fun is_valid _ _ = true;
fun maybe_unique _ _ = NONE;
- fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
+ fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
);
fun mk_deresolver module nsp_conn postprocess validate =
@@ -1125,7 +1099,7 @@
val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name);
val (_, SOME tab') = get_path_name common tab;
val (name', _) = get_path_name rem tab';
- in NameSpace.pack name' end;
+ in NameSpace.pack name' end handle BIND => (error "Missing name: " ^ quote name);
in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;