#|

CS 2800 Homework 3 - Summer 2018

This homework is done in groups. More elaborate instructions are 
posted on the course website:

 * One group member will create a group in BlackBoard.
 
 * Other group members then join the group.
 
 * Homework is submitted once. Therefore make sure the person
   submitting actually does so. In previous terms when everyone needed
   to submit we regularly had one person forget but the other submissions
   meant the team did not get a zero. Now if you forget, your team gets 0.
   - It wouldn't be a bad idea for groups to email confirmation messages
     to each other to reduce anxiety.

 * Submit the homework file (this file) on Blackboard.  Do not rename 
   this file.  There will be a 10 point penalty for this.

 * You must list the names of ALL group members below, using the given
   format. This way we can confirm group membership with the BB groups.
   If you fail to follow these instructions, it costs us time and
   it will cost you points, so please read carefully.

The format should be: FirstName1 LastName1, FirstName2 LastName2, ...
There will be a 10 pt penalty if your names do not follow this format.

Names of ALL group members: ...

* Later in the term if you want to change groups, the person who created
  the group should stay in the group. Other people can leave and create 
  other groups or change memberships (the Axel Rose membership clause). 
  Email David Sprague about group changes.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

For this homework you will need to use ACL2s.

Technical instructions:

- open this file in ACL2s as hw03.lisp

- make sure you are in BEGINNER mode. This is essential! Note that you can
  only change the mode when the session is not running, so set the correct
  mode before starting the session.

- insert your solutions into this file where indicated (usually as "...")

- only add to the file. Do not remove or comment out anything pre-existing unless
  we tell you to.

- make sure the entire file is accepted by ACL2s. In particular, there must
  be no "..." left in the code. If you don't finish all problems, comment
  the unfinished ones out. Comments should also be used for any English
  text that you may add. This file already contains many comments, so you
  can see what the syntax is.

- when done, save your file and submit it as hw03.lisp

- avoid submitting the session file (which shows your interaction with the
  theorem prover). This is not part of your solution. Only submit the lisp
  file.

Instructions for programming problems:

For each function definition, you must provide both contracts and a body.

You must also ALWAYS supply your own tests. This is in addition to the
tests sometimes provided. Make sure you produce sufficiently many new test
cases. This means: cover at least the possible scenarios according to the
data definitions of the involved types. For example, a function taking two
lists should have at least 4 tests: all combinations of each list being
empty and non-empty.

Beyond that, the number of tests should reflect the difficulty of the
function. For very simple ones, the above coverage of the data definition
cases may be sufficient. For complex functions with numerical output, you
want to test whether it produces the correct output on a reasonable
number of inputs.

Use good judgment. For unreasonably few test cases we will deduct points.

We will use ACL2s' check= function for tests. This is a two-argument
function that rejects two inputs that do not evaluate equal. You can think
of check= roughly as defined like this:

(defunc check= (x y)
  :input-contract (equal x y)
  :output-contract (equal (check= x y) t)
  t)

That is, check= only accepts two inputs with equal value. For such inputs, t
(or "pass") is returned. For other inputs, you get an error. If any check=
test in your file does not pass, your file will be rejected.

We also learned about test? in class.  This generally takes the form:
(test? (implies <Data expected> <True statement based on expected data>))

For example, one might write:
(test? (implies (and (listp x)(listp y))(equal (+ (len x)(len y))(len (app x y)))))

|#


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Contract Fulfillment
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

The following are functions that may or may not be correct. For each function,
list all of the calls that this function makes. For each call decide whether
the contract is satisfied or not. If it is satisfied, then explain why. If it
is not satisfied then explain why not. In other words, show all of the body
contracts. Do the same for the overall function contract.

---------
EXAMPLE
(defunc foo (x)
  :input-contract (listp x)
  :output-contract (natp (foo x))
  (if (endp x)
     0
     (+ 1 (foo (rest x)))))
Body Contract:
(rest x) the input-contract is satisfied because x needs to be a non-empty list
and this is ensured by the if statement and the input contract for foo.

(foo (rest x)) the input-contract is satisfied because (rest x) outputs a list.

(+ 1 (foo (rest x))) the input contract is two natural numbers. 1 is a natural by definition.
The output-contract for foo is natp and thus + has appropriate input.

