Major Section: RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are
used to build rules from formulas. Some example `:`

`corollary`

formulas from which `:type-prescription`

rules might be built are:

Examples: (implies (nth n lst) is of type characterp (and (character-listp lst) provided the two hypotheses can (< n (length lst))) be established by type reasoning (characterp (nth n lst))). (implies (demodulize a lst 'value ans) is (and (atom a) either a nonnegative integer or (true-listp lst) of the same type as ans, provided (member-equal a lst)) the hyps can be established by type (or (and reasoning (integerp (demodulize a lst 'value ans)) (>= (demodulize a lst 'value ans) 0)) (equal (demodulize a lst 'value ans) ans))).To specify the term whose type (see type-set) is described by the rule, provide that term as the value of the

`:typed-term`

field of the rule class
object.

General Form (after preprocessing; see below): (implies hyps (or type-restriction1-on-pat ... type-restrictionk-on-pat (equal pat var1) ... (equal pat varj)))where

`pat`

is the application of some function symbol to some arguments,
each `type-restrictioni-on-pat`

is a term involving `pat`

and containing
no variables outside of the occurrences of `pat`

, and each `vari`

is one
of the variables of `pat`

. Generally speaking, the `type-restriction`

terms ought to be terms that inform us as to the type of `pat`

. Ideally,
they should be ``primitive recognizing expressions'' about `pat`

;
see compound-recognizer. We describe preprocessing at the end of this
topic.If the `:typed-term`

is not provided in the rule class object, it is
computed heuristically by looking for a term in the conclusion whose type is
being restricted. An error is caused if no such term is found.

Roughly speaking, the effect of adding such a rule is to inform the ACL2
typing mechanism that `pat`

has the type described by the conclusion, when
the hypotheses are true. In particular, the type of `pat`

is within the
union of the types described by the several disjuncts. The ``type described
by'' `(equal pat vari)`

is the type of `vari`

.

More operationally, when asked to determine the type of a term that is an
instance of `pat`

, ACL2 will first attempt to establish the hypotheses.
**This is done by type reasoning alone, not rewriting!** However, if some
hypothesis is a call of `force`

, then forcing may occur, which may
ultimately invoke the rewriter; see force and see case-split. So-called
free variables in hypotheses are treated specially; see free-variables.
Provided the hypotheses are established by type reasoning, ACL2 then unions
the types described by the `type-restrictioni-on-pat`

terms together with
the types of those subexpressions of `pat`

identified by the `vari`

. The
final type computed for a term is the intersection of the types implied by
each applicable rule. Type prescription rules may be disabled.

You can limit the recursive establishment of hypotheses of rules; see set-backchain-limit.

Because only type reasoning is used to establish the hypotheses of
`:type-prescription`

rules, some care must be taken with the hypotheses.
Suppose, for example, that the non-recursive function `my-statep`

is
defined as

(defun my-statep (x) (and (true-listp x) (equal (length x) 2)))and suppose

`(my-statep s)`

occurs as a hypothesis of a
`:type-prescription`

rule that is being considered for use in the proof
attempt for a conjecture with the hypothesis `(my-statep s)`

. Since the
hypothesis in the conjecture is rewritten, it will become the conjunction of
`(true-listp s)`

and `(equal (length s) 2)`

. Those two terms will be
assumed to have type `t`

in the context in which the `:type-prescription`

rule is tried. But type reasoning will be unable to deduce that
`(my-statep s)`

has type `t`

in this context. Thus, either `my-statep`

should be disabled (see disable) during the proof attempt or else the
occurrence of `(my-statep s)`

in the `:type-prescription`

rule should be
replaced by the conjunction into which it rewrites.While this example makes it clear how non-recursive predicates can cause
problems, non-recursive functions in general can cause problems. For
example, if `(mitigate x)`

is defined to be `(if (rationalp x) (1- x) x)`

then the hypothesis `(pred (mitigate s))`

in the conjecture will rewrite,
opening `mitigate`

and splitting the conjecture into two subgoals, one in
which `(rationalp s)`

and `(pred (1- x))`

are assumed and the other in
which `(not (rationalp s))`

and `(pred x)`

are assumed. But
`(pred (mitigate s))`

will not be typed as `t`

in either of these
contexts. The moral is: beware of non-recursive functions occuring in the
hypotheses of `:type-prescription`

rules.

Because of the freedom one has in forming the conclusion of a
type-prescription, we have to use heuristics to recover the pattern, `pat`

,
whose type is being specified. In some cases our heuristics may not identify
the intended term and the `:type-prescription`

rule will be rejected as
illegal because the conclusion is not of the correct form. When this happens
you may wish to specify the `pat`

directly. This may be done by using a
suitable rule class token. In particular, when the token
`:type-prescription`

is used it means ACL2 is to compute pat with its
heuristics; otherwise the token should be of the form
`(:type-prescription :typed-term pat)`

, where `pat`

is the term whose
type is being specified.

The defun event may generate a `:type-prescription`

rule. Suppose `fn`

is the name of the function concerned. Then `(:type-prescription fn)`

is
the rune given to the type-prescription, if any, generated for `fn`

by
`defun`

. (The trivial rule, saying `fn`

has unknown type, is not
stored, but `defun`

still allocates the rune and the corollary of this
rune is known to be `t`

.)

We close with a discussion of how, before a term is parsed into a
`:type-prescription`

rule, it is preprocessed. We describe this
preprocessing in some detail below, but first consider the following
(contrived) example.

(defthm append-tp-example (let ((result (append x y))) (implies (nat-listp x) (implies (let ((second-hyp (integer-listp y))) second-hyp) (true-listp result)))) :rule-classes :type-prescription)This theorem is parsed into a type-prescription rule with the following hypotheses and conclusion.

(nat-listp x) ; first hypothesis ((lambda (second-hyp) second-hyp) (integer-listp y)) ; second hypothesis (true-listp (binary-append x y)) ; conclusionNotice that the top-level

`LET`

was expanded, i.e., `(append x y)`

was
substituted for `result`

-- more accurately, `(binary-append x y)`

was
substituted for `result`

, since `append`

is a macro that abbreviates
`binary-append`

. Also notice that the two hypotheses were ``flattened''
in the sense that they were gathered up into a list. Finally, notice that
the `LET`

in the second hypothesis was not expanded (it was merely
translated to internal form, using `LAMBDA`

). If you actually submit the
theorem above, you will get warnings, which you may choose to ignore; the
application of `type-prescription`

rules is somewhat subtle, so if you use
them then you may wish to experiment to see which forms work best for you.Here is the detail promised above, for parsing a term into a
`:type-prescription`

rule. There are two steps. (1) ACL2 first translates
the term, expanding all macros (see trans) and also expanding away calls of
all so-called ``guard holders,'' `mv-list`

and `return-last`

(the
latter resulting for example from calls of `prog2$`

, `mbe`

, or
`ec-call`

), as well as expansions of the macro ``the`

'. (2) Then the
the translated term is traversed top-down, expanding away `lambda`

s
(`let`

, `let*`

, and `mv-let`

expressions) and flattening the
`IMPLIES`

structure, until the conclusion is exposed; then the
conclusion's `lambda`

s are also expanded away. The simplest way to
understand (2) may be to look at the definition of ACL2 source function
`unprettyify-tp`

, which implements Step (2), say by evaluating
`:`

`pe`

` unprettyify-tp`

.