replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
authorwenzelm
Fri Aug 03 16:28:15 2007 +0200 (2007-08-03)
changeset 241378d7896398147
parent 24136 0c6c943d8f1e
child 24138 bd3fc8ff6bc9
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
doc-src/IsarImplementation/Thy/prelim.thy
src/HOL/OrderedGroup.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/res_axioms.ML
src/Pure/Isar/element.ML
src/Pure/Tools/codegen_data.ML
src/Pure/pure_thy.ML
src/Pure/theory.ML
src/Tools/Compute_Oracle/compute.ML
src/Tools/Compute_Oracle/linker.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Thu Aug 02 23:18:13 2007 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Fri Aug 03 16:28:15 2007 +0200
     1.3 @@ -156,8 +156,8 @@
     1.4    \end{mldecls}
     1.5    \begin{mldecls}
     1.6    @{index_ML_type theory_ref} \\
     1.7 -  @{index_ML Theory.self_ref: "theory -> theory_ref"} \\
     1.8    @{index_ML Theory.deref: "theory_ref -> theory"} \\
     1.9 +  @{index_ML Theory.check_thy: "theory -> theory_ref"} \\
    1.10    \end{mldecls}
    1.11  
    1.12    \begin{description}
    1.13 @@ -187,12 +187,14 @@
    1.14    always valid theory; updates on the original are propagated
    1.15    automatically.
    1.16  
    1.17 -  \item @{ML "Theory.self_ref"}~@{text "thy"} and @{ML
    1.18 -  "Theory.deref"}~@{text "thy_ref"} convert between @{ML_type
    1.19 -  "theory"} and @{ML_type "theory_ref"}.  As the referenced theory
    1.20 -  evolves monotonically over time, later invocations of @{ML
    1.21 +  \item @{ML "Theory.deref"}~@{text "thy_ref"} turns a @{ML_type
    1.22 +  "theory_ref"} into an @{ML_type "theory"} value.  As the referenced
    1.23 +  theory evolves monotonically over time, later invocations of @{ML
    1.24    "Theory.deref"} may refer to a larger context.
    1.25  
    1.26 +  \item @{ML "Theory.check_thy"}~@{text "thy"} produces a @{ML_type
    1.27 +  "theory_ref"} from a valid @{ML_type "theory"} value.
    1.28 +
    1.29    \end{description}
    1.30  *}
    1.31  
     2.1 --- a/src/HOL/OrderedGroup.thy	Thu Aug 02 23:18:13 2007 +0200
     2.2 +++ b/src/HOL/OrderedGroup.thy	Fri Aug 03 16:28:15 2007 +0200
     2.3 @@ -1104,7 +1104,7 @@
     2.4    
     2.5  val eq_reflection = @{thm eq_reflection};
     2.6    
     2.7 -val thy_ref = Theory.self_ref @{theory};
     2.8 +val thy_ref = Theory.check_thy @{theory};
     2.9  
    2.10  val T = TFree("'a", ["OrderedGroup.ab_group_add"]);
    2.11  
     3.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Aug 02 23:18:13 2007 +0200
     3.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Aug 03 16:28:15 2007 +0200
     3.3 @@ -596,7 +596,7 @@
     3.4    let
     3.5      fun add_eq_thms (dtco, (_, (vs, cs))) thy =
     3.6        let
     3.7 -        val thy_ref = Theory.self_ref thy;
     3.8 +        val thy_ref = Theory.check_thy thy;
     3.9          val const = ("op =", SOME dtco);
    3.10          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
    3.11        in
     4.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Aug 02 23:18:13 2007 +0200
     4.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Aug 03 16:28:15 2007 +0200
     4.3 @@ -80,7 +80,7 @@
     4.4    inside that theory -- because it's needed for Skolemization *)
     4.5  
     4.6  (*This will refer to the final version of theory ATP_Linkup.*)
     4.7 -val recon_thy_ref = Theory.self_ref (the_context ());
     4.8 +val recon_thy_ref = Theory.check_thy @{theory}
     4.9  
    4.10  (*If called while ATP_Linkup is being created, it will transfer to the
    4.11    current version. If called afterward, it will transfer to the final version.*)
     5.1 --- a/src/Pure/Isar/element.ML	Thu Aug 02 23:18:13 2007 +0200
     5.2 +++ b/src/Pure/Isar/element.ML	Fri Aug 03 16:28:15 2007 +0200
     5.3 @@ -411,7 +411,7 @@
     5.4      in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
     5.5  
     5.6  fun instT_morphism thy env =
     5.7 -  let val thy_ref = Theory.self_ref thy in
     5.8 +  let val thy_ref = Theory.check_thy thy in
     5.9      Morphism.morphism
    5.10       {name = I, var = I,
    5.11        typ = instT_type env,
    5.12 @@ -460,7 +460,7 @@
    5.13      end;
    5.14  
    5.15  fun inst_morphism thy envs =
    5.16 -  let val thy_ref = Theory.self_ref thy in
    5.17 +  let val thy_ref = Theory.check_thy thy in
    5.18      Morphism.morphism
    5.19       {name = I, var = I,
    5.20        typ = instT_type (#1 envs),
     6.1 --- a/src/Pure/Tools/codegen_data.ML	Thu Aug 02 23:18:13 2007 +0200
     6.2 +++ b/src/Pure/Tools/codegen_data.ML	Fri Aug 03 16:28:15 2007 +0200
     6.3 @@ -100,7 +100,7 @@
     6.4    case Susp.peek r
     6.5     of SOME thms => (Susp.value o f thy) thms
     6.6       | NONE => let
     6.7 -          val thy_ref = Theory.self_ref thy;
     6.8 +          val thy_ref = Theory.check_thy thy;
     6.9          in lazy_thms (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    6.10  
    6.11  fun merge' _ ([], []) = (false, [])
     7.1 --- a/src/Pure/pure_thy.ML	Thu Aug 02 23:18:13 2007 +0200
     7.2 +++ b/src/Pure/pure_thy.ML	Fri Aug 03 16:28:15 2007 +0200
     7.3 @@ -238,8 +238,8 @@
     7.4  
     7.5  fun lookup_thms thy =
     7.6    let
     7.7 -    val thy_ref = Theory.self_ref thy;
     7.8      val (space, thms) = #theorems (get_theorems thy);
     7.9 +    val thy_ref = Theory.check_thy thy;
    7.10    in
    7.11      fn name =>
    7.12        Option.map (map (Thm.transfer (Theory.deref thy_ref)))     (*dynamic identity*)
     8.1 --- a/src/Pure/theory.ML	Thu Aug 02 23:18:13 2007 +0200
     8.2 +++ b/src/Pure/theory.ML	Fri Aug 03 16:28:15 2007 +0200
     8.3 @@ -32,7 +32,7 @@
     8.4    val axioms_of: theory -> (string * term) list
     8.5    val all_axioms_of: theory -> (string * term) list
     8.6    val defs_of : theory -> Defs.T
     8.7 -  val self_ref: theory -> theory_ref
     8.8 +  val check_thy: theory -> theory_ref
     8.9    val deref: theory_ref -> theory
    8.10    val merge: theory * theory -> theory
    8.11    val merge_refs: theory_ref * theory_ref -> theory_ref
    8.12 @@ -65,7 +65,7 @@
    8.13  val parents_of = Context.parents_of;
    8.14  val ancestors_of = Context.ancestors_of;
    8.15  
    8.16 -val self_ref = Context.self_ref;
    8.17 +val check_thy = Context.check_thy;
    8.18  val deref = Context.deref;
    8.19  val merge = Context.merge;
    8.20  val merge_refs = Context.merge_refs;
     9.1 --- a/src/Tools/Compute_Oracle/compute.ML	Thu Aug 02 23:18:13 2007 +0200
     9.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Fri Aug 03 16:28:15 2007 +0200
     9.3 @@ -267,7 +267,7 @@
     9.4  
     9.5  	val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
     9.6  
     9.7 -    in Computer (Theory.self_ref thy, encoding, Termtab.keys hyptable, shyptable, prog) end
     9.8 +    in Computer (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog) end
     9.9  
    9.10  (*fun timeit f =
    9.11      let
    10.1 --- a/src/Tools/Compute_Oracle/linker.ML	Thu Aug 02 23:18:13 2007 +0200
    10.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Fri Aug 03 16:28:15 2007 +0200
    10.3 @@ -365,8 +365,9 @@
    10.4  					 end)
    10.5  				     ths (cs, [])
    10.6  	val (_, ths) = add_monos thy monocs ths
    10.7 +  val computer = create_computer machine thy ths
    10.8      in
    10.9 -	PComputer (machine, Theory.self_ref thy, ref (create_computer machine thy ths), ref ths)
   10.10 +	PComputer (machine, Theory.check_thy thy, ref computer, ref ths)
   10.11      end
   10.12  
   10.13  fun add_instances (PComputer (machine, thyref, rcomputer, rths)) cs = 
   10.14 @@ -389,4 +390,4 @@
   10.15  	map (fn ct => Compute.rewrite (!rcomputer) ct) cts
   10.16      end
   10.17  		 							      			    
   10.18 -end
   10.19 \ No newline at end of file
   10.20 +end