commit d602f445aa3f7e8b2cc2e9c6f66f3bc7392b6253
parent 10b870085a4b94f8a1aef0d8431a0b8cb0019edc
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Mon, 4 Aug 2014 18:49:54 -0400
add multi arg lam, app, and +
Diffstat:
| M | stlc-tests.rkt | | | 20 | ++++++++++---------- |
| M | stlc.rkt | | | 63 | +++++++++++++++++++++++++++++++++++++++++---------------------- |
2 files changed, 51 insertions(+), 32 deletions(-)
diff --git a/stlc-tests.rkt b/stlc-tests.rkt
@@ -1,16 +1,16 @@
#lang s-exp "stlc.rkt"
-(check-type-error ((λ (x : Int) (+ x 1)) "10"))
-(check-type ((λ (x : Int) (+ x 1)) 10) : Int)
-(check-equal? ((λ (x : Int) (+ x 1)) 10) 11)
-(check-type-and-result ((λ (x : Int) (+ x 1)) 10) : Int => 11)
+(check-type-error ((λ ([x : Int]) (+ x 1)) "10"))
+(check-type ((λ ([x : Int]) (+ x 1)) 10) : Int)
+(check-equal? ((λ ([x : Int]) (+ x 1)) 10) 11)
+(check-type-and-result ((λ ([x : Int]) (+ x 1)) 10) : Int => 11)
; HO fn
-(check-type-and-result ((λ (f : (→ Int Int)) (f 10)) (λ (x : Int) (+ x 1))) : Int => 11)
-(check-type (λ (f : (→ Int Int)) (f 10)) : (→ (→ Int Int) Int))
-(check-type (λ (f : (→ Int Int)) (λ (x : Int) (f (f x)))) : (→ (→ Int Int) (→ Int Int)))
+(check-type-and-result ((λ ([f : (→ Int Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
+(check-type (λ ([f : (→ Int Int)]) (f 10)) : (→ (→ Int Int) Int))
+(check-type (λ ([f : (→ Int Int)]) (λ ([x : Int]) (f (f x)))) : (→ (→ Int Int) (→ Int Int)))
(check-type-error (λ (f : (→ Int Int)) (λ (x : String) (f (f x)))))
;; shadowed var
-(check-type-error ((λ (x : Int) ((λ (x : String) x) x)) 10))
-(check-type-and-result ((λ (x : String) ((λ (x : Int) (+ x 1)) 10)) "ten") : Int => 11)
-\ No newline at end of file
+(check-type-error ((λ ([x : Int]) ((λ ([x : String]) x) x)) 10))
+(check-type-and-result ((λ ([x : String]) ((λ ([x : Int]) (+ x 1)) 10)) "ten") : Int => 11)
+\ No newline at end of file
diff --git a/stlc.rkt b/stlc.rkt
@@ -1,14 +1,18 @@
#lang racket
-(require (for-syntax syntax/parse syntax/id-table))
-(provide (except-out (all-from-out racket) λ #%app + #%datum))
+(require (for-syntax syntax/parse syntax/id-table syntax/stx racket/list
+ "stx-utils.rkt"))
+(provide (except-out (all-from-out racket) λ #%app + #%datum let))
-(provide (rename-out [myλ λ] [myapp #%app] [my+ +] [mydatum #%datum]))
+(provide (rename-out [myλ λ] [myapp #%app] [my+ +] [mydatum #%datum] #;[mylet let]))
-(provide Int String Bool →)
+(provide Int String Bool → Listof)
(define Int #f)
(define String #f)
(define Bool #f)
(define → #f)
+(define Listof #f)
+
+(define-for-syntax TYPE-ENV-PROP 'Γ)
(require (for-syntax rackunit))
(provide check-type-error check-type check-type-and-result)
@@ -71,6 +75,15 @@
(local-expand
#`(λ (#,x) #,(syntax-property e 'Γ (hash-set Γ (syntax->datum x) τ)))
'expression null))
+(define-for-syntax (expand/Γ/:=s e outer-e x:τs)
+ (define Γ (or (syntax-property outer-e TYPE-ENV-PROP) (hash)))
+ (define xs (stx-map stx-car x:τs))
+ (define τs (stx-map stx-cadr x:τs))
+ (local-expand
+ #`(λ #,xs #,(syntax-property e TYPE-ENV-PROP
+ (apply hash-set* Γ
+ (append-map (λ (x τ) (list (syntax->datum x) τ)) xs τs))))
+ 'expression null))
(define-syntax (mydatum stx)
(syntax-parse stx
@@ -83,34 +96,40 @@
(define-syntax (my+ stx)
(syntax-parse stx
- [(_ e1 e2)
- #:with e1+ (expand/Γ #'e1 stx)
- #:with e2+ (expand/Γ #'e2 stx)
- #:when (assert-type #'e1+ #'Int)
- #:when (assert-type #'e2+ #'Int)
- (⊢ (syntax/loc stx (+ e1 e2)) #'Int)]))
+ [(_ e ...)
+; [(_ e1 e2)
+; #:with e1+ (expand/Γ #'e1 stx)
+; #:with e2+ (expand/Γ #'e2 stx)
+ #:with (e+ ...) (stx-map (λ (estx) (expand/Γ estx stx)) #'(e ...))
+; #:when (assert-type #'e1+ #'Int)
+; #:when (assert-type #'e2+ #'Int)
+ #:when (andmap (λ (estx) (assert-type estx #'Int)) (syntax->list #'(e+ ...)))
+ (⊢ (syntax/loc stx (+ e+ ...)) #'Int)]))
+; (⊢ (syntax/loc stx (+ e1+ e2+)) #'Int)]))
(define-syntax (myλ stx)
(syntax-parse stx #:datum-literals (:)
- [(_ (x:id : τ1) e)
+ [(_ ([x:id : τ] ...) e)
;; - can't use free-identifier=? for the hash table (or free-id-table)
;; because I have to set the table now, but once I get under the λ, the
;; x's won't be free-id=? to the one in the table
;; use symbols instead of identifiers for now --- should be fine because
;; I'm manually managing the environment
- #:with (lam xs e+) (expand/Γ/:= #'e stx #'x #'τ1)
-; (expand/Γ/:= #'(λ (x) #,(syntax-property #'e 'Γ (hash-set
-; (or (syntax-property stx 'Γ) (hash))
-; (syntax->datum #'x) #'τ1))) stx)
+ #:with (lam xs e+) (expand/Γ/:=s #'e stx #'((x τ) ...))
#:with τ2 (typeof #'e+)
- (⊢ (syntax/loc stx (lam xs e+)) #'(→ τ1 τ2))]))
+ (⊢ (syntax/loc stx (lam xs e+)) #'(→ τ ... τ2))]))
+
+;(define-syntax (mylet stx)
+; (syntax-parse stx #:datum-literals (:)
+; [(_ ([x:id : τ]) e)
+; #:
(define-syntax (myapp stx)
(syntax-parse stx #:literals (→)
- [(_ e1 e2)
- #:with e1+ (expand/Γ #'e1 stx)
- #:with e2+ (expand/Γ #'e2 stx)
- #:with (→ τ1 τ2) (typeof #'e1+)
- #:when (assert-type #'e2+ #'τ1)
- (⊢ (syntax/loc stx (#%app e1+ e2+)) #'τ2)]))
+ [(_ e_fn e_arg ...)
+ #:with e_fn+ (expand/Γ #'e_fn stx)
+ #:with (e_arg+ ...) (stx-map (λ (e) (expand/Γ e stx)) #'(e_arg ...))
+ #:with (→ τ ... τ_res) (typeof #'e_fn+)
+ #:when (andmap assert-type (syntax->list #'(e_arg+ ...)) (syntax->list #'(τ ...)))
+ (⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]))
