paulson@1526: (*  Title:      Pure/theory.ML
paulson@1526:     ID:         $Id$
paulson@1526:     Author:     Lawrence C Paulson and Markus Wenzel
paulson@1526: 
wenzelm@5025: The abstract type "theory" of theories.
paulson@1526: *)
wenzelm@3767: signature BASIC_THEORY =
wenzelm@3767: sig
paulson@1526:   type theory
paulson@1526:   exception THEORY of string * theory list
wenzelm@3996:   val rep_theory: theory ->
wenzelm@3814:     {sign: Sign.sg,
obua@16108:       const_deps: Defs.graph,
wenzelm@3996:       axioms: term Symtab.table,
wenzelm@4996:       oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
wenzelm@4019:       parents: theory list,
wenzelm@4019:       ancestors: theory list}
wenzelm@3996:   val sign_of: theory -> Sign.sg
wenzelm@6188:   val is_draft: theory -> bool
wenzelm@3996:   val syn_of: theory -> Syntax.syntax
wenzelm@3996:   val parents_of: theory -> theory list
wenzelm@4019:   val ancestors_of: theory -> theory list
wenzelm@3996:   val subthy: theory * theory -> bool
wenzelm@3996:   val eq_thy: theory * theory -> bool
wenzelm@3996:   val cert_axm: Sign.sg -> string * term -> string * term
wenzelm@6311:   val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
wenzelm@6311:     string list -> string * string -> string * term
wenzelm@3996:   val read_axm: Sign.sg -> string * string -> string * term
wenzelm@3996:   val inferT_axm: Sign.sg -> string * term -> string * term
wenzelm@3767: end
wenzelm@3767: 
wenzelm@3767: signature THEORY =
wenzelm@3767: sig
wenzelm@3767:   include BASIC_THEORY
wenzelm@3996:   val axiomK: string
wenzelm@3996:   val oracleK: string
wenzelm@4912:   (*theory extension primitives*)
wenzelm@3996:   val add_classes: (bclass * xclass list) list -> theory -> theory
wenzelm@3996:   val add_classes_i: (bclass * class list) list -> theory -> theory
wenzelm@3996:   val add_classrel: (xclass * xclass) list -> theory -> theory
wenzelm@3996:   val add_classrel_i: (class * class) list -> theory -> theory
wenzelm@8897:   val add_defsort: string -> theory -> theory
wenzelm@3996:   val add_defsort_i: sort -> theory -> theory
wenzelm@3996:   val add_types: (bstring * int * mixfix) list -> theory -> theory
wenzelm@4846:   val add_nonterminals: bstring list -> theory -> theory
wenzelm@3996:   val add_tyabbrs: (bstring * string list * string * mixfix) list
paulson@1526:     -> theory -> theory
wenzelm@3996:   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
paulson@1526:     -> theory -> theory
wenzelm@8897:   val add_arities: (xstring * string list * string) list -> theory -> theory
wenzelm@3996:   val add_arities_i: (string * sort list * sort) list -> theory -> theory
wenzelm@3996:   val add_consts: (bstring * string * mixfix) list -> theory -> theory
wenzelm@3996:   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
wenzelm@3996:   val add_syntax: (bstring * string * mixfix) list -> theory -> theory
wenzelm@3996:   val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
wenzelm@3996:   val add_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
wenzelm@3996:   val add_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
wenzelm@15747:   val del_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
wenzelm@15747:   val del_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
wenzelm@3996:   val add_trfuns:
wenzelm@4344:     (string * (Syntax.ast list -> Syntax.ast)) list *
wenzelm@4344:     (string * (term list -> term)) list *
wenzelm@4344:     (string * (term list -> term)) list *
wenzelm@4344:     (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
wenzelm@3996:   val add_trfunsT:
wenzelm@4344:     (string * (bool -> typ -> term list -> term)) list -> theory -> theory
wenzelm@14645:   val add_advanced_trfuns:
wenzelm@14645:     (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list *
wenzelm@14645:     (string * (Sign.sg -> term list -> term)) list *
wenzelm@14645:     (string * (Sign.sg -> term list -> term)) list *
wenzelm@14645:     (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list -> theory -> theory
wenzelm@14645:   val add_advanced_trfunsT:
wenzelm@14645:     (string * (Sign.sg -> bool -> typ -> term list -> term)) list -> theory -> theory
wenzelm@2693:   val add_tokentrfuns:
wenzelm@6311:     (string * string * (string -> string * real)) list -> theory -> theory
wenzelm@6311:   val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
wenzelm@6311:     -> theory -> theory
wenzelm@4617:   val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
wenzelm@3996:   val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
wenzelm@3996:   val add_axioms: (bstring * string) list -> theory -> theory
wenzelm@3996:   val add_axioms_i: (bstring * term) list -> theory -> theory
wenzelm@4996:   val add_oracle: bstring * (Sign.sg * Object.T -> term) -> theory -> theory
skalberg@14223:   val add_finals: bool -> string list -> theory -> theory
skalberg@14223:   val add_finals_i: bool -> term list -> theory -> theory
wenzelm@9320:   val add_defs: bool -> (bstring * string) list -> theory -> theory
wenzelm@9320:   val add_defs_i: bool -> (bstring * term) list -> theory -> theory
wenzelm@3996:   val add_path: string -> theory -> theory
wenzelm@4846:   val parent_path: theory -> theory
wenzelm@4846:   val root_path: theory -> theory
wenzelm@11501:   val absolute_path: theory -> theory
wenzelm@16134:   val qualified_names: theory -> theory
wenzelm@16134:   val no_base_names: theory -> theory
wenzelm@16134:   val custom_accesses: (string list -> string list list) -> theory -> theory
wenzelm@16134:   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
wenzelm@16134:     theory -> theory
wenzelm@16134:   val restore_naming: theory -> theory -> theory
wenzelm@12588:   val hide_space: bool -> string * xstring list -> theory -> theory
wenzelm@12588:   val hide_space_i: bool -> string * string list -> theory -> theory
wenzelm@12588:   val hide_classes: bool -> string list -> theory -> theory
wenzelm@12588:   val hide_types: bool -> string list -> theory -> theory
wenzelm@12588:   val hide_consts: bool -> string list -> theory -> theory
wenzelm@3996:   val add_name: string -> theory -> theory
wenzelm@5862:   val copy: theory -> theory
wenzelm@6661:   val prep_ext: theory -> theory
wenzelm@3996:   val prep_ext_merge: theory list -> theory
paulson@4970:   val requires: theory -> string -> string -> unit
wenzelm@6369:   val assert_super: theory -> theory -> theory
wenzelm@3996:   val pre_pure: theory
paulson@1526: end;
paulson@1526: 
wenzelm@6188: signature PRIVATE_THEORY =
wenzelm@5642: sig
wenzelm@5642:   include THEORY
wenzelm@6546:   val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
wenzelm@12311:     (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
wenzelm@5642:   val print_data: Object.kind -> theory -> unit
wenzelm@5642:   val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
wenzelm@5642:   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
wenzelm@5642: end;
paulson@1526: 
wenzelm@5642: 
wenzelm@6188: structure Theory: PRIVATE_THEORY =
paulson@1526: struct
wenzelm@2206: 
wenzelm@3996: 
wenzelm@2206: (** datatype theory **)
paulson@1526: 
paulson@1526: datatype theory =
paulson@1526:   Theory of {
paulson@1526:     sign: Sign.sg,
obua@16108:     const_deps: Defs.graph,
wenzelm@3996:     axioms: term Symtab.table,
wenzelm@4996:     oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
wenzelm@4019:     parents: theory list,
wenzelm@4019:     ancestors: theory list};
paulson@1526: 
obua@16158: fun make_theory sign const_deps axioms oracles parents ancestors =
obua@16158:   Theory {sign = sign, const_deps = const_deps, axioms = axioms,
skalberg@14223:     oracles = oracles,  parents = parents, ancestors = ancestors};
wenzelm@3996: 
paulson@1526: fun rep_theory (Theory args) = args;
paulson@1526: 
wenzelm@3996: val sign_of = #sign o rep_theory;
wenzelm@6188: val is_draft = Sign.is_draft o sign_of;
wenzelm@14645: val syn_of = Sign.syn_of o sign_of;
wenzelm@3996: val parents_of = #parents o rep_theory;
wenzelm@4019: val ancestors_of = #ancestors o rep_theory;
wenzelm@3996: 
paulson@1526: (*errors involving theories*)
paulson@1526: exception THEORY of string * theory list;
paulson@1526: 
paulson@1526: (*compare theories*)
paulson@1526: val subthy = Sign.subsig o pairself sign_of;
paulson@1526: val eq_thy = Sign.eq_sg o pairself sign_of;
paulson@1526: 
wenzelm@6369: (*check for some theory*)
paulson@4970: fun requires thy name what =
wenzelm@10930:   if Sign.exists_stamp name (sign_of thy) then ()
wenzelm@4846:   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
paulson@1526: 
wenzelm@6369: fun assert_super thy1 thy2 =
wenzelm@6369:   if subthy (thy1, thy2) then thy2
wenzelm@6369:   else raise THEORY ("Not a super theory", [thy1, thy2]);
wenzelm@6369: 
wenzelm@4846: (*partial Pure theory*)
nipkow@9282: val pre_pure =
obua@16158:   make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty [] [];
paulson@1526: 
paulson@1526: 
paulson@1526: 
paulson@1526: (** extend theory **)
paulson@1526: 
wenzelm@8725: (*name spaces*)
wenzelm@3996: val axiomK = "axiom";
wenzelm@3814: val oracleK = "oracle";
wenzelm@3814: 
wenzelm@3814: 
wenzelm@3814: (* extend logical part of a theory *)
wenzelm@3814: 
paulson@1526: fun err_dup_axms names =
wenzelm@10494:   error ("Duplicate axiom name(s): " ^ commas_quote names);
paulson@1526: 
wenzelm@3814: fun err_dup_oras names =
wenzelm@10494:   error ("Duplicate oracles: " ^ commas_quote names);
wenzelm@3814: 
obua@16158: fun ext_theory thy ext_sg new_axms new_oras =
paulson@1526:   let
obua@16158:     val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
paulson@1526:     val draft = Sign.is_draft sign;
wenzelm@3996:     val axioms' =
wenzelm@4488:       Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
paulson@1526:         handle Symtab.DUPS names => err_dup_axms names;
wenzelm@3814:     val oracles' =
wenzelm@4488:       Symtab.extend (oracles, new_oras)
wenzelm@3814:         handle Symtab.DUPS names => err_dup_oras names;
wenzelm@4019:     val (parents', ancestors') =
wenzelm@4019:       if draft then (parents, ancestors) else ([thy], thy :: ancestors);
paulson@1526:   in
obua@16158:     make_theory (ext_sg sign) const_deps axioms' oracles' parents' ancestors'
paulson@1526:   end;
paulson@1526: 
paulson@1526: 
paulson@1526: (* extend signature of a theory *)
paulson@1526: 
obua@16158: fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) [] [];
paulson@1526: 
wenzelm@14645: val add_classes            = ext_sign Sign.add_classes;
wenzelm@14645: val add_classes_i          = ext_sign Sign.add_classes_i;
wenzelm@14645: val add_classrel           = ext_sign Sign.add_classrel;
wenzelm@14645: val add_classrel_i         = ext_sign Sign.add_classrel_i;
wenzelm@14645: val add_defsort            = ext_sign Sign.add_defsort;
wenzelm@14645: val add_defsort_i          = ext_sign Sign.add_defsort_i;
wenzelm@14645: val add_types              = ext_sign Sign.add_types;
wenzelm@14645: val add_nonterminals       = ext_sign Sign.add_nonterminals;
wenzelm@14645: val add_tyabbrs            = ext_sign Sign.add_tyabbrs;
wenzelm@14645: val add_tyabbrs_i          = ext_sign Sign.add_tyabbrs_i;
wenzelm@14645: val add_arities            = ext_sign Sign.add_arities;
wenzelm@14645: val add_arities_i          = ext_sign Sign.add_arities_i;
wenzelm@14645: val add_consts             = ext_sign Sign.add_consts;
wenzelm@14645: val add_consts_i           = ext_sign Sign.add_consts_i;
wenzelm@14645: val add_syntax             = ext_sign Sign.add_syntax;
wenzelm@14645: val add_syntax_i           = ext_sign Sign.add_syntax_i;
wenzelm@14645: val add_modesyntax         = curry (ext_sign Sign.add_modesyntax);
wenzelm@14645: val add_modesyntax_i       = curry (ext_sign Sign.add_modesyntax_i);
wenzelm@15747: val del_modesyntax         = curry (ext_sign Sign.del_modesyntax);
wenzelm@15747: val del_modesyntax_i       = curry (ext_sign Sign.del_modesyntax_i);
wenzelm@14645: val add_trfuns             = ext_sign Sign.add_trfuns;
wenzelm@14645: val add_trfunsT            = ext_sign Sign.add_trfunsT;
wenzelm@14645: val add_advanced_trfuns    = ext_sign Sign.add_advanced_trfuns;
wenzelm@14645: val add_advanced_trfunsT   = ext_sign Sign.add_advanced_trfunsT;
wenzelm@14645: val add_tokentrfuns        = ext_sign Sign.add_tokentrfuns;
wenzelm@6311: fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
wenzelm@14645: val add_trrules            = ext_sign Sign.add_trrules;
wenzelm@14645: val add_trrules_i          = ext_sign Sign.add_trrules_i;
wenzelm@14645: val add_path               = ext_sign Sign.add_path;
wenzelm@14645: val parent_path            = add_path "..";
wenzelm@14645: val root_path              = add_path "/";
wenzelm@14645: val absolute_path          = add_path "//";
wenzelm@16134: val qualified_names        = ext_sign (K Sign.qualified_names) ();
wenzelm@16134: val no_base_names          = ext_sign (K Sign.no_base_names) ();
wenzelm@16134: val custom_accesses        = ext_sign Sign.custom_accesses;
wenzelm@16134: val set_policy             = ext_sign Sign.set_policy;
wenzelm@16134: val restore_naming         = ext_sign Sign.set_naming o Sign.naming_of o sign_of;
wenzelm@14645: val add_space              = ext_sign Sign.add_space;
wenzelm@14645: val hide_space             = ext_sign o Sign.hide_space;
wenzelm@14645: val hide_space_i           = ext_sign o Sign.hide_space_i;
wenzelm@14645: fun hide_classes b         = curry (hide_space_i b) Sign.classK;
wenzelm@14645: fun hide_types b           = curry (hide_space_i b) Sign.typeK;
wenzelm@14645: fun hide_consts b          = curry (hide_space_i b) Sign.constK;
wenzelm@14645: val add_name               = ext_sign Sign.add_name;
wenzelm@14645: val copy                   = ext_sign (K Sign.copy) ();
wenzelm@14645: val prep_ext               = ext_sign (K Sign.prep_ext) ();
wenzelm@3814: 
wenzelm@3996: 
wenzelm@6311: 
wenzelm@3814: (** add axioms **)
wenzelm@3814: 
paulson@1526: (* prepare axioms *)
paulson@1526: 
paulson@1526: fun err_in_axm name =
paulson@1526:   error ("The error(s) above occurred in axiom " ^ quote name);
paulson@1526: 
berghofe@14184: fun no_vars sg tm = (case (term_vars tm, term_tvars tm) of
berghofe@14184:     ([], []) => tm
berghofe@14184:   | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
berghofe@14184:       (Pretty.str "Illegal schematic variable(s) in term:" ::
berghofe@14184:        map (Sign.pretty_term sg) ts @
berghofe@14184:        map (Sign.pretty_typ sg o TVar) ixns)))));
paulson@1526: 
paulson@1526: fun cert_axm sg (name, raw_tm) =
paulson@1526:   let
wenzelm@14828:     val (t, T, _) = Sign.certify_term (Sign.pp sg) sg raw_tm
wenzelm@2979:       handle TYPE (msg, _, _) => error msg
wenzelm@3996:            | TERM (msg, _) => error msg;
paulson@1526:   in
wenzelm@9537:     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
paulson@1526:     assert (T = propT) "Term not of type prop";
berghofe@14184:     (name, no_vars sg t)
wenzelm@9629:   end;
paulson@1526: 
wenzelm@5057: (*some duplication of code with read_def_cterm*)
wenzelm@6661: fun read_def_axm (sg, types, sorts) used (name, str) =
wenzelm@3814:   let
wenzelm@14914:     val ts = Syntax.read (Sign.is_logtype sg) (Sign.syn_of sg) propT str;
wenzelm@14828:     val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT);
wenzelm@9320:   in cert_axm sg (name, t) end
paulson@1960:   handle ERROR => err_in_axm name;
paulson@1526: 
skalberg@15531: fun read_axm sg name_str = read_def_axm (sg, K NONE, K NONE) [] name_str;
wenzelm@5057: 
paulson@1526: fun inferT_axm sg (name, pre_tm) =
wenzelm@14828:   let val (t, _) = Sign.infer_types (Sign.pp sg) sg
skalberg@15531:     (K NONE) (K NONE) [] true ([pre_tm], propT);
berghofe@14184:   in (name, no_vars sg t) end
paulson@1526:   handle ERROR => err_in_axm name;
paulson@1526: 
paulson@1526: 
paulson@1526: (* extend axioms of a theory *)
paulson@1526: 
wenzelm@3814: fun ext_axms prep_axm raw_axms (thy as Theory {sign, ...}) =
paulson@1526:   let
wenzelm@3814:     val raw_axms' = map (apfst (Sign.full_name sign)) raw_axms;
wenzelm@3814:     val axioms =
wenzelm@3814:       map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms';
wenzelm@4996:     val ext_sg = Sign.add_space (axiomK, map fst axioms);
obua@16158:   in ext_theory thy ext_sg axioms [] end;
paulson@1526: 
paulson@1526: val add_axioms = ext_axms read_axm;
paulson@1526: val add_axioms_i = ext_axms cert_axm;
paulson@1526: 
paulson@1526: 
wenzelm@3814: (* add oracle **)
wenzelm@3814: 
wenzelm@3814: fun add_oracle (raw_name, oracle) (thy as Theory {sign, ...}) =
wenzelm@3814:   let
wenzelm@3814:     val name = Sign.full_name sign raw_name;
wenzelm@4996:     val ext_sg = Sign.add_space (oracleK, [name]);
obua@16158:   in ext_theory thy ext_sg [] [(name, (oracle, stamp ()))] end;
wenzelm@3814: 
wenzelm@3814: 
wenzelm@3767: 
wenzelm@3767: (** add constant definitions **)
wenzelm@3767: 
wenzelm@3767: (* clash_types, clash_consts *)
wenzelm@3767: 
obua@16108: (*check if types have common instance (ignoring sorts)
wenzelm@3767: 
wenzelm@3767: fun clash_types ty1 ty2 =
wenzelm@3767:   let
wenzelm@3767:     val ty1' = Type.varifyT ty1;
wenzelm@3767:     val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
wenzelm@9320:   in Type.raw_unify (ty1', ty2') end;
wenzelm@3767: 
wenzelm@3767: fun clash_consts (c1, ty1) (c2, ty2) =
wenzelm@3767:   c1 = c2 andalso clash_types ty1 ty2;
obua@16108: *)
wenzelm@3767: 
wenzelm@16134: 
obua@16108: (* clash_defns 
wenzelm@3767: 
wenzelm@3767: fun clash_defn c_ty (name, tm) =
skalberg@14204:   let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals (Logic.strip_imp_concl tm)))) in
skalberg@15531:     if clash_consts c_ty (c, ty') then SOME (name, ty') else NONE
skalberg@15531:   end handle TERM _ => NONE;
wenzelm@3767: 
wenzelm@3767: fun clash_defns c_ty axms =
skalberg@15570:   distinct (List.mapPartial (clash_defn c_ty) axms);
obua@16108: *)
wenzelm@3767: 
wenzelm@3767: 
wenzelm@9320: (* overloading *)
nipkow@9280: 
wenzelm@9320: datatype overloading = NoOverloading | Useless | Plain;
wenzelm@9320: 
wenzelm@9320: fun overloading sg declT defT =
wenzelm@10403:   let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in
wenzelm@10403:     if Sign.typ_instance sg (declT, T) then NoOverloading
wenzelm@14789:     else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts T) then Useless
wenzelm@9320:     else Plain
nipkow@9280:   end;
nipkow@9280: 
nipkow@9280: 
wenzelm@3767: (* dest_defn *)
wenzelm@3767: 
wenzelm@3767: fun dest_defn tm =
wenzelm@3767:   let
wenzelm@3787:     fun err msg = raise TERM (msg, [tm]);
wenzelm@3767: 
wenzelm@3767:     val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
wenzelm@3767:       handle TERM _ => err "Not a meta-equality (==)";
wenzelm@3767:     val (head, args) = strip_comb lhs;
wenzelm@9320:     val c_ty as (c, ty) = dest_Const head
wenzelm@3767:       handle TERM _ => err "Head of lhs not a constant";
wenzelm@3767: 
wenzelm@4141:     fun dest_free (Free (x, _)) = x
wenzelm@4141:       | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
wenzelm@4141:       | dest_free _ = raise Match;
wenzelm@4141: 
wenzelm@4141:     val show_frees = commas_quote o map dest_free;
wenzelm@3767:     val show_tfrees = commas_quote o map fst;
wenzelm@3767: 
wenzelm@3767:     val lhs_dups = duplicates args;
wenzelm@3767:     val rhs_extras = gen_rems (op =) (term_frees rhs, args);
wenzelm@3767:     val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
wenzelm@3767:   in
wenzelm@4141:     if not (forall (can dest_free) args) then
wenzelm@3767:       err "Arguments (on lhs) must be variables"
wenzelm@3767:     else if not (null lhs_dups) then
wenzelm@3767:       err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
wenzelm@3767:     else if not (null rhs_extras) then
wenzelm@3767:       err ("Extra variables on rhs: " ^ show_frees rhs_extras)
wenzelm@3767:     else if not (null rhs_extrasT) then
wenzelm@3767:       err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
nipkow@9282:     else if exists_Const (fn c_ty' => c_ty' = c_ty) rhs then
wenzelm@3767:       err ("Constant to be defined occurs on rhs")
wenzelm@9320:     else (c_ty, rhs)
wenzelm@3767:   end;
wenzelm@3767: 
wenzelm@3767: 
wenzelm@3767: (* check_defn *)
wenzelm@3767: 
wenzelm@3814: fun err_in_defn sg name msg =
wenzelm@9320:   (error_msg msg;
wenzelm@9320:     error ("The error(s) above occurred in definition " ^ quote (Sign.full_name sg name)));
wenzelm@9320: 
obua@16108: fun pretty_const sg (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
wenzelm@3767: 
obua@16113: fun cycle_msg sg (infinite, namess) = 
obua@16113:   let val header = if not (infinite) then "cyclic dependency found: " else "infinite chain found: "
obua@16113:   in
obua@16113:       Pretty.string_of (Pretty.block (((Pretty.str header) :: Pretty.fbrk :: (
obua@16113:         let      
obua@16113: 	    fun f last (ty, constname, defname) =  
obua@16113: 		(pretty_const sg (constname, ty)) @ (if last then [] else [Pretty.str (" depends via "^ quote defname^ " on ")])
obua@16108:           	
obua@16113: 	in
obua@16113: 	    foldr (fn (x,r) => (f (r=[]) x)@[Pretty.fbrk]@r) [] namess
obua@16113: 	end))))
obua@16113:   end
wenzelm@9320: 
obua@16158: fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
skalberg@14223:   let
obua@16108:     
obua@16108:     val name = Sign.full_name sg name
obua@16108:       
wenzelm@10494:     fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
wenzelm@10494:       Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
wenzelm@3767: 
wenzelm@10494:     fun def_txt (c_ty, txt) = Pretty.block
wenzelm@10494:       (Pretty.str "Definition of " :: pretty_const c_ty @
wenzelm@10494:         (if txt = "" then [] else [Pretty.str txt]));
wenzelm@10494: 
wenzelm@10494:     fun show_defn c (dfn, ty') = Pretty.block
wenzelm@10494:       (Pretty.str "  " :: pretty_const (c, ty') @ [Pretty.str " in ", Pretty.str dfn]);
wenzelm@3767: 
wenzelm@9320:     val (c_ty as (c, ty), rhs) = dest_defn tm
nipkow@9280:       handle TERM (msg, _) => err_in_defn sg name msg;
obua@16108: 
obua@16108:     fun decl deps c = 
obua@16158: 	(case Sign.const_type sg c of 
obua@16158: 	     SOME T => (Defs.declare deps (c, T) handle _ => deps, T)
obua@16158: 	   | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
wenzelm@9320: 
obua@16108:     val (deps, c_decl) = decl deps c
obua@16108: 
obua@16108:     val body = Term.term_constsT rhs
obua@16108:     val deps = foldl (fn ((c, _), deps) => fst (decl deps c)) deps body
obua@16108: 
wenzelm@3767:   in
wenzelm@9320:       (case overloading sg c_decl ty of
wenzelm@16134:          Useless =>
wenzelm@10494:            err_in_defn sg name (Pretty.string_of (Pretty.chunks
wenzelm@16134:            [Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str
obua@16108:               "imposes additional sort constraints on the declared type of the constant"]))   
obua@16108:        | ov =>
obua@16108: 	 let 
obua@16158: 	     val deps' = Defs.define deps c_ty name body
obua@16108: 		 handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s) 
obua@16113: 		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg (false, s))
obua@16113:                       | Defs.INFINITE_CHAIN s => err_in_defn sg name (cycle_msg sg (true, s)) 
obua@16108:                       | Defs.CLASH (_, def1, def2) => err_in_defn sg name (
obua@16158: 			  "clashing definitions "^ quote def1 ^" and "^ quote def2)
obua@16158: 		      | Defs.FINAL cfinal =>
obua@16158: 			err_in_defn sg name (Pretty.string_of (Pretty.block
obua@16158: 			  ([Pretty.str "The constant",Pretty.brk 1] @
obua@16158: 			   pretty_const cfinal @
obua@16158: 			   [Pretty.brk 1,Pretty.str "has been declared final"]))) 
obua@16158: 	 in
obua@16158: 	     ((if ov = Plain andalso not overloaded then
obua@16158: 		   warning (Pretty.string_of (Pretty.chunks
obua@16158: 		     [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
obua@16158: 	       else
obua@16158: 		   ()); (deps', def::axms))
obua@16158: 	 end)
wenzelm@3767:   end;
wenzelm@3767: 
wenzelm@3767: 
wenzelm@3767: (* add_defs *)
wenzelm@3767: 
wenzelm@9320: fun ext_defns prep_axm overloaded raw_axms thy =
wenzelm@3767:   let
obua@16158:     val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
skalberg@15570:     val all_axioms = List.concat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
wenzelm@9320: 
wenzelm@9320:     val axms = map (prep_axm sign) raw_axms;
obua@16158:     val (const_deps', _) = Library.foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
wenzelm@3767:   in
obua@16158:     make_theory sign const_deps' axioms oracles parents ancestors
wenzelm@9320:     |> add_axioms_i axms
wenzelm@3767:   end;
wenzelm@3767: 
wenzelm@3767: val add_defs_i = ext_defns cert_axm;
wenzelm@3767: val add_defs = ext_defns read_axm;
wenzelm@3767: 
wenzelm@3767: 
skalberg@14223: (* add_finals *)
skalberg@14223: 
skalberg@14223: fun ext_finals prep_term overloaded raw_terms thy =
skalberg@14223:   let
obua@16158:     val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
obua@16158:     fun mk_final (tm, finals) =
obua@16158: 	let
obua@16158:             fun err msg = raise TERM(msg,[tm])
obua@16158:             val (c,ty) = dest_Const tm
obua@16158: 		handle TERM _ => err "Can only make constants final"
obua@16158:             val c_decl =
obua@16158: 		(case Sign.const_type sign c of 
obua@16158: 		     SOME T => T
obua@16158: 		   | NONE => err ("Undeclared constant " ^ quote c))
obua@16158: 	    val _ =
obua@16158: 		case overloading sign c_decl ty of
obua@16158: 		    NoOverloading => ()
obua@16158: 		  | Useless => err "Sort restrictions too strong"
obua@16158: 		  | Plain => (if overloaded then () else warning "Type is more general than declared")
obua@16158: 	    val finals = Defs.declare finals (c, c_decl) handle _ => finals
obua@16158: 	in
obua@16158: 	    Defs.finalize finals (c,ty)
obua@16158: 	end
skalberg@14223:     val consts = map (prep_term sign) raw_terms;
obua@16158:     val const_deps' = foldl mk_final const_deps consts;
skalberg@14223:   in
obua@16158:     make_theory sign const_deps' axioms oracles parents ancestors
skalberg@14223:   end;
skalberg@14223: 
skalberg@14223: local
skalberg@14223:   fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
wenzelm@14828:   fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg;
skalberg@14223: in
skalberg@14223: val add_finals = ext_finals read_term;
skalberg@14223: val add_finals_i = ext_finals cert_term;
skalberg@14223: end;
skalberg@14223: 
skalberg@14223: fun merge_final sg =
skalberg@14223:   let
skalberg@14223:     fun merge_single (tys,ty) =
skalberg@14223:       if exists (curry (Sign.typ_instance sg) ty) tys
skalberg@14223:       then tys
skalberg@14223:       else (ty::gen_rem (Sign.typ_instance sg) (tys,ty));
skalberg@14223:     fun merge ([],_) = []
skalberg@14223:       | merge (_,[]) = []
skalberg@15570:       | merge input = Library.foldl merge_single input;
skalberg@14223:   in
skalberg@15531:     SOME o merge
skalberg@14223:   end;
skalberg@14223: 
wenzelm@3878: 
wenzelm@3865: (** additional theory data **)
wenzelm@3865: 
wenzelm@4996: val init_data = curry (ext_sign Sign.init_data);
wenzelm@4996: fun print_data kind = Sign.print_data kind o sign_of;
wenzelm@4996: fun get_data kind f = Sign.get_data kind f o sign_of;
wenzelm@4996: fun put_data kind f = ext_sign (Sign.put_data kind f);
wenzelm@3865: 
wenzelm@3865: 
wenzelm@3767: 
wenzelm@6661: (** merge theories **)          (*exception ERROR*)
wenzelm@4019: 
wenzelm@3878: (*merge list of theories from left to right, preparing extend*)
wenzelm@3967: fun prep_ext_merge thys =
wenzelm@15703:   let
wenzelm@15703:     val sign' = Sign.prep_ext_merge (map sign_of thys)
wenzelm@3814: 
wenzelm@15703:     val depss = map (#const_deps o rep_theory) thys;
obua@16108:     val deps' = foldl (uncurry Defs.merge) (hd depss) (tl depss)
obua@16113:       handle Defs.CIRCULAR namess => error (cycle_msg sign' (false, namess))
obua@16113: 	   | Defs.INFINITE_CHAIN namess => error (cycle_msg sign' (true, namess))
wenzelm@15703: 
wenzelm@15703:     val axioms' = Symtab.empty;
nipkow@9282: 
wenzelm@15703:     fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
wenzelm@15703:     val oracles' =
wenzelm@15703:       Symtab.make (gen_distinct eq_ora
wenzelm@15703:         (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
wenzelm@15703:       handle Symtab.DUPS names => err_dup_oras names;
wenzelm@4019: 
wenzelm@15703:     val parents' = gen_distinct eq_thy thys;
wenzelm@15703:     val ancestors' =
wenzelm@15703:       gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
wenzelm@15703:   in
obua@16158:     make_theory sign' deps' axioms' oracles' parents' ancestors'
wenzelm@15703:   end;
paulson@1526: 
wenzelm@3885: 
paulson@1526: end;
paulson@1526: 
wenzelm@3767: structure BasicTheory: BASIC_THEORY = Theory;
wenzelm@3767: open BasicTheory;
wenzelm@15716: