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!**
Of course, if some hypothesis is to be forced, it is so
treated; 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`

.)