; term: "2-unify.scm"
; This is just the datatype for term. There are variable terms ("x", "foo", etc),
; constant terms (1, 2, #f, etc), and application terms ((func arg), (bar quux))
(define-datatype term term?
  (var-term
    (id symbol?))
  (constant-term
    (datum constant?))
  (app-term
    (terms (list-of term?))))


; unify-term: "2-unify.scm"
; This is the function that does the actual unification
; Anything can be substituted for a variable term as long as the
; variable being substituted for doesn't appear in the substitution
; A constant term can be substituted for an identical constant 
; An application term can be substituted with another application term
; if each component can also be unified
(define unify-term
  (lambda (t u)
    (cases term t
      (var-term (tid)
        (if (or (var-term? u) (not (memv tid (all-ids u))))
          (unit-subst tid u)
          #f))
      (else
        (cases term u
          (var-term (uid) (unify-term u t))
          (constant-term (udatum)
            (cases term t
              (constant-term (tdatum)
                (if (equal? tdatum udatum) (empty-subst) #f))
              (else #f)))
          (app-term (us)
            (cases term t
              (app-term (ts) (unify-terms ts us))
              (else #f))))))))

; constant?: "2-unify.scm"
; The constant? predicate checks if a value is a valid "constant" 
; (number, boolean, string, or null)
(define constant?
  (lambda (x)
    (or (boolean? x) (number? x) (string? x) (null? x))))

; var-term?: "2-unify.scm"
; The var-term? predicate checks if a term is a variable term
(define var-term?
  (lambda (t)
    (cases term t
      (var-term (id) #t)
      (else #f))))

; all-ids: "2-unify.scm"
; all-ids returns a list of all the identifiers used in a term
(define all-ids
  (lambda (t)
    (cases term t
      (var-term (id) (list id))
      (constant-term (datum) '())
      (app-term (ts) (all-ids-terms ts)))))

; all-ids-terms: "2-unify.scm"
; all-ids-terms retuns a list of all the unique identifiers in a list of terms
(define all-ids-terms
  (lambda (ts)
    (map-union all-ids ts)))

; unit-subst: "2-unify.scm"
; unit-subst returns a substitution for a single symbol with a term
(define unit-subst
  (lambda (id new-term)
    (lambda (id2)
      (if (eq? id2 id) new-term (var-term id2)))))

; empty-subst: "2-unify.scm"
; empty-subst is the empty substitution 
(define empty-subst
  (lambda ()
    (lambda (id) (var-term id))))

; compose-subst: "2-unify.scm"
; compose-substs composes two substitutions
; it returns a substitution that applies s1 then s2
(define compose-substs
  (lambda (s1 s2)
    (lambda (id)
      (subst-in-term (apply-subst s1 id) s2))))

; apply-subst: "2-unify.scm"
; apply-subst applies a substitution to an identifier
(define apply-subst
  (lambda (subst id)
    (subst id)))

; unify-terms: "2-unify.scm"
; unify-terms unifies a list of terms of equal length
; two empty lists result in an empty substitution
; an empty and non-empty list results in no substitution
; anything else results in the substitution for the car of each list 
; composed with the substitution for the rest of each list
(define unify-terms
  (lambda (ts us)
    (cond
      ((and (null? ts) (null? us)) (empty-subst))
      ((or (null? ts) (null? us)) #f)
      (else 
        (let ((subst-car (unify-term (car ts) (car us))))
          (if (not subst-car)
            #f
            (let ((new-ts (subst-in-terms (cdr ts) subst-car))
                  (new-us (subst-in-terms (cdr us) subst-car)))
              (let ((subst-cdr (unify-terms new-ts new-us)))
                (if (not subst-cdr)
                  #f
                  (compose-substs subst-car subst-cdr))))))))))

; map-union: "2-unify.scm"
; map-union maps a function that returns a list to every element of a list
; the result is the union of the results of each application result
(define map-union
  (lambda (f ls)
    (cond
      ((null? ls) '())
      (else (union (f (car ls)) (map-union f (cdr ls)))))))


; union: "2-unify.scm"
; union finds the union of two sets (represented as lists)
(define union
  (lambda (set1 set2)
    (cond
      ((null? set1) set2)
      ((memv (car set1) set2) (union (cdr set1) set2))
      (else (cons (car set1) (union (cdr set1) set2))))))

; subst-in-terms: "2-unify.scm"
; subst-in-terms maps a substitution to every term in a list of terms
(define subst-in-terms
  (lambda (ts subst)
    (map (lambda (t) (subst-in-term t subst)) ts)))

; subst-in-term: "2-unify.scm"
; subst-in-term runs a substitution on a single term
; var-terms get their symbol mapped with apply-substs
; constant terms are unchanged
; application terms have each component run against the substitution
(define subst-in-term
  (lambda (t subst)
    (cases term t
      (var-term (id)
        (apply-subst subst id))
      (constant-term (datum)
        (constant-term datum))
      (app-term (ts)
        (app-term (subst-in-terms ts subst))))))

; valid-substs checks is a substitution is "valid"
; this is used for sanity checks in the test framework
; for THIS implementation a substituton is a procedure so this is the 
; best check we can do
(define valid-subst procedure?)