伊莎贝尔战术分析

Question

有没有工具可以分析 Isabelle 的战术？

我基本上有一种形式的战术

REPEAT ( tac1 ORELSE ... ORELSE tacN )

我想弄清楚每种策略的运行时间，以识别 优化的热点。

我可能需要以嵌套方式执行此操作，例如

tac1 = tac12 THEN simp_tac ...

我想知道在简化上花费了多少时间。

Answer 1

不确定这是否是您要查找的内容，但 ML 中有 timeit，您可以将其包装在函数周围。这是一个 Eisbach 包装器：

ML \<open>fun method_evaluate text ctxt facts =
  Method.NO_CONTEXT_TACTIC ctxt
    (Method.evaluate_runtime text ctxt facts)\<close>


method_setup timeit =
 \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
   let
     fun timed_tac st seq = Seq.make (fn () => Option.map (apsnd (timed_tac st))
       (timeit (fn () => (Seq.pull seq))));
     fun tac st' =
       timed_tac st' (method_evaluate m ctxt facts st');
   in SIMPLE_METHOD tac [] end)
\<close>

(https://github.com/seL4/l4v/blob/0f38e20094/lib/Eisbach_Methods.thy#L76)

由于选择的 Eisbach 包装器刚刚出现在另一个问题中，我将看看将其大部分包含在分发中。