Auto prover of Combinatory Logic

clp.scm

(use-modules (ice-9 match))

(define (cl str)
  (define (parser s)
    (let lp((i 0) (ret '()))
      (cond
       ((= i (string-length s))
        (map (lambda (x)
               (if (char? x) (string->symbol (string x)) x))
             (reverse ret)))
       ((char=? (string-ref s i) #\()
        (let* ((j (string-index s #\)))
               (sl (parser (substring s (1+ i) j))))
          (lp (1+ j) (cons sl ret))))
       (else
        (lp (1+ i) (cons (string-ref s i) ret)))))) 
  (define (-> l r) (if (list? l) (append l r) (cons l r)))
  (define (%cl e)
    (match e
      (('I P rest ...) (%cl (-> P rest)))
      (('K P Q rest ...) (%cl (-> P rest)))
      (('S P Q R rest ...) (%cl (-> (-> P (list R (list Q R))) rest)))
      ((x (rest ...)) (-> x (%cl rest)))
      (else e)))
  (for-each display (%cl (parser str)))
  (newline))

scheme@(guile-user)> (cl "SIIx")

[NOW]  (S I I x)
[APP]  SPQR => PRQR
  S I I x => I x I x

[NOW]  (I x (I x))
[APP]  IP => P
  I x => x

[NOW]  (x (I x))

[NOW]  (I x)
[APP]  IP => P
  I x => x

[NOW]  (x)
xx