;; B* demo. (include-book "tools/bstar" :dir :system) (doc 'b*) ;; Simple LET*-like usage: (b* ((a (+ 1 2)) (b (* a 3))) ;; "implicit PROGN" in result: (cw "(+ A B) is ~x0~%" (+ a b)) (* a b)) (defun two-values (x) (mv x (* 2 x))) ;; MV usage and implicit IGNORABLE declaration: (b* (((mv a b) (two-values (+ 1 2))) ((mv ?c d) (two-values (+ a b)))) d) ;; Inline conditional: (b* ((a (+ 1 2)) ((when (< a 3)) ;; implicit PROGN (cw "a is less than 3~%") (* a 2))) (* a 1/2)) ;; Error triple support: (b* (((er &) ;; ignored value (with-output :off :all (defthm foo (equal x x) :rule-classes nil))) (- ;; "run for side effects" (cw "foo proved~%")) ((er &) (with-output :off :all (defthm bar (equal x y) :rule-classes nil)))) (value (cw "done"))) ;; Time permitting, go through that one with :trans1. nil ;; def-patbind-macro (progn (defun my-triple-first (x) (car x)) (defun my-triple-second (x) (cadr x)) (defun my-triple-third (x) (cddr x))) (def-patbind-macro my-triple (my-triple-first my-triple-second my-triple-third)) ;; Arbitrarily nestable: (b* (((my-triple (cons (my-triple a b c) d) e f) '(((a b . c) . d) e . f))) (list a b c d e f)) (cw "End b* demo.~%") ;; Rulesets demo (include-book "tools/rulesets" :dir :system) (def-ruleset builtin-recursive-defs '(len nth)) (add-to-ruleset builtin-recursive-defs '(append)) (get-ruleset 'builtin-recursive-defs (w state)) (def-ruleset! builtin-recursive-defs '(nth len)) ;; use in in-theory (in-theory (disable* minimal-theory (:ruleset builtin-recursive-defs))) (set-inhibit-warnings "theory") (in-theory (e/d** (minimal-theory append) ((:rules-of-class :definition :here)) ((:ruleset builtin-recursive-defs)))) (in-theory (theory 'ground-zero)) (cw "End rulesets demo.~%") ;; Flag.lisp demo (include-book "tools/flag" :dir :system) (pe 'pseudo-termp) (mutual-recursion (defun make-arith-term (oracle) (cond ((or (atom oracle) (eq (car oracle) nil)) ''1) ((eq (car oracle) '+) (cons '+ (make-arith-list (cdr oracle)))) (t (list '- (make-arith-term (cdr oracle)))))) (defun make-arith-list (oracle) (if (or (atom oracle) (eq (car oracle) nil)) nil (cons (make-arith-term (cadr oracle)) (make-arith-list (cddr oracle)))))) (flag::make-flag make-arith-flag make-arith-term) ;; Fails miserably. (defthm pseudo-termp-make-arith-term (pseudo-termp (make-arith-term oracle))) (defthm-make-arith-flag pseudo-termp-make-arith-term-lemma (make-arith-term (pseudo-termp (make-arith-term oracle)) :name pseudo-termp-make-arith-term) (make-arith-list (pseudo-term-listp (make-arith-list oracle)) :name pseudo-term-listp-make-arith-list :rule-classes nil) :hints (("goal" :induct (make-arith-flag flag oracle)))) (u) (defthm-make-arith-flag pseudo-termp-make-arith-term-lemma (make-arith-term (pseudo-termp (make-arith-term oracle)) :name pseudo-termp-make-arith-term) (make-arith-list (pseudo-term-listp (make-arith-list oracle)) ;; Don't introduce this lemma. :skip t) :hints (("goal" :induct (make-arith-flag flag oracle)))) (cw "End flag demo~%") ;; defsort demo: (include-book "defsort/defsort" :dir :system) ;; Need guards. (defun rational-key-alist-elt (x) (declare (xargs :guard t)) (and (consp x) (rationalp (car x)))) (defun key-< (x y) (declare (xargs :guard (and (rational-key-alist-elt x) (rational-key-alist-elt y)))) (< (car x) (car y))) (defsort :comparablep rational-key-alist-elt :compare< key-< :prefix alist-key) (pe 'alist-key-sort-sorts) (pe 'alist-key-sort-preserves-duplicity) (cw "End defsort demo") (quit) cd /projects/hvg/sswords/e/acl2/books/ihs/ ../cert.pl -h ../cert.pl -c *.lisp TIME_CERT=t time ../cert.pl *.lisp -j 8 cat Makefile-tmp ../critpath.pl @logops.lisp