# Re: [isabelle] Using timeLimit with tactics

On Fri, 2012-05-18 at 17:56 +0200, Ognjen Maric wrote:
> ML_prf {*
> fun loop_tac ctxt i = loop_tac ctxt i
> *}
> apply(tactic {*
> TimeLimit.timeLimit (Time.fromMilliseconds 500) (loop_tac @{context}) 1
> *})
> apply(tactic {*
> TimeLimit.timeLimit (Time.fromMilliseconds 500) loop_tac @{context} 1
> *})
> The difference is the grouping of the arguments in the first example (hence
> changing the type of timeLimit's result)
TimeLimit.timeLimit t f x applies f to x, raising a TimeOut if this
takes longer than t.
loop_tac is a curried function that takes two arguments. With the second
grouping, timeLimit limits the runtime of partially applying loop_tac to
one argument (@{context}). But this partial application (which yields
loop_tac @{context}, a function of one argument) takes (almost) no time
anyway.
Infinite recursion happens once you apply loop_tac @{context} to an
argument (i.e., 1). But with the second grouping, this application is no
longer guarded by timeLimit.
Best regards,
Tjark

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*