other
(in-package "ACL2")
pc-valuemacro
(defmacro pc-value (sym) (cond ((eq sym 'ss-alist) '(f-get-global 'pc-ss-alist state)) (t `(cdr (assoc-eq ',SYM (f-get-global 'pc-output state))))))
pc-assignmacro
(defmacro pc-assign (key val) (cond ((eq key 'ss-alist) `(f-put-global 'pc-ss-alist ,VAL state)) (t `(f-put-global 'pc-output (put-assoc-eq ',KEY ,VAL (f-get-global 'pc-output state)) state))))
initialize-pc-acl2function
(defun initialize-pc-acl2 (state) (er-progn (assign pc-output nil) (pprogn (pc-assign ss-alist nil) (pc-assign old-ss nil) (pc-assign state-stack nil) (pc-assign next-pc-enabled-array-suffix 0) (pc-assign pc-depth 0) (assign in-verify-flg nil))))
state-stackmacro
(defmacro state-stack nil '(pc-value state-stack))
other
(defrec pc-info ((print-macroexpansion-flg . print-prompt-and-instr-flg) prompt . prompt-depth-prefix) nil)
pc-print-prompt-and-instr-flgmacro
(defmacro pc-print-prompt-and-instr-flg nil '(access pc-info (f-get-global 'pc-info state) :print-prompt-and-instr-flg))
pc-print-macroexpansion-flgmacro
(defmacro pc-print-macroexpansion-flg nil '(access pc-info (f-get-global 'pc-info state) :print-macroexpansion-flg))
pc-promptmacro
(defmacro pc-prompt nil '(access pc-info (f-get-global 'pc-info state) :prompt))
pc-prompt-depth-prefixmacro
(defmacro pc-prompt-depth-prefix nil '(access pc-info (f-get-global 'pc-info state) :prompt-depth-prefix))
other
(defrec pc-state (instruction (goals . abbreviations) local-tag-tree pc-ens . tag-tree) nil)
*pc-state-fields-for-primitives*constant
(defconst *pc-state-fields-for-primitives* '(instruction goals abbreviations tag-tree local-tag-tree pc-ens))
instructionmacro
(defmacro instruction (&optional state-stack-supplied-p) `(access pc-state (car ,(IF STATE-STACK-SUPPLIED-P 'STATE-STACK '(STATE-STACK))) :instruction))
goalsmacro
(defmacro goals (&optional state-stack-supplied-p) `(access pc-state (car ,(IF STATE-STACK-SUPPLIED-P 'STATE-STACK '(STATE-STACK))) :goals))
abbreviationsmacro
(defmacro abbreviations (&optional state-stack-supplied-p) `(access pc-state (car ,(IF STATE-STACK-SUPPLIED-P 'STATE-STACK '(STATE-STACK))) :abbreviations))
local-tag-treemacro
(defmacro local-tag-tree (&optional state-stack-supplied-p) `(access pc-state (car ,(IF STATE-STACK-SUPPLIED-P 'STATE-STACK '(STATE-STACK))) :local-tag-tree))
pc-ensmacro
(defmacro pc-ens (&optional state-stack-supplied-p) `(access pc-state (car ,(IF STATE-STACK-SUPPLIED-P 'STATE-STACK '(STATE-STACK))) :pc-ens))
tag-treemacro
(defmacro tag-tree (&optional state-stack-supplied-p) `(access pc-state (car ,(IF STATE-STACK-SUPPLIED-P 'STATE-STACK '(STATE-STACK))) :tag-tree))
other
(defrec goal (conc depends-on (hyps . current-addr) goal-name) t)
*goal-fields*constant
(defconst *goal-fields* '(conc hyps current-addr goal-name depends-on))
concmacro
(defmacro conc (&optional ss-supplied-p) `(access goal (car (goals ,SS-SUPPLIED-P)) :conc))
hypsmacro
(defmacro hyps (&optional ss-supplied-p) `(access goal (car (goals ,SS-SUPPLIED-P)) :hyps))
current-addrmacro
(defmacro current-addr (&optional ss-supplied-p) `(access goal (car (goals ,SS-SUPPLIED-P)) :current-addr))
goal-namemacro
(defmacro goal-name (&optional ss-supplied-p) `(access goal (car (goals ,SS-SUPPLIED-P)) :goal-name))
depends-onmacro
(defmacro depends-on (&optional ss-supplied-p) `(access goal (car (goals ,SS-SUPPLIED-P)) :depends-on))
make-official-pc-commandmacro
(defmacro make-official-pc-command (sym) `(intern-in-package-of-symbol (symbol-name ,SYM) 'acl2-pkg-witness))
intern-in-keyword-packagefunction
(defun intern-in-keyword-package (sym) (declare (xargs :guard (symbolp sym))) (intern (symbol-name sym) "KEYWORD"))
make-pretty-pc-commandfunction
(defun make-pretty-pc-command (x) (declare (xargs :guard (symbolp x))) (intern-in-keyword-package x))
make-pretty-pc-instrfunction
(defun make-pretty-pc-instr (instr) (declare (xargs :guard (or (symbolp instr) (and (consp instr) (symbolp (car instr)))))) (if (atom instr) (make-pretty-pc-command instr) (if (null (cdr instr)) (make-pretty-pc-command (car instr)) (cons (make-pretty-pc-command (car instr)) (cdr instr)))))
change-pc-statemacro
(defmacro change-pc-state (pc-s &rest args) (list* 'change 'pc-state pc-s args))
make-official-pc-instrfunction
(defun make-official-pc-instr (instr) (if (consp instr) (if (and (symbolp (car instr)) (true-listp (cdr instr))) (cons (make-official-pc-command (car instr)) (cdr instr)) (list (make-official-pc-command 'illegal) instr)) (if (symbolp instr) (list (make-official-pc-command instr)) (if (and (integerp instr) (> instr 0)) (list (make-official-pc-command 'dv) instr) (list (make-official-pc-command 'illegal) instr)))))
check-formals-lengthfunction
(defun check-formals-length (formals args fn ctx state) (declare (xargs :guard (and (symbol-listp formals) (true-listp args)))) (let ((max-length (if (member-eq '&rest formals) 'infinity (length (remove '&optional formals)))) (min-length (let ((k (max (length (member-eq '&rest formals)) (length (member-eq '&optional formals))))) (- (length formals) k))) (n (length args))) (if (and (<= min-length n) (or (eq max-length 'infinity) (<= n max-length))) (value t) (if (equal min-length max-length) (er soft ctx "Wrong number of arguments in argument list ~x0 to ~x1. There should ~ be ~n2 argument~#3~[s~/~/s~] to ~x1." args fn min-length (zero-one-or-more min-length)) (if (equal max-length 'infinity) (er soft ctx "Wrong number of arguments in argument list ~x0 to ~x1. There should ~ be at least ~n2 argument~#3~[s~/~/s~] to ~x1." args fn min-length (min min-length 2)) (er soft ctx "Wrong number of arguments in argument list ~x0 to ~x1. There should ~ be between ~n2 and ~n3 arguments to ~x1." args fn min-length max-length))))))
check-&optional-and-&restfunction
(defun check-&optional-and-&rest (formals state) (cond ((not (true-listp formals)) (er soft 'check-&optional-and-&rest "The formals are supposed to be a true list, but they are ~x0." formals)) ((member-eq '&optional (cdr (member-eq '&optional formals))) (er soft 'check-&optional-and-&rest "The &optional keywords occurs more than once in ~x0." formals)) (t (let ((r-formals (reverse formals))) (if (or (eq (car r-formals) '&optional) (eq (car r-formals) '&rest)) (er soft 'check-&optional-and-&rest "The &optional and &rest keywords may not occur as the last element of ~ the formals list, ~x0." formals) (if (member-eq '&rest (cddr r-formals)) (er soft 'check-&optional-and-&rest "The &rest keyword may not occur except as the next-to-last ~ member of the formals list, which is not the case for ~x0." formals) (value t)))))))
make-let-pairs-from-formalsfunction
(defun make-let-pairs-from-formals (formals arg) (if (consp formals) (if (eq (car formals) '&optional) (make-let-pairs-from-formals (cdr formals) arg) (if (eq (car formals) '&rest) (list (list (cadr formals) arg)) (cons (list (car formals) (list 'car arg)) (make-let-pairs-from-formals (cdr formals) (list 'cdr arg))))) nil))
all-symbolsmutual-recursion
(mutual-recursion (defun all-symbols (form) (cond ((symbolp form) (list form)) ((atom form) nil) ((eq (car form) 'quote) nil) (t (union-eq (all-symbols (car form)) (all-symbols-list (cdr form)))))) (defun all-symbols-list (x) (if (consp x) (union-eq (all-symbols (car x)) (all-symbols-list (cdr x))) nil)))
make-access-bindingsfunction
(defun make-access-bindings (record-name record fields) (if (consp fields) (cons `(,(CAR FIELDS) (access ,RECORD-NAME ,RECORD ,(INTERN-IN-KEYWORD-PACKAGE (CAR FIELDS)))) (make-access-bindings record-name record (cdr fields))) nil))
let-form-for-pc-state-varsfunction
(defun let-form-for-pc-state-vars (form) (let ((vars (all-symbols form))) (let* ((goal-vars (intersection-eq *goal-fields* vars)) (pc-state-vars (if goal-vars (intersection-eq *pc-state-fields-for-primitives* (cons 'goals vars)) (intersection-eq *pc-state-fields-for-primitives* vars)))) `(let ,(MAKE-ACCESS-BINDINGS 'PC-STATE 'PC-STATE PC-STATE-VARS) (let ,(MAKE-ACCESS-BINDINGS 'GOAL '(CAR GOALS) GOAL-VARS) ,FORM)))))
check-field-namesfunction
(defun check-field-names (formals ctx state) (let ((bad-formals (intersection-eq formals (append *goal-fields* *pc-state-fields-for-primitives*)))) (if bad-formals (er soft ctx "It is illegal to use names of pc-state or goal fields as formals to~ define commands with ~x0, in this case ~&1." ctx bad-formals) (value t))))
print-no-changemacro
(defmacro print-no-change (&optional str alist (col '0)) `(print-no-change-fn ,STR ,ALIST ,COL state))
print-no-change2macro
(defmacro print-no-change2 (&rest args) `(pprogn ,(CONS 'PRINT-NO-CHANGE ARGS) (mv nil state)))
print-no-change-fnfunction
(defun print-no-change-fn (str alist col state) (declare (xargs :guard (or (stringp str) (null str)))) (io? proof-builder nil state (col alist str) (mv-let (col state) (let ((channel (proofs-co state))) (mv-let (col state) (fmt1 "~|*** NO CHANGE ***" nil col channel state nil) (if str (mv-let (col state) (fmt1 " -- " nil col channel state nil) (mv-let (col state) (fmt1 str alist col channel state (term-evisc-tuple nil state)) (fmt1 "~|" nil col channel state nil))) (fmt1 "~|" nil col channel state nil)))) (declare (ignore col)) state)))
maybe-update-instructionmacro
(defmacro maybe-update-instruction (instr pc-state-and-state) `(mv-let (pc-state state) ,PC-STATE-AND-STATE (mv (and pc-state (if (access pc-state pc-state :instruction) pc-state (change-pc-state pc-state :instruction (make-pretty-pc-instr ,INSTR)))) state)))
pc-primitive-defun-formfunction
(defun pc-primitive-defun-form (raw-name name formals doc body) `(defun ,NAME (args state) ,@(AND DOC (LIST DOC)) (mv-let (erp v state) (check-formals-length ',FORMALS args ',RAW-NAME ',NAME state) (declare (ignore v)) (if erp (mv nil state) (let ((pc-state (change pc-state (car (state-stack)) :instruction nil)) ,@(MAKE-LET-PAIRS-FROM-FORMALS FORMALS 'ARGS)) ,@(BUTLAST BODY 1) (maybe-update-instruction (cons ',RAW-NAME args) ,(LET-FORM-FOR-PC-STATE-VARS (CAR (LAST BODY)))))))))
pc-command-table-guardfunction
(defun pc-command-table-guard (key val wrld) (and (function-symbolp key wrld) (or (eq val 'macro) (eq val 'atomic-macro) (eq val 'meta) (and (eq val 'primitive) (global-val 'boot-strap-flg wrld)))))
other
(table pc-command-table nil nil :guard (pc-command-table-guard key val world))
add-pc-commandmacro
(defmacro add-pc-command (name command-type) `(table pc-command-table ',NAME ,COMMAND-TYPE))
pc-command-typemacro
(defmacro pc-command-type (name) `(cdr (assoc-equal ,NAME (table-alist 'pc-command-table (w state)))))
print-no-change3macro
(defmacro print-no-change3 (&optional str alist (col '0)) `(pprogn (print-no-change-fn ,STR ,ALIST ,COL state) (value nil)))
add-pc-command-1function
(defun add-pc-command-1 (name command-type state) (table-fn 'pc-command-table `(',NAME ',COMMAND-TYPE) state (list 'table 'pc-command-table (list 'quote name) (list 'quote command-type))))
toggle-pc-macro-fnfunction
(defun toggle-pc-macro-fn (name new-tp state) (let ((tp (pc-command-type name))) (if (null tp) (print-no-change3 "The command ~x0 is not a proof-builder command." (list (cons #\0 name))) (case tp (macro (if (or (null new-tp) (equal (symbol-name new-tp) "ATOMIC-MACRO")) (add-pc-command-1 name 'atomic-macro state) (if (equal (symbol-name new-tp) "MACRO") (print-no-change3 "~x0 is already a non-atomic macro." (list (cons #\0 name))) (print-no-change3 "You can't change a proof-builder macro ~ to have type ~x0." (list (cons #\0 new-tp)))))) (atomic-macro (if (or (null new-tp) (equal (symbol-name new-tp) "MACRO")) (add-pc-command-1 name 'macro state) (if (equal (symbol-name new-tp) "ATOMIC-MACRO") (print-no-change3 "~x0 is already an atomic macro." (list (cons #\0 name))) (print-no-change3 "You can't change a proof-builder atomic macro ~ to have type ~x0." (list (cons #\0 new-tp)))))) (otherwise (print-no-change3 "You can't change the type of a proof-builder ~x0 command." (list (cons #\0 tp))))))))
pc-meta-or-macro-defunfunction
(defun pc-meta-or-macro-defun (raw-name name formals doc body) `(defun ,NAME (args state) (declare (xargs :mode :program :stobjs state)) ,@(AND DOC (LIST DOC)) (er-progn (check-formals-length ',FORMALS args ',RAW-NAME ',NAME state) (let ((state-stack (state-stack)) ,@(MAKE-LET-PAIRS-FROM-FORMALS FORMALS 'ARGS)) ,@(BUTLAST BODY 1) (let ((very-silly-copy-of-state-stack state-stack)) (declare (ignore very-silly-copy-of-state-stack)) ,(CAR (LAST BODY)))))))
goal-namesfunction
(defun goal-names (goals) (if (consp goals) (cons (access goal (car goals) :goal-name) (goal-names (cdr goals))) nil))
instructions-of-state-stackfunction
(defun instructions-of-state-stack (ss acc) (if (consp ss) (instructions-of-state-stack (cdr ss) (cons (access pc-state (car ss) :instruction) acc)) (cdr acc)))
fms0macro
(defmacro fms0 (str &optional alist col (evisc-tuple 'nil evisc-tuple-p)) `(mv-let (new-col state) (fmt1 ,STR ,ALIST ,(OR COL 0) (proofs-co state) state ,(IF EVISC-TUPLE-P EVISC-TUPLE '(TERM-EVISC-TUPLE NIL STATE))) (declare (ignore new-col)) state))
with-output-forcedmacro
(defmacro with-output-forced (output-chan signature code) (cond ((or (not (true-listp signature)) (member-eq output-chan signature)) (er hard 'with-output-forced "Ill-formed call: ~x0" `(with-output-forced ,OUTPUT-CHAN ,SIGNATURE ,CODE))) (t code)))
print-pc-promptfunction
(defun print-pc-prompt (state) (io? proof-builder nil (mv col state) nil (let ((chan (proofs-co state))) (with-output-forced chan (col state) (fmt1 (pc-prompt) nil 0 chan state nil))) :default-bindings ((col 0))))
pc-macroexpandfunction
(defun pc-macroexpand (raw-instr state) (let ((instr (make-official-pc-instr raw-instr))) (if (member-eq (pc-command-type (car instr)) '(macro atomic-macro)) (er-let* ((val (xtrans-eval (list (car instr) (list 'quote (cdr instr)) 'state) nil t t 'pc-macroexpand state t))) (pc-macroexpand val state)) (value instr))))
find-goalfunction
(defun find-goal (name goals) (if (consp goals) (if (equal name (access goal (car goals) :goal-name)) (car goals) (find-goal name (cdr goals))) nil))
print-all-goals-proved-messagefunction
(defun print-all-goals-proved-message (state) (io? proof-builder nil state nil (pprogn (print-no-change "There are no unproved goals!") (if (f-get-global 'in-verify-flg state) (fms0 "You may wish to exit.~%") state))))
when-goalsmacro
(defmacro when-goals (form) `(if (goals t) ,FORM (print-all-goals-proved-message state)))
when-goals-tripmacro
(defmacro when-goals-trip (form) `(if (goals t) ,FORM (pprogn (print-all-goals-proved-message state) (value 'skip))))
current-immediate-depsfunction
(defun current-immediate-deps (goal-name goal-names) (if (consp goal-names) (if (and (consp (car goal-names)) (equal goal-name (caar goal-names))) (cons (car goal-names) (current-immediate-deps goal-name (cdr goal-names))) (current-immediate-deps goal-name (cdr goal-names))) nil))
goal-dependent-pfunction
(defun goal-dependent-p (parent name) (if (consp name) (if (equal parent (car name)) t (goal-dependent-p parent (car name))) nil))
current-all-depsfunction
(defun current-all-deps (goal-name goal-names) (if (consp goal-names) (if (goal-dependent-p goal-name (car goal-names)) (cons (car goal-names) (current-immediate-deps goal-name (cdr goal-names))) (current-immediate-deps goal-name (cdr goal-names))) nil))
maybe-print-proved-goal-messagefunction
(defun maybe-print-proved-goal-message (goal old-goals goals state) (let* ((name (access goal goal :goal-name)) (new-names (goal-names goals)) (names (set-difference-equal new-names (goal-names old-goals)))) (pprogn (if names (fms0 "~|~%Creating ~n0 new ~#1~[~/goal~/goals~]: ~&2.~%" (list (cons #\0 (length names)) (cons #\1 (zero-one-or-more (length names))) (cons #\2 names)) 0 nil) state) (if (find-goal name goals) state (let ((unproved-deps (current-all-deps name new-names))) (if unproved-deps (fms0 "~|~%The proof of the current goal, ~x0, has been ~ completed. However, the following subgoals remain ~ to be proved:~%~ ~ ~&1.~%Now proving ~x2.~%" (list (cons #\0 name) (cons #\1 unproved-deps) (cons #\2 (access goal (car goals) :goal-name))) 0 nil) (if goals (fms0 "~|~%The proof of the current goal, ~x0, has been ~ completed, as have all of its subgoals.~%Now proving ~x1.~%" (list (cons #\0 name) (cons #\1 (access goal (car goals) :goal-name))) 0 nil) (pprogn (fms0 "~|*!*!*!*!*!*!* All goals have been proved! ~ *!*!*!*!*!*!*~%") (if (f-get-global 'in-verify-flg state) (fms0 "You may wish to exit.~%") state)))))))))
accumulate-ttree-in-pc-statefunction
(defun accumulate-ttree-in-pc-state (pc-state state) (er-let* ((ttree (accumulate-ttree-and-step-limit-into-state (access pc-state pc-state :tag-tree) :skip state))) (value (change-pc-state pc-state :tag-tree ttree))))
pc-process-assumptionsfunction
(defun pc-process-assumptions (pc-ens ttree wrld state) (let ((n (count-assumptions ttree))) (pprogn (cond ((< n 101) state) (t (io? prove nil state (n) (fms "~%Note: processing ~x0 forced hypotheses which we now ~ collect)~%" (list (cons #\0 n)) (proofs-co state) state nil)))) (mv-let (n0 assns pairs ttree1) (extract-and-clausify-assumptions nil ttree nil pc-ens wrld (splitter-output)) (cond ((= n0 0) (mv nil nil ttree state)) (t (mv (strip-cdrs pairs) assns ttree1 state)))))))
make-implicationfunction
(defun make-implication (assumptions concl) (cond (assumptions (fcons-term* 'implies (conjoin assumptions) concl)) (t concl)))
cl-set-to-implicationsfunction
(defun cl-set-to-implications (cl-set) (if (null cl-set) nil (cons (make-implication (dumb-negate-lit-lst (butlast (car cl-set) 1)) (car (last (car cl-set)))) (cl-set-to-implications (cdr cl-set)))))
known-assumptionsfunction
(defun known-assumptions (type-alist assns) (cond ((null assns) nil) ((dumb-type-alist-implicationp type-alist (access assumption (car assns) :type-alist)) (cons (access assumption (car assns) :term) (known-assumptions type-alist (cdr assns)))) (t (known-assumptions type-alist (cdr assns)))))
add-assumptions-to-top-goalfunction
(defun add-assumptions-to-top-goal (goal-unproved-p known-assumptions forced-goals remaining-goals) (if forced-goals (if goal-unproved-p (cons (if known-assumptions (if forced-goals (change goal (car remaining-goals) :hyps (append (access goal (car remaining-goals) :hyps) known-assumptions) :depends-on (+ (access goal (car remaining-goals) :depends-on) (length forced-goals))) (change goal (car remaining-goals) :hyps (append (access goal (car remaining-goals) :hyps) known-assumptions))) (if forced-goals (change goal (car remaining-goals) :depends-on (+ (access goal (car remaining-goals) :depends-on) (length forced-goals))) (car remaining-goals))) (append forced-goals (cdr remaining-goals))) (append forced-goals remaining-goals)) remaining-goals))
unproved-goalsfunction
(defun unproved-goals (pc-state) (let ((goals (access pc-state pc-state :goals))) (if (and goals (equal (access goal (car goals) :conc) *t*)) (cdr goals) goals)))
initial-rcnst-from-ensfunction
(defun initial-rcnst-from-ens (ens wrld state splitter-output) (make-rcnst ens wrld state :splitter-output splitter-output :force-info t))
make-new-goals-fixed-hypsfunction
(defun make-new-goals-fixed-hyps (termlist hyps goal-name start-index) (if (consp termlist) (cons (make goal :conc (car termlist) :hyps hyps :current-addr nil :goal-name (cons goal-name start-index) :depends-on 1) (make-new-goals-fixed-hyps (cdr termlist) hyps goal-name (1+ start-index))) nil))
pc-single-step-primitivefunction
(defun pc-single-step-primitive (instr state) (state-global-let* ((guard-checking-on nil)) (let* ((goals (goals)) (wrld (w state)) (old-tag-tree (tag-tree))) (cond ((null goals) (pprogn (print-all-goals-proved-message state) (mv nil nil state))) (t (mv-let (erp stobjs-out/vals state) (trans-eval-default-warning (list (car instr) (list 'quote (cdr instr)) 'state) 'pc-single-step state t) (let ((vals (cdr stobjs-out/vals))) (cond (erp (pprogn (print-no-change "An error occurred in executing ~X01." (list (cons #\0 instr) (cons #\1 (abbrev-evisc-tuple state)))) (mv 'pc-single-step-error-primitive nil state))) (t (assert$ (equal (car stobjs-out/vals) '(nil state)) (cond ((car vals) (let ((pc-ens (make-pc-ens (pc-ens) state))) (mv-let (step-limit bad-ass ttree) (resume-suspended-assumption-rewriting (access pc-state (car vals) :local-tag-tree) nil nil nil (initial-rcnst-from-ens pc-ens wrld state (splitter-output)) wrld state (initial-step-limit wrld state)) (declare (ignore step-limit)) (cond (bad-ass (pprogn (let ((assumnote (car (access assumption bad-ass :assumnotes)))) (print-no-change "When applying the rune ~x0 to the target ~x1, a ~ hypothesis of the form (~x2 ...) or (~x3 ...) was ~ later found to be false." (list (cons #\0 (access assumnote assumnote :rune)) (cons #\1 (access assumnote assumnote :target)) (cons #\2 'force) (cons #\3 'case-split)))) (mv nil nil state))) (t (let* ((returned-pc-state (car vals)) (remaining-goals (unproved-goals returned-pc-state)) (goal-name (goal-name)) (goal-unproved-p (and remaining-goals (equal goal-name (access goal (car remaining-goals) :goal-name)))) (hyps (hyps)) (returned-goal (let* ((goals (access pc-state returned-pc-state :goals))) (and goals (equal goal-name (access goal (car goals) :goal-name)) (car goals)))) (depends-on (cond (returned-goal (access goal returned-goal :depends-on)) (t (depends-on))))) (mv-let (cl-set assns ttree state) (pc-process-assumptions pc-ens ttree wrld state) (mv-let (contradictionp hyps-type-alist ttree0) (cond ((and assns goal-unproved-p) (type-alist-clause (dumb-negate-lit-lst hyps) nil nil nil pc-ens wrld nil nil)) (t (mv nil nil nil))) (cond (contradictionp (er-let* ((new-pc-state (let ((local-ttree (cons-tag-trees ttree ttree0))) (accumulate-ttree-in-pc-state (change-pc-state (car vals) :goals (cdr goals) :tag-tree (cons-tag-trees local-ttree old-tag-tree) :local-tag-tree local-ttree) state)))) (pprogn (io? proof-builder nil state (instr goal-name) (fms0 "~|AHA! A contradiction has ~ been discovered in the ~ hypotheses of goal ~x0 in the ~ course of executing ~ instruction ~x1, in the ~ process of preparing to deal ~ with forced assumptions.~|" (list (cons #\0 goal-name) (cons #\1 instr)) 0 nil)) (io? proof-builder nil state (goals) (maybe-print-proved-goal-message (car goals) goals (cdr goals) state)) (pc-assign state-stack (cons new-pc-state (state-stack))) (value new-pc-state)))) (t (let* ((termlist (cl-set-to-implications cl-set)) (forced-goals (make-new-goals-fixed-hyps termlist hyps goal-name depends-on)) (new-goals (add-assumptions-to-top-goal goal-unproved-p (known-assumptions hyps-type-alist assns) forced-goals remaining-goals)) (pc-state-1 (change-pc-state (car vals) :goals new-goals :tag-tree (cons-tag-trees ttree old-tag-tree) :local-tag-tree ttree))) (er-let* ((new-pc-state (accumulate-ttree-in-pc-state pc-state-1 state))) (pprogn (cond (forced-goals (io? proof-builder nil state (forced-goals) (fms0 "~|~%NOTE (forcing): Creating ~ ~n0 new ~#1~[~/goal~/goals~] ~ due to FORCE or CASE-SPLIT ~ hypotheses of rules.~%" (list (cons #\0 (length forced-goals)) (cons #\1 (zero-one-or-more (length forced-goals))))))) (t state)) (io? proof-builder nil state (new-goals goals) (maybe-print-proved-goal-message (car goals) goals new-goals state)) (pc-assign state-stack (cons new-pc-state (state-stack))) (value new-pc-state)))))))))))))) (t (mv nil nil state)))))))))))))
maybe-print-macroexpansionfunction
(defun maybe-print-macroexpansion (instr raw-instr state) (let ((pc-print-macroexpansion-flg (pc-print-macroexpansion-flg))) (if (and pc-print-macroexpansion-flg (not (eq (car instr) (make-official-pc-command 'lisp))) (not (equal instr (make-official-pc-instr raw-instr)))) (io? proof-builder nil state (pc-print-macroexpansion-flg instr) (fms0 ">> ~x0~|" (list (cons #\0 instr)) 0 (if (and (consp pc-print-macroexpansion-flg) (integerp (car pc-print-macroexpansion-flg)) (integerp (cdr pc-print-macroexpansion-flg)) (> (car pc-print-macroexpansion-flg) 0) (> (cdr pc-print-macroexpansion-flg) 0)) (evisc-tuple (car pc-print-macroexpansion-flg) (cdr pc-print-macroexpansion-flg) nil nil) nil))) state)))
pc-single-step-1function
(defun pc-single-step-1 (raw-instr state) (mv-let (erp instr state) (pc-macroexpand raw-instr state) (if erp (pprogn (io? proof-builder nil state (raw-instr) (fms0 "~%Macroexpansion of instruction ~x0 failed!~%" (list (cons #\0 raw-instr)))) (mv erp nil state)) (case (pc-command-type (car instr)) (primitive (pprogn (maybe-print-macroexpansion instr raw-instr state) (pc-single-step-primitive instr state))) (meta (cond ((and (not (f-get-global 'in-verify-flg state)) (not (getpropc (car instr) 'predefined nil (w state)))) (er soft 'proof-builder "You may only invoke a user-defined proof-builder meta ~ command, such as ~x0, when you are inside the ~ interactive ~x1 loop." (car instr) 'verify)) (t (pprogn (maybe-print-macroexpansion instr raw-instr state) (mv-let (erp stobjs-out/vals state) (trans-eval-default-warning (list (car instr) (list 'quote (cdr instr)) 'state) 'pc-single-step state t) (assert$ (equal (car stobjs-out/vals) *error-triple-sig*) (if erp (pprogn (print-no-change "Very odd -- an error ~ occurred in executing ~x0." (list (cons #\0 instr))) (mv 'pc-single-step-error-meta nil state)) (let ((vals (cdr stobjs-out/vals))) (mv (car vals) (cadr vals) state))))))))) ((macro atomic-macro) (value (er hard 'pc-single-step "Encountered instruction ~x0 whose pc-macroexpansion ~ produced ~x1, which is headed by a macro command!" raw-instr instr))) (otherwise (pprogn (print-no-change "Undefined instruction, ~x0." (list (cons #\0 (make-pretty-pc-instr instr)))) (value nil)))))))
union-lastn-pc-tag-treesfunction
(defun union-lastn-pc-tag-trees (n ss acc) (if (zp n) acc (union-lastn-pc-tag-trees (1- n) (cdr ss) (cons-tag-trees (access pc-state (car ss) :local-tag-tree) acc))))
pc-single-stepfunction
(defun pc-single-step (raw-instr state) (declare (xargs :guard (consp raw-instr))) (let ((tp (pc-command-type (car raw-instr)))) (if (eq tp 'atomic-macro) (let* ((saved-ss (state-stack)) (old-len (length saved-ss))) (mv-let (erp val state) (pc-single-step-1 raw-instr state) (let* ((new-ss (state-stack)) (new-len (length new-ss)) (diff (- new-len old-len))) (if (and (< old-len new-len) (equal saved-ss (nthcdr diff new-ss))) (pprogn (pc-assign state-stack (cons (change pc-state (car new-ss) :instruction (make-pretty-pc-instr raw-instr) :local-tag-tree (union-lastn-pc-tag-trees diff new-ss nil)) saved-ss)) (mv erp val state)) (mv erp val state))))) (pc-single-step-1 raw-instr state))))
*pc-complete-signal*constant
(defconst *pc-complete-signal* 'acl2-pc-complete)
print-re-entering-proof-builderfunction
(defun print-re-entering-proof-builder (eof-p state) (io? proof-builder nil state (eof-p) (fms0 "~|~%~ /-----------------------------------------------------------\~%~ | Note: Re-entering the proof-builder after ~s0 |~%~ | Submit EXIT if you want to exit the proof-builder. |~%~ \-----------------------------------------------------------/~%" (list (cons #\0 (cond (eof-p "end of file. ") (t "error or abort.")))))))
chk-absstobj-invariantsfunction
(defun chk-absstobj-invariants (state) (declare (xargs :stobjs state)) (mv-let (erp msg state) (read-acl2-oracle state) (declare (ignore erp)) (cond (msg (pprogn (f-put-global 'illegal-to-certify-message msg state) (f-put-global 'ld-pre-eval-filter :illegal-state state) (error-fms nil 'chk-absstobj-invariants nil "~@0" (list (cons #\0 msg)) state))) (t state))))
pc-main-loopfunction
(defun pc-main-loop (instr-list quit-conditions last-value pc-print-prompt-and-instr-flg state) (cond ((null instr-list) (mv nil last-value state)) (t (pprogn (chk-absstobj-invariants state) (cond ((illegal-state-p state) (mv t nil state)) (t (mv-let (col state) (if pc-print-prompt-and-instr-flg (print-pc-prompt state) (mv 0 state)) (mv-let (erp instr state) (if (consp instr-list) (pprogn (if pc-print-prompt-and-instr-flg (io? proof-builder nil state (col instr-list) (fms0 "~y0~|" (list (cons #\0 (car instr-list))) col)) state) (value (car instr-list))) (read-object instr-list state)) (cond (erp (pprogn (print-re-entering-proof-builder t state) (pc-main-loop instr-list quit-conditions last-value pc-print-prompt-and-instr-flg state))) (t (mv-let (signal val state) (pc-single-step (make-official-pc-instr instr) state) (cond ((or (and signal (or (member-eq 'signal quit-conditions) (and (eq signal *pc-complete-signal*) (member-eq 'exit quit-conditions)))) (and (null val) (member-eq 'value quit-conditions))) (mv signal val state)) (t (let ((new-last-value (and last-value (null signal) val))) (pc-main-loop (if (consp instr-list) (cdr instr-list) instr-list) quit-conditions new-last-value pc-print-prompt-and-instr-flg state)))))))))))))))
make-initial-goalfunction
(defun make-initial-goal (term) (make goal :conc term :hyps nil :current-addr nil :goal-name 'main :depends-on 1))
initial-state-stackfunction
(defun initial-state-stack (term raw-term event-name rule-classes pc-ens) (list (make pc-state :instruction (list :start (list event-name rule-classes raw-term)) :goals (list (make-initial-goal term)) :local-tag-tree nil :tag-tree nil :abbreviations nil :pc-ens pc-ens)))
event-name-and-types-and-raw-termfunction
(defun event-name-and-types-and-raw-term (state-stack) (cadr (access pc-state (car (last state-stack)) :instruction)))
install-initial-state-stackmacro
(defmacro install-initial-state-stack (term raw-term event-name rule-classes) `(pprogn (pc-assign state-stack (initial-state-stack ,TERM ,RAW-TERM ,EVENT-NAME ,RULE-CLASSES nil)) (pc-assign old-ss nil)))
pc-main1function
(defun pc-main1 (instr-list quit-conditions pc-print-prompt-and-instr-flg state) (with-prover-step-limit! :start (pc-main-loop instr-list quit-conditions t pc-print-prompt-and-instr-flg state)))
pc-mainfunction
(defun pc-main (term raw-term event-name rule-classes instr-list quit-conditions pc-print-prompt-and-instr-flg in-verify-flg state) (pprogn (install-initial-state-stack term raw-term event-name rule-classes) (cond (in-verify-flg (f-put-global 'in-verify-flg in-verify-flg state)) (t state)) (pc-main1 instr-list quit-conditions pc-print-prompt-and-instr-flg state)))
pc-topfunction
(defun pc-top (raw-term event-name rule-classes instr-list quit-conditions in-verify-flg state) (declare (xargs :guard (symbolp event-name))) (mv-let (erp term state) (translate raw-term t t t 'pc-top (w state) state) (if erp (mv t nil state) (pc-main term raw-term event-name rule-classes instr-list quit-conditions t in-verify-flg state))))
illegal-fnpmutual-recursion
(mutual-recursion (defun illegal-fnp (x w) (cond ((atom x) nil) ((eq (car x) 'quote) nil) ((symbolp (car x)) (let ((arity (arity (car x) w))) (if (and arity (eql (length (cdr x)) arity)) (illegal-fnp-list (cdr x) w) (car x)))) ((consp (car x)) (illegal-fnp-list (cdr x) w)) (t nil))) (defun illegal-fnp-list (x w) (cond ((endp x) nil) (t (or (illegal-fnp (car x) w) (illegal-fnp-list (cdr x) w))))))
verify-fnfunction
(defun verify-fn (raw-term raw-term-supplied-p event-name rule-classes instructions state) (cond ((f-get-global 'in-verify-flg state) (er soft 'verify "You are apparently already inside the VERIFY interactive loop. It ~ is illegal to enter such a loop recursively.")) (t (let ((ld-level (f-get-global 'ld-level state))) (mv-let (erp val state) (cond (raw-term-supplied-p (state-global-let* ((print-base 10) (print-radix nil) (inhibit-output-lst (remove1-eq 'proof-builder (f-get-global 'inhibit-output-lst state)))) (pc-top raw-term event-name rule-classes (append instructions *standard-oi*) (list 'exit) ld-level state))) ((null (state-stack)) (er soft 'verify "There is no interactive verification to re-enter!")) (t (let ((bad-fn (illegal-fnp (access goal (car (access pc-state (car (last (state-stack))) :goals)) :conc) (w state)))) (cond (bad-fn (er soft 'verify "The current proof-builder session was begun in an ACL2 world ~ with function symbol ~x0, but that function symbol no longer ~ exists." bad-fn)) (t (state-global-let* ((print-base 10) (print-radix nil) (inhibit-output-lst (remove1-eq 'proof-builder (f-get-global 'inhibit-output-lst state)))) (pprogn (f-put-global 'in-verify-flg ld-level state) (pc-main1 (append instructions *standard-oi*) (list 'exit) t state)))))))) (cond ((equal erp *pc-complete-signal*) (pprogn (f-put-global 'in-verify-flg nil state) (value val))) (t (mv erp val state))))))))
print-unproved-goals-messagefunction
(defun print-unproved-goals-message (goals state) (io? proof-builder nil state (goals) (fms0 "~%There ~#0~[is~/are~] ~x1 unproved goal~#0~[~/s~] from replay ~ of instructions. To enter the proof-builder state that exists ~ at this point, type (VERIFY).~%" (list (cons #\0 goals) (cons #\1 (length goals))))))
state-stack-from-instructionsfunction
(defun state-stack-from-instructions (raw-term event-name rule-classes instructions replay-flg quit-conditions state) (if replay-flg (pprogn (io? proof-builder nil state nil (fms0 "~|~%Entering the proof-builder....~%~%")) (er-progn (pc-top raw-term event-name rule-classes instructions quit-conditions nil state) (value (state-stack)))) (value (state-stack))))
state-from-instructionsfunction
(defun state-from-instructions (raw-term event-name rule-classes instructions quit-conditions state) (mv-let (erp val state) (pc-top raw-term event-name rule-classes instructions quit-conditions nil state) (declare (ignore erp val)) state))
print-pc-defthmfunction
(defun print-pc-defthm (ev state) (io? proof-builder nil state (ev) (fms0 "~|~Y01" (list (cons #\0 ev) (cons #\1 (ld-evisc-tuple state))))))
print-pc-goalmacro
(defmacro print-pc-goal (&optional goal) `(let ((goal ,(OR GOAL '(CAR (ACCESS PC-STATE (CAR (STATE-STACK)) :GOALS))))) (io? proof-builder nil state (goal) (if goal (fms0 "~%------- ~x3 -------~|~ Conc: ~q0~|~ Hyps: ~q1~|~ Addr: ~Y2n~|~ Deps: ~Y4n~|" (list (cons #\0 (untranslate (access goal goal :conc) t (w state))) (cons #\1 (let ((hyps (access goal goal :hyps))) (cond ((null hyps) t) ((null (cdr hyps)) (untranslate (car hyps) t (w state))) (t (cons 'and (untranslate-lst hyps t (w state))))))) (cons #\2 (access goal goal :current-addr)) (cons #\3 (access goal goal :goal-name)) (cons #\4 (access goal goal :depends-on)) (cons #\n nil))) (fms0 "~%No goal in CAR of state-stack.~|")))))
print-pc-statemacro
(defmacro print-pc-state (&optional pc-state) `(let ((pc-state ,(OR PC-STATE '(CAR (STATE-STACK))))) (io? proof-builder nil state (pc-state) (if pc-state (fms0 "~%Instr: ~y0~|~ Goals: ~y1~|~ Abbrs: ~y2~|~ Local ttree: ~y3~|~ Ttree: ~y4~|" (list (cons #\0 (access pc-state pc-state :instruction)) (cons #\1 (access pc-state pc-state :goals)) (cons #\2 (access pc-state pc-state :abbreviations)) (cons #\3 (access pc-state pc-state :local-tag-tree)) (cons #\4 (access pc-state pc-state :tag-tree)))) (fms0 "~%No state in CAR of state-stack.~|")))))
proof-builderfunction
(defun proof-builder (event-name raw-term term rule-classes instructions wrld state) (declare (ignore term wrld)) (cond ((and (not (f-get-global 'in-verify-flg state)) (ld-skip-proofsp state)) (value nil)) (t (mv-let (erp state-stack state) (state-stack-from-instructions raw-term event-name rule-classes instructions (not (f-get-global 'in-verify-flg state)) '(signal value) state) (if erp (pprogn (io? proof-builder nil state nil (fms0 "~%~%Replay of proof-builder instructions ~ aborted.~%")) (if (f-get-global 'in-verify-flg state) (mv *pc-complete-signal* nil state) (silent-error state))) (let ((goals (access pc-state (car state-stack) :goals))) (if (null goals) (value (access pc-state (car state-stack) :tag-tree)) (pprogn (print-unproved-goals-message goals state) (if (f-get-global 'in-verify-flg state) (mv *pc-complete-signal* nil state) (silent-error state))))))))))
verifymacro
(defmacro verify (&optional (raw-term 'nil raw-term-supplied-p) &key event-name (rule-classes '(:rewrite)) instructions) (declare (xargs :guard (symbolp event-name))) (if (and raw-term-supplied-p (eq raw-term nil)) '(pprogn (io? proof-builder nil state nil (fms0 "It is not permitted to enter the interactive proof-builder ~ with a goal of NIL! If you really MEANT to do such a ~ thing, (VERIFY 'NIL).~%")) (value :invisible)) `(verify-fn ',RAW-TERM ',RAW-TERM-SUPPLIED-P ',EVENT-NAME ',RULE-CLASSES ',INSTRUCTIONS state)))
other
(set-guard-msg verify (let ((name (cadr (assoc-keyword :event-name (cdr args))))) (msg "The :event-name argument for VERIFY must be a symbol, ~ unlike ~x0.~@1" name (if (and (consp name) (eq (car name) 'quote) (cdr name) (symbolp (cadr name)) (null (cddr name))) (msg " Perhaps you intended the :EVENT-NAME to be ~ ~x0 instead of ~x1." (cadr name) name) ""))))
sublis-expr-non-quotepsmutual-recursion
(mutual-recursion (defun sublis-expr-non-quoteps (alist term) (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) term (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)))))))
invert-abbreviations-alistfunction
(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)))))
abbreviatefunction
(defun abbreviate (term abbreviations) (if (null abbreviations) term (sublis-expr-non-quoteps (invert-abbreviations-alist abbreviations) term)))
untrans0macro
(defmacro untrans0 (term &optional iff-flg abbreviations) `(untranslate (abbreviate ,TERM ,ABBREVIATIONS) ,IFF-FLG (w state)))
untrans0-lst-fnfunction
(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))
untrans0-lstmacro
(defmacro untrans0-lst (termlist &optional iff-flg abbreviations) `(untrans0-lst-fn ,TERMLIST ,IFF-FLG ,ABBREVIATIONS state))