wenzelm@19: (* Title: Pure/sign.ML clasohm@0: ID: $Id$ wenzelm@251: Author: Lawrence C Paulson and Markus Wenzel clasohm@0: wenzelm@251: The abstract type "sg" of signatures. clasohm@0: *) clasohm@0: wenzelm@19: signature SIGN = paulson@1501: sig paulson@1501: type sg wenzelm@2197: val rep_sg: sg -> wenzelm@2197: {tsig: Type.type_sig, wenzelm@2197: const_tab: typ Symtab.table, wenzelm@2197: syn: Syntax.syntax, wenzelm@2197: stamps: string ref list} paulson@1501: val subsig: sg * sg -> bool paulson@1501: val eq_sg: sg * sg -> bool paulson@1501: val same_sg: sg * sg -> bool paulson@1501: val is_draft: sg -> bool paulson@1501: val const_type: sg -> string -> typ option paulson@1501: val classes: sg -> class list paulson@1501: val subsort: sg -> sort * sort -> bool paulson@1501: val nodup_Vars: term -> unit paulson@1501: val norm_sort: sg -> sort -> sort paulson@1501: val nonempty_sort: sg -> sort list -> sort -> bool paulson@1501: val print_sg: sg -> unit paulson@1501: val pretty_sg: sg -> Pretty.T paulson@1501: val pprint_sg: sg -> pprint_args -> unit paulson@1501: val pretty_term: sg -> term -> Pretty.T paulson@1501: val pretty_typ: sg -> typ -> Pretty.T paulson@1501: val pretty_sort: sort -> Pretty.T paulson@1501: val string_of_term: sg -> term -> string paulson@1501: val string_of_typ: sg -> typ -> string paulson@1501: val pprint_term: sg -> term -> pprint_args -> unit paulson@1501: val pprint_typ: sg -> typ -> pprint_args -> unit paulson@1501: val certify_typ: sg -> typ -> typ paulson@1501: val certify_term: sg -> term -> term * typ * int paulson@1501: val read_typ: sg * (indexname -> sort option) -> string -> typ paulson@1501: val infer_types: sg -> (indexname -> typ option) -> paulson@1501: (indexname -> sort option) -> string list -> bool paulson@1501: -> term list * typ -> int * term * (indexname * typ) list paulson@1501: val add_classes: (class * class list) list -> sg -> sg paulson@1501: val add_classrel: (class * class) list -> sg -> sg paulson@1501: val add_defsort: sort -> sg -> sg paulson@1501: val add_types: (string * int * mixfix) list -> sg -> sg paulson@1501: val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg paulson@1501: val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg paulson@1501: val add_arities: (string * sort list * sort) list -> sg -> sg paulson@1501: val add_consts: (string * string * mixfix) list -> sg -> sg paulson@1501: val add_consts_i: (string * typ * mixfix) list -> sg -> sg paulson@1501: val add_syntax: (string * string * mixfix) list -> sg -> sg paulson@1501: val add_syntax_i: (string * typ * mixfix) list -> sg -> sg wenzelm@2359: val add_modesyntax: (string * bool) * (string * string * mixfix) list -> sg -> sg wenzelm@2359: val add_modesyntax_i: (string * bool) * (string * typ * mixfix) list -> sg -> sg paulson@1501: val add_trfuns: paulson@1501: (string * (ast list -> ast)) list * paulson@1501: (string * (term list -> term)) list * paulson@1501: (string * (term list -> term)) list * paulson@1501: (string * (ast list -> ast)) list -> sg -> sg wenzelm@2385: val add_trfunsT: wenzelm@2385: (string * (typ -> term list -> term)) list -> sg -> sg wenzelm@2693: val add_tokentrfuns: wenzelm@2693: (string * string * (string -> string * int)) list -> sg -> sg paulson@1810: val add_trrules: (string * string) Syntax.trrule list -> sg -> sg paulson@1810: val add_trrules_i: ast Syntax.trrule list -> sg -> sg paulson@1501: val add_name: string -> sg -> sg paulson@1501: val make_draft: sg -> sg paulson@1501: val merge: sg * sg -> sg paulson@1501: val proto_pure: sg paulson@1501: val pure: sg paulson@1501: val cpure: sg paulson@1501: val const_of_class: class -> string paulson@1501: val class_of_const: string -> class paulson@1501: end; clasohm@0: paulson@1501: structure Sign : SIGN = wenzelm@143: struct clasohm@0: wenzelm@2979: wenzelm@251: (** datatype sg **) wenzelm@251: wenzelm@251: (*the "ref" in stamps ensures that no two signatures are identical -- it is wenzelm@251: impossible to forge a signature*) wenzelm@143: wenzelm@19: datatype sg = wenzelm@143: Sg of { wenzelm@2185: tsig: Type.type_sig, (*order-sorted signature of types*) wenzelm@143: const_tab: typ Symtab.table, (*types of constants*) wenzelm@143: syn: Syntax.syntax, (*syntax for parsing and printing*) wenzelm@143: stamps: string ref list}; (*unique theory indentifier*) clasohm@0: clasohm@0: fun rep_sg (Sg args) = args; wenzelm@402: val tsig_of = #tsig o rep_sg; clasohm@0: nipkow@206: wenzelm@2979: (* inclusion and equality *) paulson@2180: wenzelm@2185: local wenzelm@2185: (*avoiding polymorphic equality: factor 10 speedup*) wenzelm@2185: fun mem_stamp (_:string ref, []) = false wenzelm@2185: | mem_stamp (x, y :: ys) = x = y orelse mem_stamp (x, ys); wenzelm@2185: wenzelm@2185: fun subset_stamp ([], ys) = true wenzelm@2185: | subset_stamp (x :: xs, ys) = wenzelm@2185: mem_stamp (x, ys) andalso subset_stamp (xs, ys); paulson@2180: wenzelm@2185: (*fast partial test*) wenzelm@2185: fun fast_sub ([]: string ref list, _) = true wenzelm@2185: | fast_sub (_, []) = false wenzelm@2185: | fast_sub (x :: xs, y :: ys) = wenzelm@2185: if x = y then fast_sub (xs, ys) wenzelm@2185: else fast_sub (x :: xs, ys); wenzelm@2185: in wenzelm@2185: fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = wenzelm@2185: s1 = s2 orelse subset_stamp (s1, s2); wenzelm@2185: wenzelm@2185: fun fast_subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = wenzelm@2185: s1 = s2 orelse fast_sub (s1, s2); paulson@2180: wenzelm@2185: fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = wenzelm@2185: s1 = s2 orelse (subset_stamp (s1, s2) andalso subset_stamp (s2, s1)); wenzelm@2185: end; wenzelm@2185: wenzelm@402: wenzelm@2185: (*test if same theory names are contained in signatures' stamps, wenzelm@2185: i.e. if signatures belong to same theory but not necessarily to the wenzelm@2185: same version of it*) wenzelm@2185: fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = wenzelm@2185: eq_set_string (pairself (map (op !)) (s1, s2)); wenzelm@2185: wenzelm@2185: (*test for drafts*) wenzelm@386: fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true wenzelm@386: | is_draft _ = false; wenzelm@386: clasohm@0: wenzelm@402: (* consts *) wenzelm@402: wenzelm@2979: fun const_type (Sg {const_tab, ...}) c = Symtab.lookup (const_tab, c); wenzelm@386: wenzelm@386: wenzelm@620: (* classes and sorts *) wenzelm@402: wenzelm@402: val classes = #classes o Type.rep_tsig o tsig_of; wenzelm@402: wenzelm@402: val subsort = Type.subsort o tsig_of; wenzelm@402: val norm_sort = Type.norm_sort o tsig_of; wenzelm@1216: val nonempty_sort = Type.nonempty_sort o tsig_of; wenzelm@402: wenzelm@2979: (* FIXME move to Sorts? *) wenzelm@620: fun pretty_sort [c] = Pretty.str c wenzelm@620: | pretty_sort cs = Pretty.str_list "{" "}" cs; wenzelm@620: wenzelm@402: clasohm@0: wenzelm@251: (** print signature **) wenzelm@251: paulson@2228: fun stamp_names stamps = rev (map ! stamps); wenzelm@386: wenzelm@251: fun print_sg sg = wenzelm@251: let wenzelm@251: fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty); wenzelm@251: wenzelm@2963: fun pretty_classrel (cl, cls) = Pretty.block wenzelm@1216: (Pretty.str (cl ^ " <") :: Pretty.brk 1 :: wenzelm@1216: Pretty.commas (map Pretty.str cls)); wenzelm@251: wenzelm@251: fun pretty_default cls = Pretty.block wenzelm@251: [Pretty.str "default:", Pretty.brk 1, pretty_sort cls]; wenzelm@251: nipkow@963: fun pretty_ty (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n); wenzelm@251: wenzelm@251: fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block wenzelm@620: [prt_typ syn (Type (ty, map (fn v => TVar ((v, 0), [])) vs)), wenzelm@251: Pretty.str " =", Pretty.brk 1, prt_typ syn rhs]; wenzelm@251: wenzelm@251: fun pretty_arity ty (cl, []) = Pretty.block wenzelm@251: [Pretty.str (ty ^ " ::"), Pretty.brk 1, Pretty.str cl] wenzelm@251: | pretty_arity ty (cl, srts) = Pretty.block wenzelm@251: [Pretty.str (ty ^ " ::"), Pretty.brk 1, wenzelm@251: Pretty.list "(" ")" (map pretty_sort srts), wenzelm@251: Pretty.brk 1, Pretty.str cl]; wenzelm@251: nipkow@963: fun pretty_arities (ty, ars) = map (pretty_arity ty) ars; wenzelm@251: wenzelm@251: fun pretty_const syn (c, ty) = Pretty.block wenzelm@266: [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty]; wenzelm@251: wenzelm@251: wenzelm@251: val Sg {tsig, const_tab, syn, stamps} = sg; wenzelm@2963: val {classes, classrel, default, tycons, abbrs, arities} = wenzelm@2185: Type.rep_tsig tsig; wenzelm@251: in wenzelm@386: Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps)); wenzelm@251: Pretty.writeln (Pretty.strs ("classes:" :: classes)); wenzelm@2979: Pretty.writeln (Pretty.big_list "classrel:" (map pretty_classrel classrel)); wenzelm@251: Pretty.writeln (pretty_default default); nipkow@963: Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons)); wenzelm@251: Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs)); nipkow@963: Pretty.writeln (Pretty.big_list "arities:" wenzelm@2979: (List.concat (map pretty_arities arities))); wenzelm@251: Pretty.writeln (Pretty.big_list "consts:" wenzelm@2979: (map (pretty_const syn) (Symtab.dest const_tab))) wenzelm@251: end; wenzelm@251: wenzelm@251: wenzelm@562: fun pretty_sg (Sg {stamps, ...}) = wenzelm@562: Pretty.str_list "{" "}" (stamp_names stamps); wenzelm@562: wenzelm@562: val pprint_sg = Pretty.pprint o pretty_sg; wenzelm@251: wenzelm@251: wenzelm@251: wenzelm@251: (** pretty printing of terms and types **) wenzelm@251: clasohm@922: fun pretty_term (Sg {syn, stamps, ...}) = paulson@2138: let val curried = "CPure" mem_string (map ! stamps); clasohm@922: in Syntax.pretty_term curried syn end; clasohm@922: wenzelm@251: fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn; wenzelm@251: wenzelm@1239: fun string_of_term (Sg {syn, stamps, ...}) = paulson@2138: let val curried = "CPure" mem_string (map ! stamps); clasohm@922: in Syntax.string_of_term curried syn end; clasohm@922: wenzelm@251: fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn; wenzelm@251: wenzelm@251: fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg); wenzelm@251: fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg); clasohm@0: clasohm@0: wenzelm@169: wenzelm@562: (** read types **) (*exception ERROR*) wenzelm@562: wenzelm@562: fun err_in_type s = wenzelm@562: error ("The error(s) above occurred in type " ^ quote s); wenzelm@562: wenzelm@562: fun read_raw_typ syn tsig sort_of str = wenzelm@2586: Syntax.read_typ syn (Type.eq_sort tsig) (Type.get_sort tsig sort_of) str wenzelm@562: handle ERROR => err_in_type str; wenzelm@562: wenzelm@562: (*read and certify typ wrt a signature*) wenzelm@562: fun read_typ (Sg {tsig, syn, ...}, sort_of) str = wenzelm@2185: Type.cert_typ tsig (read_raw_typ syn tsig sort_of str) wenzelm@562: handle TYPE (msg, _, _) => (writeln msg; err_in_type str); wenzelm@562: wenzelm@562: wenzelm@562: wenzelm@386: (** certify types and terms **) (*exception TYPE*) wenzelm@251: wenzelm@2185: fun certify_typ (Sg {tsig, ...}) ty = Type.cert_typ tsig ty; wenzelm@251: wenzelm@2979: (*check for duplicate TVars with distinct sorts*) wenzelm@2979: fun nodup_TVars (tvars, T) = wenzelm@2979: (case T of wenzelm@2979: Type (_, Ts) => nodup_TVars_list (tvars, Ts) wenzelm@2979: | TFree _ => tvars wenzelm@2979: | TVar (v as (a, S)) => wenzelm@2979: (case assoc_string_int (tvars, a) of wenzelm@2979: Some S' => wenzelm@2979: if S = S' then tvars wenzelm@2979: else raise_type ("Type variable " ^ Syntax.string_of_vname a ^ wenzelm@2979: " has two distinct sorts") [TVar (a, S'), T] [] wenzelm@2979: | None => v :: tvars)) wenzelm@2979: (*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*) wenzelm@2979: and nodup_TVars_list (tvars, []) = tvars wenzelm@2979: | nodup_TVars_list (tvars, T :: Ts) = wenzelm@2979: nodup_TVars_list (nodup_TVars (tvars, T), Ts); nipkow@1494: wenzelm@2979: (*check for duplicate Vars with distinct types*) nipkow@1494: fun nodup_Vars tm = wenzelm@2979: let wenzelm@2979: fun nodups vars tvars tm = wenzelm@2979: (case tm of wenzelm@2979: Const (c, T) => (vars, nodup_TVars (tvars, T)) wenzelm@2979: | Free (a, T) => (vars, nodup_TVars (tvars, T)) wenzelm@2979: | Var (v as (ixn, T)) => wenzelm@2979: (case assoc_string_int (vars, ixn) of wenzelm@2979: Some T' => wenzelm@2979: if T = T' then (vars, nodup_TVars (tvars, T)) wenzelm@2979: else raise_type ("Variable " ^ Syntax.string_of_vname ixn ^ wenzelm@2979: " has two distinct types") [T', T] [] wenzelm@2979: | None => (v :: vars, tvars)) wenzelm@2979: | Bound _ => (vars, tvars) wenzelm@2979: | Abs(_, T, t) => nodups vars (nodup_TVars (tvars, T)) t wenzelm@2979: | s $ t => wenzelm@2979: let val (vars',tvars') = nodups vars tvars s in wenzelm@2979: nodups vars' tvars' t wenzelm@2979: end); wenzelm@2979: in nodups [] [] tm; () end; wenzelm@2979: wenzelm@251: wenzelm@386: fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t wenzelm@386: | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u wenzelm@386: | mapfilt_atoms f a = (case f a of Some y => [y] | None => []); clasohm@0: wenzelm@2979: wenzelm@386: fun certify_term (sg as Sg {tsig, ...}) tm = wenzelm@251: let wenzelm@251: fun valid_const a T = wenzelm@386: (case const_type sg a of wenzelm@2185: Some U => Type.typ_instance (tsig, T, U) wenzelm@251: | _ => false); wenzelm@169: wenzelm@251: fun atom_err (Const (a, T)) = wenzelm@251: if valid_const a T then None wenzelm@251: else Some ("Illegal type for constant " ^ quote a ^ " :: " ^ wenzelm@251: quote (string_of_typ sg T)) wenzelm@251: | atom_err (Var ((x, i), _)) = wenzelm@251: if i < 0 then Some ("Negative index for Var " ^ quote x) else None wenzelm@251: | atom_err _ = None; wenzelm@251: wenzelm@251: val norm_tm = wenzelm@2185: (case it_term_types (Type.typ_errors tsig) (tm, []) of wenzelm@2185: [] => map_term_types (Type.norm_typ tsig) tm wenzelm@251: | errs => raise_type (cat_lines errs) [] [tm]); nipkow@1494: val _ = nodup_Vars norm_tm; wenzelm@251: in wenzelm@386: (case mapfilt_atoms atom_err norm_tm of wenzelm@251: [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm) wenzelm@251: | errs => raise_type (cat_lines errs) [] [norm_tm]) wenzelm@251: end; wenzelm@251: wenzelm@251: wenzelm@251: wenzelm@583: (** infer_types **) (*exception ERROR*) wenzelm@251: wenzelm@2979: (* wenzelm@2979: ts: list of alternative parses (hopefully only one is type-correct) wenzelm@2979: T: expected type wenzelm@2979: wenzelm@2979: def_type: partial map from indexnames to types (constrains Frees, Vars) wenzelm@2979: def_sort: partial map from indexnames to sorts (constrains TFrees, TVars) wenzelm@2979: used: list of already used type variables wenzelm@2979: freeze: if true then generated parameters are turned into TFrees, else TVars wenzelm@2979: *) wenzelm@2979: wenzelm@2979: fun infer_types sg def_type def_sort used freeze (ts, T) = wenzelm@251: let wenzelm@562: val Sg {tsig, ...} = sg; wenzelm@2979: val prt = setmp Syntax.show_brackets true (pretty_term sg); wenzelm@2979: val prT = pretty_typ sg; wenzelm@2979: val infer = Type.infer_types prt prT tsig (const_type sg) wenzelm@2979: def_type def_sort used freeze; wenzelm@169: wenzelm@2979: val T' = certify_typ sg T handle TYPE (msg, _, _) => error msg; clasohm@623: wenzelm@2979: fun warn () = wenzelm@2979: if length ts > 1 andalso length ts <= ! Syntax.ambiguity_level nipkow@952: then (*no warning shown yet*) wenzelm@2979: warning "Currently parsed input \ wenzelm@2979: \produces more than one parse tree.\n\ wenzelm@2979: \For more information lower Syntax.ambiguity_level." nipkow@952: else (); clasohm@623: wenzelm@2979: datatype result = wenzelm@2979: One of int * term * (indexname * typ) list | wenzelm@2979: Errs of string list | wenzelm@2979: Ambigs of term list; clasohm@623: wenzelm@2979: fun process_term (res, (t, i)) = wenzelm@2979: let val ([u], tye) = infer [T'] [t] in wenzelm@2979: (case res of wenzelm@2979: One (_, t0, _) => Ambigs ([u, t0]) wenzelm@2979: | Errs _ => One (i, u, tye) wenzelm@2979: | Ambigs us => Ambigs (u :: us)) wenzelm@2979: end handle TYPE (msg, _, _) => wenzelm@2979: (case res of wenzelm@2979: Errs errs => Errs (msg :: errs) wenzelm@2979: | _ => res); wenzelm@2979: in wenzelm@2979: (case foldl process_term (Errs [], ts ~~ (0 upto (length ts - 1))) of wenzelm@2979: One res => wenzelm@2979: (if length ts > ! Syntax.ambiguity_level then wenzelm@2979: writeln "Fortunately, only one parse tree is type correct.\n\ nipkow@952: \It helps (speed!) if you disambiguate your grammar or your input." wenzelm@2979: else (); res) wenzelm@2979: | Errs errs => (warn (); error (cat_lines errs)) wenzelm@2979: | Ambigs us => wenzelm@2979: (warn (); error ("Error: More than one term is type correct:\n" ^ wenzelm@2979: (cat_lines (map (Pretty.string_of o prt) us))))) clasohm@623: end; wenzelm@251: wenzelm@251: wenzelm@2979: clasohm@623: (** extend signature **) (*exception ERROR*) clasohm@623: wenzelm@620: (** signature extension functions **) (*exception ERROR*) wenzelm@386: wenzelm@386: fun decls_of name_of mfixs = wenzelm@386: map (fn (x, y, mx) => (name_of x mx, y)) mfixs; wenzelm@386: wenzelm@386: wenzelm@386: (* add default sort *) wenzelm@386: wenzelm@386: fun ext_defsort (syn, tsig, ctab) defsort = wenzelm@2185: (syn, Type.ext_tsig_defsort tsig defsort, ctab); wenzelm@386: wenzelm@386: wenzelm@386: (* add type constructors *) wenzelm@386: wenzelm@386: fun ext_types (syn, tsig, ctab) types = wenzelm@386: (Syntax.extend_type_gram syn types, wenzelm@2185: Type.ext_tsig_types tsig (decls_of Syntax.type_name types), wenzelm@386: ctab); wenzelm@386: wenzelm@386: wenzelm@386: (* add type abbreviations *) wenzelm@386: wenzelm@386: fun read_abbr syn tsig (t, vs, rhs_src) = wenzelm@386: (t, vs, read_raw_typ syn tsig (K None) rhs_src) wenzelm@386: handle ERROR => error ("in type abbreviation " ^ t); wenzelm@386: wenzelm@386: fun ext_abbrs rd_abbr (syn, tsig, ctab) abbrs = wenzelm@386: let wenzelm@386: fun mfix_of (t, vs, _, mx) = (t, length vs, mx); wenzelm@386: val syn1 = Syntax.extend_type_gram syn (map mfix_of abbrs); wenzelm@386: wenzelm@386: fun decl_of (t, vs, rhs, mx) = wenzelm@562: rd_abbr syn1 tsig (Syntax.type_name t mx, vs, rhs); wenzelm@386: in wenzelm@2185: (syn1, Type.ext_tsig_abbrs tsig (map decl_of abbrs), ctab) wenzelm@386: end; wenzelm@386: paulson@2228: fun ext_tyabbrs_i arg = ext_abbrs (K (K I)) arg; paulson@2228: fun ext_tyabbrs arg = ext_abbrs read_abbr arg; wenzelm@386: wenzelm@386: wenzelm@386: (* add type arities *) wenzelm@386: wenzelm@386: fun ext_arities (syn, tsig, ctab) arities = wenzelm@386: let wenzelm@2185: val tsig1 = Type.ext_tsig_arities tsig arities; wenzelm@2185: val log_types = Type.logical_types tsig1; wenzelm@386: in wenzelm@386: (Syntax.extend_log_types syn log_types, tsig1, ctab) wenzelm@386: end; wenzelm@386: wenzelm@386: wenzelm@386: (* add term constants and syntax *) wenzelm@386: wenzelm@386: fun err_in_const c = wenzelm@386: error ("in declaration of constant " ^ quote c); wenzelm@386: wenzelm@386: fun err_dup_consts cs = wenzelm@386: error ("Duplicate declaration of constant(s) " ^ commas_quote cs); wenzelm@386: wenzelm@251: wenzelm@386: fun read_const syn tsig (c, ty_src, mx) = wenzelm@386: (c, read_raw_typ syn tsig (K None) ty_src, mx) wenzelm@562: handle ERROR => err_in_const (Syntax.const_name c mx); wenzelm@386: wenzelm@2197: fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab) raw_consts = wenzelm@386: let wenzelm@2979: fun prep_const (c, ty, mx) = wenzelm@2185: (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx) wenzelm@2185: handle TYPE (msg, _, _) wenzelm@2185: => (writeln msg; err_in_const (Syntax.const_name c mx)); wenzelm@386: wenzelm@386: val consts = map (prep_const o rd_const syn tsig) raw_consts; wenzelm@386: val decls = wenzelm@386: if syn_only then [] wenzelm@562: else filter_out (equal "" o fst) (decls_of Syntax.const_name consts); wenzelm@386: in wenzelm@2197: (Syntax.extend_const_gram syn prmode consts, tsig, wenzelm@386: Symtab.extend_new (ctab, decls) wenzelm@386: handle Symtab.DUPS cs => err_dup_consts cs) wenzelm@386: end; wenzelm@386: wenzelm@2359: val ext_consts_i = ext_cnsts (K (K I)) false ("", true); wenzelm@2359: val ext_consts = ext_cnsts read_const false ("", true); wenzelm@2359: val ext_syntax_i = ext_cnsts (K (K I)) true ("", true); wenzelm@2359: val ext_syntax = ext_cnsts read_const true ("", true); wenzelm@2197: fun ext_modesyntax_i sg (prmode, consts) = ext_cnsts (K (K I)) true prmode sg consts; wenzelm@2197: fun ext_modesyntax sg (prmode, consts) = ext_cnsts read_const true prmode sg consts; wenzelm@386: wenzelm@386: wenzelm@386: (* add type classes *) wenzelm@386: wenzelm@386: fun const_of_class c = c ^ "_class"; wenzelm@386: wenzelm@386: fun class_of_const c_class = wenzelm@386: let wenzelm@386: val c = implode (take (size c_class - 6, explode c_class)); wenzelm@386: in wenzelm@386: if const_of_class c = c_class then c wenzelm@386: else raise_term ("class_of_const: bad name " ^ quote c_class) [] wenzelm@386: end; wenzelm@386: wenzelm@386: wenzelm@386: fun ext_classes (syn, tsig, ctab) classes = wenzelm@386: let wenzelm@562: val names = map fst classes; wenzelm@386: val consts = wenzelm@386: map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names; wenzelm@386: in wenzelm@386: ext_consts_i wenzelm@2185: (Syntax.extend_consts syn names, Type.ext_tsig_classes tsig classes, ctab) wenzelm@386: consts wenzelm@386: end; wenzelm@386: wenzelm@386: wenzelm@2963: (* add to classrel *) wenzelm@421: wenzelm@421: fun ext_classrel (syn, tsig, ctab) pairs = wenzelm@2963: (syn, Type.ext_tsig_classrel tsig pairs, ctab); wenzelm@421: wenzelm@421: wenzelm@1159: (* add to syntax *) wenzelm@386: wenzelm@1159: fun ext_syn extfun (syn, tsig, ctab) args = wenzelm@1159: (extfun syn args, tsig, ctab); wenzelm@386: wenzelm@386: wenzelm@386: (* build signature *) wenzelm@386: wenzelm@386: fun ext_stamps stamps name = wenzelm@386: let wenzelm@386: val stmps = (case stamps of ref "#" :: ss => ss | ss => ss); wenzelm@386: in wenzelm@386: if exists (equal name o !) stmps then wenzelm@386: error ("Theory already contains a " ^ quote name ^ " component") wenzelm@402: else ref name :: stmps wenzelm@386: end; wenzelm@386: wenzelm@386: fun make_sign (syn, tsig, ctab) stamps name = wenzelm@386: Sg {tsig = tsig, const_tab = ctab, syn = syn, wenzelm@386: stamps = ext_stamps stamps name}; wenzelm@386: wenzelm@386: fun extend_sign extfun name decls (Sg {tsig, const_tab, syn, stamps}) = wenzelm@386: make_sign (extfun (syn, tsig, const_tab) decls) stamps name; wenzelm@386: wenzelm@386: wenzelm@386: (* the external interfaces *) wenzelm@386: wenzelm@2197: val add_classes = extend_sign ext_classes "#"; wenzelm@2197: val add_classrel = extend_sign ext_classrel "#"; wenzelm@2197: val add_defsort = extend_sign ext_defsort "#"; wenzelm@2197: val add_types = extend_sign ext_types "#"; wenzelm@2197: val add_tyabbrs = extend_sign ext_tyabbrs "#"; wenzelm@2197: val add_tyabbrs_i = extend_sign ext_tyabbrs_i "#"; wenzelm@2197: val add_arities = extend_sign ext_arities "#"; wenzelm@2197: val add_consts = extend_sign ext_consts "#"; wenzelm@2197: val add_consts_i = extend_sign ext_consts_i "#"; wenzelm@2197: val add_syntax = extend_sign ext_syntax "#"; wenzelm@2197: val add_syntax_i = extend_sign ext_syntax_i "#"; wenzelm@2197: val add_modesyntax = extend_sign ext_modesyntax "#"; wenzelm@2197: val add_modesyntax_i = extend_sign ext_modesyntax_i "#"; wenzelm@2197: val add_trfuns = extend_sign (ext_syn Syntax.extend_trfuns) "#"; wenzelm@2385: val add_trfunsT = extend_sign (ext_syn Syntax.extend_trfunsT) "#"; wenzelm@2693: val add_tokentrfuns = extend_sign (ext_syn Syntax.extend_tokentrfuns) "#"; wenzelm@2197: val add_trrules = extend_sign (ext_syn Syntax.extend_trrules) "#"; wenzelm@2197: val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#"; wenzelm@386: wenzelm@386: fun add_name name sg = extend_sign K name () sg; wenzelm@386: val make_draft = add_name "#"; wenzelm@386: wenzelm@386: wenzelm@386: wenzelm@620: (** merge signatures **) (*exception TERM*) (*exception ERROR (* FIXME *)*) wenzelm@143: wenzelm@251: fun merge (sg1, sg2) = wenzelm@2185: if fast_subsig (sg2, sg1) then sg1 wenzelm@2185: else if fast_subsig (sg1, sg2) then sg2 wenzelm@2185: else if subsig (sg2, sg1) then sg1 wenzelm@251: else if subsig (sg1, sg2) then sg2 wenzelm@386: else if is_draft sg1 orelse is_draft sg2 then wenzelm@386: raise_term "Illegal merge of draft signatures" [] wenzelm@251: else wenzelm@251: (*neither is union already; must form union*) wenzelm@251: let wenzelm@251: val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, wenzelm@251: stamps = stamps1} = sg1; wenzelm@251: val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2, wenzelm@251: stamps = stamps2} = sg2; wenzelm@251: wenzelm@386: wenzelm@402: val stamps = merge_rev_lists stamps1 stamps2; wenzelm@402: val _ = wenzelm@402: (case duplicates (stamp_names stamps) of wenzelm@402: [] => () wenzelm@402: | dups => raise_term ("Attempt to merge different versions of theories " wenzelm@402: ^ commas_quote dups) []); wenzelm@402: wenzelm@2185: val tsig = Type.merge_tsigs (tsig1, tsig2); wenzelm@251: wenzelm@251: val const_tab = Symtab.merge (op =) (const_tab1, const_tab2) wenzelm@386: handle Symtab.DUPS cs => wenzelm@386: raise_term ("Incompatible types for constant(s) " ^ commas_quote cs) []; wenzelm@386: wenzelm@386: val syn = Syntax.merge_syntaxes syn1 syn2; wenzelm@251: in wenzelm@251: Sg {tsig = tsig, const_tab = const_tab, syn = syn, stamps = stamps} wenzelm@251: end; wenzelm@143: clasohm@0: clasohm@0: wenzelm@251: (** the Pure signature **) clasohm@0: clasohm@922: val proto_pure = wenzelm@2185: make_sign (Syntax.pure_syn, Type.tsig0, Symtab.null) [] "#" wenzelm@410: |> add_types wenzelm@386: (("fun", 2, NoSyn) :: wenzelm@386: ("prop", 0, NoSyn) :: wenzelm@386: ("itself", 1, NoSyn) :: wenzelm@562: Syntax.pure_types) wenzelm@562: |> add_classes [(logicC, [])] wenzelm@410: |> add_defsort logicS wenzelm@410: |> add_arities wenzelm@386: [("fun", [logicS, logicS], logicS), wenzelm@386: ("prop", [], logicS), wenzelm@386: ("itself", [logicS], logicS)] wenzelm@562: |> add_syntax Syntax.pure_syntax wenzelm@2359: |> add_modesyntax (("symbols", true), Syntax.pure_sym_syntax) wenzelm@410: |> add_trfuns Syntax.pure_trfuns wenzelm@2693: |> add_trfunsT Syntax.pure_trfunsT wenzelm@410: |> add_consts wenzelm@2197: [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)), wenzelm@2197: ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)), wenzelm@2211: ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), clasohm@865: ("all", "('a => prop) => prop", Binder ("!!", 0, 0)), wenzelm@573: ("TYPE", "'a itself", NoSyn)] wenzelm@2211: |> add_syntax wenzelm@2211: [("==>", "[prop, prop] => prop", Delimfix "op ==>")] clasohm@922: |> add_name "ProtoPure"; clasohm@922: clasohm@922: val pure = proto_pure clasohm@1180: |> add_syntax Syntax.pure_appl_syntax wenzelm@410: |> add_name "Pure"; clasohm@0: clasohm@922: val cpure = proto_pure clasohm@1180: |> add_syntax Syntax.pure_applC_syntax clasohm@922: |> add_name "CPure"; clasohm@0: clasohm@0: end;