src/Pure/theory.ML
author berghofe
Thu Apr 21 19:12:03 2005 +0200 (2005-04-21)
changeset 15797 a63605582573
parent 15747 00d637286a69
child 16108 cf468b93a02e
permissions -rw-r--r--
- Eliminated nodup_vars check.
- Unification and matching functions now check types of term variables / sorts
of type variables when applying a substitution.
- Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list
as argument, to allow for proper instantiation of theorems containing
type variables with same name but different sorts.
     1 (*  Title:      Pure/theory.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4 
     5 The abstract type "theory" of theories.
     6 *)
     7 
     8 signature BASIC_THEORY =
     9 sig
    10   type theory
    11   exception THEORY of string * theory list
    12   val rep_theory: theory ->
    13     {sign: Sign.sg,
    14       const_deps: unit Graph.T,
    15       final_consts: typ list Symtab.table,
    16       axioms: term Symtab.table,
    17       oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    18       parents: theory list,
    19       ancestors: theory list}
    20   val sign_of: theory -> Sign.sg
    21   val is_draft: theory -> bool
    22   val syn_of: theory -> Syntax.syntax
    23   val parents_of: theory -> theory list
    24   val ancestors_of: theory -> theory list
    25   val subthy: theory * theory -> bool
    26   val eq_thy: theory * theory -> bool
    27   val cert_axm: Sign.sg -> string * term -> string * term
    28   val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    29     string list -> string * string -> string * term
    30   val read_axm: Sign.sg -> string * string -> string * term
    31   val inferT_axm: Sign.sg -> string * term -> string * term
    32 end
    33 
    34 signature THEORY =
    35 sig
    36   include BASIC_THEORY
    37   val axiomK: string
    38   val oracleK: string
    39   (*theory extension primitives*)
    40   val add_classes: (bclass * xclass list) list -> theory -> theory
    41   val add_classes_i: (bclass * class list) list -> theory -> theory
    42   val add_classrel: (xclass * xclass) list -> theory -> theory
    43   val add_classrel_i: (class * class) list -> theory -> theory
    44   val add_defsort: string -> theory -> theory
    45   val add_defsort_i: sort -> theory -> theory
    46   val add_types: (bstring * int * mixfix) list -> theory -> theory
    47   val add_nonterminals: bstring list -> theory -> theory
    48   val add_tyabbrs: (bstring * string list * string * mixfix) list
    49     -> theory -> theory
    50   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
    51     -> theory -> theory
    52   val add_arities: (xstring * string list * string) list -> theory -> theory
    53   val add_arities_i: (string * sort list * sort) list -> theory -> theory
    54   val add_consts: (bstring * string * mixfix) list -> theory -> theory
    55   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    56   val add_syntax: (bstring * string * mixfix) list -> theory -> theory
    57   val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
    58   val add_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    59   val add_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
    60   val del_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    61   val del_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
    62   val add_trfuns:
    63     (string * (Syntax.ast list -> Syntax.ast)) list *
    64     (string * (term list -> term)) list *
    65     (string * (term list -> term)) list *
    66     (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
    67   val add_trfunsT:
    68     (string * (bool -> typ -> term list -> term)) list -> theory -> theory
    69   val add_advanced_trfuns:
    70     (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list *
    71     (string * (Sign.sg -> term list -> term)) list *
    72     (string * (Sign.sg -> term list -> term)) list *
    73     (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list -> theory -> theory
    74   val add_advanced_trfunsT:
    75     (string * (Sign.sg -> bool -> typ -> term list -> term)) list -> theory -> theory
    76   val add_tokentrfuns:
    77     (string * string * (string -> string * real)) list -> theory -> theory
    78   val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
    79     -> theory -> theory
    80   val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    81   val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
    82   val add_axioms: (bstring * string) list -> theory -> theory
    83   val add_axioms_i: (bstring * term) list -> theory -> theory
    84   val add_oracle: bstring * (Sign.sg * Object.T -> term) -> theory -> theory
    85   val add_finals: bool -> string list -> theory -> theory
    86   val add_finals_i: bool -> term list -> theory -> theory
    87   val add_defs: bool -> (bstring * string) list -> theory -> theory
    88   val add_defs_i: bool -> (bstring * term) list -> theory -> theory
    89   val add_path: string -> theory -> theory
    90   val parent_path: theory -> theory
    91   val root_path: theory -> theory
    92   val absolute_path: theory -> theory
    93   val hide_space: bool -> string * xstring list -> theory -> theory
    94   val hide_space_i: bool -> string * string list -> theory -> theory
    95   val hide_classes: bool -> string list -> theory -> theory
    96   val hide_types: bool -> string list -> theory -> theory
    97   val hide_consts: bool -> string list -> theory -> theory
    98   val add_name: string -> theory -> theory
    99   val copy: theory -> theory
   100   val prep_ext: theory -> theory
   101   val prep_ext_merge: theory list -> theory
   102   val requires: theory -> string -> string -> unit
   103   val assert_super: theory -> theory -> theory
   104   val pre_pure: theory
   105 end;
   106 
   107 signature PRIVATE_THEORY =
   108 sig
   109   include THEORY
   110   val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
   111     (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
   112   val print_data: Object.kind -> theory -> unit
   113   val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
   114   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
   115 end;
   116 
   117 
   118 structure Theory: PRIVATE_THEORY =
   119 struct
   120 
   121 
   122 (** datatype theory **)
   123 
   124 (*Note: dependencies are only tracked for non-overloaded constant definitions*)
   125 
   126 datatype theory =
   127   Theory of {
   128     sign: Sign.sg,
   129     const_deps: unit Graph.T,
   130     final_consts: typ list Symtab.table,
   131     axioms: term Symtab.table,
   132     oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
   133     parents: theory list,
   134     ancestors: theory list};
   135 
   136 fun make_theory sign const_deps final_consts axioms oracles parents ancestors =
   137   Theory {sign = sign, const_deps = const_deps, final_consts = final_consts, axioms = axioms,
   138     oracles = oracles,  parents = parents, ancestors = ancestors};
   139 
   140 fun rep_theory (Theory args) = args;
   141 
   142 val sign_of = #sign o rep_theory;
   143 val is_draft = Sign.is_draft o sign_of;
   144 val syn_of = Sign.syn_of o sign_of;
   145 val parents_of = #parents o rep_theory;
   146 val ancestors_of = #ancestors o rep_theory;
   147 
   148 (*errors involving theories*)
   149 exception THEORY of string * theory list;
   150 
   151 (*compare theories*)
   152 val subthy = Sign.subsig o pairself sign_of;
   153 val eq_thy = Sign.eq_sg o pairself sign_of;
   154 
   155 (*check for some theory*)
   156 fun requires thy name what =
   157   if Sign.exists_stamp name (sign_of thy) then ()
   158   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   159 
   160 fun assert_super thy1 thy2 =
   161   if subthy (thy1, thy2) then thy2
   162   else raise THEORY ("Not a super theory", [thy1, thy2]);
   163 
   164 (*partial Pure theory*)
   165 val pre_pure =
   166   make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty Symtab.empty [] [];
   167 
   168 
   169 
   170 (** extend theory **)
   171 
   172 (*name spaces*)
   173 val axiomK = "axiom";
   174 val oracleK = "oracle";
   175 
   176 
   177 (* extend logical part of a theory *)
   178 
   179 fun err_dup_axms names =
   180   error ("Duplicate axiom name(s): " ^ commas_quote names);
   181 
   182 fun err_dup_oras names =
   183   error ("Duplicate oracles: " ^ commas_quote names);
   184 
   185 fun ext_theory thy ext_sg ext_deps new_axms new_oras =
   186   let
   187     val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
   188     val draft = Sign.is_draft sign;
   189     val axioms' =
   190       Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
   191         handle Symtab.DUPS names => err_dup_axms names;
   192     val oracles' =
   193       Symtab.extend (oracles, new_oras)
   194         handle Symtab.DUPS names => err_dup_oras names;
   195     val (parents', ancestors') =
   196       if draft then (parents, ancestors) else ([thy], thy :: ancestors);
   197   in
   198     make_theory (ext_sg sign) (ext_deps const_deps) final_consts axioms' oracles' parents' ancestors'
   199   end;
   200 
   201 
   202 (* extend signature of a theory *)
   203 
   204 fun ext_sign extfun decls thy = ext_theory thy (extfun decls) I [] [];
   205 
   206 val add_classes            = ext_sign Sign.add_classes;
   207 val add_classes_i          = ext_sign Sign.add_classes_i;
   208 val add_classrel           = ext_sign Sign.add_classrel;
   209 val add_classrel_i         = ext_sign Sign.add_classrel_i;
   210 val add_defsort            = ext_sign Sign.add_defsort;
   211 val add_defsort_i          = ext_sign Sign.add_defsort_i;
   212 val add_types              = ext_sign Sign.add_types;
   213 val add_nonterminals       = ext_sign Sign.add_nonterminals;
   214 val add_tyabbrs            = ext_sign Sign.add_tyabbrs;
   215 val add_tyabbrs_i          = ext_sign Sign.add_tyabbrs_i;
   216 val add_arities            = ext_sign Sign.add_arities;
   217 val add_arities_i          = ext_sign Sign.add_arities_i;
   218 val add_consts             = ext_sign Sign.add_consts;
   219 val add_consts_i           = ext_sign Sign.add_consts_i;
   220 val add_syntax             = ext_sign Sign.add_syntax;
   221 val add_syntax_i           = ext_sign Sign.add_syntax_i;
   222 val add_modesyntax         = curry (ext_sign Sign.add_modesyntax);
   223 val add_modesyntax_i       = curry (ext_sign Sign.add_modesyntax_i);
   224 val del_modesyntax         = curry (ext_sign Sign.del_modesyntax);
   225 val del_modesyntax_i       = curry (ext_sign Sign.del_modesyntax_i);
   226 val add_trfuns             = ext_sign Sign.add_trfuns;
   227 val add_trfunsT            = ext_sign Sign.add_trfunsT;
   228 val add_advanced_trfuns    = ext_sign Sign.add_advanced_trfuns;
   229 val add_advanced_trfunsT   = ext_sign Sign.add_advanced_trfunsT;
   230 val add_tokentrfuns        = ext_sign Sign.add_tokentrfuns;
   231 fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
   232 val add_trrules            = ext_sign Sign.add_trrules;
   233 val add_trrules_i          = ext_sign Sign.add_trrules_i;
   234 val add_path               = ext_sign Sign.add_path;
   235 val parent_path            = add_path "..";
   236 val root_path              = add_path "/";
   237 val absolute_path          = add_path "//";
   238 val add_space              = ext_sign Sign.add_space;
   239 val hide_space             = ext_sign o Sign.hide_space;
   240 val hide_space_i           = ext_sign o Sign.hide_space_i;
   241 fun hide_classes b         = curry (hide_space_i b) Sign.classK;
   242 fun hide_types b           = curry (hide_space_i b) Sign.typeK;
   243 fun hide_consts b          = curry (hide_space_i b) Sign.constK;
   244 val add_name               = ext_sign Sign.add_name;
   245 val copy                   = ext_sign (K Sign.copy) ();
   246 val prep_ext               = ext_sign (K Sign.prep_ext) ();
   247 
   248 
   249 
   250 (** add axioms **)
   251 
   252 (* prepare axioms *)
   253 
   254 fun err_in_axm name =
   255   error ("The error(s) above occurred in axiom " ^ quote name);
   256 
   257 fun no_vars sg tm = (case (term_vars tm, term_tvars tm) of
   258     ([], []) => tm
   259   | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
   260       (Pretty.str "Illegal schematic variable(s) in term:" ::
   261        map (Sign.pretty_term sg) ts @
   262        map (Sign.pretty_typ sg o TVar) ixns)))));
   263 
   264 fun cert_axm sg (name, raw_tm) =
   265   let
   266     val (t, T, _) = Sign.certify_term (Sign.pp sg) sg raw_tm
   267       handle TYPE (msg, _, _) => error msg
   268            | TERM (msg, _) => error msg;
   269   in
   270     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   271     assert (T = propT) "Term not of type prop";
   272     (name, no_vars sg t)
   273   end;
   274 
   275 (*some duplication of code with read_def_cterm*)
   276 fun read_def_axm (sg, types, sorts) used (name, str) =
   277   let
   278     val ts = Syntax.read (Sign.is_logtype sg) (Sign.syn_of sg) propT str;
   279     val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT);
   280   in cert_axm sg (name, t) end
   281   handle ERROR => err_in_axm name;
   282 
   283 fun read_axm sg name_str = read_def_axm (sg, K NONE, K NONE) [] name_str;
   284 
   285 fun inferT_axm sg (name, pre_tm) =
   286   let val (t, _) = Sign.infer_types (Sign.pp sg) sg
   287     (K NONE) (K NONE) [] true ([pre_tm], propT);
   288   in (name, no_vars sg t) end
   289   handle ERROR => err_in_axm name;
   290 
   291 
   292 (* extend axioms of a theory *)
   293 
   294 fun ext_axms prep_axm raw_axms (thy as Theory {sign, ...}) =
   295   let
   296     val raw_axms' = map (apfst (Sign.full_name sign)) raw_axms;
   297     val axioms =
   298       map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms';
   299     val ext_sg = Sign.add_space (axiomK, map fst axioms);
   300   in ext_theory thy ext_sg I axioms [] end;
   301 
   302 val add_axioms = ext_axms read_axm;
   303 val add_axioms_i = ext_axms cert_axm;
   304 
   305 
   306 (* add oracle **)
   307 
   308 fun add_oracle (raw_name, oracle) (thy as Theory {sign, ...}) =
   309   let
   310     val name = Sign.full_name sign raw_name;
   311     val ext_sg = Sign.add_space (oracleK, [name]);
   312   in ext_theory thy ext_sg I [] [(name, (oracle, stamp ()))] end;
   313 
   314 
   315 
   316 (** add constant definitions **)
   317 
   318 (* clash_types, clash_consts *)
   319 
   320 (*check if types have common instance (ignoring sorts)*)
   321 
   322 fun clash_types ty1 ty2 =
   323   let
   324     val ty1' = Type.varifyT ty1;
   325     val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
   326   in Type.raw_unify (ty1', ty2') end;
   327 
   328 fun clash_consts (c1, ty1) (c2, ty2) =
   329   c1 = c2 andalso clash_types ty1 ty2;
   330 
   331 
   332 (* clash_defns *)
   333 
   334 fun clash_defn c_ty (name, tm) =
   335   let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals (Logic.strip_imp_concl tm)))) in
   336     if clash_consts c_ty (c, ty') then SOME (name, ty') else NONE
   337   end handle TERM _ => NONE;
   338 
   339 fun clash_defns c_ty axms =
   340   distinct (List.mapPartial (clash_defn c_ty) axms);
   341 
   342 
   343 (* overloading *)
   344 
   345 datatype overloading = NoOverloading | Useless | Plain;
   346 
   347 fun overloading sg declT defT =
   348   let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in
   349     if Sign.typ_instance sg (declT, T) then NoOverloading
   350     else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts T) then Useless
   351     else Plain
   352   end;
   353 
   354 
   355 (* dest_defn *)
   356 
   357 fun dest_defn tm =
   358   let
   359     fun err msg = raise TERM (msg, [tm]);
   360 
   361     val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
   362       handle TERM _ => err "Not a meta-equality (==)";
   363     val (head, args) = strip_comb lhs;
   364     val c_ty as (c, ty) = dest_Const head
   365       handle TERM _ => err "Head of lhs not a constant";
   366 
   367     fun dest_free (Free (x, _)) = x
   368       | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
   369       | dest_free _ = raise Match;
   370 
   371     val show_frees = commas_quote o map dest_free;
   372     val show_tfrees = commas_quote o map fst;
   373 
   374     val lhs_dups = duplicates args;
   375     val rhs_extras = gen_rems (op =) (term_frees rhs, args);
   376     val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
   377   in
   378     if not (forall (can dest_free) args) then
   379       err "Arguments (on lhs) must be variables"
   380     else if not (null lhs_dups) then
   381       err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
   382     else if not (null rhs_extras) then
   383       err ("Extra variables on rhs: " ^ show_frees rhs_extras)
   384     else if not (null rhs_extrasT) then
   385       err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
   386     else if exists_Const (fn c_ty' => c_ty' = c_ty) rhs then
   387       err ("Constant to be defined occurs on rhs")
   388     else (c_ty, rhs)
   389   end;
   390 
   391 
   392 (* check_defn *)
   393 
   394 fun err_in_defn sg name msg =
   395   (error_msg msg;
   396     error ("The error(s) above occurred in definition " ^ quote (Sign.full_name sg name)));
   397 
   398 fun cycle_msg namess = "Cyclic dependency of constants:\n" ^
   399   cat_lines (map (space_implode " -> " o map quote o rev) namess);
   400 
   401 fun add_deps (c, cs) deps =
   402   let fun declare (G, x) = Graph.new_node (x, ()) G handle Graph.DUP _ => G
   403   in Library.foldl declare (deps, c :: cs) |> Graph.add_deps_acyclic (c, cs) end;
   404 
   405 fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
   406   let
   407     fun is_final (c, ty) =
   408       case Symtab.lookup(final_consts,c) of
   409         SOME [] => true
   410       | SOME tys => exists (curry (Sign.typ_instance sg) ty) tys
   411       | NONE => false;
   412 
   413     fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   414       Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
   415 
   416     fun def_txt (c_ty, txt) = Pretty.block
   417       (Pretty.str "Definition of " :: pretty_const c_ty @
   418         (if txt = "" then [] else [Pretty.str txt]));
   419 
   420     fun show_defn c (dfn, ty') = Pretty.block
   421       (Pretty.str "  " :: pretty_const (c, ty') @ [Pretty.str " in ", Pretty.str dfn]);
   422 
   423     val (c_ty as (c, ty), rhs) = dest_defn tm
   424       handle TERM (msg, _) => err_in_defn sg name msg;
   425     val c_decl =
   426       (case Sign.const_type sg c of SOME T => T
   427       | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
   428 
   429     val clashed = clash_defns c_ty axms;
   430   in
   431     if not (null clashed) then
   432       err_in_defn sg name (Pretty.string_of (Pretty.chunks
   433         (def_txt (c_ty, " clashes with") :: map (show_defn c) clashed)))
   434     else if is_final c_ty then
   435       err_in_defn sg name (Pretty.string_of (Pretty.block
   436         ([Pretty.str "The constant",Pretty.brk 1] @
   437 	 pretty_const c_ty @
   438 	 [Pretty.brk 1,Pretty.str "has been declared final"])))
   439     else
   440       (case overloading sg c_decl ty of
   441         NoOverloading =>
   442           (add_deps (c, Term.term_consts rhs) deps
   443               handle Graph.CYCLES namess => err_in_defn sg name (cycle_msg namess),
   444             def :: axms)
   445       | Useless =>
   446            err_in_defn sg name (Pretty.string_of (Pretty.chunks
   447              [Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str
   448                  "imposes additional sort constraints on the declared type of the constant"]))
   449       | Plain =>
   450          (if not overloaded then warning (Pretty.string_of (Pretty.chunks
   451            [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see "
   452                ^ quote (Sign.full_name sg name) ^ ")")]))
   453          else (); (deps, def :: axms)))
   454   end;
   455 
   456 
   457 (* add_defs *)
   458 
   459 fun ext_defns prep_axm overloaded raw_axms thy =
   460   let
   461     val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
   462     val all_axioms = List.concat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
   463 
   464     val axms = map (prep_axm sign) raw_axms;
   465     val (const_deps', _) = Library.foldl (check_defn sign overloaded final_consts) ((const_deps, all_axioms), axms);
   466   in
   467     make_theory sign const_deps' final_consts axioms oracles parents ancestors
   468     |> add_axioms_i axms
   469   end;
   470 
   471 val add_defs_i = ext_defns cert_axm;
   472 val add_defs = ext_defns read_axm;
   473 
   474 
   475 (* add_finals *)
   476 
   477 fun ext_finals prep_term overloaded raw_terms thy =
   478   let
   479     val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
   480     fun mk_final (finals,tm) =
   481       let
   482         fun err msg = raise TERM(msg,[tm]);
   483         val (c,ty) = dest_Const tm
   484           handle TERM _ => err "Can only make constants final";
   485         val c_decl =
   486           (case Sign.const_type sign c of SOME T => T
   487           | NONE => err ("Undeclared constant " ^ quote c));
   488         val simple =
   489 	  case overloading sign c_decl ty of
   490 	    NoOverloading => true
   491 	  | Useless => err "Sort restrictions too strong"
   492 	  | Plain => if overloaded then false
   493 		     else err "Type is more general than declared";
   494         val typ_instance = Sign.typ_instance sign;
   495       in
   496         if simple then
   497 	  (case Symtab.lookup(finals,c) of
   498 	    SOME [] => err "Constant already final"
   499 	  | _ => Symtab.update((c,[]),finals))
   500 	else
   501 	  (case Symtab.lookup(finals,c) of
   502 	    SOME [] => err "Constant already completely final"
   503           | SOME tys => if exists (curry typ_instance ty) tys
   504 			then err "Instance of constant is already final"
   505 			else Symtab.update((c,ty::gen_rem typ_instance (tys,ty)),finals)
   506 	  | NONE => Symtab.update((c,[ty]),finals))
   507       end;
   508     val consts = map (prep_term sign) raw_terms;
   509     val final_consts' = Library.foldl mk_final (final_consts,consts);
   510   in
   511     make_theory sign const_deps final_consts' axioms oracles parents ancestors
   512   end;
   513 
   514 local
   515   fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
   516   fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg;
   517 in
   518 val add_finals = ext_finals read_term;
   519 val add_finals_i = ext_finals cert_term;
   520 end;
   521 
   522 fun merge_final sg =
   523   let
   524     fun merge_single (tys,ty) =
   525       if exists (curry (Sign.typ_instance sg) ty) tys
   526       then tys
   527       else (ty::gen_rem (Sign.typ_instance sg) (tys,ty));
   528     fun merge ([],_) = []
   529       | merge (_,[]) = []
   530       | merge input = Library.foldl merge_single input;
   531   in
   532     SOME o merge
   533   end;
   534 
   535 
   536 (** additional theory data **)
   537 
   538 val init_data = curry (ext_sign Sign.init_data);
   539 fun print_data kind = Sign.print_data kind o sign_of;
   540 fun get_data kind f = Sign.get_data kind f o sign_of;
   541 fun put_data kind f = ext_sign (Sign.put_data kind f);
   542 
   543 
   544 
   545 (** merge theories **)          (*exception ERROR*)
   546 
   547 (*merge list of theories from left to right, preparing extend*)
   548 fun prep_ext_merge thys =
   549   let
   550     val sign' = Sign.prep_ext_merge (map sign_of thys)
   551 
   552     val depss = map (#const_deps o rep_theory) thys;
   553     val deps' = Library.foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
   554       handle Graph.CYCLES namess => error (cycle_msg namess);
   555 
   556     val final_constss = map (#final_consts o rep_theory) thys;
   557     val final_consts' =
   558       Library.foldl (Symtab.join (merge_final sign')) (hd final_constss, tl final_constss);
   559     val axioms' = Symtab.empty;
   560 
   561     fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   562     val oracles' =
   563       Symtab.make (gen_distinct eq_ora
   564         (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
   565       handle Symtab.DUPS names => err_dup_oras names;
   566 
   567     val parents' = gen_distinct eq_thy thys;
   568     val ancestors' =
   569       gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
   570   in
   571     make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
   572   end;
   573 
   574 
   575 end;
   576 
   577 structure BasicTheory: BASIC_THEORY = Theory;
   578 open BasicTheory;
   579