#lang racket/base

(require redex)

(provide all-defined-out)

(define-language ScopeLanguage
  (x  ::= variable-not-otherwise-mentioned)
  (S  ::= x)
  (Sₙ ::= (S natural))
  (l  ::= x
          (Sₙ x))
  (τ  ::= bool
          unit
          (τ → τ))
  (e  ::= x
          true
          false
          ()
          (λ [x : τ] e)
          (e e)
          l
          d)
  (d  ::= {e ... ¦ e :- e}
          ⊛
          ∅)
  (a  ::= (define l : τ
            d)
          (call Sₙ))
  (σ  ::= (scope S a ...))
  (P  ::= (σ ...)))

(define-term P1/ScopeLanguage
  ((scope A 
     (define x : bool 
       {¦ true :- true}))))

(define-term P2/ScopeLanguage
  ((scope A 
     (define x : bool
       {¦ true :- true}))
   (scope B
     (call (A 1))
     (define y : bool 
       {¦ true :- ((A 1) x)}))))

(define-term P3/ScopeLanguage
  ((scope A 
     (define x : bool 
       {¦ true :- true}))
   (scope B
     (define ((A 1) x) : bool 
       {¦ true :- false})
     (call (A 1))
     (define y : bool 
       {¦ true :- ((A 1) x)}))))

(define-extended-language DefaultCalculus ScopeLanguage
  (e      ::= ....
              [e : τ]
              (values e ...)
              (let-values [(l ...) e] ;; move "values" here
                e))
  (σ      ::= ....
              (define (x e ...)
                e))
  (Γ      ::= ·
              (x : τ Γ))
  (Δ      ::= ·
              (l Δ))
  (v      ::= true
              false
              (λ [x : τ] e)
              ⊛
              ∅)
  (Cλ     ::= (hole e)
              (v hole)
              {v ... ¦ hole :- e}
              {v ... ¦ true :- hole})
  (C      ::= Cλ
              {v ... hole e ... ¦ e :- e})
  (Cλ-alt ::= hole
              (Cλ-alt e)
              (v Cλ-alt)
              {v ... ¦ Cλ-alt :- e}
              {v ... ¦ true :- Cλ-alt})
  (C-alt  ::= Cλ-alt
              {v ... C-alt e ... ¦ e :- e}))

(define-term P1/DefaultCalculus
  ((define (A x)
     (let-values [(x) (values {(x ()) ¦ true :- {¦ true :- true}})]
       (values x)))))

(define-term P2/DefaultCalculus
  ((define (A x)
     (let-values [(x) (values {(x ()) ¦ true :- {¦ true :- true}})]
     (values x)))
   (define (B y)
     (let-values [(((A 1) x)) (values (λ (u : unit) ∅))]
     (let-values [(((A 1) x)) (A ((A 1) x))]
     (let-values [(y) (values {(y ()) ¦ true :- {¦ true :- ((A 1) x)}})]
     (values y)))))))

(define-term P3/DefaultCalculus
  ((define (A x)
     (let-values [(x) (values {(x ()) ¦ true :- {¦ true :- true}})]
     (values x)))
   (define (B y)
     (let-values [(((A 1) x)) (values (λ (u : unit) ∅))]
     (let-values [(((A 1) x))
                  (values {(((A 1) x) ()) ¦ true :- {¦ true :- false}})]
     (let-values [(((A 1) x)) (A (λ (u : unit) ((A 1) x)))]
     (let-values [(y) (values {(y ()) ¦ true :- {¦ true :- ((A 1) x)}})]
     (values y))))))))

(define-extended-language EnrichedLambdaCalculus DefaultCalculus
  (τ ::= ....
         top
         (list τ)
         (option τ))
  (e ::= ....
         None
         (Some e)
         (match e [e e] ...)
         (list e ...)
         (fold-left e e e)
         (raise ε)
         (try e [ε e])
         (if e e e))
  (ε ::= ∅
         ⊛))

