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))).To specify the term whose type (see type-set) is described by the rule, provide that term as the value of the(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))).

`:typed-term`

field of the rule class
object.

General Form: (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.
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.

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`

.)