#|
We introduce the ACL2s data definition framework via a sequence
of examples.

Singleton types allow us to define types that contain only one
object. For example:
|#

(defdata one 1)

#|
All data definitions give rise to a recognizer.  The above data
definition gives rise to the recognizer onep.
|#

(onep 1)
(onep '1)
(onep 2)
(onep 'hello)
(onep "1")

#|
Enumerated types allow you to define finite types.
|#

(defdata name (enum '(bob ken david)))

(thm (implies (namep x)
              (or (equal x 'bob)
                  (equal x 'ken)
                  (equal x 'david))))
#|
Range types allow you 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 256) < _)))

(test? (implies (and (probabilityp x)
                     (probabilityp y))
                (probabilityp (+ x y))))

(test? (implies (and (probabilityp x)
                     (probabilityp y))
                (probabilityp (- x y))))

(test? (implies (and (probabilityp x)
                     (probabilityp y))
                (probabilityp (* x y))))

(test? (implies (and (big-natp x)
                     (big-natp y))
                (big-natp (+ x y))))

(test? (implies (and (big-natp x)
                     (big-natp y))
                (big-natp (- x y))))

(test? (implies (and (big-natp x)
                     (big-natp y))
                (big-natp (* x y))))

#|
Notice that we need to provide a domain, which is either integer
or rational, and the set of numbers is specified with
inequalities using < and <=.  One of the lower or upper bounds
can be omitted, in which case the corresponding value is taken to
be negative or positive infinity.

Product types allow us to define structured data. The example
below defines a type consisting of list with exactly two strings.
|#

(defdata fullname (list string string))

#|
Records are  product types, where the fields are named. For
example, we could have defined fullname as follows.
|#


(defdata fullname-rec (record (first . string)
                              (last . string)))

#|
In addition to the recognizer fullname-recp, the above type
definition gives rise to the constructor fullname-rec which
takes two strings as arguments and constructs a record of
type fullname-rec. The type definition also generates the
accessors fullname-rec-first and fullname-rec-last
that when applied to an object of type fullname-rec return
the first and last fields, respectively.
|#

(fullname-rec-first (fullname-rec "Wade" "Wilson"))
(fullname-rec-last (fullname-rec "Wade" "Wilson"))#|ACL2s-ToDo-Line|#

#|

We will finish with defdata in the next lecture.

|#