Type-prescription-debugging
Improve a built-in type-prescription rule
A type-prescription rule is introduced automatically when a
function is defined (see defun). However, that rule might not be what
you expect. In this topic we explore how you might be able to improve that
rule, by way of an example.
First consider the following definition.
ACL2 !>(defun f (x) (alistp x))
Since F is non-recursive, its admission is trivial. We observe that
the type of F is described by the theorem
(OR (EQUAL (F X) T) (EQUAL (F X) NIL)). We used the :type-prescription
rule ALISTP.
Summary
Form: ( DEFUN F ...)
Rules: ((:TYPE-PRESCRIPTION ALISTP))
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
F
ACL2 !>
Notice in particular the phrase, ``We used the :type-prescription rule
ALISTP,'' and the corresponding rune (:TYPE-PRESCRIPTION ALISTP)
in the list of rules printed in the summary. These are telling us that
ACL2 used the indicated rule during the process of computing a
type-prescription rule for f.
Now suppose that in a different session we instead proceed as follows.
ACL2 !>(in-theory (disable (:type-prescription alistp)))
Summary
Form: ( IN-THEORY (DISABLE ...))
Rules: NIL
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
(:NUMBER-OF-ENABLED-RUNES 3298)
ACL2 !>(defun f (x) (alistp x))
Since F is non-recursive, its admission is trivial. We could deduce
no constraints on the type of F.
Summary
Form: ( DEFUN F ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
F
ACL2 !>
Notice that this time ``We could deduce no constraints on the type of F,''
because in this context, type-set reasoning does not see that the body
of f is a Boolean, because (:type-prescription alistp) has been
disabled. Thus, the ``Rules'' field of the summary is empty this
time.
Consider the following story. On Monday, you run the first session, and a
subsequent proof uses type-set reasoning to conclude that (f x) is
Boolean, even after you disable the definition of f. Then
on Tuesday, you run the second session, and are surprised to find that ACL2 no
longer reasons (during that same subsequent proof attempt) that (f x) is
Boolean. You want to debug this problem, so you look back in the log where
you defined f, and you see the ``deduce no constraints'' message —
but then you look further back, at Monday's log, where you find the definition
of f ``used the :type-prescription rule ALISTP'' to conclude that ``the
type of F is described by the theorem (OR (EQUAL (F X) T) (EQUAL (F X)
NIL))''. The mention of ALISTP in that definition's output from Monday,
together with the corresponding mention of (:TYPE-PRESCRIPTION ALISTP) in
the ``Rules'' field of the summary, leads you to resolve the issue as follows.
On Monday, when (:TYPE-PRESCRIPTION ALISTP) was enabled, ACL2 used
type-set reasoning to conclude that the body of f is Boolean, but on
Tuesday, (:TYPE-PRESCRIPTION ALISTP) was disabled at that point and hence
the body of f was not known to be Boolean by type-set reasoning. Hence
on Tuesday, no Boolean type-prescription rule was stored for f at
definition time, which is why the subsequent proof attempt failed to use such
a rule. So you avoid disabling (:TYPE-PRESCRIPTION ALISTP) until after
submitting the defun for f, and now ACL2's type reasoning knows that f returns a
Boolean.
