;; rewriting rules as tactics

;;; pattern-match 

;;; unify takes 4 arguments:  M1, Subj, S1, and S2, and returns a tactic.
;;; M1 and Subj are terms in internal form
;;; S1 and S2 are equal-length lists of names.
;;; returns a substitution theta on the fv's of M1 ONLY
;;; so this is like unification, except that M1 is the pattern and Subj
;;; is the subject

;;; (lambda ,S1 ,M1)theta =_alpha (lambda ,S2 ,Subj)theta
;;; if such a theta exists, we succeed and return it
;;; else we fail.

(define match
  (lambda (pat subj s1 s2)
    (cond
      ((and (const? pat) (const? subj))
       (if (equal?
             (const->datum pat)      
             (const->datum subj))
         (succeed (make-empty-subst))
         (fail)))
      ((and (var? pat) (var? subj))
       (match-two-vars pat subj s1 s2))
      ((var? pat)
       (match-one-var pat subj s1 s2))
      ((var? subj)                      ; if subj is var and pat
                                        ; isn't, then fail
       (fail))
      ((and (app? pat) (app? subj))
       (and-then
         (match (app->rator pat) (app->rator subj)
           s1 s2)
         (lambda (theta)
           (and-then
             (match (subst (app->rand pat) theta)
                    (subst (app->rand subj) theta)
                    s1 s2)
             (lambda (theta2)
               (succeed (comp-subst theta theta2)))))))
      ((and (abs? pat) (abs? subj))
       (match (abs->body pat) (abs->body subj)
         (cons (abs->bv pat) s1)
         (cons (abs->bv subj) s2)))
      (else (fail)))))

(define match-two-vars
  (lambda (v10 v20 s10 s20)             ; v1 is pattern variable
    (let ((v1 (var->sym v10))
          (v2 (var->sym v20)))
      (let loop ((s1 s10) (s2 s20))
        (cond
          ((and (null? s1) (null? s2))
           (succeed (make-unit-subst v1 v20)))
          ((or (null? s1) (null? s2))
           ;; don't fail here, raise an error immediately
           (error 'match-two-vars
             "bound-variable lists had different lengths: ~s and ~s"
             s10 s20))
          ((and (eq? v1 (car s1)) (eq? v2 (car s2)))
           (succeed (make-empty-subst)))
          ((or (eq? v1 (car s1)) (eq? v2 (car s2)))
           (fail))
          (else
            (loop (cdr s1) (cdr s2))))))))

(define match-one-var
  (lambda (vm1 subj s1 s2)
    (let ((v1 (var->sym vm1)))
      (if
        (and
          (not (memq v1 s1))
          (not (non-empty-intersection?
                 s2
                 (fv subj)))
          )
        (succeed (make-unit-subst v1 subj))
        (fail)))))

(define test-match
  (lambda (t1 t2)
    (let ((t1 (parse t1))
          (t2 (parse t2)))
      (run-tac
        (match t1 t2 '() '())
        (lambda (theta)
          (display* theta
            (unparse (subst t1 theta)) 
            (unparse t2)))
        (lambda () 'non-matchable)))))

(define rewrite1                      ; lhs * rhs -> term -> tac
  (lambda (lhs rhs)
    (lambda (term)
      (and-then
        (match lhs term '() ())
        (lambda (theta)
          (succeed (subst rhs theta)))))))

(define rule1
  (rewrite1
    (parse '("S" x y z))
    (parse '((x z) (y z)))))

(define test-tacfn
  (lambda (term tacfn)
    (run-tac
      (tacfn (parse term))
      unparse
      (lambda () 'failed))))

(define rewrite-rules                   ; rules -> term -> tac
  (lambda (rules)
    (lambda (term)
      (let loop ((rules rules))
        (if (null? rules)
          (fail)
          (or-else
            ((rewrite1
               (car (car rules))
               (cadr (car rules)))
             term)
            (loop (cdr rules))))))))
  
(define sk-rules
  `((,(parse '("S" x y z))
     ,(parse '((x z) (y z))))
    (,(parse '("K" x y))
     ,(parse 'x))))

(define cll                             ; combinator leftmost
                                        ; term -> tac
  (leftmost (rewrite-rules sk-rules)))


(define cll*
  (repeat cll))

(define parse-rules
  (lambda (pairs-of-terms)
    (map (lambda (pair)
           (list (parse (car pair))
                 (parse (cadr pair))))
         pairs-of-terms)))

(define ih
  (leftmost
    (rewrite-rules
      (parse-rules
        '((("a1" symtab pi u zeta kappa)
           ("b1" (lambda (id) (symtab (u id)))
                 (lambda (z) (pi u ("cons" z zeta) kappa))))
          (("a2" symtab pi u zeta kappa)
           ("b2" (lambda (id) (symtab (u id)))
                 (lambda (z) (pi u ("cons" z zeta) kappa))))
          (("add" pi u ("cons" z2 ("cons" z1 zeta)) kappa)
           (pi u ("cons" ("plus" z1 z2) zeta) kappa)))))))

(define rule2
  (rewrite-rules
    (parse-rules
      '((('a x) ('b x))))))