--- a/src/Pure/sign.ML Sat Jun 11 22:15:52 2005 +0200
+++ b/src/Pure/sign.ML Sat Jun 11 22:15:53 2005 +0200
@@ -13,9 +13,8 @@
val rep_sg: sg ->
{self: sg_ref,
tsig: Type.tsig,
- consts: (typ * stamp) Symtab.table,
+ consts: (typ * stamp) NameSpace.table,
naming: NameSpace.naming,
- spaces: {class: NameSpace.T, tycon: NameSpace.T, const: NameSpace.T},
data: data}
val stamp_names_of: sg -> string list
val exists_stamp: string -> sg -> bool
@@ -59,16 +58,13 @@
val the_const_type: sg -> string -> typ
val declared_tyname: sg -> string -> bool
val declared_const: sg -> string -> bool
- val classK: string
- val typeK: string
- val constK: string
- val intern: sg -> string -> xstring -> string
- val extern: sg -> string -> string -> xstring
- val extern_table: sg -> string -> 'a Symtab.table -> (xstring * 'a) list
+ val class_space: sg -> NameSpace.T
+ val type_space: sg -> NameSpace.T
+ val const_space: sg -> NameSpace.T
val intern_class: sg -> xstring -> string
val extern_class: sg -> string -> xstring
- val intern_tycon: sg -> xstring -> string
- val extern_tycon: sg -> string -> xstring
+ val intern_type: sg -> xstring -> string
+ val extern_type: sg -> string -> xstring
val intern_const: sg -> xstring -> string
val extern_const: sg -> string -> xstring
val intern_sort: sg -> sort -> sort
@@ -106,8 +102,8 @@
val read_typ: sg * (indexname -> sort option) -> string -> typ
val read_typ_syntax: sg * (indexname -> sort option) -> string -> typ
val read_typ_abbrev: sg * (indexname -> sort option) -> string -> typ
- val read_tyname: sg -> string -> typ (*exception TYPE*)
- val read_const: sg -> string -> term (*exception TYPE*)
+ val read_tyname: sg -> string -> typ
+ val read_const: sg -> string -> term
val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) ->
(indexname -> sort option) -> string list -> bool
-> (term list * typ) list -> term list * (indexname * typ) list
@@ -167,8 +163,12 @@
val custom_accesses: (string list -> string list list) -> sg -> sg
val set_policy: (string -> bstring -> string) * (string list -> string list list) -> sg -> sg
val restore_naming: sg -> sg -> sg
- val hide_space: bool -> string * string list -> sg -> sg
- val hide_space_i: bool -> string * string list -> sg -> sg
+ val hide_classes: bool -> xstring list -> sg -> sg
+ val hide_classes_i: bool -> string list -> sg -> sg
+ val hide_types: bool -> xstring list -> sg -> sg
+ val hide_types_i: bool -> string list -> sg -> sg
+ val hide_consts: bool -> xstring list -> sg -> sg
+ val hide_consts_i: bool -> string list -> sg -> sg
val merge_refs: sg_ref * sg_ref -> sg_ref
val merge: sg * sg -> sg
val prep_ext_merge: sg list -> sg
@@ -194,13 +194,12 @@
datatype sg =
Sg of
{id: string ref,
- stamps: string ref list, (*unique theory indentifier*)
- syn: syn} * (*syntax for parsing and printing*)
- {self: sg_ref, (*mutable self reference*)
- tsig: Type.tsig, (*order-sorted signature of types*)
- consts: (typ * stamp) Symtab.table, (*type schemes of constants*)
+ stamps: string ref list, (*unique theory indentifier*)
+ syn: syn} * (*syntax for parsing and printing*)
+ {self: sg_ref, (*mutable self reference*)
+ tsig: Type.tsig, (*order-sorted signature of types*)
+ consts: (typ * stamp) NameSpace.table, (*type schemes of constants*)
naming: NameSpace.naming,
- spaces: {class: NameSpace.T, tycon: NameSpace.T, const: NameSpace.T},
data: data}
and data =
Data of
@@ -222,9 +221,9 @@
SgRef of sg ref option;
(* FIXME assign!??? *)
-fun make_sg (id, self, stamps) naming data (syn, tsig, consts, spaces) =
+fun make_sg (id, self, stamps) naming data (syn, tsig, consts) =
Sg ({id = id, stamps = stamps, syn = syn}, {self = self, tsig = tsig,
- consts = consts, naming = naming, spaces = spaces, data = data});
+ consts = consts, naming = naming, data = data});
fun rep_sg (Sg (_, args)) = args;
@@ -365,37 +364,39 @@
val sg = make_sg (id, self, id :: stamps') naming data sign;
in assign self sg; sg end;
-fun new_sg f (sg as Sg ({stamps, syn, ...}, {self = _, tsig, consts, naming, spaces, data})) =
+fun new_sg f (sg as Sg ({stamps, syn, ...}, {self = _, tsig, consts, naming, data})) =
let
val _ = check_stale "Sign.new_sg" sg;
val self' = SgRef (SOME (ref sg));
val data' = f data;
- in create_sg "#" self' stamps naming data' (syn, tsig, consts, spaces) end;
+ in create_sg "#" self' stamps naming data' (syn, tsig, consts) end;
val prep_ext = new_sg prep_ext_data;
val copy = new_sg copy_data;
-fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
+fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, data})) =
let
val _ = check_stale "Sign.add_name" sg;
val (self', data') =
if is_draft sg then (self, data)
else (SgRef (SOME (ref sg)), prep_ext_data data);
- in create_sg name self' stamps naming data' (syn, tsig, consts, spaces) end;
+ in create_sg name self' stamps naming data' (syn, tsig, consts) end;
-fun map_sg keep f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
+fun map_sg keep f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, data})) =
let
val _ = check_stale "Sign.map_sg" sg;
val (self', data') =
if is_draft sg andalso keep then (self, data)
else (SgRef (SOME (ref sg)), prep_ext_data data);
- val (naming', data', sign') = f (naming, data', (syn, tsig, consts, spaces));
+ val (naming', data', sign') = f (naming, data', (syn, tsig, consts));
in create_sg "#" self' stamps naming' data' sign' end;
fun map_naming f = map_sg true (fn (naming, data, sign) => (f naming, data, sign));
fun map_data f = map_sg true (fn (naming, data, sign) => (naming, f data, sign));
fun map_sign f = map_sg true (fn (naming, data, sign) => (naming, data, f sign));
-fun map_syn f = map_sign (fn (syn, tsig, consts, spaces) => (f syn, tsig, consts, spaces));
+fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts));
+fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
+fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
@@ -453,25 +454,15 @@
(** primitive signatures **)
-val empty_spaces =
- {class = NameSpace.empty, tycon = NameSpace.empty, const = NameSpace.empty};
-
-fun merge_spaces
- ({class = class1, tycon = tycon1, const = const1},
- {class = class2, tycon = tycon2, const = const2}) =
- {class = NameSpace.merge (class1, class2),
- tycon = NameSpace.merge (tycon1, tycon2),
- const = NameSpace.merge (const1, const2)};
-
val pure_syn =
Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
val dummy_sg = make_sg (ref "", SgRef NONE, []) NameSpace.default_naming empty_data
- (pure_syn, Type.empty_tsig, Symtab.empty, empty_spaces);
+ (pure_syn, Type.empty_tsig, NameSpace.empty_table);
val pre_pure =
create_sg "#" (SgRef (SOME (ref dummy_sg))) [] NameSpace.default_naming empty_data
- (pure_syn, Type.empty_tsig, Symtab.empty, empty_spaces);
+ (pure_syn, Type.empty_tsig, NameSpace.empty_table);
val PureN = "Pure";
val CPureN = "CPure";
@@ -538,56 +529,31 @@
(* consts signature *)
-fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (consts, c));
+fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (#2 consts, c));
fun the_const_type sg c =
(case const_type sg c of SOME T => T
| NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
-fun declared_tyname sg c = is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c));
-fun declared_const sg c = is_some (const_type sg c);
-
-
-(* name spaces *)
-
-val classK = "class";
-val typeK = "type";
-val constK = "const";
-
-fun illegal_space kind = "Illegal signature name space: " ^ quote kind;
+fun declared_tyname sg c =
+ is_some (Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of sg))), c));
-fun space_of sg kind = #spaces (rep_sg sg) |>
- (if kind = classK then #class
- else if kind = typeK then #tycon
- else if kind = constK then #const
- else raise TERM (illegal_space kind, []));
-
-fun map_space kind f {class, tycon, const} =
- let
- val (class', tycon', const') =
- if kind = classK then (f class, tycon, const)
- else if kind = typeK then (class, f tycon, const)
- else if kind = constK then (class, tycon, f const)
- else raise TERM (illegal_space kind, []);
- in {class = class', tycon = tycon', const = const'} end;
-
-fun declare_names sg kind = map_space kind o fold (declare_name sg);
-fun hide_names kind = map_space kind oo (fold o NameSpace.hide);
+fun declared_const sg c = is_some (const_type sg c);
(** intern / extern names **)
-val intern = NameSpace.intern oo space_of;
-val extern = NameSpace.extern oo space_of;
-fun extern_table sg = curry NameSpace.extern_table o space_of sg;
+val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
+val type_space = #1 o #types o Type.rep_tsig o tsig_of;
+val const_space = #1 o #consts o rep_sg
-fun intern_class sg = intern sg classK;
-fun extern_class sg = extern sg classK;
-fun intern_tycon sg = intern sg typeK;
-fun extern_tycon sg = extern sg typeK;
-fun intern_const sg = intern sg constK;
-fun extern_const sg = extern sg constK;
+val intern_class = NameSpace.intern o class_space;
+val extern_class = NameSpace.extern o class_space;
+val intern_type = NameSpace.intern o type_space;
+val extern_type = NameSpace.extern o type_space;
+val intern_const = NameSpace.intern o const_space;
+val extern_const = NameSpace.extern o const_space;
val intern_sort = map o intern_class;
val extern_sort = map o extern_class;
@@ -614,11 +580,11 @@
in
-val intern_typ = typ_mapping intern_class intern_tycon;
-val extern_typ = typ_mapping extern_class extern_tycon;
-val intern_term = term_mapping intern_class intern_tycon intern_const;
-val extern_term = term_mapping extern_class extern_tycon extern_const;
-val intern_tycons = typ_mapping (K I) intern_tycon;
+val intern_typ = typ_mapping intern_class intern_type;
+val extern_typ = typ_mapping extern_class extern_type;
+val intern_term = term_mapping intern_class intern_type intern_const;
+val extern_term = term_mapping extern_class extern_type extern_const;
+val intern_tycons = typ_mapping (K I) intern_type;
end;
@@ -636,7 +602,7 @@
fun pretty_arity sg (a, Ss, S) =
let
- val a' = extern_tycon sg a;
+ val a' = extern_type sg a;
val dom =
if null Ss then []
else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
@@ -734,7 +700,7 @@
-(** read and certify entities **) (*exception ERROR*)
+(** read and certify entities **) (*exception ERROR/TYPE*)
(* sorts *)
@@ -775,18 +741,20 @@
end;
-(* type and constant names *) (*exception TYPE*) (* FIXME really!? *)
+(* type and constant names *)
fun read_tyname sg raw_c =
- let val c = intern_tycon sg raw_c in
- (case Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c) of
+ let val c = intern_type sg raw_c in
+ (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of sg))), c) of
SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
- | _ => raise TYPE ("Undeclared type constructor: " ^ quote c, [], []))
+ | _ => error ("Undeclared type constructor: " ^ quote c))
end;
fun read_const sg raw_c =
- let val c = intern_const sg raw_c
- in the_const_type sg c; Const (c, dummyT) end;
+ let
+ val c = intern_const sg raw_c;
+ val _ = the_const_type sg c handle TYPE (msg, _, _) => error msg;
+ in Const (c, dummyT) end;
@@ -867,8 +835,8 @@
(* add default sort *)
-fun gen_add_defsort prep_sort s sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
- (syn, Type.set_defsort (prep_sort sg s) tsig, consts, spaces));
+fun gen_add_defsort prep_sort s sg =
+ sg |> map_tsig (Type.set_defsort (prep_sort sg s));
val add_defsort = gen_add_defsort read_sort;
val add_defsort_i = gen_add_defsort certify_sort;
@@ -876,38 +844,34 @@
(* add type constructors *)
-fun add_types types sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
+fun add_types types sg = sg |> map_sign (fn (syn, tsig, consts) =>
let
val syn' = map_syntax (Syntax.extend_type_gram types) syn;
- val decls = map (fn (a, n, mx) => (full_name sg (Syntax.type_name a mx), n)) types;
- val tsig' = Type.add_types decls tsig;
- val spaces' = declare_names sg typeK (map #1 decls) spaces;
- in (syn', tsig', consts, spaces') end);
+ val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
+ val tsig' = Type.add_types (naming_of sg) decls tsig;
+ in (syn', tsig', consts) end);
(* add nonterminals *)
-fun add_nonterminals bnames sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
+fun add_nonterminals bnames sg = sg |> map_sign (fn (syn, tsig, consts) =>
let
val syn' = map_syntax (Syntax.extend_consts bnames) syn;
- val names = map (full_name sg) bnames;
- val tsig' = Type.add_nonterminals names tsig;
- val spaces' = declare_names sg typeK names spaces;
- in (syn', tsig', consts, spaces') end);
+ val tsig' = Type.add_nonterminals (naming_of sg) bnames tsig;
+ in (syn', tsig', consts) end);
(* add type abbreviations *)
fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) sg =
- sg |> map_sign (fn (syn, tsig, consts, spaces) =>
+ sg |> map_sign (fn (syn, tsig, consts) =>
let
val syn' = map_syntax (Syntax.extend_type_gram [(a, length vs, mx)]) syn;
- val a' = full_name sg (Syntax.type_name a mx);
+ val a' = Syntax.type_name a mx;
val abbr = (a', vs, prep_typ sg rhs) handle ERROR =>
- error ("in type abbreviation " ^ quote (Syntax.type_name a' mx));
- val tsig' = Type.add_abbrevs [abbr] tsig;
- val spaces' = declare_names sg typeK [a'] spaces;
- in (syn', tsig', consts, spaces') end);
+ error ("in type abbreviation " ^ quote a');
+ val tsig' = Type.add_abbrevs (naming_of sg) [abbr] tsig;
+ in (syn', tsig', consts) end);
val add_tyabbrs = fold (gen_add_tyabbr (read_typ_syntax o no_def_sort));
val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax);
@@ -915,15 +879,14 @@
(* add type arities *)
-fun gen_add_arities int_tycon prep_sort arities sg =
- sg |> map_sign (fn (syn, tsig, consts, spaces) =>
- let
- fun prep_arity (a, Ss, S) = (int_tycon sg a, map (prep_sort sg) Ss, prep_sort sg S)
- handle ERROR => error ("in arity for type " ^ quote a);
- val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
- in (syn, tsig', consts, spaces) end);
+fun gen_add_arities int_type prep_sort arities sg = sg |> map_tsig (fn tsig =>
+ let
+ fun prep_arity (a, Ss, S) = (int_type sg a, map (prep_sort sg) Ss, prep_sort sg S)
+ handle ERROR => error ("in arity for type " ^ quote a);
+ val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
+ in tsig' end);
-val add_arities = gen_add_arities intern_tycon read_sort;
+val add_arities = gen_add_arities intern_type read_sort;
val add_arities_i = gen_add_arities (K I) certify_sort;
@@ -956,15 +919,10 @@
fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
val args = map prep raw_args;
- val decls = args |> map (fn (c, T, mx) =>
- (full_name sg (Syntax.const_name c mx), (T, stamp ())));
- in
- sg |> map_sign (fn (syn, tsig, consts, spaces) =>
- (syn, tsig,
- Symtab.extend (consts, decls) handle Symtab.DUPS cs => err_dup_consts cs,
- declare_names sg constK (map #1 decls) spaces))
- |> add_syntax_i args
- end;
+ val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, (T, stamp ())));
+ fun extend_consts consts = NameSpace.extend_table (naming_of sg) (consts, decls)
+ handle Symtab.DUPS cs => err_dup_consts cs;
+ in sg |> map_consts extend_consts |> add_syntax_i args end;
val add_consts = gen_add_consts (read_typ o no_def_sort);
val add_consts_i = gen_add_consts certify_typ;
@@ -979,14 +937,12 @@
handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
fun gen_add_class int_class (bclass, raw_classes) sg =
- sg |> map_sign (fn (syn, tsig, consts, spaces) =>
+ sg |> map_sign (fn (syn, tsig, consts) =>
let
- val class = full_name sg bclass;
val classes = map (int_class sg) raw_classes;
val syn' = map_syntax (Syntax.extend_consts [bclass]) syn;
- val tsig' = Type.add_classes (pp sg) [(class, classes)] tsig;
- val spaces' = declare_names sg classK [class] spaces;
- in (syn', tsig', consts, spaces') end)
+ val tsig' = Type.add_classes (pp sg) (naming_of sg) [(bclass, classes)] tsig;
+ in (syn', tsig', consts) end)
|> add_consts_i [(const_of_class bclass, a_itselfT --> propT, Syntax.NoSyn)];
val add_classes = fold (gen_add_class intern_class);
@@ -995,12 +951,11 @@
(* add to classrel *)
-fun gen_add_classrel int_class raw_pairs sg =
- sg |> map_sign (fn (syn, tsig, consts, spaces) =>
- let
- val pairs = map (pairself (int_class sg)) raw_pairs;
- val tsig' = Type.add_classrel (pp sg) pairs tsig;
- in (syn, tsig', consts, spaces) end);
+fun gen_add_classrel int_class raw_pairs sg = sg |> map_tsig (fn tsig =>
+ let
+ val pairs = map (pairself (int_class sg)) raw_pairs;
+ val tsig' = Type.add_classrel (pp sg) pairs tsig;
+ in tsig' end);
val add_classrel = gen_add_classrel intern_class;
val add_classrel_i = gen_add_classrel (K I);
@@ -1035,7 +990,7 @@
(* add translation rules *)
fun add_trrules args sg = sg |> map_syn (fn syn =>
- let val rules = map (Syntax.map_trrule (apfst (intern_tycon sg))) args
+ let val rules = map (Syntax.map_trrule (apfst (intern_type sg))) args
in map_syntax (Syntax.extend_trrules (is_logtype sg) (make_syntax sg syn) rules) syn end);
val add_trrules_i = map_syn o map_syntax o Syntax.extend_trrules_i;
@@ -1053,14 +1008,13 @@
(* hide names *)
-fun hide_space fully (kind, xnames) sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
- let
- val names = map (intern sg kind) xnames;
- val spaces' = hide_names kind fully names spaces;
- in (syn, tsig, consts, spaces') end);
-
-fun hide_space_i fully (kind, names) = map_sign (fn (syn, tsig, consts, spaces) =>
- (syn, tsig, consts, hide_names kind fully names spaces));
+fun hide_classes b xs sg = sg |> map_tsig (Type.hide_classes b (map (intern_class sg) xs));
+val hide_classes_i = map_tsig oo Type.hide_classes;
+fun hide_types b xs sg = sg |> map_tsig (Type.hide_types b (map (intern_type sg) xs));
+val hide_types_i = map_tsig oo Type.hide_types;
+fun hide_consts b xs sg =
+ sg |> map_consts (apfst (fold (NameSpace.hide b o intern_const sg) xs));
+val hide_consts_i = (map_consts o apfst) oo (fold o NameSpace.hide);
@@ -1101,28 +1055,25 @@
else
let
val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
- {self = _, tsig = tsig1, consts = consts1,
- naming = _, spaces = spaces1, data = data1}) = sg1;
+ {self = _, tsig = tsig1, consts = consts1, naming = _, data = data1}) = sg1;
val Sg ({id = _, stamps = stamps2, syn = Syn (syntax2, trfuns2)},
- {self = _, tsig = tsig2, consts = consts2,
- naming = _, spaces = spaces2, data = data2}) = sg2;
+ {self = _, tsig = tsig2, consts = consts2, naming = _, data = data2}) = sg2;
val stamps = merge_stamps stamps1 stamps2;
val syntax = Syntax.merge_syntaxes syntax1 syntax2;
val trfuns = merge_trfuns trfuns1 trfuns2;
val syn = Syn (syntax, trfuns);
- val consts = Symtab.merge eq_snd (consts1, consts2)
+ val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
handle Symtab.DUPS cs => err_dup_consts cs;
val naming = NameSpace.default_naming;
- val spaces = merge_spaces (spaces1, spaces2);
val data = merge_data (data1, data2);
val pre_sg = make_sg (ref "", SgRef (SOME (ref dummy_sg)), ref "#" :: stamps1)
- naming data (syn, tsig1, consts, spaces);
+ naming data (syn, tsig1, consts);
val tsig = Type.merge_tsigs (pp pre_sg) (tsig1, tsig2);
val self = SgRef (SOME (ref dummy_sg));
- val sg = make_sg (ref "", self, stamps) naming data (syn, tsig, consts, spaces);
+ val sg = make_sg (ref "", self, stamps) naming data (syn, tsig, consts);
in assign self sg; syn_of sg; sg end;
in