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 "S(KS)Kgfj")

[NOW]  (S (K S) K g f j)
[APP]  SPQR => PRQR
  S (K S) K g => (K S) g K g

[NOW]  (K S g (K g) f j)
[APP]  KPQ => P
  K S g => S

[NOW]  (S (K g) f j)
[APP]  SPQR => PRQR
  S (K g) f j => (K g) j f j

[NOW]  (K g j (f j))
[APP]  KPQ => P
  K g j => g

[NOW]  (g (f j))

[NOW]  (f j)
gfj

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