#|

CS 2800 Homework 2 - 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, ...
Names of ALL group members: ...............

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). 
  We will post additional instructions about this later.

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

For this homework you will need to use ACL2s.

Technical instructions:

- open this file in ACL2s as hw02.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 hw02.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.

|#

#|

Since this is our first programming exercise, we will simplify the
interaction with ACL2s somewhat: instead of asking it to formally *prove*
the various conditions for admitting a function, we will just require that
they be *tested* on a reasonable number of inputs. This is achieved using
the following directive (do not remove it!):
|#
:program

#|

Notes:

1. Testing is cheaper but less powerful than proving. So, by turning off
proving and doing only testing, it is possible that the functions we are
defining cause runtime errors even if called on valid inputs. In the future
we will require functions complete with admission proofs, i.e. without the
above directive. For this first homework, the functions are simple enough
that there is a good chance ACL2s's testing will catch any contract or
termination errors you may have.

2. The tests ACL2s runs test only the conditions for admitting the
function. They do not test for "functional correctness", i.e. does the
function do what it is supposed to do? ACL2s has no way of telling what
your function is supposed to do. That is what your own tests are for.

3. For now, testing is written using check= expressions.  These take the following
format (and should be familiar to those of you that took Fundies I)
(check= <expression> <thing it should be equal to>)
EX: (check= (- 4/3 1) 1/3)

|#

#|
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 Part I:
 The functions below should warm you up for the rest of the 
 assignment.
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 But first, let me get ahead of myself.  Typically we would ask
 these sorts of questions for HW03 or 4 but since we need a special kind
 of list: a list of rationals (lor).  The data definition below
 creates a data type called a list of rationals which is a list that
 can ONLY have rational numbers in it (no need to test if a list
 element is a rational, just need to check if the list is empty or not.
 This list also has a built in recognizer "lorp" which tests if 
 a variable is a list of rationals. I've also created a list of natural 
 numbers that can be recognized by calling "lonp"
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|#
;; Lists of rational numbers
(defdata lor (listof rational))
;; Lists of natural numbers
(defdata lon (listof nat))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; DEFINE
;; how-many: All x List -> Nat
;;
;; (how-many e l) returns the number of occurrences of element e 
;; in list l.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defunc how-many (e l)
  .......)

(check= (how-many  1 ())     0)
(check= (how-many  1 '(1 1)) 2)
;; Remember to add additional tests

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; DEFINE
;; tser: List (non-empty) -> List
;; TSER is just rest backwards. Thus (tser l) removes the last
;; element in list l and returns all other elements in the list
;; in their original order.
(defunc tser (l)
  :input-contract (and (listp l)(consp l))
  :output-contract (listp (tser l))
  .......)

(check= (tser '(a b c)) '(a b))
;; Add tests
.......

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; DEFINE
;; 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))
  .......)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; DEFINE
;; flat-listp
;; flat-listp: Any -> Boolean
;;
;; (flat-list l) takes an input l and returns true if and only if
;; l is a list AND each element in l is not a list. 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defunc flat-listp (l)
  .......)

