#|

Author: Pete Manolios
Date:   9/7/2018

Code used in lecture 1 of Computer-Aided Reasoning.  We did not get
through all of this. The parts we did not get to are commented out.

|#

(in-package "ACL2S")

(progn
  (defunc app (x y)
    :input-contract (and (true-listp x) (true-listp y))
    :output-contract (true-listp (app x y))
    (append x y))

  (defunc head (x)
    :input-contract (and (true-listp x) (consp x))
    :output-contract t
    (car x))

  (defunc tail (x)
    :input-contract (and (true-listp x) (consp x))
    :output-contract (true-listp (tail x))
    (cdr x))

  (defthm append-right-id
    (implies (true-listp a)
             (equal (append a nil) a)))

  (defthm equal-len-0
    (equal (equal (len x) 0) (atom x))))

"
BEGIN DEMO 1

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

"
Defdata automatically generates \"enumerators\"
"

(nth-name 0)
(nth-name 1)
(nth-name 2)
(nth-name 12)

"
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 ((* 1024 1024) < _)))

"
Property-based testing with test?
"

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

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

#|

We only got up to this point. Uncomment this region if you want to
explore the rest of the file.

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


"
Consider a more complex data definition
"

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

"
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 snowcrash files
"

(defconst *cs4820-dir*
  '("cs4820" (("demo.lisp" 12) ("sorting.lisp" 34))))

"
It might be a subdirectory of a projects directory
"

(dirp `("projects" (,*cs4820-dir* 
                    ("acl2" (("other-model.lisp" 92))))))

"
The data definition framework has more advanced features, e.g.,
it supports recursive record types, map types, custom types, and
so on. 
"

"
Here is a more interesting example describing the syntax of the
ctl* temporal logic
"

(defdata atomic-formula var)

(defdata 
  (ctl* (oneof t 
               nil
               atomic-formula
               (list '~ ctl*)
               (list ctl* '& ctl*)
               (list ctl* '! ctl*)
               (list ctl* '=> ctl*)
               (list ctl* '<=> ctl*)
               (list 'E ctl*path)
               (list 'A ctl*path)))
  (ctl*path (oneof ctl* 
                   (list '~ ctl*path)
                   (list ctl*path '& ctl*path)
                   (list ctl*path '! ctl*path)
                   (list ctl*path '=> ctl*path)
                   (list ctl*path '<=> ctl*path)
                   (list 'X ctl*path)
                   (list 'F ctl*path)
                   (list 'G ctl*path)
                   (list ctl*path 'U ctl*path))))

(ctl*p t)
(ctl*p '(E a))
(ctl*p '(a U b))
(ctl*pathp '(a U b))
(ctl*p '(E (a U b)))

(thm (implies (ctl*p x) (ctl*pathp x)))

(thm (implies (ctl*pathp x) (ctl*p x)))

"END DEMO 1"

"BEGIN DEMO 2

Notice that in ACL2s mode listp is not what you expect, ...
"

"Dotted pairs"
(cons 1 2)

"*, +, append are macros"

(+ 1 2 3 4)
(+)
(*)
(* 1 2 3)
(append '(1 2) '(3 4))
(append '(1 2) '(3 4) '(5 6))

(listp '(1 2))
(listp (cons 1 2))

(true-listp '(1 2))
(true-listp (cons 1 2))

(car '(1 . 2))
(cdr '(1 . 2))
(cadr '(1 2 . 3))
(cddr '(1 2 . 3))

(in-package "ACL2")
:pe +
:pe *
:pe append
:pe listp
:pe true-listp
:pe cadr
:trans1 (* 1 2 3)
:trans1 (*)
:trans1 (cadr '(1 2 . 3))
:trans1 (append '(1 2) '(3 4) '(5 6))
(in-package "ACL2S")

#|

Rotate buffer to the left begin.

An example of how contracts are used to help students learn how
to program and specify contracts.

|#

"
Define a function that given a buffer, l, (a list) and a natural
number, n, rotates the buffer to the left n times.

(Rotate-buffer-left '(1 2 3 4 5) 2) = '(3 4 5 1 2)

"

(defunc Rotate-buffer-left (l n)
  :input-contract (and (true-listp l) (natp n))
  :output-contract (true-listp (Rotate-buffer-left l n))
  (cond ((equal n 0) l)
        (t (Rotate-buffer-left (app (tail l) (head l))
                               (- n 1)))))

(defunc Rotate-buffer-left (l n)
  :input-contract (and (true-listp l) (natp n))
  :output-contract (true-listp (Rotate-buffer-left l n))
  (cond ((equal n 0) l)
        ((endp l) nil)
        (t (Rotate-buffer-left (app (tail l) (head l))
                               (- n 1)))))

(defunc Rotate-buffer-left (l n)
  :input-contract (and (true-listp l) (natp n))
  :output-contract (true-listp (Rotate-buffer-left l n))
  (cond ((equal n 0) l)
        ((endp l) nil)
        (t (Rotate-buffer-left (app (tail l) (list (head l)))
                               (- n 1)))))
  
(check= (Rotate-buffer-left '(1 2 3 4 5) 2) '(3 4 5 1 2))

(thm (implies (and (true-listp l) (natp n))
              (equal (len (Rotate-buffer-left l n))
                     (len l))))

(defunc RBL (l n)
  :input-contract (and (true-listp l) (natp n))
  :output-contract (true-listp (RBL l n))
  (cond ((equal n 0) l)
        ((endp l) l)
        (t (RBL (app (list (head l)) (tail l))
                (- n 1)))))

(test? (implies (and (true-listp l)
                     (natp n))
                (equal (RBL l n)
                       (Rotate-buffer-left l n))))

"END DEMO 2"

|#