[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] gensubst



Erika Rice <erice@cs.washington.edu> wrote:

> Is there a description of the arguments of the "gensubst" substitution
> function available somewhere?
> 
> Thank you, 
> 
>     Erika Rice

Here it is.

Regards,
Sam

gensubst (obj substfn testfn)

gensubst walks down the term obj, applying the testfn function to
each subterm recursively.  If it returns a non-nil value, then the
substfn function is applied.  If it results in a term that is not
eq to the original term, it causes a creation of copies of the
branch leading to the substitution term.  Note that there is no
check for type correctness; the substitution is made blindly.  If
you are simply substituting terms for variables, use substit
instead, as this is faster and guaranteed to be type correct if the
bindings are.  An example using gensubst is expose-binding-types,
which is applied to TCCs so that the types are made visible.

  (defun expose-binding-types (expr)
    (let ((*visible-only* t))
      (gensubst expr #'expose-binding-types! #'expose-binding-types?)))

  (defmethod expose-binding-types? (ex)
    (declare (ignore ex))
    nil)

  (defmethod expose-binding-types? ((ex type-application))
    t)

  (defmethod expose-binding-types? ((ex untyped-bind-decl))
    t)

  (defmethod expose-binding-types! ((ex type-application))
    ex)

  (defmethod expose-binding-types! ((ex untyped-bind-decl))
    (let ((dtype (or (and (type ex) (print-type (type ex)))
		     (declared-type ex)
		     (type ex))))
      (if dtype
	  (change-class (copy ex 'declared-type dtype) 'bind-decl)
	  ex)))


There are two global variables that affect gensubst.
*parsing-or-unparsing* says whether the term has been typechecked,
and *visible-only* will only go down the visible subterms; in
particular, it will only affect declared types (reflected in the
print-type slot), not the expanded canonical form of the type.