# HG changeset patch # User wenzelm # Date 1085167362 -7200 # Node ID e65d77313a9455c2ea39fe457cb47d16005dcceb # Parent e7f7ed4c06f285caa56245a71e37689ab718b2b5 xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup; diff -r e7f7ed4c06f2 -r e65d77313a94 src/Pure/sign.ML --- a/src/Pure/sign.ML Fri May 21 21:22:10 2004 +0200 +++ b/src/Pure/sign.ML Fri May 21 21:22:42 2004 +0200 @@ -23,15 +23,15 @@ type data val rep_sg: sg -> {self: sg_ref, - tsig: Type.type_sig, - const_tab: typ Symtab.table, + tsig: Type.tsig, + consts: (typ * stamp) Symtab.table, path: string list option, spaces: (string * NameSpace.T) list, data: data} val name_of: sg -> string val stamp_names_of: sg -> string list val exists_stamp: string -> sg -> bool - val tsig_of: sg -> Type.type_sig + val tsig_of: sg -> Type.tsig val deref: sg_ref -> sg val self_ref: sg -> sg_ref val subsig: sg * sg -> bool @@ -46,10 +46,9 @@ val defaultS: sg -> sort val subsort: sg -> sort * sort -> bool val nodup_vars: term -> term - val norm_sort: sg -> sort -> sort val of_sort: sg -> typ * sort -> bool val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list - val univ_witness: sg -> (typ * sort) option + val universal_witness: sg -> (typ * sort) option val typ_instance: sg -> typ * typ -> bool val classK: string val typeK: string @@ -92,9 +91,7 @@ val certify_class: sg -> class -> class val certify_sort: sg -> sort -> sort val certify_typ: sg -> typ -> typ - val certify_typ_no_norm: sg -> typ -> typ - val certify_tycon: sg -> string -> string - val certify_tyabbr: sg -> string -> string + val certify_typ_raw: sg -> typ -> typ val certify_tyname: sg -> string -> string val certify_const: sg -> string -> string val certify_term: sg -> term -> term * typ * int @@ -102,7 +99,7 @@ val read_raw_typ: sg * (indexname -> sort option) -> string -> typ val read_typ: sg * (indexname -> sort option) -> string -> typ val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ - val read_typ_no_norm': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ + val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ val infer_types: sg -> (indexname -> typ option) -> (indexname -> sort option) -> string list -> bool -> xterm list * typ -> term * (indexname * typ) list @@ -190,8 +187,8 @@ stamps: string ref list, (*unique theory indentifier*) syn: syn} * (*syntax for parsing and printing*) {self: sg_ref, (*mutable self reference*) - tsig: Type.type_sig, (*order-sorted signature of types*) - const_tab: typ Symtab.table, (*type schemes of constants*) + tsig: Type.tsig, (*order-sorted signature of types*) + consts: (typ * stamp) Symtab.table, (*type schemes of constants*) path: string list option, (*current name space entry prefix*) spaces: (string * NameSpace.T) list, (*name spaces for consts, types etc.*) data: data} (*anytype data*) @@ -215,9 +212,9 @@ SgRef of sg ref option; (*make signature*) -fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) = +fun make_sign (id, self, tsig, consts, syn, path, spaces, data, stamps) = Sg ({id = id, stamps = stamps, syn = syn}, {self = self, tsig = tsig, - const_tab = const_tab, path = path, spaces = spaces, data = data}); + consts = consts, path = path, spaces = spaces, data = data}); (* basic operations *) @@ -231,7 +228,7 @@ val pprint_sg = Pretty.pprint o pretty_sg; val tsig_of = #tsig o rep_sg; -fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c); +fun const_type (Sg (_, {consts, ...})) c = apsome #1 (Symtab.lookup (consts, c)); (* id and self *) @@ -334,11 +331,10 @@ val classes = Type.classes o tsig_of; val defaultS = Type.defaultS o tsig_of; val subsort = Type.subsort o tsig_of; -val norm_sort = Type.norm_sort o tsig_of; val of_sort = Type.of_sort o tsig_of; val witness_sorts = Type.witness_sorts o tsig_of; -val univ_witness = Type.univ_witness o tsig_of; -fun typ_instance sg (T, U) = Type.typ_instance (tsig_of sg, T, U); +val universal_witness = Type.universal_witness o tsig_of; +val typ_instance = Type.typ_instance o tsig_of; (** signature data **) @@ -357,8 +353,7 @@ error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg); fun err_uninit sg kind = - error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ - of_theory sg); + error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg); (*Trying to access theory data using get / put operations from a different instance of the TheoryDataFun result. Typical cure: re-load all files*) @@ -454,7 +449,7 @@ end; fun extend_sign keep extfun name decls - (sg as Sg ({id = _, stamps, syn}, {self, tsig, const_tab, path, spaces, data})) = + (sg as Sg ({id = _, stamps, syn}, {self, tsig, consts, path, spaces, data})) = let val _ = check_stale sg; val (self', data') = @@ -462,7 +457,7 @@ else (SgRef (Some (ref sg)), prep_ext_data data); in create_sign self' stamps name - (extfun sg (syn, tsig, const_tab, (path, spaces), data') decls) + (extfun sg (syn, tsig, consts, (path, spaces), data') decls) end; @@ -494,14 +489,15 @@ (*make full names*) fun full _ "" = error "Attempt to declare empty name \"\"" - | full None name = name - | full (Some path) name = - if NameSpace.is_qualified name then - error ("Attempt to declare qualified name " ^ quote name) + | full None bname = bname + | full (Some path) bname = + if NameSpace.is_qualified bname then + error ("Attempt to declare qualified name " ^ quote bname) else - (if not (Syntax.is_identifier name) - then warning ("Declared non-identifier name " ^ quote name) else (); - NameSpace.pack (path @ [name])); + let val name = NameSpace.pack (path @ [bname]) in + if Syntax.is_identifier bname then () + else warning ("Declared non-identifier " ^ quote name); name + end; (*base name*) val base_name = NameSpace.base; @@ -579,12 +575,12 @@ val pure_syn = Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty)); -val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0, +val dummy_sg = make_sign (ref "", SgRef None, Type.empty_tsig, Symtab.empty, pure_syn, Some [], [], empty_data, []); val pre_pure = create_sign (SgRef (Some (ref dummy_sg))) [] "#" - (pure_syn, Type.tsig0, Symtab.empty, (Some [], []), empty_data); + (pure_syn, Type.empty_tsig, Symtab.empty, (Some [], []), empty_data); val PureN = "Pure"; val CPureN = "CPure"; @@ -658,8 +654,8 @@ error ("The error(s) above occurred in type " ^ quote s); fun rd_raw_typ syn tsig spaces def_sort str = - intrn_tycons spaces - (Syntax.read_typ syn (Type.get_sort tsig def_sort (intrn_sort spaces)) (intrn_sort spaces) str + intrn_tycons spaces (Syntax.read_typ syn + (TypeInfer.get_sort tsig def_sort (intrn_sort spaces)) (intrn_sort spaces) str handle ERROR => err_in_type str); fun read_raw_typ' syn (sg as Sg (_, {tsig, spaces, ...}), def_sort) str = @@ -673,10 +669,10 @@ (cert (tsig_of sg) (rd (sg, def_sort) str) handle TYPE (msg, _, _) => (error_msg msg; err_in_type str)); in - val read_typ = read_typ_aux read_raw_typ Type.cert_typ; - val read_typ_no_norm = read_typ_aux read_raw_typ Type.cert_typ_no_norm; - fun read_typ' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ; - fun read_typ_no_norm' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ_no_norm; + val read_typ = read_typ_aux read_raw_typ Type.cert_typ; + val read_typ_raw = read_typ_aux read_raw_typ Type.cert_typ_raw; + fun read_typ' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ; + fun read_typ_raw' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ_raw; end; @@ -686,22 +682,15 @@ val certify_class = Type.cert_class o tsig_of; val certify_sort = Type.cert_sort o tsig_of; val certify_typ = Type.cert_typ o tsig_of; -val certify_typ_no_norm = Type.cert_typ_no_norm o tsig_of; - -fun certify_tycon sg c = - if is_some (Symtab.lookup (#tycons (Type.rep_tsig (tsig_of sg)), c)) then c - else raise TYPE ("Undeclared type constructor " ^ quote c, [], []); - -fun certify_tyabbr sg c = - if is_some (Symtab.lookup (#abbrs (Type.rep_tsig (tsig_of sg)), c)) then c - else raise TYPE ("Unknown type abbreviation " ^ quote c, [], []); +val certify_typ_raw = Type.cert_typ_raw o tsig_of; fun certify_tyname sg c = - certify_tycon sg c handle TYPE _ => certify_tyabbr sg c handle TYPE _ => - raise TYPE ("Unknown type name " ^ quote c, [], []); + if is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c + else raise TYPE ("Undeclared type constructor: " ^ quote c, [], []); fun certify_const sg c = - if is_some (const_type sg c) then c else raise TYPE ("Undeclared constant " ^ quote c, [], []); + if is_some (const_type sg c) then c + else raise TYPE ("Undeclared constant: " ^ quote c, [], []); (* certify_term *) @@ -781,34 +770,34 @@ in typ_of ([], tm) end; - fun certify_term sg tm = let val _ = check_stale sg; - val tsig = tsig_of sg; + + val tm' = Term.map_term_types (Type.cert_typ (tsig_of sg)) tm; + val tm' = if tm = tm' then tm else tm'; (*avoid copying of already normal term*) + + fun err msg = raise TYPE (msg, [], [tm']); fun show_const a T = quote a ^ " :: " ^ quote (string_of_typ sg T); - fun atom_err (errs, Const (a, T)) = - (case const_type sg a of - None => ("Undeclared constant " ^ show_const a T) :: errs - | Some U => - if typ_instance sg (T, U) then errs - else ("Illegal type for constant " ^ show_const a T) :: errs) - | atom_err (errs, Var ((x, i), _)) = - if i < 0 then ("Negative index for Var " ^ quote x) :: errs else errs - | atom_err (errs, _) = errs; + fun check_atoms (t $ u) = (check_atoms t; check_atoms u) + | check_atoms (Abs (_, _, t)) = check_atoms t + | check_atoms (Const (a, T)) = + (case const_type sg a of + None => err ("Undeclared constant " ^ show_const a T) + | Some U => + if typ_instance sg (T, U) then () + else err ("Illegal type for constant " ^ show_const a T)) + | check_atoms (Var ((x, i), _)) = + if i < 0 then err ("Malformed variable: " ^ quote x) else () + | check_atoms _ = (); + in + check_atoms tm'; + nodup_vars tm'; + (tm', type_check sg tm', maxidx_of_term tm') + end; - val norm_tm = - (case it_term_types (Type.typ_errors tsig) (tm, []) of - [] => Type.norm_term tsig tm - | errs => raise TYPE (cat_lines errs, [], [tm])); - val _ = nodup_vars norm_tm; - in - (case foldl_aterms atom_err ([], norm_tm) of - [] => (norm_tm, type_check sg norm_tm, maxidx_of_term norm_tm) - | errs => raise TYPE (cat_lines errs, [], [norm_tm])) - end; (** infer_types **) (*exception ERROR*) @@ -834,7 +823,7 @@ map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args; fun infer ts = OK - (Type.infer_types prt prT tsig (const_type sg) def_type def_sort + (TypeInfer.infer_types prt prT tsig (const_type sg) def_type def_sort (intern_const sg) (intern_tycons sg) (intern_sort sg) used freeze typs ts) handle TYPE (msg, _, _) => Error msg; @@ -899,7 +888,7 @@ (* add default sort *) fun ext_defS prep_sort sg (syn, tsig, ctab, (path, spaces), data) S = - (syn, Type.ext_tsig_defsort tsig (prep_sort sg syn tsig spaces S), + (syn, Type.set_defsort (prep_sort sg syn tsig spaces S) tsig, ctab, (path, spaces), data); fun ext_defsort arg = ext_defS rd_sort arg; @@ -911,13 +900,10 @@ fun ext_types _ (syn, tsig, ctab, (path, spaces), data) types = let val decls = decls_of path Syntax.type_name types in (map_syntax (Syntax.extend_type_gram types) syn, - Type.ext_tsig_types tsig decls, ctab, + Type.add_types decls tsig, ctab, (path, add_names spaces typeK (map fst decls)), data) end; -fun ext_nonterminals sign sg nonterms = - ext_types sign sg (map (fn n => (n, 0, Syntax.NoSyn)) nonterms); - (* add type abbreviations *) @@ -936,13 +922,23 @@ val spaces' = add_names spaces typeK (map #1 abbrs'); val decls = map (rd_abbr sg syn' tsig spaces') abbrs'; in - (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'), data) + (syn', Type.add_abbrs decls tsig, ctab, (path, spaces'), data) end; fun ext_tyabbrs abbrs = ext_abbrs read_abbr abbrs; fun ext_tyabbrs_i abbrs = ext_abbrs no_read abbrs; +(* add nonterminals *) + +fun ext_nonterminals _ (syn, tsig, ctab, (path, spaces), data) bnames = + let val names = map (full path) bnames in + (map_syntax (Syntax.extend_consts names) syn, + Type.add_nonterminals names tsig, ctab, + (path, add_names spaces typeK names), data) + end; + + (* add type arities *) fun ext_ars int prep_sort sg (syn, tsig, ctab, (path, spaces), data) arities = @@ -950,7 +946,7 @@ val prepS = prep_sort sg syn tsig spaces; fun prep_arity (c, Ss, S) = (if int then intrn spaces typeK c else c, map prepS Ss, prepS S); - val tsig' = Type.ext_tsig_arities tsig (map prep_arity arities); + val tsig' = Type.add_arities (map prep_arity arities) tsig; val log_types = Type.logical_types tsig'; in (map_syntax (Syntax.extend_log_types log_types) syn, @@ -980,10 +976,10 @@ fun ext_cnsts rd_const syn_only prmode sg (syn, tsig, ctab, (path, spaces), data) raw_consts = let - fun prep_const (c, ty, mx) = - (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx) - handle TYPE (msg, _, _) => - (error_msg msg; err_in_const (const_name path c mx)); + val prep_typ = compress_type o Type.varifyT o Type.no_tvars o + (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig); + fun prep_const (c, ty, mx) = (c, prep_typ ty, mx) handle TYPE (msg, _, _) => + (error_msg msg; err_in_const (const_name path c mx)); val consts = map (prep_const o rd_const sg syn tsig (path, spaces)) raw_consts; val decls = @@ -991,7 +987,7 @@ else decls_of path Syntax.const_name consts; in (map_syntax (Syntax.extend_const_gram prmode consts) syn, tsig, - Symtab.extend (ctab, decls) + Symtab.extend (ctab, map (fn (c, T) => (c, (T, stamp ()))) decls) handle Symtab.DUPS cs => err_dup_consts cs, (path, add_names spaces constK (map fst decls)), data) end; @@ -1031,7 +1027,7 @@ in ext_consts_i sg (map_syntax (Syntax.extend_consts names) syn, - Type.ext_tsig_classes tsig classes', ctab, (path, spaces'), data) + Type.add_classes classes' tsig, ctab, (path, spaces'), data) consts end; @@ -1040,7 +1036,7 @@ fun ext_classrel int _ (syn, tsig, ctab, (path, spaces), data) pairs = let val intrn = if int then map (pairself (intrn_class spaces)) else I in - (syn, Type.ext_tsig_classrel tsig (intrn pairs), ctab, (path, spaces), data) + (syn, Type.add_classrel (intrn pairs) tsig, ctab, (path, spaces), data) end; @@ -1116,13 +1112,13 @@ fun copy_data (k, (e, mths as (cp, _, _, _))) = (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths)); -fun copy (sg as Sg ({id = _, stamps, syn}, {self, tsig, const_tab, path, spaces, data})) = +fun copy (sg as Sg ({id = _, stamps, syn}, {self, tsig, consts, path, spaces, data})) = let val _ = check_stale sg; val self' = SgRef (Some (ref sg)); val Data tab = data; val data' = Data (Symtab.map copy_data tab); - in create_sign self' stamps "#" (syn, tsig, const_tab, (path, spaces), data') end; + in create_sign self' stamps "#" (syn, tsig, consts, (path, spaces), data') end; (* the external interfaces *) @@ -1204,10 +1200,10 @@ else let val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)}, - {self = _, tsig = tsig1, const_tab = const_tab1, + {self = _, tsig = tsig1, consts = consts1, path = _, spaces = spaces1, data = data1}) = sg1; val Sg ({id = _, stamps = stamps2, syn = Syn (syntax2, trfuns2)}, - {self = _, tsig = tsig2, const_tab = const_tab2, + {self = _, tsig = tsig2, consts = consts2, path = _, spaces = spaces2, data = data2}) = sg2; val id = ref ""; @@ -1218,9 +1214,8 @@ val syntax = Syntax.merge_syntaxes syntax1 syntax2; val trfuns = merge_trfuns trfuns1 trfuns2; val tsig = Type.merge_tsigs (tsig1, tsig2); - val const_tab = Symtab.merge (op =) (const_tab1, const_tab2) - handle Symtab.DUPS cs => - raise TERM ("Incompatible types for constant(s) " ^ commas_quote cs, []); + val consts = Symtab.merge eq_snd (consts1, consts2) + handle Symtab.DUPS cs => err_dup_consts cs; val path = Some []; val kinds = distinct (map fst (spaces1 @ spaces2)); @@ -1231,7 +1226,7 @@ val data = merge_data (data1, data2); - val sign = make_sign (id, self, tsig, const_tab, Syn (syntax, trfuns), + val sign = make_sign (id, self, tsig, consts, Syn (syntax, trfuns), path, spaces, data, stamps); in self_ref := sign; syn_of sign; sign end;