other
(in-package "GL")
other
(include-book "gl-util")
other
(define nat-nat-alistp (x) (if (atom x) (eq x nil) (and (consp (car x)) (natp (caar x)) (natp (cdar x)) (nat-nat-alistp (cdr x)))) /// (defthm nat-nat-alistp-of-cons (equal (nat-nat-alistp (cons a b)) (and (nat-nat-alistp b) (consp a) (natp (car a)) (natp (cdr a))))) (defthmd nat-nat-alistp-when-consp (implies (consp x) (equal (nat-nat-alistp x) (and (consp (car x)) (natp (caar x)) (natp (cdar x)) (nat-nat-alistp (cdr x)))))))
other
(defstobj interp-profiler (prof-enabledp :type (satisfies booleanp)) (prof-indextable) (prof-totalcount :type (integer 0 *) :initially 0) (prof-nextindex :type (integer 0 *) :initially 0) (prof-array :type (array (unsigned-byte 32) (0)) :initially 0 :resizable t) (prof-stack :type (satisfies nat-nat-alistp)))
other
(defstobj interp-st is-obligs is-constraint is-constraint-db is-add-bvars-allowed (is-backchain-limit :type (or (integer 0 *) null)) (is-prof :type interp-profiler))
other
(define backchain-limit-decrement ((limit (or (natp limit) (not limit)))) :returns (mv (old-limit (or (natp old-limit) (not old-limit)) :rule-classes :type-prescription) (new-limit (or (natp new-limit) (not new-limit)) :rule-classes :type-prescription)) (b* ((limit (mbe :logic (and limit (nfix limit)) :exec limit))) (mv limit (if (and limit (not (eql 0 limit))) (+ -1 limit) limit))))
other
(define is-decrement-backchain-limit (interp-st) :returns (mv (old-limit (or (natp old-limit) (equal old-limit nil)) :rule-classes :type-prescription) (new-interp-st)) :enabled t (b* ((limit (is-backchain-limit interp-st)) ((mv old-limit new-limit) (backchain-limit-decrement limit)) (interp-st (update-is-backchain-limit new-limit interp-st))) (mv old-limit interp-st)))
other
(defconst *glcp-common-inputs* '(pathcond clk config interp-st bvar-db state))
other
(defconst *glcp-common-guards* '((interp-defs-alistp (is-obligs interp-st)) (glcp-config-p config) (interp-defs-alistp (glcp-config->overrides config))))
other
(defconst *glcp-stobjs* '(pathcond interp-st bvar-db state))
glcp-valuemacro
(defmacro glcp-value (&rest results) `(mv ,@GL::RESULTS nil ,@(CDR GL::*GLCP-COMMON-RETVALS*)))
glcp-value-nopathcondmacro
(defmacro glcp-value-nopathcond (&rest results) `(mv ,@GL::RESULTS nil ,@(CDDR GL::*GLCP-COMMON-RETVALS*)))
glcp-interp-error-tracefunction
(defun glcp-interp-error-trace (msg) (declare (ignore msg) (xargs :guard t)) nil)
break-on-glcp-errormacro
(defmacro break-on-glcp-error (flg) (if flg '(trace$ (glcp-interp-error-trace :entry (progn$ (cw "GLCP interpreter error:~%~@0~%" msg) (break$)))) '(untrace$ glcp-interp-error-trace)))
glcp-interp-abortmacro
(defmacro glcp-interp-abort (msg &key (nvals '1)) `(mv ,@(GL::MAKE-LIST-AC GL::NVALS NIL NIL) ,GL::MSG ,@(CDR GL::*GLCP-COMMON-RETVALS*)))
other
(defund glcp-interp-sanitize-error (err) (declare (xargs :guard t)) (if (eq err :unreachable) "Unreachable error from a strange source" err))
other
(defthm glcp-interp-sanitize-under-iff (iff (glcp-interp-sanitize-error err) err) :hints (("Goal" :in-theory (enable glcp-interp-sanitize-error))))
other
(defthm glcp-interp-sanitize-not-unreachable (not (equal (glcp-interp-sanitize-error err) :unreachable)) :hints (("Goal" :in-theory (enable glcp-interp-sanitize-error))))
glcp-interp-errormacro
(defmacro glcp-interp-error (msg &key (nvals '1)) (declare (xargs :guard t)) `(let ((msg (glcp-interp-sanitize-error ,GL::MSG))) (progn$ (glcp-interp-error-trace msg) (glcp-interp-abort msg :nvals ,GL::NVALS))))
patbind-glcp-specialmacro
(defmacro patbind-glcp-special (args bindings expr) `(b* (((mv ,@(CDR GL::ARGS) ,(CAR GL::ARGS) ,@(CDR GL::*GLCP-COMMON-RETVALS*)) ,(CAR GL::BINDINGS))) ,GL::EXPR))
patbind-glcp-ermacro
(defmacro patbind-glcp-er (args bindings expr) (b* ((nvalsp (member :nvals args)) (nvals (or (cadr nvalsp) 1)) (args (take (- (len args) (len nvalsp)) args))) `(b* (((mv ,@GL::ARGS patbind-glcp-er-error ,@(CDR GL::*GLCP-COMMON-RETVALS*)) ,(CAR GL::BINDINGS)) ((when patbind-glcp-er-error) (glcp-interp-abort patbind-glcp-er-error :nvals ,GL::NVALS))) (check-vars-not-free (patbind-glcp-er-error) ,GL::EXPR))))
glcp-run-branchmacro
(defmacro glcp-run-branch (branchcond expr) `(b* ((branchcond (bfr-constr-mode-fix ,GL::BRANCHCOND (is-constraint interp-st))) ((mv contra pathcond undo) (bfr-assume branchcond pathcond)) ((when contra) (b* ((pathcond (bfr-unassume pathcond undo))) (glcp-value t nil))) ((glcp-special err retval) ,GL::EXPR) (pathcond (bfr-unassume pathcond undo)) ((when err) (if (eq err :unreachable) (glcp-value t nil) (glcp-interp-abort err :nvals 2)))) (glcp-value nil retval)))
other
(defund glcp-non-branch-err-p (err) (declare (xargs :guard t)) (and err (not (eq err :branch-unreachable))))
cpathcondmacro
(defmacro cpathcond nil '(bfr-and (bfr-hyp->bfr pathcond) (bfr-constr-mode->bfr (is-constraint interp-st))))
glcp-put-name-eachfunction
(defun glcp-put-name-each (name lst) (if (atom lst) nil (cons (incat name (symbol-name name) "-" (symbol-name (car lst))) (glcp-put-name-each name (cdr lst)))))
other
(mutual-recursion (defun event-forms-collect-fn-names (x) (if (atom x) nil (append (event-form-collect-fn-names (car x)) (event-forms-collect-fn-names (cdr x))))) (defun event-form-collect-fn-names (x) (case (car x) ((defun defund) (list (cadr x))) ((mutual-recursion progn) (event-forms-collect-fn-names (cdr x))))))
other
(defund glcp-term-obj-p (x) (declare (xargs :guard t)) (and (consp x) (let* ((tag (car x))) (or (eq tag :g-apply) (eq tag :g-var)))))
other
(defconst *glcp-interp-template* `(progn (mutual-recursion (defun interp-test (x alist . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 12 0 0) :verify-guards nil :guard (and (posp clk) (pseudo-termp x) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* ((clk (1- clk)) ((glcp-er xobj) (interp-term-equivs x alist '(iff) . ,GL::*GLCP-COMMON-INPUTS*))) (simplify-if-test xobj . ,GL::*GLCP-COMMON-INPUTS*))) (defun interp-term-equivs (x alist contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list clk 2020 (acl2-count x) 40) :guard (and (natp clk) (pseudo-termp x) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((when (zp clk)) (glcp-interp-error "The clock ran out.")) ((glcp-er xobj) (interp-term x alist contexts . ,GL::*GLCP-COMMON-INPUTS*)) ((unless (glcp-term-obj-p xobj)) (glcp-value xobj)) ((mv er xobj) (try-equivalences-loop xobj pathcond contexts clk (glcp-config->param-bfr config) bvar-db state)) ((when er) (glcp-interp-error er))) (glcp-value xobj))) (defun interp-term (x alist contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 2020 (acl2-count x) 20) :well-founded-relation nat-list-< :hints (("goal" :in-theory (e/d** ((:rules-of-class :executable-counterpart :here) open-nat-list-< len nfix fix acl2-count-of-cons-greater acl2-count-of-sum acl2-count-of-general-consp-car acl2-count-of-general-consp-cdr car-cons cdr-cons commutativity-of-+ unicity-of-0 null atom eq acl2-count-last-cdr-when-cadr-hack car-cdr-elim natp-compound-recognizer zp-compound-recognizer posp-compound-recognizer pos-fix g-ite-depth-sum-of-gl-args-split-ite-then g-ite-depth-sum-of-gl-args-split-ite-else g-ite->test-acl2-count-decr g-ite->then-acl2-count-decr g-ite->else-acl2-count-decr g-apply->args-acl2-count-thm acl2-count-of-car-g-apply->args acl2-count-of-cadr-g-apply->args (:type-prescription acl2-count) (:type-prescription g-ite-depth-sum) (:t len)) ((tau-system))))) :verify-guards nil :guard (and (posp clk) (pseudo-termp x) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((when (null x)) (glcp-value nil)) ((when (symbolp x)) (glcp-value (cdr (hons-assoc-equal x alist)))) ((when (atom x)) (glcp-interp-error (msg "GLCP: The unquoted atom ~x0 is not a term~%" x))) ((when (eq (car x) 'quote)) (glcp-value (g-concrete-quote (car (cdr x))))) ((when (consp (car x))) (b* (((glcp-er actuals) (interp-list (cdr x) alist . ,GL::*GLCP-COMMON-INPUTS*)) (formals (car (cdar x))) (body (car (cdr (cdar x))))) (if (and (mbt (and (equal (len actuals) (len formals)) (symbol-listp formals))) (fast-no-duplicatesp formals) (not (member-eq nil formals))) (interp-term body (pairlis$ formals actuals) contexts . ,GL::*GLCP-COMMON-INPUTS*) (glcp-interp-error (msg "Badly formed lambda application: ~x0~%" x))))) ((when (eq (car x) 'if)) (let ((test (car (cdr x))) (tbr (car (cdr (cdr x)))) (fbr (car (cdr (cdr (cdr x)))))) (interp-if/or test tbr fbr x alist contexts . ,GL::*GLCP-COMMON-INPUTS*))) ((when (eq (car x) 'gl-aside)) (if (eql (len x) 2) (prog2$ (gl-aside-wormhole (cadr x) alist) (glcp-value nil)) (glcp-interp-error "Error: wrong number of args to GL-ASIDE~%"))) ((when (eq (car x) 'gl-ignore)) (glcp-value nil)) ((when (eq (car x) 'gl-hide)) (glcp-value (gl-term-to-apply-obj x alist))) ((when (eq (car x) 'gl-error)) (if (eql (len x) 2) (b* (((glcp-er result) (interp-term (cadr x) alist nil . ,GL::*GLCP-COMMON-INPUTS*)) (state (f-put-global 'gl-error-result result state))) (glcp-interp-error (msg "Error: GL-ERROR call encountered. Data associated with the ~ error is accessible using (@ ~x0).~%" 'gl-error-result))) (glcp-interp-error "Error: wrong number of args to GL-ERROR~%"))) ((when (eq (car x) 'return-last)) (if (eql (len x) 4) (if (equal (cadr x) ''time$1-raw) (b* (((mv time$-args err ,@(CDR GL::*GLCP-COMMON-RETVALS*)) (let ((clk (1- clk))) (interp-term-equivs (caddr x) alist nil . ,GL::*GLCP-COMMON-INPUTS*)))) (mbe :logic (interp-term (car (last x)) alist contexts . ,GL::*GLCP-COMMON-INPUTS*) :exec (if (and (not err) (general-concretep time$-args)) (return-last 'time$1-raw (general-concrete-obj time$-args) (interp-term (car (last x)) alist contexts . ,GL::*GLCP-COMMON-INPUTS*)) (time$ (interp-term (car (last x)) alist contexts . ,GL::*GLCP-COMMON-INPUTS*))))) (interp-term (car (last x)) alist contexts . ,GL::*GLCP-COMMON-INPUTS*)) (glcp-interp-error "Error: wrong number of args to RETURN-LAST~%"))) (fn (car x)) ((glcp-er actuals) (interp-list (cdr x) alist . ,GL::*GLCP-COMMON-INPUTS*))) (interp-fncall fn actuals x contexts . ,GL::*GLCP-COMMON-INPUTS*))) (defun interp-fncall (fn actuals x contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 1414 0 20) :guard (and (posp clk) (symbolp fn) (not (eq fn 'quote)) (true-listp actuals) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* ((pathcond (lbfr-hyp-fix pathcond)) (uninterp (cdr (hons-assoc-equal fn (table-alist 'gl-uninterpreted-functions (w state))))) ((mv fncall-failed ans) (if (and (or (not uninterp) (eq uninterp :concrete-only)) (general-concrete-listp actuals)) (magic-ev-fncall-logic fn (general-concrete-obj-list actuals) state) (mv t nil))) ((unless fncall-failed) (b* ((interp-st (is-prof-simple-increment-exec fn interp-st))) (glcp-value (mk-g-concrete ans)))) ((glcp-er successp term bindings) (rewrite fn actuals :fncall contexts . ,GL::*GLCP-COMMON-INPUTS*)) ((when successp) (b* ((clk (1- clk))) (interp-term-equivs term bindings contexts . ,GL::*GLCP-COMMON-INPUTS*))) ((mv ok ans pathcond) (run-gified fn actuals pathcond clk config bvar-db state)) ((when ok) (b* ((interp-st (is-prof-simple-increment-g fn interp-st))) (glcp-value ans))) ((when (and uninterp (not (eq uninterp :no-concrete)))) (glcp-value (g-apply fn actuals))) ((mv erp body formals obligs1) (interp-function-lookup fn (is-obligs interp-st) (glcp-config->overrides config) (w state))) ((when erp) (glcp-value (g-apply fn actuals))) (interp-st (update-is-obligs obligs1 interp-st)) ((unless (equal (len formals) (len actuals))) (glcp-interp-error (msg "~ In the function call ~x0, function ~x1 is given ~x2 arguments, but its arity is ~x3. Its formal parameters are ~x4." x fn (len actuals) (len formals) formals))) (clk (1- clk)) (interp-st (is-prof-push `(:d ,GL::FN) interp-st)) ((glcp-er xobj) (interp-term-equivs body (pairlis$ formals actuals) contexts . ,GL::*GLCP-COMMON-INPUTS*)) (interp-st (is-prof-pop-increment t interp-st))) (glcp-value xobj))) (defun interp-if/or (test tbr fbr x alist contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 2020 (+ (acl2-count test) (acl2-count tbr) (acl2-count fbr)) 60) :verify-guards nil :guard (and (posp clk) (pseudo-termp test) (pseudo-termp tbr) (pseudo-termp fbr) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (if (hqual test tbr) (interp-or test fbr x alist contexts . ,GL::*GLCP-COMMON-INPUTS*) (interp-if test tbr fbr x alist contexts . ,GL::*GLCP-COMMON-INPUTS*))) (defun maybe-interp (x alist contexts branchcond . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 2020 (acl2-count x) 45) :verify-guards nil :guard (and (natp clk) (pseudo-termp x) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (glcp-run-branch branchcond (interp-term-equivs x alist contexts . ,GL::*GLCP-COMMON-INPUTS*))) (defun interp-or (test fbr x alist contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 2020 (+ (acl2-count test) (acl2-count fbr)) 50) :verify-guards nil :guard (and (posp clk) (pseudo-termp test) (pseudo-termp fbr) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* (((glcp-er test-obj) (interp-term-equivs test alist (glcp-or-test-contexts contexts) . ,GL::*GLCP-COMMON-INPUTS*)) ((glcp-er test-bfr) (simplify-if-test test-obj . ,GL::*GLCP-COMMON-INPUTS*)) ((glcp-er else-unreach else) (maybe-interp fbr alist contexts (bfr-not test-bfr) . ,GL::*GLCP-COMMON-INPUTS*)) ((when else-unreach) (glcp-value test-obj))) (merge-branches test-bfr test-obj else x nil contexts . ,GL::*GLCP-COMMON-INPUTS*))) (defun interp-if (test tbr fbr x alist contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 2020 (+ (acl2-count test) (acl2-count tbr) (acl2-count fbr)) 50) :verify-guards nil :guard (and (posp clk) (pseudo-termp test) (pseudo-termp tbr) (pseudo-termp fbr) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* (((glcp-er test-bfr) (interp-test test alist . ,GL::*GLCP-COMMON-INPUTS*)) ((glcp-er then-unreachable then) (maybe-interp tbr alist contexts test-bfr . ,GL::*GLCP-COMMON-INPUTS*)) ((glcp-er else-unreachable else) (maybe-interp fbr alist contexts (bfr-not test-bfr) . ,GL::*GLCP-COMMON-INPUTS*)) ((when then-unreachable) (if else-unreachable (glcp-interp-abort :unreachable) (glcp-value else))) ((when else-unreachable) (glcp-value then))) (merge-branches test-bfr then else x nil contexts . ,GL::*GLCP-COMMON-INPUTS*))) (defun merge-branches (test-bfr then else x switchedp contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 1818 (+ (acl2-count then) (acl2-count else)) (if switchedp 20 30)) :verify-guards nil :guard (and (posp clk) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*) (ignorable x)) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((when (eq test-bfr t)) (glcp-value then)) ((when (eq test-bfr nil)) (glcp-value else)) ((when (hons-equal then else)) (glcp-value then)) ((when (or (atom then) (and (g-keyword-symbolp (tag then)) (or (not (eq (tag then) :g-apply)) (not (symbolp (g-apply->fn then))) (eq (g-apply->fn then) 'quote))))) (if switchedp (merge-branch-subterms (bfr-not test-bfr) else then x contexts . ,GL::*GLCP-COMMON-INPUTS*) (merge-branches (bfr-not test-bfr) else then x t contexts . ,GL::*GLCP-COMMON-INPUTS*))) (fn (if (eq (tag then) :g-apply) (g-apply->fn then) 'cons)) (rules (fn-branch-merge-rules fn (glcp-config->branch-merge-rules config) (w state))) ((mv backchain-limit interp-st) (is-decrement-backchain-limit interp-st)) ((glcp-er successp term bindings) (if (eql 0 backchain-limit) (glcp-value nil nil nil) (rewrite-apply-rules rules 'if (list (g-boolean test-bfr) then else) contexts . ,GL::*GLCP-COMMON-INPUTS*))) (interp-st (update-is-backchain-limit backchain-limit interp-st)) ((when successp) (b* ((clk (1- clk))) (interp-term-equivs term bindings contexts . ,GL::*GLCP-COMMON-INPUTS*)))) (if switchedp (merge-branch-subterms (bfr-not test-bfr) else then x contexts . ,GL::*GLCP-COMMON-INPUTS*) (merge-branches (bfr-not test-bfr) else then x t contexts . ,GL::*GLCP-COMMON-INPUTS*)))) (defun merge-branch-subterms (test-bfr then else x contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 1818 (+ (acl2-count then) (acl2-count else)) 15) :guard (and (posp clk) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* (((when (or (atom then) (atom else) (xor (eq (tag then) :g-apply) (eq (tag else) :g-apply)) (not (or (eq (tag then) :g-apply) (and (general-consp then) (general-consp else)))) (and (eq (tag then) :g-apply) (not (and (symbolp (g-apply->fn then)) (not (eq (g-apply->fn then) 'quote)) (eq (g-apply->fn then) (g-apply->fn else)) (int= (len (g-apply->args then)) (len (g-apply->args else)))))))) (b* (((mv res pathcond) (gobj-ite-merge test-bfr then else pathcond))) (glcp-value res))) ((unless (eq (tag then) :g-apply)) (b* (((glcp-er car) (merge-branches test-bfr (general-consp-car then) (general-consp-car else) x nil nil . ,GL::*GLCP-COMMON-INPUTS*)) ((glcp-er cdr) (merge-branches test-bfr (general-consp-cdr then) (general-consp-cdr else) x nil nil . ,GL::*GLCP-COMMON-INPUTS*))) (glcp-value (gl-cons-maybe-split car cdr (glcp-config->split-conses config) (w state))))) ((glcp-er args) (merge-branch-subterm-lists test-bfr (g-apply->args then) (g-apply->args else) x . ,GL::*GLCP-COMMON-INPUTS*))) (interp-fncall (g-apply->fn then) args x contexts . ,GL::*GLCP-COMMON-INPUTS*))) (defun merge-branch-subterm-lists (test-bfr then else x . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 1818 (+ (acl2-count then) (acl2-count else)) 15) :guard (and (posp clk) (equal (len then) (len else)) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((when (atom then)) (glcp-value nil)) ((cons then1 thenr) then) ((cons else1 elser) else) ((glcp-er rest) (merge-branch-subterm-lists test-bfr thenr elser x . ,GL::*GLCP-COMMON-INPUTS*)) ((glcp-er first) (merge-branches test-bfr then1 else1 x nil nil . ,GL::*GLCP-COMMON-INPUTS*))) (glcp-value (cons first rest)))) (defun maybe-simplify-if-test (test-obj branchcond . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list clk 1300 (acl2-count test-obj) 15) :verify-guards nil :guard (and (natp clk) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (glcp-run-branch branchcond (simplify-if-test test-obj . ,GL::*GLCP-COMMON-INPUTS*))) (defun simplify-if-test (test-obj . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list clk 1300 (acl2-count test-obj) 10) :verify-guards nil :guard (and (natp clk) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* ((pathcond (lbfr-hyp-fix pathcond))) (if (atom test-obj) (glcp-value (and test-obj t)) (pattern-match test-obj ((g-boolean bfr) (b* ((bfr (hyp-fix bfr pathcond)) (bfr (bfr-constr-mode-fix bfr (is-constraint interp-st)))) (glcp-value bfr))) ((g-number &) (glcp-value t)) ((g-concrete v) (glcp-value (and v t))) ((g-var &) (b* (((mv bvar bvar-db) (add-term-bvar-unique test-obj bvar-db)) (bvar-db (maybe-add-equiv-term test-obj bvar bvar-db state)) (bfr (bfr-to-param-space (glcp-config->param-bfr config) (bfr-var bvar))) (bfr (hyp-fix bfr pathcond)) (bfr (bfr-constr-mode-fix bfr (is-constraint interp-st)))) (glcp-value bfr))) ((g-ite test then else) (b* (((glcp-er test-bfr) (simplify-if-test test . ,GL::*GLCP-COMMON-INPUTS*)) (then-hyp test-bfr) (else-hyp (bfr-not test-bfr)) ((glcp-er then-unreach then-bfr) (maybe-simplify-if-test then then-hyp . ,GL::*GLCP-COMMON-INPUTS*)) ((glcp-er else-unreach else-bfr) (maybe-simplify-if-test else else-hyp . ,GL::*GLCP-COMMON-INPUTS*)) ((when then-unreach) (if else-unreach (glcp-interp-abort :unreachable) (glcp-value else-bfr))) ((when else-unreach) (glcp-value then-bfr))) (glcp-value (bfr-ite test-bfr then-bfr else-bfr)))) ((g-apply fn args) (simplify-if-test-fncall fn args . ,GL::*GLCP-COMMON-INPUTS*)) (& (glcp-value t)))))) (defun simplify-if-test-fncall (fn args . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list clk 1300 (acl2-count args) 10) :verify-guards nil :guard (and (natp clk) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((when (or (not (symbolp fn)) (eq fn 'quote))) (glcp-interp-error (msg "Non function symbol in g-apply: ~x0" fn))) ((when (and (eq fn 'not) (eql (len args) 1))) (b* (((glcp-er neg-bfr) (simplify-if-test (first args) . ,GL::*GLCP-COMMON-INPUTS*))) (glcp-value (bfr-not neg-bfr)))) ((when (and (eq fn 'equal) (eql (len args) 2) (or (eq (car args) nil) (eq (cadr args) nil)))) (b* (((glcp-er neg-bfr) (simplify-if-test (or (car args) (cadr args)) . ,GL::*GLCP-COMMON-INPUTS*))) (glcp-value (bfr-not neg-bfr)))) ((when (and (eq fn 'gl-force-check-fn) (eql (len args) 3))) (b* (((glcp-er sub-bfr) (simplify-if-test (first args) . ,GL::*GLCP-COMMON-INPUTS*)) ((mv pathcond-sat newcond) (bfr-force-check sub-bfr (if (second args) (cpathcond) t) (third args))) ((when pathcond-sat) (glcp-value newcond))) (glcp-interp-abort :unreachable))) ((when (zp clk)) (glcp-interp-error "Clock ran out in simplify-if-test")) ((glcp-er successp term bindings) (rewrite fn args :if-test '(iff) . ,GL::*GLCP-COMMON-INPUTS*)) ((when successp) (b* (((glcp-er xobj) (interp-test term bindings . ,GL::*GLCP-COMMON-INPUTS*)) (interp-st (is-prof-pop-increment t interp-st))) (glcp-value xobj))) (x (g-apply fn args)) (look (get-term->bvar x bvar-db)) ((when look) (b* ((bfr (bfr-to-param-space (glcp-config->param-bfr config) (bfr-var look))) (bfr (bfr-constr-mode-fix bfr (is-constraint interp-st))) (bfr (hyp-fix bfr pathcond))) (glcp-value bfr))) ((unless (is-add-bvars-allowed interp-st)) (glcp-interp-abort :intro-bvars-fail)) (bvar (next-bvar bvar-db)) (bvar-db (add-term-bvar x bvar-db)) (bvar-db (maybe-add-equiv-term x bvar bvar-db state)) ((glcp-er) (add-bvar-constraints x . ,GL::*GLCP-COMMON-INPUTS*)) (bfr (bfr-to-param-space (glcp-config->param-bfr config) (bfr-var bvar))) (bfr (bfr-constr-mode-fix bfr (is-constraint interp-st))) (bfr (hyp-fix bfr pathcond))) (glcp-value bfr))) (defun add-bvar-constraints (lit . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :stobjs ,GL::*GLCP-STOBJS* :guard (and (posp clk) . ,GL::*GLCP-COMMON-GUARDS*) :measure (list (pos-fix clk) 1000 0 0)) (ignorable pathcond)) (b* ((pathcond (lbfr-hyp-fix pathcond)) (ccat (is-constraint-db interp-st)) ((mv substs ccat) (ec-call (gbc-process-new-lit lit ccat state))) (interp-st (update-is-constraint-db ccat interp-st))) (add-bvar-constraint-substs substs . ,GL::*GLCP-COMMON-INPUTS*))) (defun add-bvar-constraint-substs (substs . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :stobjs ,GL::*GLCP-STOBJS* :guard (and (posp clk) . ,GL::*GLCP-COMMON-GUARDS*) :measure (list (pos-fix clk) 900 (len substs) 0)) (ignorable pathcond)) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((when (atom substs)) (glcp-value)) (subst (car substs)) ((unless (and (consp subst) (symbolp (car subst)) (alistp (cdr subst)))) (add-bvar-constraint-substs (cdr substs) . ,GL::*GLCP-COMMON-INPUTS*)) ((cons thm alist) subst) (thm-body (meta-extract-formula thm state)) ((unless (pseudo-termp thm-body)) (add-bvar-constraint-substs (cdr substs) . ,GL::*GLCP-COMMON-INPUTS*)) ((mv new-constraint . ,(REMOVE 'GL::PATHCOND GL::*GLCP-COMMON-RETVALS*)) (b* (((local-stobjs pathcond) (mv new-constraint . ,GL::*GLCP-COMMON-RETVALS*)) (pathcond (bfr-hyp-init pathcond))) (interp-test thm-body alist . ,GL::*GLCP-COMMON-INPUTS*))) ((when (eq er :intro-bvars-fail)) (add-bvar-constraint-substs (cdr substs) . ,GL::*GLCP-COMMON-INPUTS*)) ((when er) (glcp-interp-abort er :nvals 0)) ((mv ?contra upd-constraint &) (bfr-constr-assume new-constraint (is-constraint interp-st))) (interp-st (update-is-constraint upd-constraint interp-st))) (add-bvar-constraint-substs (cdr substs) . ,GL::*GLCP-COMMON-INPUTS*))) (defun rewrite (fn actuals rwtype contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :stobjs ,GL::*GLCP-STOBJS* :guard (and (posp clk) (symbolp fn) (not (eq fn 'quote)) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :measure (list (pos-fix clk) 1212 0 0)) (ignorable rwtype)) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((mv backchain-limit interp-st) (is-decrement-backchain-limit interp-st)) ((when (eql 0 backchain-limit)) (glcp-value nil nil nil)) (fn-rewrites (fn-rewrite-rules fn (glcp-config->rewrite-rule-table config) (w state))) ((glcp-er successp term bindings :nvals 3) (rewrite-apply-rules fn-rewrites fn actuals contexts . ,GL::*GLCP-COMMON-INPUTS*)) (interp-st (update-is-backchain-limit backchain-limit interp-st))) (glcp-value successp term bindings))) (defun rewrite-apply-rules (fn-rewrites fn actuals contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :stobjs ,GL::*GLCP-STOBJS* :guard (and (posp clk) (pseudo-rewrite-rule-listp fn-rewrites) (symbolp fn) (not (eq fn 'quote)) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :measure (list (pos-fix clk) 88 (len fn-rewrites) 0))) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((when (atom fn-rewrites)) (glcp-value nil nil nil)) (rule (car fn-rewrites)) ((glcp-er successp term bindings :nvals 3) (rewrite-apply-rule rule fn actuals contexts . ,GL::*GLCP-COMMON-INPUTS*)) ((when successp) (glcp-value successp term bindings))) (rewrite-apply-rules (cdr fn-rewrites) fn actuals contexts . ,GL::*GLCP-COMMON-INPUTS*))) (defun rewrite-apply-rule (rule fn actuals contexts . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :stobjs ,GL::*GLCP-STOBJS* :guard (and (pseudo-rewrite-rule-p rule) (posp clk) (symbolp fn) (not (eq fn 'quote)) (contextsp contexts) . ,GL::*GLCP-COMMON-GUARDS*) :measure (list (pos-fix clk) 44 0 0))) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((rewrite-rule rule) rule) ((unless (and (mbt (and (symbolp rule.equiv) (not (eq rule.equiv 'quote)) (not (eq rule.subclass 'meta)) (pseudo-termp rule.lhs))) (consp rule.lhs) (eq (car rule.lhs) fn))) (cw "malformed gl rewrite rule (lhs)?? ~x0~%" rule) (glcp-value nil nil nil)) ((unless (or (eq rule.equiv 'equal) (member rule.equiv contexts))) (glcp-value nil nil nil)) ((mv unify-ok gobj-bindings) (glcp-unify-term/gobj-list (cdr rule.lhs) actuals nil)) ((unless unify-ok) (glcp-value nil nil nil)) ((unless (mbt (pseudo-term-listp rule.hyps))) (cw "malformed gl rewrite rule (hyps)?? ~x0~%" rule) (glcp-value nil nil nil)) (interp-st (is-prof-push rule.rune interp-st)) (add-bvars-allowed (is-add-bvars-allowed interp-st)) (interp-st (update-is-add-bvars-allowed nil interp-st)) ((glcp-er hyps-ok gobj-bindings :nvals 3) (relieve-hyps rule.rune rule.hyps gobj-bindings . ,GL::*GLCP-COMMON-INPUTS*)) (interp-st (update-is-add-bvars-allowed add-bvars-allowed interp-st)) ((unless hyps-ok) (b* ((interp-st (is-prof-pop-increment nil interp-st))) (glcp-value nil nil nil))) ((unless (mbt (pseudo-termp rule.rhs))) (cw "malformed gl rewrite rule (rhs)?? ~x0~%" rule) (b* ((interp-st (is-prof-pop-increment nil interp-st))) (glcp-value nil nil nil)))) (glcp-value t rule.rhs gobj-bindings))) (defun relieve-hyps (rune hyps bindings . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :stobjs ,GL::*GLCP-STOBJS* :guard (and (pseudo-term-listp hyps) (posp clk) . ,GL::*GLCP-COMMON-GUARDS*) :measure (list (pos-fix clk) 22 (len hyps) 0)) (ignorable rune)) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((when (atom hyps)) (glcp-value t bindings)) ((glcp-er ok bindings :nvals 2) (relieve-hyp rune (car hyps) bindings . ,GL::*GLCP-COMMON-INPUTS*)) ((when (not ok)) (glcp-value nil bindings))) (relieve-hyps rune (cdr hyps) bindings . ,GL::*GLCP-COMMON-INPUTS*))) (defun relieve-hyp (rune hyp bindings . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :stobjs ,GL::*GLCP-STOBJS* :guard (and (pseudo-termp hyp) (posp clk) . ,GL::*GLCP-COMMON-GUARDS*) :measure (list (pos-fix clk) 15 0 0)) (ignorable rune)) (b* ((pathcond (lbfr-hyp-fix pathcond)) ((when (and (consp hyp) (eq (car hyp) 'synp))) (b* (((mv erp successp bindings) (glcp-relieve-hyp-synp hyp bindings state)) ((when erp) (glcp-interp-error (if (eq erp t) "t" erp) :nvals 2))) (glcp-value successp bindings))) ((mv bfr . ,GL::*GLCP-COMMON-RETVALS*) (interp-test hyp bindings . ,GL::*GLCP-COMMON-INPUTS*)) ((when (eq er :intro-bvars-fail)) (glcp-value nil bindings)) ((when er) (glcp-interp-abort er :nvals 2)) ((when (eq bfr t)) (glcp-value t bindings))) (glcp-value nil bindings))) (defun interp-list (x alist . ,GL::*GLCP-COMMON-INPUTS*) (declare (xargs :measure (list (pos-fix clk) 2020 (acl2-count x) 20) :guard (and (natp clk) (pseudo-term-listp x) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,GL::*GLCP-STOBJS*)) (b* ((pathcond (lbfr-hyp-fix pathcond))) (if (atom x) (glcp-value nil) (b* (((glcp-er car) (interp-term-equivs (car x) alist nil . ,GL::*GLCP-COMMON-INPUTS*)) ((glcp-er cdr) (interp-list (cdr x) alist . ,GL::*GLCP-COMMON-INPUTS*))) (glcp-value (cons car cdr))))))) (defund interp-top-level-term (term alist . ,(SUBST 'GL::PATHCOND-BFR 'GL::PATHCOND GL::*GLCP-COMMON-INPUTS*)) (declare (xargs :guard (and (pseudo-termp term) (posp clk) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs ,(REMOVE 'GL::PATHCOND GL::*GLCP-STOBJS*) :verify-guards nil)) (b* (((local-stobjs pathcond) (mv bfr-val . ,GL::*GLCP-COMMON-RETVALS*)) (config (glcp-config-update-term term config)) (pathcond (bfr-hyp-init pathcond)) ((mv contra pathcond ?undo) (bfr-assume pathcond-bfr pathcond)) ((when contra) (obs-cw "Path condition is unsatisfiable~%") (glcp-value nil))) (interp-test term alist . ,GL::*GLCP-COMMON-INPUTS*))) (defund interp-concl (term alist pathcond-bfr clk config interp-st bvar-db1 bvar-db state) (declare (xargs :guard (and (pseudo-termp term) (posp clk) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs (interp-st bvar-db bvar-db1 state) :verify-guards nil)) (b* ((al (gobj-alist-to-param-space alist pathcond-bfr)) (bvar-db (init-bvar-db (base-bvar bvar-db1) bvar-db)) (bvar-db (parametrize-bvar-db pathcond-bfr bvar-db1 bvar-db)) ((mv contra constraint &) (bfr-constr-assume (bfr-to-param-space pathcond-bfr (bfr-constr-mode->bfr (is-constraint interp-st))) (bfr-constr-init))) (constraint-db (parametrize-constraint-db pathcond-bfr (is-constraint-db interp-st))) (config (glcp-config-update-param pathcond-bfr config)) (interp-st (update-is-constraint constraint interp-st)) (interp-st (update-is-constraint-db constraint-db interp-st)) ((when contra) (obs-cw "Constraints unsatisfiable~%") (glcp-value-nopathcond t)) ((unless pathcond-bfr) (glcp-value-nopathcond t)) (pathcond-bfr (bfr-to-param-space pathcond-bfr pathcond-bfr))) (interp-top-level-term term al . ,(SUBST 'GL::PATHCOND-BFR 'GL::PATHCOND GL::*GLCP-COMMON-INPUTS*)))) (defund interp-hyp/concl (hypo concl alist clk config interp-st next-bvar bvar-db bvar-db1 state) (declare (xargs :guard (and (pseudo-termp hypo) (pseudo-termp concl) (posp clk) . ,GL::*GLCP-COMMON-GUARDS*) :stobjs (interp-st bvar-db bvar-db1 state) :verify-guards nil)) (b* ((bvar-db (init-bvar-db next-bvar bvar-db)) (bvar-db1 (init-bvar-db next-bvar bvar-db1)) (config (glcp-config-update-param t config)) ((mv hyp-bfr . ,(REMOVE 'GL::PATHCOND GL::*GLCP-COMMON-RETVALS*)) (interp-top-level-term hypo alist . ,(SUBST T 'GL::PATHCOND GL::*GLCP-COMMON-INPUTS*))) ((when er) (mv hyp-bfr nil bvar-db1 . ,(REMOVE 'GL::PATHCOND GL::*GLCP-COMMON-RETVALS*))) ((mv er unsat) (glcp-vacuity-check hyp-bfr config)) ((when er) (mv hyp-bfr nil bvar-db1 . ,(REMOVE 'GL::PATHCOND GL::*GLCP-COMMON-RETVALS*))) (concl (if unsat ''t concl)) ((mv concl-bfr . ,(SUBST 'GL::BVAR-DB1 'GL::BVAR-DB (REMOVE 'GL::PATHCOND GL::*GLCP-COMMON-RETVALS*))) (interp-concl concl alist hyp-bfr clk config interp-st bvar-db bvar-db1 state))) (mv hyp-bfr concl-bfr bvar-db1 . ,(REMOVE 'GL::PATHCOND GL::*GLCP-COMMON-RETVALS*)))) (defun interp-term-under-hyp (hypo term al next-bvar config interp-st bvar-db bvar-db1 state) (declare (xargs :stobjs (interp-st bvar-db bvar-db1 state) :verify-guards nil)) (b* ((bvar-db (init-bvar-db next-bvar bvar-db)) (bvar-db1 (init-bvar-db next-bvar bvar-db1)) (interp-st (update-is-obligs nil interp-st)) (interp-st (update-is-constraint (bfr-constr-init) interp-st)) (interp-st (update-is-constraint-db (table-alist 'gl-bool-constraints (w state)) interp-st)) ((mv hyp-bfr . ,(REMOVE 'GL::PATHCOND GL::*GLCP-COMMON-RETVALS*)) (interp-top-level-term hypo al t (glcp-config->hyp-clk config) config interp-st bvar-db state)) ((when er) (mv nil nil nil er interp-st bvar-db bvar-db1 state)) (param-al (gobj-alist-to-param-space al hyp-bfr)) (bvar-db1 (parametrize-bvar-db hyp-bfr bvar-db bvar-db1)) (config (glcp-config-update-param hyp-bfr config)) (hyp-bfr (bfr-to-param-space hyp-bfr hyp-bfr)) ((mv res-obj . ,(SUBST 'GL::BVAR-DB1 'GL::BVAR-DB (REMOVE 'GL::PATHCOND GL::*GLCP-COMMON-RETVALS*))) (interp-top-level-term term param-al hyp-bfr (glcp-config->concl-clk config) config interp-st bvar-db1 state))) (mv hyp-bfr param-al res-obj er interp-st bvar-db bvar-db1 state)))))
other
(defconst *glcp-clause-proc-template* `(progn (defun run-parametrized (hyp concl vars bindings id obligs config interp-st state) (declare (xargs :stobjs (state interp-st) :verify-guards nil)) (b* ((bound-vars (strip-cars bindings)) ((glcp-config config) config) ((unless (pseudo-termp hyp)) (glcp-error "The hyp is not a pseudo-term.~%")) (hyp-unbound-vars (set-difference-eq (simple-term-vars hyp) bound-vars)) ((when hyp-unbound-vars) (prog2$ (flush-hons-get-hash-table-link obligs) (glcp-error (msg "~ In ~@0: The hyp contains the following unbound variables: ~x1~%" id hyp-unbound-vars)))) ((unless (shape-spec-bindingsp bindings)) (flush-hons-get-hash-table-link obligs) (glcp-error (msg "~ In ~@0: the bindings don't satisfy shape-spec-bindingsp: ~x1" id bindings))) (obj (shape-spec-bindings->sspecs bindings)) ((unless (fast-no-duplicatesp (shape-spec-list-indices obj))) (glcp-error (msg "~ In ~@0: the shape spec indices contain duplicates: ~x1" id (duplicated-members (shape-spec-list-indices obj))))) ((unless (fast-no-duplicatesp (shape-spec-list-vars obj))) (glcp-error (msg "~ In ~@0: the shape spec vars contain duplicates: ~x1" id (duplicated-members (shape-spec-list-vars obj))))) ((unless (subsetp-equal vars bound-vars)) (flush-hons-get-hash-table-link obligs) (glcp-error (msg "~ In ~@0: The conclusion countains the following unbound variables: ~x1~%" id (set-difference-eq vars bound-vars)))) (constraint-db (gbc-db-make-fast (table-alist 'gl-bool-constraints (w state)))) ((unless (gbc-db-emptyp constraint-db)) (flush-hons-get-hash-table-link obligs) (gbc-db-free constraint-db) (glcp-error (msg "The constraint database stored in the table ~ GL::GL-BOOL-CONSTRAINTS contains nonempty ~ substitutions -- somehow it has gotten corrupted!~%"))) (config (change-glcp-config config :shape-spec-alist bindings)) (al (shape-specs-to-interp-al bindings)) (cov-clause (list '(not (gl-cp-hint 'coverage)) (dumb-negate-lit hyp) (shape-spec-list-oblig-term obj (strip-cars bindings)))) ((local-stobjs bvar-db bvar-db1) (mv erp val bvar-db bvar-db1 interp-st state)) (interp-st (update-is-obligs obligs interp-st)) (interp-st (update-is-constraint (bfr-constr-init) interp-st)) (interp-st (update-is-constraint-db constraint-db interp-st)) (interp-st (update-is-add-bvars-allowed t interp-st)) (interp-st (update-is-prof-enabledp config.prof-enabledp interp-st)) (next-bvar (shape-spec-max-bvar-list (shape-spec-bindings->sspecs bindings))) ((mv hyp-bfr concl-bfr bvar-db1 . ,(REMOVE 'GL::PATHCOND GL::*GLCP-COMMON-RETVALS*)) (interp-hyp/concl hyp concl al config.concl-clk config interp-st next-bvar bvar-db bvar-db1 state)) (interp-st (is-prof-report interp-st)) ((when er) (flush-hons-get-hash-table-link (is-obligs interp-st)) (gbc-db-free (is-constraint-db interp-st)) (mv er nil bvar-db bvar-db1 interp-st state)) ((mv erp val-clause state) (glcp-analyze-interp-result hyp-bfr concl-bfr (bfr-constr-mode->bfr (is-constraint interp-st)) bindings id concl config bvar-db1 state)) ((when erp) (flush-hons-get-hash-table-link (is-obligs interp-st)) (gbc-db-free (is-constraint-db interp-st)) (mv erp nil bvar-db bvar-db1 interp-st state)) (val (list val-clause cov-clause (is-obligs interp-st)))) (gbc-db-free (is-constraint-db interp-st)) (mv erp val bvar-db bvar-db1 interp-st state))) ,'(DEFUN GL::RUN-CASES (GL::PARAM-ALIST GL::CONCL GL::VARS GL::OBLIGS GL::CONFIG GL::INTERP-ST GL::STATE) (DECLARE (GL::XARGS :STOBJS (GL::STATE GL::INTERP-ST) :VERIFY-GUARDS NIL)) (IF (ATOM GL::PARAM-ALIST) (GL::MV NIL (CONS NIL GL::OBLIGS) GL::INTERP-ST GL::STATE) (GL::B* (((GL::MV GL::ERR (CONS REST GL::OBLIGS) GL::INTERP-ST GL::STATE) (GL::RUN-CASES (CDR GL::PARAM-ALIST) GL::CONCL GL::VARS GL::OBLIGS GL::CONFIG GL::INTERP-ST GL::STATE)) ((WHEN GL::ERR) (GL::MV GL::ERR NIL GL::INTERP-ST GL::STATE)) (GL::HYP (CAAR GL::PARAM-ALIST)) (GL::ID (CADAR GL::PARAM-ALIST)) (GL::G-BINDINGS (CDDAR GL::PARAM-ALIST)) (- (GL::GLCP-CASES-WORMHOLE (GL::GLCP-CONFIG->RUN-BEFORE-CASES GL::CONFIG) GL::ID)) ((GL::MV GL::ERR (LIST GL::VAL-CLAUSE GL::COV-CLAUSE GL::OBLIGS) GL::INTERP-ST GL::STATE) (GL::RUN-PARAMETRIZED GL::HYP GL::CONCL GL::VARS GL::G-BINDINGS GL::ID GL::OBLIGS GL::CONFIG GL::INTERP-ST GL::STATE)) ((WHEN GL::ERR) (GL::MV GL::ERR NIL GL::INTERP-ST GL::STATE)) (- (GL::GLCP-CASES-WORMHOLE (GL::GLCP-CONFIG->RUN-AFTER-CASES GL::CONFIG) GL::ID))) (GL::MV NIL (CONS (LIST* GL::VAL-CLAUSE GL::COV-CLAUSE REST) GL::OBLIGS) GL::INTERP-ST GL::STATE)))) ,'(DEFUN GL::CLAUSE-PROC (GL::CLAUSE GL::HINTS GL::INTERP-ST GL::STATE) (DECLARE (GL::XARGS :STOBJS (GL::STATE GL::INTERP-ST) :VERIFY-GUARDS NIL)) (GL::B* (((LIST GL::BINDINGS GL::PARAM-BINDINGS GL::HYP GL::PARAM-HYP GL::CONCL GL::?UNTRANS-CONCL GL::CONFIG) GL::HINTS) ((GL::MV GL::ERR GL::OVERRIDES GL::STATE) (GL::PREFERRED-DEFS-TO-OVERRIDES (GL::TABLE-ALIST 'GL::PREFERRED-DEFS (GL::W GL::STATE)) GL::STATE)) ((WHEN GL::ERR) (GL::MV GL::ERR NIL GL::INTERP-ST GL::STATE)) (GL::CONFIG (GL::CHANGE-GLCP-CONFIG GL::CONFIG :OVERRIDES GL::OVERRIDES :REWRITE-RULE-TABLE (GL::TABLE-ALIST 'GL::GL-REWRITE-RULES (GL::W GL::STATE)) :BRANCH-MERGE-RULES (GL::GL-BRANCH-MERGE-RULES (GL::W GL::STATE)))) ((UNLESS (GL::PSEUDO-TERMP GL::HYP)) (GL::GLCP-ERROR "The hyp is not a pseudo-term.~%")) (GL::HYP-CLAUSE (CONS '(NOT (GL::GL-CP-HINT 'GL::HYP)) (APPEND GL::CLAUSE (LIST GL::HYP)))) ((UNLESS (GL::PSEUDO-TERMP GL::CONCL)) (GL::GLCP-ERROR "The concl is not a pseudo-term.~%")) (GL::CONCL-CLAUSE (CONS '(NOT (GL::GL-CP-HINT 'GL::CONCL)) (APPEND GL::CLAUSE (LIST (LIST 'NOT GL::CONCL))))) ((UNLESS GL::PARAM-BINDINGS) (GL::B* (((GL::MV GL::ERR (LIST GL::RES-CLAUSE GL::COV-CLAUSE GL::OBLIGS) GL::INTERP-ST GL::STATE) (GL::RUN-PARAMETRIZED GL::HYP GL::CONCL (GL::SIMPLE-TERM-VARS GL::CONCL) GL::BINDINGS "main theorem" NIL GL::CONFIG GL::INTERP-ST GL::STATE)) ((WHEN GL::ERR) (GL::MV GL::ERR NIL GL::INTERP-ST GL::STATE))) (GL::OBS-CW "GL symbolic simulation OK~%") (GL::CLEAR-MEMOIZE-TABLE 'GL::GLCP-GET-BRANCH-MERGE-RULES) (GL::MV NIL (LIST* GL::HYP-CLAUSE GL::CONCL-CLAUSE GL::RES-CLAUSE GL::COV-CLAUSE (INTERP-DEFS-ALIST-CLAUSES (GL::FLUSH-HONS-GET-HASH-TABLE-LINK GL::OBLIGS))) GL::INTERP-ST GL::STATE))) ((UNLESS (GL::PSEUDO-TERMP GL::PARAM-HYP)) (GL::GLCP-ERROR "The param-hyp is not a pseudo-term.~%")) (GL::FULL-HYP (GL::CONJOIN (LIST GL::PARAM-HYP GL::HYP))) (GL::PARAM-ALIST (GL::PARAM-BINDINGS-TO-ALIST GL::FULL-HYP GL::PARAM-BINDINGS)) (GL::PARAMS-COV-TERM (GL::DISJOIN (GL::STRIP-CARS GL::PARAM-ALIST))) (GL::PARAMS-COV-VARS (GL::SIMPLE-TERM-VARS GL::PARAMS-COV-TERM)) (- (GL::OBS-CW "Checking case split coverage ...~%")) ((GL::MV GL::ERR (LIST GL::PARAMS-COV-RES-CLAUSE GL::PARAMS-COV-COV-CLAUSE GL::OBLIGS0) GL::INTERP-ST GL::STATE) (IF (GL::GLCP-CONFIG->CASE-SPLIT-OVERRIDE GL::CONFIG) (GL::MV NIL (LIST `((NOT (GL::GL-CP-HINT 'GL::CASESPLIT)) (NOT ,GL::HYP) ,GL::PARAMS-COV-TERM) '('T) 'GL::OBLIGS) GL::INTERP-ST GL::STATE) (GL::RUN-PARAMETRIZED GL::HYP GL::PARAMS-COV-TERM GL::PARAMS-COV-VARS GL::BINDINGS "case-split coverage" 'GL::OBLIGS GL::CONFIG GL::INTERP-ST GL::STATE))) ((WHEN GL::ERR) (GL::MV GL::ERR NIL GL::INTERP-ST GL::STATE)) (- (GL::OBS-CW "Case-split coverage OK~%")) ((GL::MV GL::ERR (CONS GL::CASES-RES-CLAUSES GL::OBLIGS1) GL::INTERP-ST GL::STATE) (GL::RUN-CASES GL::PARAM-ALIST GL::CONCL (GL::SIMPLE-TERM-VARS GL::CONCL) GL::OBLIGS0 GL::CONFIG GL::INTERP-ST GL::STATE)) ((WHEN GL::ERR) (GL::MV GL::ERR NIL GL::INTERP-ST GL::STATE))) (GL::CLEAR-MEMOIZE-TABLE 'GL::GLCP-GET-BRANCH-MERGE-RULES) (GL::MV NIL (LIST* GL::HYP-CLAUSE GL::CONCL-CLAUSE (APPEND GL::CASES-RES-CLAUSES (LIST* GL::PARAMS-COV-RES-CLAUSE GL::PARAMS-COV-COV-CLAUSE (INTERP-DEFS-ALIST-CLAUSES (GL::FLUSH-HONS-GET-HASH-TABLE-LINK GL::OBLIGS1))))) GL::INTERP-ST GL::STATE)))))
other
(defconst *glcp-fnnames* (event-forms-collect-fn-names (list *glcp-interp-template* *glcp-clause-proc-template*)))
glcp-name-substfunction
(defun glcp-name-subst (clause-proc) (b* ((subst-names (append '(run-gified geval geval-list geval-ev geval-ev-lst geval-ev-falsify geval-ev-meta-extract-global-badguy) (remove 'clause-proc *glcp-fnnames*)))) (pairlis$ (cons 'clause-proc subst-names) (cons clause-proc (glcp-put-name-each clause-proc subst-names)))))