proofery.rkt

#lang racket
(require 2htdp/image)
 
(define-syntax structs
  (syntax-rules ()
    [(_) (begin)]
    [(_ (name args ...) rest ...) (begin (struct name (args ...) #:transparent)
                                         (structs rest ...))]))

(structs
 (inf c r ps)
 (rul r i)
 (wild)
 (ref x)
 (sum l r)
 (inl x)
 (inr x)
 (case x l lx r rx)
 (prod f s)
 (pair f s)
 (fst x)
 (snd x)
 (fun from to)
 (lam p t x)
 (app f a)
 (unit)
 (unitt)
 (void)
 (broken)
 (t l r))
 
(define (txt x (size 20))
  (text (~a x) size "black"))
 
(define (infer c r . ps)
  (inf c r ps))
 
(define (rule r (i #f))
  (rul r i))
 

(define (draw-rule rule)
  (match rule
    [#f (txt " ")]
    [(rul name num)
     (define rimg (txt name))
     (match num
       [#f rimg]
       [n (define iimg (txt n 14))
          (overlay/xy rimg (image-width rimg) 10 iimg)])]))

(define (whitespace w)
  (rectangle w 20 'solid (color 0 0 0 0)))

(define (besidel l)
  (match l
    ['() (whitespace 10)]
    [(list x) x]
    [l (apply beside/align 'bottom l)]))

(define (draw-inf-halp i)
  (match i
    [(inf c r ps)
     (define c-img (beside (whitespace 2) (txt c) (whitespace 2)))
     (define r-img (draw-rule r))
     (match (map draw-inf-halp ps)
       [(list (list p-imgs p-insetls p-insetrs) ...)
        (define p-img (besidel (add-between p-imgs (whitespace 15))))
        (define p-insetl (if (null? p-insetls) 0 (first p-insetls)))
        (define p-insetr (if (null? p-insetrs) 0 (last p-insetrs)))
        (define p-insetlength (- (image-width p-img) p-insetl p-insetr))        
        (define c-start0 (+ (/ (- p-insetlength (image-width c-img)) 2) p-insetl))
        (define c-start (if (< c-start0 0) 0 c-start0))
        (define p-start (if (< c-start0 0) (- c-start0) 0))
        (match (if (> p-insetlength (image-width c-img))
                   (cons (+ p-start p-insetl) p-insetlength)
                   (cons c-start (image-width c-img)))
          [(cons line-start line-length)
           (define line-end (+ line-start line-length))
           (define empty (rectangle (max (+ p-start (image-width p-img))
                                         (+ line-end (image-width r-img) 4)
                                         (+ c-start (image-width c-img)))
                                    (+ (image-height c-img) (image-height p-img) 6)
                                    'solid
                                    (color 0 0 0 0)))
           (define (place-img arg scene)
             (match arg
               [(list img x y) (place-image/align img x y 'left 'top scene)]))
           (define prem/conc (foldl place-img
                                  empty
                                  (list (list p-img p-start 0)
                                        (list c-img c-start (+ (image-height p-img) 6)))))
           (define prem/conc/rul (if r
                                     (foldl place-img
                                            prem/conc
                                            (list (list r-img (+ line-end 4) (- (image-height p-img) 12))
                                                  (list (line line-length 0 'black) line-start (+ (image-height p-img) 3))))
                                     prem/conc))
           (list prem/conc/rul c-start (- (image-width empty) (+ c-start (image-width c-img))))])])]))
 
(define (typeof exp (env '()))
  (match exp
    [(ref x) (let ([res (assoc x env)])
               (if res (cdr res) (broken)))]
    [(inl x) (sum (typeof x env) (wild))]
    [(inr x) (sum (wild) (typeof x env))]
    [(case x l lx r rx)
     (match (typeof x env)
       [(sum lt rt) (typecheck (typeof lx (cons (cons l lt) env))
                               (typeof rx (cons (cons r rt) env)))])]
    [(pair f s) (prod (typeof f env) (typeof s env))]
    [(lam p t x) (fun t (typeof x (cons (cons p t) env)))]
    [(app f a)
     (match (typeof f env)
       [(fun f t) (if (broken? (typecheck f (typeof a env))) (broken) t)]
       [_ (broken)])]
    [(fst x) (match (typeof x env) [(prod f _) f])]
    [(snd x) (match (typeof x env) [(prod _ s) s])]
    [(unit) (unitt)]))
 
(define (typecheck at bt)
  (match (t at bt)
    [(t (wild) x) x]
    [(t x (wild)) x]
    [(t (sum al ar) (sum bl br)) (sum (typecheck al bl) (typecheck ar br))]
    [(t (prod af as) (prod bf bs)) (prod (typecheck af bf) (typecheck as bs))]
    [(t (fun af at) (fun bf bt)) (fun (typecheck af bf) (typecheck at bt))]
    [(t (unitt) (unitt)) (unitt)]
    [(t (void) (void)) (void)]
    [(t at bt) (if (equal? at bt)
                   at
                   (broken) #;(error (format "expected: ~a found: ~a~n" at bt)))]))
 
(define-syntax parse
  (syntax-rules (· λ : inl inr case ↦ pair fst snd)
    [(_ ·) (unit)]
    [(_ (pair f s)) (pair (parse f) (parse s))]
    [(_ (fst x)) (fst (parse x))]
    [(_ (snd x)) (snd (parse x))]
    [(_ (inl l)) (inl (parse l))]
    [(_ (inr r)) (inr (parse r))]
    [(_ (case x (inl(l) ↦ lx) (inr(r) ↦ rx))) (case (parse x) 'l (parse lx) 'r (parse rx))]
    [(_ (λ (p : t) x)) (lam 'p (parse-type t) (parse x))]
    [(_ (λ (p : t) . rest)) (parse (λ (p : t) (λ . rest)))]
    [(_ (f a)) (app (parse f) (parse a))]
    [(_ (f a . rest)) (parse ((f a) . rest))]
    [(_ x) (ref 'x)]))

(define (draw-inf i)
  (car (draw-inf-halp i)))
 
(define-syntax parse-type
  (syntax-rules (→ + ×)
    [(_ (f → t)) (fun (parse-type f) (parse-type t))]
    [(_ (f → t → . rest)) (parse-type (f → (t → . rest)))]
    [(_ (f → t)) (fun (parse-type f) (parse-type t))]
    [(_ (l + r)) (sum (parse-type l) (parse-type r))]
    [(_ (f × s)) (prod (parse-type f) (parse-type s))]
    [(_ 1) (unitt)]
    [(_ 0) (void)]
    [(_ x) 'x]))
 
(define (translate x (env '()))
  (define c (string-append (string-join (map (compose translate-type cdr) (reverse env)) ", ")
                           "⊢"
                           (translate-type (typeof x env))))
  (match x
    [(unit) (infer c (rule "⊤I"))]
    [(lam p t x) (infer c (rule "⊃I") (translate x (cons (cons p t) env)))]
    [(app f a) (infer c (rule "⊃E") (translate f env) (translate a env))]
    [(pair a b) (infer c (rule "∧I") (translate a env) (translate b env))]
    [(fst p) (infer c (rule "∧E" 1) (translate p env))]
    [(snd p) (infer c (rule "∧E" 2) (translate p env))]
    [(inl l) (infer c (rule "∨I" 1) (translate l env))]
    [(inr r) (infer c (rule "∨I" 2) (translate r env))]
    [(case x l lx r rx) (match (typeof x env)
                          [(sum lt rt) (infer c
                                              (rule "∨E")
                                              (translate x env)
                                              (translate lx (cons (cons l lt) env))
                                              (translate rx (cons (cons r rt) env)))])]
    [(ref x) (match env
               ['() (infer c (rule "?"))]
               [(list (cons a _) rest ...)
                (if (equal? a x)
                    (infer c (rule "H"))
                    (infer c (rule "W") (translate (ref x) rest)))])]
    [_ (infer c (rule "?"))]))
 
(define (translate-type ty)
  (if (symbol? ty)
      (~a ty)
      (match ty
        [(fun f (void)) (string-append "¬" (translate-type f))]
        [(fun (fun f1 f2) t) (string-append "(" (translate-type (fun f1 f2)) ")⊃" (translate-arg t))]
        [(fun f t) (string-append (translate-type f) "⊃" (translate-type t))]
        [(sum l r) (string-append (paren l) "∨" (paren r))]
        [(prod f s) (string-append (paren f) "∧" (paren s))]
        [(void) "⊥"]
        [(unitt) "⊤"]
        [(wild) "_"]
        [(broken) "?"])))
 
(define (paren ty)
  (if (symbol? ty)
      (~a ty)
      (match ty
        [(void) "⊥"]
        [(unitt) "⊤"]
        [(wild) "_"]
        [(broken) "?"]
        [(fun f (void)) (string-append "¬" (translate-type f))]
        [x (string-append "(" (translate-type x) ")")])))
 
(define (translate-arg a)
  (match a
    [(fun f (void)) (string-append "¬" (translate-type f))]
    [(fun (fun f1 f2) t) (string-append "(" (translate-type (fun f1 f2)) ")⊃" (translate-arg t))]
    [(fun f t) (string-append (translate-type f) "⊃" (translate-arg t))]
    [x (translate-type x)]))
 
(define-syntax-rule (draw x) (draw-inf (translate (parse x))))
 
(draw
 (λ (f : (A → B → C)) (x : (A × B))
   (f (fst x) (snd x))))
 
(draw
 (λ (f : (A → B)) (g : (B → C)) (a : A)
   (g (f a))))
 
(draw
 (λ (s : (A + B)) (f : (A → C)) (g : (B → C))
   (case s
     (inl(l) ↦ (f l))
     (inr(r) ↦ (g r)))))