# HG changeset patch # User wenzelm # Date 877601595 -7200 # Node ID ddeb5a0fd08dfe4193fa4f84b34dd42e14712e65 # Parent d3c2159b75fad2d2dfd8d26fe7ecfcfc70c40457 hide id, stamps; added stamp_names_of, name_of; replaced make_draft by prep_ext; improved print_sg; tuned; diff -r d3c2159b75fa -r ddeb5a0fd08d src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Oct 23 12:10:55 1997 +0200 +++ b/src/Pure/sign.ML Thu Oct 23 12:13:15 1997 +0200 @@ -20,15 +20,15 @@ type sg type sg_ref val rep_sg: sg -> - {id: string ref, (* FIXME hide!? *) - self: sg_ref, + {self: sg_ref, tsig: Type.type_sig, const_tab: typ Symtab.table, syn: Syntax.syntax, path: string list, spaces: (string * NameSpace.T) list, - data: Data.T, - stamps: string ref list} (* FIXME hide!? *) + data: Data.T} + val name_of: sg -> string + val stamp_names_of: sg -> string list val tsig_of: sg -> Type.type_sig val deref: sg_ref -> sg val self_ref: sg -> sg_ref @@ -115,7 +115,7 @@ val put_data: string * exn -> sg -> sg val print_data: sg -> string -> unit val merge_refs: sg_ref * sg_ref -> sg_ref - val make_draft: sg -> sg + val prep_ext: sg -> sg val merge: sg * sg -> sg val proto_pure: sg val pure: sg @@ -131,40 +131,47 @@ (** datatype sg **) datatype sg = - Sg of { - id: string ref, (*id*) - self: sg_ref, (*mutable self reference*) + Sg of + {id: string ref, (*id*) + stamps: string ref list} * (*unique theory indentifier*) + {self: sg_ref, (*mutable self reference*) tsig: Type.type_sig, (*order-sorted signature of types*) const_tab: typ Symtab.table, (*type schemes of constants*) syn: Syntax.syntax, (*syntax for parsing and printing*) - path: string list, (*current name space entry prefix*) - spaces: (string * NameSpace.T) list, (*name spaces for consts, types etc.*) - data: Data.T, (*additional data*) - stamps: string ref list} (*unique theory indentifier*) - (*the "ref" in stamps ensures that no two signatures are identical - -- it is impossible to forge a signature*) + path: string list, (*current name space entry prefix*) + spaces: (string * NameSpace.T) list, (*name spaces for consts, types etc.*) + data: Data.T} (*additional data*) and sg_ref = SgRef of sg ref option; (*make signature*) fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) = - Sg {id = id, self = self, tsig = tsig, const_tab = const_tab, syn = syn, - path = path, spaces = spaces, data = data, stamps = stamps}; + Sg ({id = id, stamps = stamps}, {self = self, tsig = tsig, const_tab = const_tab, + syn = syn, path = path, spaces = spaces, data = data}); + + +(* basic components *) + +fun rep_sg (Sg (_, args)) = args; -(*dest signature*) -fun rep_sg (Sg args) = args; +(*show stamps*) +fun stamp_names_of (Sg ({stamps, ...}, _)) = rev (map ! stamps); +fun pretty_sg sg = Pretty.str_list "{" "}" (stamp_names_of sg); +val str_of_sg = Pretty.str_of o pretty_sg; +val pprint_sg = Pretty.pprint o pretty_sg; + + val tsig_of = #tsig o rep_sg; val self_ref = #self o rep_sg; - -fun get_data (Sg {data, ...}) = Data.get data; -fun print_data (Sg {data, ...}) = Data.print data; - +val get_data = Data.get o #data o rep_sg; +val print_data = Data.print o #data o rep_sg; -(*show stamps*) -fun stamp_names stamps = rev (map ! stamps); +fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c); +val classes = #classes o Type.rep_tsig o tsig_of; -fun pretty_sg (Sg {stamps, ...}) = Pretty.str_list "{" "}" (stamp_names stamps); -val pprint_sg = Pretty.pprint o pretty_sg; +val subsort = Type.subsort o tsig_of; +val norm_sort = Type.norm_sort o tsig_of; +val nonempty_sort = Type.nonempty_sort o tsig_of; (* signature id *) @@ -172,11 +179,17 @@ fun deref (SgRef (Some (ref sg))) = sg | deref (SgRef None) = sys_error "Sign.deref"; -fun check_stale (sg as Sg {id, self = SgRef (Some (ref (Sg {id = id', ...}))), ...}) = +fun check_stale (sg as Sg ({id, ...}, + {self = SgRef (Some (ref (Sg ({id = id', ...}, _)))), ...})) = if id = id' then sg - else raise TERM ("Stale signature: " ^ Pretty.str_of (pretty_sg sg), []) + else raise TERM ("Stale signature: " ^ str_of_sg sg, []) | check_stale _ = sys_error "Sign.check_stale"; +fun name_of (sg as Sg ({id = ref name, ...}, _)) = + if name = "" orelse name = "#" then + raise TERM ("Nameless signature " ^ str_of_sg sg, []) + else name; + (* inclusion and equality *) @@ -196,13 +209,13 @@ if x = y then fast_sub (xs, ys) else fast_sub (x :: xs, ys); in - fun eq_sg (sg1 as Sg {id = id1, ...}, sg2 as Sg {id = id2, ...}) = + fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) = (check_stale sg1; check_stale sg2; id1 = id2); - fun subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) = + fun subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) = eq_sg (sg1, sg2) orelse subset_stamp (s1, s2); - fun fast_subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) = + fun fast_subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) = eq_sg (sg1, sg2) orelse fast_sub (s1, s2); end; @@ -210,11 +223,11 @@ (*test if same theory names are contained in signatures' stamps, i.e. if signatures belong to same theory but not necessarily to the same version of it*) -fun same_sg (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) = +fun same_sg (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) = eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2)); (*test for drafts*) -fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true +fun is_draft (Sg ({stamps = ref "#" :: _, ...}, _)) = true | is_draft _ = false; @@ -239,12 +252,12 @@ sign end; -fun extend_sign extfun name decls - (sg as Sg {id = _, self, tsig, const_tab, syn, path, spaces, data, stamps}) = +fun extend_sign keep extfun name decls + (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) = let val _ = check_stale sg; val (self', data') = - if is_draft sg then (self, data) + if is_draft sg andalso keep then (self, data) else (SgRef (Some (ref sg)), Data.prep_ext data); in create_sign self' stamps name @@ -252,20 +265,6 @@ end; -(* consts *) - -fun const_type (Sg {const_tab, ...}) c = Symtab.lookup (const_tab, c); - - -(* classes and sorts *) - -val classes = #classes o Type.rep_tsig o tsig_of; - -val subsort = Type.subsort o tsig_of; -val norm_sort = Type.norm_sort o tsig_of; -val nonempty_sort = Type.nonempty_sort o tsig_of; - - (** name spaces **) @@ -360,7 +359,7 @@ (mapping (trn constK) add_term_consts t); - fun spaces_of (Sg {spaces, ...}) = spaces; + val spaces_of = #spaces o rep_sg; in @@ -392,7 +391,7 @@ val intern_tycons = intrn_tycons o spaces_of; - fun full_name (Sg {path, ...}) = full path; + val full_name = full o #path o rep_sg; end; @@ -400,16 +399,16 @@ (** pretty printing of terms and types **) -fun pretty_term (Sg {syn, spaces, stamps, ...}) t = +fun pretty_term (sg as Sg (_, {syn, spaces, ...})) t = Syntax.pretty_term syn - ("CPure" mem_string (map ! stamps)) + ("CPure" mem_string (stamp_names_of sg)) (if ! long_names then t else extrn_term spaces t); -fun pretty_typ (Sg {syn, spaces, ...}) T = +fun pretty_typ (Sg (_, {syn, spaces, ...})) T = Syntax.pretty_typ syn (if ! long_names then T else extrn_typ spaces T); -fun pretty_sort (Sg {syn, spaces, ...}) S = +fun pretty_sort (Sg (_, {syn, spaces, ...})) S = Syntax.pretty_sort syn (if ! long_names then S else extrn_sort spaces S); @@ -446,10 +445,12 @@ let fun prt_cls c = pretty_sort sg [c]; fun prt_sort S = pretty_sort sg S; - fun prt_tycon t = Pretty.str (cond_extern sg typeK t); fun prt_arity t (c, Ss) = pretty_arity sg (t, Ss, [c]); fun prt_typ ty = Pretty.quote (pretty_typ sg ty); - fun prt_const c = Pretty.quote (Pretty.str (cond_extern sg constK c)); + + val ext_class = cond_extern sg classK; + val ext_tycon = cond_extern sg typeK; + val ext_const = cond_extern sg constK; fun pretty_space (kind, space) = Pretty.block (Pretty.breaks @@ -466,7 +467,7 @@ [Pretty.str "default:", Pretty.brk 1, pretty_sort sg S]; fun pretty_ty (t, n) = Pretty.block - [prt_tycon t, Pretty.str (" " ^ string_of_int n)]; + [Pretty.str (ext_tycon t), Pretty.str (" " ^ string_of_int n)]; fun pretty_abbr (t, (vs, rhs)) = Pretty.block [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)), @@ -475,14 +476,15 @@ fun pretty_arities (t, ars) = map (prt_arity t) ars; fun pretty_const (c, ty) = Pretty.block - [prt_const c, Pretty.str " ::", Pretty.brk 1, prt_typ ty]; + [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty]; - val Sg {id = _, self = _, tsig, const_tab, syn = _, path, spaces, data, stamps} = sg; + val Sg (_, {self = _, tsig, const_tab, syn = _, path, spaces, data}) = sg; val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces; val {classes, classrel, default, tycons, abbrs, arities} = Type.rep_tsig tsig; + val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab)); in - Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps)); + Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names_of sg)); Pretty.writeln (Pretty.strs ("data:" :: Data.kinds data)); Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]); Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces')); @@ -492,7 +494,7 @@ Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons)); Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr abbrs)); Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities arities))); - Pretty.writeln (Pretty.big_list "consts:" (map pretty_const (Symtab.dest const_tab))) + Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts)) end; @@ -508,7 +510,7 @@ handle ERROR => err_in_type str); (*read and certify typ wrt a signature*) -fun read_typ (sg as Sg {tsig, syn, spaces, ...}, def_sort) str = +fun read_typ (sg as Sg (_, {tsig, syn, spaces, ...}), def_sort) str = (check_stale sg; Type.cert_typ tsig (read_raw_typ syn tsig spaces def_sort str) handle TYPE (msg, _, _) => (error_msg msg; err_in_type str)); @@ -517,7 +519,7 @@ (** certify types and terms **) (*exception TYPE*) -fun certify_typ (Sg {tsig, ...}) ty = Type.cert_typ tsig ty; +val certify_typ = Type.cert_typ o tsig_of; (*check for duplicate TVars with distinct sorts*) fun nodup_TVars (tvars, T) = @@ -564,19 +566,19 @@ | mapfilt_atoms f a = (case f a of Some y => [y] | None => []); -fun certify_term (sg as Sg {tsig, ...}) tm = +fun certify_term sg tm = let val _ = check_stale sg; + val tsig = tsig_of sg; - fun valid_const a T = - (case const_type sg a of - Some U => Type.typ_instance (tsig, T, U) - | _ => false); + fun show_const a T = quote a ^ " :: " ^ quote (string_of_typ sg T); fun atom_err (Const (a, T)) = - if valid_const a T then None - else Some ("Illegal type for constant " ^ quote a ^ " :: " ^ - quote (string_of_typ sg T)) + (case const_type sg a of + None => Some ("Undeclared constant " ^ show_const a T) + | Some U => + if Type.typ_instance (tsig, T, U) then None + else Some ("Illegal type for constant " ^ show_const a T)) | atom_err (Var ((x, i), _)) = if i < 0 then Some ("Negative index for Var " ^ quote x) else None | atom_err _ = None; @@ -608,7 +610,7 @@ fun infer_types sg def_type def_sort used freeze (ts, T) = let - val Sg {tsig, ...} = sg; + val tsig = tsig_of sg; val prt = setmp Syntax.show_brackets true (setmp long_names true (pretty_term sg)); @@ -838,35 +840,34 @@ (* the external interfaces *) -val add_classes = extend_sign (ext_classes true) "#"; -val add_classes_i = extend_sign (ext_classes false) "#"; -val add_classrel = extend_sign (ext_classrel true) "#"; -val add_classrel_i = extend_sign (ext_classrel false) "#"; -val add_defsort = extend_sign (ext_defsort true) "#"; -val add_defsort_i = extend_sign (ext_defsort false) "#"; -val add_types = extend_sign ext_types "#"; -val add_tyabbrs = extend_sign ext_tyabbrs "#"; -val add_tyabbrs_i = extend_sign ext_tyabbrs_i "#"; -val add_arities = extend_sign (ext_arities true) "#"; -val add_arities_i = extend_sign (ext_arities false) "#"; -val add_consts = extend_sign ext_consts "#"; -val add_consts_i = extend_sign ext_consts_i "#"; -val add_syntax = extend_sign ext_syntax "#"; -val add_syntax_i = extend_sign ext_syntax_i "#"; -val add_modesyntax = extend_sign ext_modesyntax "#"; -val add_modesyntax_i = extend_sign ext_modesyntax_i "#"; -val add_trfuns = extend_sign (ext_syn Syntax.extend_trfuns) "#"; -val add_trfunsT = extend_sign (ext_syn Syntax.extend_trfunsT) "#"; -val add_tokentrfuns = extend_sign (ext_syn Syntax.extend_tokentrfuns) "#"; -val add_trrules = extend_sign (ext_syn Syntax.extend_trrules) "#"; -val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#"; -val add_path = extend_sign ext_path "#"; -val add_space = extend_sign ext_space "#"; -val init_data = extend_sign ext_init_data "#"; -val put_data = extend_sign ext_put_data "#"; -fun add_name name sg = extend_sign K name () sg; - -val make_draft = add_name "#"; +val add_classes = extend_sign true (ext_classes true) "#"; +val add_classes_i = extend_sign true (ext_classes false) "#"; +val add_classrel = extend_sign true (ext_classrel true) "#"; +val add_classrel_i = extend_sign true (ext_classrel false) "#"; +val add_defsort = extend_sign true (ext_defsort true) "#"; +val add_defsort_i = extend_sign true (ext_defsort false) "#"; +val add_types = extend_sign true ext_types "#"; +val add_tyabbrs = extend_sign true ext_tyabbrs "#"; +val add_tyabbrs_i = extend_sign true ext_tyabbrs_i "#"; +val add_arities = extend_sign true (ext_arities true) "#"; +val add_arities_i = extend_sign true (ext_arities false) "#"; +val add_consts = extend_sign true ext_consts "#"; +val add_consts_i = extend_sign true ext_consts_i "#"; +val add_syntax = extend_sign true ext_syntax "#"; +val add_syntax_i = extend_sign true ext_syntax_i "#"; +val add_modesyntax = extend_sign true ext_modesyntax "#"; +val add_modesyntax_i = extend_sign true ext_modesyntax_i "#"; +val add_trfuns = extend_sign true (ext_syn Syntax.extend_trfuns) "#"; +val add_trfunsT = extend_sign true (ext_syn Syntax.extend_trfunsT) "#"; +val add_tokentrfuns = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#"; +val add_trrules = extend_sign true (ext_syn Syntax.extend_trrules) "#"; +val add_trrules_i = extend_sign true (ext_syn Syntax.extend_trrules_i) "#"; +val add_path = extend_sign true ext_path "#"; +val add_space = extend_sign true ext_space "#"; +val init_data = extend_sign true ext_init_data "#"; +val put_data = extend_sign true ext_put_data "#"; +fun add_name name sg = extend_sign true K name () sg; +fun prep_ext sg = extend_sign false K "#" () sg; @@ -895,18 +896,17 @@ else (*neither is union already; must form union*) let - val Sg {id = _, self = _, tsig = tsig1, const_tab = const_tab1, syn = syn1, - path = _, spaces = spaces1, data = data1, stamps = stamps1} = sg1; - val Sg {id = _, self = _, tsig = tsig2, const_tab = const_tab2, syn = syn2, - path = _, spaces = spaces2, data = data2, stamps = stamps2} = sg2; - + val Sg ({id = _, stamps = stamps1}, {self = _, tsig = tsig1, const_tab = const_tab1, + syn = syn1, path = _, spaces = spaces1, data = data1}) = sg1; + val Sg ({id = _, stamps = stamps2}, {self = _, tsig = tsig2, const_tab = const_tab2, + syn = syn2, path = _, spaces = spaces2, data = data2}) = sg2; val id = ref ""; - val self_ref = ref sg1; (*dummy value*) + val self_ref = ref sg1; (*dummy value*) val self = SgRef (Some self_ref); val stamps = merge_rev_lists stamps1 stamps2; val _ = - (case duplicates (stamp_names stamps) of + (case duplicates (map ! stamps) of [] => () | dups => raise TERM ("Attempt to merge different versions of theories " ^ commas_quote dups, []));