# 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')