#|
CSU290 Homework 1 - Fall 2008

Student name:  TODO: PUT YOUR NAME HERE

For this homework, you will need to use ACL2s.  See the class web page
and http://acl2s.peterd.org/acl2s/doc/ for more info on how to get it
on your own computer and how to run it in the CCIS computer labs.  Also,
if you installed ACL2s before 9/16, you must upgrade to the latest version
for CHECK= to work. See http://acl2s.peterd.org/acl2s/doc/#update_plugin

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

You should edit this file in ACL2s as hwk1.lisp.  You have a couple options:

Option 1:
  Once you have a project, create a new ACL2s/Lisp file called hwk1.lisp,
      *** Be sure to choose "Programming" session mode! ***
  You should use that session mode until further notice.  The other defaults
  are fine.  With hwk1.lisp editor open, select, copy and paste the contents
  of this file (probably from your web browser) to that editor.  Go ahead
  and save.

Option 2:
  Make sure you have a project in your Eclipse workspace.  Find out
  where it is on your system (in the Navigator, right click your project,
  click "Properties", and look at the "Location").  Download and save this
  file in that project location.  For Eclipse to notice the new file,
  right click the project and click "Refresh".  Now double-click hwk1.lisp
  to open it.  Type Ctrl+Shift+o (Mac: Cmd+Shift+o) (the letter o) and
  confirm that you want to create an associated session.  Go to the menu
  ACL2s -> Set session mode... and choose "Programming".  You should use
  that session mode until further notice.

Ok.  Now you should be able to tweak the rest 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 if input is complete.
|#

; Numbers - basics

(check= (+ 2 2) #)
(check= (- 5) #)
(check= (/ 10 5) #)
(check= (* 5 1/2) #)
(check= 0/376 #)
(check= -4/8 #)

; Numbers - destructors for rationals

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

; Numbers - predicates (these are t or nil)

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

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

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

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

(check= (rationalp 3/2) #)
(check= (rationalp 42) #)
(check= (rationalp nil) #)


; Booleans  (these are t or nil)

(check= (equal 0 nil) #)
(check= (equal nil Nil) #)
(check= (equal 3 6/2) #)
(check= (and t nil) #)
(check= (and t t) #)
(check= (and t t nil t) #)
(check= (and nil) #)
(check= (or t nil) #)
(check= (or t t) #)
(check= (or t t nil t) #)
(check= (or nil) #)
(check= (not t) #)
(check= (not nil) #)
(check= (not 0) #)



; Identity elements

(check= (+) #)
(check= (*) #)
(check= (or) #)
(check= (and) #)



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Part 2: Defining functions
;
; Fill in these function definitions, and fill in tests as examples.
; 
; You 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.
;
; Note that a type such as ``nat'' refers to something satisfying the
; NATP predicate, which is a natural number.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; F->C: rational -> rational
; Converts Fahrenheit temperatures to Celsius
; Celsius = (Fahrenheit - 32) * 5/9
; (construct tests as examples before writing function)
(defun f->c (f)
  #)

(check= (f->c #) #)
(check= (f->c #) #)
(check= (f->c #) #)
(check= (f->c #) #)


; GCF: nat nat -> nat
; Finds the greatest common factor of two naturals using Euclid's
; original algorithm of repeated subtraction.  For an imperative
; description see
; http://en.wikipedia.org/w/index.php?title=Euclidean_algorithm&oldid=237106509#Original_algorithm
; (construct tests as examples before writing function)
(defun gcf (a b)
  #)

(check= (gcf # #) #)
(check= (gcf # #) #)
(check= (gcf # #) #)
(check= (gcf # #) #)
(check= (gcf # #) #)


; 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
; (construct tests as examples before writing function)
(defun divisible-by-rec (x f)
  #)

(check= (divisible-by-rec # #) #)
(check= (divisible-by-rec # #) #)
(check= (divisible-by-rec # #) #)
(check= (divisible-by-rec # #) #)
(check= (divisible-by-rec # #) #)


; DIVISIBLE-BY-SIMPLE: nat nat -> boolean
; Checks whether x is divisible by f, using just a
; couple functions discussed in class.
; (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)
  #)

(check= (divisible-by-simple # #) #)
(check= (divisible-by-simple # #) #)
(check= (divisible-by-simple # #) #)
(check= (divisible-by-simple # #) #)
(check= (divisible-by-simple # #) #)





;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Part 3: Evaluates to <?> (again)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; Lists - basics (these are t or nil)

(check= (equal nil ()) #)
(check= (endp nil) #)
(check= (endp 12) #)
(check= (endp "hi") #)
(check= (endp '(3)) #)
(check= (true-listp nil) #)
(check= (true-listp 12) #)
(check= (true-listp "hi") #)
(check= (true-listp '(3)) #)
(check= (true-listp (cons 1 2)) #)