commit b439327d78085069960714b0ec9116edfc3fd264
parent 51f9008b9910872afb3be92c3e4914771bf54661
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 20 Apr 2016 13:51:05 -0400
define-type automatically defines accessors and predicates for record variants
Diffstat:
3 files changed, 82 insertions(+), 3 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -1,5 +1,4 @@
#lang s-exp "typecheck.rkt"
-(require (for-syntax syntax/id-set))
(require racket/fixnum racket/flonum)
(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let let* and #%datum begin
@@ -10,7 +9,7 @@
(require (only-in "ext-stlc.rkt" →?))
(require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
(reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
-(require (only-in "stlc+rec-iso.rkt" ~× ×?))
+(require (only-in "stlc+rec-iso.rkt" ~× ×?)) ; using current-type=? from here
(provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
(reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
(require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil)))
@@ -240,9 +239,14 @@
#:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((exposed-acc ...) ...)
+ (stx-map
+ (λ (C fs) (stx-map (λ (f) (format-id C "~a-~a" C f)) fs))
+ #'(Cons ...) #'((fld ...) ...))
#:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
#'(StructName ...) #'((fld ...) ...))
#:with (Cons? ...) (stx-map mk-? #'(StructName ...))
+ #:with (exposed-Cons? ...) (stx-map mk-? #'(Cons ...))
#`(begin
(define-syntax (NameExtraInfo stx)
(syntax-parse stx
@@ -252,6 +256,22 @@
#:extra-info 'NameExtraInfo
#:no-provide)
(struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
+ (define-syntax (exposed-acc stx) ; accessor for records
+ (syntax-parse stx
+ [_:id (⊢ acc (∀ (X ...) (ext-stlc:→ (Name X ...) τ)))]
+ [(o . rst) ; handle if used in fn position
+ #:with app (datum->syntax #'o '#%app)
+ #`(app
+ #,(assign-type #'acc #'(∀ (X ...) (ext-stlc:→ (Name X ...) τ)))
+ . rst)])) ... ...
+ (define-syntax (exposed-Cons? stx) ; predicates for each variant
+ (syntax-parse stx
+ [_:id (⊢ Cons? (∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))]
+ [(o . rst) ; handle if used in fn position
+ #:with app (datum->syntax #'o '#%app)
+ #`(app
+ #,(assign-type #'Cons? #'(∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))
+ . rst)])) ...
(define-syntax (Cons stx)
(syntax-parse stx
; no args and not polymorphic
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -310,6 +310,59 @@
(check-type (λ ([x : X]) (λ ([y : Y]) y)) : (→/test {X} X (→/test {Y} Y Y)))
(check-not-type (λ ([x : X]) (λ ([y : Y]) x)) : (→/test X (→ X X)))
+;; records and automatically-defined accessors and predicates
+(define-type (RecoTest X Y)
+ (RT1 [x : X] [y : Y] [z : String])
+ (RT2 [a : Y] [b : X] [c : (List X)])
+ (RT3 X Y)) ; mixing records and non-records allowed
+
+(check-type RT1-x : (→/test (RecoTest X Y) X))
+(check-type RT1-y : (→/test (RecoTest X Y) Y))
+(check-type RT1-z : (→/test (RecoTest X Y) String))
+(check-type RT2-a : (→/test (RecoTest X Y) Y))
+(check-type RT2-b : (→/test (RecoTest X Y) X))
+
+(check-type RT1? : (→/test (RecoTest X Y) Bool))
+(check-type RT2? : (→/test (RecoTest X Y) Bool))
+(check-type RT3? : (→/test (RecoTest X Y) Bool))
+
+(check-type (RT1-x (RT1 1 #t "2")) : Int -> 1)
+(check-type (RT1-y (RT1 1 #t "2")) : Bool -> #t)
+(check-type (RT1-z (RT1 1 #t "2")) : String -> "2")
+
+(check-type (RT2-a (RT2 1 #f Nil)) : Int -> 1)
+(check-type (RT2-b (RT2 1 #f Nil)) : Bool -> #f)
+(check-type (RT2-c (RT2 1 #f Nil)) : (List Bool) -> Nil)
+
+(check-type (RT1? (RT1 1 2 "3")) : Bool -> #t)
+(check-type (RT1? (RT2 1 2 Nil)) : Bool -> #f)
+(check-type (RT1? (RT3 1 "2")) : Bool -> #f)
+(check-type (RT3? (RT3 1 2)) : Bool -> #t)
+(check-type (RT3? (RT1 1 2 "3")) : Bool -> #f)
+
+(typecheck-fail RT3-x #:with-msg "unbound identifier")
+
+;; accessors produce runtime exception if given wrong variant
+(check-runtime-exn (RT1-x (RT2 1 #f (Cons #t Nil))))
+(check-runtime-exn (RT1-y (RT2 1 #f (Cons #t Nil))))
+(check-runtime-exn (RT1-z (RT2 1 #f (Cons #t Nil))))
+(check-runtime-exn (RT1-x (RT3 1 2)))
+(check-runtime-exn (RT2-a (RT1 1 #f "2")))
+(check-runtime-exn (RT2-c (RT1 1 #f "2")))
+(check-runtime-exn (RT2-c (RT1 1 #f "2")))
+(check-runtime-exn (RT2-a (RT3 #f #t)))
+
+;; non-match version
+(define (rt-fn [rt : (RecoTest X Y)] -> X)
+ (if (RT1? rt)
+ (RT1-x rt)
+ (if (RT2? rt)
+ (RT2-b rt)
+ (match rt with [RT3 x y -> x][RT1 x y z -> x][RT2 a b c -> b]))))
+(check-type (rt-fn (RT1 1 #f "3")) : Int -> 1)
+(check-type (rt-fn (RT2 #f 2 Nil)) : Int -> 2)
+(check-type (rt-fn (RT3 10 20)) : Int -> 10)
+
; ext-stlc tests --------------------------------------------------
diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
@@ -1,6 +1,6 @@
#lang racket/base
(require (for-syntax rackunit syntax/srcloc) rackunit "../typecheck.rkt")
-(provide check-type typecheck-fail check-not-type check-props)
+(provide check-type typecheck-fail check-not-type check-props check-runtime-exn)
(begin-for-syntax
(define (add-esc s) (string-append "\\" s))
@@ -91,3 +91,9 @@
"Expected type check failure but expression ~a has valid type, OR wrong err msg received."
(syntax->datum #'e)))))
#'(void)]))
+
+(define-syntax (check-runtime-exn stx)
+ (syntax-parse stx
+ [(_ e)
+ #:with e- (expand/df #'e)
+ (syntax/loc stx (check-exn exn:fail? (lambda () e-)))]))
