#lang racket

#|
GroundTerm ::       Bool | Sym | () | Cons t u
Var ∋ x :: Nat
|# 

#| var? : Term -> Bool |# 
(define var? number?)

#| var : Nat -> Var |# 
(define (var n) n) 

#|
Term ∋ t,u :: Var | Bool | Sym | () | Cons t u

Solve equations over these terms. 
|#GG

'3
'(cat (fish 1) (horse 2))

'(2 3 1)
'(cat (fish 1) (horse 2))

#|
Not just decide if solvable, but produce a solution.

Subst ∋ s :: () | Cons (Var × Term) Subst

Similar and different from an environment.
|#

'3
'(cat (fish 1) (horse 2))
'(3 . (cat (fish 1) (horse 2)))

'(2 3 1)
'(cat (fish 1) (horse 2))
'((1 . (horse 2)) (3 . (fish 1)) (2 . cat))

#|
Again, these should be /solutions/ to equations. 
So additional restrictions:

1. No var is the LHS or RHS if it already appears as an LHS
   '((0 . cat) (0 . dog))
   '((0 . 1) (1 . 2))
|#

(define (walk t s)
  (let ((pr (and (var? t) (assv t s))))
    (if pr (walk (cdr pr) s) t)))

#|
2. No /association/ creates a cycle.
   '((0 . (0)))
   '((0 . (1)) (1 . (0)))
|#

