#|

Author: Pete Manolios
Date:   9/9/2021

Code used in lecture 2 of Computer-Aided Reasoning.  


|#

(in-package "ACL2S")

"
BEGIN DEMO 1

We introduce the ACL2s data definition framework via a sequence of
examples. The idea is to just remind everyone of defdata.  These notes
are not meant to be exhaustive.  So, read the reading material!
"

"
Range types allow us to define a range of numbers.  The two
examples below show how to define the rational interval [0..1]
and the integers greater than 2^{64}.
"

(defdata probability (range rational (0 <= _ <= 1))) 
(defdata big-nat (range integer ((expt 2 64) < _)))

"
Property-based testing with test?
"

(test? (=> (^ (probabilityp x)
              (probabilityp y))
           (probabilityp (+ x y))))

(test? (=> (^ (probabilityp x)
              (probabilityp y))
           (probabilityp (* x y))))

(test? (=> (^ (big-natp x)
              (big-natp y))
           (big-natp (+ x y))))

(test? (=> (^ (big-natp x)
              (big-natp y))
           (big-natp (- x y))))

(test? (=> (big-natp x)
           (big-natp (1- x))))

"
We can create list types using the listof combinator as follows.
"

(defdata loi (listof integer))

"
This defines the type consisting of lists of integers.
"

"
Recursive type expressions involve the oneof
combinator and product combinations, where additionally there is
a (recursive) reference to the type being defined.
For example, here is another way of defining a list of integers.
"

(defdata loint (oneof nil (cons integer loint)))

"Notice that lointp and loip are equivalent.
"

(thm (== (lointp x) (loip x)))

"
Consider a more complex data definition
"

(defdata UnaryOp '~)
(defdata BinOp (enum '(& + => ==)))
(defdata PropEx (oneof boolean 
                       var
                       (list UnaryOp PropEx)
                       (list PropEx Binop PropEx)))

"We now show an example of a custom data definition with a recognizer
and an enumerator for natural numbers divisible by 9 and >100.
"

(definec customp (x :all) :bool
  (^ (integerp x)
     (= 0 (mod x 9))
     (> x 100)))

(definec nth-custom-builtin (n :nat) :int
  :post (customp (nth-custom-builtin n))
  (+ (* 9 n) 108))

"Here is the simplest way to create a custom type.
"

(register-type custom :predicate customp :enumerator nth-custom-builtin)

"Pay attention to the stats.
"

(must-fail
  (test? (=> (customp x)
             (! (= 0 (mod x 17))))))

"Notice that without the custom type, the stats are not as good.
"

(must-fail
  (test? (=> (^ (integerp x)
                (= 0 (mod x 9))
                (> x 100))
             (! (= 0 (mod x 17))))))

"We can use custom types to construct new types without restriction.
"

(defdata fob (oneof custom boolean))

"Some examples of the enumerator.
"

(nth-fob 0)
(nth-fob 1)
(nth-fob 2)
(nth-fob 3)
(nth-fob 4)
(nth-fob 5)