Make a rule for the ACL2 ``type checker''

This documentation topic describes the syntactic form of ``tau-system'' rules; these rules extend ACL2's ``type checker.'' For an introduction to the tau system, see introduction-to-the-tau-system.

There happens to be a *function* named

When in the default (``greedy'') mode (see `set-tau-auto-mode`),
every `defun` and every `rule-classes`)
of every `defthm` stored as a rule *of any* `rewrite` rule might contribute to
the tau database! To add a rule to the tau database without adding any other
kind of rule, tag it with `rule-classes` `rule-classes`

General Forms:Boolean: (booleanp (p v))Eval: (p 'const) or (p *const*)Simple: (implies (p v) (q v))Conjunctive: (implies (and (p1 v) ... (pk v)) (q v)), ; Here k must exceed 1.Signature Form 1: (implies (and (p1 x1) (p2 x2) ...) (q (fn x1 x2 ...)))Signature Form 2: (implies (and (p1 x1) (p2 x2) ...) (q (mv-nth 'n (fn x1 x2 ...))))Bounder Form 1 (or Form 2): (implies (and (tau-intervalp i1) ... (or (equal (tau-interval-dom i1) 'dom1-1) ...) ... (in-tau-intervalp x1 i1) ...) (and (tau-intervalp (bounder-fn i1 ...)) (in-tau-intervalptarget(bounder-fn i1 ...)))) wheretargetis (fn x1 ... y1 ...) inForm 1, and (mv-nth 'n (fn x1 ... y1 ...)) inForm 2Big Switch: (equal (fn . formals) body)MV-NTH Synonym: (equal (nth-alt x y) (mv-nth x y)) or (equal (mv-nth x y) (nth-alt x y))

The symbols `equal`, `eq`, `eql`, and `=`. By
``arithmetic comparison'' we mean `<`, `<=`, `>=`, or `>`. Any of these tau predicates may appear negated.

The notation

(INTEGERP X) (EQUAL V 'MONDAY) (<= I 16) (NOT (EQUAL X 'SUNDAY))

The different rule forms above affect different aspects of the tau system. We discuss each form in more detail below.

The documentation below is written as though the tau system is in auto
mode! To ensure that the only rules added to the tau system are those
explicitly assigned to `set-tau-auto-mode` to select manual mode.

General Form:Boolean: (booleanp (p v))

Here

General Form:Eval: (p 'const) or (p *const*)

Here

Generally, when the tau system must determine whether an enabled tau
predicate is true or false on a constant, it simply evaluates the predicate on
the constant. This can be impossible or very inefficient if

A difficulty, however, is determining that a slow down is due to the
evaluation of tau predicates and not some other reason. The first step is
determining that tau is slowing the proof down. See `time-tracker-tau`
for an explanation of `Time-tracker-tau` gives some ways of determining whether tau predicate
evaluation is involved. (If worse comes to worst, consider the following
hack: In the ACL2 source file

General Form:Simple: (implies (p v) (q v))

Here

(implies (natp x) (integerp x)) (implies (integerp x) (rationalp x)) (implies (integerp x) (not (true-listp x))) (implies (natp x) (not (< x 0))) (implies (symbol-alistp x) (alistp x))

Because the tau system records the transitive closure of the Simple rules,
any time a term is known to satisfy

General Form:Conjunctive: (implies (and (p1 v) ... (pk v)) (q v)), ; Here k must exceed 1.

The

For example, the following Conjunctive rule allows tau to conclude that if
weekday

(implies (and (weekdayp d) (not (eq d 'MON)) (not (eq d 'TUE)) (not (eq d 'WED)) (not (eq d 'THU))) (eq d 'FRI))

The tau database is not closed under conjunctive rules; they are applied dynamically.

General Form:Signature Form 1: (implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp) (q (fn x1 x2 ... xn)))

The

The Signature form actually allows multiple tau predicates to be applied to
each variable, e.g., x1 might be required to be both an

A Signature rule informs tau that the function

An example Signature rule is

(implies (and (integer-listp x) (integer-listp y)) (integer-listp (append x y)))

Of course, a function may have multiple signatures:

(implies (and (symbol-listp x) (symbol-listp y)) (symbol-listp (append x y)))

Here is a Signature rule for the function

(implies (and (symbol-listp x) (integer-listp y)) (symbol-alistp (pairlis$ x y)))

The tau system can consequently check this theorem by composing the last two rules shown and exploiting Simple rule stating that symbol-alists are also alists:

(thm (implies (and (symbol-listp a) (symbol-listp b) (integer-listp y)) (alistp (pairlis$ (append a b) y))))

Since

When a Signature rule has an

(implies (and (natp n) (integer-listp a) (< n (len a))) (integerp (nth n a)))

Note that the last hypothesis is a dependent hypothesis: it is not a tau
predicate but a relationship between `type-set` cannot establish

Note also that if this signature could be phrased in a way that eliminates
the dependency between

(implies (and (natp n) (register-filep a) (< n 16)) (integerp (nth n a)))

In this theorem we require only that

General Form:Signature Form 2: (implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp) (q (mv-nth 'n (fn x1 x2 ... xn))))

This form of signature rule is just like form 1 except that it is useful for functions that return multiple-values and allows us to ``type-check'' their individual outputs.

General Form:Bounder Forms 1 and 2: (implies (and (tau-intervalp i1) ... (or (equal (tau-interval-dom i1) 'dom1-1) ...) ... (in-tau-intervalp x1 i1) ...) (and (tau-intervalp (bounder-fn i1 ...)) (in-tau-intervalptarget(bounder-fn i1 ...))))

where *target* is either *Form 1* or
*Form 2*.

This form is for advanced users only and the schema given above is just a
reminder of the general shape. A ``bounder'' for a given function symbol,

General Form:Big Switch: (equal (fn . formals) body)

In the Big Switch form,

(equal (conditional-type x y) (if (consp x) (consp y) (integerp y)))

The idea is that the tau system can treat calls of

Since equality-to-constants are tau predicates, a more common example of a Big Switch rule is

(equal (dtypep x expr) (case x (STMT (stmt-typep expr)) (EXPR (expr-typep expr)) (MODULE (module-typep expr)) (otherwise nil)))

This is because

Big Switch rules are recognized when a function is defined (if tau is in
automatic mode). They generally do not have to be proved explicitly, though
they might be when mutual recursion is involved. Only the first detected Big
Switch rule about a function

General Form:MV-NTH Synonym: (equal (nth-alt x y) (mv-nth x y)) or (equal (mv-nth x y) (nth-alt x y))

Rules of this form just tell the tau system that the user-defined function
`mv-nth`.
Because ACL2's rewriter gives special handling to

- Introduction-to-the-tau-system
- A decision procedure for runtime types
- Set-tau-auto-mode
- Turn on or off automatic (``greedy'') generation of
:tau-system rules - Bounders
- Intervals, bounder functions, and bounder correctness
- In-tau-intervalp
- Boolean membership in a tau interval
- Make-tau-interval
- Make a tau interval
- Time-tracker-tau
- Messages about expensive use of the tau-system
- Tau-intervalp
- Boolean recognizer for tau intervals
- Tau-status
- Query or set tau system status
- Tau-data
- To see what tau knows about a function symbol
- Tau-interval-lo-rel
- Access the lower bound relation of a tau interval
- Tau-interval-hi-rel
- Access the upper bound relation of a tau interval
- Tau-interval-hi
- Access the upper bound of a tau interval
- Tau-interval-lo
- Access the lower bound of a tau interval
- Tau-interval-dom
- Access the domain of a tau interval
- Tau-database
- To see the tau database as a (very large) object