#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])))])