Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Slow top-down contraction of abbreviations

view this post on Zulip Email Gateway (Apr 18 2024 at 15:51):

From: Fabian Immler <cl-isabelle-users@lists.cam.ac.uk>
Hello everyone,

We observed that pretty printing is slow when you have an abbreviation that is deeply nested in a term.
Consider e.g. the abbreviation int == of_nat in iterate_bind, where

iterate_bind n = do {
x ← Some x;
...;
x ← Some x;
Some (int x)
}

For n = 1500 (a term size not uncommon in program verification), pretty printing takes about 60s.
This is due to the fact that abbreviations are contracted top-down
(Proof_Context.standard_term_uncheck->contract_abbrevs->Pattern.rewrite_term_top).
Bottom-up rewriting (Pattern.rewrite_term) takes less than a second (and obviously produces the same result in this case).

Interestingly, contract_abbrevs used to do bottom-up rewriting prior to 5d2fe4e09354.
And while I am sure there must have been a reason for this change, the changeset unfortunately does not give a justification.

Concrete explorations are below, with contract_abbrevs' as a parameterized variant of
contract_abbrevs.

This is certainly a very delicate business, but does anyone have insights if or how this situation
could be improved?

Best wishes,
Fabian

—
Fabian Immler
fimmler@apple.com <mailto:fimmler@apple.com>
 SEG Formal Verification

Scratch.thy:
=========

theory Scratch
imports
Main
(* "HOL-Library.Monad_Syntax" *)
begin

ML ‹
fun iterate_bind 0 = Abs ("x", @{typ "nat"}, @{const Some("int")} $ (@{term int} $ Bound 0))
| iterate_bind i =
Abs ("x", @{typ nat},
@{const Option.bind(nat, int)} $ (@{const Some(nat)} $ Bound 0) $
iterate_bind (i - 1))

(* when including "HOL-Library.Monad_Syntax"
iterate_bind 3 = @{term "λx. do {
x ← Some x;
x ← Some x;
x ← Some x;
Some (int x)
}"}
*)
›

