src/Pure/theory.ML
changeset 22684 a614c5f506ea
parent 22600 043232f8dde2
child 22689 b800228434a8
     1.1 --- a/src/Pure/theory.ML	Sat Apr 14 17:36:14 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Sat Apr 14 17:36:16 2007 +0200
     1.3 @@ -7,32 +7,29 @@
     1.4  
     1.5  signature BASIC_THEORY =
     1.6  sig
     1.7 -  val rep_theory: theory ->
     1.8 -   {axioms: term NameSpace.table,
     1.9 -    defs: Defs.T,
    1.10 -    oracles: ((theory * Object.T -> term) * stamp) NameSpace.table}
    1.11 -  val parents_of: theory -> theory list
    1.12 -  val ancestors_of: theory -> theory list
    1.13    val eq_thy: theory * theory -> bool
    1.14    val subthy: theory * theory -> bool
    1.15 -  val cert_axm: theory -> string * term -> string * term
    1.16 -  val read_def_axm: theory * (indexname -> typ option) * (indexname -> sort option) ->
    1.17 -    string list -> string * string -> string * term
    1.18 -  val read_axm: theory -> string * string -> string * term
    1.19 -  val inferT_axm: theory -> string * term -> string * term
    1.20  end
    1.21  
    1.22  signature THEORY =
    1.23  sig
    1.24    include BASIC_THEORY
    1.25    include SIGN_THEORY
    1.26 +  val parents_of: theory -> theory list
    1.27 +  val ancestors_of: theory -> theory list
    1.28    val begin_theory: string -> theory list -> theory
    1.29    val end_theory: theory -> theory
    1.30    val checkpoint: theory -> theory
    1.31    val copy: theory -> theory
    1.32    val init_data: theory -> theory
    1.33 +  val rep_theory: theory ->
    1.34 +   {axioms: term NameSpace.table,
    1.35 +    defs: Defs.T,
    1.36 +    oracles: ((theory * Object.T -> term) * stamp) NameSpace.table}
    1.37    val axiom_space: theory -> NameSpace.T
    1.38 +  val axiom_table: theory -> term Symtab.table
    1.39    val oracle_space: theory -> NameSpace.T
    1.40 +  val oracle_table: theory -> ((theory * Object.T -> term) * stamp) Symtab.table
    1.41    val axioms_of: theory -> (string * term) list
    1.42    val all_axioms_of: theory -> (string * term) list
    1.43    val defs_of : theory -> Defs.T
    1.44 @@ -43,6 +40,9 @@
    1.45    val merge_list: theory list -> theory                    (*exception TERM*)
    1.46    val requires: theory -> string -> string -> unit
    1.47    val assert_super: theory -> theory -> theory
    1.48 +  val cert_axm: theory -> string * term -> string * term
    1.49 +  val read_axm: theory -> string * string -> string * term
    1.50 +  val inferT_axm: theory -> string * term -> string * term
    1.51    val add_axioms: (bstring * string) list -> theory -> theory
    1.52    val add_axioms_i: (bstring * term) list -> theory -> theory
    1.53    val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
    1.54 @@ -139,7 +139,10 @@
    1.55  (* basic operations *)
    1.56  
    1.57  val axiom_space = #1 o #axioms o rep_theory;
    1.58 +val axiom_table = #2 o #axioms o rep_theory;
    1.59 +
    1.60  val oracle_space = #1 o #oracles o rep_theory;
    1.61 +val oracle_table = #2 o #oracles o rep_theory;
    1.62  
    1.63  val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
    1.64  fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
    1.65 @@ -173,17 +176,15 @@
    1.66      (name, Sign.no_vars (Sign.pp thy) t)
    1.67    end;
    1.68  
    1.69 -fun read_def_axm (thy, types, sorts) used (name, str) =
    1.70 +fun read_axm thy (name, str) =
    1.71    let
    1.72      val ts = Syntax.read (ProofContext.init thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
    1.73      val (t, _) =
    1.74        Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
    1.75 -        types sorts (Name.make_context used) true (ts, propT);
    1.76 +        (K NONE) (K NONE) Name.context true (ts, propT);
    1.77    in cert_axm thy (name, t) end
    1.78    handle ERROR msg => err_in_axm msg name;
    1.79  
    1.80 -fun read_axm thy name_str = read_def_axm (thy, K NONE, K NONE) [] name_str;
    1.81 -
    1.82  fun inferT_axm thy (name, pre_tm) =
    1.83    let
    1.84      val pp = Sign.pp thy;