(check= (flat-listp '(1 2 (3))) nil)
(check= (flat-listp '(1 2 3)) t)
;; Make sure you add additional tests
.......................


#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Part II: GCD
The greatest common divisor of two numbers is the largest natural number
that evenly divides the two numbers.....you probably already knew this.
Let's calculate this in ACL2s.
|#

 ;; gpos for potential positive integers greater than 1. 
(defdata gpos (range integer (2 <= _)))
;; A list of whole numbers greater than 1.
(defdata log (listof gpos))
  
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; factors : gpos -> log
;; returns a list containing all PRIME factors of n including (possibly) 
;; n. Notice you will likely need a helper function.
.......

;; Note the factors for 12 *could* be listed as 1 2 3 4 6 12 but
;; really 12 is uniquely represented as the product of non-decreasing 
;; prime numbers: 2*2*3.  Thus factors will return '(2 2 3)  
;; 13 is prime so it isn't decomposed into other
;; primes and '(13) is returned. 
(check= (factors 2)'(2))
(check= (factors 4)'(2 2))
(check= (factors 6)'(2 3))
(check= (factors 12)'(2 2 3))
(check= (factors 13)'(13))

;; GIVEN
;; Defined in class. Removes
;; the first instance of an element in a list
(defunc delete (e l)
  :input-contract (listp l)
  :output-contract (listp (delete e l))
  (if (endp l)
    l
    (if (equal e (first l))
      (rest l)
      (cons (first l)(delete e (rest l))))))

;; Ignore. Uncomment if you wanted to use logic mode
;(sig delete (all (listof :b)) => (listof :b))

;; DEFINE
;; intersect: list x list -> list
;; (intersect l1 l2) returns a list containing every element 
;; that is in both lists l1 and l2.
;; NOTE: we must delete common elements from l2 because l1 can have duplicates.
;;       Thus this is a list intersect not a set intersect.
(defunc intersect (l1 l2)
  .......)

;; DEFINE
;; coprime: gpos x gpos -> boolean
;; Your job is to use the functions above to figure out if two
;; numbers are coprime (have no common factors) 
(defunc coprimep (a b)
  .......)

;; Ignore: this line is for ACL2s. Uncomment if in logic mode.
;(sig intersect ((listof :b) (listof :b)) => (listof :b))

;; DEFINE
;; gcd: pos x pos -> pos
;; (gcd a b) determines the greatest common divisor for a and b.
;; Do you remember how to calculate that with prime factors?
(defunc gcd (a b)
  .......)

(check= (gcd 7 6) 1)
(check= (gcd 8 6) 2)
(check= (gcd 12 6) 6)

;; Add additional tests
.......

#|
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 Part III: List manipulation
 This following section deals with functions involving lists in general.
 Some functions you write may be useful in subsequent functions.
 In all cases, you can define your own helper functions if that simplifies
 your code
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|#


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define
; sublist-start: List x Nat -> List
;
; (sublist-start l size) returns the sublist of list l of length size 
; starting with the first element. If size > the length of l,  return
; the entire list.
(defunc sublist-start (l size)
  .......)

(check= (sublist-start '(1 2 3 4) 2) '(1 2))
(check= (sublist-start '(1 2 3 4) 0) nil)
(check= (sublist-start '(1 2 3 4) 5) '(1 2 3 4))

;; Additional testing (students don't need test? but the
;; test below should be WAY more powerful than a series of 
;; exact tests
.......


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define
; sublist: List x Nat x Nat -> List
;
; (sublist l start end) returns the sublist of list l starting with element start
; and ending with elment end (inclusive). If start > end then return nil.
; Index numbers are 0 based. Thus the first element is element 0.
.......

(check= (sublist '(1 2 3 4) 2 3) '(3 4))
(check= (sublist '(1 2 3 4) 2 2) '(3))
(check= (sublist nil 1 1) nil)

;; GIVEN
;; all-identp: list -> Boolean
;; (all-identp l) just sees if all elements in l are identical
(defunc all-identp (l)
  :input-contract (listp l)
  :output-contract (booleanp (all-identp l))
  (if (or (endp l) (endp (rest l)))
    t
    (if (equal (first l)(second l))
      (all-identp (rest l))
      nil)))

;; You can leave off extra tests.  I'm just giving a function in case it makes
;; your life easier.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define
; max-ident-sublist: List -> Nat
;
; (max-ident-sublist l) returns the size of the largest sublist of identical
; elements (without removing or re-arranging elements in l.
; HINT: Note that if l does not just have the same element througout, you can 
; calculate max-ident-sublist on two slightly smaller sublists of l to
; find your answer. Notice the functions we've already written.
(defunc max-ident-sublist (l)
  .......)

(check= (max-ident-sublist '(1 2 3 3 3 4)) 3)
(check= (max-ident-sublist '(a c b b c d c)) 2)
(check= (max-ident-sublist nil) 0)
; Extra Checks (for examples)
.......


 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; DEFINE (not graded)
 ;; find-in: Atom x List -> Boolean
 ;; find-in takes an singleton element (e) (which is NOT a list) 
 ;; plus a list to search (l) and returns true if e is anywhere in
 ;; l, including in a sublist. See the checks below for examples.
 ;; When do you stop? When will you need to search a sub-list?
 ;; HOW do you search that sub-list?
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (defunc find-in (e l)
   :input-contract (and (atom e)(listp l))
   :output-contract (booleanp (find-in e l))
   .......)

(check= (find-in 4 '(a (2 4) 3)) t)
(check= (find-in 4 '(a (2 3) 4)) t)
(check= (find-in 4 '(a (2 5) 3)) nil)
(check= (find-in 4 '(a (2 (3 (2 1) (3 4)) 3))) t)
(check= (find-in 'a nil) nil)
(check= (find-in 'a '(a (2 a) 3)) t)
(check= (find-in nil '(a () 3)) t) ;; What's going on here?


;;====================================================
;; Now a bit of a challenge (thus don't panic if you don't get it right):
;; List Distance

;; Let's figure out how similar two lists are to one another 
;; where order is a critical factor. Two identical lists would have
;; a distance of 0 and two lists with no common elements would have a
;; distance of the length of the LARGEST list (since you would replace 
;; all elements from the short list and then add remaining elements).
;;
;; Your job will be to calculate the minimal list distance between any two lists
;; For two lists you can add, remove, or replace any given list element
;; (this problem is actually highly related to Levenshtein or string edit distances:
;; https://en.wikipedia.org/wiki/Levenshtein_distance)
;; Your approach does not need to be efficient. Here is what you need to consider:
;; 1) How similar are two lists? How do you determine how many times the ith element
;; in the source and target lists are the same?
;; 2) What is the distance if the source or target lists are empty?
;; 3) For two non-empty lists, examine the first of the source and the first of the target.
;;    You can add to the source list, remove the first from the source list or change 
;;    the first (each of these operations cost 1). After that you need to find the list 
;;    distance of the new list.
;; 4) it may help to have a function that takes 3 values and returns the minimum value.
;;
;; To avoid infinite loops, you should ONLY add/remove/replace if the first of each list is
;; different (but you must recur in either event) and only add (first target) to the source, not
;; some other element.

;; list-dist: list x list -> nat
;; list-dist calculates the list distance (nat) between 
;; list src (source) and list tgt (target)
(defunc list-dist (src tgt)
  .............)

(check= (list-dist '(1 2 3 4 5 6)'(2 3 4 5)) 2) ; Remove 1 and 6 from the first list
(check= (list-dist '(1 2 3 4 5 6)'(2 4 6)) 3)
(check= (list-dist '(2 4 6) '(1 2 3 4 5 6)) 3) ; Add 1, 3, and 5 to the first list
(check= (list-dist '(1 2 3 4 5 6)'(6 4 2)) 5)
(check= (list-dist '(1 2 3 4 5 6)'(1 2 2 5 5 6)) 2) ; change the 3 and 4 to 2 and 5.
;; Add additional checks and test? s.
....................