src/Pure/theory.ML
author wenzelm
Sun Jun 05 23:07:29 2005 +0200 (2005-06-05)
changeset 16291 ea4e64b2f25a
parent 16198 cfd070a2cc4d
child 16313 79b37d5e50b1
permissions -rw-r--r--
renamed const_deps to defs;
improved error messages;
major cleanup -- removed quite a bit of dead code;
     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       defs: Defs.graph,
    15       axioms: term Symtab.table,
    16       oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    17       parents: theory list,
    18       ancestors: theory list}
    19   val sign_of: theory -> Sign.sg
    20   val is_draft: theory -> bool
    21   val syn_of: theory -> Syntax.syntax
    22   val parents_of: theory -> theory list
    23   val ancestors_of: theory -> theory list
    24   val subthy: theory * theory -> bool
    25   val eq_thy: theory * theory -> bool
    26   val cert_axm: Sign.sg -> string * term -> string * term
    27   val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    28     string list -> string * string -> string * term
    29   val read_axm: Sign.sg -> string * string -> string * term
    30   val inferT_axm: Sign.sg -> string * term -> string * term
    31 end
    32 
    33 signature THEORY =
    34 sig
    35   include BASIC_THEORY
    36   val axiomK: string
    37   val oracleK: string
    38   (*theory extension primitives*)
    39   val add_classes: (bclass * xclass list) list -> theory -> theory
    40   val add_classes_i: (bclass * class list) list -> theory -> theory
    41   val add_classrel: (xclass * xclass) list -> theory -> theory
    42   val add_classrel_i: (class * class) list -> theory -> theory
    43   val add_defsort: string -> theory -> theory
    44   val add_defsort_i: sort -> theory -> theory
    45   val add_types: (bstring * int * mixfix) list -> theory -> theory
    46   val add_nonterminals: bstring list -> theory -> theory
    47   val add_tyabbrs: (bstring * string list * string * mixfix) list
    48     -> theory -> theory
    49   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
    50     -> theory -> theory
    51   val add_arities: (xstring * string list * string) list -> theory -> theory
    52   val add_arities_i: (string * sort list * sort) list -> theory -> theory
    53   val add_consts: (bstring * string * mixfix) list -> theory -> theory
    54   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    55   val add_syntax: (bstring * string * mixfix) list -> theory -> theory
    56   val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
    57   val add_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    58   val add_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
    59   val del_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    60   val del_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
    61   val add_trfuns:
    62     (string * (Syntax.ast list -> Syntax.ast)) list *
    63     (string * (term list -> term)) list *
    64     (string * (term list -> term)) list *
    65     (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
    66   val add_trfunsT:
    67     (string * (bool -> typ -> term list -> term)) list -> theory -> theory
    68   val add_advanced_trfuns:
    69     (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list *
    70     (string * (Sign.sg -> term list -> term)) list *
    71     (string * (Sign.sg -> term list -> term)) list *
    72     (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list -> theory -> theory
    73   val add_advanced_trfunsT:
    74     (string * (Sign.sg -> bool -> typ -> term list -> term)) list -> theory -> theory
    75   val add_tokentrfuns:
    76     (string * string * (string -> string * real)) list -> theory -> theory
    77   val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
    78     -> theory -> theory
    79   val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    80   val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
    81   val add_axioms: (bstring * string) list -> theory -> theory
    82   val add_axioms_i: (bstring * term) list -> theory -> theory
    83   val add_oracle: bstring * (Sign.sg * Object.T -> term) -> theory -> theory
    84   val add_finals: bool -> string list -> theory -> theory
    85   val add_finals_i: bool -> term list -> theory -> theory
    86   val add_defs: bool -> (bstring * string) list -> theory -> theory
    87   val add_defs_i: bool -> (bstring * term) list -> theory -> theory
    88   val add_path: string -> theory -> theory
    89   val parent_path: theory -> theory
    90   val root_path: theory -> theory
    91   val absolute_path: theory -> theory
    92   val qualified_names: theory -> theory
    93   val no_base_names: theory -> theory
    94   val custom_accesses: (string list -> string list list) -> theory -> theory
    95   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    96     theory -> theory
    97   val restore_naming: theory -> theory -> theory
    98   val hide_space: bool -> string * xstring list -> theory -> theory
    99   val hide_space_i: bool -> string * string list -> theory -> theory
   100   val hide_classes: bool -> string list -> theory -> theory
   101   val hide_types: bool -> string list -> theory -> theory
   102   val hide_consts: bool -> string list -> theory -> theory
   103   val add_name: string -> theory -> theory
   104   val copy: theory -> theory
   105   val prep_ext: theory -> theory
   106   val prep_ext_merge: theory list -> theory
   107   val requires: theory -> string -> string -> unit
   108   val assert_super: theory -> theory -> theory
   109   val pre_pure: theory
   110 end;
   111 
   112 signature PRIVATE_THEORY =
   113 sig
   114   include THEORY
   115   val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
   116     (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
   117   val print_data: Object.kind -> theory -> unit
   118   val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
   119   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
   120 end;
   121 
   122 structure Theory: PRIVATE_THEORY =
   123 struct
   124 
   125 
   126 (** datatype theory **)
   127 
   128 datatype theory =
   129   Theory of {
   130     sign: Sign.sg,
   131     defs: Defs.graph,
   132     axioms: term Symtab.table,
   133     oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
   134     parents: theory list,
   135     ancestors: theory list};
   136 
   137 fun make_theory sign defs axioms oracles parents ancestors =
   138   Theory {sign = sign, defs = defs, axioms = axioms,
   139     oracles = oracles, parents = parents, ancestors = ancestors};
   140 
   141 fun rep_theory (Theory args) = args;
   142 
   143 val sign_of = #sign o rep_theory;
   144 val is_draft = Sign.is_draft o sign_of;
   145 val syn_of = Sign.syn_of o sign_of;
   146 val parents_of = #parents o rep_theory;
   147 val ancestors_of = #ancestors o rep_theory;
   148 
   149 (*errors involving theories*)
   150 exception THEORY of string * theory list;
   151 
   152 (*compare theories*)
   153 val subthy = Sign.subsig o pairself sign_of;
   154 val eq_thy = Sign.eq_sg o pairself sign_of;
   155 
   156 (*check for some theory*)
   157 fun requires thy name what =
   158   if Sign.exists_stamp name (sign_of thy) then ()
   159   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   160 
   161 fun assert_super thy1 thy2 =
   162   if subthy (thy1, thy2) then thy2
   163   else raise THEORY ("Not a super theory", [thy1, thy2]);
   164 
   165 (*partial Pure theory*)
   166 val pre_pure =
   167   make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty [] [];
   168 
   169 
   170 
   171 (** extend theory **)
   172 
   173 (*name spaces*)
   174 val axiomK = "axiom";
   175 val oracleK = "oracle";
   176 
   177 
   178 (* extend logical part of a theory *)
   179 
   180 fun err_dup_axms names =
   181   error ("Duplicate axiom name(s): " ^ commas_quote names);
   182 
   183 fun err_dup_oras names =
   184   error ("Duplicate oracles: " ^ commas_quote names);
   185 
   186 fun ext_theory thy ext_sg new_axms new_oras =
   187   let
   188     val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
   189     val draft = Sign.is_draft sign;
   190     val axioms' = Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
   191       handle Symtab.DUPS names => err_dup_axms names;
   192     val oracles' = Symtab.extend (oracles, new_oras)
   193       handle Symtab.DUPS names => err_dup_oras names;
   194     val (parents', ancestors') =
   195       if draft then (parents, ancestors) else ([thy], thy :: ancestors);
   196   in make_theory (ext_sg sign) defs axioms' oracles' parents' ancestors' end;
   197 
   198 
   199 (* extend signature of a theory *)
   200 
   201 fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) [] [];
   202 
   203 val add_classes            = ext_sign Sign.add_classes;
   204 val add_classes_i          = ext_sign Sign.add_classes_i;
   205 val add_classrel           = ext_sign Sign.add_classrel;
   206 val add_classrel_i         = ext_sign Sign.add_classrel_i;
   207 val add_defsort            = ext_sign Sign.add_defsort;
   208 val add_defsort_i          = ext_sign Sign.add_defsort_i;
   209 val add_types              = ext_sign Sign.add_types;
   210 val add_nonterminals       = ext_sign Sign.add_nonterminals;
   211 val add_tyabbrs            = ext_sign Sign.add_tyabbrs;
   212 val add_tyabbrs_i          = ext_sign Sign.add_tyabbrs_i;
   213 val add_arities            = ext_sign Sign.add_arities;
   214 val add_arities_i          = ext_sign Sign.add_arities_i;
   215 val add_consts             = ext_sign Sign.add_consts;
   216 val add_consts_i           = ext_sign Sign.add_consts_i;
   217 val add_syntax             = ext_sign Sign.add_syntax;
   218 val add_syntax_i           = ext_sign Sign.add_syntax_i;
   219 val add_modesyntax         = curry (ext_sign Sign.add_modesyntax);
   220 val add_modesyntax_i       = curry (ext_sign Sign.add_modesyntax_i);
   221 val del_modesyntax         = curry (ext_sign Sign.del_modesyntax);
   222 val del_modesyntax_i       = curry (ext_sign Sign.del_modesyntax_i);
   223 val add_trfuns             = ext_sign Sign.add_trfuns;
   224 val add_trfunsT            = ext_sign Sign.add_trfunsT;
   225 val add_advanced_trfuns    = ext_sign Sign.add_advanced_trfuns;
   226 val add_advanced_trfunsT   = ext_sign Sign.add_advanced_trfunsT;
   227 val add_tokentrfuns        = ext_sign Sign.add_tokentrfuns;
   228 fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
   229 val add_trrules            = ext_sign Sign.add_trrules;
   230 val add_trrules_i          = ext_sign Sign.add_trrules_i;
   231 val add_path               = ext_sign Sign.add_path;
   232 val parent_path            = add_path "..";
   233 val root_path              = add_path "/";
   234 val absolute_path          = add_path "//";
   235 val qualified_names        = ext_sign (K Sign.qualified_names) ();
   236 val no_base_names          = ext_sign (K Sign.no_base_names) ();
   237 val custom_accesses        = ext_sign Sign.custom_accesses;
   238 val set_policy             = ext_sign Sign.set_policy;
   239 val restore_naming         = ext_sign Sign.restore_naming o sign_of;
   240 val add_space              = ext_sign Sign.add_space;
   241 val hide_space             = ext_sign o Sign.hide_space;
   242 val hide_space_i           = ext_sign o Sign.hide_space_i;
   243 fun hide_classes b         = curry (hide_space_i b) Sign.classK;
   244 fun hide_types b           = curry (hide_space_i b) Sign.typeK;
   245 fun hide_consts b          = curry (hide_space_i b) Sign.constK;
   246 val add_name               = ext_sign Sign.add_name;
   247 val copy                   = ext_sign (K Sign.copy) ();
   248 val prep_ext               = ext_sign (K Sign.prep_ext) ();
   249 
   250 
   251 
   252 (** add axioms **)
   253 
   254 (* prepare axioms *)
   255 
   256 fun err_in_axm name =
   257   error ("The error(s) above occurred in axiom " ^ quote name);
   258 
   259 fun no_vars pp tm =
   260   (case (Term.term_vars tm, Term.term_tvars tm) of
   261     ([], []) => tm
   262   | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
   263       (Pretty.str "Illegal schematic variable(s) in term:" ::
   264        map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns)))));
   265 
   266 fun cert_axm sg (name, raw_tm) =
   267   let
   268     val pp = Sign.pp sg;
   269     val (t, T, _) = Sign.certify_term pp sg raw_tm
   270       handle TYPE (msg, _, _) => error msg
   271         | TERM (msg, _) => error msg;
   272   in
   273     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   274     assert (T = propT) "Term not of type prop";
   275     (name, no_vars pp t)
   276   end;
   277 
   278 (*some duplication of code with read_def_cterm*)
   279 fun read_def_axm (sg, types, sorts) used (name, str) =
   280   let
   281     val ts = Syntax.read (Sign.is_logtype sg) (Sign.syn_of sg) propT str;
   282     val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT);
   283   in cert_axm sg (name, t) end
   284   handle ERROR => err_in_axm name;
   285 
   286 fun read_axm sg name_str = read_def_axm (sg, K NONE, K NONE) [] name_str;
   287 
   288 fun inferT_axm sg (name, pre_tm) =
   289   let
   290     val pp = Sign.pp sg;
   291     val (t, _) = Sign.infer_types pp sg (K NONE) (K NONE) [] true ([pre_tm], propT);
   292   in (name, no_vars pp t) end
   293   handle ERROR => err_in_axm name;
   294 
   295 
   296 (* extend axioms of a theory *)
   297 
   298 local
   299 
   300 fun gen_add_axioms prep_axm raw_axms thy =
   301   let
   302     val sg = sign_of thy;
   303     val raw_axms' = map (apfst (Sign.full_name sg)) raw_axms;
   304     val axioms =
   305       map (apsnd (Term.compress_term o Logic.varify) o prep_axm sg) raw_axms';
   306     val ext_sg = Sign.add_space (axiomK, map fst axioms);
   307   in ext_theory thy ext_sg axioms [] end;
   308 
   309 in
   310 
   311 val add_axioms = gen_add_axioms read_axm;
   312 val add_axioms_i = gen_add_axioms cert_axm;
   313 
   314 end;
   315 
   316 
   317 (* add oracle **)
   318 
   319 fun add_oracle (raw_name, oracle) (thy as Theory {sign, ...}) =
   320   let
   321     val name = Sign.full_name sign raw_name;
   322     val ext_sg = Sign.add_space (oracleK, [name]);
   323   in ext_theory thy ext_sg [] [(name, (oracle, stamp ()))] end;
   324 
   325 
   326 
   327 (** add constant definitions **)
   328 
   329 (* overloading *)
   330 
   331 datatype overloading = Clean | Implicit | Useless;
   332 
   333 fun overloading sg overloaded declT defT =
   334   let
   335     val defT' = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT);
   336   in
   337     if Sign.typ_instance sg (declT, defT') then Clean
   338     else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts defT') then Useless
   339     else if overloaded then Clean
   340     else Implicit
   341   end;
   342 
   343 
   344 (* dest_def *)
   345 
   346 fun dest_def pp tm =
   347   let
   348     fun err msg = raise TERM (msg, [tm]);
   349 
   350     val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
   351       handle TERM _ => err "Not a meta-equality (==)";
   352     val (head, args) = Term.strip_comb lhs;
   353     val (c, T) = Term.dest_Const head
   354       handle TERM _ => err "Head of lhs not a constant";
   355 
   356     fun dest_free (Free (x, _)) = x
   357       | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
   358       | dest_free _ = raise Match;
   359 
   360     val show_terms = commas_quote o map (Pretty.string_of_term pp);
   361     val show_frees = commas_quote o map dest_free;
   362     val show_tfrees = commas_quote o map fst;
   363 
   364     val lhs_nofrees = filter (not o can dest_free) args;
   365     val lhs_dups = duplicates args;
   366     val rhs_extras = term_frees rhs |> fold (remove op =) args;
   367     val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T);
   368   in
   369     if not (null lhs_nofrees) then
   370       err ("Non-variables as arguments on lhs: " ^ show_terms lhs_nofrees)
   371     else if not (null lhs_dups) then
   372       err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
   373     else if not (null rhs_extras) then
   374       err ("Extra variables on rhs: " ^ show_frees rhs_extras)
   375     else if not (null rhs_extrasT) then
   376       err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
   377     else if exists_Const (equal (c, T)) rhs then
   378       err ("Constant to be defined occurs on rhs")
   379     else ((c, T), rhs)
   380   end;
   381 
   382 
   383 (* check_def *)
   384 
   385 fun pretty_const pp (c, T) =
   386  [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   387   Pretty.quote (Pretty.typ pp (Type.freeze_type T))];    (* FIXME zero indexes!? *)
   388 
   389 (* FIXME move error messages to defs.ML !? *)
   390 
   391 fun pretty_path pp path = fold_rev (fn (T, c, def) =>
   392   fn [] => [Pretty.block (pretty_const pp (c, T))]
   393    | prts => Pretty.block (pretty_const pp (c, T) @
   394       [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
   395 
   396 fun defs_circular pp path =
   397   Pretty.str "Cyclic dependency in definitions: " :: pretty_path pp path
   398   |> Pretty.chunks |> Pretty.string_of;
   399 
   400 fun defs_infinite_chain pp path =
   401   Pretty.str "Infinite chain in definitions: " :: pretty_path pp path
   402   |> Pretty.chunks |> Pretty.string_of;
   403 
   404 fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;
   405 
   406 fun defs_final pp const =
   407   (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const)
   408   |> Pretty.block |> Pretty.string_of;
   409 
   410 (* FIXME move to defs.ML; avoid exceptions *)
   411 fun declare sg c defs =
   412   let val T = Sign.the_const_type sg c
   413   in if_none (try (Defs.declare defs) (c, T)) defs end;
   414 
   415 
   416 fun check_def sg overloaded (bname, tm) defs =
   417   let
   418     val pp = Sign.pp sg;
   419     val name = Sign.full_name sg bname;
   420 
   421     fun err msg = error (Pretty.string_of (Pretty.chunks
   422      [Pretty.str msg,
   423       Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ quote name ^ ":"),
   424         Pretty.fbrk, Pretty.quote (Pretty.term pp tm)]]));
   425 
   426     fun show_def const txt =
   427       [Pretty.block (Pretty.str "Definition of " :: pretty_const pp const), Pretty.str txt]
   428       |> Pretty.chunks |> Pretty.string_of;
   429 
   430     val ((c, defT), rhs) = dest_def pp tm handle TERM (msg, _) => err msg;
   431     val rhs_consts = Term.term_constsT rhs;
   432     val declT = Sign.the_const_type sg c;
   433 
   434     val _ =
   435       (case overloading sg overloaded declT defT of
   436         Clean => ()
   437       | Implicit => warning (show_def (c, defT)
   438           ("is strictly less general than the declared type (see " ^ quote name ^ ")"))
   439       | Useless => err (Library.setmp show_sorts true (show_def (c, defT))
   440           "imposes additional sort constraints on the declared type of the constant"));
   441 
   442     val decl_defs = defs |> declare sg c |> fold (declare sg) (map #1 rhs_consts);
   443   in
   444     Defs.define decl_defs (c, defT) name rhs_consts
   445       handle Defs.DEFS msg => err ("DEFS: " ^ msg)   (* FIXME sys_error!? *)
   446         | Defs.CIRCULAR path => err (defs_circular pp path)
   447         | Defs.INFINITE_CHAIN path => err (defs_infinite_chain pp path)
   448         | Defs.CLASH (_, def1, def2) => err (defs_clash def1 def2)
   449         | Defs.FINAL const => err (defs_final pp const)
   450   end;
   451 
   452 
   453 (* add_defs *)
   454 
   455 local
   456 
   457 fun gen_add_defs prep_axm overloaded raw_axms thy =
   458   let
   459     val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
   460     val axms = map (prep_axm sign) raw_axms;
   461     val defs' = fold (check_def sign overloaded) axms defs;
   462   in
   463     make_theory sign defs' axioms oracles parents ancestors
   464     |> add_axioms_i axms
   465   end;
   466 
   467 in
   468 
   469 val add_defs_i = gen_add_defs cert_axm;
   470 val add_defs = gen_add_defs read_axm;
   471 
   472 end;
   473 
   474 
   475 (* add_finals *)
   476 
   477 local
   478 
   479 fun gen_add_finals prep_term overloaded raw_terms thy =
   480   let
   481     val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
   482     fun finalize tm finals =
   483       let
   484         fun err msg = raise TERM (msg, [tm]);    (* FIXME error!? *)
   485         val (c, defT) =
   486           (case tm of Const x => x
   487           | Free _ => err "Attempt to finalize variable (or undeclared constant)"
   488           | _ => err "Attempt to finalize non-constant term");
   489         val declT = Sign.the_const_type sign c
   490           handle TYPE (msg, _, _) => err msg;
   491         val _ =
   492           (case overloading sign overloaded declT defT of
   493             Clean => ()
   494           | Implcit => warning ("Finalizing " ^ quote c ^
   495               " at a strictly less general type than declared")
   496           | Useless => err "Sort constraints stronger than declared");
   497       in
   498         Defs.finalize (if_none (try (Defs.declare finals) (c, declT)) finals) (c, defT)
   499       end;
   500     val defs' = fold finalize (map (prep_term sign) raw_terms) defs;
   501   in make_theory sign defs' axioms oracles parents ancestors end;
   502 
   503 fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
   504 fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg;
   505 
   506 in
   507 
   508 val add_finals = gen_add_finals read_term;
   509 val add_finals_i = gen_add_finals cert_term;
   510 
   511 end;
   512 
   513 
   514 
   515 (** additional theory data **)
   516 
   517 val init_data = curry (ext_sign Sign.init_data);
   518 fun print_data kind = Sign.print_data kind o sign_of;
   519 fun get_data kind f = Sign.get_data kind f o sign_of;
   520 fun put_data kind f = ext_sign (Sign.put_data kind f);
   521 
   522 
   523 
   524 (** merge theories **)          (*exception ERROR*)
   525 
   526 (*merge list of theories from left to right, preparing extend*)
   527 fun prep_ext_merge thys =
   528   let
   529     val sign' = Sign.prep_ext_merge (map sign_of thys);
   530 
   531     val defss = map (#defs o rep_theory) thys;
   532     val defs' = foldl (uncurry Defs.merge) (hd defss) (tl defss)
   533       handle Defs.CIRCULAR namess => error (defs_circular (Sign.pp sign') namess)
   534         | Defs.INFINITE_CHAIN namess => error (defs_infinite_chain (Sign.pp sign') namess);
   535 
   536     val axioms' = Symtab.empty;
   537 
   538     fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   539     val oracles' =
   540       Symtab.make (gen_distinct eq_ora
   541         (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
   542       handle Symtab.DUPS names => err_dup_oras names;
   543 
   544     val parents' = gen_distinct eq_thy thys;
   545     val ancestors' =
   546       gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
   547   in make_theory sign' defs' axioms' oracles' parents' ancestors' end;
   548 
   549 
   550 end;
   551 
   552 structure BasicTheory: BASIC_THEORY = Theory;
   553 open BasicTheory;