Email Gateway (Aug 19 2022 at 11:18): Email Gateway (Aug 19 2022 at 11:18):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I'm currently working on enhanced tracing capabilities in the
simplifier, and as such implement a capability to set "term
breakpoints". The idea is that the user can specify a term pattern, and
if that pattern occurs in a simplification step, certain actions are
triggered.
To declare a breakpoint, I'd like to have a command (could also be an
attribute, but that is not important at this point) which works in proof
mode and parses a specified term and adds it to an internal data
structure. The usual use case could be something like
have "...."
using [[break_term "?x > 0"]]
The problem is how to parse the term. A naive use of Syntax.read_term
fails because ?x is an unknown schematic variable. On the other hand,
the @{cpat} antiquotation which seems like a good fit handles already
existing schematic variables not quite correctly:
notepad
begin
let ?x = 0
ML_prf{*
@{cpat "?x > ?y"}
(* produces: val it = "?y < ?x": cterm *)
(* instead of: val it = "?y < 0": cterm *)
*}
end
To summarize the constraints: I'd like to have a Proof.context-aware
term parsing, which works correctly for existing schematic and locally
fixed variables. Lars Noschinski also pointed out that care needs to be
taken of these two different kinds of fixed variables:
notepad begin
{ have P sorry } note A = this
{ fix P have P sorry } note B = this
end
Regards
Lars
Email Gateway (Aug 19 2022 at 11:19):From: Lars Noschinski <noschinl@in.tum.de>
These are two separate issues: if we want to use schematic variables
as"holes" in the breakpoint, we need a method, whichv handles both bound
and unbound schematic variables.
If on the other hand we want to use free variables for the holes then
there is this issue which variables are too be generalized.
-- Lars
Email Gateway (Aug 19 2022 at 11:20):From: Makarius <makarius@sketis.net>
The usual way to do the latter is to specify the "eigen context"
excplicitly via some 'for' specification.
The general scheme looks like this:
foobar for x y z
So you augment the local context by additional fixes, read/process foobar
(whatever that is exactly), and export the result into the original
context. Thus there will be certain new schematic variables originating
from eigen-variables x y z. This is similar to Pure quantification
!!x y z. foobar within the language of propositions, but works for
arbitrary things within some Proof.context.
See for example the method "ind_cases" in Isabelle/HOL. (Note that in
Isabelle/jEdit you can hover-click over some proof text that uses it, to
get quickly to the ML definition of it. Or you say 'print_methods' and
hover-click over "ind_cases" in its output.)
Makarius
Last updated: Apr 25 2024 at 12:23 UTC