Re: [isabelle] Handling theory errors



On Fri, 27 Feb 2009, Omar Montano Rivas wrote:

> fun activate_defs eqs thry =
>  case eqs of
>     (name,eqns) :: teq => activate_defs teq (simple_function name eqns thry
> handle ERROR e => thry)
>   |     _     => thry;
> 
> val eqs1 = [ at {prop "DEF1 x Cero = Siguiente x"},
> @{prop "DEF1 (x::numero) (Siguiente y) = Siguiente (DEF1 x y)"}];
> 
> val eqs2 = [ at {prop "DEF2 x Cero = Siguiente x"},
> @{prop "DEF2 x y = (DEF2::numero=>numero=>numero) x y"}];
> 
> val eqs3 = [ at {prop "DEF3 x Cero = (x::numero)"},
> @{prop "DEF3 x (Siguiente y) = Siguiente (DEF3 (x::numero) y)"}];
> *}
> 
> 
> (* This generates the Stale theory error *)
> setup{*
> activate_defs [("DEF1",eqs1),("DEF2",eqs2),("DEF3",eqs3)]
> *}

As explained in section 1.1.1 of the Isabelle/Isar Implementation manual, 
theories are essentially a linear type, with run-time checking of 
non-linear updates.  In activate_defs above, the application of 
simple_function can well update thry before raising the ERROR, so thry 
passed in the handler comes out as stale. The Theory.checkpoint operation 
described in the manual is able to amend this. E.g. like this:

fun activate_defs eqs thy0 =
  let val thy = Theory.checkpoint thy0 in
    case eqs of
       (name,eqns) :: teq => activate_defs teq (simple_function name 
         eqns thy handle ERROR e => thy)
     |     _     => thy
  end

Note that the canonical naming convention for theories is "thy...", this 
makes it easier to do static analysis in such error cases, by 
"eye-balling" the sources.

Anyway, handling general ERROR exceptions like above can easily lead into 
obscure situations -- the error could stem from a quite different spot 
than you expect.  Which source of ERROR did you have in mind anyway?


BTW, in the coming release, there will be less situations where stale 
theories can emerge in regular user code.  I will also try harder to get 
regular ML interfaces for the 'function' package in -- then you do not 
have to copy half of the command wrapper implementation.


	Makarius





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