#|

Author: Pete Manolios
Date:   9/11/2018

Code used in lecture 2 of Computer-Aided Reasoning.  

|#

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

"
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 lointp and loip are equivalent.
"

(thm (equal (lointp x) (loip x)))

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

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

(defunc customp (x)
  :input-contract t
  :output-contract (booleanp (customp x))
  (and (integerp x)
       (equal 0 (mod x 9))
       (> x 100)))

(defunc nth-custom-builtin (n)
  :input-contract (natp n)
  :output-contract (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)

"Load a book that includes the useful must-fail macro.
"

(include-book "misc/eval" :dir :system)

"Pay attention to the stats.
"

(must-fail
 (test? (implies (customp x)
                 (not (equal 0 (mod x 17))))))

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

(must-fail
 (test? (implies (and (integerp x)
                      (equal 0 (mod x 9))
                      (> x 100))
                 (not (equal 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)

"Next we consider signatures. 
We define concat, which is the same as append, 
but for which we do not have any theorems.
"

(defunc concat (x y)
  :input-contract (and (true-listp x) (true-listp y))
  :output-contract (true-listp (concat x y))
  (if (endp x)
      y
    (cons (car x) (concat (cdr x) y))))

; Holds due to the contract theorem
(thm (implies (and (true-listp x)
                   (true-listp y))
              (true-listp (concat x y))))

; Requires proof by induction
(thm (implies (and (loip x)
                   (loip y))
              (loip (concat x y))))

; No proof by induction, due to a signature rule
(thm (implies (and (loip x)
                   (loip y))
              (loip (append x y))))

; Here is an example of a signature rule
(sig concat ((listof :a) (listof :a)) => (listof :a))

; Now, notice that this goes through with no induction
(thm (implies (and (loip x)
                   (loip y))
              (loip (concat x y))))

"
Look at the sig forms in the file base-theory.lisp to
see more examples. Here are a few.
"

(sig nth (nat (listof :a)) => :a 
     :satisfies (< x1 (len x2)))

(sig take (nat (listof :a)) => (listof :a)
     :satisfies (<= x1 (len x2))
     :hints (("Goal" :cases ((equal x1 (len x2))))))


"END DEMO 1"