(endp x) the input-contract requires x to be a list. This is ensured by the input contract
of foo.

(if (endp x)....) the input-contract requires (endp x) to be a boolean.  endp returns a boolean
based on its output contract.

Function Contract:

(+ 1 (foo (rest x))) If the recursive call obeys the contract, then the returned value must be a nat
since the inputs are naturals.

0 Since 0 is an natural number, the output-contract holds.

Thus the overal function contract is satisfied.
----------
|#

;; since the following functions may have errors in their contracts, we turn ACL2s's
;; checking off temporarily
:program
(acl2s-defaults :set testing-enabled nil)

:program


;; 1. The following function supposedly computes the modulo of an integer by a nat.
(defunc mod (x y)
  :input-contract (and (integerp x) (natp y) (not (equal y 0)))
  :output-contract (natp (mod x y))
  (cond ((>= x y) (mod (- x y) y))
        ((>= x 0) x)
        (t (mod (+ x y) y))))

#|
............


2. The following function supposedly computes the magnitude of a rational for
scientific notation.
|#


(defunc mag (x)
  :input-contract (and (rationalp x) (>= x 0))
  :output-contract (natp (mag x))
  (cond ((equal x 0) 0)
        ((>= x 10) (+ (mag (/ x 10)) 1))
        ((< x 1) (- (mag (* x 10)) 1))
        (t 0)))

#|
............



3. The following function does something mysterious.
|#

(defunc ack (m n)
  :input-contract (and (natp m) (natp n))
  :output-contract (natp (ack m n))
  (cond ((equal m 0) (+ n 1))
        ((equal n 0) (ack (- m 1) 1))
        (t           (ack (- m 1) (ack m (- n 1))))))


#|
.................

|#
 
;; Turn proper testing back on
:logic
(acl2s-defaults :set testing-enabled t)

