ex-stlc.scm

(define-rel
  (!-o gamma expr type)
  ((!-o-clause-i !-o) (!-o-full-clause-i !-o lookupo))
  (rule-case)
  (matche (expr type)
    ((,x ,T) (symbolo x) (lookupo `(,x : ,T) gamma)
     (== rule-case 'var))
    (((lambda (,x) ,e) (,T1 -> ,T2))
     (!-o `((,x : ,T1) . ,gamma) e T2)
     (== rule-case 'abs))
    (((,e1 ,e2) ,T)
     (fresh (T1)
       (!-o gamma e1 `(,T1 -> ,T))
       (!-o gamma e2 T1))
     (== rule-case 'app))))

(define-rel
  (!!-o gamma expr type)
  ((!!-o-clause-i !!-o) (!!-o-full-clause-i !!-o lookupo))
  (rule-case)
  (matche (expr type)
    ((#t boolean)
     (== rule-case 'true))
    ((#f boolean)
     (== rule-case 'false))
    ((,num integer) (numbero num)
     (== rule-case 'num))
    (((car ,e) ,T1) (fresh (T2) (!!-o gamma e `(,T1 X ,T2)))
     (== rule-case 'car))
    (((cdr ,e) ,T2) (fresh (T1) (!!-o gamma e `(,T1 X ,T2)))
     (== rule-case 'cdr))
    (((cons ,e1 ,e2) (,T1 X ,T2))
     (!!-o gamma e1 T1)
     (!!-o gamma e2 T2)
     (== rule-case 'cons))
    ((,x ,T) (symbolo x) (lookupo `(,x : ,T) gamma)
     (== rule-case 'var))
    (((lambda (,x) ,e) (,T1 -> ,T2))
     (!!-o `((,x : ,T1) . ,gamma) e T2)
     (== rule-case 'abs))
    (((,e1 ,e2) ,T)
     (fresh (T1)
       (!!-o gamma e1 `(,T1 -> ,T))
       (!!-o gamma e2 T1))
     (== rule-case 'app))
    (((if ,e1 ,e2 ,e3) ,T)
     (!!-o gamma e1 'boolean)
     (!!-o gamma e2 T)
     (!!-o gamma e3 T)
     (== rule-case 'if))))

(define (lookupo binding gamma)
  (matche (binding gamma)
    (((,x : ,v) ((,x : ,v) . ,_)))
    (((,x : ,v) ((,y : ,_) . ,gamma1)) (=/= x y) (lookupo binding gamma1))))

(define (to-clause clause-i)
  (lambda (head tail)
    (fresh (rule-case)
      (clause-i head tail rule-case))))
(define !-o-clause (to-clause !-o-clause-i))
(define !!-o-clause (to-clause !!-o-clause-i))

(define (to-clause-case clause-i)
  (lambda (head tail rule-case)
    (clause-i head tail rule-case)))
(define !-o-clause-case (to-clause-case !-o-clause-i))
(define !!-o-clause-case (to-clause-case !!-o-clause-i))

(define (to-debug-clause-case full-clause-i)
  (lambda (head tail rule-case)
    (conde
      ((full-clause-i head tail rule-case))
      ((== tail '())
       (== rule-case '())
       (conde
         ((fresh (binding rho)
            (== `(lookupo ,binding ,rho) head)
            (lookupo binding rho)))
         ((fresh (x y)
            (== `(== ,x ,y) head)
            (== x y))))))))
(define !-o-debug-clause-case (to-debug-clause-case !-o-full-clause-i))
(define !!-o-debug-clause-case (to-debug-clause-case !!-o-full-clause-i))