typing.rkt

#lang racket
(require "mk.rkt")

;; mostly https://gist.github.com/swannodette/997140
;; probably sprinkled with broken

(define (findo x l o)
  (fresh (s v d)
    (symbolo x)
    (== `((,s : ,v) . ,d) l)
    (conde
      ((== s x) (== v o))
      ((=/= s x) (findo x d o)))))

(define (findno x l)
  (conde
    ((== l '()))
    ((fresh (n v d)
       (== `((,n : ,v) . ,d) l)
       (=/= x n)
       (findno x d)))))
 
(define (typedo c x t)
  (conde
    ((findo x c t))
    ((findno x c)
     (conde
       ((fresh (p b s rt l)
          (== x `(λ (,p) ,b))
          (== t `(,s -> ,rt))
          (== l `((,p : ,s) . ,c))
          (typedo l b rt)))
       ((fresh (f a p)
          (== x `(,f ,a))
          (typedo c f `(,p -> ,t))
          (typedo c a p)))))))

;; ((_.0 -> _.1))
(run* (q)
  (fresh (f g a b t)
    (typedo `((,f : ,a) (,g : ,b)) `(,f ,g) t)
    (== q a)))

;; ((int -> _.0))
(run* (q)
  (fresh (f g a t)
    (typedo `((,f : ,a) (,g : int)) `(,f ,g) t)
    (== q a)))

;; (int)
(run* (q)
  (fresh (f g a t)
    (typedo `((,f : (int -> float)) (,g : ,a))
            `(,f ,g)
            t)
    (== q a)))

;; ()
(run* (t)
  (fresh (f a)
    (typedo '(,f : a) '(,f ,f) t)))

;; ((_.0 -> ((_.0 -> _.1) -> _.1)))
(run* (t)
  (fresh (x y)
    (typedo '() `(λ (,x) (λ (,y) (,y ,x))) t)))

;; (((_.0 -> _.1) -> (_.0 -> _.1)))
(run* (t)
  (typedo '() '(λ (x) (λ (y) (x y))) t))