; *************** BEGIN INITIALIZATION FOR PROGRAMMING MODE *************** ;
; (Nothing to see here!  Your actual file is after this initialization code);

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the TRACE* book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
; only load for interactive sessions: 
#+acl2s-startup (include-book "trace-star" :uncertified-okp nil :dir :acl2s-modes :ttags ((:acl2s-interaction)) :load-compiled-file nil);v4.0 change

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading the EVALABLE-LD-PRINTING book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
; only load for interactive sessions: 
#+acl2s-startup (include-book "evalable-ld-printing" :uncertified-okp nil :dir :acl2s-modes :ttags ((:acl2s-interaction)) :load-compiled-file nil);v4.0 change

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading ACL2s customizations book.~%Please choose \"Recertify ACL2s system books\" under the ACL2s menu and retry after successful recertification.") (value :invisible))
(include-book "custom" :dir :acl2s-modes :uncertified-okp nil :load-compiled-file :comp)

#+acl2s-startup (er-progn (assign fmt-error-msg "Problem loading programming mode.") (value :invisible))
(er-progn 
  (program)
  (defun book-beginning () ()) ; to prevent book development
  (set-irrelevant-formals-ok :warn)
  (set-bogus-mutual-recursion-ok :warn)
  (set-ignore-ok :warn)
  (set-verify-guards-eagerness 0)
  (set-default-hints '(("Goal" :error "This depends on a proof, and proofs are disabled in Programming mode.  The session mode can be changed under the \"ACL2s\" menu.")))
  (reset-prehistory t)
  (set-guard-checking :none)
  (assign evalable-ld-printingp t)
  (assign evalable-printing-abstractions '(list cons))
  (assign triple-print-prefix "; ")
  (mv
    (cw "~@0Programming mode loaded.~%~@1"
      #+acl2s-startup "${NoMoReSnIp}$~%" #-acl2s-startup ""
      #+acl2s-startup "${SnIpMeHeRe}$~%" #-acl2s-startup "")
    :invisible state))

; **************** END INITIALIZATION FOR PROGRAMMING MODE **************** ;
;$ACL2s-SMode$;Programming
#|
CS2800 Homework 2 - Fall 2010

Student name:  TODO: PUT YOUR NAMES HERE (Both you and your partner)

For this homework, you will need to use ACL2s.  See the class web page
and http://acl2s.ccs.neu.edu/acl2s/doc/ for more info on how to get it
on your own computer and how to run it in the CCIS computer labs.

We also assume you have some familiarity with ACL2s (go to lab; see the
tutorial http://acl2s.ccs.neu.edu/acl2s/doc/#tutorial etc.)


You should edit this file in ACL2s as hwk2.lisp.  Make sure you
that the session mode is "Programming". You should modify the
marked portions of this file in accordance with the instructions in comments
like these.  You should turn in a .lisp file (this one!) for which all the
forms are accepted by ACL2; thus, please delete or comment out any parts you
haven't completed by turn-in time.
|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Part 1: Evaluates to <?>
;
; For each of these, try to predict what the left-hand-side of the equality
; will evaluate to and then replace the # with the correct value--in the
; canonical form ACL2 prints when passed that expression in the
; read-eval-print loop.  For example:
;   (check= (/ 5 4) #))
; should become
;   (check= (/ 5 4) 5/4))
; which is accepted by ACL2 after moving the line past it.  (The arguments
; to CHECK= must be equal for ACL2 to accept the check.)  What you
; fill in should be an atom, written differently if the left hand side is
; already an atom.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|
Recommendations:  If you want to copy the left-hand expressions to the
session for evaluation, put the cursor at the beginning of the expression,
and press Ctrl+Shift+Space (Mac: Cmd+Shift+Space) to select that
subexpression.  Also, if you're in the middle of the expression, pressing
that sequence repeatedly selects larger and larger expressions.  Press
Ctrl+c to copy, Ctrl/Cmd+Shift+o to switch to the session editor, and
Ctrl+v to paste (assuming the session is running).  Pressing Enter at the
end of a complete REPL input should submit it.  Ctrl+Enter anywhere at the
REPL submits as if input is complete.
|#

; Numbers - basics

(check= (- (* 4 9) 32)          4)
(check= (- 0)                   0)
(check= (- 12)                  -12)
(check= (* (- (+ 16 12) 11) 42) 714)
(check= (/ 128 8)               16)
(check= -4/8 -1/2)
(check= (* 5 1/2) 5/2)
(check= 0/376 0)

(defconst *PI-APPROX* 22/7) 


(check= (/ *PI-APPROX* 0)         0)
(check= (/ 0 0)                      0)
(check= (* 4 *PI-APPROX* 1/3 2/3) 176/63)

; Numbers - destructors for rationals

(check= (denominator 6/8) 4)
(check= (numerator (/ 2 -4)) -1)

; Numbers - predicates (these are t or nil)

(check= (integerp -1) t)
(check= (integerp 0) t)
(check= (integerp 1) t)
(check= (integerp 3/2) nil)
(check= (integerp 4/2) t)

(check= (natp -1) nil)
(check= (natp 0) t)
(check= (natp 1) t)
(check= (natp 3/2) nil)
(check= (natp 4/2) t)


(check= (natp *PI-APPROX*)      nil)
(check= (integerp *PI-APPROX*)  nil)
(check= (rationalp *PI-APPROX*) t)


(check= (zp 0) t)
(check= (zp 1) nil)
(check= (zp -1) t)
(check= (zp 3/2) t)
(check= (zp 4/2) nil)
(check= (zp "hi") t)
(check= (zp nil) t)

(check= (posp -1) nil)
(check= (posp 0) nil)
(check= (posp 1) t)
(check= (posp 3/2) nil)
(check= (posp 4/2) t)

(check= (natp (cons 1 (cons 2 nil)))              nil)
(check= (rationalp (first (list 1 2)))            t)
(check= (integerp (rest (cons 'a 0)))             t)
(check= (rationalp 3/2) t)
(check= (rationalp 42) t)
(check= (rationalp nil) nil)


; Booleans and and/or functions
(check= (equal 0 nil) nil)
(check= (equal nil Nil) t)
(check= (equal 3 6/2) t)
(check= (and t nil) nil)
(check= (and t t nil t) nil)
(check= (and nil) nil)
(check= (or t t) t)
(check= (or t t nil t) t)
(check= (or nil) nil)
(check= (not nil) t)
(check= (not 0) nil)
(check= (not 1) nil)
(check= (and t (equal 1 1) 12 5/7) 5/7)
(check= (or (natp -1) 12 5/7 (not t)) 12)


; Identity elements

(check= (+) 0)
(check= (*) 1)
(check= (or) nil)
(check= (and) t)

; Lists: constructors and destructors

(check= (first (list 42 54 87))                       42)
(check= (rest (list 1 3 4))                           '(3 4))
(check= (rest (list nil 1))                           '(1))
(check= (first (cons 2 (cons 1 nil)))                 2)
(check= (first (rest (cons 3 (cons 2 (cons 1 nil))))) 2)
(check= (rest (rest (cons 3 (cons 2 (cons 1 nil)))))  '(1))
(check= (first (cons "left" "right"))                   "left")
(check= (rest (cons 'left 'right))                    'right)
(check= (first (rest (cons 'left 'right)))            nil)
(check= (rest "hello world")                          nil)
(check= (first 123)                                   nil)

; TrueLists: predicates

(check= (true-listp nil)                            t)
(check= (true-listp (cons 1 (cons 2 (cons 3 nil)))) t)
(check= (true-listp (cons 'left 'right))            nil)
(check= (true-listp (cons (cons 'a 'b) 'c))         nil)
(check= (true-listp (cons (cons 'a 'b) nil))        t)
(check= (true-listp "hello world")                  nil)
 
(check= (endp nil)                   t)
(check= (endp (cons 1 (cons 2 nil))) nil)
(check= (endp (cons 'left 'right))   nil)
(check= (endp 'a)                    t)
(check= (endp "hello world")         t)
(check= (endp 0) t)

(check= (consp nil)                   nil)
(check= (consp (cons 1 (cons 2 (list 0)))) t)
(check= (consp (cons 'left 'right))   t)
(check= (consp 'a)                    nil)
(check= (consp "hello world")         nil)
(check= (consp 12) nil)

;quotes
(check= (equal 1 '1) t)
(check= (equal 1 ''1) nil)
(check= (equal "hello" '"hello") t)
(check= (equal -3/2 '-3/2) t)
;(check= (equal a 'a) #) ;is this a static error? if yes comment it out
;(check= (equal (1 2 3) '(1 2 3)) t) ;is this  a static error? if yes comment it out
(check= (equal 'a ''a) nil)
(check= (equal (list 1 2 3) '(1 2 3)) t)
(check= (equal (list 1 2) (cons 1 (cons 2 nil))) t)
(check= (equal (list 1 2) (cons 1 (list 2))) t)
;(check= (equal (list a b c) '(a b c)) nil) ;is this  a static error? if yes comment it out
(check= (equal (list 'a 'b 'c) '(a b c)) t)
(check= (car ''a) 'quote)



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Part 2:
;
; In part 2, you have to provide definitions for the function
; stubs below. You can use auxiliary definitions, if you need
; them. You have to use the design recipe and the design
; guidelines presented in class. 
; So, make sure you use the check= to test your
; definitions and that you provide contracts for any auxiliary
; functions you define. Also specify the purpose/usage of the 
;function in the documentation string like in the function stubs.
; Your function should terminate on all inputs, so include some tests
; outside the intended domain.  For some of these, it might be easy to
; expand the intended domain, which is fine.
;

; 
; Notation:
; A type such as ``nat'' refers to something satisfying the
; NATP predicate, which is a natural number.
; "all" is the type we give in contracts for a parameter with no restrictions
; A type beginning with "Lo" means "[true] list of" whatever type follows.
; | means or

; Question 2: Basic methods
; The following methods should be fairly straight-forward
; to implement, and are a good exercise in recursive thinking.
; The following functions are allowed in definitions:
;   if
;   cond
;   endp
;   atom
;   list
;   cons
;   car
;   cdr
;   equal
;   >
;   <
;   <=
;   >=
;   and
;   or
;   not
;   +
;   -
;   *
;   /
;   natp
;  integerp
;  append

;Make sure you write the check= tests BEFORE you write the function definition and dont fill in
;the check= rhs argument by evaluation. check= tests u shud write manually here, this makes sure
;you catch simple bugs in your definition.
;Also dont forget to write a few check= tests that handle totality of ACL2 functions

; odd-integer?: integer -> Boolean
; Implementation details: recursively define.
(defun odd-integer? (x)
" Usage: Returns true if x is an odd integer, nil otherwise."
  (cond ((= x 0) nil)
        ((= x 1) t)
        ((< x 0) (odd-integer? (+ 2 x)))
        (t (odd-integer? (- x 2)))))

(check= (odd-integer? 0) nil)
(check= (odd-integer? 1) t)
(check= (odd-integer? -5) t)
(check= (odd-integer? 5) t)
(check= (odd-integer? -88) nil)
(check= (odd-integer? nil) nil)

; lo-odd-integerp: All -> Boolean
; hint: if u think u could use odd-integer? then notice the different contracts might
;force you to define a slightly modified check!
(defun lo-odd-integerp (l)
" Usage: Returns t if all elements in l are odd integers, nil otherwise."
  (if (endp l)
    (if (equal l nil)
      t
      nil)
    (and (integerp (car l));here is that extra check, to extend the domain to All
         (odd-integer? (car l))
         (lo-odd-integerp (cdr l)))))
      

(check= (lo-odd-integerp  5) nil)
(check= (lo-odd-integerp  '(1 87 -5)) t)
(check= (lo-odd-integerp  '(0 2 -4)) nil)
(check= (lo-odd-integerp  nil) t)
(check= (lo-odd-integerp  '(1 . 3)) nil)

; find-key-by-value: All ListOfTwo-element-lists -> All
; ListofRecords is a list of elements, each of which is a List of two elements
;See purpose of function in documentation string below:
;I have given one example test:
;(check= (find-key-by-value 2 (list (list "a" 1) (list "b" 2) (list "c" 3))) "b")

(defun find-key-by-value (value l)
" Usage: Searches l for the first element whose second element is value.
 returns the key if found.
 returns nil if there is no such element."
  (if (endp l)
    nil
    (let ((first-entry (car l)))
    (if (equal value (cadr first-entry))
      (car first-entry);if found return key
      ;else recurse on rest of list
      (find-key-by-value value (cdr l))))))
      
      

(check= (find-key-by-value 2 (list (list "a" 1) (list "b" 2) (list "c" 3))) "b")
(check= (find-key-by-value 2 nil) nil)
(check= (find-key-by-value 2 "helloo") nil)
(check= (find-key-by-value 2 (list (list 1 "a") (list 2 "b"))) nil)
(check= (find-key-by-value 2 (list (cons "a" 1) (cons "b" 2))) nil)

;rev: true-list -> true-list
(defun rev (l)
  "reverses a true-list"
  (if (endp l)
    nil
    (append (rev (cdr l)) (list (car l)))))

;nth-element: nat true-list -> All
(defun nth-element (n l)
  "finds the nth element(zero indexing) in the list, returns nil
   if n >= (len l)"
  (if (endp l)
    nil
    (if (= 0 n)
      (car l)
      (nth-element (- n 1) (cdr l)))))

; nth-last-element: nat true-list -> All
;hint: define rev and another helper function
(defun nth-last-element (n l)
"Usage: Returns the n-th last element of l (counting from 0) 
 Returns nil if n >= the  length of l"
  (nth-element n (rev l)))


(check= (nth-last-element 0 '(1 2 3)) 3)
(check= (nth-last-element 2 '(1 2 3)) 1)
(check= (nth-last-element 3 '(1 2 3)) nil)
(check= (nth-last-element 0 nil) nil)
(check= (nth-last-element 7 '(1 2 3)) nil)


;; min-element-acc: LoInteger(of length >= 1) Int -> Int
;; LoInteger is a list of integers
(defun min-element-acc (l ans)
" Usage: Returns m where m <= all elements of l using an
accumulator style definition as explained in class"
  (if (endp l)
    ans
    (if (< (car l) ans)
      (min-element-acc (cdr l) (car l))
      (min-element-acc (cdr l) ans))))


(check= (min-element-acc '(3 5 7 2 12) 8) 2)
(check= (min-element-acc '(14 8 99 43) 3) 3)
(check= (min-element-acc nil 3) 3)



; DIVISIBLE-BY-REC: nat nat -> boolean
; Uses recursion to check whether x is divisible by f.
; (Hint: if f is positive and x >= f, then f divides x if and only if
;  f divides x-f)
; Either boolean value is OK if f is zero--or outside the domain
(defun divisible-by-rec (x f)
  (if (zp x)
    t;0 is divisible by any f
    (if (zp f)
      nil; lets say 0 or any other atom does not divide any x
      (if (< x f)
        nil;if x is less than f, then f does not divide x
        (divisible-by-rec (- x f) f)))))
        
    

(check= (divisible-by-rec 5 3) nil)
(check= (divisible-by-rec 55 5) t)
(check= (divisible-by-rec 5 0) nil)
(check= (divisible-by-rec 0 32) t)
(check= (divisible-by-rec 2 4) nil)


; DIVISIBLE-BY-SIMPLE: nat nat -> boolean
; (can copy tests from divisible-by-rec)
#|
 It might be tricky figuring out how to implement this one without
 recursion and using only functions you already know.  Feel free to
 discuss with classmates.  And review the arithmetic functions.
|#
(defun divisible-by-simple (x f)
"Checks whether x is divisible by f, using just a
 couple functions you have already seen."
(if (zp f)
  nil
  (natp (/ x f))))

(check= (divisible-by-simple 5 3) nil)
(check= (divisible-by-simple 55 5) t)
(check= (divisible-by-simple 5 0) nil)
(check= (divisible-by-simple 0 32) t)
(check= (divisible-by-simple 2 4) nil)

; replace-element: All All true-list -> true-list
(defun replace-element (old new l)
" Usage: Returns l with all elements that equal old replaced with new."
  (if (endp l)
    nil
    (if (equal old (car l))
      (cons new (replace-element old new (cdr l)))
      (cons (car l) (replace-element old new (cdr l))))))

(check= (replace-element 1 'one '(1 2 1 3 4 1)) '(one 2 one 3 4 one))
(check= (replace-element 2 44 nil) nil)
(check= (replace-element 2 44 '(4 44 55 65 2 77 78 2)) '(4 44 55 65 44 77 78 44))

;last-element: true-list -> All
(defun last-element (l)
  "gets the last element in l"
  (cond ((endp l);has no elements
         nil)
        ((endp (cdr l)) (car l));has only one element
        (t (last-element (cdr l)))));recur on rest i.e find last element in rest

(check= (last-element '(1 2 3)) 3)
(check= (last-element nil) nil)
(check= (last-element '(1)) 1)

(defun remove-last-element (l)
  "removes the last element from l and returns the resulting list"
  (cond ((endp l);l has no elements
         nil)
        ((endp (cdr l));l has only one element
         nil);if we remove the lone element, we return the empty list
        (t
         (cons (car l) ;remove the last element in the rest of the list
               (remove-last-element (cdr l))))))
(check= (remove-last-element '(1 2 3)) '(1 2))
(check= (remove-last-element nil) nil)
(check= (remove-last-element '(1)) nil)
                                                                                                                       
; rotate-right: true-list nat -> true-list
(defun rotate-right (l n)
"Usage: Rotate the list l to the right n times"
  (cond ((zp n)
         l);nothing left to rotate
        ((or (endp l) (endp (cdr l)));empty or single element list
         l);no point in rotating
        (t (rotate-right (cons (last-element l)
                               (remove-last-element l));one single right rotate
                         (- n 1)))));call rotate right on resulting list n-1 times

(check= (rotate-right nil 3) nil)
(check= (rotate-right '(1) 4) '(1))
(check= (rotate-right '(1 2 3 4 5 6) 3) '(4 5 6 1 2 3))
(check= (rotate-right '(1 2 3 4 5 6) 0) '(1 2 3 4 5 6 ))
(check= (rotate-right '(1 2 3 4 5 6) 6) '(1 2 3 4 5 6 ))
(check= (rotate-right '(1 2 3 4 5 6) 9) '(4 5 6 1 2 3))#|ACL2s-ToDo-Line|#