defaggregate

(in-package "STD")

(include-book "../defaggregate")

(include-book "../deflist")

(include-book "std/testing/assert-bang" :dir :system)

(encapsulate nil
  (defun foof-p
    (x)
    (declare (xargs :guard t))
    (keywordp x))
  (defmacro foom-p (x) `(keywordp ,STD::X))
  (defaggregate containerf
    (thing)
    :require ((foof-p-of-containerf->thing (foof-p thing)))
    :tag :containerf)
  (defaggregate containerm
    (thing)
    :require ((foom-p-of-containerm->thing (foom-p thing)))
    :tag :containerm))

(mutual-recursion (defund foo-p
    (x)
    (declare (xargs :guard t))
    (and (consp x)
      (eq (car x) :foo)
      (alistp (cdr x))
      (consp (cdr x))
      (let ((bar (cdr (assoc 'bar (cdr x)))))
        (declare (ignorable bar))
        (and (foo-list-p bar)))))
  (defund foo-list-p
    (x)
    (declare (xargs :guard t
        :normalize nil
        :verify-guards t
        :guard-debug nil
        :guard-hints nil))
    (if (consp x)
      (and (foo-p (car x))
        (foo-list-p (cdr x)))
      (null x))))

(defaggregate foo
  (bar)
  :require ((foo-list-p-of-foo->bar (foo-list-p bar)))
  :already-definedp t
  :tag :foo)

(deflist foo-list-p
  (x)
  (foo-p x)
  :elementp-of-nil nil
  :already-definedp t
  :true-listp t)

(defaggregate pair-o-ints
  ((left integerp "Left part of pair") (right integerp "Right part of pair"))
  :tag :pair-o-ints)

(defund sum-a-pair
  (x)
  (declare (xargs :guard (pair-o-ints-p x)))
  (b* (((pair-o-ints x) x) (- (cw "left is ~x0~%" x.left))
      (- (cw "right is ~x0~%" x.right)))
    (+ x.left x.right)))

(assert! (equal (sum-a-pair (make-pair-o-ints :left 4 :right 5))
    9))

(defsection test-of-tree-layout
  (defaggregate employee
    :tag :employee ((name stringp "some documentation") (salary natp
        :rule-classes :type-prescription :default 25))
    :layout :tree :short "Hello!")
  (assert! (b* ((emp (make-employee :name "foo")))
      (and (equal (employee->name emp) "foo")
        (equal (employee->salary emp) 25))))
  (assert! (b* ((emp (make-employee :name "foo")) ((employee emp) emp))
      (and (equal emp.name "foo") (equal emp.salary 25))))
  (assert! (b* ((emp (make-employee :name "foo")) ((employee emp) emp))
      (and (equal emp.name "foo")
        (equal emp.salary 25)
        emp)))
  (assert! (b* ((emp (make-employee :name "foo")) ((employee emp2) emp))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* (((employee emp2) (make-employee :name "foo")))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* ((emp (make-employee :name "foo")) ((employee emp) (change-employee emp :name "bar")))
      (and (equal emp.name "bar") (equal emp.salary 25))))
  (assert! (b* ((?emp (make-employee :name "foo")) ((employee emp) (change-employee emp :name "bar" :salary 156)))
      (and (equal emp.name "bar")
        (equal emp.salary 156)))))

(defsection test-of-honsed-tree-layout
  (defaggregate h-employee
    :tag :h-employee ((name stringp "some documentation") (salary natp
        :rule-classes :type-prescription :default 25))
    :layout :tree :hons t
    :short "Hello!")
  (assert! (b* ((emp (make-h-employee :name "foo")))
      (and (equal (h-employee->name emp) "foo")
        (equal (h-employee->salary emp) 25))))
  (assert! (b* ((emp (make-h-employee :name "foo")) ((h-employee emp) emp))
      (and (equal emp.name "foo") (equal emp.salary 25))))
  (assert! (b* ((emp (make-h-employee :name "foo")) ((h-employee emp) emp))
      (and (equal emp.name "foo")
        (equal emp.salary 25)
        emp)))
  (assert! (b* ((emp (make-h-employee :name "foo")) ((h-employee emp2) emp))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* (((h-employee emp2) (make-h-employee :name "foo")))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* ((emp (make-h-employee :name "foo")) ((h-employee emp) (change-h-employee emp :name "bar")))
      (and (equal emp.name "bar") (equal emp.salary 25))))
  (assert! (b* ((?emp (make-h-employee :name "foo")) ((h-employee emp) (change-h-employee emp :name "bar" :salary 156)))
      (and (equal emp.name "bar")
        (equal emp.salary 156)))))

(defsection test-of-fulltree
  (defaggregate employee2
    :tag :employee2 ((name stringp "some documentation") (salary natp
        :rule-classes :type-prescription :default 25))
    :layout :tree :short "Hello!")
  (assert! (b* ((emp (make-employee2 :name "foo")))
      (and (equal (employee2->name emp) "foo")
        (equal (employee2->salary emp) 25))))
  (assert! (b* ((emp (make-employee2 :name "foo")) ((employee2 emp) emp))
      (and (equal emp.name "foo") (equal emp.salary 25))))
  (assert! (b* ((emp (make-employee2 :name "foo")) ((employee2 emp) emp))
      (and (equal emp.name "foo")
        (equal emp.salary 25)
        emp)))
  (assert! (b* ((emp (make-employee2 :name "foo")) ((employee2 emp2) emp))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* (((employee2 emp2) (make-employee2 :name "foo")))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* ((emp (make-employee2 :name "foo")) ((employee2 emp) (change-employee2 emp :name "bar")))
      (and (equal emp.name "bar") (equal emp.salary 25))))
  (assert! (b* ((?emp (make-employee2 :name "foo")) ((employee2 emp) (change-employee2 emp :name "bar" :salary 156)))
      (and (equal emp.name "bar")
        (equal emp.salary 156)))))

(defsection test-of-fulltree
  (defaggregate h-employee2
    :tag :h-employee2 ((name stringp "some documentation") (salary natp
        :rule-classes :type-prescription :default 25))
    :layout :tree :hons t
    :short "Hello!")
  (assert! (b* ((emp (make-h-employee2 :name "foo")))
      (and (equal (h-employee2->name emp) "foo")
        (equal (h-employee2->salary emp) 25))))
  (assert! (b* ((emp (make-h-employee2 :name "foo")) ((h-employee2 emp) emp))
      (and (equal emp.name "foo") (equal emp.salary 25))))
  (assert! (b* ((emp (make-h-employee2 :name "foo")) ((h-employee2 emp) emp))
      (and (equal emp.name "foo")
        (equal emp.salary 25)
        emp)))
  (assert! (b* ((emp (make-h-employee2 :name "foo")) ((h-employee2 emp2) emp))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* (((h-employee2 emp2) (make-h-employee2 :name "foo")))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* ((emp (make-h-employee2 :name "foo")) ((h-employee2 emp) (change-h-employee2 emp :name "bar")))
      (and (equal emp.name "bar") (equal emp.salary 25))))
  (assert! (b* ((?emp (make-h-employee2 :name "foo")) ((h-employee2 emp) (change-h-employee2 emp :name "bar" :salary 156)))
      (and (equal emp.name "bar")
        (equal emp.salary 156)))))

(defsection test-of-list
  (defaggregate employee3
    :tag :employee3 ((name stringp "some documentation") (salary natp
        :rule-classes :type-prescription :default 25))
    :layout :list :short "Hello!")
  (assert! (b* ((emp (make-employee3 :name "foo")))
      (and (equal (employee3->name emp) "foo")
        (equal (employee3->salary emp) 25))))
  (assert! (b* ((emp (make-employee3 :name "foo")) ((employee3 emp) emp))
      (and (equal emp.name "foo") (equal emp.salary 25))))
  (assert! (b* ((emp (make-employee3 :name "foo")) ((employee3 emp) emp))
      (and (equal emp.name "foo")
        (equal emp.salary 25)
        emp)))
  (assert! (b* ((emp (make-employee3 :name "foo")) ((employee3 emp2) emp))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* (((employee3 emp2) (make-employee3 :name "foo")))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* ((emp (make-employee3 :name "foo")) ((employee3 emp) (change-employee3 emp :name "bar")))
      (and (equal emp.name "bar") (equal emp.salary 25))))
  (assert! (b* ((?emp (make-employee3 :name "foo")) ((employee3 emp) (change-employee3 emp :name "bar" :salary 156)))
      (and (equal emp.name "bar")
        (equal emp.salary 156)))))

(defsection test-of-alist
  (defaggregate employee4
    :tag :employee4 ((name stringp "some documentation") (salary natp
        :rule-classes :type-prescription :default 25))
    :layout :alist :short "Hello!")
  (assert! (b* ((emp (make-employee4 :name "foo")))
      (and (equal (employee4->name emp) "foo")
        (equal (employee4->salary emp) 25))))
  (assert! (b* ((emp (make-employee4 :name "foo")) ((employee4 emp) emp))
      (and (equal emp.name "foo") (equal emp.salary 25))))
  (assert! (b* ((emp (make-employee4 :name "foo")) ((employee4 emp) emp))
      (and (equal emp.name "foo")
        (equal emp.salary 25)
        emp)))
  (assert! (b* ((emp (make-employee4 :name "foo")) ((employee4 emp2) emp))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* (((employee4 emp2) (make-employee4 :name "foo")))
      (and (equal emp2.name "foo")
        (equal emp2.salary 25)
        emp2)))
  (assert! (b* ((emp (make-employee4 :name "foo")) ((employee4 emp) (change-employee4 emp :name "bar")))
      (and (equal emp.name "bar") (equal emp.salary 25))))
  (assert! (b* ((?emp (make-employee4 :name "foo")) ((employee4 emp) (change-employee4 emp :name "bar" :salary 156)))
      (and (equal emp.name "bar")
        (equal emp.salary 156)))))

(defaggregate m0 (a b c))

(assert! (let ((topic (find-topic 'm0-p
         (get-xdoc-table (w state)))))
    (and topic
      (equal (cdr (assoc :parents topic)) '(undocumented)))))

(set-default-parents foo bar)

(defaggregate m1 (a b c))

(assert! (let ((topic (find-topic 'm1-p
         (get-xdoc-table (w state)))))
    (and topic
      (equal (cdr (assoc :parents topic))
        '(foo bar)))))

(defaggregate m2
  (a b c)
  :parents (bar))

(assert! (let ((topic (find-topic 'm2-p
         (get-xdoc-table (w state)))))
    (and topic
      (equal (cdr (assoc :parents topic)) '(bar)))))

(defaggregate pancake
  :tag :pancake ((syrup booleanp) (butter booleanp)
    (sugar natp))
  :extra-binder-names (messy)
  :layout :tree :verbosep t)

(define pancake->messy
  ((x pancake-p))
  (and (pancake->syrup x)
    (pancake->butter x)))

(define pancake-info
  ((x pancake-p))
  (b* (((pancake x)))
    (msg "syrupy: ~x0 buttery: ~x1 messy: ~x2~%"
      x.syrup
      x.butter
      x.messy))
  ///
  (assert! (equal (pancake-info (make-pancake :syrup t :butter nil :sugar 5))
      (msg "syrupy: ~x0 buttery: ~x1 messy: ~x2~%" t nil nil))))

(defaggregate student
  ((firstname stringp) (lastname stringp)
    (grade natp))
  :layout :fulltree :extra-binder-names (fullname))

(define student->fullname
  ((x student-p))
  :returns (fullname stringp :rule-classes :type-prescription)
  (concatenate 'string
    (student->firstname x)
    " "
    (student->lastname x)))

(assert! (equal (b* ((fred (make-student :firstname "Fredrick"
           :lastname "Flintstone"
           :grade 7)) ((student fred)))
      (concatenate 'string
        "Fred's full name is "
        fred.fullname
        "."))
    "Fred's full name is Fredrick Flintstone."))

(assert! (b* ((grade (make-student :firstname "foo"
         :lastname "bar"
         :grade 6)) (new (change-student grade :firstname "blah")))
    (and (equal (student->grade new)
        (student->grade grade))
      (equal (student->lastname new)
        (student->lastname grade))
      (equal (student->firstname new) "blah")
      (equal (student->firstname grade) "foo"))))

(define change-test
  ((grade student-p))
  (change-student grade :firstname "blah"))

(defsection test-of-pred-option
  (defaggregate point
    ((x integerp) (y integerp))
    :pred pointp)
  (assert! (pointp (point 3 2))))