Email Gateway (Aug 18 2022 at 13:05): Email Gateway (Aug 18 2022 at 13:05):From: Omar Montano Rivas <O.Montano-Rivas-2@sms.ed.ac.uk>
Hi all!
When modifying a theory, for instance using
"FundefPackage.add_fundef_i", how sould errors be handled? In
particular, catching them and using the original theory results in
stale theory errors?
This is the problematic theory:
(***********)
theory Test
imports Main
begin
datatype numero = Cero | Siguiente numero
ML {*
local
val by_pat_completeness_simp =
Proof.global_terminal_proof
(Method.Basic (K FundefDatatype.pat_completeness, Position.none),
SOME (Method.Source_i (Args.src (("HOL.auto", []),
Position.none))));
val termination_by_lexicographic_order =
FundefPackage.setup_termination_proof NONE
#> Proof.global_terminal_proof
(Method.Basic (LexicographicOrder.lexicographic_order [],
Position.none), NONE);
in
fun simple_function name eqs thy =
let
val group = serial_string ();
val config = FundefCommon.FundefConfig
{sequential = false, default = "%x. arbitrary", domintros =
false, tailrec = false};
in
tracing group;
TheoryTarget.init NONE thy
|> LocalTheory.set_group group
|> FundefPackage.add_fundef_i
[(name, NONE, NoSyn)] (map (fn t => (("", []), t)) eqs) config
[]
|> by_pat_completeness_simp
|> LocalTheory.restore
|> LocalTheory.set_group group
|> termination_by_lexicographic_order
|> ProofContext.theory_of
end;
end;
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 = [@{prop "DEF1 x Cero = Siguiente x"},
@{prop "DEF1 (x::numero) (Siguiente y) = Siguiente (DEF1 x y)"}];
val eqs2 = [@{prop "DEF2 x Cero = Siguiente x"},
@{prop "DEF2 x y = (DEF2::numero=>numero=>numero) x y"}];
val eqs3 = [@{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)]
*}
(* However swapping DEF1 and DEF2 generates no error *)
setup{*
activate_defs [("DEF2",eqs2),("DEF1",eqs1),("DEF3",eqs3)]
*}
(***********)
Thanks in advance!
Regards,
Omar Montano
Email Gateway (Aug 18 2022 at 13:05):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 08:18 UTC