;;;; amb-pl-solver.scm
;;;; From "Continuations by example" ..." by Matt Might

(module amb-pl-solver (with-solution)

(import scheme)
(import (chicken base))
(import (chicken syntax))
(import amb)
(import amb-extras)

;;this is not the most efficient implementation.
;;a continuation is captured for each
;;occurrence of the same variable,
;;instead of one for each variable.

(define-syntax solve
  (syntax-rules (and or xor implies not)
    ;
    ((solve ?form ?body)
      (solve ?form ?body ?form) )
    ;
    ((solve (not ?phi) ?body ?assertion)
      (solve ?phi ?body ?assertion) )
    ;
    ((solve (and ?phi) ?body ?assertion)
      (solve ?phi ?body ?assertion) )
    ;
    ((solve (and ?phi1 ?phi2 ...) ?body ?assertion)
      (solve ?phi1 (solve (and ?phi2 ...) ?body ?assertion)) )
    ;
    ((solve (or ?phi) ?body ?assertion)
      (solve ?phi ?body ?assertion) )
    ;
    ((solve (or ?phi1 ?phi2 ...) ?body ?assertion)
      (solve ?phi1 (solve (or ?phi2 ...) ?body ?assertion)) )
    ;
    ((solve (xor ?phi) ?body ?assertion)
      (solve ?phi ?body ?assertion) )
    ;
    ((solve (xor ?phi1 ?phi2 ...) ?body ?assertion)
      (solve ?phi1 (solve (xor ?phi2 ...) ?body ?assertion)) )
    ;
    ((solve (implies ?phi1 ?phi2) ?body ?assertion)
      (solve ?phi1 (solve ?phi2 ?body ?assertion)) )
    ;
    ((solve #t ?body ?assertion)
     ?body )
    ;
    ((solve #f ?body ?assertion)
      (amb-failure-continuation) )
    ;
    ((solve ?v ?body ?assertion)
      (let ((?v (amb #t #f)))
        (amb-assert ?assertion)
        ?body ) ) ) )

(define-syntax with-solution
  (syntax-rules ()
    ((with-solution ?formula ?body0 ...)
      (solve ?formula (begin ?body0 ...) ) ) ) )

) ;amb-pl-solver