;; 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