--- a/src/Pure/zterm.ML Wed Dec 06 20:57:53 2023 +0100
+++ b/src/Pure/zterm.ML Wed Dec 06 21:28:12 2023 +0100
@@ -157,11 +157,12 @@
val ztyp_ord: ztyp * ztyp -> order
val aconv_zterm: zterm * zterm -> bool
val ztyp_of: typ -> ztyp
+ val zterm_cache_consts: Consts.T -> {zterm: term -> zterm, ztyp: typ -> ztyp}
+ val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
+ val zterm_of: theory -> term -> zterm
val typ_of: ztyp -> typ
- val zterm_of: Consts.T -> term -> zterm
- val term_of: Consts.T -> zterm -> term
- val global_zterm_of: theory -> term -> zterm
- val global_term_of: theory -> zterm -> term
+ val term_of_consts: Consts.T -> zterm -> term
+ val term_of: theory -> zterm -> term
val dummy_proof: 'a -> zproof
val todo_proof: 'a -> zproof
val axiom_proof: theory -> string -> term -> zproof
@@ -322,6 +323,37 @@
| ztyp_of (Type (c, [T])) = if c = "itself" then ZItself (ztyp_of T) else ZType1 (c, ztyp_of T)
| ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);
+fun zterm_cache_consts consts =
+ let
+ val typargs = Consts.typargs consts;
+
+ val ztyp_cache = Unsynchronized.ref Typtab.empty;
+ fun ztyp T =
+ (case Typtab.lookup (! ztyp_cache) T of
+ SOME Z => Z
+ | NONE =>
+ let val Z = ztyp_of T
+ in Unsynchronized.change ztyp_cache (Typtab.update (T, Z)); Z end);
+
+ fun zterm (Free (x, T)) = ZVar ((x, ~1), ztyp T)
+ | zterm (Var (xi, T)) = ZVar (xi, ztyp T)
+ | zterm (Bound i) = ZBound i
+ | zterm (Const (c, T)) =
+ (case typargs (c, T) of
+ [] => ZConst0 c
+ | [T] => ZConst1 (c, ztyp T)
+ | Ts => ZConst (c, map ztyp Ts))
+ | zterm (Abs (a, T, b)) = ZAbs (a, ztyp T, zterm b)
+ | zterm ((t as Const (c, _)) $ (u as Const ("Pure.type", _))) =
+ if String.isSuffix Logic.class_suffix c then
+ ZClass (ztyp (Logic.dest_type u), Logic.class_of_const c)
+ else ZApp (zterm t, zterm u)
+ | zterm (t $ u) = ZApp (zterm t, zterm u);
+ in {ztyp = ztyp, zterm = zterm} end;
+
+val zterm_cache = zterm_cache_consts o Sign.consts_of;
+val zterm_of = #zterm o zterm_cache;
+
fun typ_of (ZTVar ((a, ~1), S)) = TFree (a, S)
| typ_of (ZTVar v) = TVar v
| typ_of (ZFun (T, U)) = typ_of T --> typ_of U
@@ -331,26 +363,7 @@
| typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
| typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
-fun zterm_of consts =
- let
- val typargs = Consts.typargs consts;
- fun zterm (Free (x, T)) = ZVar ((x, ~1), ztyp_of T)
- | zterm (Var (xi, T)) = ZVar (xi, ztyp_of T)
- | zterm (Bound i) = ZBound i
- | zterm (Const (c, T)) =
- (case typargs (c, T) of
- [] => ZConst0 c
- | [T] => ZConst1 (c, ztyp_of T)
- | Ts => ZConst (c, map ztyp_of Ts))
- | zterm (Abs (a, T, b)) = ZAbs (a, ztyp_of T, zterm b)
- | zterm ((t as Const (c, _)) $ (u as Const ("Pure.type", _))) =
- if String.isSuffix Logic.class_suffix c then
- ZClass (ztyp_of (Logic.dest_type u), Logic.class_of_const c)
- else ZApp (zterm t, zterm u)
- | zterm (t $ u) = ZApp (zterm t, zterm u);
- in zterm end;
-
-fun term_of consts =
+fun term_of_consts consts =
let
val instance = Consts.instance consts;
fun const (c, Ts) = Const (c, instance (c, Ts));
@@ -365,8 +378,7 @@
| term (ZClass (T, c)) = Logic.mk_of_class (typ_of T, c);
in term end;
-val global_zterm_of = zterm_of o Sign.consts_of;
-val global_term_of = term_of o Sign.consts_of;
+val term_of = term_of_consts o Sign.consts_of;
@@ -380,7 +392,7 @@
fun const_proof thy a A =
let
- val t = global_zterm_of thy A;
+ val t = zterm_of thy A;
val instT =
ZTVars.build (t |> (fold_types o fold_tvars) (fn v => fn tab =>
if ZTVars.defined tab v then tab else ZTVars.update (v, ZTVar v) tab));
@@ -395,14 +407,14 @@
fun oracle_proof thy name = const_proof thy (ZOracle name);
fun assume_proof thy A =
- ZHyp (global_zterm_of thy A);
+ ZHyp (zterm_of thy A);
fun trivial_proof thy A =
- ZAbsP ("H", global_zterm_of thy A, ZBoundP 0);
+ ZAbsP ("H", zterm_of thy A, ZBoundP 0);
fun implies_intr_proof thy A prf =
let
- val h = global_zterm_of thy A;
+ val h = zterm_of thy A;
fun proof i (ZHyp t) = if aconv_zterm (h, t) then ZBoundP i else raise Same.SAME
| proof i (ZAbst (x, T, p)) = ZAbst (x, T, proof i p)
| proof i (ZAbsP (x, t, p)) = ZAbsP (x, t, proof (i + 1) p)
@@ -415,8 +427,9 @@
fun forall_intr_proof thy T (a, x) prf =
let
- val Z = ztyp_of T;
- val z = global_zterm_of thy x;
+ val {ztyp, zterm} = zterm_cache thy;
+ val Z = ztyp T;
+ val z = zterm x;
fun term i b =
if aconv_zterm (b, z) then ZBound i
@@ -442,7 +455,7 @@
in ZAbst (a, Z, Same.commit (proof 0) prf) end;
-fun forall_elim_proof thy t p = ZAppt (p, global_zterm_of thy t);
+fun forall_elim_proof thy t p = ZAppt (p, zterm_of thy t);
fun of_class_proof (T, c) = ZClassP (ztyp_of T, c);
@@ -471,17 +484,19 @@
fun reflexive_proof thy T t =
let
- val A = ztyp_of T;
- val x = global_zterm_of thy t;
+ val {ztyp, zterm} = zterm_cache thy;
+ val A = ztyp T;
+ val x = zterm t;
in map_const_proof (fn "'a" => A, fn "x" => x) reflexive_axiom end;
fun symmetric_proof thy T t u prf =
if is_reflexive_proof prf then prf
else
let
- val A = ztyp_of T;
- val x = global_zterm_of thy t;
- val y = global_zterm_of thy u;
+ val {ztyp, zterm} = zterm_cache thy;
+ val A = ztyp T;
+ val x = zterm t;
+ val y = zterm u;
val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom;
in ZAppP (ax, prf) end;
@@ -490,33 +505,37 @@
else if is_reflexive_proof prf2 then prf1
else
let
- val A = ztyp_of T;
- val x = global_zterm_of thy t;
- val y = global_zterm_of thy u;
- val z = global_zterm_of thy v;
+ val {ztyp, zterm} = zterm_cache thy;
+ val A = ztyp T;
+ val x = zterm t;
+ val y = zterm u;
+ val z = zterm v;
val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y | "z" => z) transitive_axiom;
in ZAppP (ZAppP (ax, prf1), prf2) end;
fun equal_intr_proof thy t u prf1 prf2 =
let
- val A = global_zterm_of thy t;
- val B = global_zterm_of thy u;
+ val {ztyp, zterm} = zterm_cache thy;
+ val A = zterm t;
+ val B = zterm u;
val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
in ZAppP (ZAppP (ax, prf1), prf2) end;
fun equal_elim_proof thy t u prf1 prf2 =
let
- val A = global_zterm_of thy t;
- val B = global_zterm_of thy u;
+ val {ztyp, zterm} = zterm_cache thy;
+ val A = zterm t;
+ val B = zterm u;
val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
in ZAppP (ZAppP (ax, prf1), prf2) end;
fun abstract_rule_proof thy T U x t u prf =
let
- val A = ztyp_of T;
- val B = ztyp_of U;
- val f = global_zterm_of thy t;
- val g = global_zterm_of thy u;
+ val {ztyp, zterm} = zterm_cache thy;
+ val A = ztyp T;
+ val B = ztyp U;
+ val f = zterm t;
+ val g = zterm u;
val ax =
map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f | "g" => g)
abstract_rule_axiom;
@@ -524,12 +543,13 @@
fun combination_proof thy T U f g t u prf1 prf2 =
let
- val A = ztyp_of T;
- val B = ztyp_of U;
- val f' = global_zterm_of thy f;
- val g' = global_zterm_of thy g;
- val x = global_zterm_of thy t;
- val y = global_zterm_of thy u;
+ val {ztyp, zterm} = zterm_cache thy;
+ val A = ztyp T;
+ val B = ztyp U;
+ val f' = zterm f;
+ val g' = zterm g;
+ val x = zterm t;
+ val y = zterm u;
val ax =
map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f' | "g" => g' | "x" => x | "y" => y)
combination_axiom;
@@ -555,9 +575,9 @@
fun instantiate_proof thy (Ts, ts) prf =
let
- val instT = ZTVars.build (Ts |> fold (fn (v, T) => ZTVars.add (v, ztyp_of T)));
- val inst =
- ZVars.build (ts |> fold (fn ((v, T), t) => ZVars.add ((v, ztyp_of T), global_zterm_of thy t)));
+ val {ztyp, zterm} = zterm_cache thy;
+ val instT = ZTVars.build (Ts |> fold (fn (v, T) => ZTVars.add (v, ztyp T)));
+ val inst = ZVars.build (ts |> fold (fn ((v, T), t) => ZVars.add ((v, ztyp T), zterm t)));
val typ =
if ZTVars.is_empty instT then Same.same
else subst_type_same (Same.function (ZTVars.lookup instT));
@@ -598,9 +618,7 @@
fun rotate_proof thy Bs Bi' params asms m prf =
let
- val ztyp = ztyp_of;
- val zterm = global_zterm_of thy;
-
+ val {ztyp, zterm} = zterm_cache thy;
val i = length asms;
val j = length Bs;
in
@@ -612,7 +630,7 @@
fun permute_prems_proof thy prems' j k prf =
let
- val zterm = global_zterm_of thy;
+ val {ztyp, zterm} = zterm_cache thy;
val n = length prems';
in
mk_ZAbsP (map zterm prems')