;; 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= (/ 3 2) #)
;
; should become
;
;   (check= (/ 3 2) 3/2)
;
; 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.



(check= (booleanp t) #)

(check= (booleanp nil) #)
(check=  (booleanp 7) #) 


(check=  (symbolp t)         #) 
(check=  (symbolp nil)    #) 
(check=  (atom t)   #)
(check=  (consp nil)
(check=  (equal nil nil) 
(check=  (equal nil t) 
(check=  (equal T t)         #)     

 (check= (+ 5)
 (check= (+ 3 2 1)
 (check= (* -2)  
 (check= (* 1 2 3)
 (check= (+)     
 (check= (*)    


(check=  (- 5)    
(check=  (- -10)  
(check=  (- 0)    
(check=  (/ 1)    
(check=  (/ 5)    
(check=  (/ -2/3) 

(check=  (equal 7/9 14/18)
(check=  (equal 8/2 4)    




(check= (* (- (+ 6 12) 1) 2) #)
(check= -2/8 #)
(check= (* 5 1/3) #)


; Numbers - predicates (these are t or nil)

(check= (integerp -1) #)
(check= (integerp 3/2) #)
(check= (natp 1) #)
(check= (natp 6/2) #)
(check= (zp nil) #)
(check= (zp 0000) #)

(check= (posp 0) #)
(check= (posp 4/2) #)

(check= (integerp (first (rest (list -12 "b" "a" 0 43))))             #)


; Booleans and and/or functions
(check= (not 0) #)
(check= (and t (not nil) 13 (zp -1) 1/7) #)
(check= (or (not 4) (natp -1) 0 1/7 (not t)) #)


; Lists: constructors and destructors

(check= (first (cons 2 (cons 1 nil)))                 #)
(check= (first (rest (cons 3 (list 2 1)))) #)
(check= (rest (list nil))                          #)
(check= (rest (cons nil nil)) #)
(check= (rest nil)) #)
(check= (first 123)                                   #)

; TrueLists: predicates

(check= (true-listp (cons (list 1 2) nil))        #)
(check= (true-listp 11)                  #)
 
(check= (endp "qqq")                    #)
(check= (endp -0) #)

(check= (consp (list 12)) #)
(check= (consp (list) #))

;quotes
(check= (equal '1 ''1) #)
(check= (equal "ok" '"ok") #)
(check= (equal -3 '-3) #)
(check= (equal  bb 'bb) #) ;is this a static error? if yes comment it out
(check= (equal (f 3) '(f 3)) #) ;is this  a static error?  yes comment it out
(check= (equal 'a ''a) #)
(check= (equal (list 1 2 3) '(1 2 3)) #)
(check= (equal (list 'a 'b) '(a b)) #)
(check= (equal '(1 2 3) (quote (1 2 3))) #)
(check= (car (car '('(1 2) '(3) '(4 5 6)))) #)
(check=  (car (car '((1 2) (3) (4 5 6)))) #)


(defun foo (x) (list x 'x))
(check= (foo 3) #)

;; Part 2: Recursive Definitions

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



; number-elements: true-list -> NumberedList
; NumberedList is a list of 2-element lists
; Implementation details: recursively define an auxiliary
; function whose second argument is the index.

(defun number-elements (l)
"Usage: Here is an example of how this works. Given the list
 (a b c) number-elements should return ((0 a) (1 b) (2 c)).
 In general, given a list l, number-elements numbers the
 elements of l by returning a 2-element list whose first element
 is the index, say n, and whose second element is the nth
 element of l. Indexing starts from 0."
  #)

; in: All true-list -> Boolean
(defun in (x l)
"Usage: Searches l for x and returns t if it is found, nil otherwise. "
  #)

; rem-dups: true-list -> true-list
(defun rem-dups (l)
"Usage: Returns a new list which is l without the duplicate elements"
  #)

; ordered-elementp: true-list -> Boolean
(defun ordered-elementp (l)
"Usage: Returns true if x is ordered with the relation <, nil otherwise."
  #)

; merge-ordered: OrderedList OrderedList -> OrderedList
; OrderedList is a list of elements ordered with the relation <
(defun merge-ordered (l1 l2)
"Usage: Returns a list containing the elements in l1 l2, ordered with the relation <"
  #)