#|
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))

(fullnamep '(Stavros Tripakis))
(fullnamep '("Stavros Tripakis"))
(fullnamep '("Stavros" "Tripakis"))
(fullnamep '("Stavros"))
(fullnamep '("Stavros" 42))
(fullnamep '("Stavros" "the bro" "Tripakis"))
(fullnamep '("Stavros the bro" "Tripakis"))

#|
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-recp (fullname-rec "Stavros" "Tripakis"))
(fullname-recp (fullname-rec "Stavros"))

(fullname-rec-first (fullname-rec "Wade" "Wilson"))
(fullname-rec-last (fullname-rec "Wade" "Wilson"))


#|

So far we have covered

Singleton types
Recognizers
Enumerated Types
Range Types
Product Types
Records
|#

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


(defdata loi (listof integer))

#|
This defines the type consisting of true lists of integers.

We can check that a loi is a true list:
|#

(thm (implies (loip x) (tlp x)))

(loip '(1 2 3))
(loip '(1 -2 3))
(loip '(1 1/2 3))
(loip nil)
(loip (cons 1 2))

;; An alist is just a list of conses.
;; An assignment is an alist from var's to rationals.

(defdata assignment (alistof var rational))

(check= (assignmentp '((x . 1) (y . 1/2))) t)
(check= (assignmentp '((x 1) (y 1/2))) nil)

(defdata varrat (cons var rational))
(defdata assignment2 (listof varrat))

(thm (equal (assignmentp x) (assignment2p x)))


#|
Union types allow us to take the union of existing types.
Here is an example.
|#

(defdata intstr (oneof integer string))

(intstrp 42)
(intstrp "hello")
(intstrp '(1 2 3))

#|
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 this is how we've been describing recursive types so
far!

We now discuss what templates user-defined datatypes that are
recursive give rise to. Many of the datatypes we define are just
lists of existing types. For example, we can define a list of
rationals as follows.
|#

(defdata lor (listof rational))

#|
If we define a function that recurs on one of its arguments,
which is a list of rationals, we just use the list template and
can assume that if the list is non-empty then the first element
is a rational and the rest of the list is a list of rationals.
|#

(definec lorlen (l :lor) :nat
  (if (endp l)
    0
    (+ 1 (lorlen (rest l)))))

#|
If we have a more complex data definition, say:
|#

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

#|
Then the template we wind up with is exactly what you would
expect from the data definition.

(defunc foo (px ...)
  :input-contract (and (PropExp px) ...)
  :output-contract (... (foo px ...))
  (cond ((booleanp px) ...)
        ((varp px) ...)
        ((UnaryOpp (first px)) ... (foo (second px)) ...)
        (t ...(foo (second px)) ... (foo (third px)) ...)))

Notice that in the last case, there is no need to check 
(BinOpp (first px)), 

since it has to hold, hence the t. Also, for the recursive cases,
we get to assume that foo works correctly on the destructed
argument ((second px) and (third px)).
|#

#|
Let's look at one more example. Consider a filesystem.

A file is a pair consisting of a string (name) and a natural
number (inode).
|#

(defdata file (list string nat))

#|
A directory is a pair consisting of a string (the directory name)
and a list whose elements are either files or directories
(subdirectories). This is a mutually-recursive type definition.
|#

(defdata 
  (dir (list string dir-file-list))
  (dir-file-list (listof file-dir))
  (file-dir (oneof file dir)))

(file-dirp nil)
(file-dirp '("myfile" 187))

(dirp "mydir")
(dirp '("mydir" nil))

#|
For example, here is a directory that contains your cs2800 hwks
|#

(defconst *cs2800-dir*
  '("cs2800" (("hw2.lisp" 12) ("hw3.lisp" 84))))

(dirp *cs2800-dir*)

#|
The cs2800 dir might also be a subdirectory of a classes directory:
|#

(dirp '("classes" (("cs2800" (("hw2.lisp" 12) ("hw3.lisp" 84)))
		   ("cs2500" (("hw2.lisp" 92))))))

;; another way to write this is using the backquote, comma duo:
(dirp `("classes" (,*cs2800-dir* ("cs2500" (("hw2.lisp" 92))))))
;; in this way, *cs2800-dir* is evaluated, and we don't have to
;; copy-paste it.

(equal `("classes" (,*cs2800-dir* ("cs2500" (("hw2.lisp" 92)))))
	'("classes" (("cs2800" (("hw2.lisp" 12) ("hw3.lisp" 84)))
		     ("cs2500" (("hw2.lisp" 92))))))

#|
Not all mutually recursive data type definitions make sense:
|#
(defdata
  (type1 (list type2))
  (type2 (list type1)))

#|
In order to "bootstrap" the construction of the type, 
we need to start from somewhere, e.g., from the empty list:
|#
(defdata
  (type1 (listof type2))
  (type2 (list type1)))

#|
In fact this also works:
|#

(defdata mytype (listof mytype))
(mytypep nil)
(mytypep '(nil))
(mytypep '(nil nil))
(mytypep '(nil nil nil))
(mytypep '((nil)))
(mytypep '((nil) (nil nil nil nil)))


#|
The data definition framework has more advanced features, e.g.,
it supports recursive record types, map types, custom types, and
so on. We will introduce such features as needed.
|#

#|

We could have also defined dir as follows

(defdata 
  (dir (list string dir-file-list))
  (dir-file-list (listof (oneof file dir))))

but it is a good idea to give all reasonable types names since we now
don't have the type file-dir, which may be useful.

So, as a general rule, we will provide names for subtypes, ie, we
prefer the first solution.

|#

#|

For documentation, you can use :doc.

|#

:doc definec
:doc defdata