;; Sequence Calculus in miniKanren
;;
;; To run this, you will need a copy of
;;   https://github.com/webyrd/miniKanren-with-symbolic-constraints
;; (assumed to be in miniKanren from here on)
;;
;; To prove or disprove something:
;;   guile -l miniKanren/mk-guile.scm -e prove -s sequentcalc.scm "'()" "'(or a (not b))"
;;
;; To query for valid statements, run the guile repl:
;;   $ guile -l miniKanren/mk-guile.scm -l sequentcalc.scm
;;   ;; what should q be to make ⇒ a ∧ ¬ q valid? (up to 10 results)
;;   scheme@(guile-user)> (run 10 (q) (sequent '() `(or a (not ,q))))
;;   ;; what could p,q be to make p ⇒ q true? (up to 10 results)
;;   scheme@(guile-user)> (run 10 (p q) (sequent p q))
;;
;; Note that (run*) should usually be avoided, since it will almost
;; always not terminate (as there are usually an infinite amount
;; of possible completions).

(use-modules (ice-9 match))

;; goal: is q a member of the list l?
(define
  (membero q l)
  (fresh (x xs)
         (== l `(,x . ,xs))
         (conde
          ((== q x))
          ((membero q xs)))))

;; goal: list l only contains q
(define (onlo q l)
  (conde ((== l '()))
         ((fresh (x xs)
                 (== l `(,x . ,xs))
                 (== x q)
                 (onlo q xs)))))

;; goal: rest = l with all instances of q removed
(define (removo q l rest)
  (conde
   ((== rest '()) (onlo q l))
   ((absento q rest) (== rest l))
   ((fresh (x xs r rs)
           (== l `(,x . ,xs))
           (== rest `(,r . ,rs))
           (conde
            ((== q x) (=/= q r) (removo q xs `(,r . ,rs)))
            ((=/= q x) (== x r) (removo q xs rs)))))))

(define (sequent gamma delta)
  (conde
   ;; the base axiom: a,Γ ⇒ a,Δ
   ((fresh (a) (membero a gamma) (membero a delta)))
   ;; the not axiom: ⊥,Γ ⇒ Δ
   ((membero 'bottom gamma))
   ;; the not left rule
   ((fresh (f)
           ;; there is ¬F on the left side
           (membero `(not ,f) gamma)
           ;; prove that Γ ⇒ F,Δ
           (fresh (g) (removo `(not ,f) gamma g) (sequent g `(,f . ,delta)))))
   ;; the not right rule
   ((fresh (f)
           (membero `(not ,f) delta)
           (fresh (d) (removo `(not ,f) delta d) (sequent `(,f . ,gamma) d))))
   ;; the and left rule
   ((fresh (a b)
           (membero `(and ,a ,b) gamma)
           (fresh (g)
                  (removo `(and ,a ,b) gamma g)
                  (sequent `(,a . (,b . ,g)) delta))))
   ;; the and right rule
   ((fresh (a b)
           (membero `(and ,a ,b) delta)
           (fresh (d)
                  (removo `(and ,a ,b) delta d)
                  (sequent gamma `(,a . ,d))
                  (sequent gamma `(,b . ,d)))))
   ;; the left or rule
   ((fresh (a b)
           (membero `(or ,a ,b) gamma)
           (fresh (g)
                  (removo `(or ,a ,b) gamma g)
                  (sequent `(,a . ,g) delta)
                  (sequent `(,b . ,g) delta))))
   ;; the right or rule
   ((fresh (a b)
           (membero `(or ,a ,b) delta)
           (fresh (d)
                  (removo `(or ,a ,b) delta d)
                  (sequent gamma `(,a . (,b . ,d))))))
   ;; the left arrow rule
   ((fresh (a b)
           (membero `(arrow ,a ,b) gamma)
           (fresh (g)
                  (removo `(arrow ,a ,b) gamma g)
                  (sequent g `(,a . ,delta))
                  (sequent `(,b . ,g) delta))))
   ;; the right arrow rule
   ((fresh (a b)
           (membero `(arrow ,a ,b) delta)
           (fresh (d)
                  (removo `(arrow ,a ,b) delta d)
                  (sequent `(a . ,gamma) `(,b . ,d)))))))

(define (prove args)
  (let ((gamma (eval-string (car (cdr args))))
        (delta (eval-string (car (cdr (cdr args))))))
    (if (equal? '() (run 1 (q) (sequent gamma delta)))
        (display "does not follow from sequent calculus")
        (display "follows from sequent calculus"))
    (newline)))


(define (pretty formula)
  (match formula
    (('and a b) (string-append "(" (pretty a) " ∧ " (pretty b) ")"))
    (('or a b) (string-append "(" (pretty a) " ∨ " (pretty b) ")"))
    (('not a) (string-append "¬" (pretty a)))
    (('arrow a b) (string-append "(" (pretty a) " → " (pretty b) ")"))
    ('bottom "⊥")
    (a (if (symbol? a) (symbol->string a) "[]"))))

(define (prettylist formulae)
  (map (lambda (f) (map pretty f)) formulae))