(define (occurs? x v s)
  (let ((v (walk v s)))
    (cond
      ((var? v) (eqv? x v))
      ((pair? v) (or (occurs? x (car v) s)
                     (occurs? x (cdr v) s)))
      (else #f))))

(define (ext-s x v s)
  (cond
    ((occurs? x v s) #f) 
    (else `((,x . ,v) . ,s))))

#|

There is often more than one solution to an equation. How do we
choose? What sort of solution do we want?  We want it to be no more
specific than necessary — a /most general/ one. 
|#

(define (unify t u s)
  (let ((t (walk t s)) (u (walk u s)))
    (cond
      ((eqv? t u) s) ;; both same variable
      ((var? t) (ext-s t u s)) ;; add association 
      ((var? u) (ext-s u t s)) ;; add association 
      ((and (pair? t) (pair? u)) ;; recur
       (let ((s (unify (car t) (car u) s)))
         (and s (unify (cdr t) (cdr u) s))))
      (else #f)))) ;; "clash" – fail

#|
We can solve an equation, and produce solutions. 
Ta da!
|#

(unify '2 'cat '())

#| And we can almost solve /incrementally/! |#
(unify '(2 . 0) '(cat . 2) '())
(unify '0 '2 (unify '2 'cat '()))

;; But! (unify '0 '2 (unify 'dog 'cat '()))

#|
Moreover:  
1. Passing store explicitly.
2. No (lexical) scope for variables.
3. Doesn't allow multiple answers.
4. Doesn't allow incremental solving/failure. 
|#

#|
1. State is explicit
– Add plumbing
|#

#| 
Goal :: Subst -> List Subst

 == : Term Term -> Goal |#
;; tentative
;; (define ((== t u) s)
;;   (let ((s (unify t u s)))
;;     (if s (list s) '())))

#| call/empty-s : Goal -> List Subst |#
;; tentative
;; (define (call/empty-s g)
;;   (g '()))

;; (call/empty-s (== '0 'cat))

#|
2. No (lexical) scope for variables.
– Use Racket's scope. 
|#

;;   (λ (x) (== x 'cat))

;; (((λ (x) (== x 'cat)) 0) '())

;; Which number to pass? Multiple variables?

#|
State ∋ s/c     :: Subst × Count
Count ∋ c       :: Nat
Goal  ∋ g,g₁,g₂ :: State -> List State
|#

#| call/empty-s : Goal -> List State |#
;; tentative
;; (define (call/empty-s g)
;;   (g '(() . 0)))

#| == : Term Term -> Goal |#
(define ((== t u) s/c)
  (let ((s (unify t u (car s/c))))
    (if s (list `(,s . ,(cdr s/c))) '())))

#| (Var -> Goal) -> Goal |# 
(define ((call/fresh f) s/c)
  (let ((c (cdr s/c)))
    (let ((g (f (var c))))
      (g `(,(car s/c) . ,(add1 c))))))

;; (call/empty-s
;;   (call/fresh
;;     (λ (x)
;;       (call/fresh 
;;         (λ (y)
;;           (== `(,y . ,x) `(cat . ,y)))))))

#|
3. Doesn't allow multiple answers.
– must have disjunction.
|#

#| Goal Goal -> Goal |# 
;; (define ((disj g₁ g₂) s/c) (___ (g₁ s/c) (g₂ s/c)))

;; (call/empty-s
;;   (call/fresh
;;     (λ (x)
;;       (disj 
;;         (== x 'cat)
;;         (== x 'dog)))))

#| List State List State -> List State |# 
;; tentative 
(define (___ $₁ $₂)
  (cond
    ((null? $₁) $₂)
    (else (cons (car $₁) (___ (cdr $₁) $₂)))))

#|
4. Doesn't allow incremental solving/failure. 
– must have conjunction
|#

#| Goal Goal -> Goal |# 
(define ((conj g₁ g₂) s/c) ($append-map g₂ (g₁ s/c)))

#| Goal List State -> List State |# 
;; tentative 
;; (define ($append-map g $)
;;   (cond
;;     ((null? $) '())
;;     (else (___ (g (car $)) ($append-map g (cdr $))))))

;; (call/empty-s
;;   (call/fresh
;;     (λ (x)
;;       (conj 
;;         (== x 'cat)
;;         (== x 'dog)))))

;; Properly shadows 
;; (call/empty-s
;;   (call/fresh
;;     (λ (x)
;;       (conj 
;;        (== x 'cat)
;;        (call/fresh
;;          (λ (x) 
;;            (== x 'dog)))))))

#|
5. Cannot program recursively
– add recursion (thoughtfully!)
|#

;; (define (turtles x)
;;   (disj
;;     (== x 'turtle)
;;     (turtles x)))

;; (call/empty-s
;;   (turtles 'turtle))

#|
Stream ∋ $,$₁,$₂ :: State × Stream | () | Delay Stream
Goal  ∋ g,g₁,g₂  :: State ↛ Stream
|#

(define-syntax-rule (define-relation (n . args) g)
  (define ((n . args) s/c)
    (delay (g s/c))))

(delay 5)
(force (delay 5))

(define-relation (empty x)
  (empty x))

;; (call/empty-s (empty 'cat))
#| 
MatureStream :: Cons State Stream | ()
|#

#| pull : Stream ↛ Mature Stream |# 
(define (pull $)
  (cond 
    ((promise? $) (pull (force $)))
    (else $)))

#| call/empty-s : Goal ↛ Mature Stream |#
(define (call/empty-s g)
  (pull (g '(() . 0))))

#| Goal Stream -> Stream |# 
(define ($append-map g $)
  (cond
    ((null? $) '())
    ((promise? $) (delay ($append-map g (force $))))
    (else ($append (g (car $)) ($append-map g (cdr $))))))

#| Stream Stream -> Stream |# 
;; tentative
;; (define ($append $₁ $₂)
;;   (cond
;;     ((null? $₁) $₂)
;;     ((promise? $₁) (delay ($append (force $₁) $₂)))
;;     (else (cons (car $₁) ($append (cdr $₁) $₂)))))

(define-relation (turtles x)
  (disj
    (== x 'turtle)
    (turtles x)))

;; (call/empty-s 
;;   (call/fresh 
;;     (λ (x)
;;       (disj (turtles x) (empty x)))))

#| But we can't get! |#

(call/empty-s 
  (call/fresh 
    (λ (x)
      (disj (empty x) (cats x)))))

#| And even worse |#

(define-relation (cats x)
  (disj
    (== x 'cat)
    (cats x)))

;; (call/empty-s 
;;   (call/fresh 
;;     (λ (x)
;;       (disj (turtles x) (cats x)))))

#| Stream Stream -> Stream |# 
(define ($append $₁ $₂)
  (cond
    ((null? $₁) $₂)
    ((promise? $₁) (delay ($append $₂ (force $₁))))
    (else (cons (car $₁) ($append (cdr $₁) $₂)))))

;; JUST HERE TO MAKE IT RUN
(define ((disj g₁ g₂) s/c) ($append (g₁ s/c) (g₂ s/c)))

(call/empty-s 
  (call/fresh 
    (λ (x)
      (disj (empty x) (cats x)))))

(call/empty-s 
  (call/fresh 
    (λ (x)
      (disj (turtles x) (cats x)))))

(define-relation (appendº l t o)
  (disj
    (conj (== l '()) (== t o))
    (call/fresh
      (λ (a) 
        (call/fresh 
          (λ (d)
            (conj
              (== `(,a . ,d) l)
              (call/fresh 
                (λ (res)
                  (conj
                    (== `(,a . ,res) o)
                    (appendº d t res)))))))))))


(call/empty-s 
  (appendº '(a b c) '(d e) '(a b c d e)))

(call/empty-s 
  (call/fresh
    (λ (o)
      (appendº '(a b c) '(d e) o))))

(call/empty-s 
  (call/fresh
    (λ (l)
      (call/fresh
       (λ (t)
         (appendº l t '(a b c d e)))))))