axioms and oracles: NameSpace.table;
authorwenzelm
Thu Jun 09 12:03:26 2005 +0200 (2005-06-09)
changeset 16339b02b6da609c3
parent 16338 3d1851acb4d0
child 16340 fd027bb32896
axioms and oracles: NameSpace.table;
added axioms_of, all_axioms_of;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Thu Jun 09 12:03:25 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Jun 09 12:03:26 2005 +0200
     1.3 @@ -12,8 +12,8 @@
     1.4    val rep_theory: theory ->
     1.5      {sign: Sign.sg,
     1.6        defs: Defs.graph,
     1.7 -      axioms: term Symtab.table,
     1.8 -      oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
     1.9 +      axioms: term NameSpace.table,
    1.10 +      oracles: ((Sign.sg * Object.T -> term) * stamp) NameSpace.table,
    1.11        parents: theory list,
    1.12        ancestors: theory list}
    1.13    val sign_of: theory -> Sign.sg
    1.14 @@ -33,12 +33,11 @@
    1.15  signature THEORY =
    1.16  sig
    1.17    include BASIC_THEORY
    1.18 -  val axiomK: string
    1.19 -  val oracleK: string
    1.20 -  (*theory extension primitives*)
    1.21 -  val add_classes: (bclass * xclass list) list -> theory -> theory
    1.22 -  val add_classes_i: (bclass * class list) list -> theory -> theory
    1.23 -  val add_classrel: (xclass * xclass) list -> theory -> theory
    1.24 +  val axioms_of: theory -> (string * term) list
    1.25 +  val all_axioms_of: theory -> (string * term) list
    1.26 +  val add_classes: (bstring * xstring list) list -> theory -> theory
    1.27 +  val add_classes_i: (bstring * class list) list -> theory -> theory
    1.28 +  val add_classrel: (xstring * xstring) list -> theory -> theory
    1.29    val add_classrel_i: (class * class) list -> theory -> theory
    1.30    val add_defsort: string -> theory -> theory
    1.31    val add_defsort_i: sort -> theory -> theory
    1.32 @@ -129,8 +128,8 @@
    1.33    Theory of {
    1.34      sign: Sign.sg,
    1.35      defs: Defs.graph,
    1.36 -    axioms: term Symtab.table,
    1.37 -    oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    1.38 +    axioms: term NameSpace.table,
    1.39 +    oracles: ((Sign.sg * Object.T -> term) * stamp) NameSpace.table,
    1.40      parents: theory list,
    1.41      ancestors: theory list};
    1.42  
    1.43 @@ -146,6 +145,9 @@
    1.44  val parents_of = #parents o rep_theory;
    1.45  val ancestors_of = #ancestors o rep_theory;
    1.46  
    1.47 +val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
    1.48 +fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy));
    1.49 +
    1.50  (*errors involving theories*)
    1.51  exception THEORY of string * theory list;
    1.52  
    1.53 @@ -164,33 +166,29 @@
    1.54  
    1.55  (*partial Pure theory*)
    1.56  val pre_pure =
    1.57 -  make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty [] [];
    1.58 +  make_theory Sign.pre_pure Defs.empty NameSpace.empty_table NameSpace.empty_table [] [];
    1.59  
    1.60  
    1.61  
    1.62  (** extend theory **)
    1.63  
    1.64 -(*name spaces*)
    1.65 -val axiomK = "axiom";
    1.66 -val oracleK = "oracle";
    1.67 -
    1.68 -
    1.69  (* extend logical part of a theory *)
    1.70  
    1.71 -fun err_dup_axms names =
    1.72 -  error ("Duplicate axiom name(s): " ^ commas_quote names);
    1.73 +fun err_dup_axms dups = error ("Duplicate axiom(s): " ^ commas_quote dups);
    1.74 +fun err_dup_oras dups = error ("Duplicate oracle(s): " ^ commas_quote dups);
    1.75  
    1.76 -fun err_dup_oras names =
    1.77 -  error ("Duplicate oracles: " ^ commas_quote names);
    1.78 -
    1.79 -fun ext_theory thy ext_sg new_axms new_oras =
    1.80 +fun ext_theory thy ext_sg axms oras =
    1.81    let
    1.82      val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
    1.83      val draft = Sign.is_draft sign;
    1.84 -    val axioms' = Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
    1.85 -      handle Symtab.DUPS names => err_dup_axms names;
    1.86 -    val oracles' = Symtab.extend (oracles, new_oras)
    1.87 -      handle Symtab.DUPS names => err_dup_oras names;
    1.88 +    val naming = Sign.naming_of sign;
    1.89 +
    1.90 +    val axioms' = NameSpace.extend_table naming
    1.91 +        (if draft then axioms else NameSpace.empty_table, axms)
    1.92 +      handle Symtab.DUPS dups => err_dup_axms dups;
    1.93 +    val oracles' = NameSpace.extend_table naming (oracles, oras)
    1.94 +      handle Symtab.DUPS dups => err_dup_oras dups;
    1.95 +
    1.96      val (parents', ancestors') =
    1.97        if draft then (parents, ancestors) else ([thy], thy :: ancestors);
    1.98    in make_theory (ext_sg sign) defs axioms' oracles' parents' ancestors' end;
    1.99 @@ -237,7 +235,6 @@
   1.100  val custom_accesses        = ext_sign Sign.custom_accesses;
   1.101  val set_policy             = ext_sign Sign.set_policy;
   1.102  val restore_naming         = ext_sign Sign.restore_naming o sign_of;
   1.103 -val add_space              = ext_sign Sign.add_space;
   1.104  val hide_space             = ext_sign o Sign.hide_space;
   1.105  val hide_space_i           = ext_sign o Sign.hide_space_i;
   1.106  fun hide_classes b         = curry (hide_space_i b) Sign.classK;
   1.107 @@ -300,11 +297,8 @@
   1.108  fun gen_add_axioms prep_axm raw_axms thy =
   1.109    let
   1.110      val sg = sign_of thy;
   1.111 -    val raw_axms' = map (apfst (Sign.full_name sg)) raw_axms;
   1.112 -    val axioms =
   1.113 -      map (apsnd (Term.compress_term o Logic.varify) o prep_axm sg) raw_axms';
   1.114 -    val ext_sg = Sign.add_space (axiomK, map fst axioms);
   1.115 -  in ext_theory thy ext_sg axioms [] end;
   1.116 +    val axms = map (apsnd (Term.compress_term o Logic.varify) o prep_axm sg) raw_axms;
   1.117 +  in ext_theory thy I axms [] end;
   1.118  
   1.119  in
   1.120  
   1.121 @@ -316,11 +310,8 @@
   1.122  
   1.123  (* add oracle **)
   1.124  
   1.125 -fun add_oracle (raw_name, oracle) (thy as Theory {sign, ...}) =
   1.126 -  let
   1.127 -    val name = Sign.full_name sign raw_name;
   1.128 -    val ext_sg = Sign.add_space (oracleK, [name]);
   1.129 -  in ext_theory thy ext_sg [] [(name, (oracle, stamp ()))] end;
   1.130 +fun add_oracle (bname, oracle) thy =
   1.131 +  ext_theory thy I [] [(bname, (oracle, stamp ()))];
   1.132  
   1.133  
   1.134  
   1.135 @@ -537,13 +528,16 @@
   1.136        handle Defs.CIRCULAR namess => error (defs_circular (Sign.pp sign') namess)
   1.137          | Defs.INFINITE_CHAIN namess => error (defs_infinite_chain (Sign.pp sign') namess);
   1.138  
   1.139 -    val axioms' = Symtab.empty;
   1.140 +    val axioms' = NameSpace.empty_table;
   1.141  
   1.142 +    val oras_spaces = map (#1 o #oracles o rep_theory) thys;
   1.143 +    val oras_space' = Library.foldl NameSpace.merge (hd oras_spaces, tl oras_spaces);
   1.144      fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   1.145 -    val oracles' =
   1.146 +    val oras' =
   1.147        Symtab.make (gen_distinct eq_ora
   1.148 -        (List.concat (map (Symtab.dest o #oracles o rep_theory) thys)))
   1.149 +        (List.concat (map (Symtab.dest o #2 o #oracles o rep_theory) thys)))
   1.150        handle Symtab.DUPS names => err_dup_oras names;
   1.151 +    val oracles' = (oras_space', oras');
   1.152  
   1.153      val parents' = gen_distinct eq_thy thys;
   1.154      val ancestors' =