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.