Gl-set-uninterpreted
Prevent GL from interpreting a function's definition or concretely executing it.
Usage:
;; disallow definition expansion and concrete execution
(gl::gl-set-uninterpreted fnname)
(gl::gl-set-uninterpreted fnname t) ;; same as above
;; disallow definition expansion but allow concrete execution
(gl::gl-set-uninterpreted fnname :concrete-only)
;; disallow concrete execution but allow definition expansion
(gl::gl-set-uninterpreted fnname :no-concrete)
;; remove restrictions
(gl::gl-set-uninterpreted fnname nil)
(gl::gl-unset-uninterpreted fnname) ;; same
prevents GL from opening the definition of fnname and/or concretely executing
it. GL will still apply rewrite rules to a call of fnname. If the
call is not rewritten away, symbolic execution of a fnname call will
simply produce an object (of the :g-apply type) representing a call of
fnname on the given arguments.
gl::gl-unset-uninterpreted undoes the effect of gl::gl-set-uninterpreted.
Note that gl::gl-set-uninterpreted has virtually no effect when
applied to a GL primitive: a function that has its ``symbolic
counterpart'' built into the GL clause processor you're using. (It
actually does do a little — it can prevent the function from being
applied to concrete values before rewrite rules are applied. But that
could change in the future.) But what is a GL primitive? That
depends on the current GL clause processor, and can only be determined
reliably by looking at the definition of the following function
symbol:
(cdr (assoc-eq 'gl::run-gified
(table-alist 'gl::latest-greatest-gl-clause-proc (w state))))
For example, this function symbol is 'gl::glcp-run-gified immediately after
including the community-book "centaur/gl/gl". Now use :pe
on this function symbol. The body of that definition should be of the form
(case fn ...), which matches fn against all the GL primitives for the
current GL clause processor.
