src/Pure/theory.ML
author wenzelm
Sat Jun 11 22:15:54 2005 +0200 (2005-06-11)
changeset 16369 96d73621fabb
parent 16339 b02b6da609c3
child 16443 82a116532e3e
permissions -rw-r--r--
renamed hide_classes/types/consts to hide_XXX_i;
added separate hide_classes/types/consts;
refer to name spaces values instead of names;
     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 NameSpace.table,
    16       oracles: ((Sign.sg * Object.T -> term) * stamp) NameSpace.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 axioms_of: theory -> (string * term) list
    37   val all_axioms_of: theory -> (string * term) list
    38   val add_classes: (bstring * xstring list) list -> theory -> theory
    39   val add_classes_i: (bstring * class list) list -> theory -> theory
    40   val add_classrel: (xstring * xstring) list -> theory -> theory
    41   val add_classrel_i: (class * class) list -> theory -> theory
    42   val add_defsort: string -> theory -> theory
    43   val add_defsort_i: sort -> theory -> theory
    44   val add_types: (bstring * int * mixfix) list -> theory -> theory
    45   val add_nonterminals: bstring list -> theory -> theory
    46   val add_tyabbrs: (bstring * string list * string * mixfix) list
    47     -> theory -> theory
    48   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
    49     -> theory -> theory
    50   val add_arities: (xstring * string list * string) list -> theory -> theory
    51   val add_arities_i: (string * sort list * sort) list -> theory -> theory
    52   val add_consts: (bstring * string * mixfix) list -> theory -> theory
    53   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    54   val add_syntax: (bstring * string * mixfix) list -> theory -> theory
    55   val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
    56   val add_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    57   val add_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
    58   val del_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    59   val del_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 qualified_names: theory -> theory
    92   val no_base_names: theory -> theory
    93   val custom_accesses: (string list -> string list list) -> theory -> theory
    94   val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
    95     theory -> theory
    96   val restore_naming: theory -> theory -> theory
    97   val hide_classes: bool -> xstring list -> theory -> theory
    98   val hide_classes_i: bool -> string list -> theory -> theory
    99   val hide_types: bool -> xstring list -> theory -> theory
   100   val hide_types_i: bool -> string list -> theory -> theory
   101   val hide_consts: bool -> xstring list -> theory -> theory
   102   val hide_consts_i: 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 NameSpace.table,
   133     oracles: ((Sign.sg * Object.T -> term) * stamp) NameSpace.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 val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
   150 fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy));
   151 
   152 (*errors involving theories*)
   153 exception THEORY of string * theory list;
   154 
   155 (*compare theories*)
   156 val subthy = Sign.subsig o pairself sign_of;
   157 val eq_thy = Sign.eq_sg o pairself sign_of;
   158 
   159 (*check for some theory*)
   160 fun requires thy name what =
   161   if Sign.exists_stamp name (sign_of thy) then ()
   162   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   163 
   164 fun assert_super thy1 thy2 =
   165   if subthy (thy1, thy2) then thy2
   166   else raise THEORY ("Not a super theory", [thy1, thy2]);
   167 
   168 (*partial Pure theory*)
   169 val pre_pure =
   170   make_theory Sign.pre_pure Defs.empty NameSpace.empty_table NameSpace.empty_table [] [];
   171 
   172 
   173 
   174 (** extend theory **)
   175 
   176 (* extend logical part of a theory *)
   177 
   178 fun err_dup_axms dups = error ("Duplicate axiom(s): " ^ commas_quote dups);
   179 fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
   180 
   181 fun ext_theory thy ext_sg axms oras =
   182   let
   183     val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
   184     val draft = Sign.is_draft sign;
   185     val naming = Sign.naming_of sign;
   186 
   187     val axioms' = NameSpace.extend_table naming
   188         (if draft then axioms else NameSpace.empty_table, axms)
   189       handle Symtab.DUPS dups => err_dup_axms dups;
   190     val oracles' = NameSpace.extend_table naming (oracles, oras)
   191       handle Symtab.DUPS dups => err_dup_oras dups;
   192 
   193     val (parents', ancestors') =
   194       if draft then (parents, ancestors) else ([thy], thy :: ancestors);
   195   in make_theory (ext_sg sign) defs axioms' oracles' parents' ancestors' end;
   196 
   197 
   198 (* extend signature of a theory *)
   199 
   200 fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) [] [];
   201 
   202 val add_classes            = ext_sign Sign.add_classes;
   203 val add_classes_i          = ext_sign Sign.add_classes_i;
   204 val add_classrel           = ext_sign Sign.add_classrel;
   205 val add_classrel_i         = ext_sign Sign.add_classrel_i;
   206 val add_defsort            = ext_sign Sign.add_defsort;
   207 val add_defsort_i          = ext_sign Sign.add_defsort_i;
   208 val add_types              = ext_sign Sign.add_types;
   209 val add_nonterminals       = ext_sign Sign.add_nonterminals;
   210 val add_tyabbrs            = ext_sign Sign.add_tyabbrs;
   211 val add_tyabbrs_i          = ext_sign Sign.add_tyabbrs_i;
   212 val add_arities            = ext_sign Sign.add_arities;
   213 val add_arities_i          = ext_sign Sign.add_arities_i;
   214 val add_consts             = ext_sign Sign.add_consts;
   215 val add_consts_i           = ext_sign Sign.add_consts_i;
   216 val add_syntax             = ext_sign Sign.add_syntax;
   217 val add_syntax_i           = ext_sign Sign.add_syntax_i;
   218 val add_modesyntax         = curry (ext_sign Sign.add_modesyntax);
   219 val add_modesyntax_i       = curry (ext_sign Sign.add_modesyntax_i);
   220 val del_modesyntax         = curry (ext_sign Sign.del_modesyntax);
   221 val del_modesyntax_i       = curry (ext_sign Sign.del_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 qualified_names        = ext_sign (K Sign.qualified_names) ();
   235 val no_base_names          = ext_sign (K Sign.no_base_names) ();
   236 val custom_accesses        = ext_sign Sign.custom_accesses;
   237 val set_policy             = ext_sign Sign.set_policy;
   238 val restore_naming         = ext_sign Sign.restore_naming o sign_of;
   239 val hide_classes           = ext_sign o Sign.hide_classes;
   240 val hide_classes_i         = ext_sign o Sign.hide_classes_i;
   241 val hide_types             = ext_sign o Sign.hide_types;
   242 val hide_types_i           = ext_sign o Sign.hide_types_i;
   243 val hide_consts            = ext_sign o Sign.hide_consts;
   244 val hide_consts_i          = ext_sign o Sign.hide_consts_i;
   245 val add_name               = ext_sign Sign.add_name;
   246 val copy                   = ext_sign (K Sign.copy) ();
   247 val prep_ext               = ext_sign (K Sign.prep_ext) ();
   248 
   249 
   250 
   251 (** add axioms **)
   252 
   253 (* prepare axioms *)
   254 
   255 fun err_in_axm name =
   256   error ("The error(s) above occurred in axiom " ^ quote name);
   257 
   258 fun no_vars pp tm =
   259   (case (Term.term_vars tm, Term.term_tvars tm) of
   260     ([], []) => tm
   261   | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
   262       (Pretty.str "Illegal schematic variable(s) in term:" ::
   263        map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns)))));
   264 
   265 fun cert_axm sg (name, raw_tm) =
   266   let
   267     val pp = Sign.pp sg;
   268     val (t, T, _) = Sign.certify_term pp sg raw_tm
   269       handle TYPE (msg, _, _) => error msg
   270         | TERM (msg, _) => error msg;
   271   in
   272     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   273     assert (T = propT) "Term not of type prop";
   274     (name, no_vars pp t)
   275   end;
   276 
   277 (*some duplication of code with read_def_cterm*)
   278 fun read_def_axm (sg, types, sorts) used (name, str) =
   279   let
   280     val ts = Syntax.read (Sign.is_logtype sg) (Sign.syn_of sg) propT str;
   281     val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT);
   282   in cert_axm sg (name, t) end
   283   handle ERROR => err_in_axm name;
   284 
   285 fun read_axm sg name_str = read_def_axm (sg, K NONE, K NONE) [] name_str;
   286 
   287 fun inferT_axm sg (name, pre_tm) =
   288   let
   289     val pp = Sign.pp sg;
   290     val (t, _) = Sign.infer_types pp sg (K NONE) (K NONE) [] true ([pre_tm], propT);
   291   in (name, no_vars pp t) end
   292   handle ERROR => err_in_axm name;
   293 
   294 
   295 (* extend axioms of a theory *)
   296 
   297 local
   298 
   299 fun gen_add_axioms prep_axm raw_axms thy =
   300   let
   301     val sg = sign_of thy;
   302     val axms = map (apsnd (Term.compress_term o Logic.varify) o prep_axm sg) raw_axms;
   303   in ext_theory thy I axms [] end;
   304 
   305 in
   306 
   307 val add_axioms = gen_add_axioms read_axm;
   308 val add_axioms_i = gen_add_axioms cert_axm;
   309 
   310 end;
   311 
   312 
   313 (* add oracle **)
   314 
   315 fun add_oracle (bname, oracle) thy =
   316   ext_theory thy I [] [(bname, (oracle, stamp ()))];
   317 
   318 
   319 
   320 (** add constant definitions **)
   321 
   322 (* overloading *)
   323 
   324 datatype overloading = Clean | Implicit | Useless;
   325 
   326 fun overloading sg overloaded declT defT =
   327   let
   328     val defT' = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT);
   329   in
   330     if Sign.typ_instance sg (declT, defT') then Clean
   331     else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts defT') then Useless
   332     else if overloaded then Clean
   333     else Implicit
   334   end;
   335 
   336 
   337 (* dest_def *)
   338 
   339 fun dest_def pp tm =
   340   let
   341     fun err msg = raise TERM (msg, [tm]);
   342 
   343     val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
   344       handle TERM _ => err "Not a meta-equality (==)";
   345     val (head, args) = Term.strip_comb lhs;
   346     val (c, T) = Term.dest_Const head
   347       handle TERM _ => err "Head of lhs not a constant";
   348 
   349     fun dest_free (Free (x, _)) = x
   350       | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
   351       | dest_free _ = raise Match;
   352 
   353     val show_terms = commas_quote o map (Pretty.string_of_term pp);
   354     val show_frees = commas_quote o map dest_free;
   355     val show_tfrees = commas_quote o map fst;
   356 
   357     val lhs_nofrees = filter (not o can dest_free) args;
   358     val lhs_dups = duplicates args;
   359     val rhs_extras = term_frees rhs |> fold (remove op =) args;
   360     val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T);
   361   in
   362     if not (null lhs_nofrees) then
   363       err ("Non-variables as arguments on lhs: " ^ show_terms lhs_nofrees)
   364     else if not (null lhs_dups) then
   365       err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
   366     else if not (null rhs_extras) then
   367       err ("Extra variables on rhs: " ^ show_frees rhs_extras)
   368     else if not (null rhs_extrasT) then
   369       err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
   370     else if exists_Const (equal (c, T)) rhs then
   371       err ("Constant to be defined occurs on rhs")
   372     else ((c, T), rhs)
   373   end;
   374 
   375 
   376 (* check_def *)
   377 
   378 fun pretty_const pp (c, T) =
   379  [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   380   Pretty.quote (Pretty.typ pp (Type.freeze_type T))];    (* FIXME zero indexes!? *)
   381 
   382 (* FIXME move error messages to defs.ML !? *)
   383 
   384 fun pretty_path pp path = fold_rev (fn (T, c, def) =>
   385   fn [] => [Pretty.block (pretty_const pp (c, T))]
   386    | prts => Pretty.block (pretty_const pp (c, T) @
   387       [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
   388 
   389 fun chain_history_msg s = 
   390     if Defs.chain_history () then s^": " 
   391     else s^" (set DEFS_CHAIN_HISTORY=ON for full history): "
   392 
   393 fun defs_circular pp path =
   394   Pretty.str (chain_history_msg "Cyclic dependency of definitions") :: pretty_path pp path
   395   |> Pretty.chunks |> Pretty.string_of;
   396 
   397 fun defs_infinite_chain pp path =
   398   Pretty.str (chain_history_msg "Infinite chain of definitions") :: pretty_path pp path
   399   |> Pretty.chunks |> Pretty.string_of;
   400 
   401 fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;
   402 
   403 fun defs_final pp const =
   404   (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const)
   405   |> Pretty.block |> Pretty.string_of;
   406 
   407 (* FIXME move to defs.ML; avoid exceptions *)
   408 fun declare sg c defs =
   409   let val T = Sign.the_const_type sg c
   410   in if_none (try (Defs.declare defs) (c, T)) defs end;
   411 
   412 
   413 fun check_def sg overloaded (bname, tm) defs =
   414   let
   415     val pp = Sign.pp sg;
   416     val name = Sign.full_name sg bname;
   417 
   418     fun err msg = error (Pretty.string_of (Pretty.chunks
   419      [Pretty.str msg,
   420       Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ quote name ^ ":"),
   421         Pretty.fbrk, Pretty.quote (Pretty.term pp tm)]]));
   422 
   423     fun show_def const txt =
   424       [Pretty.block (Pretty.str "Definition of " :: pretty_const pp const), Pretty.str txt]
   425       |> Pretty.chunks |> Pretty.string_of;
   426 
   427     val ((c, defT), rhs) = dest_def pp tm handle TERM (msg, _) => err msg;
   428     val rhs_consts = Term.term_constsT rhs;
   429     val declT = Sign.the_const_type sg c;
   430 
   431     val _ =
   432       (case overloading sg overloaded declT defT of
   433         Clean => ()
   434       | Implicit => warning (show_def (c, defT)
   435           ("is strictly less general than the declared type (see " ^ quote name ^ ")"))
   436       | Useless => err (Library.setmp show_sorts true (show_def (c, defT))
   437           "imposes additional sort constraints on the declared type of the constant"));
   438 
   439     val decl_defs = defs |> declare sg c |> fold (declare sg) (map #1 rhs_consts);
   440   in
   441     Defs.define decl_defs (c, defT) name rhs_consts
   442       handle Defs.DEFS msg => err ("DEFS: " ^ msg)   (* FIXME sys_error!? *)
   443         | Defs.CIRCULAR path => err (defs_circular pp path)
   444         | Defs.INFINITE_CHAIN path => err (defs_infinite_chain pp path)
   445         | Defs.CLASH (_, def1, def2) => err (defs_clash def1 def2)
   446         | Defs.FINAL const => err (defs_final pp const)
   447   end;
   448 
   449 
   450 (* add_defs *)
   451 
   452 local
   453 
   454 fun gen_add_defs prep_axm overloaded raw_axms thy =
   455   let
   456     val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
   457     val axms = map (prep_axm sign) raw_axms;
   458     val defs' = fold (check_def sign overloaded) axms defs;
   459   in
   460     make_theory sign defs' axioms oracles parents ancestors
   461     |> add_axioms_i axms
   462   end;
   463 
   464 in
   465 
   466 val add_defs_i = gen_add_defs cert_axm;
   467 val add_defs = gen_add_defs read_axm;
   468 
   469 end;
   470 
   471 
   472 (* add_finals *)
   473 
   474 local
   475 
   476 fun gen_add_finals prep_term overloaded raw_terms thy =
   477   let
   478     val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
   479     fun finalize tm finals =
   480       let
   481         fun err msg = raise TERM (msg, [tm]);    (* FIXME error!? *)
   482         val (c, defT) =
   483           (case tm of Const x => x
   484           | Free _ => err "Attempt to finalize variable (or undeclared constant)"
   485           | _ => err "Attempt to finalize non-constant term");
   486         val declT = Sign.the_const_type sign c
   487           handle TYPE (msg, _, _) => err msg;
   488         val _ =
   489           (case overloading sign overloaded declT defT of
   490             Clean => ()
   491           | Implcit => warning ("Finalizing " ^ quote c ^
   492               " at a strictly less general type than declared")
   493           | Useless => err "Sort constraints stronger than declared");
   494       in
   495         Defs.finalize (if_none (try (Defs.declare finals) (c, declT)) finals) (c, defT)
   496       end;
   497     val defs' = fold finalize (map (prep_term sign) raw_terms) defs;
   498   in make_theory sign defs' axioms oracles parents ancestors end;
   499 
   500 fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
   501 fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg;
   502 
   503 in
   504 
   505 val add_finals = gen_add_finals read_term;
   506 val add_finals_i = gen_add_finals cert_term;
   507 
   508 end;
   509 
   510 
   511 
   512 (** additional theory data **)
   513 
   514 val init_data = curry (ext_sign Sign.init_data);
   515 fun print_data kind = Sign.print_data kind o sign_of;
   516 fun get_data kind f = Sign.get_data kind f o sign_of;
   517 fun put_data kind f = ext_sign (Sign.put_data kind f);
   518 
   519 
   520 
   521 (** merge theories **)          (*exception ERROR*)
   522 
   523 (*merge list of theories from left to right, preparing extend*)
   524 fun prep_ext_merge thys =
   525   let
   526     val sign' = Sign.prep_ext_merge (map sign_of thys);
   527 
   528     val defss = map (#defs o rep_theory) thys;
   529     val defs' = foldl (uncurry Defs.merge) (hd defss) (tl defss)
   530       handle Defs.CIRCULAR namess => error (defs_circular (Sign.pp sign') namess)
   531         | Defs.INFINITE_CHAIN namess => error (defs_infinite_chain (Sign.pp sign') namess);
   532 
   533     val axioms' = NameSpace.empty_table;
   534 
   535     val oras_spaces = map (#1 o #oracles o rep_theory) thys;
   536     val oras_space' = Library.foldl NameSpace.merge (hd oras_spaces, tl oras_spaces);
   537     fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   538     val oras' =
   539       Symtab.make (gen_distinct eq_ora
   540         (List.concat (map (Symtab.dest o #2 o #oracles o rep_theory) thys)))
   541       handle Symtab.DUPS names => err_dup_oras names;
   542     val oracles' = (oras_space', oras');
   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;