;; Nada Amin (namin@mit.edu)
;; 6.945 Problem Set 5
;; Due: Wed. 12 Mar. 2008

(load "../test-manager/load.scm")
(load "load.scm")

;; Problem 5.1
#|

For match:and, the dictionary will get passed from one match to the
next, while, for match:or, it will be routed to all the matches in
parallel. The rationale is that, for a match:or, the user only cares
about the combinator that succeeds, while for a match:and, it cares
about all of them. For match:and, an alternative would be to try to
combine the dictionary at the end, but, there might be a conflict, and
in that case, the user probably intented all combinators to use the
dictionary consistently, so passing the dictionary from one match to
the next will do the right thing.

For match:and, in case of success, another design issue is what to
return if the number of tokens eaten by each combinator differ. My
choice is to return the max number of tokens eaten, the rationale
being that (a) the user would want to move forward as much as possible, 
(b) the base case (null? combinators) eats no token at all, so min
wouldn't make sense.

|#

;; A.
(define (match:and . combinators)
  (lambda (data dictionary succeed)
    (if (null? combinators)
        (succeed dictionary 0)
        (let ((c (car combinators))
              (cs (cdr combinators)))
          (c data dictionary 
             (lambda (dictionary n1)
               ((apply match:and cs)
                data dictionary
                (lambda (dictionary n2)
                  (succeed dictionary (max n1 n2))))))))))

;; B.
(define (match:or . combinators)
  (lambda (data dictionary succeed)
    (if (null? combinators)
        #f
        (let ((c (car combinators))
              (cs (cdr combinators)))
          (or (c data dictionary succeed)
              ((apply match:or cs) data dictionary succeed))))))
;; C.
(define (compile-match-and pattern use-env loop)
  `(match:and ,@(map loop (cdr pattern))))

(eq-put! '?and 'pattern-keyword compile-match-and)

(define (compile-instantiate-and skel use-env loop)
  `(instantiate:and ,@(map loop (cdr skel))))

(eq-put! '?and 'template-keyword compile-instantiate-and)

(define (compile-match-or pattern use-env loop)
  `(match:or ,@(map loop (cdr pattern))))

(eq-put! '?or 'pattern-keyword compile-match-or)

(define (compile-instantiate-or skel use-env loop)
  `(instantiate:or ,@(map loop (cdr skel))))

(eq-put! '?or 'template-keyword compile-instantiate-or)

;; D.
#|
Honestly, I am having trouble coming up with interesting examples...

