src/Pure/theory.ML
changeset 24666 9885a86f14a8
parent 24626 85eceef2edc7
child 24708 d9b00117365e
     1.1 --- a/src/Pure/theory.ML	Thu Sep 20 20:56:33 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Sep 20 20:56:34 2007 +0200
     1.3 @@ -15,30 +15,28 @@
     1.4  sig
     1.5    include BASIC_THEORY
     1.6    include SIGN_THEORY
     1.7 +  val assert_super: theory -> theory -> theory
     1.8    val parents_of: theory -> theory list
     1.9    val ancestors_of: theory -> theory list
    1.10 -  val begin_theory: string -> theory list -> theory
    1.11 -  val end_theory: theory -> theory
    1.12 +  val check_thy: theory -> theory_ref
    1.13 +  val deref: theory_ref -> theory
    1.14 +  val merge: theory * theory -> theory
    1.15 +  val merge_refs: theory_ref * theory_ref -> theory_ref
    1.16 +  val merge_list: theory list -> theory
    1.17    val checkpoint: theory -> theory
    1.18    val copy: theory -> theory
    1.19 -  val rep_theory: theory ->
    1.20 -   {axioms: term NameSpace.table,
    1.21 -    defs: Defs.T,
    1.22 -    oracles: ((theory * Object.T -> term) * stamp) NameSpace.table}
    1.23 +  val requires: theory -> string -> string -> unit
    1.24    val axiom_space: theory -> NameSpace.T
    1.25    val axiom_table: theory -> term Symtab.table
    1.26    val oracle_space: theory -> NameSpace.T
    1.27    val oracle_table: theory -> ((theory * Object.T -> term) * stamp) Symtab.table
    1.28    val axioms_of: theory -> (string * term) list
    1.29    val all_axioms_of: theory -> (string * term) list
    1.30 -  val defs_of : theory -> Defs.T
    1.31 -  val check_thy: theory -> theory_ref
    1.32 -  val deref: theory_ref -> theory
    1.33 -  val merge: theory * theory -> theory
    1.34 -  val merge_refs: theory_ref * theory_ref -> theory_ref
    1.35 -  val merge_list: theory list -> theory
    1.36 -  val requires: theory -> string -> string -> unit
    1.37 -  val assert_super: theory -> theory -> theory
    1.38 +  val defs_of: theory -> Defs.T
    1.39 +  val at_begin: (theory -> theory option) -> theory -> theory
    1.40 +  val at_end: (theory -> theory option) -> theory -> theory
    1.41 +  val begin_theory: string -> theory list -> theory
    1.42 +  val end_theory: theory -> theory
    1.43    val cert_axm: theory -> string * term -> string * term
    1.44    val read_axm: theory -> string * string -> string * term
    1.45    val add_axioms: (bstring * string) list -> theory -> theory
    1.46 @@ -51,111 +49,11 @@
    1.47    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
    1.48  end
    1.49  
    1.50 -signature THEORY_INTERPRETATOR =
    1.51 -sig
    1.52 -  type T
    1.53 -  type interpretator = T list -> theory -> theory
    1.54 -  val add_those: T list -> theory -> theory
    1.55 -  val all_those: theory -> T list
    1.56 -  val add_interpretator: interpretator -> theory -> theory
    1.57 -  val init: theory -> theory
    1.58 -end;
    1.59 -
    1.60 -signature THEORY_INTERPRETATOR_KEY =
    1.61 -sig
    1.62 -  type T
    1.63 -  val eq: T * T -> bool
    1.64 -end;
    1.65 -
    1.66 -structure Theory =
    1.67 +structure Theory: THEORY =
    1.68  struct
    1.69  
    1.70  
    1.71 -(** datatype thy **)
    1.72 -
    1.73 -datatype thy = Thy of
    1.74 - {axioms: term NameSpace.table,
    1.75 -  defs: Defs.T,
    1.76 -  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
    1.77 -  consolidate: theory -> theory};
    1.78 -
    1.79 -fun make_thy (axioms, defs, oracles, consolidate) =
    1.80 -  Thy {axioms = axioms, defs = defs, oracles = oracles, consolidate = consolidate};
    1.81 -
    1.82 -fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
    1.83 -fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
    1.84 -
    1.85 -structure ThyData = TheoryDataFun
    1.86 -(
    1.87 -  type T = thy;
    1.88 -  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, I);
    1.89 -  val copy = I;
    1.90 -
    1.91 -  fun extend (Thy {axioms, defs, oracles, consolidate}) =
    1.92 -    make_thy (NameSpace.empty_table, defs, oracles, consolidate);
    1.93 -
    1.94 -  fun merge pp (thy1, thy2) =
    1.95 -    let
    1.96 -      val Thy {axioms = _, defs = defs1, oracles = oracles1,
    1.97 -        consolidate = consolidate1} = thy1;
    1.98 -      val Thy {axioms = _, defs = defs2, oracles = oracles2,
    1.99 -        consolidate = consolidate2} = thy2;
   1.100 -
   1.101 -      val axioms = NameSpace.empty_table;
   1.102 -      val defs = Defs.merge pp (defs1, defs2);
   1.103 -      val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   1.104 -        handle Symtab.DUP dup => err_dup_ora dup;
   1.105 -      val consolidate = consolidate1 #> consolidate2;
   1.106 -    in make_thy (axioms, defs, oracles, consolidate) end;
   1.107 -);
   1.108 -
   1.109 -fun rep_theory thy = ThyData.get thy |> (fn Thy {axioms, defs, oracles, ...} =>
   1.110 -  {axioms = axioms, defs = defs, oracles = oracles});
   1.111 -
   1.112 -fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, consolidate}) =>
   1.113 -  make_thy (f (axioms, defs, oracles, consolidate)));
   1.114 -
   1.115 -fun map_axioms f = map_thy
   1.116 -  (fn (axioms, defs, oracles, consolidate) => (f axioms, defs, oracles, consolidate));
   1.117 -fun map_defs f = map_thy
   1.118 -  (fn (axioms, defs, oracles, consolidate) => (axioms, f defs, oracles, consolidate));
   1.119 -fun map_oracles f = map_thy
   1.120 -  (fn (axioms, defs, oracles, consolidate) => (axioms, defs, f oracles, consolidate));
   1.121 -
   1.122 -
   1.123 -(* basic operations *)
   1.124 -
   1.125 -val axiom_space = #1 o #axioms o rep_theory;
   1.126 -val axiom_table = #2 o #axioms o rep_theory;
   1.127 -
   1.128 -val oracle_space = #1 o #oracles o rep_theory;
   1.129 -val oracle_table = #2 o #oracles o rep_theory;
   1.130 -
   1.131 -val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
   1.132 -
   1.133 -val defs_of = #defs o rep_theory;
   1.134 -
   1.135 -fun requires thy name what =
   1.136 -  if Context.exists_name name thy then ()
   1.137 -  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   1.138 -
   1.139 -
   1.140 -(* interpretators *)
   1.141 -
   1.142 -fun add_consolidate f = map_thy
   1.143 -  (fn (axioms, defs, oracles, consolidate) => (axioms, defs, oracles, consolidate #> f));
   1.144 -
   1.145 -fun consolidate thy =
   1.146 -  let
   1.147 -    val Thy {consolidate, ...} = ThyData.get thy;
   1.148 -  in
   1.149 -    thy |> consolidate
   1.150 -  end;
   1.151 -
   1.152 -
   1.153 -(** type theory **)
   1.154 -
   1.155 -(* context operations *)
   1.156 +(** theory context operations **)
   1.157  
   1.158  val eq_thy = Context.eq_thy;
   1.159  val subthy = Context.subthy;
   1.160 @@ -169,17 +67,128 @@
   1.161  
   1.162  val check_thy = Context.check_thy;
   1.163  val deref = Context.deref;
   1.164 +
   1.165  val merge = Context.merge;
   1.166  val merge_refs = Context.merge_refs;
   1.167  
   1.168  fun merge_list [] = raise THEORY ("Empty merge of theories", [])
   1.169    | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
   1.170  
   1.171 -val begin_theory = Sign.local_path o consolidate oo Context.begin_thy Sign.pp;
   1.172 -val end_theory = Context.finish_thy;
   1.173  val checkpoint = Context.checkpoint_thy;
   1.174  val copy = Context.copy_thy;
   1.175  
   1.176 +fun requires thy name what =
   1.177 +  if Context.exists_name name thy then ()
   1.178 +  else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   1.179 +
   1.180 +
   1.181 +
   1.182 +(** theory wrappers **)
   1.183 +
   1.184 +type wrapper = (theory -> theory option) * stamp;
   1.185 +
   1.186 +fun apply_wrappers (wrappers: wrapper list) =
   1.187 +  let
   1.188 +    fun app [] res = res
   1.189 +      | app ((f, _) :: fs) (changed, thy) =
   1.190 +          (case f thy of
   1.191 +            NONE => app fs (changed, thy)
   1.192 +          | SOME thy' => app fs (true, thy'));
   1.193 +    fun app_fixpoint thy =
   1.194 +      (case app wrappers (false, thy) of
   1.195 +        (false, _) => thy
   1.196 +      | (true, thy') => app_fixpoint thy');
   1.197 +  in app_fixpoint end;
   1.198 +
   1.199 +
   1.200 +
   1.201 +(** datatype thy **)
   1.202 +
   1.203 +datatype thy = Thy of
   1.204 + {axioms: term NameSpace.table,
   1.205 +  defs: Defs.T,
   1.206 +  oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
   1.207 +  wrappers: wrapper list * wrapper list};
   1.208 +
   1.209 +fun make_thy (axioms, defs, oracles, wrappers) =
   1.210 +  Thy {axioms = axioms, defs = defs, oracles = oracles, wrappers = wrappers};
   1.211 +
   1.212 +fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
   1.213 +fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
   1.214 +
   1.215 +structure ThyData = TheoryDataFun
   1.216 +(
   1.217 +  type T = thy;
   1.218 +  val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, ([], []));
   1.219 +  val copy = I;
   1.220 +
   1.221 +  fun extend (Thy {axioms, defs, oracles, wrappers}) =
   1.222 +    make_thy (NameSpace.empty_table, defs, oracles, wrappers);
   1.223 +
   1.224 +  fun merge pp (thy1, thy2) =
   1.225 +    let
   1.226 +      val Thy {axioms = _, defs = defs1, oracles = oracles1, wrappers = (bgs1, ens1)} = thy1;
   1.227 +      val Thy {axioms = _, defs = defs2, oracles = oracles2, wrappers = (bgs2, ens2)} = thy2;
   1.228 +
   1.229 +      val axioms' = NameSpace.empty_table;
   1.230 +      val defs' = Defs.merge pp (defs1, defs2);
   1.231 +      val oracles' = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   1.232 +        handle Symtab.DUP dup => err_dup_ora dup;
   1.233 +      val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   1.234 +      val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   1.235 +    in make_thy (axioms', defs', oracles', (bgs', ens')) end;
   1.236 +);
   1.237 +
   1.238 +fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
   1.239 +
   1.240 +fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, wrappers}) =>
   1.241 +  make_thy (f (axioms, defs, oracles, wrappers)));
   1.242 +
   1.243 +
   1.244 +fun map_axioms f = map_thy
   1.245 +  (fn (axioms, defs, oracles, wrappers) => (f axioms, defs, oracles, wrappers));
   1.246 +
   1.247 +fun map_defs f = map_thy
   1.248 +  (fn (axioms, defs, oracles, wrappers) => (axioms, f defs, oracles, wrappers));
   1.249 +
   1.250 +fun map_oracles f = map_thy
   1.251 +  (fn (axioms, defs, oracles, wrappers) => (axioms, defs, f oracles, wrappers));
   1.252 +
   1.253 +fun map_wrappers f = map_thy
   1.254 +  (fn (axioms, defs, oracles, wrappers) => (axioms, defs, oracles, f wrappers));
   1.255 +
   1.256 +
   1.257 +(* basic operations *)
   1.258 +
   1.259 +val axiom_space = #1 o #axioms o rep_theory;
   1.260 +val axiom_table = #2 o #axioms o rep_theory;
   1.261 +
   1.262 +val oracle_space = #1 o #oracles o rep_theory;
   1.263 +val oracle_table = #2 o #oracles o rep_theory;
   1.264 +
   1.265 +val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
   1.266 +fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
   1.267 +
   1.268 +val defs_of = #defs o rep_theory;
   1.269 +
   1.270 +
   1.271 +(* begin/end theory *)
   1.272 +
   1.273 +val begin_wrappers = rev o #1 o #wrappers o rep_theory;
   1.274 +val end_wrappers = rev o #2 o #wrappers o rep_theory;
   1.275 +
   1.276 +fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
   1.277 +fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
   1.278 +
   1.279 +fun begin_theory name imports =
   1.280 +  let
   1.281 +    val thy = Context.begin_thy Sign.pp name imports;
   1.282 +    val wrappers = begin_wrappers thy;
   1.283 +  in thy |> Sign.local_path |> apply_wrappers wrappers end;
   1.284 +
   1.285 +fun end_theory thy =
   1.286 +  thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;
   1.287 +
   1.288  
   1.289  (* signature operations *)
   1.290  
   1.291 @@ -188,10 +197,7 @@
   1.292  
   1.293  
   1.294  
   1.295 -(** axioms **)
   1.296 -
   1.297 -fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
   1.298 -
   1.299 +(** add axioms **)
   1.300  
   1.301  (* prepare axioms *)
   1.302  
   1.303 @@ -350,66 +356,5 @@
   1.304  
   1.305  end;
   1.306  
   1.307 -functor TheoryInterpretatorFun(Key: THEORY_INTERPRETATOR_KEY) : THEORY_INTERPRETATOR =
   1.308 -struct
   1.309 -
   1.310 -open Key;
   1.311 -
   1.312 -type interpretator = T list -> theory -> theory;
   1.313 -
   1.314 -fun apply ips x = fold_rev (fn (_, f) => f x) ips;
   1.315 -
   1.316 -structure InterpretatorData = TheoryDataFun (
   1.317 -  type T = ((serial * interpretator) list * T list) * (theory -> theory);
   1.318 -  val empty = (([], []), I);
   1.319 -  val extend = I;
   1.320 -  val copy = I;
   1.321 -  fun merge pp (((interpretators1, done1), upd1), ((interpretators2, done2), upd2)) =
   1.322 -    let
   1.323 -      fun diff (interpretators1 : (serial * interpretator) list, done1)
   1.324 -        (interpretators2, done2) = let
   1.325 -          val interpretators = subtract (eq_fst (op =)) interpretators1 interpretators2;
   1.326 -          val undone = subtract eq done2 done1;
   1.327 -        in apply interpretators undone end;
   1.328 -      val interpretators = AList.merge (op =) (K true) (interpretators1, interpretators2);
   1.329 -      val done = Library.merge eq (done1, done2);
   1.330 -      val upd_new = diff (interpretators2, done2) (interpretators1, done1)
   1.331 -        #> diff (interpretators1, done1) (interpretators2, done2);
   1.332 -      val upd = upd1 #> upd2 #> upd_new;
   1.333 -    in ((interpretators, done), upd) end;
   1.334 -);
   1.335 -
   1.336 -fun consolidate thy =
   1.337 -  let
   1.338 -    val (_, upd) = InterpretatorData.get thy;
   1.339 -  in
   1.340 -    thy |> upd |> (InterpretatorData.map o apsnd) (K I)
   1.341 -  end;
   1.342 -
   1.343 -val init = Theory.add_consolidate consolidate;
   1.344 -
   1.345 -fun add_those xs thy =
   1.346 -  let
   1.347 -    val ((interpretators, _), _) = InterpretatorData.get thy;
   1.348 -  in
   1.349 -    thy
   1.350 -    |> apply interpretators xs
   1.351 -    |> (InterpretatorData.map o apfst o apsnd) (append xs)
   1.352 -  end;
   1.353 -
   1.354 -val all_those = snd o fst o InterpretatorData.get;
   1.355 -
   1.356 -fun add_interpretator interpretator thy =
   1.357 -  let
   1.358 -    val ((interpretators, xs), _) = InterpretatorData.get thy;
   1.359 -  in
   1.360 -    thy
   1.361 -    |> interpretator (rev xs)
   1.362 -    |> (InterpretatorData.map o apfst o apfst) (cons (serial (), interpretator))
   1.363 -  end;
   1.364 -
   1.365 -end;
   1.366 -
   1.367 -structure Theory: THEORY = Theory;
   1.368  structure BasicTheory: BASIC_THEORY = Theory;
   1.369  open BasicTheory;