#|

Challenge problem 1.

This challenge problem is an extension of the lab03 simple arithmetic
expression interpreter that deal with errors.

It is intentionally more open-ended that labs and homeworks to force
you to make design decisions. So, expect to do some amount of design
exploration.

Do not try this unless you completed all of lab03.

We will define an interpreter for simple arithmetic expressions.

An arithmetic expressions, aexpr, is one of the following:

- a rational number (we use the builtin type rational)
- a variable (we use the builtin type var)
- a list of the form 
  (- <aexpr>)
  where <aexpr> is an arithmetic expression

- a list of the form
  (<aexpr> <oper> <aexpr>)
  where <oper> is one of +, -, *, or / 
  and both <aexpr>'s are arithmetic expressions.

|#

(set-defunc-function-contract-strictp nil)
(set-defunc-body-contracts-strictp nil)

;; Unary operators
(defdata uoper '-)

;; Binary operators
(defdata boper (enum '(+ * - /)))

;; Arithmetic expressions
(defdata
  (u-aexpr (list uoper aexpr))
  (b-aexpr (list aexpr boper aexpr))
  (aexpr (oneof rational var u-aexpr b-aexpr)))

;; Some sanity checks.
;; We are checking that an aexpr satisfies exactly one of the oneof
;; types in its definition. defdata-disjoint checks that two types are
;; disjoint. 
(defdata-disjoint rational var)
(defdata-disjoint rational u-aexpr)
(defdata-disjoint rational b-aexpr)
(defdata-disjoint var u-aexpr)
(defdata-disjoint var b-aexpr)
(defdata-disjoint u-aexpr b-aexpr)

;; An assignment is an alist from vars to rationals.
(defdata assignment (alistof var rational))

;; A function to lookup a var in an assignment, with d as the default
;; value.
(definec lookup (v :var a :assignment d :rational) :rational
  (cond ((endp a) d)
        ((equal (caar a) v)
         (cdar a))
        (t (lookup v (cdr a) d))))

;; Define aeval, a function that given an aexpr and an assignment
;; evaluates the expression, using the assignment to assign values to
;; var's.  If a var appears in the aexpr but not in the assignment,
;; then the value of the var should be 1.

;; A difference with lab03 is that we allow division, so we have to
;; deal with divide by 0. If a divide by 0 occurs during the
;; evaluation of an expression, we will return an error. We will do
;; that by just returning the symbol error. To support that we will
;; define the following types.

(defdata er 'error)
(defdata rat-err (oneof rational er))

;; Define the function aeval: given an aexpr, e, and an assigment, a,
;; aeval returns something of type rat-err, by evaluating the
;; expression, as per the comments above. You can define helper
;; functions as needed.
(definec aeval (e :aexpr a :assignment) :rat-err
  ...)

(check= (aeval '((x + y) - (- z))
               '((y . 3/2) (z . 1/2)))
        3)

(check= (aeval '((x + y) / (- z))
               '((y . 3/2) (z . 0)))
        'error)

;; Specify the following properties using aeval. 
;; 1. -x = -(-(-x)), for symbol x
(test? ...)

;; 2. (x - y) = (x + (- y)), for vars x, y
(test? ...)

;; 3. (x * (y + z)) = ((x * y) + (x * z)), for aexpr's x, y, z
(test? ...)

;; 4. (1 / (x / y)) = (y / x), for aexpr's x, y
(test? ...)

;; Notice that 4 is not true! Why not? See counterexamples, so how do
;; we make it true? See 5.

;; 5. (1 / (x / y)) = (y / x), for aexpr's x, y, unless there is an error
;; Feel fre to define functions if needed.
(test? ...)

;; Since it is possible to generate errors, we often want to prove
;; that an error cannot occur, so rephrase properties 1-3 above to
;; also state that the aevals in your formalization do not lead to
;; errors (or equivalently that they return rationals).

;; 1a. -x = -(-(-x)), for symbol x 
(test? ...)

;; 2a. (x - y) = (x + (- y)), for vars x, y 
(test? ...)

;; 3a. (x * (y + z)) = ((x * y) + (x * z)), for aexpr's x, y, z
(test? ...)

;; Rephrase property 5 to more directly account for errors.  To do
;; this, define two properties.

;; The first property, 5a, is like property 5, but it has an extra
;; hypothesis, which can be an and/or. Also the conclusion states that
;; no errors occur. The added hypothesis should be be minimally
;; restrictive, eg, (natp x) is more restrictive than (rationalp x).

;; The second property, 5b, is like 5a, except the extra hypothesis
;; you added in 5a is negated and the conclusion states that the aeval
;; of at least one of (1 / (x / y)), (y / x) leads to an error.

;; 5a. 
(test? ...)

;; 5b.
(test? ...)