# HG changeset patch # User wenzelm # Date 1186151302 -7200 # Node ID 90a9a6fe0d0189182b5b4df2d87e6fdc9f9ff241 # Parent 6f6b698b9def746a56711987084960263b959173 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref; thread-safeness: when creating certified items, perform Theory.check_thy *last*; diff -r 6f6b698b9def -r 90a9a6fe0d01 src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Aug 03 16:28:21 2007 +0200 +++ b/src/Pure/thm.ML Fri Aug 03 16:28:22 2007 +0200 @@ -190,10 +190,11 @@ fun typ_of (Ctyp {T, ...}) = T; fun ctyp_of thy raw_T = - let val T = Sign.certify_typ thy raw_T in - Ctyp {thy_ref = Theory.self_ref thy, T = T, - maxidx = Term.maxidx_of_typ T, sorts = may_insert_typ_sorts thy T []} - end; + let + val T = Sign.certify_typ thy raw_T; + val maxidx = Term.maxidx_of_typ T; + val sorts = may_insert_typ_sorts thy T []; + in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end; fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts), maxidx, sorts}) = map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts @@ -235,7 +236,7 @@ let val (t, T, maxidx) = Sign.certify_term thy tm; val sorts = may_insert_term_sorts thy t []; - in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; + in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) = Theory.merge_refs (r1, r2); @@ -331,16 +332,17 @@ (ct1 as Cterm {t = t1, sorts = sorts1, ...}, ct2 as Cterm {t = t2, sorts = sorts2, maxidx = maxidx2, ...}) = let - val thy_ref = merge_thys0 ct1 ct2; - val (Tinsts, tinsts) = match (Theory.deref thy_ref) (t1, t2) (Vartab.empty, Vartab.empty); + val thy = Theory.deref (merge_thys0 ct1 ct2); + val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) = - (Ctyp {T = TVar ((a, i), S), thy_ref = thy_ref, maxidx = i, sorts = sorts}, - Ctyp {T = T, thy_ref = thy_ref, maxidx = maxidx2, sorts = sorts}); + (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts}, + Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}); fun mk_ctinst ((x, i), (T, t)) = let val T = Envir.typ_subst_TVars Tinsts T in - (Cterm {t = Var ((x, i), T), T = T, thy_ref = thy_ref, maxidx = i, sorts = sorts}, - Cterm {t = t, T = T, thy_ref = thy_ref, maxidx = maxidx2, sorts = sorts}) + (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy, + maxidx = i, sorts = sorts}, + Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}) end; in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; @@ -406,7 +408,7 @@ val union_hyps = OrdList.union Term.fast_term_ord; -(* merge theories of cterms/thms; raise exception if incompatible *) +(* merge theories of cterms/thms -- trivial absorption only *) fun merge_thys1 (Cterm {thy_ref = r1, ...}) (th as Thm {thy_ref = r2, ...}) = Theory.merge_refs (r1, r2); @@ -448,12 +450,13 @@ let val Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop} = thm; val thy = Theory.deref thy_ref; + val _ = subthy (thy, thy') orelse raise THM ("transfer: not a super theory", 0, [thm]); + val is_eq = eq_thy (thy, thy'); + val _ = Theory.check_thy thy; in - if not (subthy (thy, thy')) then - raise THM ("transfer: not a super theory", 0, [thm]) - else if eq_thy (thy, thy') then thm + if is_eq then thm else - Thm {thy_ref = Theory.self_ref thy', + Thm {thy_ref = Theory.check_thy thy', der = der, tags = tags, maxidx = maxidx, @@ -506,7 +509,7 @@ val witnessed = map #2 (Sign.witness_sorts thy present extra); in Sorts.subtract witnessed shyps end; in - Thm {thy_ref = thy_ref, der = der, tags = tags, maxidx = maxidx, + Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop} end; @@ -523,14 +526,14 @@ fun get_ax thy = Symtab.lookup (Theory.axiom_table thy) name |> Option.map (fn prop => - Thm {thy_ref = Theory.self_ref thy, - der = Pt.infer_derivs' I (false, Pt.axm_proof name prop), - tags = [], - maxidx = maxidx_of_term prop, - shyps = may_insert_term_sorts thy prop [], - hyps = [], - tpairs = [], - prop = prop}); + let + val der = Pt.infer_derivs' I (false, Pt.axm_proof name prop); + val maxidx = maxidx_of_term prop; + val shyps = may_insert_term_sorts thy prop []; + in + Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], + maxidx = maxidx, shyps = shyps, hyps = [], tpairs = [], prop = prop} + end); in (case get_first get_ax (theory :: Theory.ancestors_of theory) of SOME thm => thm @@ -559,9 +562,13 @@ Pt.get_name hyps prop prf; fun put_name name (Thm {thy_ref, der = (ora, prf), tags, maxidx, shyps, hyps, tpairs = [], prop}) = - Thm {thy_ref = thy_ref, - der = (ora, Pt.thm_proof (Theory.deref thy_ref) name hyps prop prf), - tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop} + let + val thy = Theory.deref thy_ref; + val der = (ora, Pt.thm_proof thy name hyps prop prf); + in + Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx, + shyps = shyps, hyps = hyps, tpairs = [], prop = prop} + end | put_name _ thm = raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]); val get_tags = #tags o rep_thm; @@ -586,15 +593,12 @@ end; fun norm_proof (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = - let val thy = Theory.deref thy_ref in - Thm {thy_ref = thy_ref, - der = Pt.infer_derivs' (Pt.rew_proof thy) der, - tags = tags, - maxidx = maxidx, - shyps = shyps, - hyps = hyps, - tpairs = tpairs, - prop = prop} + let + val thy = Theory.deref thy_ref; + val der = Pt.infer_derivs' (Pt.rew_proof thy) der; + in + Thm {thy_ref = Theory.check_thy thy, der = der, tags = tags, maxidx = maxidx, + shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop} end; fun adjust_maxidx_thm i (th as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) = @@ -964,29 +968,28 @@ (**** Derived rules ****) (*Smash unifies the list of term pairs leaving no flex-flex pairs. - Instantiates the theorem and deletes trivial tpairs. - Resulting sequence may contain multiple elements if the tpairs are - not all flex-flex. *) + Instantiates the theorem and deletes trivial tpairs. Resulting + sequence may contain multiple elements if the tpairs are not all + flex-flex.*) fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) = - Unify.smash_unifiers (Theory.deref thy_ref) tpairs (Envir.empty maxidx) - |> Seq.map (fn env => - if Envir.is_empty env then th - else - let - val tpairs' = tpairs |> map (pairself (Envir.norm_term env)) - (*remove trivial tpairs, of the form t==t*) - |> filter_out (op aconv); - val prop' = Envir.norm_term env prop; - in - Thm {thy_ref = thy_ref, - der = Pt.infer_derivs' (Pt.norm_proof' env) der, - tags = [], - maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'), - shyps = may_insert_env_sorts (Theory.deref thy_ref) env shyps, - hyps = hyps, - tpairs = tpairs', - prop = prop'} - end); + let val thy = Theory.deref thy_ref in + Unify.smash_unifiers thy tpairs (Envir.empty maxidx) + |> Seq.map (fn env => + if Envir.is_empty env then th + else + let + val tpairs' = tpairs |> map (pairself (Envir.norm_term env)) + (*remove trivial tpairs, of the form t==t*) + |> filter_out (op aconv); + val der = Pt.infer_derivs' (Pt.norm_proof' env) der; + val prop' = Envir.norm_term env prop; + val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'); + val shyps = may_insert_env_sorts thy env shyps; + in + Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], maxidx = maxidx, + shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'} + end) + end; (*Generalization of fixed variables @@ -1062,12 +1065,11 @@ let val Ctyp {T, thy_ref = thy_ref1, ...} = cT and Ctyp {T = U, thy_ref = thy_ref2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU; - val thy_ref' = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_ref1, thy_ref2)); - val thy' = Theory.deref thy_ref'; + val thy' = Theory.deref (Theory.merge_refs (thy_ref, Theory.merge_refs (thy_ref1, thy_ref2))); val sorts' = Sorts.union sorts_U sorts; in (case T of TVar (v as (_, S)) => - if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy_ref', sorts')) + if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (Theory.check_thy thy', sorts')) else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], []) | _ => raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: not a type variable", @@ -1135,18 +1137,14 @@ (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) fun class_triv thy c = - let val Cterm {thy_ref, t, maxidx, sorts, ...} = - cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), Sign.certify_class thy c)) - handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); + let + val Cterm {t, maxidx, sorts, ...} = + cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), Sign.certify_class thy c)) + handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); + val der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])); in - Thm {thy_ref = thy_ref, - der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])), - tags = [], - maxidx = maxidx, - shyps = sorts, - hyps = [], - tpairs = [], - prop = t} + Thm {thy_ref = Theory.check_thy thy, der = der, tags = [], maxidx = maxidx, + shyps = sorts, hyps = [], tpairs = [], prop = t} end; (*Internalize sort constraints of type variable*) @@ -1261,7 +1259,7 @@ val thy = Theory.deref thy_ref; val (tpairs, Bs, Bi, C) = dest_state (state, i); fun newth n (env as Envir.Envir {maxidx, ...}, tpairs) = - Thm {thy_ref = thy_ref, + Thm { der = Pt.infer_derivs' ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o Pt.assumption_proof Bs Bi n) der, @@ -1276,7 +1274,8 @@ if Envir.is_empty env then (*avoid wasted normalizations*) Logic.list_implies (Bs, C) else (*normalize the new rule fully*) - Envir.norm_term env (Logic.list_implies (Bs, C))}; + Envir.norm_term env (Logic.list_implies (Bs, C)), + thy_ref = Theory.check_thy thy}; fun addprfs [] _ = Seq.empty | addprfs ((t, u) :: apairs) n = Seq.make (fn () => Seq.pull (Seq.mapp (newth n) @@ -1501,8 +1500,7 @@ tpairs=rtpairs, prop=rprop,...} = orule (*How many hyps to skip over during normalization*) and nlift = Logic.count_prems (strip_all_body Bi) + (if eres_flg then ~1 else 0) - val thy_ref = merge_thys2 state orule; - val thy = Theory.deref thy_ref; + val thy = Theory.deref (merge_thys2 state orule); (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **) fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = let val normt = Envir.norm_term env; @@ -1521,8 +1519,7 @@ (ntps, (map normt (Bs @ As), normt C)) end val th = - Thm{thy_ref = thy_ref, - der = Pt.infer_derivs + Thm{der = Pt.infer_derivs ((if Envir.is_empty env then I else if Envir.above env smax then (fn f => fn der => f (Pt.norm_proof' env der)) @@ -1534,7 +1531,8 @@ shyps = may_insert_env_sorts thy env (Sorts.union rshyps sshyps), hyps = union_hyps rhyps shyps, tpairs = ntpairs, - prop = Logic.list_implies normp} + prop = Logic.list_implies normp, + thy_ref = Theory.check_thy thy} in Seq.cons th thq end handle COMPOSE => thq; val (rAs,B) = Logic.strip_prems(nsubgoal, [], rprop) handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); @@ -1615,24 +1613,20 @@ (case Symtab.lookup (Theory.oracle_table thy1) name of NONE => raise THM ("Unknown oracle: " ^ name, 0, []) | SOME (f, _) => f); - val thy_ref1 = Theory.self_ref thy1; + val thy_ref1 = Theory.check_thy thy1; in fn (thy2, data) => let val thy' = Theory.merge (Theory.deref thy_ref1, thy2); val (prop, T, maxidx) = Sign.certify_term thy' (oracle (thy', data)); + val shyps' = may_insert_term_sorts thy' prop []; + val der = (true, Pt.oracle_proof name prop); in if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else - Thm {thy_ref = Theory.self_ref thy', - der = (true, Pt.oracle_proof name prop), - tags = [], - maxidx = maxidx, - shyps = may_insert_term_sorts thy' prop [], - hyps = [], - tpairs = [], - prop = prop} + Thm {thy_ref = Theory.check_thy thy', der = der, tags = [], + maxidx = maxidx, shyps = shyps', hyps = [], tpairs = [], prop = prop} end end;