;;;  A very small prolog, for Problem Set #3:
;;;      Pattern Matching, Unification, and Logic Programming
;;;
;;;  Original versions by Mike Dixon
;;;  Updated by Brian Smith
;;;  Last edited by Mike:  Thursday, 7 June 1984

;;;  Note:  To run this program, you must supply the definitions of:
;;;      UNNAMED-WILD
;;;      NAMED-WILD
;;;      PATTERN-NAME
;;;      BOUND
;;;      THE-BINDING
;;;      UNIFY
;;;
;;;   (as explained in the problem set)



(define NANO-PROLOG
   (lambda [goal defns]
      (solve [goal] [] defns [] goal)))

(define SOLVE
   (lambda [goals bindings defns stack original-goal]
      (if (null goals)
          (begin (print primary-stream "  --: ")
                 (print primary-stream (update original-goal bindings))
                 (print primary-stream cr)
                 (backtrack stack defns original-goal))
          (let [[goal (first goals)]]
             (solve-goal (pargs goal)
                         (lookup (pproc goal) defns)
                         (rest goals)
                         bindings stack defns original-goal)))))

(define BACKTRACK
   (lambda [stack defns original-goal]
      (if (null stack)
          'done
          (solve-goal . (append stack [defns original-goal])))))

(define SOLVE-GOAL
   (lambda [args clauses goals bindings stack defns original-goal]
      (if (null clauses)
          (backtrack stack defns original-goal)
          (letseq [[clause (clone (first clauses))]
                   [r (unify (first clause) args bindings)]]
             (if (sequence r)
                 (solve (append (rest clause) goals)
                        r
                        defns
                        [args (rest clauses) goals bindings stack]
                        original-goal)
                 (solve-goal args (rest clauses) goals bindings
                             stack defns original-goal))))))

(define UPDATE
   (lambda [goal bindings]
      (cond [(atom goal) goal]
            [(rail goal)
             (if (null goal)
                 goal
                 (cons (update (first goal) bindings)
                       (update (rest goal) bindings)))]
            [(unnamed-wild goal) goal]
            [(named-wild goal)
             (if (bound goal bindings)
                 (update (the-binding goal bindings) bindings)
                 goal)]
            [(pair goal) (pcons (pproc goal) (update (pargs goal) bindings))])))

(define CLONE
   (lambda [clause]
      (first (cloner clause []))))

(define CLONER
   (lambda [s b]
      (cond [(atom s) [s b]]
            [(rail s)
             (if (null s)
                 [s b]
                 (letseq [[r (cloner (first s) b)]
                          [r2 (cloner (rest s) (second r))]]
                    [(cons (first r) (first r2)) (second r2)]))]
            [(unnamed-wild s) [s b]]
            [(named-wild s)
             (if (bound s b)
                 [(the-binding s b) b]
                 (let [[new '(? ,(acons))]]
                    [new (cons [(pattern-name s) new] b)])))]
            [(pair s)
             (let [[r (cloner (pargs s) b)]]
                [(pcons (pproc s) (first r)) (second r)])])))

(define LOOKUP
   (lambda [name defns]
      (cond [(null defns) '[]]
            [(= name (pproc (first (first defns))))
             (cons (cons (pargs (first (first defns)))
                         (rest (first defns)))
                   (lookup name (rest defns)))]
            [$T (lookup name (rest defns))])))