Fgl-trace
Trace an FGL rule.
The fgl-trace macro traces a specified rule (given by its FGL rune) and
allows specifying the condition under which an application of the rule will be
traced and what output will be printed.
Example:
(fgl-trace (:formula logext-to-logapp)
:cond (fgl-object-case n :g-integer)
:on-entry (list 'logext-to-logapp n x)
:on-success (msg "~x0 success: n=~x1 x=~x2 result=~x3" 'logext-to-logapp n x result)
:on-failure (msg "~x0 failure: hyp ~x1 errmsg ~x2" 'logext-to-logapp failed-hyp errmsg)
:restore-rules t
:location state)
See fgl-untrace and fgl-untrace-all to remove traces from rules.
Note that the trace-rewrites flag of the fgl-config object must
be set to T for tracing to work at all. This can be set in either of the
following ways:
;; Table setting overrides default
(table fgl::fgl-config-table :trace-rewrites t)
;; State global overrides table setting
(assign :fgl-trace-rewrites t)
Arguments
The first argument is a rune satisfying fgl-generic-rune-p. The rest of
the arguments are optional keyword/value pairs among the following:
- :cond cond-expr: If provided, limits the tracing of the rule to
applications where cond-expr evaluates to true. The expression may use the standard
trace variables (see below).
- :on-entry entry-expr: If provided, entry-expr is evaluated when
starting an attempt to apply the rule. The expression may use the standard
trace variables. The resulting object should either be nil, in which case
nothing is printed, :default, in which case the default entry message is
printed (same as if the keyword was not provided), or a msg
object, in which case it is printed with the ~@ formatting directive.
- :on-relieve-hyp relieve-expr: If provided, after each successful
relieving of a hypothesis (for a rewrite rule) or after successfully evaluating
the metafunction (for a meta rule), relieve-expr is evaluated and may
cause some output to be printed. (By default no output is printed in this case,
unlike for entry, success, and failure.) The expression may use the standard
trace variables as well as hyp (see below). The resulting object should either
be nil/:default, in which cases nothing is printed, or a msg object, in which case it is printed with the ~@ formatting
directive.
- :on-success success-expr: If provided, success-expr is evaluated
when the rule has been applied successfully. The expression may use the
standard trace variables as well as result and additionally rhs if
the rule is a meta rule (see below). The resulting object should either be
nil, in which case nothing is printed, :default, in which case the
default success message is printed (same as if the keyword was not provided),
or a msg object, in which case it is printed with the ~@
formatting directive.
- :on-failure failure-expr: If provided, failure-expr is evaluated
when the application of the rule has failed. For a rewrite rule, this may be
either because of an unrelieved hypothesis or an error or abort. For a meta
rule, this is due to an error or abort in rewriting the RHS; a failure in
applying the metafunction instead results in the eval-failure
condition (below). The expression may use the standard trace variables as well
as errmsg and hyp and additionally rhs if the rule is a meta
rule (see below). The resulting object should either be nil, in which
case nothing is printed, :default, in which case the default failure
message is printed (same as if the keyword was not provided), or a msg object, in which case it is printed with the ~@ formatting
directive.
- :on-eval-success success-expr: If provided, and if the rule is a meta
rule, success-expr is evaluated when the metafunction has been
successfully executed, before the resulting RHS term is rewritten. The
expression may use the standard trace variables as well as rhs (see
below). The resulting object should either be nil/:default, in which
case nothing is printed, or a msg object, in which case it is
printed with the ~@ formatting directive.
- :on-eval-failure failure-expr: If provided, and if the rule is a meta
rule, failure-expr is evaluated when the metafunction has been
unsuccessfully executed. The expression may use the standard trace variables
as well as errmsg (see below). The resulting object should either be
nil/:default, in which case nothing is printed, or a msg
object, in which case it is printed with the ~@ formatting directive.
- :restore-rules restorep: If provided and restorep is nonnil,
whenever an application of the rule is traced the current trace rules are
backed up at the start and restored at the end of tracing (albeit before
evaluating the success or failure expressions). This is useful if you want a
trace of one rule to cause tracing of another rule; see fgl-advanced-tracing.
Variables usable in tracing expressions
The following variables can be used in all trace expressions; note these
symbols are in the FGL package. Additionally, the variables bound in
bindings may be used directly if they aren't shadowed by one of these
symbols.
- depth: the number of traced rule applications currently in process;
this counts the current rule application, even if it ends up not being
traced (i.e. its cond expression evaluates to nil).
- rune: the name of the traced rule.
- fn, args: the function and arguments (FGL objects) of the
object being rewritten.
- bindings: The substitution under which the rule is being applied. At
any point in applying a rewrite rule, this is the unifying substitution plus
any free variable bindings that have been added. When applying a meta or
primitive rule, the bindings are initially empty. For a meta rule, after
evaluating the metafunction, it is populated with the bindings returned by the
metafunction (for a primitive, it remains empty).
The following variables can be used in some situtations:
- result: The final result of the rule application, i.e. the rewritten
RHS, available in the :on-success case.
- hyp: The index of the relevant hypothesis--in the :on-relieve-hyp
case, this is the index of the latest hypothesis relieved, and in the
:on-failure case this is the index of the failed hypothesis, if any,
otherwise NIL.
- errmsg: The error message ending application of the rule, or NIL if
none, available in :on-failure and :on-eval-failure cases.
- rhs: the computed RHS term returned by a metafunction, available in
the :on-eval-success and metafunctions' :on-success and
:on-failure cases.
Tracing rules during FGL processing
The fgl-trace macro installs an updated set of traced rules in the
:fgl-trace-rule-alist state global variable. When starting a symbolic
execution, the value of that state global is copied into the FGL interpreter
state's trace-alist field. Therefore, running fgl-trace during
symbolic simulation (e.g. during evaluation of a trace expression) won't affect
the rules traced during the current symbolic execution. Instead, you can use
fgl-trace* (with much the same interface) to add a traced rule, fgl-untrace* to untrace a rule, and fgl-untrace-all* to untrace all
rules. Note that if a traced rule has the :restore-rules flag set, then
any modifications to the traced rules will be undone (set back to the state
upon beginning application of the rule) after the rule is finished.