(define match:test-and
  (compile-and-run-pattern
   '(?and (++ #!rest (? a not-zero?)) (** #!rest (? a not-zero?)))))

(define (and-test expression)
  (match:test-and
   (list (default-simplify expression))
   '()
   (lambda (dict n)
     (pp dict)
     #f)))

(and-test '(* 3 2))
;((a 6))
;Value: #f

(define match:test-or
  (compile-and-run-pattern
   '(?or (++ #!rest (? a not-zero?)) (** #!rest (? a not-zero?)))))

(define (or-test expression)
  (match:test-or
   (list (default-simplify expression))
   '()
   (lambda (dict n)
     (pp dict)
     #f)))

(or-test '(* 3 2))
;((a 6))
;((a 6))
;Value: #f
|#

;; Problem 5.2

(define distribute-common-factors
  (rule-simplifier
   (list

    (rule (+ (* (?? s1) (? a) (?? t1)) 
             (* (?? s2) (? a) (?? t2)) 
             (?? r))
          none
          (+ (* (: a) (+ (* ,@(: s1) ,@(: t1)) 
                         (* ,@(: s2) ,@(: t2)))) 
             ,@(: r)))

    (rule (+ (?? r1) 
             (? a) 
             (?? r2) 
             (* (?? s1) (? a) (?? t1))
             (?? r3))
          none
          (+ (* (: a) (+ 1 (* ,@(: s1) ,@(: t1))))
             ,@(: r1)
             ,@(: r2)
             ,@(: r3)))

    (rule (+ (?? r1) 
             (* (?? s1) (? a) (?? t1))
             (?? r2) 
             (? a) 
             (?? r3))
          none
          (+ (* (: a) (+ 1 (* ,@(: s1) ,@(: t1))))
             ,@(: r1)
             ,@(: r2)
             ,@(: r3)))

    (rule (+ (? a))
          none
          (: a))

    (rule (* (? a))
          none
          (: a))

    (rule (+ (?? as) (+ (?? bs)) (?? cs))
          none
          (+ ,@(: as) ,@(: bs) ,@(: cs)))
    

    (rule (* (?? as) (* (?? bs)) (?? cs))
          none
          (* ,@(: as) ,@(: bs) ,@(: cs)))
    
    )))


#|
(define test-dcf
  (compose distribute-common-factors default-simplify))

(test-dcf '(+ (* (? y) (? x) (? a)) (* (? y) (? z) (? x))))
;Value: (* (? x) (? y) (+ (? a) (? z)))

(test-dcf '(+ (* (? y) (? x) (? a)) (* (? y) (? z) (? x)) (? y)))
;Value: (* (? y) (+ 1 (* (? a) (? x)) (* (? x) (? z))))
;; N.B. this shows that the rules only distribute the common factors at the outermost level.
|#

(define (match:product . factor-combinators)
  (define (product-imaginer expr dictionary succeed)
    (cond ;;
          ;; Stub...
          ;; Maybe add more cases later...
          ;;
          (else #f)))
  ;; Try to convert expression to a product before match.
  (match:transform
   (compose distribute-common-factors default-simplify)
   (match-subexpressions 'MATCH:PRODUCT
                         product? '* (lambda () 1)
                         product-imaginer
                         factor-combinators)))

;; Problem 5.3

;; A.

#|

It is useful to introduce a unification variable, 
in case we're re-using the imagined part somewhere else.
Here is an example:

(define match:test-unif
  (compile-and-run-pattern
   '(++ (// (? n) (? d)) (? d))))

(define (unif-test expression)
  (match:test-unif
   (list (default-simplify expression))
   '()
   (lambda (dict n)
     (pp dict)
     #f)))

(unif-test '(? x))
;((($$$ 1) (? x)) (d ($$$ 1)) (n 0))
;Value: #f

Without the unification, this general solution wouldn't be found --
perhaps the variable x would have to be arbitrarily instantiated.

(unif-test '1)
;((($$$ 2) 0) (d ($$$ 2)) (n ($$$ 2)))
;((($$$ 3) 1) (d ($$$ 3)) (n 0))
;((d 1) (n 0))
;Value: #f

The first solution is bad, because d = 0 effectively.
This is solved now. Note that writing

(define match:test-unif
  (compile-and-run-pattern
   '(++ (// (? n) (? d not-zero?)) (? d not-zero?))))

actually solves the problem, but not writing

(define match:test-unif
  (compile-and-run-pattern
   '(++ (// (? n) (? d not-zero?)) (? d))))

because the unification doesn't take into account the predicate.

|#

;; B.

(define (unknown->not-zero-unknown u)
  (list '!!!
        (cadr u)))

(define (match:unknown? pattern)
  (and (pair? pattern)
       (or (eq? (car pattern) '$$$)
           (eq? (car pattern) '!!!))))

(define (not-zero-unknown)
  (unknown->not-zero-unknown (unknown)))

(define (match:not-zero-unknown? pattern)
  (and (pair? pattern)
       (eq? (car pattern) '!!!)))

(define (extend-if-possible var val dictionary)
  (let ((binding1 (match:lookup var dictionary)))
    (cond (binding1
           (match:unify (match:value binding1) val dictionary))
          ((match:unknown? val)
           (let ((binding2 (match:lookup val dictionary)))
             (if binding2
                 (match:unify var (match:value binding2) dictionary)
                 (if (match:not-zero-unknown? var)
                     (match:bind val var dictionary) ;; swap to make sure non-zero constraint gets propagated
                     (match:bind var val dictionary)))))
          ((unify:depends-on? val var dictionary) #f)
          (else (if (and (match:not-zero-unknown? var) (eq? '0 val))
                    #f
                    (match:bind var val dictionary))))))

(define (match:quotient numerator-combinator denominator-combinator)
  (let ((operands-matcher
         (match:list numerator-combinator denominator-combinator)))
    (define (quotient-defaultify expr) `(,expr 1))
    (define (quotient-match data dictionary succeed)
      (match-binary-args 'MATCH:QUOTIENT
                         quotient? '/ quotient-defaultify
                         quotient-imaginer
                         operands-matcher
                         data dictionary succeed))
    (define (quotient-imaginer expr dictionary succeed)
      ;;
      ;; Should restrict unknowns below to be nonzero denominators.
      ;;
      (cond ((expr:zero? expr)
             (operands-matcher (list (list 0 (not-zero-unknown)))
                               dictionary
                               succeed))
            ((expr:one? expr)
             (let ((x (not-zero-unknown)))
               (operands-matcher (list (list x x))
                                 dictionary
                                 succeed)))
            ;;
            ;; Maybe add more cases later...
            ;;
            (else #f)))
    (match:transform default-simplify quotient-match)))

#|
(define match:test-unif
  (compile-and-run-pattern
   '(++ (// (? n) (? d)) (? d))))

(define (unif-test expression)
  (match:test-unif
   (list (default-simplify expression))
   '()
   (lambda (dict n)
     (pp dict)
     #f)))

(unif-test '(? x))
;((($$$ 1) (? x)) (d ($$$ 1)) (n 0))
;Value: #f

(unif-test '1)
;((($$$ 3) 1) (d ($$$ 3)) (n 0))
;((d 1) (n 0))
;Value: #f
|#

;; Problem 5.4

(define (match:product . factor-combinators)
  (define (product-imaginer expr dictionary succeed)
    (cond ((expr:zero? expr)
           ((match-args '* (lambda () (unknown)) factor-combinators)
            (list (list 0))
            dictionary
            succeed))
          ;; Maybe add more cases later...
          ;;
          (else #f)))
  ;; Try to convert expression to a product before match.
  (match:transform
   default-simplify
   (match-subexpressions 'MATCH:PRODUCT
                         product? '* (lambda () 1)
                         product-imaginer
                         factor-combinators)))

#|
;;; Test cases

(define match:quadratic
  (compile-and-run-pattern
   '(++ (** (^^ (? var not-numeric?) 2) #!rest (? a not-zero?))
        (** (? var) #!rest (? b))
        #!rest (? c))))

(define (quadratic-test expression)
  (match:quadratic
   (list (default-simplify expression))
   '()
   (lambda (dict n)
     (and (= n 1)
          (let ((a (match:value (match:lookup 'a dict)))
                (b (match:value (match:lookup 'b dict)))
                (c (match:value (match:lookup 'c dict)))
                (var (match:value (match:lookup 'var dict))))      
            (and (indep-of? a var)
                 (indep-of? b var)
                 (indep-of? c var)
                 (pp dict)))
          #f))))

(quadratic-test '(+ (expt x 2) (* 2 x) 3))
((c 3) (b 2) (a 1) (var x))
;Value: #f

(quadratic-test '(expt x 2))
((c 0) (b 0) (($$$ 1) x) (a 1) (var x))
;Value: #f
;;; See problem 5.4

(quadratic-test '(+ (expt x 2) (* 2 x y) (expt y 2)))
((c (expt y 2)) (b (* 2 y)) (a 1) (var x))
((c (expt x 2)) (b (* x 2)) (a 1) (var y))
;Value: #f

(quadratic-test '(+ (* 2 (expt x 2)) (* (sqrt 2) (expt x 2)) 3))
((c 3) (b 0) (($$$ 19) x) (a (+ 2 (sqrt 2))) (var x))
#f 
;;; See problem 5.4

(quadratic-test '(+ (* 2 (expt x 2)) (* a (expt x 2)) 3))
;Value: #f
;;; See problem 5.5

(quadratic-test '(+ (* 2 (expt x 2)) (* 2 x) 3))
((c 3) (b 2) (a 2) (var x))
;Value: #f

(quadratic-test '(+ (* 2 x) (* 2 (expt x 2)) 3))
((c 3) (b 2) (a 2) (var x))
;Value: #f

(quadratic-test '(+ (* 2 x) 3 (* 2 (expt x 2) y)))
((c 3) (b 2) (a (* 2 y)) (var x))
;Value: #f

(quadratic-test '(+ (expt x 2) (* 2 x (sin x))))
;Value: #f

(quadratic-test '(* (+ x y) (- x y)))
((c (* -1 (expt y 2))) (b 0) (($$$ 27) x) (a 1) (var x))
((c (* (expt x 2))) (b 0) (($$$ 30) y) (a -1) (var y))
;Value: #f
;;; See problem 5.4

(quadratic-test '(* (+ x y) (- x y) x))
((c (* (expt x 3))) (b 0) (($$$ 40) y) (a (* x -1)) (var y))
;Value: #f
;;; See problem 5.4
|#

;; Problem 5.5

#|

To solve

(quadratic-test '(+ (* 2 (expt x 2)) (* a (expt x 3)) 3))

we need to collect like-terms in order to suit the pattern
matcher. The issue is that what consitutes like-terms depends on the
problem. Here, we're matching

(++ (** (^^ (? var not-numeric?) 2) #!rest (? a not-zero?))
        (** (? var) #!rest (? b))
        #!rest (? c))))

so it makes sense to collect terms of the form (expt x 2). This is
tricky to implement. We'd have to make the collection of terms
contingent upon the pattern to match.

To solve the third case (var (+ x y)) of

(quadratic-test '(+ (expt x 2) (* 2 x y) (expt y 2)))

is even trickier. We have to realize that we can combine two
subexpressions x and y into a form (+ x y) that never appears as such
in the problem. We could try a brute-force approach (attempt all
possible combinations of two subexpressions, etc.) but that's not very
satisfying. I suppose we could filter the brute-force combinations by
looking at just multiplications: here, we have (* 2 x y) so it would
make sense to only search for possible additive combinations from the
set (2,x,y), which would include (+ x y) . However, this solution is
problem-specific.

|#