; On suppose juste que les prédicats de meme noms ont tous le meme nombre
;  d'expressions.
;

(define exp1 '(f ?x (g ?y (h a)) b))

(define var1 '?x)
(define var2 '?y)
(define var3 '?z)

(define int1 42)
(define con1 'q)


(define
  (terme:variable? u)
  (cond ( (not (symbol? u)) #f) 
        (else (string=? "?" (substring (symbol->string u) 0 1)))
  )
)

(define
  (terme:constante? u)
  (cond ( (integer? u) #t)
        ( (not (symbol? u)) #f)
        (else (not (terme:variable? u)))
  )
)

(define
  (terme:predicat p)
  (cond ( (terme:variable? p) #f)
        ( (terme:constante? p) #f)
        (else (car p))
  )
)

(define
  (terme:fils-liste p)
  (cond ( (terme:variable? p) #f)
        ( (terme:constante? p) #f)
        (else (cdr p))
  )
)
;
; Some special occur check
(define
  (some-oc f u l)
  (if (null? l)
      #f
      (or (f u (car l)) 
          (some-oc f u (cdr l))
      )
  )
)

;
; On cherche u dans p
(define
  (occur-check u p)
  (cond ( (terme:variable? p) (equal? u p))
        ( (terme:constante? p) (equal? u p))
        (else (some-oc occur-check u (terme:fils-liste p))) 
  )
)

;
; Dans une liste l, remplace les occurences de e par f
(define
  (remplace e f l)
  (cond ( (and (list? l) 
               (not (null? l))) 
          (append (cons (remplace e f (car l)) '()) (remplace e f (cdr l))))
        ( (equal? l e) f)
        (else l)
  )
)
(remplace '?x '?y '(f ?x (h ?x ?x) ?x))

(define
  (nouvelle-pile pile expr1 expr2)
  (if (null? pile)
      '()
      (cons (remplace expr2 expr1 (car pile)) 
            (nouvelle-pile (cdr pile) expr1 expr2))
  )
)

(define
  (nouvelle-pile-4cas pile expr1 expr2)
  (if (null? expr1)
      pile
      (nouvelle-pile-4cas (append pile (cons (car expr1) 
                                       (cons (car expr2) '())))
                          (cdr expr1) (cdr expr2))
  )
)

(nouvelle-pile '(a ?y) 'a '?y)

(define
  (r-nouvel-pgu pgu expr1 expr2)
  (if (null? pgu) 
      '()
      (cons (remplace expr2 expr1 (car pgu)) 
            (r-nouvel-pgu (cdr pgu) expr1 expr2))
  )
)

(define
  (nouvel-pgu pgu expr1 expr2)
  (append (r-nouvel-pgu pgu expr1 expr2) (cons expr1 (cons expr2 '())))
)

(define
  (unific pile pgu)
  (if (null? pile) 
       pgu 
; La pile est ainsi: '(p1 p2 p3 p4 p5 p6) ou p1 = p2, p3 = p4, p5 = p6
; On recupere la 1ere equation, les 2 membres et on les separe
       (let ( (expr1 (car pile))
              (expr2 (car (cdr pile)))
              (pile  (cdr (cdr pile)))
            )
; 1 er cas, X et Y sont deux expressions identiques
            (cond ( (equal? expr1 expr2) (unific pile pgu))

; 2 nd cas, X est une variable absente de Y
                  ( (and (terme:variable? expr1)
                         (not (occur-check expr1 expr2))
                    ) 
(begin
  (display "cas 2\n")
                    (unific (nouvelle-pile pile expr2 expr1) 
                            (nouvel-pgu pgu expr2 expr1))
)
                  )

; 3 em cas, Y est une variable absente de X
                  ( (and (terme:variable? expr2)
                         (not (occur-check expr2 expr1))
                    )
(begin
  (display "cas 3\n")
  (display "nouv pgu:")
  (display pgu)
  (display " ")
  (display expr1)
  (display " ")
  (display expr2)
  (display " = ")
  (display (nouvel-pgu pgu expr1 expr2))
  (display "\n")
                    (unific (nouvelle-pile pile expr1 expr2)
                            (nouvel-pgu pgu expr1 expr2))
)
                  )
 
; 4 em cas: f(n) == f(m)
                  ( (and (terme:predicat expr1)
                         (terme:predicat expr2)
                         (equal? (terme:predicat expr1) (terme:predicat expr2))
                    )
(begin
  (display "cas 4\n")
  (display (nouvelle-pile-4cas pile (cdr expr1) (cdr expr2)))
  (display " -\n")
                    (unific (nouvelle-pile-4cas pile (cdr expr1) (cdr expr2))
                            pgu)
)
                  )
; Sinon, c'est faux
                  (else '())
            )
       )
  )
)

(define
  (unification expr1 expr2)
  (unific (cons expr1 (cons expr2 '())) '())
)

(terme:variable? var1)
(terme:variable? exp1)
(terme:variable? int1)
(terme:variable? con1)

(terme:constante? var1)
(terme:constante? exp1)
(terme:constante? int1)
(terme:constante? con1)

(terme:predicat var1)
(terme:predicat exp1)
(terme:predicat int1)
(terme:predicat con1)

(terme:fils-liste var1)
(terme:fils-liste exp1)
(terme:fils-liste int1)
(terme:fils-liste con1)

(unification 'a '?x)
(unification '?x 'a)
(unification 'a 'a)
(unification '(p a) '(p ?x))

(unification '(p a ?x (f (g ?y))) '(p ?z (f ?z) (f ?u)))

(unification '(p a u) '(p ?x ?z))
(display "\n")
(display "\n")