Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- #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])
Add Comment
Please, Sign In to add comment