Stream: Mirror: Isabelle Users Mailing List

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

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

Last updated: May 04 2024 at 20:16 UTC