# HG changeset patch
# User wenzelm
# Date 1701894492 -3600
# Node ID 3c7ab17380a89aa87f537fc5fae9a633211af40e
# Parent  00962876301c0b4bb6dabfcfd8fe952a70a57ddf
performance tuning: cache for ztyp_of within zterm_of;
clarified signature;

diff -r 00962876301c -r 3c7ab17380a8 src/Pure/zterm.ML
--- 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')