other
(in-package "GL")
other
(include-book "tools/flag" :dir :system)
other
(include-book "std/util/bstar" :dir :system)
other
(include-book "std/lists/acl2-count" :dir :system)
other
(include-book "clause-processors/term-vars" :dir :system)
other
(verify-termination def-body)
other
(verify-guards fgetprop)
other
(verify-termination latest-body)
other
(verify-guards latest-body)
other
(verify-termination body)
wgetprop-fnfunction
(defun wgetprop-fn (sym prop default world) (declare (xargs :guard (and (symbolp sym) (symbolp prop) (plist-worldp world)))) (b* ((look1 (ec-call (assoc-equal sym (table-alist 'override-props world)))) (look2 (and look1 (ec-call (assoc-equal prop (ec-call (cdr look1))))))) (if look2 (ec-call (cdr look2)) (getprop sym prop default 'current-acl2-world world))))
wgetpropmacro
(defmacro wgetprop (sym prop &optional default (world 'world)) `(wgetprop-fn ,GL::SYM ,GL::PROP ,GL::DEFAULT ,GL::WORLD))
incat-fnfunction
(defun incat-fn (pkg-witness name) (let ((pkg-witness (cond ((let ((p (symbol-package-name pkg-witness))) (or (equal p "KEYWORD") (equal p *main-lisp-package-name*))) 'genvar) (t pkg-witness)))) (intern-in-package-of-symbol name pkg-witness)))
incatmacro
(defmacro incat (sym &rest strings) `(incat-fn ,GL::SYM (concatenate 'string . ,GL::STRINGS)))
my-def-bodyfunction
(defun my-def-body (name world) (let ((def-body (ec-call (def-body name world)))) (and (not (access def-body def-body :hyp)) (eq (access def-body def-body :equiv) 'equal) `(equal ,(FCONS-TERM GL::NAME (ACCESS DEF-BODY GL::DEF-BODY :FORMALS)) ,(ACCESS DEF-BODY GL::DEF-BODY :CONCL)))))
preferred-defs-table-guardfunction
(defun preferred-defs-table-guard (fn thm world) (b* ((formals (wgetprop fn 'formals :none)) ((when (eq formals :none)) (cw "Error setting preferred-defs: ~x0 is not a function symbol (it does not have a FORMALS property.)~%" fn)) (rule (wgetprop thm 'theorem :none)) ((when (eq rule :none)) (cw "Error setting preferred-defs: ~x0 is not the name of a theorem.~%" thm)) ((unless (and (eql (len rule) 3) (eq (car rule) 'equal) (consp (cadr rule)) (eq (caadr rule) fn))) (cw "Error setting preferred-defs: Theorem ~x0 does not have the required form: ~x1~%." thm `(equal (,GL::FN . ,GL::FORMALS) body))) ((unless (equal (cdadr rule) formals)) (cw "Error setting preferred-defs: Theorem ~x0 does not have the required form: ~x1.~% In particular, the formals of ~x2 are different from the variable names used in the theorem. Try instead using the form (GL::SET-PREFERRED-DEF ~x2 ~x0) to correct this.~%" thm `(equal (,GL::FN . ,GL::FORMALS) body) fn)) (missing-vars (set-difference-eq (all-vars rule) formals)) ((when missing-vars) (cw "Error setting preferred-defs: The definition body suggested by theorem ~x0 contains the variables ~x1, which are not among the formals of ~x2.~%" thm missing-vars fn))) t))
other
(table preferred-defs nil nil :guard (preferred-defs-table-guard key val world))
set-preferred-def-fnfunction
(defun set-preferred-def-fn (fn thm world) (b* ((formals (wgetprop fn 'formals :none)) ((when (eq formals :none)) (cw "Error in set-preferred-def: ~x0 is not a function symbol (it does not have a FORMALS property.)~%" fn)) (rule (wgetprop thm 'theorem :none)) ((when (eq rule :none)) (cw "Error in set-preferred-def: ~x0 is not the name of a theorem.~%" thm)) ((unless (and (eql (len rule) 3) (eq (car rule) 'equal) (consp (cadr rule)) (eq (caadr rule) fn))) (cw "Error in set-preferred-def: Theorem ~x0 does not have the required form: ~x1~%." thm `(equal (,GL::FN . ,GL::FORMALS) body))) (rule-formals (cdadr rule)) (events (if (equal formals rule-formals) nil `((table override-props ',GL::FN (cons ',(CONS 'GL::FORMALS GL::RULE-FORMALS) (cdr (assoc ',GL::FN (table-alist 'override-props world)))))))) (missing-vars (set-difference-eq (all-vars rule) rule-formals)) ((when missing-vars) (cw "Error in set-preferred-def: The definition body suggested by theorem ~x0 contains the variables ~x1, which are not among the arguments passed to ~x2 in that theorem.~%" thm missing-vars fn))) (cons 'progn (append events `((table preferred-defs ',GL::FN ',GL::THM))))))
set-preferred-defmacro
(defmacro set-preferred-def (fn thm) `(make-event (set-preferred-def-fn ',GL::FN ',GL::THM (w state))))
gl-clause-proc-exec-fns-tablemacro
(defmacro gl-clause-proc-exec-fns-table nil '(table-alist 'gl-clause-proc-exec-fns world))
gl-clause-proc-forbidden-exec-fnsmacro
(defmacro gl-clause-proc-forbidden-exec-fns nil '(cdr (assoc 'forbid (gl-clause-proc-exec-fns-table))))
forbid-clause-proc-exec-fnsmacro
(defmacro forbid-clause-proc-exec-fns (fns) `(progn (value-triple (not (cw "NOTE: Forbid-clause-proc-exec-fns currently doesn't do ~ anything useful; it is conceivable that it may again in the ~ future.~%"))) (table gl-clause-proc-exec-fns 'forbid (append ,GL::FNS (gl-clause-proc-forbidden-exec-fns)))))
add-clause-proc-exec-fnsmacro
(defmacro add-clause-proc-exec-fns (fns) (declare (ignore fns)) `(value-triple (not (cw "DEPRECATED: Add-clause-proc-exec-fns is no longer necessary; GL ~ clause processors no longer have a fixed set of functions they ~ can concretely execute.~%"))))
norm-function-bodyfunction
(defun norm-function-body (fn world) (declare (xargs :guard (and (symbolp fn) (plist-worldp world)))) (let* ((alst (table-alist 'preferred-defs world)) (entry (ec-call (assoc-equal fn alst)))) (if (and (consp entry) (symbolp (cdr entry))) (let* ((name (cdr entry)) (rule (wgetprop name 'theorem)) (formals (wgetprop fn 'formals))) (and (eql (len rule) 3) (eq (car rule) 'equal) (consp (cadr rule)) (eq (caadr rule) fn) (equal (cdadr rule) formals) (caddr rule))) (wgetprop fn 'unnormalized-body))))
norm-function-body-and-def-namefunction
(defun norm-function-body-and-def-name (fn world) (declare (xargs :guard (and (symbolp fn) (plist-worldp world)))) (let* ((alst (table-alist 'preferred-defs world)) (entry (ec-call (assoc-equal fn alst)))) (if (and (consp entry) (symbolp (cdr entry))) (let* ((name (cdr entry)) (rule (wgetprop name 'theorem)) (formals (wgetprop fn 'formals))) (if (and (eql (len rule) 3) (eq (car rule) 'equal) (consp (cadr rule)) (eq (caadr rule) fn) (equal (cdadr rule) formals)) (mv (cdr entry) (caddr rule)) (mv nil nil))) (mv fn (wgetprop fn 'unnormalized-body)))))
other
(in-theory (disable norm-function-body-and-def-name norm-function-body))
other
(program)
gl-fnsymfunction
(defun gl-fnsym (fn) (incat 'foo (symbol-package-name fn) "::" (symbol-name fn) "$"))
glcmacro
(defmacro glc (fn &rest args) `(,(GL::GL-FNSYM GL::FN) ,@GL::ARGS hyp clk config bvar-db state))
def-acl2-aliasesfunction
(defun def-acl2-aliases (lst) (if (atom lst) nil (let ((macro (incat 'foo (symbol-name (car lst))))) (list* `(defmacro ,GL::MACRO (&rest args) `(,',(CAR GL::LST) . ,GL::ARGS)) (def-acl2-aliases (cdr lst))))))
other
(make-event `(progn . ,(GL::DEF-ACL2-ALIASES '(GL::G-BOOLEAN GL::G-BOOLEAN-P GL::G-BOOLEAN->BOOL GL::G-NUMBER GL::G-NUMBER-P GL::G-NUMBER->NUM GL::G-INTEGER GL::G-INTEGER-P GL::G-INTEGER->BITS GL::G-CONCRETE GL::G-CONCRETE-P GL::G-CONCRETE->OBJ GL::G-ITE GL::G-ITE-P GL::G-ITE->TEST GL::G-ITE->THEN GL::G-ITE->ELSE GL::G-APPLY GL::G-APPLY-P GL::G-APPLY->FN GL::G-APPLY->ARGS GL::G-VAR GL::G-VAR-P GL::G-VAR->NAME))))
other
(logic)
other
(defund dumb-negate-lit (term) (declare (xargs :guard (pseudo-termp term))) (cond ((null term) ''t) ((atom term) `(not ,GL::TERM)) ((eq (car term) 'quote) (kwote (not (cadr term)))) ((eq (car term) 'not) (cadr term)) ((eq (car term) 'equal) (cond ((or (eq (cadr term) nil) (equal (cadr term) ''nil)) (caddr term)) ((or (eq (caddr term) nil) (equal (caddr term) ''nil)) (cadr term)) (t `(not ,GL::TERM)))) (t `(not ,GL::TERM))))
other
(defthm pseudo-termp-of-dumb-negate-lit (implies (pseudo-termp term) (pseudo-termp (dumb-negate-lit term))) :hints (("Goal" :in-theory (enable dumb-negate-lit pseudo-termp))))
other
(defund-inline maybe-fmt-to-comment-window (test str alist col evisc-tuple print-base-radix) (declare (xargs :guard t)) (and test (fmt-to-comment-window str alist col evisc-tuple print-base-radix)))
maybe-cwmacro
(defmacro maybe-cw (test str &rest args) `(maybe-fmt-to-comment-window ,GL::TEST ,GL::STR (pairlis2 *base-10-chars* (list ,@GL::ARGS)) 0 nil nil))
other
(defund-inline observation-uninhibited (state) (declare (xargs :guard t :stobjs state :guard-hints (("goal" :in-theory (e/d (state-p1) (state-p-implies-and-forward-to-state-p1)))))) (not (let ((lst (f-get-global 'inhibit-output-lst state))) (and (true-listp lst) (member-eq 'observation lst)))))