(define-metafunction DefaultCalculus
  same : τ τ ... -> boolean
  [(same τ)                #t]
  [(same τ τ   τ_rest ...) (same τ τ_rest ...)]
  [(same τ τ_1 τ_rest ...) #f])

(test-equal
 (term (same unit))
 #t)

(test-equal
 (term (same (bool → bool) (bool → bool) (bool → bool)))
 #t)

(test-equal
 (term (same (bool → bool) (bool → unit) (bool → bool)))
 #f)

(define-metafunction DefaultCalculus
  different : x x -> boolean
  [(different x x)       #f]
  [(different x x_other) #t])

(test-equal (term (different a b)) #t)

(test-equal (term (different a a)) #f)

#| _____Typing rules for the default calculus_____ |#

(define-judgment-form
  DefaultCalculus
  #:mode (has-type I I O)
  #:contract (has-type Γ e τ)
  [
   ------------------------ "T-Var"
   (has-type (x : τ Γ) x τ)]

  [(has-type Γ x τ)
   (side-condition (different x x_prime))
   -------------------------------------- "T-Lookup"
   (has-type (x_prime : τ_prime Γ) x τ)]

  [
   ---------------------- "T-True"
   (has-type Γ true bool)]

  [
   ----------------------- "T-False"
   (has-type Γ false bool)]

  [
   -------------------- "T-Unit"
   (has-type Γ () unit)]

  [
   ---------------------- "T-ConflictError"
   (has-type Γ [⊛ : τ] τ)]

  [
   ---------------------- "T-EmptyError"
   (has-type Γ [∅ : τ] τ)]
  
  [(has-type (x : τ_dom Γ) e τ_rng)
   ---------------------------------------------- "T-App"
   (has-type Γ (λ [x : τ_dom] e) (τ_dom → τ_rng))]

  [(has-type Γ e_dom τ_dom)
   (has-type Γ e_fun (τ_dom → τ_rng))
   ---------------------------------- "T-Abs"
   (has-type Γ (e_fun e_dom) τ_rng)]

  [(has-type Γ e_i τ_i) ...
   (has-type Γ e_just bool)
   (has-type Γ e_cons τ)
   (side-condition (same τ τ_i ...))
   ------------------------------------------- "T-Default"
   (has-type Γ {e_i ... ¦ e_just :- e_cons} τ)])

(test-equal
 (judgment-holds (has-type (jet : unit ·) jet τ) τ)
 '(unit))

(test-equal
 (judgment-holds (has-type (set : unit ·) jet τ) τ)
 '())

(test-equal
 (judgment-holds (has-type · true τ) τ)
 '(bool))

(test-equal
 (judgment-holds (has-type · false τ) τ)
 '(bool))

(test-equal
 (judgment-holds (has-type · () τ) τ)
 '(unit))

(test-equal
 (judgment-holds
  (has-type (alpha : unit (alpha : bool ·)) alpha τ) τ)
 '(unit))

(test-equal
 (judgment-holds (has-type · (λ [x : bool] ()) τ) τ)
 '((bool → unit)))

(test-equal
 (judgment-holds
  (has-type (helper : (unit → bool) ·) 
            (λ [dummy : unit] (helper dummy)) τ) τ)
 '((unit → bool)))

(test-equal
 (judgment-holds
  (has-type (aux : (bool → (bool → bool)) ·)
            ((aux true) false) τ) τ)
 '(bool))

(test-equal
 (judgment-holds (has-type · [⊛ : unit] τ) τ)
 '(unit))

(test-equal
 (judgment-holds (has-type · [∅ : bool] τ) τ)
 '(bool))

(test-equal
 (judgment-holds
  (has-type (e₁ : unit (e₂ : unit (e₃ : unit ·)))
            {e₁ e₂ ¦ true :- e₃} τ) τ)
 '(unit))

(test-equal
 (judgment-holds
  (has-type (e₁ : unit (e₂ : bool (e₃ : unit ·)))
            {e₁ e₂ ¦ false :- e₃} τ) τ)
 '())

(test-equal
 (judgment-holds
  (has-type · {{¦ false :- true} ¦ true :- true} τ) τ)
 '(bool))

#| _____Reduction rules for the default calculus_____ |#

(define-metafunction DefaultCalculus
  not-∅? : e -> boolean
  [(not-∅? ∅) #f]
  [(not-∅? e) #t])

(define-metafunction DefaultCalculus
  not-⊛? : e -> boolean
  [(not-⊛? ⊛) #f]
  [(not-⊛? e) #t])

(define-judgment-form
  DefaultCalculus
  #:mode (reduces-to I O)
  #:contract (reduces-to e e)
  [(reduces-to e e_prime)
   (side-condition (not-⊛? e_prime))
   (side-condition (not-∅? e_prime))
   ---------------------------------------------- "D-Context"
   (reduces-to (in-hole C e) (in-hole C e_prime))]

  [(reduces-to e ⊛)
   ---------------------------- "D-ContextConflictError"
   (reduces-to (in-hole C e) ⊛)]

  [(reduces-to e ∅)
   ----------------------------- "D-ContextEmptyError"
   (reduces-to (in-hole Cλ e) ∅)]

  [
   ------------------------------------------------- "D-Beta"
   (reduces-to ((λ [x : τ] e) v) (substitute e x v))]

  [
   ---------------------------------- "D-DefaultTrueNoExceptions"
   (reduces-to {∅ ... ¦ true :- v} v)]

  [
   ----------------------------------- "D-DefaultFalseNoExceptions"
   (reduces-to {∅ ... ¦ false :- e} ∅)]

  [(side-condition (not-∅? v))
   ------------------------------------------- "D-DefaultOneException"
   (reduces-to {∅ ... v ∅ ... ¦ e_1 :- e_2} v)]

  [(side-condition (not-∅? v_i))
   (side-condition (not-∅? v_j))
   ------------------------------------------ "D-DefaultExceptionsConflict"
   (reduces-to
    {e_i ... v_i e_j ... v_j ¦ e_1 :- e_2} ⊛)])

(test-equal
 (judgment-holds
  (reduces-to ((λ [x : bool] true) ((λ [x : bool] ∅) true)) e) e)
 '(∅))

(test-equal
 (judgment-holds
   (reduces-to {((λ [x : bool] ⊛) true) ¦ true :- true} e) e)
 '(⊛))

(test-equal
 (judgment-holds
  (reduces-to {((λ [x : bool] x) true) ¦ true :- true} e) e)
 '({true ¦ true :- true}))

(test-equal
 (judgment-holds
  (reduces-to ((λ (x : bool) ()) true) e) e)
 '(()))

(test-equal
 (judgment-holds
  (reduces-to {∅ ¦ {∅ ∅ ¦ true :- ∅} :- false} e) e)
 '(∅))

(test-equal
 (judgment-holds
  (reduces-to {∅ {∅ ¦ true :- ⊛} ¦ true :- false} e) e)
 '(⊛))

(test-equal
 (judgment-holds
  (reduces-to {∅ {∅ ¦ true :- false} ¦ true :- false} e) e)
 '({∅ false ¦ true :- false}))

(test-equal
 (judgment-holds
  (reduces-to ((λ [x : bool] false)
               {¦ false :- (λ (x : bool) x)}) e) e)
 '(∅))

(test-equal
 (judgment-holds
  (reduces-to ((λ [x : bool] {∅ ⊛ ∅ ¦ true :- true}) false) e) e)
 '({∅ ⊛ ∅ ¦ true :- true}))

(test-equal
 (judgment-holds
  (reduces-to {∅ ⊛ ∅ ¦ true :- true} e) e)
 '(⊛))

(test-equal
 (judgment-holds
  (reduces-to ((λ [x : bool] x) {true ∅ ∅ ¦ true :- false}) e) e)
 '(((λ [x : bool] x) true)))

(test-equal
 (judgment-holds
  (reduces-to ((λ [x : bool] x) true) e) e)
 '(true))

(test-equal
 (judgment-holds
  (reduces-to {true false ∅ true ¦ true :- true} e) e)
 '(⊛))

(test-equal
 (judgment-holds
  (reduces-to {{¦ false :- true} ¦ true :- true} e) e)
 '())

#| _____Reduction rules for the default calculus, II_____ |#

(define-metafunction DefaultCalculus
  is-⊛? : e -> boolean
  [(is-⊛? ⊛) #t]
  [(is-⊛? e) #f])

(define-metafunction DefaultCalculus
  is-∅? : e -> boolean
  [(is-∅? ∅) #t]
  [(is-∅? e) #f])

(define reduces-to-alt
  (reduction-relation
   DefaultCalculus #:domain e #:codomain e
   ;; _____ D-Beta _____
   (--> (in-hole Cλ-alt ((λ [x : τ] e) v)) e_step
        (where e_step (substitute e x v))
        (side-condition (equal? (term ∅) (term e_step)))
        "D-Beta/ContextEmptyError")
   (--> (in-hole C-alt ((λ [x : τ] e) v)) e_step
        (where e_step (substitute e x v))
        (side-condition (equal? (term ⊛) (term e_step)))
        "D-Beta/ContextConflictError")
   (--> (in-hole C-alt ((λ [x : τ] e) v)) (in-hole C-alt e_step)
        (where e_step (substitute e x v))
        (side-condition (not (equal? (term e_step) (term ∅))))
        (side-condition (not (equal? (term e_step) (term ⊛))))
        "D-Beta/Context")
   ;; _____ D-DefaultTrueNoExceptions _____
   (--> (in-hole Cλ-alt {∅ ... ¦ true :- ∅}) ∅
        "D-DefaultTrueNoExceptions/ContextEmptyError")
   (--> (in-hole C-alt {∅ ... ¦ true :- ⊛}) ⊛
        "D-DefaultTrueNoExceptions/ContextConflictError")
   (--> (in-hole C-alt {∅ ... ¦ true :- v}) (in-hole C-alt v)
        (side-condition (not (equal? (term v) (term ∅))))
        (side-condition (not (equal? (term v) (term ⊛))))
        "D-DefaultTrueNoExceptions/Context")
   ;; _____ D-DefaultFalseNoExceptions _____
   (--> (in-hole Cλ-alt {∅ ... ¦ false :- e}) ∅
        "D-DefaultFalseNoExceptions")
   ;; _____ D-DefaultOneException _____
   (--> (in-hole C-alt {∅ ... ⊛ ∅ ... ¦ e_1 :- e_2}) ⊛
        "D-DefaultOneException/ContextConflictError")
   (--> (in-hole C-alt {∅ ... v ∅ ... ¦ e_1 :- e_2}) (in-hole C-alt v)
        (side-condition (not (equal? (term v) (term ∅))))
        (side-condition (not (equal? (term v) (term ⊛))))
        "D-DefaultOneException/Context")
   ;; _____ D-DefaultExceptionsConflict _____
   (--> (in-hole C-alt {e_i ... v_i e_j ... v_j ¦ e_1 :- e_2}) ⊛
        (side-condition (not (equal? (term v_i) (term ∅))))
        (side-condition (not (equal? (term v_j) (term ∅))))
        "D-DefaultExceptionsConflict")))

(test-->
 reduces-to-alt
 (term ((λ [x : bool] true) ((λ [x : bool] ∅) true)))
 (term ∅))

(test-->
 reduces-to-alt
 (term {((λ [x : bool] ⊛) true) ¦ true :- true})
 (term ⊛))

(test-->
 reduces-to-alt
 (term {((λ [x : bool] x) true) ¦ true :- true})
 (term {true ¦ true :- true}))

(test-->
 reduces-to-alt
 (term ((λ [x : bool] ()) true))
 (term ()))

(test-->
 reduces-to-alt
 (term {∅ ¦ {∅ ∅ ¦ true :- ∅} :- false})
 (term ∅))

(test-->
 reduces-to-alt
 (term {∅ {∅ ¦ true :- ⊛} ¦ true :- false})
 (term ⊛))

(test-->
 reduces-to-alt
 (term {∅ {∅ ¦ true :- false} ¦ true :- false})
 (term {∅ false ¦ true :- false}))

(test-->
 reduces-to-alt
 (term ((λ [x : bool] false) {¦ false :- (λ [x : bool] x)}))
 (term ∅))

(test-->
 reduces-to-alt
 (term ((λ [x : bool] {∅ ⊛ ∅ ¦ true :- true}) false))
 (term {∅ ⊛ ∅ ¦ true :- true}))

(test-->
 reduces-to-alt
 (term {∅ ⊛ ∅ ¦ true :- true})
 (term ⊛))

(test-->
 reduces-to-alt
 (term ((λ [x : bool] x) {true ∅ ∅ ¦ true :- false}))
 (term ((λ (x : bool) x) true)))

(test-->
 reduces-to-alt
 (term ((λ [x : bool] x) true))
 (term true))

(test-->
 reduces-to-alt
 (term {true false ∅ true ¦ true :- true})
 (term ⊛))

#| _____Compiling the scope language to a default calculus_____ |#

(define-metafunction DefaultCalculus
  lookup-scope : P S -> σ
  [(lookup-scope ((scope S a ...) σ ...) S)
   (scope S a ...)]
  [(lookup-scope ((scope S_other a ...) σ ...) S)
   (lookup-scope (σ ...) S)]
  [(lookup-scope () S)
   ,(error "lookup-scope")])

(test-equal
 (term (lookup-scope P1/ScopeLanguage A)) #t
 #:equiv (λ (actual expected) #t))

(test-equal
 (term (lookup-scope P2/ScopeLanguage B)) #t
 #:equiv (λ (actual expected) #t))

(define-metafunction DefaultCalculus
  local-vars-helper : (a ...) (x ...) -> (x ...)
  [(local-vars-helper () (x ...))
   (x ...)]
  [(local-vars-helper ((define x : τ e) a ...) (x_i ...))
   (local-vars-helper (a ...) (x_i ...))
   (side-condition (member (term x) (term (x_i ...))))]
  [(local-vars-helper ((define x : τ e) a ...) (x_i ...))
   (local-vars-helper (a ...) (x_i ... x))
   (side-condition (not (member (term x) (term (x_i ...)))))]
  [(local-vars-helper ((define (Sₙ x_prime) : τ e) a ...) (x ...))
   (local-vars-helper (a ...) (x ...))]
  [(local-vars-helper ((call Sₙ) a ...) (x ...))
   (local-vars-helper (a ...) (x ...))])

(define-metafunction DefaultCalculus
  local-vars : σ -> (x ...)
  [(local-vars (scope S a ...))
   (local-vars-helper (a ...) ())])

(test-equal
 (term 
  (local-vars
   (scope S
     (define x : bool 
       {¦ true :- true})
     (define y : bool
       {¦ true :- true})
     (define x : bool 
       {¦ true :- true})
     (define x : bool 
       {¦ true :- true})
     (define z : bool 
       {¦ true :- true}))))
 (term (x y z)))

(test-equal
 (term 
  (local-vars
   (scope S
     (define ((T 1) x) : bool
       {¦ true :- true}))))
 (term ()))

(define-metafunction DefaultCalculus
  calls-helper : (a ...) (Sₙ ...) -> (Sₙ ...)
  [(calls-helper () (Sₙ ...))
   (Sₙ ...)]
  [(calls-helper ((define l : τ e) a ...) (Sₙ ...))
   (calls-helper (a ...) (Sₙ ...))]
  [(calls-helper ((call Sₙ) a ...) (Sₙ_i ...))
   (calls-helper (a ...) (Sₙ_i ... Sₙ))
   (side-condition (not (member (term Sₙ) (term (Sₙ_i ...)))))]
  [(calls-helper ((call Sₙ) a ...) (Sₙ_i ...))
   (calls-helper (a ...) (Sₙ_i ...))
   (side-condition (member (term Sₙ) (term (Sₙ_i ...))))])

(define-metafunction DefaultCalculus
  calls : σ -> (Sₙ ...)
  [(calls (scope S a ...))
   (calls-helper (a ...) ())])

(test-equal
 (term 
  (calls
   (scope S
     (define x : bool 
       {¦ true :- true})
     (call (T 1))
     (define ((U 1) x) : bool
       {¦ true :- true})
     (call (T 2))
     (define z : bool
       {¦ true :- true}))))
 (term ((T 1) (T 2))))

(test-equal
 (term 
  (calls
   (scope S
     (call (T 1))
     (call (T 1)))))
 (term ((T 1))))

(define-metafunction DefaultCalculus
  replicate : (x ...) -> (e ...)
  [(replicate ()) ()]
  [(replicate (x x_rest ...))
   ((λ [u : unit] ∅) e_rest ...)
   (where (e_rest ...) (replicate (x_rest ...)))])

(define-metafunction DefaultCalculus
  init : (Sₙ ...) P e -> e
  [(init () P e)
   e]
  [(init ((S number) Sₙ ...) P e)
   (let-values [(((S number) x) ...)  (values e_thunk ...)]
     (init (Sₙ ...) P e))
   (where (x ...) (local-vars (lookup-scope P S)))
   (where (e_thunk ...) (replicate (x ...)))])

(define-metafunction DefaultCalculus
  force : Δ x -> e
  [(force ·     x) (x ())]
  [(force (x Δ) x) x]
  [(force (_ Δ) x) (force Δ x)])

(define-metafunction DefaultCalculus
  thunk : Δ l -> e
  [(thunk ·     l) l]
  [(thunk (l Δ) l) (λ [u : unit] l)]
  [(thunk (_ Δ) l) (thunk Δ l)])

(define-metafunction DefaultCalculus
  add : (l ...) Δ -> Δ
  [(add ()             Δ) Δ]
  [(add (l l_rest ...) Δ) (add (l_rest ...) (l Δ))])

(define-judgment-form
  DefaultCalculus
  #:mode (compiles-atoms I I I I O)
  #:contract (compiles-atoms P S Δ (a ...) e)

  [(where σ (lookup-scope P S))
   (where (x ...) (local-vars σ))
   (where (e ...) ((force Δ x) ...))
   --------------------------------- "C-Empty"
   (compiles-atoms P S Δ ()
     (values e ...))]

  [(compiles-atoms P S (l Δ) (a ...) e_rest)
   ------------------------------------------------- "C-Def"
   (compiles-atoms P S Δ ((define l : τ e) a ...)
     (let-values [(l) (values {(l ()) ¦ true :- e})] 
       e_rest))]

  [(where (x_call ...) (local-vars (lookup-scope P S_call)))
   (where (l_call ...) (((S_call number) x_call) ...))
   (compiles-atoms P S (add (l_call ...) Δ) (a ...) e_rest)
   (side-condition (not (equal? (term S) (term S_call))))
   --------------------------------------------------------- "C-Call"
   (compiles-atoms P S Δ ((call (S_call number)) a ...)
     (let-values [(l_call ...) (S_call (thunk Δ l_call) ...)]
       e_rest))])

(define-judgment-form
  DefaultCalculus
  #:mode (compiles-scope I I O)
  #:contract (compiles-scope P S σ)
  [(where σ (lookup-scope P S))
   (where (scope S a ...) σ)
   (where (Sₙ_i ...) (calls σ))
   (where (x_i ...) (local-vars σ))
   (compiles-atoms P S · (a ...) e)
   ----------------------------------- "C-Scope"
   (compiles-scope P S
     (define (S x_i ...)
       (init (Sₙ_i ...) P e)))])

(define-judgment-form
  DefaultCalculus
  #:mode (compiles I O)
  #:contract (compiles P P)
  [(where P (σ_sl ...))
   (where ((scope S a ...) ...) (σ_sl ...))
   (compiles-scope P S σ_dc) ...
   ------------------------------------------ "C-Program"
   (compiles (σ_sl ...) (σ_dc ...))])

(test-equal
 (judgment-holds (compiles P1/ScopeLanguage P) P)
 (list (term P1/DefaultCalculus)))

(test-equal
 (judgment-holds (compiles P2/ScopeLanguage P) P)
 (list (term P2/DefaultCalculus)))

(test-equal
 (judgment-holds (compiles P3/ScopeLanguage P) P)
 (list (term P3/DefaultCalculus)))

#| _____Translation rules from default calculus to lambda calculus_____ |#

(define-judgment-form
  EnrichedLambdaCalculus
  #:mode (translates I O)
  #:contract (translates e e)
  [
   ------------------------ "C-EmptyError"
   (translates ∅ (raise ∅))]

  [
   ------------------------ "C-ConflictError"
   (translates ⊛ (raise ⊛))]

  [
   ---------------- "C-Var"
   (translates x x)]

  [
   -------------------------- "C-Var/Subscope"
   (translates (Sₙ x) (Sₙ x))]

  [
   ---------------------- "C-Literal/true"
   (translates true true)]

  [
   ------------------------ "C-Literal/false"
   (translates false false)]

  [
   ------------------ "C-Literal/unit"
   (translates () ())]

  [(translates e e_prime)
   ---------------------------------------------- "C-Abs"
   (translates (λ [x : τ] e) (λ [x : τ] e_prime))]

  [(translates e_1 e_1_prime)
   (translates e_2 e_2_prime)
   -------------------------------------------- "C-App"
   (translates (e_1 e_2) (e_1_prime e_2_prime))]

  [(translates e_i e_i_prime) ...
   ---------------------------------------------------- "C-Values"
   (translates (values e_i ...) (values e_i_prime ...))]

  [(translates l_i l_i_prime) ...
   (translates e_assign e_assign_prime)
   (translates e_tail e_tail_prime)
   --------------------------------------------- "C-LetValues"
   (translates 
    (let-values [(l_i ...) e_assign] 
      e_tail)
    (let-values [(l_i_prime ...) e_assign_prime]
      e_tail_prime))]

  [(translates e_i e_i_prime) ...
   (translates e_just e_just_prime)
   (translates e_cons e_cons_prime)
   ----------------------------------------------- "C-Default"
   (translates 
    {e_i ... ¦ e_just :- e_cons}
    (let-values 
        [(r-exceptions)
         (values
          (fold-left
           (λ [acc : (option top)]
             (λ [elt : (unit → top)]
               (let-values 
                   [(elt)
                    (values
                     (try (Some (elt ()))
                          [∅ None]))]
                 (match (values acc elt)
                   [(values None elt)
                    elt]
                   [(values (Some acc) None)
                    (Some acc)]
                   [(values (Some acc) (Some elt))
                    (raise ⊛)]))))
           None
           (list (λ [u : unit] e_i_prime) ...)))]
      (match r-exceptions
        [None (if e_just_prime
                  e_cons_prime
                  (raise ∅))]
        [(Some exception) exception])))])