commit 3a42569f6436ff49997578b3fa90ad20bd52b71a
parent ee2789d7778c1de49af3e0c214a10d3173ce9306
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 22 May 2015 19:00:40 -0400
add records and variants
Diffstat:
5 files changed, 188 insertions(+), 48 deletions(-)
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -95,10 +95,10 @@
(syntax-parse stx #:datum-literals (:)
[(_ e : ascribed-τ)
#:with (e- τ) (infer+erase #'e)
- #:fail-unless (type=? #'ascribed-τ #'τ)
+ #:fail-unless (type=? #'τ #'ascribed-τ)
(format "~a does not have type ~a\n"
(syntax->datum #'e) (syntax->datum #'ascribed-τ))
- (⊢ #'e- #'τ)]))
+ (⊢ #'e- #'ascribed-τ)]))
(define-syntax (let/tc stx)
(syntax-parse stx
diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt
@@ -1,24 +1,85 @@
#lang racket/base
(require
- (for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
+ (for-syntax racket/base syntax/parse syntax/stx racket/syntax racket/string
+ "stx-utils.rkt" "typecheck.rkt")
+ (for-meta 2 racket/base syntax/parse racket/syntax)
"typecheck.rkt")
-(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ))
- (except-in "stlc+tup.rkt" #%app λ))
-(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])
- tup proj)
+(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ tup proj let))
+ (except-in "stlc+tup.rkt" #%app λ tup proj let))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ] [stlc:let let]))
(provide (all-from-out "stlc+tup.rkt"))
-
+;(provide define-type-alias define-variant module quote submod)
+(provide tup proj var case)
+
+
;; Simply-Typed Lambda Calculus, plus variants
+;; define-type-alias (also provided to programmer)
;; Types:
;; - types from stlc+tup.rkt
+;; - extend tuple type × to include records
+;; - sum type constructor ∨
;; Terms:
;; - terms from stlc+tup.rkt
+;; - extend tup to include records
+;; - sums (var)
+
+(provide define-type-alias)
+(define-syntax (define-type-alias stx)
+ (syntax-parse stx
+ [(_ τ:id τ-expanded)
+ (if (identifier? #'τ-expanded)
+ #'(define-syntax τ (make-rename-transformer #'τ-expanded))
+ #'(define-syntax τ
+ (λ (stx)
+ (syntax-parse stx
+ ; τ-expanded must have the context of its use, not definition
+ ; so the appropriate #%app is used
+ [x:id (datum->syntax #'x 'τ-expanded)]))))]))
+
+;; records
+(define-syntax (tup stx)
+ (syntax-parse stx #:datum-literals (=)
+ [(_ [l:str = e] ...)
+ #:with ((e- τ) ...) (infers+erase #'(e ...))
+ (⊢ #'(list (list l e-) ...) #'(× [l τ] ...))]
+ [(_ e ...)
+ #'(stlc:tup e ...)]))
+(define-syntax (proj stx)
+ (syntax-parse stx
+ [(_ rec l:str)
+ #:with (rec- τ_rec) (infer+erase #'rec)
+ #:fail-unless (×? #'τ_rec) "not record type"
+ #:with (× [l_τ τ] ...) #'τ_rec
+ #:with (l_match τ_match) (str-stx-assoc #'l #'((l_τ τ) ...))
+ (⊢ #'(cadr (assoc l rec)) #'τ_match)]
+ [(_ e ...)
+ #'(stlc:proj e ...)]))
+
+
+(define-type-constructor ∨)
-;(provide Integer)
-;(define-syntax Integer (make-rename-transformer #'Int))
-;(define-syntax Integer (λ (stx) (syntax-parse stx [x:id #'Int])))
-(define-type-alias Integer Int)
-;(provide ArithBinOp)
-; expanded form must have context of its use, so it has the proper #%app
-;(define-syntax ArithBinOp (λ (stx) (syntax-parse stx [x:id (datum->syntax #'x '(→ Int Int Int))])))
-(define-type-alias ArithBinOp (→ Int Int Int))
-\ No newline at end of file
+(define-syntax (var stx)
+ (syntax-parse stx #:datum-literals (as =)
+ [(_ l:str = e as τ)
+ #:when (∨? #'τ)
+ #:with (∨ (l_τ τ_l) ...) (eval-τ #'τ)
+ #:with (l_match τ_match) (str-stx-assoc #'l #'((l_τ τ_l) ...))
+ #:with (e- τ_e) (infer+erase #'e)
+ #:when (type=? #'τ_match #'τ_e)
+ (⊢ #'(list l e) #'τ)]))
+(define-syntax (case stx)
+ (syntax-parse stx #:datum-literals (of =>)
+ [(_ e [l:str x => e_l] ...)
+ #:with (e- τ_e) (infer+erase #'e)
+ #:when (∨? #'τ_e)
+ #:with (∨ (l_x τ_x) ...) #'τ_e
+ #:fail-when (null? (syntax->list #'(l ...))) "no clauses"
+ #:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
+ #:fail-unless (stx-andmap stx-str=? #'(l ...) #'(l_x ...)) "case clauses is not exhaustive"
+ #:with (((x-) e_l- τ_el) ...)
+ (stx-map (λ (bs e) (infer/type-ctxt+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
+ #:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
+ (⊢ #'(let ([l_e (car e-)])
+ (cond [(string=? l_e l) (let ([x- (cadr e-)]) e_l-)] ...))
+ (stx-car #'(τ_el ...)))]))
+
+\ No newline at end of file
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
@@ -16,10 +16,16 @@
(define (stx-member v stx)
(member v (syntax->list stx) free-identifier=?))
-
+(define (str-stx-member v stx)
+ (member (datum->syntax v) (map datum->syntax (syntax->list stx)) string=?))
+(define (str-stx-assoc v stx)
+ (assoc v (map syntax->list (syntax->list stx)) stx-str=?))
(define (stx-length stx) (length (syntax->list stx)))
(define (stx-last stx) (last (syntax->list stx)))
(define (stx-list-ref stx i)
- (list-ref (syntax->list stx) i))
-\ No newline at end of file
+ (list-ref (syntax->list stx) i))
+
+(define (stx-str=? s1 s2)
+ (string=? (syntax-e s1) (syntax-e s2)))
+\ No newline at end of file
diff --git a/tapl/tests/stlc+var-tests.rkt b/tapl/tests/stlc+var-tests.rkt
@@ -1,12 +1,83 @@
#lang s-exp "../stlc+var.rkt"
(require "rackunit-typechecking.rkt")
+;; define-type-alias
+(define-type-alias Integer Int)
+(define-type-alias ArithBinOp (→ Int Int Int))
+
(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer)
(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int)
(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer)
(check-type + : ArithBinOp)
(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
+;; records (ie labeled tuples)
+(check-type "Stephen" : String)
+(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+ (× ["name" String] ["phone" Int] ["male?" Bool]))
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+ : String ⇒ "Stephen")
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name")
+ : String ⇒ "Stephen")
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone")
+ : Int ⇒ 781)
+(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?")
+ : Bool ⇒ #t)
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+ (× ["my-name" String] ["phone" Int] ["male?" Bool]))
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+ (× ["name" String] ["my-phone" Int] ["male?" Bool]))
+(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
+ (× ["name" String] ["phone" Int] ["is-male?" Bool]))
+
+
+(check-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit]))
+(check-not-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
+(typecheck-fail ((λ ([x : (∨ ["coffee" Unit] ["tea" Unit])]) x)
+ (var "coffee" = (void) as (∨ ["coffee" Unit]))))
+(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) : (∨ ["coffee" Unit] ["tea" Unit]))
+(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
+ : (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit]))
+
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ ["coffee" x => 1])) ; not enough clauses
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ ["coffee" x => 1]
+ ["teaaaaaa" x => 2])) ; wrong clause
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ ["coffee" x => 1]
+ ["tea" x => 2]
+ ["coke" x => 3])) ; too many clauses
+(typecheck-fail
+ (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit]))
+ ["coffee" x => "1"]
+ ["tea" x => 2])) ; mismatched branch types
+(check-type
+ (case (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit]))
+ ["coffee" x => x]
+ ["tea" x => 2]) : Int ⇒ 1)
+(define-type-alias Drink (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool]))
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int))
+(check-type
+ (case ((λ ([d : Drink]) d)
+ (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool])))
+ ["coffee" x => (+ (+ x x) (+ x x))]
+ ["tea" x => 2]
+ ["coke" y => 3])
+ : Int ⇒ 4)
+
+(check-type
+ (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink))
+ ["coffee" x => (+ (+ x x) (+ x x))]
+ ["tea" x => 2]
+ ["coke" y => 3])
+ : Int ⇒ 4)
+
+;; previous tests: ------------------------------------------------------------
;; tests for tuples -----------------------------------------------------------
(check-type (tup 1 2 3) : (× Int Int Int))
(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -46,26 +46,13 @@
[_ #'τ]))
(define τ (void))
(define-for-syntax (τ? stx)
- (syntax-parse stx
+ (syntax-parse (eval-τ stx)
[(τ_arg (... ...))
(for/or ([id (syntax->list #'(τ_arg (... ...)))])
(type=? #'τ id))]
[_ #f]))
)]))
-(define-syntax (define-type-alias stx)
- (syntax-parse stx
- [(_ τ:id τ-expanded)
- #`(begin
- (provide τ)
- #,(if (identifier? #'τ-expanded)
- #'(define-syntax τ (make-rename-transformer #'τ-expanded))
- #'(define-syntax τ
- (λ (stx)
- (syntax-parse stx
- ; τ-expanded must have the context of its use, not definition
- ; so the appropriate #%app is used
- [x:id (datum->syntax #'x 'τ-expanded)])))))]))
;; type classes
(begin-for-syntax
(define (errmsg:bad-type τ)
@@ -81,9 +68,10 @@
(begin-for-syntax
(define (is-type? τ)
- (if (identifier? τ)
- (identifier-binding τ)
- (stx-andmap is-type? τ)))
+ ;(printf "~a\n" τ)
+ (or (string? (syntax-e τ))
+ (and (identifier? τ) (identifier-binding τ))
+ (and (stx-pair? τ) (stx-andmap is-type? τ))))
;; ⊢ : Syntax Type -> Syntax
;; Attaches type τ to (expanded) expression e.
; (define (⊢ e τ) (syntax-property (quasisyntax/loc e #,e) 'type τ))
@@ -101,6 +89,7 @@
(let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e)))
(list #'xs+ #'e+ (typeof #'e+))]
[([x τ] ...) (infer/type-ctxt+erase #'([x : τ] ...) e)]))
+ ; all xs are bound in the same scope
(define (infers/type-ctxt+erase ctxt es)
(syntax-parse ctxt
[(b:typed-binding ...)
@@ -122,7 +111,10 @@
(define (types=? τs1 τs2)
(and (= (stx-length τs1) (stx-length τs2))
(stx-andmap type=? τs1 τs2)))
-
+ (define (same-types? τs)
+ (define τs-lst (syntax->list τs))
+ (or (null? τs-lst)
+ (andmap (λ (τ) (type=? (car τs-lst) τ)) (cdr τs-lst))))
;; typeof : Syntax -> Type or #f
;; Retrieves type of given stx, or #f if input has not been assigned a type.
(define (typeof stx) (syntax-property stx 'type))
@@ -143,16 +135,21 @@
(stx-andmap assert-type es τs))
(define (eval-τ τ)
- (define app (datum->syntax τ '#%app)) ; #%app in τ's ctxt
- ;; stop right before expanding #%app
- (define maybe-app-τ (local-expand τ 'expression (list app)))
- ;; manually remove app and recursively expand
- (if (identifier? maybe-app-τ) ; base type
- maybe-app-τ
- (syntax-parse maybe-app-τ
- [(τ ...)
- #:with (τ-exp ...) (stx-map eval-τ #'(τ ...))
- #'(τ-exp ...)])))
+ (syntax-parse τ
+ [s:str τ] ; record field
+ [_
+; (printf "eval: ~a\n" τ)
+ (define app (datum->syntax τ '#%app)) ; #%app in τ's ctxt
+ ;; stop right before expanding #%app
+ (define maybe-app-τ (local-expand τ 'expression (list app)))
+ ; (printf "after eval: ~a\n" τ)
+ ;; manually remove app and recursively expand
+ (if (identifier? maybe-app-τ) ; base type
+ maybe-app-τ
+ (syntax-parse maybe-app-τ
+ [(τ ...)
+ #:with (τ-exp ...) (stx-map eval-τ #'(τ ...))
+ #'(τ-exp ...)]))]))
;; type=? : Type Type -> Boolean
;; Indicates whether two types are equal
@@ -168,6 +165,7 @@
; adding a type constructor should extend type equality
; #:datum-literals (→)
[(x:id y:id) (free-identifier=? τ1 τ2)]
+ [(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
[((τ1 ...) (τ2 ...))
(types=? #'(τ1 ...) #'(τ2 ...))]
#;[((x ... → x_out) (y ... → y_out))
@@ -244,6 +242,10 @@
#:when (stx-andmap assert-type #'es+ #'τs-ext)
(⊢ (syntax/loc stx (op . es+)) #'τ_result)])))]))
+(define-for-syntax (mk-pred x) (format-id x "~a?" x))
+(define-for-syntax (mk-acc base field) (format-id base "~a-~a" base field))
+
+
;; type environment -----------------------------------------------------------
#;(begin-for-syntax
