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