ML ‹
(* Pretty printing such a term with "show_abbrevs" is slow: *)
local
val ctxt = @{context}
val t = iterate_bind 1500
val ct = Thm.cterm_of ctxt t
val _ = timeap_msg "show_abbrevs=true" (Syntax.string_of_term ctxt) t
val ctxt' = Config.put Proof_Context.show_abbrevs false ctxt
val _ = timeap_msg "show_abbrevs=false" (Syntax.string_of_term ctxt') t
in
val t = t
end
›

ML ‹
fun contract_abbrevs' ctxt rewrite_term t =
let
val thy = Proof_Context.theory_of ctxt;
val consts = Proof_Context.consts_of ctxt;
val abbrev = false;
val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
in
if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t
else rewrite_term thy [] [match_abbrev] t
end;
›
ML ‹val t1 = timeap_msg "top-down" (contract_abbrevs' @{context} Pattern.rewrite_term_top) t›
ML ‹val t2 = timeap_msg "bot-up" (contract_abbrevs' @{context} Pattern.rewrite_term ) t›
ML ‹t1 = t2›

end

view this post on Zulip Email Gateway (Feb 03 2025 at 21:17):

From: Makarius <makarius@sketis.net>
There has been more than one reason to slow down pretty-printing of terms.

In Isabelle2025-RC1 this should all be much better, and hopefully without
newly introduced problems.

Now is the time for testing ...

Makarius

On 18/04/2024 16:50, Fabian Immler (via cl-isabelle-users Mailing List) wrote:

Hello everyone,

We observed that pretty printing is slow when you have an abbreviation that is
deeply nested in a term.
Consider e.g. the abbreviation int == of_nat in iterate_bind, where

iterate_bind n = do {
      x ← Some x;
      ...;
      x ← Some x;
      Some (int x)
    }

For n = 1500 (a term size not uncommon in program verification), pretty
printing takes about 60s.
This is due to the fact that abbreviations are contracted top-down
(Proof_Context.standard_term_uncheck->contract_abbrevs->Pattern.rewrite_term_top).
Bottom-up rewriting (Pattern.rewrite_term) takes less than a second (and
obviously produces the same result in this case).

Interestingly, contract_abbrevs used to do bottom-up rewriting prior to
5d2fe4e09354.
And while I am sure there must have been a reason for this change, the
changeset unfortunately does not give a justification.

Concrete explorations are below, with contract_abbrevs' as a parameterized
variant of
contract_abbrevs.

This is certainly a very delicate business, but does anyone have insights if
or how this situation
could be improved?

Best wishes,
Fabian

—
Fabian Immler
fimmler@apple.com <mailto:fimmler@apple.com>
 SEG Formal Verification

Scratch.thy:
=========

theory Scratch
  imports
    Main
(* "HOL-Library.Monad_Syntax" *)
begin

ML ‹
fun iterate_bind 0 = Abs ("x", @{typ "nat"}, @{const Some("int")} $ (@{term
int} $ Bound 0))
  | iterate_bind i =
    Abs ("x", @{typ nat},
      @{const Option.bind(nat, int)} $ (@{const Some(nat)} $ Bound 0) $
      iterate_bind (i - 1))

(* when including "HOL-Library.Monad_Syntax"
iterate_bind 3 =  @{term "λx. do {
    x ← Some x;
    x ← Some x;
    x ← Some x;
    Some (int x)
  }"}
*)
›

ML ‹
(* Pretty printing such a term with "show_abbrevs" is slow: *)
local
val ctxt = @{context}
val t = iterate_bind 1500
val ct = Thm.cterm_of ctxt t
val _ = timeap_msg "show_abbrevs=true"  (Syntax.string_of_term ctxt) t
val ctxt' = Config.put Proof_Context.show_abbrevs false ctxt
val _ = timeap_msg "show_abbrevs=false" (Syntax.string_of_term ctxt') t
in
  val t = t
end
›

ML ‹
fun contract_abbrevs' ctxt rewrite_term t =
  let
    val thy = Proof_Context.theory_of ctxt;
    val consts = Proof_Context.consts_of ctxt;
    val abbrev = false;
    val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
    fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u)
(retrieve u));
  in
    if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can
Term.type_of t) then t
    else rewrite_term thy [] [match_abbrev] t
  end;
›
ML ‹val t1 = timeap_msg "top-down" (contract_abbrevs' @{context}
Pattern.rewrite_term_top) t›
ML ‹val t2 = timeap_msg "bot-up"   (contract_abbrevs' @{context}
Pattern.rewrite_term    ) t›
ML ‹t1 = t2›

end

view this post on Zulip Email Gateway (Feb 06 2025 at 13:47):

From: Fabian Immler <cl-isabelle-users@lists.cam.ac.uk>
Thank you, this looks great from what I can tell.

The pathological example from this thread is much improved (from about 60s to 1s).
Pretty printing the pathological example with "HOL-Library.Monad_Syntax" is also much improved:
iterate_bind 600 took 20s in Isabelle2024, now this is down to 0.2s.

In regular usage over the past weeks (since Isabelle2025-RC0), I did not notice any problems with the speed of pretty printing.

Best wishes,
Fabian

—
Fabian Immler
fimmler@apple.com
 SEG Formal Verification

On 3. Feb 2025, at 22:09, Makarius <makarius@sketis.net> wrote:

There has been more than one reason to slow down pretty-printing of terms.

In Isabelle2025-RC1 this should all be much better, and hopefully without newly introduced problems.

Now is the time for testing ...

Makarius

On 18/04/2024 16:50, Fabian Immler (via cl-isabelle-users Mailing List) wrote:

Hello everyone,
We observed that pretty printing is slow when you have an abbreviation that is deeply nested in a term.
Consider e.g. the abbreviation int == of_nat in iterate_bind, where
iterate_bind n = do {
x ← Some x;
...;
x ← Some x;
Some (int x)
}
For n = 1500 (a term size not uncommon in program verification), pretty printing takes about 60s.
This is due to the fact that abbreviations are contracted top-down
(Proof_Context.standard_term_uncheck->contract_abbrevs->Pattern.rewrite_term_top).
Bottom-up rewriting (Pattern.rewrite_term) takes less than a second (and obviously produces the same result in this case).
Interestingly, contract_abbrevs used to do bottom-up rewriting prior to 5d2fe4e09354.
And while I am sure there must have been a reason for this change, the changeset unfortunately does not give a justification.
Concrete explorations are below, with contract_abbrevs' as a parameterized variant of
contract_abbrevs.
This is certainly a very delicate business, but does anyone have insights if or how this situation
could be improved?
Best wishes,
Fabian
—
Fabian Immler
fimmler@apple.com <mailto:fimmler@apple.com> <mailto:fimmler@apple.com>
 SEG Formal Verification
Scratch.thy:
=========
theory Scratch
imports
Main
(* "HOL-Library.Monad_Syntax" *)
begin
ML ‹
fun iterate_bind 0 = Abs ("x", @{typ "nat"}, @{const Some("int")} $ (@{term int} $ Bound 0))
| iterate_bind i =
Abs ("x", @{typ nat},
@{const Option.bind(nat, int)} $ (@{const Some(nat)} $ Bound 0) $
iterate_bind (i - 1))
(* when including "HOL-Library.Monad_Syntax"
iterate_bind 3 = @{term "λx. do {
x ← Some x;
x ← Some x;
x ← Some x;
Some (int x)
}"}
*)
›
ML ‹
(* Pretty printing such a term with "show_abbrevs" is slow: *)
local
val ctxt = @{context}
val t = iterate_bind 1500
val ct = Thm.cterm_of ctxt t
val _ = timeap_msg "show_abbrevs=true" (Syntax.string_of_term ctxt) t
val ctxt' = Config.put Proof_Context.show_abbrevs false ctxt
val _ = timeap_msg "show_abbrevs=false" (Syntax.string_of_term ctxt') t
in
val t = t
end
›
ML ‹
fun contract_abbrevs' ctxt rewrite_term t =
let
val thy = Proof_Context.theory_of ctxt;
val consts = Proof_Context.consts_of ctxt;
val abbrev = false;
val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
in
if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t
else rewrite_term thy [] [match_abbrev] t
end;
›
ML ‹val t1 = timeap_msg "top-down" (contract_abbrevs' @{context} Pattern.rewrite_term_top) t›
ML ‹val t2 = timeap_msg "bot-up" (contract_abbrevs' @{context} Pattern.rewrite_term ) t›
ML ‹t1 = t2›
end

Last updated: Mar 09 2025 at 12:28 UTC