#lang racket (require redex "subst.rkt") (provide L Ev red types) (define-language L (p (e ...)) (e (e e ...) (λ ((x t) ...) e) x (+ e ...) number (amb e ...)) (t (→ t ... t) num) (x variable-not-otherwise-mentioned)) (define-extended-language Ev L (P (e ... E e ...)) (E (v ... E e ...) (+ v ... E e ...) hole) (v (λ ((x t) ...) e) number) (Γ · (x : t Γ))) (define red (reduction-relation Ev #:domain p (--> (in-hole P ((λ ((x t) ..._1) e) v ..._1)) (in-hole P (subst e (x v) ...)) "βv") (--> (in-hole P (+ number_1 ...)) (in-hole P (Σ number_1 ...)) "+") (--> (e_1 ... (in-hole E (amb e_2 ...)) e_3 ...) (e_1 ... (in-hole E e_2) ... e_3 ...) "amb"))) (define-judgment-form Ev #:contract (types Γ e t) #:mode (types I I O) [(types Γ e_1 (→ t_2 ... t_3)) (types Γ e_2 t_2) ... ----- (types Γ (e_1 e_2 ...) t_3)] [(types (x_1 : t_1 Γ) (λ ((x_2 t_2) ...) e) (→ t_2 ... t)) ----- (types Γ (λ ((x_1 t_1) (x_2 t_2) ...) e) (→ t_1 t_2 ... t))] [(types Γ e t) ----- (types Γ (λ () e) (→ t))] [(types (x : t Γ) x t)] [(types Γ x_1 t_1) (side-condition (different x_1 x_2)) ----- (types (x_2 : t_2 Γ) x_1 t_1)] [(types Γ e num) ... ----- (types Γ (+ e ...) num)] [(types Γ number num)] [(types Γ e num) ... ----- (types Γ (amb e ...) num)]) (define-metafunction Ev Σ : number ... -> number [(Σ number ...) ,(apply + (term (number ...)))]) (define-metafunction Ev subst : any (x any) ... -> any [(subst any_body (x any_b) ...) ,(subst/proc x? (term (x ...)) (term (any_b ...)) (term any_body))]) (define x? (redex-match Ev x)) (define-metafunction Ev different : x x -> any [(different x x) #f] [(different x_1 x_2) #t]) (define (progress) (redex-check Ev e (if (types? (term e)) (or (v? (term e)) (reduces? (term e))) #t))) (define (types? e) (not (null? (judgment-holds (types · ,e t) t)))) (define v? (redex-match Ev v)) (define (reduces? e) (not (null? (apply-reduction-relation red (term (,e))))))