|
|
|---|
|
|
|
|---|
Wrapper to mark a function call with some data for use by the FGL rewriter
(annotate arg x) → *
Annotate is just a two-argument function that returns its second argument. It is intended to be used to temporarily associate the data in its first argument with the subterm in its second argument, such that rewrite rules can treat that subterm differently based on whether it has an annotation and what it contains.
Example: print some info about a call before going on to rewrite it as normal:
(fgl::def-fgl-rewrite print-first-argument-of-my-fn (implies (and (fgl::bind-fn-annotation annot 'my-fn) (not annot)) (equal (my-fn a b) (fgl::fgl-prog2 (fgl::syntax-interp (cw "my-fn first arg: ~x0~%" a)) (fgl::annotate :already-printed (my-fn a b))))))
Normally, a rule that included the unchanged LHS in the RHS would loop. However, the RHS of the rule wraps an annotation around the LHS call, and the hypotheses of this rule check that there is no annotation wrapped around the call, so when trying this rule on the LHS occurrence in the RHS, it will fail instead of looping.
The associated utility bind-fn-annotation binds to a variable the annotation data from the annotation wrapped around the most recent (innermost) call of the given function, or NIL if there was no annotation.
Another utility, bind-nth-fn-annotation, similarly binds the annotation from the nth-innermost call of the function. The following example implements a simple way of tracing the rewriting of a function -- we check that the current call of the function is not yet annotated, so that the rule doesn't loop; then we look for a prior call of the function and get its annotation to find the nesting depth to use for the tracing:
(defun next-printed-annotation-index (old-annot) (case-match old-annot ((':printed n) (if (natp n) (+ 1 n) 0)) (& 0))) (fgl::def-fgl-rewrite trace-my-fn (implies (and (fgl::bind-fn-annotation annot 'my-fn) (not annot) (fgl::bind-nth-fn-annotation old-annot 1 'my-fn) (equal index (next-printed-annotation-index old-annot))) (equal (my-fn a b) (fgl::fgl-prog2 (fgl::syntax-interp (cw "~t0~x0> my-fn ~x1~%" index a)) (let ((res (fgl::annotate `(:printed ,index) (my-fn a b)))) (fgl::fgl-prog2 (fgl::syntax-interp (cw "~t0<~x0 my-fn ~x1~%" index a)) res))))))
Function:
(defun annotate (arg x) (declare (ignore arg)) (declare (xargs :guard t)) (let ((__function__ 'annotate)) (declare (ignorable __function__)) x))