#lang racket
(require redex)

;; syntax
(define-language Lambda0
  (e x
     n
     (lambda (x τ) e)
     (e e)
     (op e e)
     (fix e))
  (n integer)
  (τ Int
     (τ -> τ))
  (op + - *)
  (x variable-not-otherwise-mentioned)
  ; not surface syntax -- just used for type checking
  (Γ (γ ...))
  (γ (x τ)))

;; type checking
(define-judgment-form Lambda0
  #:mode (type I I O)
  #:contract (type Γ e τ)
  [(type Γ n Int)]
  [(type ( (x_0 τ_0) ... (x τ) (x_1 τ_1) ... ) x τ)]
  [(type Γ e_1 Int) (type Γ e_2 Int)
   ---
   (type Γ (op e_1 e_2) Int)]
  [(type (ext-type-env Γ (x τ_1)) e τ_2)
   ----
   (type Γ (lambda (x τ_1) e) (τ_1 -> τ_2))]
  [(type Γ e_1 (τ_1 -> τ_2)) (type Γ e_2 τ_1)
   ---
   (type Γ (e_1 e_2) τ_2)]
  [(type Γ e (τ -> τ))
   ----
   (type Γ (fix e) τ)])



;; extend given type enviroment with new type binding
(define-metafunction Lambda0
  ext-type-env : Γ γ -> Γ
  [(ext-type-env ((x_old τ_old) ...) (x_new τ_new)) ((x_old τ_old) ... (x_new τ_new))])


;; capture-avoiding substitution (from mf)
(define-metafunction Lambda0
  subst-n : (x any) ... any -> any
  [(subst-n (x_1 any_1) (x_2 any_2) ... any_3)
   (subst x_1 any_1 (subst-n (x_2 any_2) ... any_3))]
  [(subst-n any_3) any_3])

(define-metafunction Lambda0
  subst : x any any -> any
  ;; 1. x_1 bound, so don't continue in lambda body
  [(subst x_1 any_1 (lambda (x_1 τ) any_2))
   (lambda (x_1 τ) any_2)
   #;(side-condition (not (member (term x_1)
                                (term (x_2 ...)))))]
  ;; 2. general purpose capture avoiding case
  [(subst x_1 any_1 (lambda (x_2 τ) any_2))
   (lambda (x_new τ)
     (subst x_1 any_1
            (subst-vars (x_2 x_new)
                        any_2)))
   (where x_new
          ,(variables-not-in
            (term (x_1 any_1 any_2))
            (term (x_2))))]
  ;; 3. replace x_1 with e_1
  [(subst x_1 any_1 x_1) any_1]
  ;; 4. x_1 and x_2 are different, so don't replace
  [(subst x_1 any_1 x_2) x_2]
  ;; the last cases cover all other expressions
  [(subst x_1 any_1 (any_2 ...))
   ((subst x_1 any_1 any_2) ...)]
  [(subst x_1 any_1 (op any_2 ...))
   (op (subst x_1 any_1 any_2) ...)]
  [(subst x_1 any_1 (fix any_2 ...))
   (fix (subst x_1 any_1 any_2) ...)]
  [(subst x_1 any_1 any_2) any_2])

(define-metafunction Lambda0
  subst-vars : (x any) ... any -> any
  [(subst-vars (x_1 any_1) x_1) any_1]
  [(subst-vars (x_1 any_1) (any_2 ...))
   ((subst-vars (x_1 any_1) any_2) ...)]
  [(subst-vars (x_1 any_1) any_2) any_2]
  [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3)
   (subst-vars (x_1 any_1)
               (subst-vars (x_2 any_2) ... any_3))]
  [(subst-vars any) any])