resugar-church.rkt

#lang racket

(require redex)
(require "resugar-redex.rkt")
(require "lang-min.rkt")

(define-macro Cons
  [(Cons hd tl) (λ mk-cons (λ mk-empty (apply (apply mk-cons hd) tl)))])

; -1 for a thunk here
(define-macro Empty
  [(Empty) (λ mk-cons (λ mk-empty (apply mk-empty -1)))])

(define-macro Some
  [(Some x) (λ mk-some (λ mk-none (apply mk-some x)))])

(define-macro None
  [(None) (λ mk-some (λ mk-none (apply mk-none -1)))])

(define-macro Head
  [(Head lst) (apply (apply lst (λ hd (λ tl (! Some hd)))) (! None))])

(test-eval (Head (Cons 1 (Cons 2 (Cons 3 (Empty))))))

(define-macro Pair
  [(Pair x y) (λ f (apply (apply f x) y))])

(define-macro Proj1
  [(Proj1 p) (apply p (λ x (λ y x)))])

(define-macro Proj2
  [(Proj1 p) (apply p (λ x (λ y y)))])


(test-eval (Proj1 (Pair 10 20)))

(define-macro Tail
  [(Tail lst)
   (! Proj2
    (apply
     (apply lst
           (λ hd 
             (λ acc 
               (! Pair (! Some hd)
                     (apply (apply (! Proj1 acc)
                                   (λ x (! Cons x (! Proj2 acc))))
                            (λ dummy (! Proj2 acc)))))))
     (! Pair (! None) (! Empty))))])

(test-eval
 (Tail (Cons 1 (Cons 2 (Cons 3 (Empty))))))