; ACL2 Version 2.7 -- A Computational Logic for Applicative Common Lisp
; Copyright (C) 2002 University of Texas at Austin
; *** Fixed version of proof-checker-b.lisp ***
#|
We have discovered, thanks to an example sent in by John Erickson, that ACL2
has had a soundness bug (probably for many years) that can occur when using the
proof-checker. Specifically, the expand command, and hence x and x-dumb
commands (which call expand), are involved; see :DOC PROOF-CHECKER-COMMANDS.
The bug can occur when applying the above commands when the current term is a
call of a constrained function symbol for which there is a :definition rule.
This bug will be fixed when ACL2 Version 2.8 is released, which may not be for
a few months. In the meantime, if you want a fix, you can replace source file
proof-checker-b.lisp with a fixed version, which modifies the
functionality of the above commands. Simply obtain the fixed-proof-checker-b.lisp and
replace proof-checker-b.lisp with that file, and
recompile/rebuild.
WIth this fix, the proof-checker's expand command will succeed
only when the function symbol of the current term is a defined function symbol,
in which case the original definition is always used, in analogy to how the
:expand hint works in the prover; see :DOC HINTS.
Here is an example that exhibits the above bug.
(in-package "ACL2")
(encapsulate
(((foo *) => *)
((bar *) => *))
(local (defun foo (x) x))
(local (defun bar (x) (not x)))
(defthm foo-open
(equal (foo x) x)
:rule-classes :definition)
(defthm bar-not-foo
(equal (bar x) (not (foo x)))
:rule-classes :definition))
(defthm bad (equal (foo x) (bar x))
:rule-classes nil
:instructions
((:dv 1) :expand :nx :expand :top :s))
(defthm contradiction
nil
:rule-classes nil
:hints (("Goal" :use bad)))
|#
; This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright
; (C) 1997 Computational Logic, Inc. See the documentation topic NOTES-2-0.
; This program is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
; Written by: Matt Kaufmann and J Strother Moore
; email: Kaufmann@cs.utexas.edu and Moore@cs.utexas.edu
; Department of Computer Sciences
; University of Texas at Austin
; Austin, TX 78712-1188 U.S.A.
(in-package "ACL2")
(defmacro install-new-pc-meta-or-macro (command-type raw-name name formals doc body)
`(progn ,(pc-meta-or-macro-defun raw-name name formals doc body)
(add-pc-command ,name ',command-type)))
(defun define-pc-meta-or-macro-fn (command-type raw-name formals body)
(let ((name (make-official-pc-command raw-name)) )
(mv-let
(doc body)
(remove-doc
(case command-type
(meta " (meta)")
(macro " (macro)")
(atomic-macro " (atomic macro)")
(otherwise ""))
body)
`(install-new-pc-meta-or-macro ,command-type ,raw-name ,name
,formals ,doc ,body))))
(defmacro define-pc-meta (raw-name formals &rest body)
#-small-acl2-image
":Doc-Section Proof-checker
define a proof-checker meta command~/
Built-in proof-checker meta commands include ~c[undo] and ~c[restore], and
others (~c[lisp], ~c[exit], and ~c[sequence]); ~pl[proof-checker-commands].
The advanced proof-checker user can define these as well. See ACL2
source file ~c[proof-checker-b.lisp] for examples, and contact the ACL2
implementors if those examples do not provide sufficient
documentation.~/~/"
(define-pc-meta-or-macro-fn 'meta raw-name formals body))
(defmacro define-pc-macro (raw-name formals &rest body)
#-small-acl2-image
":Doc-Section Proof-checker
define a proof-checker macro command~/
~bv[]
Example:
(define-pc-macro ib (&optional term)
(value
(if term
`(then (induct ,term) bash)
`(then induct bash))))
~ev[]
The example above captures a common paradigm: one attempts to prove
the current goal by inducting and then simplifying the resulting
goals. (~pl[proof-checker-commands] for documentation of the
command ~c[then], which is itself a pc-macro command, and commands
~c[induct] and ~c[bash].) Rather than issuing ~c[(then induct bash)], or
worse yet issuing ~c[induct] and then issuing ~c[bash] for each resulting
goals, the above definition of ~c[ib] would let you issue ~c[ib] and get the
same effect.~/
~bv[]
General Form:
(define-pc-macro cmd args doc-string dcl ... dcl body)
~ev[]
where ~c[cmd] is the name of the pc-macro than you want to define,
~c[args] is its list of formal parameters. ~c[Args] may include lambda-list
keywords ~c[&optional] and ~c[&rest]; ~pl[macro-args], but note that
here, ~c[args] may not include ~c[&key] or ~c[&whole].
The value of ~c[body] should be an ACL2 ``error triple,'' i.e., have the
form ~c[(mv erp xxx state)] for some ~c[erp] and ~c[xxx]. If ~c[erp] is
~c[nil], then ~c[xxx] is handed off to the proof-checker's instruction
interpreter. Otherwise, evaluation typically halts. We may write
more on the full story later if there is interest in reading it.~/"
(define-pc-meta-or-macro-fn 'macro raw-name formals body))
(defmacro define-pc-atomic-macro (raw-name formals &rest body)
(define-pc-meta-or-macro-fn 'atomic-macro raw-name formals body))
(defmacro toggle-pc-macro (name &optional new-tp)
#-small-acl2-image
":Doc-Section Proof-checker
change an ordinary macro command to an atomic macro, or vice-versa~/
~bv[]
Example:
(toggle-pc-macro pro)
~ev[]
Change ~c[pro] from an atomic macro command to an ordinary one (or
vice-versa, if ~c[pro] happens to be an ordinary macro command)~/
~bv[]
General Form:
(toggle-pc-macro name &optional new-tp)
~ev[]
If name is an
atomic macro command then this turns it into an ordinary one, and
vice-versa. However, if ~c[new-tp] is supplied and not ~c[nil], then it
should be the new type, or else there is no change."
`(toggle-pc-macro-fn ',(make-official-pc-command name) ',new-tp state))
(defmacro define-pc-primitive (raw-name formals &rest body)
;; I want to store the instruction automatically unless it's stored explicitly.
;; What I'll do is store the instruction at the end, unless there's already
;; one stored. So, I'll store NIL as a starting point. To implement this simply,
;; I'll impose the invariant that primitive commands never look at the instruction
;; field of the current state.
;; Note that if I put add-pc-command on the untouchables list, then I prevent
;; the user from defining new primitive commands. That's good, because I have
;; no control over what they do, since state-stack is only modified in the case
;; by the single stepper, and I allow that.
(let ((name (make-official-pc-command raw-name)))
(mv-let
(doc body)
(remove-doc " (primitive)" body)
`(progn
,(pc-primitive-defun-form raw-name name formals doc body)
(add-pc-command ,name 'primitive)))))
(define-pc-primitive comment (&rest x)
#-small-acl2-image
"insert a comment~/
~bv[]
Example:
(comment now begin difficult final goal)~/
General Form:
(comment &rest x)
~ev[]
This instruction makes no change in the state except to insert the
~c[comment] instruction.
Some comments can be used to improve the display of commands; see
documentation for ~c[comm]."
(declare (ignore x))
(mv pc-state state))
(defun non-bounded-nums (nums lower upper)
(declare (xargs :guard (and (rationalp lower)
(rationalp upper)
(true-listp nums))))
(if (consp nums)
(if (and (integerp (car nums))
(<= lower (car nums))
(<= (car nums) upper))
(non-bounded-nums (cdr nums) lower upper)
(cons (car nums)
(non-bounded-nums (cdr nums) lower upper)))
nil))
(defun delete-by-position (lst current-index nums)
(declare (xargs :guard (and (true-listp nums)
(integerp current-index))))
(if (consp lst)
(if (member-equal current-index nums)
(delete-by-position (cdr lst) (1+ current-index) nums)
(cons (car lst)
(delete-by-position (cdr lst) (1+ current-index) nums)))
nil))
(define-pc-primitive drop (&rest nums)
#-small-acl2-image
"drop top-level hypotheses~/
~bv[]
Examples:
(drop 2 3) -- drop the second and third hypotheses
drop -- drop all top-level hypotheses~/
General Forms:
(drop n1 n2 ...) -- Drop the hypotheses with the indicated indices.
drop -- Drop all the top-level hypotheses.
~ev[]
~st[Note:] If there are no top-level hypotheses, then the instruction
~c[drop] will fail. If any of the indices is out of range, i.e. is not
an integer between one and the number of top-level hypotheses
~c[(inclusive)], then ~c[(drop n1 n2 ...)] will fail."
(if nums
(let ((bad-nums (non-bounded-nums nums 1 (length hyps))))
(if bad-nums
(print-no-change2 "The following are not in-range hypothesis numbers: ~&0."
(list (cons #\0 bad-nums)))
(mv (change-pc-state
pc-state
:goals
(cons (change goal (car goals)
:hyps (delete-by-position hyps 1 nums))
(cdr goals)))
state)))
(if hyps
(mv (change-pc-state
pc-state
:goals
(cons (change goal (car goals)
:hyps nil)
(cdr goals)))
state)
(print-no-change2 "There are no hypotheses to drop!"))))
(define-pc-meta lisp (form)
;; **** Consider providing a version that expects the form to
;; be translated, together with a macro that does the translation.
;; ***** Also consider eliminating this in favor of a macro command
;; that calls SEQUENCE.
#-small-acl2-image
"evaluate the given form in Lisp~/
~bv[]
Example:
(lisp (assign xxx 3))~/
General Form:
(lisp form)
~ev[]
Evaluate ~c[form]. The ~c[lisp] command is mainly of interest for side
effects. See also ~c[print], ~c[skip], and ~c[fail].
The rest of the documentation for ~c[lisp] is of interest only to
those who use it in macro commands. If the Lisp evaluation (by
~c[trans-eval]) of form returns an ``error triple'' of the form
~c[(mv erp ((NIL NIL STATE) . (erp-1 val-1 &)) state)], then the
~c[lisp] command returns the appropriate error triple
~bv[]
(mv (or erp erp-1)
val-1
state) .
~ev[]
Otherwise, the ~c[trans-eval] of form must return an ``error triple''
of the form ~c[(mv erp (cons stobjs-out val) &)], and the ~c[lisp]
command returns the appropriate error triple
~bv[]
(mv erp
val
state).
~ev[]
Note that the output signature of the form has been lost. The user
must know the signature in order to use the output of the ~c[lisp]
command. Trans-eval, which is undocumented except by comments in
the ACL2 source code, has replaced, in ~c[val], any occurrence of
the current state or the current values of stobjs by simple symbols
such as ~c[REPLACED-STATE]. The actual values of these objects may
be recovered, in principle, from the ~c[state] returned and the
~c[user-stobj-alist] within that state. However, in practice, the
stobjs cannot be recovered because the user is denied access to
~c[user-stobj-alist]. The moral is: do not try to write macro
commands that manipulate stobjs. Should the returned ~c[val]
contain ~c[REPLACED-STATE] the value may simply be ignored and
~c[state] used, since that is what ~c[REPLACED-STATE] denotes."
(if (not (f-get-global 'in-verify-flg state))
(er soft 'acl2-pc::lisp
"You may not invoke the LISP command unless inside the ~
interactive loop.")
(if (and (symbolp form)
(or (eq form t)
(eq form nil)
(keywordp form)))
(value form)
(mv-let (erp stobjs-out vals state)
(my-trans-eval form :lisp state)
(if (equal stobjs-out '(nil nil state))
(mv (or erp (car vals)) (cadr vals) state)
(mv erp vals state))))))
(define-pc-macro fail (&optional hard)
#-small-acl2-image
"cause a failure~/
~bv[]
Examples:
fail
(fail t)~/
General Form:
(fail &optional hard)
~ev[]
This is probably only of interest to writers of macro commands.
The only function of ~c[fail] is to fail to ``succeed''.
The full story is that ~c[fail] and ~c[(fail nil)] simply return
~c[(mv nil nil state)], while ~c[(fail hard)] returns ~c[(mv hard nil state)] if
~c[hard] is not ~c[nil]. See also ~c[do-strict], ~c[do-all], and ~c[sequence]."
(if hard
(value '(lisp (mv hard nil state)))
(value '(lisp nil))))
(define-pc-macro illegal (instr)
#-small-acl2-image
"illegal instruction~/
~bv[]
Example:
(illegal -3)~/
General Form:
(illegal instruction)
~ev[]
Probably not of interest to most users; always ``fails'' since it
expands to the ~c[fail] command.
The ~c[illegal] command is used mainly in the implementation. For
example, the instruction ~c[0] is ``read'' as ~c[(illegal 0)], since ~c[dive]
expects positive integers.~/"
(pprogn (print-no-change "Illegal interactive instruction, ~x0.~% An instruction must be a ~
symbol or a proper list headed by a symbol."
(list (cons #\0 instr)))
(value :fail)))
(defun chk-assumption-free-ttree-1 (ttree ctx)
;; Same as chk-assumption-free-ttree, but returns a value.
(cond ((tagged-object 'assumption ttree)
(er hard ctx
"The 'assumption ~x0 was found in the final ttree!"
(tagged-object 'assumption ttree)))
((tagged-object 'fc-derivation ttree)
(er hard ctx
"The 'fc-derivation ~x0 was found in the final ttree!"
(tagged-object 'fc-derivation ttree)))
(t t)))
(defun put-cdr-assoc-query-id (id val alist)
(cond ((atom alist) (cons (cons id val) alist))
((eq id (caar alist)) (cons (cons id val) (cdr alist)))
(t (cons (car alist)
(put-cdr-assoc-query-id id val (cdr alist))))))
(defun set-query-val (id val state)
;; If val is 'toggle, then a NIL default is changed to T and every
;; other default is changed to NIL. Otherwise, VAL is the new default.
(let ((alist (ld-query-control-alist state)))
(set-ld-query-control-alist
(put-cdr-assoc-query-id
id
(if (eq val 'toggle)
(not (cdr-assoc-query-id id alist))
val)
alist)
state)))
(defmacro query-on-exit (&optional (val 'toggle))
`(set-query-val 'acl2-pc::exit ',val state))
(defun replay-query (state)
;; Returns a state-stack, T or NIL. A T value means we should replay instructions
;; in order to create the state-stack. A value of NIL means that we should exit
;; without creating the event (by making the state-stack nil).
;; In fact, the only time we return other than the current
;; state-stack is if we're inside verify and
;; either the query flag is off or the response is other than "Y".
(acl2-query 'acl2-pc::exit
'("~%Do you want to submit this event? Possible replies are:~%~
Y (Yes), R (yes and Replay commands), N (No, but exit), A (Abort exiting).~|~ "
:y :y :r :r :n :n :a :a)
nil state))
(define-pc-meta exit (&optional event-name rule-classes do-it-flg)
#-small-acl2-image
"exit the interactive proof-checker~/
~bv[]
Examples:
exit -- exit the interactive proof-checker
(exit append-associativity) -- exit and create a defthm
event named append-associativity~/
General Forms:
exit -- Exit without storing an event.
(exit event-name &optional rule-classes do-it-flg)
Exit, and store an event.
~ev[]
The command ~c[exit] returns you to the ACL2 loop. At a later time,
~c[(verify)] may be executed to get back into the same proof-checker
state, as long as there hasn't been an intervening use of the
proof-checker (otherwise see ~c[save]).
When given one or more arguments as shown above, ~c[exit] still returns
you to the ACL2 loop, but first, if the interactive proof is
complete, then it attempts create a ~c[defthm] event with the specified
~c[event-name] and ~c[rule-classes] (which defaults to ~c[(:rewrite)] if not
supplied). The event will be printed to the terminal, and then
normally the user will be queried whether an event should really be
created. However, if the final optional argument ~c[do-it-flg] is
supplied and not ~c[nil], then an event will be made without a query.
For example, the form
~bv[]
(exit top-pop-elim (:elim :rewrite) t)
~ev[]
causes a ~c[defthm] event named ~c[top-pop-elim] to be created with
rule-classes ~c[(:elim :rewrite)], without a query to the user (because
of the argument ~c[t]).
~st[Note:] it is permitted for ~c[event-name] to be ~c[nil]. In that case, the
name of the event will be the name supplied during the original call
of ~c[verify]. (See the documentation for ~c[verify] and ~c[commands].) Also
in that case, if ~c[rule-classes] is not supplied then it defaults to
the rule-classes supplied in the original call of ~c[verify].
~c[Comments] on ``success'' and ``failure''. An ~c[exit] instruction will
always ``fail'', so for example, if it appears as an argument of a
~c[do-strict] instruction then none of the later (instruction) arguments
will be executed. Moreover, the ``failure'' will be ``hard'' if an
event is successfully created or if the instruction is simply ~c[exit];
otherwise it will be ``soft''. See the documentation for ~c[sequence]
for an explanation of hard and soft ``failures''. An obscure but
potentially important fact is that if the ``failure'' is hard, then
the error signal is a special signal that the top-level interactive
loop can interpret as a request to exit. Thus for example, a
sequencing command that turns an error triple ~c[(mv erp val state)]
into ~c[(mv t val state)] would never cause an exit from the interactive
loop.
If the proof is not complete, then ~c[(exit event-name ...)] will not
cause an exit from the interactive loop. However, in that case it
will print out the original user-supplied goal (the one that was
supplied with the call to ~c[verify]) and the current list of
instructions."
;; I allow (exit .. nil ..) to indicate that information is to be picked up from the
;; initial pc-state.
(if (not (f-get-global 'in-verify-flg state))
(er soft 'acl2-pc::exit
"You may not invoke the EXIT command unless inside the ~
interactive loop.")
(if args
;; so it's not just a command to exit
(let* ((event-name-and-types-and-raw-term
(event-name-and-types-and-raw-term state-stack))
(event-name
(or event-name
(car event-name-and-types-and-raw-term)))
(instructions (instructions-of-state-stack state-stack nil)))
(er-let*
((event-name
(if event-name
(value event-name)
(pprogn (io? proof-checker nil state
(fms0 "Please supply an event name (or :A to abort)~%>> "))
(state-global-let*
((infixp nil))
(read-object *standard-oi* state))))))
(if (eq event-name :a)
(pprogn (io? proof-checker nil state
(fms0 "~|Exit aborted.~%"))
(mv nil nil state))
(if (null (goals t))
(let* ((rule-classes (if (consp (cdr args))
rule-classes
(if (and (consp args)
(eq (car args) nil))
(cadr event-name-and-types-and-raw-term)
'(:rewrite))))
(event-form `(defthm ,event-name
,(caddr event-name-and-types-and-raw-term)
,@(if (equal rule-classes '(:rewrite))
nil
(list :rule-classes rule-classes))
:instructions ,instructions)))
(mv-let (erp stobjs-out vals state)
(pprogn
(print-defthm event-form state)
(mv-let (erp ans state)
(if do-it-flg
(value :y)
(replay-query state))
(declare (ignore erp))
(case ans
(:y (my-trans-eval event-form
'acl2-pc::exit
state))
(:r (pprogn (state-from-instructions
(caddr event-form)
event-name
rule-classes
instructions
'(signal value)
state)
(my-trans-eval event-form
'acl2-pc::exit
state)))
(:a (mv t nil t state))
(otherwise (mv t nil nil state)))))
;; I assume here that if DEFTHM returns
;; without error, then it succeeds.
;; (f-put-global 'load-mode saved-mode state)
(if (or erp (null stobjs-out))
(if (eq vals t)
(pprogn (io? proof-checker nil state
(fms0 "~|Exit aborted.~%"))
(mv nil nil state))
(mv *pc-complete-signal* nil state))
(mv *pc-complete-signal* event-name state))))
;; otherwise, we have an incomplete proof
(pprogn (io? proof-checker nil state
(fms0 "~%Not exiting, as there remain unproved goals: ~
~&0.~%The original goal is:~%~ ~ ~ ~ ~y1~| Here is the ~
current instruction list, starting ~
with the first:~%~ ~ ~ ~ ~y2~|"
(list (cons #\0 (goal-names
(goals t)))
(cons #\1 (caddr event-name-and-types-and-raw-term))
(cons #\2 instructions))))
(mv nil nil state))))))
(pprogn (io? proof-checker nil state
(fms0 "~|Exiting....~%"))
(mv *pc-complete-signal* nil state)))))
(define-pc-meta undo (&optional n)
#-small-acl2-image
"undo some instructions~/
~bv[]
Examples:
(undo 7)
undo~/
General Forms:
(undo n) -- Undo the last n instructions. The argument n should be
a positive integer.
undo -- Same as (undo 1).
~ev[]
~st[Note:] To remove the effect of an ~c[undo] command, use ~c[restore]. See
the documentation for details.
~st[Note:] If the argument ~c[n] is greater than the total number of
interactive instructions in the current session, then ~c[(undo n)] will
simply take you back to the start of the session.
The ~c[undo] meta command always ``succeeds''; it returns
~c[(mv nil t state)] unless its optional argument is supplied and of
the wrong type (i.e. not a positive integer) or there are no
instructions to undo."
(if (and args
(not (and (integerp n)
(< 0 n))))
(pprogn (print-no-change "The optional argument to undo must be a positive integer.")
(mv nil nil state))
(let ((m (min (or n 1) (1- (length state-stack)))))
(if (null (cdr state-stack))
(pprogn (print-no-change "Already at the start.")
(mv nil nil state))
(pprogn (pc-assign old-ss state-stack)
(io? proof-checker nil state
(fms0 "~|Undoing: ~y0~|"
(list (cons #\0
(access pc-state
(car (nthcdr (1- m) state-stack))
:instruction)))))
(pc-assign state-stack
(nthcdr m state-stack))
(if (consp (cdr (state-stack)))
state
(io? proof-checker nil state
(fms0 "Back to the start.~%")))
(mv nil t state))))))
(define-pc-meta restore ()
#-small-acl2-image
"remove the effect of an UNDO command~/
~bv[]
Example and General Form:
restore
~ev[]~/
~c[Restore] removes the effect of an ~c[undo] command. This always works as
expected if ~c[restore] is invoked immediately after ~c[undo], without
intervening instructions. However, other commands may also interact
with ~c[restore], notably ``sequencing'' commands such as ~c[do-all],
~c[do-strict], ~c[protect], and more generally, ~c[sequence].
~st[Note:] Another way to control the saving of proof-checker state is
with the ~c[save] command; see the documentation for ~c[save].
The ~c[restore] command always ``succeeds''; it returns
~c[(mv nil t state)]."
(let ((old-ss (pc-value old-ss)))
(if (null old-ss)
(pprogn (io? proof-checker nil state
(fms0 "~%Nothing to restore from!~%"))
(mv nil nil state))
(let ((saved-ss state-stack))
(pprogn (pc-assign state-stack old-ss)
(pc-assign old-ss saved-ss)
(mv nil t state))))))
(defun print-commands (indexed-instrs state)
(if (null indexed-instrs)
state
(if (null (caar indexed-instrs))
(io? proof-checker nil state
(fms0 (car (cdar indexed-instrs))
(cdr (cdar indexed-instrs))))
(pprogn (io? proof-checker nil state
(fms0 "~|~x0. ~y1~|"
(list (cons #\0 (caar indexed-instrs))
(cons #\1 (cdar indexed-instrs)))))
(print-commands (cdr indexed-instrs) state)))))
(defun make-pretty-start-instr (state-stack)
(let* ((triple (event-name-and-types-and-raw-term state-stack))
(name (car triple))
(types (cadr triple)))
(if name
(list "~|[started with (~x0 ~x1 ...)]~%"
(cons #\0 name)
(cons #\1 types))
(list "~|<< no event name specified at start >>~%"))))
(defun raw-indexed-instrs (start-index finish-index state-stack)
(declare (xargs :guard (and (integerp start-index)
(integerp finish-index)
(<= start-index finish-index)
(true-listp state-stack)
;; It's tempting to add the following guard, but
;; since state-stack keeps shrinking, it can get violated
;; on recursive calls.
;; (<= finish-index (length state-stack))
)))
(if (< start-index finish-index)
(cons (cons start-index (access pc-state (car state-stack) :instruction))
(raw-indexed-instrs (1+ start-index) finish-index (cdr state-stack)))
(if (cdr state-stack)
(list (cons start-index (access pc-state (car state-stack) :instruction)))
(list (cons nil (make-pretty-start-instr state-stack))))))
(define-pc-macro sequence-no-restore (instr-list)
(value `(sequence ,instr-list nil nil nil nil t)))
(define-pc-macro skip ()
#-small-acl2-image
"``succeed'' without doing anything~/
~bv[]
Example and General Form:
skip
~ev[]~/
Make no change in the state-stack, but ``succeed''. Same as
~c[(sequence nil)]."
(value '(sequence-no-restore nil)))
(defmacro define-pc-help (name args &rest body)
#-small-acl2-image
":Doc-Section Proof-checker
define a macro command whose purpose is to print something~/
~bv[]
Example:
(define-pc-help pp ()
(if (goals t)
(io? proof-checker nil state
(fms0 \"~~|~~y0~~|\"
(list (cons #\0
(fetch-term (conc t)
(current-addr t))))))
(print-all-goals-proved-message state)))~/
General Form:
(define-pc-help name args &rest body)
~ev[]
This defines a macro command named ~c[name], as explained further below.
The ~c[body] should (after removing optional declarations) be a form
that returns ~c[state] as its single value. Typically, it will just
print something.
What ~c[(define-pc-help name args &rest body)] really does is to create
a call of ~c[define-pc-macro] that defines ~c[name] to take arguments ~c[args],
to have the declarations indicated by all but the last form in ~c[body],
and to have a body that (via ~c[pprogn]) first executes the form in the
last element of body and then returns a call to the command ~c[skip]
(which will return ~c[(mv nil t state)])."
`(define-pc-macro ,name ,args ,@(butlast body 1)
(pprogn ,(car (last body))
(value 'skip))))
(defun evisc-indexed-instrs-1 (name rev-indexed-instrs)
(if (consp rev-indexed-instrs)
(let ((instr (cdr (car rev-indexed-instrs))))
(case-match instr
((comm ':end x . &)
(if (and (eq comm (make-pretty-pc-command :comment))
(equal x name))
rev-indexed-instrs
(evisc-indexed-instrs-1 name (cdr rev-indexed-instrs))))
(& (evisc-indexed-instrs-1 name (cdr rev-indexed-instrs)))))
nil))
(defun evisc-indexed-instrs-rec (rev-indexed-instrs)
(if (consp rev-indexed-instrs)
(let ((instr (cdr (car rev-indexed-instrs)))
(evisc-cdr (evisc-indexed-instrs-rec (cdr rev-indexed-instrs))))
(case-match instr
((comm ':begin name . &)
(if (eq comm (make-pretty-pc-command :comment))
(let ((rst (evisc-indexed-instrs-1 name evisc-cdr)))
(if rst
(cons (cons (car (car rev-indexed-instrs))
(cons "***HIDING***" instr))
(cdr rst))
(cons (car rev-indexed-instrs)
evisc-cdr)))
(cons (car rev-indexed-instrs)
evisc-cdr)))
(& (cons (car rev-indexed-instrs)
evisc-cdr))))
nil))
(defun mark-unfinished-instrs (indexed-instrs)
;; any "begin" in here was not matched with an "end"
(if (consp indexed-instrs)
(let ((instr (cdr (car indexed-instrs))))
(case-match instr
((comm ':begin & . &)
(if (eq comm (make-pretty-pc-command :comment))
(cons (cons (car (car indexed-instrs))
(cons "***UNFINISHED***" instr))
(mark-unfinished-instrs (cdr indexed-instrs)))
(cons (car indexed-instrs)
(mark-unfinished-instrs (cdr indexed-instrs)))))
(& (cons (car indexed-instrs)
(mark-unfinished-instrs (cdr indexed-instrs))))))
nil))
(defun evisc-indexed-instrs (indexed-instrs)
;; for now, returns a new state stack in which we drop bookends
;; (comment (begin ) ...)
;; (comment (end ) ...)
(mark-unfinished-instrs (reverse (evisc-indexed-instrs-rec (reverse indexed-instrs)))))
(define-pc-help commands (&optional n evisc-p)
#-small-acl2-image
"display instructions from the current interactive session~/
~bv[]
Examples:
commands
(commands 10 t)~/
General Forms:
commands or (commands nil)
Print out all the instructions (in the current state-stack) in
reverse order, i.e. from the most recent instruction to the starting
instruction.
(commands n) [n a positive integer]
Print out the most recent n instructions (in the current
state-stack), in reverse order.
(commands x abbreviate-flag)
Same as above, but if abbreviate-flag is non-NIL, then do not
display commands between ``matching bookends''. See documentation
for comm for an explanation of matching bookends.
~ev[]
~st[Note]: If there are more than ~c[n] instructions in the state-stack,
then ~c[(commands n)] is the same as ~c[commands] (and also,
~c[(commands n abb)] is the same as ~c[(commands nil abb)])."
(if (and n (not (and (integerp n) (> n 0))))
(io? proof-checker nil state
(fms0 "*** The first optional argument to the COMMANDS command must be a positive integer, ~
but ~x0 is not.~|"
(list (cons #\0 n))))
(let* ((indexed-instrs (raw-indexed-instrs 1
(if n
(min n (length state-stack))
(length state-stack))
state-stack)))
(print-commands (if evisc-p (evisc-indexed-instrs indexed-instrs) indexed-instrs)
state))))
(define-pc-macro comm (&optional n)
#-small-acl2-image
"display instructions from the current interactive session~/
~bv[]
Examples:
comm
(comm 10)~/
General Form:
(comm &optional n)
~ev[]
Prints out instructions in reverse order. This is actually the same
as ~c[(commands n t)] ~-[] or, ~c[(commands nil t)] if ~c[n] is not supplied. As
explained in the documentation for ~c[commands], the final argument of ~c[t]
causes suppression of instructions occurring between so-called
``matching bookends,'' which we now explain.
A ``begin bookend'' is an instruction of the form
~bv[]
(COMMENT :BEGIN x . y).
~ev[]
Similarly, an ``end bookend'' is an instruction of the form
~bv[]
(COMMENT :END x' . y').
~ev[]
The ``name'' of the first bookend is ~c[x] and the ``name'' of the
second bookend is ~c[x']. When such a pair of instructions occurs in
the current state-stack, we call them ``matching bookends'' provided
that they have the same name (i.e. ~c[x] equals ~c[x']) and if no other
begin or end bookend with name ~c[x] occurs between them. The idea now
is that ~c[comm] hides matching bookends together with the instructions
they enclose. Here is a more precise explanation of this
``hiding''; probably there is no value in reading on!
A ~c[comm] instruction hides bookends in the following manner. (So does
a ~c[comment] instruction when its second optional argument is supplied
and non-~c[nil].) First, if the first argument ~c[n] is supplied and not
~c[nil], then we consider only the last ~c[n] instructions from the
state-stack; otherwise, we consider them all. Now the resulting
list of instructions is replaced by the result of applying the
following process to each pair of matching bookends: the pair is
removed, together with everything in between the begin and end
bookend of the pair, and all this is replaced by the ``instruction''
~bv[]
(\"***HIDING***\" :COMMENT :BEGIN name ...)
~ev[]
where ~c[(comment begin name ...)] is the begin bookend of the pair.
Finally, after applying this process to each pair of matching
bookends, each begin bookend of the form ~c[(comment begin name ...)]
that remains is replaced by
~bv[]
(\"***UNFINISHED***\" :COMMENT :BEGIN name ...) .
~ev[]"
(value (list 'commands n t)))
(defun conjuncts-of (x)
(declare (xargs :guard (pseudo-termp x)))
(if (and (nvariablep x)
(not (fquotep x))
(eq (ffn-symb x) 'if))
(cond
((equal (fargn x 3) *nil*)
(append (conjuncts-of (fargn x 1))
(conjuncts-of (fargn x 2))))
((equal (fargn x 2) *nil*) ; (if a nil c) <=> (and (not a) c)
(append (conjuncts-of (dumb-negate-lit (fargn x 1)))
(conjuncts-of (fargn x 3))))
(t (list x)))
(list x)))
(defun promote-guts (pc-state goals hyps x y no-flatten-flg)
(change-pc-state
pc-state
:goals
(cons (change goal (car goals)
:hyps (append hyps
(if no-flatten-flg
(list x)
(conjuncts-of x)))
:conc y)
(cdr goals))))
(define-pc-primitive promote (&optional do-not-flatten-flag)
#-small-acl2-image
"move antecedents of conclusion's ~c[implies] term to top-level
hypotheses~/
~bv[]
Examples:
promote
(promote t)
~ev[]
For example, if the conclusion is ~c[(implies (and x y) z)], then
after execution of ~c[promote], the conclusion will be ~c[z] and the terms ~c[x]
and ~c[y] will be new top-level hypotheses.~/
~bv[]
General Form:
(promote &optional do-not-flatten-flag)
~ev[]
Replace conclusion of ~c[(implies hyps exp)] or ~c[(if hyps exp t)] with
simply ~c[exp], adding ~c[hyps] to the list of top-level hypotheses.
Moreover, if ~c[hyps] is viewed as a conjunction then each conjunct will
be added as a separate top-level hypothesis. An exception is that
if ~c[do-not-flatten-flag] is supplied and not ~c[nil], then only one
top-level hypothesis will be added, namely ~c[hyps].
~st[Note]: You must be at the top of the conclusion in order to use this
command. Otherwise, first invoke ~c[top]."
(if current-addr
(print-no-change2 "You must be at the top ~
of the goal in order to promote the ~
antecedents of an implication. Try TOP first.")
(case-match conc
(('implies x y)
(mv (promote-guts pc-state goals hyps x y do-not-flatten-flag) state))
(('if x y *t*)
(mv (promote-guts pc-state goals hyps x y do-not-flatten-flag) state))
(& (print-no-change2 "The goal must be of the form ~x0 or ~x1."
(list (cons #\0 '(IMPLIES P Q))
(cons #\1 '(IF P Q T))))))))
(defun remove-by-indices (m indices lst)
;; (declare (xargs :guard (null (non-bounded-nums indices m (length lst)))))
;; this was ok for the original entry, but it's not preserved
(if (consp lst)
(if (member-equal m indices)
(remove-by-indices (1+ m) indices (cdr lst))
(cons (car lst) (remove-by-indices (1+ m) indices (cdr lst))))
nil))
;;; **** Should improve the following so that if form outputs a state or
;;; does return just one result, then fms0 isn't even called but instead
;;; an appropriate error message is printed.
(define-pc-macro print (form)
#-small-acl2-image
"print the result of evaluating the given form~/
~bv[]
Example:
(print (append '(a b) '(c d)))
Print the list (a b c d) to the terminal~/
General Form:
(print form)
~ev[]
Prettyprints the result of evaluating form. The evaluation of ~c[form]
should return a single value that is not ~ilc[state] or a single-threaded
object (~pl[stobj]).
If the form you want to evaluate does not satisfy the criterion
above, you should create an appropriate call of the ~c[lisp] command
instead. Notice that this command always returns
~c[(mv nil nil state)] where the second result will always be
~c[REPLACED-STATE]."
(value `(lisp (io? proof-checker nil state
(fms0 "~|~y0~|" (list (cons #\0 ,form)))))))
(defun bounded-integer-listp (i j lst)
;; If i is a non-integer, then it's -infinity.
;; If j is a non-integer, then it's +infinity.
(if (consp lst)
(and (integerp (car lst))
(if (integerp i)
(if (integerp j)
(and (<= i (car lst))
(<= (car lst) j))
(<= i (car lst)))
(<= (car lst) j)))
(null lst)))
(defun fetch-term-and-cl (term addr cl)
;; Returns the subterm of TERM at address ADDR paired with a list
;; containing the tests governing that occurrence of the subterm plus
;; the literals of the input CL. However, if CL is T then we simply
;; return (mv nil t) (see also below).
;; I've assumed that the address is a list of positive integers. If
;; the address is not valid for diving into TERM according to ADDR,
;; then we return (mv nil t). Notice that ADDR is expected to be in
;; the correct order, while CL is in reverse order and the extension
;; of CL returned in the second position is also in reverse order.
;; For the funny contrapositive subcase of IMPLIES, note that
;; (implies (implies (and u (not x)) (equal y1 y2))
;; (implies u (equal (implies y1 x) (implies y2 x))))
;; is a tautology. However, the corresponding fact does not hold in
;; general for IF; it depends on x being boolean.
(declare (xargs :guard (bounded-integer-listp 1 'infinity addr)))
(cond ((eq cl t)
(mv nil t))
((null addr)
(mv term cl))
((or (variablep term) (fquotep term))
;; can't dive any further
(mv nil t))
((and (integerp (car addr))
(< 0 (car addr))
(< (car addr) (length term)))
(case-match term
(('if t1 t2 t3)
(cond ((= 1 (car addr))
(fetch-term-and-cl t1 (cdr addr) cl))
((= 2 (car addr))
(fetch-term-and-cl t2 (cdr addr) (cons t1 cl)))
(t (fetch-term-and-cl t3 (cdr addr) (cons (dumb-negate-lit t1) cl)))))
(('implies t1 t2)
(cond ((= 1 (car addr))
(fetch-term-and-cl t1 (cdr addr) (cons (dumb-negate-lit t2) cl)))
(t
(fetch-term-and-cl t2 (cdr addr) (cons t1 cl)))))
(& (fetch-term-and-cl (nth (1- (car addr)) (fargs term)) (cdr addr) cl))))
(t
(mv nil t))))
(defun fetch-term (term addr)
;; causes hard error when appropriate
(mv-let (term cl)
(fetch-term-and-cl term addr nil)
(if (eq cl t)
(er hard 'fetch-term
"FETCH-TERM-AND-CL did not find a subterm of ~x0 at address ~x1."
term addr)
term)))
(defun governors (term addr)
(mv-let (term cl)
(fetch-term-and-cl term addr nil)
(declare (ignore term))
;; note that cl could be T rather than a list of governors
cl))
;;;;;;!!!!!!! I should generalize the following to arbitrary equivalence stuff.
(defun term-id-iff (term address iff-flg)
;; The property we want is that if one substitutes an equivalent subterm
;; of TERM at the given address (equivalent modulo the flag returned by
;; this function, that is), then the resulting term is equivalent modulo
;; the IFF-FLG argument to the original TERM. We assume that address is
;; a valid address for term. (*** This should really be a guard.)
(if (null address)
iff-flg
;; so, the term is a function application
(term-id-iff (nth (car address) term)
(cdr address)
(cond ((eq (ffn-symb term) (quote if))
(if (= (car address) 1)
t
iff-flg))
((member-eq (ffn-symb term) (quote (implies iff not)))
t)
(t
nil)))))
(defun invert-abbreviations-alist (alist)
(declare (xargs :guard (alistp alist)))
(if (null alist)
nil
(cons (cons (cdr (car alist)) (list '? (car (car alist))))
(invert-abbreviations-alist (cdr alist)))))
;; The way abbreviations will work is as follows. For input, an
;; abbreviation variable is to be thought of as a placeholder for
;; literal substitution (*before* translation!). It was tempting to
;; think of abbreviation variables as standing for something else only
;; when they're in variable position, but the problem with that
;; approach is that we can't tell about the position until we've done
;; the translation (consider macro calls that look at the first
;; character, say, for example). On a pragmatic (implementation)
;; level, it's hard to see how to implement a translator that
;; substitutes for abbreviation variables only when they're in
;; variable position, except by modifying translate. On the other
;; hand, for untranslation the specification is only that
;; (trans (untrans x)) = x, where here translation is with respect
;; to abbreviations. Notice though that this spec messes things
;; up, because if x is (quote &v) then untrans of that is still
;; (quote &v) but then trans would remove the &v, if we use sublis
;; to deal with abbreviations.
;; So, I think I'll implement abbreviations as follows. There will
;; be a new "macro":
;; (defmacro ? (x)
;; (cdr (assoc-eq x (abbreviations))))
;; Notice however that (abbreviations) generates a reference to
;; state, which isn't compatible with ? being a macro. So, I'll
;; stub it out:
(defmacro ? (x)
`(?-fn ',x))
(defstub ?-fn (x)
t)
;; Now, translation will be followed by an appropriate substitution.
;; For convenience, abbreviations will be turned into an alist whose
;; pairs are of the form ((&-fn 'var) . term).
(defun abbreviations-alist (abbreviations)
(if (consp abbreviations)
(cons (cons (fcons-term* '?-fn (kwote (caar abbreviations)))
(cdar abbreviations))
(abbreviations-alist (cdr abbreviations)))
nil))
(mutual-recursion
(defun chk-?s (term ctx state)
;; There shouldn't be any ?-fns in term.
(cond
((or (variablep term) (fquotep term))
(value nil))
((eq (ffn-symb term) '?-fn)
(case-match term
((& ('quote var))
(if (variablep var)
(er soft ctx "The variable ~x0 is not among the current abbreviations."
var)
(er soft ctx "Expected a variable in place of ~x0."
var)))
(& (value (er hard ctx "Bad call of ?-FN, ~x0. ?-FN must be called on the quotation of ~
a variable."
term)))))
((flambdap (ffn-symb term))
(er-progn (chk-?s (lambda-body (ffn-symb term)) ctx state)
(chk-?s-lst (fargs term) ctx state)))
(t (chk-?s-lst (fargs term) ctx state))))
(defun chk-?s-lst (term-lst ctx state)
(if (consp term-lst)
(er-progn (chk-?s (car term-lst) ctx state)
(chk-?s-lst (cdr term-lst) ctx state))
(value nil)))
)
(defun remove-?s (term abbreviations-alist ctx state)
(let ((newterm (sublis-expr abbreviations-alist term)))
(er-progn (chk-?s newterm ctx state)
(value newterm))))
(defun translate-abb (x abbreviations ctx state)
(mv-let
(erp term state)
(translate x t
; Since we only use this function in a logical context, we set
; logic-modep to t.
t t ctx (w state) state)
(if erp
(mv erp term state)
(remove-?s term (abbreviations-alist abbreviations) ctx state))))
(defmacro trans0 (x &optional abbreviations ctx)
`(translate-abb ,x ,abbreviations ,(or ctx ''trans0) state))
(mutual-recursion
(defun sublis-expr-non-quoteps (alist term)
;; Same as ACL2's function sublis-expr, except that it doesn't take a
;; world argument. However, for correctness it may be necessary that
;; every CDR in ALIST is non-quotep, so that we can guarantee that
;; non-quotep's are mapped to non-quotep's.
(let ((temp (assoc-equal term alist)))
(cond (temp (cdr temp))
((variablep term) term)
((fquotep term) term)
(t (let ((new-args (sublis-expr-non-quoteps-lst alist (fargs term))))
(if (quote-listp new-args)
;; then no substitution was actually made
term
;; otherwise, cons-term becomes simply cons
(cons (ffn-symb term) new-args)))))))
(defun sublis-expr-non-quoteps-lst (alist lst)
(cond ((null lst) nil)
(t (cons (sublis-expr-non-quoteps alist (car lst))
(sublis-expr-non-quoteps-lst alist (cdr lst))))))
)
(defun abbreviate (term abbreviations)
(if (null abbreviations)
term
(sublis-expr-non-quoteps (invert-abbreviations-alist abbreviations) term)))
(defmacro untrans0 (term &optional iff-flg abbreviations)
; Note that state should always be bound where this is called.
`(untranslate (abbreviate ,term ,abbreviations) ,iff-flg (w state)))
(defun untrans0-lst-fn (termlist iff-flg abbreviations state)
(if (consp termlist)
(cons (untrans0 (car termlist) iff-flg abbreviations)
(untrans0-lst-fn (cdr termlist) iff-flg abbreviations state))
nil))
(defmacro untrans0-lst (termlist &optional iff-flg abbreviations)
`(untrans0-lst-fn ,termlist ,iff-flg ,abbreviations state))
(defun p-body (conc current-addr abbreviations state)
(io? proof-checker nil state
(fms0 "~|~y0~|"
(list (cons #\0 (untrans0 (fetch-term conc current-addr)
(term-id-iff conc current-addr t)
abbreviations))))))
(define-pc-help p ()
#-small-acl2-image
"prettyprint the current term~/
~bv[]
Example and General Form:
p
~ev[]~/
Prettyprint the current term. The usual user syntax is used, so
that for example one would see ~c[(and x y)] rather than ~c[(if x y 'nil)].
(See also ~c[pp].) Also, abbreviations are inserted where appropriate;
see ~c[add-abbreviation].
The ``current term'' is the entire conclusion unless ~c[dive] commands
have been given, in which case it may be a subterm of the
conclusion.
If all goals have been proved, a message saying so will be printed
(as there will be no current ~c[term]!)."
(if (goals t)
(p-body (conc t) (current-addr t) (abbreviations t) state)
(print-all-goals-proved-message state)))
(define-pc-help pp ()
#-small-acl2-image
"prettyprint the current term~/
~bv[]
Example and General Form:
pp
~ev[]~/
This is the same as ~c[p] (see its documentation), except that raw
syntax (internal form) is used. So for example, one would see
~c[(if x y 'nil)] rather than ~c[(and x y)]. Abbreviations are however
still inserted, as with ~c[p].~/"
(if (goals t)
(io? proof-checker nil state
(fms0 "~|~y0~|"
(list (cons #\0 (fetch-term (conc t) (current-addr t))))))
(print-all-goals-proved-message state)))
(defun take-by-indices (m indices lst)
;; (declare (xargs :guard (null (non-bounded-nums indices m (length lst)))))
;; this was ok for the original entry, but it's not preserved
(if (consp lst)
(if (member-equal m indices)
(cons (car lst) (take-by-indices (1+ m) indices (cdr lst)))
(take-by-indices (1+ m) indices (cdr lst)))
nil))
(defun print-hyps (indexed-hyps ndigits abbreviations state)
(declare (xargs :guard (and (eqlable-alistp indexed-hyps)
(integerp ndigits)
(> ndigits 0))))
(if (null indexed-hyps)
state
(pprogn (io? proof-checker nil state
(fms0 "~c0. ~y1~|"
(list (cons #\0 (cons (caar indexed-hyps) ndigits))
(cons #\1 (untrans0 (cdar indexed-hyps) t abbreviations)))))
(print-hyps (cdr indexed-hyps) ndigits abbreviations state))))
(defun some-> (lst n)
;; says whether some element of lst exceeds n
(declare (xargs :guard (and (rational-listp lst)
(rationalp n))))
(if lst
(or (> (car lst) n)
(some-> (cdr lst) n))
nil))
(defun print-hyps-top (indexed-hyps abbreviations state)
(declare (xargs :guard (eqlable-alistp indexed-hyps)))
(if (null indexed-hyps)
(io? proof-checker nil state
(fms0 "~|There are no top-level hypotheses.~|"))
(print-hyps indexed-hyps (if (some-> (strip-cars indexed-hyps) 9) 2 1)
abbreviations state)))
(defun print-governors-top (indexed-hyps abbreviations state)
(declare (xargs :guard (eqlable-alistp indexed-hyps)))
(if (null indexed-hyps)
(io? proof-checker nil state
(fms0 "~|There are no governors.~|"))
(print-hyps indexed-hyps (if (some-> (strip-cars indexed-hyps) 9) 2 1)
abbreviations state)))
(defun pair-indices (seed indices lst)
;; Returns a list of indices paired with the corresponding (1-based) element of
;; lst when in range. Seed is a starting integer; we do things this way
;; because we want the result sorted (and hence want to recurse on lst).
(declare (xargs :guard (and (integerp seed)
(true-listp lst)
(bounded-integer-listp 1 (length lst) indices))))
(if lst
(let ((rest-lst
(pair-indices (1+ seed) indices (cdr lst))))
(if (member seed indices)
(cons (cons seed (car lst))
rest-lst)
rest-lst))
nil))
(define-pc-macro hyps (&optional hyps-indices govs-indices)
#-small-acl2-image
"print the hypotheses~/
~bv[]
Examples:
hyps -- print all (top-level) hypotheses
(hyps (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4
(hyps (1 3) t) -- print hypotheses 1 and 3 and all governors~/
General Form:
(hyps &optional hyps-indices govs-indices)
~ev[]
Print the indicated top-level hypotheses and governors. (The notion
of ``governors'' is defined below.) Here, ~c[hyps-indices] and
~c[govs-indices] should be lists of indices of hypotheses and governors
(respectively), except that the atom ~c[t] may be used to indicate that
one wants all hypotheses or governors (respectively).
The list of ``governors'' is defined as follows. Actually, we
define here the notion of the governors for a pair of the form
~c[]; we're interested in the special case where the
term is the conclusion and the address is the current address. If
the address is ~c[nil], then there are no governors, i.e., the list of
governors is ~c[nil]. If the term is of the form ~c[(if x y z)] and the
address is of the form ~c[(2 . rest)] or ~c[(3 . rest)], then the list of
governors is the result of ~c[cons]ing ~c[x] or its negation (respectively)
onto the list of governors for the pair ~c[] or the pair
~c[] (respectively). If the term is of the form ~c[(implies x y)]
and the address is of the form ~c[(2 . rest)], then the list of
governors is the result of ~c[cons]ing ~c[x] onto the list of governors for
the pair ~c[]. Otherwise, the list of governors for the pair
~c[] is exactly the list of governors for the pair
~c[] where ~c[argn] is the ~c[n]th argument of ~c[term].
If all goals have been proved, a message saying so will be printed.
(as there will be no current hypotheses or governors!).
The ~c[hyps] command never causes an error. It ``succeeds'' (in fact
its value is ~c[t]) if the arguments (when supplied) are appropriate,
i.e. either ~c[t] or lists of indices of hypotheses or governors,
respectively. Otherwise it ``fails'' (its value is ~c[nil])."
(if (goals t)
(let* ((hyps (hyps t))
(len-hyps (length hyps))
(govs (and govs-indices;; for efficiency
(governors (conc t) (current-addr t))))
(len-govs (length govs))
(abbs (abbreviations t))
(hyps-indices (or hyps-indices
(null args))))
(cond
((not (or (eq hyps-indices t) (bounded-integer-listp 1 len-hyps hyps-indices)))
(pprogn
(io? proof-checker nil state
(fms0 "~|Bad hypothesis-list argument to HYPS, ~x0. The hypothesis-list ~
argument should either be T or should be a list of integers between ~
1 and the number of top-level hypotheses, ~x1.~%"
(list (cons #\0 hyps-indices)
(cons #\1 len-hyps))))
(value :fail)))
((not (or (eq govs-indices t) (bounded-integer-listp 1 len-govs govs-indices)))
(pprogn
(io? proof-checker nil state
(fms0 "~|Bad governors-list argument to HYPS,~% ~x0.~%The governors-list ~
argument should either be T or should be a list of integers between ~
1 and the number of top-level governors, ~x1."
(list (cons #\0 govs-indices)
(cons #\1 len-govs))))
(value :fail)))
((and (null hyps-indices) (null govs-indices))
(pprogn
(io? proof-checker nil state
(fms0 "~|You have specified no printing of either hypotheses or governors! Perhaps ~
you should read the documentation for the HYPS command.~|"))
(value :fail)))
(t
(let ((hyps-to-print
(if (eq hyps-indices t)
(count-off 1 hyps)
(pair-indices 1 hyps-indices hyps)))
(govs-to-print
(if (eq govs-indices t)
(count-off 1 govs)
(pair-indices 1 govs-indices govs))))
(pprogn
(if hyps-indices
(pprogn
(if (eq hyps-indices t)
(io? proof-checker nil state
(fms0 "~|*** Top-level hypotheses:~|"))
(io? proof-checker nil state
(fms0 "~|*** Specified top-level hypotheses:~|")))
(print-hyps-top hyps-to-print abbs state))
state)
(if govs-indices
(pprogn
(if (eq govs-indices t)
(io? proof-checker nil state
(fms0 "~|~%*** Governors:~|"))
(io? proof-checker nil state
(fms0 "~|~%*** Specified governors:~|")))
(print-governors-top govs-to-print abbs state))
state)
(value 'skip))))))
(pprogn (print-all-goals-proved-message state)
(value 'skip))))
(define-pc-primitive demote (&rest rest-args)
#-small-acl2-image
"move top-level hypotheses to the conclusion~/
~bv[]
Examples:
demote -- demote all top-level hypotheses
(demote 3 5) -- demote hypotheses 3 and 5
~ev[]
For example, if the top-level hypotheses are ~c[x] and ~c[y] and the
conclusion is ~c[z], then after execution of ~c[demote], the conclusion will
be ~c[(implies (and x y) z)] and there will be no (top-level)
hypotheses.~/
~bv[]
General Form:
(demote &rest hyps-indices)
~ev[]
Eliminate the indicated (top-level) hypotheses, but replace the
conclusion ~c[conc] with ~c[(implies hyps conc)] where ~c[hyps] is the
conjunction of the hypotheses that were eliminated. If no arguments
are supplied, then all hypotheses are demoted, i.e. ~c[demote] is the
same as ~c[(demote 1 2 ... n)] where ~c[n] is the number of top-level
hypotheses.
~st[Note]: You must be at the top of the conclusion in order to use
this command. Otherwise, first invoke ~c[top]. Also, ~c[demote] fails if
there are no top-level hypotheses or if indices are supplied that
are out of range.~/"
(cond
(current-addr
(print-no-change2 "You must be at the top of the conclusion in order to ~
demote hypotheses. Try TOP first."))
((null hyps)
(print-no-change2 "There are no top-level hypotheses."))
(t
(let ((badindices (non-bounded-nums rest-args 1 (length hyps))))
(if badindices
(print-no-change2 "The arguments to DEMOTE ~
must be indices of active top-level hypotheses, ~
but the following are not: ~&0."
(list (cons #\0 badindices)))
(mv (change-pc-state
pc-state
:goals
(cons (change goal (car goals)
:hyps (if rest-args
(remove-by-indices 1 rest-args hyps)
nil)
:conc (make-implication
(if rest-args
(take-by-indices 1 rest-args hyps)
hyps)
conc))
(cdr goals)))
state))))))
;; **** I may want to replace the following with something taking advantage
;; of whatever ACL2 does to collect up keywords to defthm or whatever.
(defun all-keywords-p (keywords)
(if (consp keywords)
(and (keywordp (car keywords))
(all-keywords-p (cdr keywords)))
(null keywords)))
(defun pair-keywords (keywords lst)
(declare (xargs :guard (and (all-keywords-p keywords)
(keyword-value-listp lst))))
;; returns (mv alist rst)
(if (consp keywords)
(mv-let (alist rst)
(pair-keywords (cdr keywords) lst)
(let ((tail (assoc-keyword (car keywords) rst)))
(if tail
(mv (cons (cons (car tail) (cadr tail)) alist)
;; could use a remove1 version of the following, but who cares?
(remove-keyword (car keywords) rst))
(mv alist rst))))
(mv nil lst)))
(defun null-pool (pool)
(cond
((null pool) t)
((eq (access pool-element (car pool) :tag) 'being-proved-by-induction)
(null-pool (cdr pool)))
(t nil)))
(defun initial-rcnst (wrld)
(initial-rcnst-from-ens
(global-val 'global-enabled-structure wrld)
wrld))
(defun initial-pspv (term displayed-goal otf-flg wrld)
(change prove-spec-var *empty-prove-spec-var*
:rewrite-constant (initial-rcnst wrld)
:user-supplied-term term
:displayed-goal displayed-goal
:otf-flg otf-flg))
(defun pc-prove (term displayed-goal hints otf-flg wrld ctx state)
;; This is exactly the same as the ACL2 PROVE function, except that
;; we allow :bye objects in the tag tree,
;; and there's no checking of the load mode.
(prog2$
(initialize-brr-stack)
(er-let* ((ttree (prove-loop (list (list term))
(initial-pspv term
displayed-goal
otf-flg
wrld)
hints wrld ctx state)))
(er-progn
(chk-assumption-free-ttree ttree ctx state)
(value ttree)))))
(defun sublis-equal (alist tree)
(declare (xargs :guard (alistp alist)))
(let ((pair (assoc-equal tree alist)))
(if pair
(cdr pair)
(if (atom tree)
tree
(cons (sublis-equal alist (car tree))
(sublis-equal alist (cdr tree)))))))
(defun abbreviations-alist-? (abbreviations)
;; Same as abbreviations-alist, except that we assume that we
;; haven't translated yet, and hence we use ? instead of ?-fn
;; and we don't quote the variable.
(if (consp abbreviations)
(cons (cons (fcons-term* '? (caar abbreviations))
(cdar abbreviations))
(abbreviations-alist-? (cdr abbreviations)))
nil))
(defun find-?-fn (x)
;; x is not necessarily a term. Heuristically though it's useful
;; to be able to find all (?-fn var) subexpressions of x.
(if (atom x)
nil
(if (eq (car x) '?-fn)
(list (cadr x))
(union-equal (find-?-fn (car x))
(find-?-fn (cdr x))))))
(defun unproved-pc-prove-terms (ttree)
(strip-cdrs (tagged-objects :bye ttree nil)))
(defun prover-call (comm term-to-prove rest-args pc-state state)
;; We assume that the :otf-flg and :hints "hints" are locally inside
;; a variable called rest-args, which in fact are the arguments to the
;; instruction being processed.
;; Returns an error triple (mv erp-flg ttree state).
(declare (xargs :guard (keywordp comm)))
(let ((prover-call-abbreviations (access pc-state pc-state :abbreviations))
(prover-call-wrld (w state)))
(let ((prover-call-pc-ens (make-pc-ens (access pc-state pc-state :pc-ens) prover-call-wrld)))
(mv-let (prover-call-pairs prover-call-tail)
(pair-keywords '(:otf-flg :hints) rest-args)
(if prover-call-tail
(pprogn
(print-no-change
"The only keywords allowed in the arguments to the ~x0 command ~
are :otf-flg and :hints. Your ~
instruction ~x1 violates this requirement."
(list (cons #\0 comm)
(cons #\1
(make-pretty-pc-instr (cons comm rest-args)))))
(mv t nil state))
(mv-let (prover-call-erp prover-call-hints state)
(let ((un-?-hints
(sublis-equal
;; *** someday I should do this all right
(abbreviations-alist-? prover-call-abbreviations)
(cdr (assoc-eq :hints prover-call-pairs)))))
(let ((?-exprs (find-?-fn un-?-hints)))
(if ?-exprs
(pprogn
(print-no-change
"You appear to have attempted to use the following ~
abbreviation variable~#0~[~/~/s~], which however ~
~#0~[~/is~/are~] not among ~
the current abbreviation variables (see SHOW-ABBREVIATIONS): ~&1."
(list (cons #\0 (zero-one-or-more (length ?-exprs)))
(cons #\1 ?-exprs)))
(mv t nil state))
(pprogn
(io? proof-checker nil state
(fms0 "~|***** Now entering the theorem prover *****~|"))
(translate-hints 'proof-checker
un-?-hints
comm
prover-call-wrld
state)))))
(if prover-call-erp
(pprogn (print-no-change
"Failed to translate hints successfully.")
(mv t nil state))
(let ((prover-call-otf-flg (cdr (assoc-eq :otf-flg prover-call-pairs))))
(mv-let (prover-call-erp prover-call-ttree state)
(pc-prove
term-to-prove
(untranslate term-to-prove t prover-call-wrld)
prover-call-hints prover-call-otf-flg
;; ****** consider doing something faster
;; than the following in the future, which will
;; be easy if PROVE gets an enabled structure arg
(global-set 'global-enabled-structure
prover-call-pc-ens
prover-call-wrld)
comm state)
(pprogn (io? proof-checker nil state
(fms0 "~%"))
(if prover-call-erp
(pprogn (print-no-change "Proof failed.")
(mv t nil state))
(mv nil prover-call-ttree state))))))))))))
(defun make-new-goals (cl-set goal-name start-index)
;; assumes that every member of CL-SET is a non-empty true list (should be a guard)
(if (consp cl-set)
(cons (make goal
:conc (car (last (car cl-set)))
:hyps (dumb-negate-lit-lst (butlast (car cl-set) 1))
:current-addr nil
:goal-name (cons goal-name start-index)
:depends-on 1)
(make-new-goals (cdr cl-set) goal-name (1+ start-index)))
nil))
(defun same-goal (goal1 goal2)
(and (equal (access goal goal1 :hyps)
(access goal goal2 :hyps))
(equal (access goal goal1 :conc)
(access goal goal2 :conc))))
(defun remove-byes-from-tag-tree (ttree)
(cond ((null ttree) nil)
((eq ttree t)
(er hard 'remove-byes-from-tag-tree
"Found tag tree of T in REMOVE-BYES-FROM-TAG-TREE."))
((eq :bye (caar ttree))
;; then ttree is ((:bye ...)) and we could perhaps return ()
;; but we play it safe
(remove-byes-from-tag-tree (cdr ttree)))
((symbolp (caar ttree))
(cons (car ttree)
(remove-byes-from-tag-tree (cdr ttree))))
(t (cons-tag-trees
(remove-byes-from-tag-tree (car ttree))
(remove-byes-from-tag-tree (cdr ttree))))))
(define-pc-primitive prove (&rest rest-args)
#-small-acl2-image
"call the ACL2 theorem prover to prove the current goal~/
~bv[]
Examples:
prove -- attempt to prove the current goal
(prove :otf-flg t
:hints ((\"Subgoal 2\" :by foo) (\"Subgoal 1\" :use bar)))
-- attempt to prove the current goal, with the indicated hints
and with OTF-FLG set~/
General Form:
(prove &rest rest-args)
~ev[]
Attempt to prove the current goal, where ~c[rest-args] is as in the
keyword arguments to ~c[defthm] except that only ~c[:hints] and ~c[:otf-flg] are
allowed. The command succeeds exactly when the corresponding ~c[defthm]
would succeed, except that it is all right for some goals to be
given ``bye''s. Each goal given a ``bye'' will be turned into a new
subgoal. (~l[hints] for an explanation of ~c[:by] hints.)
~st[Note:] Use ~c[(= t)] instead if you are not at the top of the
conclusion. Also note that if there are any hypotheses in the
current goal, then what is actually attempted is a proof of
~c[(implies hyps conc)], where ~c[hyps] is the conjunction of the
top-level hypotheses and ~c[conc] is the goal's conclusion.
~st[Note:] It is allowed to use abbreviations in the hints."
(cond
(current-addr
(print-no-change2 "The PROVE command should only be used at ~
the top. Use (= T) if that is what you want."))
((not (keyword-value-listp rest-args))
(print-no-change2 "The argument list for the PROVE command should ~
be empty or a list of even length with keywords in the odd ~
positions. See the documentation for examples and details."))
(t
(mv-let (erp ttree state)
(prover-call
:prove (make-implication hyps conc) rest-args pc-state state)
(if erp
(mv nil state)
(let* ((new-terms
(unproved-pc-prove-terms ttree))
(new-goals
(make-new-goals new-terms goal-name depends-on)))
(if (and (equal (length new-terms)
1)
(same-goal (car new-goals)
(car goals)))
(print-no-change2 "Exactly one new goal was created by your PROVE ~
command, and it has exactly the same hypotheses ~
and conclusion as did the current goal.")
(mv
(change-pc-state
pc-state
:goals
(append new-goals (cdr goals))
:tag-tree
(cons-tag-trees
(remove-byes-from-tag-tree ttree)
tag-tree))
state))))))))
(defun add-string-val-pair-to-string-val-alist (key key1 val alist)
;; adapted from ACL2 function add-to-set-equal-in-alist
(cond ((null alist) (list (list key key1 val)))
((string-equal key (caar alist))
(cons (list* (caar alist) key1 val (cdar alist))
(cdr alist)))
(t (cons (car alist)
(add-string-val-pair-to-string-val-alist key key1 val (cdr alist))))))
(defconst *bash-skip-forcing-round-hints*
'(("[1]Goal" :by nil)
("[1]Subgoal 1" :by nil)
("[1]Subgoal 2" :by nil)
("[1]Subgoal 3" :by nil)
("[1]Subgoal 4" :by nil)
("[1]Subgoal 5" :by nil)
("[1]Subgoal 6" :by nil)
("[1]Subgoal 7" :by nil)
("[1]Subgoal 8" :by nil)
("[1]Subgoal 9" :by nil)
("[1]Subgoal 10" :by nil)
("[1]Subgoal 11" :by nil)
("[1]Subgoal 12" :by nil)
("[1]Subgoal 13" :by nil)
("[1]Subgoal 14" :by nil)
("[1]Subgoal 15" :by nil)))
(define-pc-atomic-macro bash (&rest hints)
#-small-acl2-image
"call the ACL2 theorem prover's simplifier~/
~bv[]
Examples:
bash -- attempt to prove the current goal by simplification alone
(bash (\"Subgoal 2\" :by foo) (\"Subgoal 1\" :use bar))
-- attempt to prove the current goal by simplification alone,
with the indicated hints~/
General Form:
(bash &rest hints)
~ev[]
Call the theorem prover's simplifier, creating a subgoal for each
resulting goal.
Notice that unlike ~c[prove], the arguments to ~c[bash] are spread out, and
are all hints.
~st[Note:] All forcing rounds will be skipped (unless there are more
than 15 subgoals generated in the first forcing round, an injustice
that should be rectified by the next release)."
(if (alistp hints)
(value (list :prove :hints
(append
*bash-skip-forcing-round-hints*
(add-string-val-pair-to-string-val-alist
"Goal"
;; only preprocess and simplify are allowed
:do-not
(list 'quote '(generalize eliminate-destructors
fertilize eliminate-irrelevance))
(add-string-val-pair-to-string-val-alist
"Goal"
:do-not-induct
'proof-checker
hints)))
:otf-flg t))
(pprogn (print-no-change
"A BASH instruction must be of the form~%~ ~ ~
(:BASH (goal_name_1 ...) ... (goal_name_n ...)),~%and hence ~
your instruction,~%~ ~ ~x0,~%is not legal."
(list (cons #\0 (cons :bash hints))))
(value :fail))))
(define-pc-primitive dive (n &rest rest-addr)
#-small-acl2-image
"move to the indicated subterm~/
~bv[]
Examples:
(DIVE 1) -- assign the new current subterm to be the first
argument of the existing current subterm
(DIVE 1 2) -- assign the new current subterm to be the result of
first taking the 1st argument of the existing
current subterm, and then the 2nd argument of that
~ev[]
For example, if the current subterm is
~bv[]
(* (+ a b) c),
~ev[]
then after ~c[(dive 1)] it is
~bv[]
(+ a b).
~ev[]
If after that, then ~c[(dive 2)] is invoked, the new current subterm
will be
~bv[]
b.
~ev[]
Instead of ~c[(dive 1)] followed by ~c[(dive 2)], the same current subterm
could be obtained by instead submitting the single instruction
~c[(dive 1 2)].~/
~bv[]
General Form:
(dive &rest naturals-list)
~ev[]
If ~c[naturals-list] is a non-empty list ~c[(n_1 ... n_k)] of natural
numbers, let the new current subterm be the result of selecting the
~c[n_1]-st argument of the current subterm, and then the ~c[n_2]-th subterm
of that, ..., finally the ~c[n_k]-th subterm.
~st[Note:] ~c[Dive] is related to the command ~c[pp], in that the diving is done
according to raw (translated, internal form) syntax. Use the
command ~c[dv] if you want to dive according to the syntax displayed by
the command ~c[p]. Note that ~c[(dv n)] can be abbreviated by simply ~c[n]."
(if (not (bounded-integer-listp 1 'infinity args))
(print-no-change2 "The arguments to DIVE must all be positive integers.")
(mv-let (subterm cl)
(fetch-term-and-cl (fetch-term conc current-addr) args nil)
(declare (ignore subterm))
(if (eq cl t)
(print-no-change2
"Unable to DIVE according to the address~%~ ~ ~y0."
(list (cons #\0 (cons n rest-addr))))
(mv (change-pc-state pc-state
:goals
(cons (change goal (car goals)
:current-addr
(append (access goal (car goals) :current-addr)
args))
(cdr goals)))
state)))))
; Keep this in sync with translate-in-theory-hint.
(define-pc-atomic-macro split ()
#-small-acl2-image
"split the current goal into cases~/
~bv[]
Example:
split
~ev[]
For example, if the current goal has one hypothesis ~c[(or x y)] and a
conclusion of ~c[(and a b)], then ~c[split] will create four new goals:
~bv[]
one with hypothesis X and conclusion A
one with hypothesis X and conclusion B
one with hypothesis Y and conclusion A
one with hypothesis Y and conclusion B.~/
General Form:
SPLIT
~ev[]
Replace the current goal by subgoals whose conjunction is equivalent
(primarily by propositional reasoning) to the original goal, where
each such goal cannot be similarly split.
~st[Note:] The new goals will all have their hypotheses promoted; in
particular, no conclusion will have a top function symbol of
~c[implies]. Also note that ~c[split] will fail if there is exactly one new
goal created and it is the same as the existing current goal.
The way ~c[split] really works is to call the ACL2 theorem prover with
only simplification (and preprocessing) turned on, and with only a
few built-in functions (especially, propositional ones) enabled,
namely, the ones in the list ~c[*s-prop-theory*]. However, because the
prover is called, type-set reasoning can be used to eliminate some
cases. For example, if ~c[(true-listp x)] is in the hypotheses, then
probably ~c[(true-listp (cdr x))] will be reduced to ~c[t]."
(value '(:prove :hints
(("Goal"
:do-not-induct proof-checker
:do-not '(generalize eliminate-destructors
fertilize eliminate-irrelevance)
:in-theory *s-prop-theory*)))))
;;;!!!!! I need to use push-lemma here instead. Now, ttrees contain runes
;; in place of lemma names.
(defun add-fnnames-to-tag-tree (fnnames ttree)
(if (consp fnnames)
(add-fnnames-to-tag-tree
(cdr fnnames)
(push-lemma (list :definition (car fnnames))
ttree))
ttree))
(define-pc-primitive add-abbreviation (var &optional raw-term)
#-small-acl2-image
"add an abbreviation~/
Example: ~c[(add-abbreviation v (* x y))] causes future occurrences of
~c[(* x y)] to be printed as ~c[(? v)], until (unless) a corresponding
invocation of ~c[remove-abbreviations] occurs. In this case we say that
~c[v] ``abbreviates'' ~c[(* x y)].~/
~bv[]
General Form:
(add-abbreviation var &optional raw-term)
~ev[]
Let ~c[var] be an abbreviation for ~c[raw-term], if ~c[raw-term] is supplied,
else for the current subterm. Note that ~c[var] must be a variable that
does not already abbreviate some term.
A way to think of abbreviations is as follows. Imagine that
whenever an abbreviation is added, say ~c[v] abbreviates ~c[expr], an entry
associating ~c[v] to ~c[expr] is made in an association list, which we will
call ``~c[*abbreviations-alist*]''. Then simply imagine that ~c[?] is a
function defined by something like:
~bv[]
(defun ? (v)
(let ((pair (assoc v *abbreviations-alist*)))
(if pair (cdr pair)
(error ...))))
~ev[]
Of course the implementation isn't exactly like that, since the
``constant'' ~c[*abbreviations-alist*] actually changes each time an
~c[add-abbreviation] instruction is successfully invoked. Nevertheless,
if one imagines an appropriate redefinition of the ``constant''
~c[*abbreviations-alist*] each time an ~c[add-abbreviation] is invoked, then
one will have a clear model of the meaning of such an instruction.
The effect of abbreviations on output is that before printing a
term, each subterm that is abbreviated by a variable ~c[v] is first
replaced by ~c[(? v)].
The effect of abbreviations on input is that every built-in
proof-checker command accepts abbreviations wherever a term is
expected as an argument, i.e., accepts the syntax ~c[(? v)] whenever ~c[v]
abbreviates a term. For example, the second argument of
~c[add-abbreviation] may itself use abbreviations that have been defined
by previous ~c[add-abbreviation] instructions.
See also ~c[remove-abbreviations] and ~c[show-abbreviations]."
(mv-let (erp term state)
(if (cdr args)
(trans0 raw-term abbreviations :add-abbreviation)
(value (fetch-term conc current-addr)))
(cond
(erp (mv nil state))
((variablep var)
(if (assoc-eq var abbreviations)
(print-no-change2 "The abbreviation ~x0 has already been used, and stands for ~x1."
(list (cons #\0 var)
(cons #\1 (untrans0 (cdr (assoc-eq var abbreviations))))))
(mv (change-pc-state pc-state
:abbreviations
(cons (cons var term) abbreviations)
:tag-tree
(add-fnnames-to-tag-tree (all-fnnames term) tag-tree))
state)))
(t
(print-no-change2 "An abbreviation must be a variable, but ~x0 is not."
(list (cons #\0 var)))))))
(defun not-in-domain-eq (lst alist)
(declare (xargs :guard (or (symbol-listp lst)
(symbol-alistp alist))))
(if (consp lst)
(if (assoc-eq (car lst) alist)
(not-in-domain-eq (cdr lst) alist)
(cons (car lst)
(not-in-domain-eq (cdr lst) alist)))
nil))
(define-pc-primitive remove-abbreviations (&rest vars)
#-small-acl2-image
"remove one or more abbreviations~/
~bv[]
Examples:
remove-abbreviations -- remove all abbreviations
(remove-abbreviations v w)
-- assuming that V and W currently abbreviate
terms, then they are ``removed'' in the
sense that they are no longer considered to
abbreviate those terms~/
General Forms:
(remove-abbreviations &rest vars)
~ev[]
If vars is not empty (i.e., not ~c[nil]), remove the variables in ~c[vars]
from the current list of abbreviations, in the sense that each
variable in ~c[vars] will no longer abbreviate a term.
~st[Note:] The instruction fails if at least one of the arguments
fails to be a variable that abbreviates a term.
See also the documentation for ~c[add-abbreviation], which contains a
discussion of abbreviations in general, and ~c[show-abbreviations]."
(if (null abbreviations)
(print-no-change2 "There are currently no abbreviations.")
(let ((badvars (and args (not-in-domain-eq vars abbreviations))))
(if (and args badvars)
(print-no-change2 "The variable~#0~[~/~/s~] ~&1 ~
~#0~[~/is not currently an abbreviation variable~/~
are not currently abbreviation variables~]."
(list (cons #\0 (zero-one-or-more (length badvars)))
(cons #\1 badvars)))
(mv (change-pc-state
pc-state
:abbreviations
(if args
(delete-assoc-eq-lst vars abbreviations)
nil))
state)))))
(defun print-abbreviations (vars abbreviations state)
;; Here abbreviations can contain junky pairs.
(declare (xargs :guard (and (true-listp vars)
(symbol-alistp abbreviations))))
(if (null vars)
state
(pprogn
(io? proof-checker nil state
(fms0 "~%"))
(let ((pair (assoc-equal (car vars) abbreviations)))
(if (null pair)
;; then this pair is junk
(io? proof-checker nil state
(fms0 "*** ~x0 does not abbreviate a term.~|"
(list (cons #\0 (car vars)))))
(let ((untrans-1 (untrans0 (cdr pair)))
(untrans-2 (untrans0 (cdr pair)
nil
(delete-assoc-eq (car pair) abbreviations))))
(pprogn
(io? proof-checker nil state
(fms0 "(? ~x0) is an abbreviation for:~%~ ~ "
(list (cons #\0 (car pair)))))
(io? proof-checker nil state
(fms0 "~y0~|"
(list (cons #\0 untrans-1))
2))
(if (equal untrans-1 untrans-2)
state
(pprogn
(io? proof-checker nil state
(fms0 "i.e. for~%~ ~ "))
(io? proof-checker nil state
(fms0 "~y0~|"
(list (cons #\0 untrans-2))
2))))))))
(print-abbreviations (cdr vars) abbreviations state))))
(define-pc-help show-abbreviations (&rest vars)
#-small-acl2-image
"display the current abbreviations~/
~bv[]
Examples:
(show-abbreviations v w)
-- assuming that v and w currently abbreviate terms,
then this instruction displays them together with
the terms they abbreviate
show-abbreviations
-- display all abbreviations
~ev[]
See also ~c[add-abbreviation] and ~c[remove-abbreviations]. In
particular, the documentation for ~c[add-abbreviation] contains a
general discussion of abbreviations.~/
~bv[]
General Form:
(show-abbreviations &rest vars)
~ev[]
Display each argument in ~c[vars] together with the term it abbreviates
(if any). If there are no arguments, i.e. the instruction is simply
~c[show-abbreviations], then display all abbreviations together with the
terms they abbreviate.
If the term abbreviated by a variable, say ~c[v], contains a proper
subterm that is also abbreviate by (another) variable, then both the
unabbreviated term and the abbreviated term (but not using ~c[(? v)] to
abbreviate the term) are displayed with together with ~c[v]."
(if (null (abbreviations t))
(io? proof-checker nil state
(fms0 "~|There are currently no abbreviations.~%"))
(print-abbreviations (or vars (strip-cars (abbreviations t))) (abbreviations t) state)))
(defun drop-from-end (n l)
(declare (xargs :guard (and (integerp n)
(not (< n 0))
(true-listp l)
(<= n (length l)))))
(take (- (length l) n) l))
(define-pc-primitive up (&optional n)
#-small-acl2-image
"move to the parent (or some ancestor) of the current subterm~/
~bv[]
Examples: if the conclusion is (= x (* (- y) z)) and the
current subterm is y, then we have:
up or (up 1) -- the current subterm becomes (- y)
(up 2) -- the current subterm becomes (* (- y) z)
(up 3) -- the current subterm becomes the entire conclusion
(up 4) -- no change; can't go up that many levels~/
General Form:
(up &optional n)
~ev[]
Move up ~c[n] levels in the conclusion from the current subterm, where ~c[n]
is a positive integer. If ~c[n] is not supplied or is ~c[nil], then move up
1 level, i.e., treat the instruction as ~c[(up 1)].
See also ~c[dive], ~c[top], ~c[nx], and ~c[bk]."
(let ((n (or n 1)))
(cond ((null current-addr)
(print-no-change2 "Already at the top."))
((not (and (integerp n) (> n 0)))
(print-no-change2 "If UP is supplied with an argument, it must be ~
a positive integer or NIL, unlike ~x0."
(list (cons #\0 n))))
((<= n (length current-addr))
(mv (change-pc-state pc-state
:goals
(cons (change goal (car goals)
:current-addr
(drop-from-end n current-addr))
(cdr goals)))
state))
(t
(print-no-change2 "Can only go up ~x0 level~#1~[~/~/s~]."
(list (cons #\0 (length current-addr))
(cons #\1 (zero-one-or-more (length current-addr)))))))))
(define-pc-atomic-macro top ()
#-small-acl2-image
"move to the top of the goal~/
~bv[]
Example and General Form:
top
~ev[]
For example, if the conclusion is ~c[(= x (* (- y) z))] and the
current subterm is ~c[y], then after executing ~c[top], the current subterm
will be the same as the conclusion, i.e., ~c[(= x (* (- y) z))].~/
~c[Top] is the same as ~c[(up n)], where ~c[n] is the number of times one needs
to execute ~c[up] in order to get to the top of the conclusion. The ~c[top]
command fails if one is already at the top of the conclusion.
See also ~c[up], ~c[dive], ~c[nx], and ~c[bk]."
(let ((current-addr (current-addr t)))
(value (list :up (length current-addr)))))
(defmacro expand-address-recurse
(&key (ans '(cons (car addr) rest-addr))
(new-addr '(cdr addr))
(new-raw-term '(nth (car addr) raw-term))
(new-term '(nth (car addr) term))
(new-iff-flg 'nil)
(new-accumulated-addr-r '(cons (car addr) accumulated-addr-r)))
`(mv-let (erp rest-addr)
(expand-address
,new-addr ,new-raw-term ,new-term abbreviations ,new-iff-flg ,new-accumulated-addr-r
wrld)
(if erp
(mv erp rest-addr)
(mv nil ,ans))))
(defmacro dive-once-more-error ()
'(mv "When diving to subterm ~x0 using address ~x1, ~
the additional dive to ~x2 was impossible."
(list (cons #\0 raw-term)
(cons #\1 (reverse accumulated-addr-r))
(cons #\2 (car addr)))))
(defun abbreviation-raw-term-p (x)
(and (consp x)
(eq (car x) '?)))
(defmacro addr-recur (pos b)
`(if (integerp ,pos)
(mv-let (addr new-term new-iff-flg not-flg)
,b
(if (stringp addr)
(mv addr nil nil nil)
(mv (cons ,pos addr) new-term new-iff-flg not-flg)))
(if (eq ,pos 'not)
,(case-match b
(('mv 'nil x y 'nil)
`(mv nil ,x ,y t))
(&
'(mv "a NOT term unexpected by the code; sorry" nil nil nil)))
(mv ,pos nil nil nil))))
(defun or-addr (n raw-term term iff-flg wrld)
;; We assume that term has already been abbreviated.
;; To dive n into (untranslate term iff-flg wrld), which is an
;; OR expression, we use the list (or-addr n raw-term term) in the
;; translated term.
;; We return (mv addr new-term new-iff-flg), except:
;; -- addr can be a string, denoting an error;
;; Note that not-flg is non-nil when addr really
;; gets us farther than the user requested, namely into a term x
;; such that (NOT x) had been pretty printed. So, the user should
;; provide a next address of 1. The new-term returned here "assumes"
;; that that further dive has already been done.
(if (not (and (consp raw-term)
(equal (car raw-term) 'or)))
(mv nil term iff-flg nil)
(mv-let (p q x1 x1-iff x1-pos x2 x2-iff x2-pos)
;; We only need the non-raw terms for recursive calls.
;; We put strings in for x1-pos and x2-pos that become error messages
;; in case we are supposed to go into them further.
(case-match term
(('if x1 x1 x2)
(mv (untranslate x1 iff-flg wrld)
(untranslate x2 iff-flg wrld)
x1 iff-flg "an ambiguous dive to first arg of an OR"
x2 iff-flg 3))
(('if x1 x2 *t*)
(mv (list 'not (untranslate x1 t wrld))
(untranslate x2 iff-flg wrld)
x1 t 'not
x2 iff-flg 2))
(('if x1 *t* x2)
(cond
((or iff-flg
(and (nvariablep x1)
(not (fquotep x1))
(member-eq (ffn-symb x1)
*untranslate-boolean-primitives*)))
(mv (untranslate x1 t wrld)
(untranslate x2 iff-flg wrld)
x1 t 1 x2 iff-flg 3))
(t (mv nil nil
nil nil "a non-OR term, unexpected by the code; sorry"
nil nil "a non-OR term, unexpected by the code; sorry"))))
(&
(mv nil nil
nil nil "a non-OR term, unexpected by the code; sorry"
nil nil "a non-OR term, unexpected by the code; sorry")))
(cond ((and (consp p)
(eq (car p) 'or))
(cond ((and (consp q)
(eq (car q) 'or))
(if (< n (length p))
(addr-recur x1-pos (or-addr n p x1 x1-iff wrld))
(addr-recur x2-pos (or-addr (- n (length (cdr p))) q x2
x2-iff wrld))))
(t (if (< n (length p))
(addr-recur x1-pos (or-addr n p x1 x1-iff wrld))
(if (equal n (length p))
(addr-recur x2-pos (mv nil x2 x2-iff nil))
(mv "an index that is out of range" nil nil nil))))))
((and (consp q)
(eq (car q) 'or))
(if (equal n 1)
(addr-recur x1-pos (mv nil x1 x1-iff nil))
(addr-recur x2-pos
(or-addr (- n 1) q x2 x2-iff wrld))))
(t (if (equal n 1)
(addr-recur x1-pos (mv nil x1 x1-iff nil))
(if (equal n 2)
(addr-recur x2-pos (mv nil x2 x2-iff nil))
(mv "an index that is out of range" nil nil nil))))))))
(defun and-addr (n raw-term term iff-flg wrld)
;; We assume that term has already been abbreviated.
;; To dive n into (untranslate term iff-flg wrld), which is an
;; AND expression, we use the list (and-addr n raw-term term wrld) in the
;; translated term.
;; We return (mv addr new-term new-iff-flg not-flg), except:
;; -- addr can be a string, denoting an error
;; Note that not-flg is non-nil when addr really
;; gets us farther than the user requested, namely into a term x
;; such that (NOT x) had been pretty printed. So, the user should
;; provide a next address of 1. The new-term returned here "assumes"
;; that that further dive has already been done.
(if (not (and (consp raw-term)
(equal (car raw-term) 'and)))
(mv nil term iff-flg nil)
(mv-let (p q x1 x1-iff x1-pos x2 x2-iff x2-pos)
;; We only need the non-raw terms for recursive calls.
;; We put strings in for x1-pos and x2-pos that become error messages
;; in case we are supposed to go into them further.
(case-match term
(('if x1 x2 *nil*)
(mv (untranslate x1 t wrld)
(untranslate x2 iff-flg wrld)
x1 t 1
x2 iff-flg 2))
(('if x1 *nil* x2)
(mv (list 'not (untranslate x1 t wrld))
(untranslate x2 iff-flg wrld)
x1 t 'not
x2 iff-flg 3))
(&
(mv nil nil
nil nil "a non-AND term, unexpected by the code; sorry"
nil nil "a non-AND term, unexpected by the code; sorry")))
(cond ((or (eq p t) (eq q t))
(mv "an unexpected situation in the code -- an arg of the AND prints as T"
nil nil nil))
((and (consp p)
(eq (car p) 'and))
(cond ((and (consp q)
(eq (car q) 'and))
(if (< n (length p))
(addr-recur x1-pos (and-addr n p x1 x1-iff wrld))
(addr-recur x2-pos (and-addr (- n (length (cdr p))) q x2
x2-iff wrld))))
(t (if (< n (length p))
(addr-recur x1-pos (and-addr n p x1 x1-iff wrld))
(if (equal n (length p))
(addr-recur x2-pos (mv nil x2 x2-iff nil))
(mv "an index that is out of range" nil nil nil))))))
((and (consp q)
(eq (car q) 'and))
(if (equal n 1)
(addr-recur x1-pos (mv nil x1 x1-iff nil))
(addr-recur x2-pos
(and-addr (- n 1) q x2 x2-iff wrld))))
(t (if (equal n 1)
(addr-recur x1-pos (mv nil x1 x1-iff nil))
(if (equal n 2)
(addr-recur x2-pos (mv nil x2 x2-iff nil))
(mv "an index that is out of range" nil nil nil))))))))
(defun expand-address (addr raw-term term abbreviations iff-flg accumulated-addr-r wrld)
;; This roughly parallels the definition of UNTRANSLATE in ACL2.
;; It returns an address appropriate for diving into term,
;; assuming that addr is appropriate for diving into raw-term.
;; We keep accumulated-addr-r as the raw address already traversed (in reverse order)
;; only for error messages.
;; It's tempting to have a guard of
;; (equal raw-term (untrans0 term iff-flg abbreviations)). Let's at least make
;; a weak attempt to maintain this invariant.
(cond ((or (null addr)
(equal addr '(0)))
(mv nil nil))
((abbreviation-raw-term-p raw-term)
;; The car of addr should be 0 or 1, but I'll be generous and simply strip
;; off whatever it is. By the way, it doesn't make a whole lot of sense
;; for the cdr of addr to be anything other than NIL (else why is DV being
;; used?), but I won't enforce that here.
(let ((pair (assoc-eq (cadr raw-term) abbreviations)))
(if pair
(expand-address (cdr addr) (cdr pair) term
(delete1-equal pair abbreviations)
iff-flg
(cons (car addr) accumulated-addr-r)
wrld)
(mv t (er hard 'expand-address
"Found abbreviation variable ~x0 that is not in the ~
current abbreviations alist, ~x1."
(cadr raw-term) abbreviations)))))
((not (and (integerp (car addr))
(< 0 (car addr))))
(mv "All members of an address must be positive integers ~
(except that 0 is allowed in circumstances involving ~
CASE, COND, and abbreviations, which do not apply ~
here). ~x0 violates this requirement."
(list (cons #\0 (car addr)))))
((or (variablep raw-term)
(fquotep raw-term)
(not (< (car addr) (length raw-term))))
(dive-once-more-error))
((flambda-applicationp raw-term)
(expand-address-recurse))
((atom raw-term)
(mv t (er hard 'expand-address
"Surprise! Found an unexpected raw-term atom, ~x0."
raw-term)))
(t
(case
(car raw-term)
(<=
; Note that (<= x y) is really (not (< y x)).
(cond
((not (member (car addr) '(1 2)))
(dive-once-more-error))
((= (car addr) 1)
(expand-address-recurse
:ans (cons 1 (cons 2 rest-addr))
:new-iff-flg nil
:new-term (nth 2 (nth 1 term))))
(t ; (= (car addr) 2)
(expand-address-recurse
:ans (cons 1 (cons 1 rest-addr))
:new-iff-flg nil
:new-term (nth 1 (nth 1 term))))))
((list + * append list*)
;; E.g., (and a b c d) is (if a (if b (if c d 'nil) 'nil) 'nil),
;; so diving 3 into this (to c) generates address (2 2 1),
;; but diving 4 generates address (2 2 2), not (2 2 2 1).
(let* ((lst (if (and (not (eq (car raw-term) 'list))
(= (car addr) (1- (length raw-term))))
(make-list (1- (car addr)) :initial-element 2)
(append (make-list (1- (car addr)) :initial-element 2)
'(1))))
(subterm (fetch-term term lst)))
(if subterm
(expand-address-recurse
:ans (append lst rest-addr)
:new-iff-flg nil
:new-term subterm)
(dive-once-more-error))))
((and or)
(mv-let (and-or-addr new-term new-iff-flg not-flg)
(if (eq (car raw-term) 'and)
(and-addr (car addr) raw-term
(abbreviate term abbreviations) iff-flg
wrld)
(or-addr (car addr) raw-term
(abbreviate term abbreviations) iff-flg wrld))
(cond
((stringp and-or-addr)
(mv "The dive via address ~x0 brings us to the ~x4 ~
term~%~ ~ ~y1,~|~%which translates to~%~ ~ ~
~y2.~|~%The requested dive into this ~x4 term is ~
problematic, because of ~s3. Try using DIVE ~
instead (after using PP to find the appropriate ~
address)."
(list (cons #\0 (reverse accumulated-addr-r))
(cons #\1 raw-term)
(cons #\2 term)
(cons #\3 and-or-addr)
(cons #\4 (car raw-term)))))
(not-flg
(cond
((cdr and-or-addr)
(mv t
(er hard 'expand-address
"Expected address '(not), but got ~x0."
and-or-addr)))
((not (and (consp (nth (car addr) raw-term))
(eq (car (nth (car addr) raw-term)) 'not)))
(mv "Sorry -- there seems to be an inconsistency in ~
the code. We expected a NOT term after diving ~
using address ~x0, but instead we got ~x1."
(list (cons #\0 (reverse (cons (car addr) accumulated-addr-r)))
(cons #\1 (nth (car addr) raw-term)))))
((equal (cadr addr) 1)
(expand-address-recurse
:ans (append and-or-addr (cons 1 rest-addr))
:new-addr (cddr addr)
:new-raw-term (cadr (nth (car addr) raw-term))
:new-term new-term
:new-iff-flg new-iff-flg
:new-accumulated-addr-r (cons 1 (cons (car addr) accumulated-addr-r))))
(t
(mv "The dive via address ~x0 presumably brings us ~
to the NOT term ~x1, which does not actually ~
exist in the internal syntax of the term ~
currently being dived into, ~x2. Try using ~
DIVE instead (after using PP to find the ~
appropriate address)."
(list (cons #\0 (reverse (cons (car addr) accumulated-addr-r)))
(cons #\1 (nth (car addr) raw-term))
(cons #\2 term))))))
(t
(expand-address-recurse
:ans (append and-or-addr rest-addr)
:new-term new-term
:new-iff-flg new-iff-flg)))))
(case
;; For example,
;; (case a (b c) (d e) ((f g) h) (otherwise k))
;; translates to
;; (IF (EQL A 'B)
;; C
;; (IF (EQL A 'D)
;; E
;; (IF (MEMBER A '(F G)) H K))) .
;; So, we can only dive to addresses of the form (n 1 ...)
;; and (n 0 ...), though the latter cases aren't too interesting.
;; In the example above,
;; (2 1 ...) gets us to c, which should generate (2)
;; (3 1 ...) gets us to e, which should generate (3 2)
;; (4 1 ...) gets us to h, which should generate (3 3 2)
;; (5 1 ...) gets us to k, which should generate (3 3 3).
;; (2 0 ...) gets us to b, which should generate (1 2)
;; (3 0 ...) gets us to d, which should generate (3 1 2)
;; (4 0 ...) gets us to (f g), which should generate (3 3 1 2)
;; (5 0 ...) gets us to "otherwise", which is an error
(cond
((= (car addr) 1)
(mv "The dive via address ~x0 brings us to the CASE term~%~ ~ ~x1,~%~
which corresponds to the translated term~%~ ~ ~x2.~%~
A further dive to the first argument doesn't really make sense here."
(list (cons #\0 (reverse accumulated-addr-r))
(cons #\1 raw-term)
(cons #\2 term))))
((not (and (consp (cdr addr))
(member-equal (cadr addr) '(0 1))))
(mv "The dive via address ~x0 brings us to the CASE term~%~ ~ ~x1,~%~
A further dive past argument number ~x2 to the zeroth or first ``argument'' ~
is required at this point.~%"
(list (cons #\0 (reverse accumulated-addr-r))
(cons #\1 raw-term)
(cons #\2 (car addr)))))
((and (= (cadr addr) 0)
(= (car addr) (1- (length raw-term))))
(mv "The dive via address ~x0 brings us to the CASE term~%~ ~ ~x1,~%~
A further dive to the ``otherwise'' expression is not allowed."
(list (cons #\0 (reverse accumulated-addr-r))
(cons #\1 raw-term))))
(t
(let* ((lst (if (= (cadr addr) 1)
(if (= (car addr) (1- (length raw-term)))
(make-list (- (car addr) 2) :initial-element 3)
(append (make-list (- (car addr) 2)
:initial-element 3)
'(2)))
;; otherwise (car addr) is 0 and
;; (car addr) < (1- (length raw-term))
(append (make-list (- (car addr) 2)
:initial-element 3)
'(1 2))))
(subterm (fetch-term term lst)))
(if subterm
(expand-address-recurse
:ans (append lst rest-addr)
:new-addr (cddr addr)
:new-raw-term (cadr (nth (1+ (car addr)) raw-term))
:new-term subterm
:new-iff-flg iff-flg
:new-accumulated-addr-r (cons (car addr) (cons (cadr addr) accumulated-addr-r)))
(mv t
(er hard 'expand-address
"Surprise! Unable to dive into raw-term ~x0, which is term ~x1,
using list ~x2. So far we have DV-ed using ~x3."
raw-term
term
lst
(reverse accumulated-addr-r))))))))
(cond
;; For example,
;; (cond (a b) (c d) (e f) (t g))
;; translates to
;; (if a b (if c d (if e f g)))
;; So, we can dive to addresses of the form (n 0 ...)
;; and (n 1 ...).
;; (1 0 ...) gets us to a, which should generate (1)
;; (2 0 ...) gets us to c, which should generate (3 1)
;; (3 0 ...) gets us to e, which should generate (3 3 1)
;; (4 0 ...) gets us to t, which is not allowed.
;; (1 1 ...) gets us to b, which should generate (2)
;; (2 1 ...) gets us to d, which should generate (3 2)
;; (3 1 ...) gets us to f, which should generate (3 3 2)
;; (4 1 ...) gets us to g, which should generate (3 3 3)
(cond
((not (and (consp (cdr addr))
(member-equal (cadr addr) '(0 1))))
(mv "The dive via address ~x0 brings us to the COND term~%~ ~ ~x1,~%~
A further dive past argument number ~x2 to the zeroth or first ``argument'' ~
is required at this point.~%"
(list (cons #\0 (reverse accumulated-addr-r))
(cons #\1 raw-term)
(cons #\2 (car addr)))))
((and (= (cadr addr) 0)
(= (car addr) (1- (length raw-term))))
(mv "The dive via address ~x0 brings us to the COND term~%~ ~ ~x1,~%~
A further dive to the ``T'' expression is not allowed."
(list (cons #\0 (reverse accumulated-addr-r))
(cons #\1 raw-term))))
(t
(let* ((lst (if (= (cadr addr) 1)
(if (= (car addr) (1- (length raw-term)))
(make-list (1- (car addr)) :initial-element 3)
(append (make-list (1- (car addr))
:initial-element 3)
'(2)))
;; otherwise (cadr addr) is 0 and (car addr) < (1- (length raw-term))
(append (make-list (1- (car addr))
:initial-element 3)
'(1))))
(subterm (fetch-term term lst)))
(if subterm
(expand-address-recurse
:ans (append lst rest-addr)
:new-addr (cddr addr)
:new-raw-term (cadr (nth (1+ (car addr)) raw-term))
:new-term subterm
:new-iff-flg iff-flg
:new-accumulated-addr-r (cons (car addr) (cons (cadr addr) accumulated-addr-r)))
(mv t
(er hard 'expand-address
"Surprise! Unable to dive into raw-term ~x0, which is term ~x1,
using list ~x2. So far we have DV-ed using ~x3."
raw-term
term
lst
(reverse accumulated-addr-r))))))))
(if
(expand-address-recurse
:new-iff-flg (if (= (car addr) 1) t iff-flg)))
((implies iff)
(expand-address-recurse :new-iff-flg t))
(t
(mv-let
(fn guts)
(car-cdr-nest term)
(cond
(fn
(expand-address-recurse
:ans (append (make-list (- (length (symbol-name fn)) 2)
:initial-element 1)
rest-addr)
:new-term guts))
(t (expand-address-recurse)))))))))
(defmacro dv-error (str alist)
`(pprogn (print-no-change
(string-append "Unable to dive into ~xt.~%~ ~ " ,str)
(cons (cons #\t current-term) ,alist))
(mv t nil state)))
(define-pc-atomic-macro dv (&rest rest-args)
#-small-acl2-image
"move to the indicated subterm~/
~bv[]
Examples:
(dv 1) -- assign the new current subterm to be the first argument
of the existing current subterm
(dv 1 2) -- assign the new current subterm to be the result of
first taking the 1st argument of the existing
current subterm, and then the 2nd argument of that
~ev[]
For example, if the current subterm is
~bv[]
(* (+ a b) c),
~ev[]
then after ~c[(dv 1)] it is
~bv[]
(+ a b).
~ev[]
If after that, then ~c[(dv 2)] is invoked, the new current subterm
will be
~bv[]
b.
~ev[]
Instead of ~c[(dv 1)] followed by ~c[(dv 2)], the same current subterm
could be obtained by instead submitting the single instruction
~c[(dv 1 2)].~/
~bv[]
General Form:
(dv &rest naturals-list)
~ev[]
If ~c[naturals-list] is a non-empty list ~c[(n_1 ... n_k)] of natural
numbers, let the new current subterm be the result of selecting the
~c[n_1]-st argument of the current subterm, and then the ~c[n_2]-th subterm
of that, ..., finally the ~c[n_k]-th subterm.
~st[Note:] ~c[(dv n)] may be abbreviated by simply ~c[n], so we could have typed
~c[1] instead of ~c[(dv 1)] in the first example above.
~st[Note:] See also ~c[dive], which is related to the command ~c[pp], in that
the diving is done according to raw (translated, internal form)
syntax. Use the command ~c[dv] if you want to dive according to the
syntax displayed by the command ~c[p]."
(let* ((conc (conc t))
(current-addr (current-addr t))
(abbreviations (abbreviations t))
(current-term (fetch-term conc current-addr))
(term-id-iff (term-id-iff conc current-addr t)))
(mv-let (erp addr)
;; If erp is not nil, then it's a string explaining why DV failed,
;; and then addr is a list of args for that string (except #\t is
;; associated with 'current-term).
(expand-address rest-args
(untrans0 current-term
term-id-iff
abbreviations)
current-term
abbreviations
term-id-iff
nil
(w state))
(if erp
(dv-error erp addr)
(mv nil (cons ':dive addr) state)))))
(mutual-recursion
(defun deposit-term (term addr subterm)
;; Puts subterm at address addr in term. Assumes that error checking is
;; not necessary, i.e. that addr is given correctly relative to term,
(cond ((null addr) subterm)
(t
(cons-term (ffn-symb term)
(deposit-term-lst (fargs term) (car addr) (cdr addr) subterm)))))
(defun deposit-term-lst (lst n addr subterm)
;; This simply puts (deposit-term term addr subterm) in place of the nth
;; element, term, of lst, but avoids consing up the unchanged tail.
(cond ((= 1 n)
(cons (deposit-term (car lst) addr subterm) (cdr lst)))
(t (cons (car lst) (deposit-term-lst (cdr lst) (1- n) addr subterm)))))
)
;; Suppose that we want to make congruence-based substitution. Here
;; is the plan. Then (unless the congruence is equality) we need to
;; make sure that wherever the substitution is to be made, the
;; congruence relation is enough to preserve the geneqv at the current
;; subterm. The following function actually returns a list of congruence
;; rules.
(defun geneqv-at-subterm (term addr geneqv ens wrld)
;; The property we want is that if one substitutes an equivalent
;; subterm of TERM at the given address (equivalent modulo the
;; generated equivalence relation returned by this function, that
;; is), then the resulting term is equivalent modulo geneqv to the
;; original TERM. We assume that address is a valid address for
;; term. (*** This should really be a guard.) As usual, we may
;; return NIL for 'equal.
(if (null addr)
geneqv
(geneqv-at-subterm
(nth (1- (car addr)) (fargs term))
(cdr addr)
(nth (1- (car addr))
;; ***** seems inefficient to do all the computing just below
(geneqv-lst (ffn-symb term) geneqv ens wrld))
ens
wrld)))
(defun geneqv-at-subterm-top (term addr ens wrld)
(geneqv-at-subterm term addr *geneqv-iff* ens wrld))
#|
;; In the following we want to know if every occurrence of old in term
;; is at a position at which substitution by something EQUIV to old
;; will guarantee a result that is GENEQV to term.
(mutual-recursion
(defun subst-expr1-okp (old term equiv geneqv ens wrld)
(cond ((equal term old)
(geneqv-refinementp equiv geneqv wrld))
((variablep term) t)
((fquotep term) t)
(t (subst-expr1-ok-listp old (fargs term)
(geneqv-lst (ffn-symb term) geneqv ens wrld)
equiv ens wrld))))
(defun subst-expr1-ok-listp (old args equiv geneqv-lst ens wrld)
(cond ((null args) nil)
(t (and (subst-expr1-okp
old (car args) equiv (car geneqv-lst) ens wrld)
(subst-expr1-ok-listp
old (cdr args) equiv (cdr geneqv-lst) ens wrld)))))
)
|#
;; **** Need to think about what happens if we, e.g., substitute T for X
;; inside (equal X T). Probably that's OK -- but also, consider allowing
;; an equivalence relation as an argument. One would have to check that
;; the relation is OK in at the current address, and then one would use
;; that relation instead of equal to create the proof obligation. Also,
;; consider special handling for IFF in the case that it's (IFF ... T),
;; so that we can simulate pc-nqthm's PUSH command.
;; ****** give a warning if the term to be replaced doesn't occur in the
;; current subterm
;; The following are adapted from ACL2 definitions of subst-expr1 and
;; subst-expr1-lst. Note that the parameter `new' has been dropped,
;; but the given and current equivalence relations have been added.
(defun maybe-truncate-current-address (addr term orig-addr acc state)
;; Truncates the current address if it tries to dive into a quotep.
;; Here orig-addr is the original address (used for the warning message)
;; and acc is the accumulated new address (in reverse order).
(declare (xargs :guard (true-listp addr)))
(if addr
(cond
((variablep term)
(mv (er hard 'maybe-truncate-current-address
"Found variable with non-NIL address!")
state))
((fquotep term)
(let ((new-addr (reverse acc)))
(pprogn (io? proof-checker nil state
(fms0 "~|NOTE: truncating current address from ~
~x0 to ~x1. See explanation at end of ~
help for X command.~|"
(list (cons #\0 orig-addr)
(cons #\1 new-addr))))
(mv new-addr state))))
(t
(maybe-truncate-current-address
(cdr addr) (nth (1- (car addr)) (fargs term))
orig-addr (cons (car addr) acc) state)))
(mv (reverse acc) state)))
(defun deposit-term-in-goal (given-goal conc current-addr new-term state)
;; state is passed in so that maybe-truncate-current-address can
;; print a warning message if appropriate
(let ((new-conc (deposit-term conc current-addr new-term)))
(if (quotep new-term)
(mv-let (new-current-addr state)
(maybe-truncate-current-address
current-addr new-conc current-addr nil state)
(mv (change goal given-goal
:conc
new-conc
:current-addr
new-current-addr)
state))
(mv (change goal given-goal
:conc
new-conc)
state))))
(defun split-implies (term)
;; returns hyps and conc for term, e.g.
;; (implies x y) --> (mv (list x) y),
;; (implies x (implies (and y z)) w) --> (mv (list x y z) w), and
;; (foo 3) --> (mv nil (foo 3))
(if (or (variablep term)
(fquotep term)
(not (eq (ffn-symb term) 'implies)))
(mv nil term)
(mv-let (h c)
(split-implies (fargn term 2))
(mv (append (conjuncts-of (fargn term 1)) h) c))))
(defun equiv-refinementp (equiv1 equiv2 wrld)
(member-eq equiv2
(getprop equiv1 'coarsenings nil 'current-acl2-world wrld)))
(defun find-equivalence-hyp-term (term hyps target equiv w)
;; allows backchaining through IMPLIES
(if (consp hyps)
(mv-let (h c)
(split-implies (car hyps))
(if (or (variablep c)
(fquotep c)
(not (equiv-refinementp (ffn-symb c) equiv w)))
(find-equivalence-hyp-term term (cdr hyps) target equiv w)
(let ((x (fargn c 1))
(y (fargn c 2)))
(or
(and (subsetp-equal h hyps)
(or (and (equal x term)
(equal y target))
(and (equal y term)
(equal x target))))
(find-equivalence-hyp-term term (cdr hyps) target equiv w)))))
nil))
(defun flatten-ands-in-lit-lst (x)
(if (endp x)
nil
(append (flatten-ands-in-lit (car x))
(flatten-ands-in-lit-lst (cdr x)))))
(define-pc-primitive equiv (x y &optional equiv)
#-small-acl2-image
"attempt an equality (or congruence-based) substitution~/
~bv[]
Examples:
(equiv (* x y) 3) -- replace (* x y) by 3 everywhere inside the
current subterm, if their equality is among the
top-level hypotheses or the governors
(equiv x t iff) -- replace x by t everywhere inside the current
subterm, where only propositional equivalence
needs to be maintained at each occurrence of x~/
General form:
(equiv old new &optional relation)
~ev[]
Substitute new for old everywhere inside the current subterm,
provided that either (relation old new) or (relation new old) is
among the top-level hypotheses or the governors (possibly by way of
backchaining and/or refinement; see below). If relation is ~c[nil] or
is not supplied, then it defaults to ~c[equal]. See also the command ~c[=],
which is much more flexible. Note that this command fails if no
substitution is actually made.
~st[Note:] No substitution takes place inside explicit values. So for
example, the instruction ~c[(equiv 3 x)] will cause ~c[3] to be replaced by
~c[x] if the current subterm is, say, ~c[(* 3 y)], but not if the current
subterm is ~c[(* 4 y)] even though ~c[4 = (1+ 3)].
The following remarks are quite technical and mostly describe a
certain weak form of ``backchaining'' that has been implemented for
~c[equiv] in order to support the ~c[=] command. In fact neither the term
~c[(relation old new)] nor the term ~c[(relation new old)] needs to be
~st[explicitly] among the current ``assumptions'', i.e., the top-level
hypothesis or the governors. Rather, there need only be such an
assumption that ``tells us'' ~c[(r old new)] or ~c[(r new old)], for ~st[some]
equivalence relation ~c[r] that ~st[refines] ~c[relation]. Here, ``tells us''
means that either one of the indicated terms is among those
assumptions, or else there is an assumption that is an implication
whose conclusion is one of the indicated terms and whose hypotheses
(gathered up by appropriately flattening the first argument of the
~c[implies] term) are all among the current assumptions."
(mv-let
(current-term governors)
(fetch-term-and-cl conc current-addr nil)
(cond
((eq governors t)
(mv (er hard ':=
"Found governors of T inside command ~x0!"
(cons := args))
state))
(t
(let* ((assumptions (append hyps governors))
(w (w state))
(pc-ens (make-pc-ens pc-ens w)))
(mv-let
(erp new-pc-state state)
(er-let*
((old (trans0 x abbreviations :equiv))
(new (trans0 y abbreviations :equiv))
(equiv (if (null equiv)
(value 'equal)
(if (equivalence-relationp equiv w)
(value equiv)
(er soft :equiv
"The name ~x0 is not currently the name of an ACL2 ~
equivalence relation. The current list of ~
ACL2 equivalence relations is ~x1."
equiv
(getprop 'equal 'coarsenings nil
'current-acl2-world w))))))
(if (find-equivalence-hyp-term old
(flatten-ands-in-lit-lst assumptions)
new equiv w)
(mv-let (hitp new-current-term new-ttree)
(subst-equiv-expr1 equiv new old
(geneqv-at-subterm-top conc current-addr pc-ens w)
current-term pc-ens w state tag-tree)
(if hitp
(mv-let
(new-goal state)
(deposit-term-in-goal
(car goals) conc current-addr new-current-term state)
(value (change-pc-state
pc-state
:tag-tree
new-ttree
:goals
(cons new-goal (cdr goals)))))
(pprogn
(print-no-change
"The equivalence relation that you specified, namely ~x0, is ~
not appropriate at any occurrence of the ``old'' term ~x1 ~
inside the current term, and hence no substitution has ~
been made."
(list (cons #\0 equiv)
(cons #\1 x)))
(value nil))))
(pprogn
(print-no-change
"The ~#2~[equivalence~/equality~] of the terms ~x0 and ~x1~#2~[ with respect ~
to the equivalence relation ~x3~