;; Assume by "Def of lor" that each element is a rational
;; and a lor is (cons rational lor) | nil
;; A similar claim can be made about a lon
(defdata lor (listof rational))
(defdata lon (listof nat))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; del: Any x List -> List
;; (del e l) takes an element e and a list l
;; and removes the FIRST occurance of e from l
;; If e is not in l then l is returned.
(defunc del (e l)
  :input-contract (listp l)
  :output-contract (listp (del e l))
  (if (endp l)
    l
    (if (equal e (first l))
      (rest l)
      (cons (first l) (del e (rest l))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; GIVEN
;; perm: List x List -> Boolean
;; (perm l1 l2) takes two lists (l1 and l2) and
;; returns true if and only if l1 and l2 have
;; the same elements (and the same number of each)
;; Essentially: is l2 a reordering of l1?
(defunc perm (l1 l2)
  :input-contract (and (listp l1)(listp l2))
  :output-contract (booleanp (perm l1 l2))
  (if (equal l1 l2)
    t
    (if (endp l1)
      nil
      (and (in (first l1) l2)
           (perm (rest l1) (del (first l1) l2))))))


 ;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; For sections II and III, DEFINE the functions indicated (typically denoted with "..."  
 ;; Make sure to write appropriate tests for each function that you define.


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section II: Calculating Your Grade
;;
;; Soon I will be asking you to write a program which determines
;; your mark in the course (given that BB stinks for handling
;; dropped grades). Note, this also means that at the end of term, if
;; you ask us what your grade is or why blackboard is saying X, we will
;; point you to this assignment.
;; However, first I want to define how we can store these data 
;; (FYI: Yes THESE data. Data is the plural of datum)
;;
;; We will split grades up by category (exam, assignment, or quiz)
;; Each category has a name, its weight (percentage of total grade),
;; number of grades counted (to exclude dropped grades). the max score for 
;; each assignment, and a list of the grades in that category. A full gradebook
;; is composed of all three grade categories.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;; 1. DEFINE an enumerated datatype for category names
;; (exam, assignment or quiz).
 (defdata category-name ...)

(check= (category-namep 'assignments) t)
(check= (category-namep 'tv) nil)

;; 2. DEFINE the possible weights as the range of integers 
;; from 0 to 100, inclusive
 (defdata category-weight ...)

(check= (category-weightp 66) t)
(check= (category-weightp 2/3) nil)
(check= (category-weightp 150) nil)
(check= (category-weightp 100) t)

;; 3. DEFINE a grade category as a record containing a name, weight, num-counted,
;; max-score, and grades. Num-counted and max-score shoud be positive naturals, 
;; and grades should be a list of rationals (to account for partial credit). 
;; More concretely, the tests below should pass.
(defdata grade-category ...)

(test? (implies (grade-categoryp c) (category-namep (grade-category-name c))))
(test? (implies (grade-categoryp c) (category-weightp (grade-category-weight c))))
(test? (implies (grade-categoryp c) (posp (grade-category-num-counted c))))
(test? (implies (grade-categoryp c) (posp (grade-category-max-score c))))
(test? (implies (grade-categoryp c) (lorp (grade-category-grades c))))

;; 4. DEFINE a gradebook as a list containing exactly three grade categories: assignments,
;; quizes, and exams.
 (defdata gradebook ...)

;; 5. DEFINE a datatype for letter grades (A, A-, B+, B,.... F)
(defdata lettergrade ...)

(check= (lettergradep 'A) t)
(check= (lettergradep 'F) t)
(check= (lettergradep 'E) nil)
(check= (lettergradep 'A+) nil)
(check= (lettergradep 'D+) t)

;; NOTE: These constants will be useful later in the program
(defconst *num-assignments* 10)
(defconst *num-exams* 2)
(defconst *num-quizzes* 20)

(defconst *pct-assignments* 20)
(defconst *pct-quizzes* 20)
(defconst *pct-exams* 60)

(defconst *assignments-max* 100)
(defconst *exams-max* 100)
(defconst *quizzes-max* 24)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; To avoid having to keep typing a long list of grade records, it is handy
; to define a global constant which can then be used for many check= tests.
; You should put all of the grades of your team in gradebooks. You can make
; a gradebook for each group member and we suggest your gradebook should
; contain your actual grades. ie Your check= tests should use your own 
; gradebook. Here is a modifiable example
(defconst *cs2800-a1* (grade-category 'assignments 
                                      *pct-assignments* *num-assignments* *assignments-max*
                                      '(90 80 78 82 91 85 71 64 83 85 81)))
(defconst *cs2800-q1* (grade-category 'quizzes 
                                      *pct-quizzes* *num-quizzes* *quizzes-max*
                                      '(18 18 18 18 24 24 24 18 18 18 24
                                        0  0  18 0  24 6  18 0  24 18 12)))
(defconst *cs2800-e1* (grade-category 'exams 
                                      *pct-exams* *num-exams* *exams-max*
                                      '(74 78)))
(defconst *cs2800* (list *cs2800-a1* *cs2800-q1* *cs2800-e1*))
        
        

;; GIVEN
;; sum-l: lor -> rational
;; (sum-l lr) takes a list of rationals (lr) and returns the sum of all
;; elements in the list.  If lr is empty, then return 0.
(defunc sum-l (lr)
  :input-contract (lorp lr)
  :output-contract (rationalp (sum-l lr))
  (if (endp lr)
    0
    (+ (first lr)(sum-l (rest lr)))))


;; GIVEN
;; min-l: lor (non-empty) -> rational
;; (min-l lr) takes a non-empty list of rationals (lr) and finds
;; the smallest value in that list.
(defunc min-l (lr)
  :input-contract (and (lorp lr)(consp lr))
  :output-contract (rationalp (min-l lr))
  (if (endp (rest lr))
    (first lr)
    (if (<= (first lr) (min-l (rest lr)))
      (first lr)
      (min-l (rest lr)))))

;; this line is for ACL2s
(sig del (all (listof :b)) => (listof :b))

;; 6. DEFINE
;; drop-n-lowest : Lor x Nat -> Lor
;; removes the n lowest rationals from the list, up to the length of the list
(defunc drop-n-lowest (l n)
  ...)
  
;; Write sufficient tests
..............


;; 7. DEFINE
;; get-counted-grades : grade-category -> lorp
;; returns a list containing all of the grades that should be counted from this
;; category
(defunc get-counted-grades (c)
    ...)
  
;; Write sufficient tests
.........

;; 8. DEFINE
;; get-category-pts : grade-category -> rational
;; returns the number of points you receive (for your final grade) based on the category.
;; overall grade in the given category as a rational 
;; in the range 0 <= r <= 1
(defunc get-category-pts (c)
    ...)
  
;; Write sufficient tests
.......

;; ===========SOLUTION
(defconst *MIN-D-* 50)
(defconst *MIN-D* 60)
(defconst *MIN-D+* 65)
(defconst *MIN-C-* 70)
(defconst *MIN-C* 74)
(defconst *MIN-C+* 77)
(defconst *MIN-B-* 80)
(defconst *MIN-B* 84)
(defconst *MIN-B+* 87)
(defconst *MIN-A-* 90)
(defconst *MIN-A* 94)


;; don't ask why this is necessary here; it's complicated
:program



;; 9. DEFINE
;; get-grade : gradebook -> lettergrade
;; returns the overall grade in class as a letter grade. For the purposes of this
;; assignment, assume that grades are assigned to the following ranges:
;; F: 0 <= _ < 50
;; D-: 50 <= _ < 60
;; D: 60 <= _ < 65
;; D+: 65 <= _ < 70
;; C-: 70 <= _ < 74
;; C: 74 <= _ < 77
;; C+: 77 <= _ < 80
;; B-: 80 <= _ < 84
;; B: 84 <= _ < 87
;; B+: 87 <= _ < 90
;; A-: 90 <= _ < 94
;; A: 94 <= _ <= 100
;; Please define constansts for the letter grade ranges
(defunc get-grade (gb)
    ...)
  
;; Write sufficient tests
...............

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section III: Binary Search Trees
;; Let's play with data definitions again.  This time it will be a tree
;; data structure.  More specifically, a binary search tree (feel free to wikipedia this). 
;; This means that any node in the tree has at most two children AND the first child
;; is less than or equal to the parent while the second child has a value strictly
;; greater than the parent.
;; We will assume no repetition in the tree so the first child has a value strictly less
;; than the parent.
;; Binary search trees, when balanced, allow you to search for a value in log n time
;; (like binary search).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;; DEFINE: a BSTree this is either empty (nil) or a rational number
;; and two child nodes (BSTrees). If both children are nil then the node
;; is considered a leaf node.
;; SOLUTION
..........

;;DEFINE
;; empty-bstpL BSTRee -> Boolean
;; returns true if tree bst is empty (has no nodes)
(defunc empty-bstp (bst)
 .....)

; IGNORE START
; IGNORE THESE THEOREMS. USED TO HELP ACL2S REASON
(defthm bst-empty (implies (BSTreep tree)(equal (consp tree)
                                                (not (empty-bstp tree)))))

(defthm bst-expand1
  (IMPLIES (AND (BSTreep X)
                (acl2::consp X))
           (equal (SECOND X)
                  (acl2::second x))))

(defthm bst-expand2
  (implies (and (BSTreep x)
                (consp X))
           (equal (third (acl2::double-rewrite x))
                  (acl2::third (acl2::double-rewrite x)))))
  
(defthm tr-second (implies (and (BSTreep tree)(consp tree))
                           (BSTreep (second tree))))
(defthm tr-third (implies (and (BSTreep tree)(consp tree))
                          (BSTreep (third tree))))


(defunc min (x y)
  :input-contract (and (rationalp x)(rationalp y))
  :output-contract (rationalp (min x y))
  (if (< x y) x y))

(defunc max (x y)
  :input-contract (and (rationalp x)(rationalp y))
  :output-contract (rationalp (max x y))
  (if (> x y) x y))

(defthm bst-expand3
  (implies (and (BSTreep bst)(consp bst))
           (and (equal (THIRD bst)
                       (acl2::third bst))
                (equal (second bst)
                       (acl2::second bst))
                (equal (first bst)
                       (acl2::first bst)))))

; IGNORE END

;; Sample data you can use to test your code.
(defconst *sample-bst1* 
  (list 4 
        (list 3 
              (list 1 
                    (list 0 nil nil) 
                    (list 2 nil nil)) 
              nil)
        (list 18 
              (list 7 
                        (list 5 nil (list 6 nil nil))
                        (list 9 (list 8 nil nil)
                              (list 11 (list 10 nil nil)
                                    (list 14 (list 12 nil nil)
                                          (list 16 (list 15 nil nil)
                                                (list 17 nil nil))))))
              (list 21 
                    (list 19 nil (list 20 nil nil))
                    (list 24 (list 22 nil nil)(list 25 nil nil))))))
(check= (BSTreep *sample-bst1*) t)

;; DEFINE:
;; bst-depth BSTree -> nat
;; (bst-depth bst) takes a tree bst and returns the depth of the tree (the maximum
;; distance between the root node and the furthest away leaf node)
(defunc bst-depth (bst)
  ............)

(check= (bst-depth *sample-bst1*) 8)
....... ; additional tests.


;; DEFINE
;; (bst-orderedp: BSTree -> boolean
;; (bst-orderedp bst) takes a tree bst and determines
;; if it is in the correct order.  Child elements of
;; each node are <= the parent (child 1) or
;; greater than the parent (child 2).
;; As always, you can write a helper function.
;; NOTE: I'm not demanding the REAL ordering definition which requires
;; you know that all "child 1 ancestors" to a node are <= the
;; node value while "child 2 ancestors" are > the node value.
(defunc bst-orderedp (bst)
  .........)

;; Here are some simple tests (I used to debug my solution)
;; Please add your own tests.
(check= (bst-nodeorderp *sample-bst1*) t)
(check= (bst-nodeorderp (list 19 nil (list 20 nil nil))) t)
(check= (bst-nodeorderp (list 19 nil nil)) t)
(second (list 1 (list 0 nil nil) (list 2 nil nil)))
(bst-orderedp (list 0 nil nil))

(check= (bst-orderedp *sample-bst1*) t)

;; Student added tests.
........

;; DEFINE
;; bst-in: rational x BSTree (ordered) -> Boolean
;; (bst-in r bst) returns true iff value r is in the tree bst.
(defunc bst-in (r bst)
  :input-contract (and (rationalp r)(BSTreep bst)(bst-orderedp bst))
  :output-contract (booleanp (bst-in r bst))
  ......)

;; DEFINE: Write a data definition that represented non-empty binary search trees.
(defdata NE-BSTree .......)


;; DEFINE:
;; bst-add: rational x BSTree -> BSTree
;; Add a node representing rational r to tree bst ensuring the tree
;; stays in sorted order.
;; We will claim that binary search trees do not have duplicate elements
;; Thus calling add for a value already in the tree does nothing.
;; If the value IS added then we add it to the first open (empty) child branch
;; This means the BST is not balanced.  That's OK for this homework.
(defunc bst-add (r bst)
  ........)

(check= (bst-add 4 (bst-add 3 (bst-add 1 (bst-add 10 (bst-add 5 nil)))))
        (LIST 5
              (LIST 1 NIL (LIST 3 NIL (LIST 4 NIL NIL)))
              (LIST 10 NIL NIL)))
;; ADD more tests
........

;; Finally, write two funcitons min-tree and max-tree that
;; return the minimum and maximum values for any non-empty tree.
............

#|

The purpose of a sorting algorithm is to rearrange a list of elements
in order. To test whether a sorting algorithm is correct, one must show
not only that the algorithm produces a list that is in order, but also
the same elements from the source list (and only those elements) are in 
the resultant list. Any elements that occur more than once in the
original list will occur the same number of times in the result list.

|#


;; DEFINE (not graded)
;; no-dupesp: List -> boolean
;; (no-dupesp l) returns true if and only if each element in
;; l occurs in l once (hence there are no duplicates)
(defunc no-dupesp (l)
........)

;; DEFINE (not graded)
;; orderedp: LOR -> boolean
;; (orderedp l) return true if and only if the elements in l
;; are in non-descending order. That is for any two adjacent rational numbers
;; in a list of rational numbers, the first number must be <= the second number.
(defunc orderedp (l)
..........)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section IV: Tree Sorting (Challenge Problem)
;; Now let's use our newly created binary search trees to sort
;; any given list of rational numbers. I won't be giving a lot of structure here
;; because handling more open ended questions is a critical CS skill. Write
;; a function bst-sort that sorts a list of rational numbers (using a BST to
;; do so) such that the following
;; tests pass.  You should add your own tests as well.
.............


(test? (implies (lorp lr)(orderedp (bst-sort lr))))

(test? (implies (and (lorp lr)(no-dupesp lr))
                (perm lr (bst-sort lr))))