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

Last time we 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 lists of integers.

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

(defdata intstr (oneof integer string))

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

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

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

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

#|
It might be a subdirectory of a classes directory

|#
(dirp `("classes" (,*cs2800-dir* ("cs2500" (("hw2.lisp" 92))))))

#|
Notice the backquote, comma duo.

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