diff -r e11031fe4096 -r a06868ebeb0f src/Pure/sign.ML --- 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