commit ab1703e2d65a4bdd357a239ca56de664b92923fb
parent 512d3fb3784742aa9ac823b5af7cef03e49aa3ad
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 29 Mar 2016 13:55:21 -0400
refactor match; add match support for built-in lists
- remove some redundant expansions
Diffstat:
4 files changed, 180 insertions(+), 76 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -299,84 +299,113 @@
;; match --------------------------------------------------
(define-syntax (match stx)
- (syntax-parse stx #:datum-literals (with ->)
- ;; TODO: eliminate redundant expansions
- [(_ e with . clauses)
- ;; e is tuple
- #:with [e- ty_e] (infer+erase #'e)
- #:when (×? #'ty_e)
- #:with (~× ty ...) #'ty_e
- #:with ([x ... -> e_body]) #'clauses
- #:fail-unless (stx-length=? #'(ty ...) #'(x ...))
- "match clause pattern not compatible with given tuple"
- #:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...) #'e_body)
- #:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
- #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))
- #:with z (generate-temporary)
- (⊢ (let ([z e-])
- (let ([x- (acc z)] ...) e_body-))
- : ty_body)]
- ;; e is variant
- [(_ e with . clauses)
- #:fail-when (null? (syntax->list #'clauses)) "no clauses"
- #:with [e- τ_e] (infer+erase #'e)
- #:with (~! [Clause:id x:id ...
+ (syntax-parse stx #:datum-literals (with)
+ [(_ e with . clauses)
+ #:fail-when (null? (syntax->list #'clauses)) "no clauses"
+ #:with [e- τ_e] (infer+erase #'e)
+ (cond
+ [(×? #'τ_e) ;; e is tuple
+ (syntax-parse #'clauses #:datum-literals (->)
+ [([x ... -> e_body])
+ #:with (~× ty ...) #'τ_e
+ #:fail-unless (stx-length=? #'(ty ...) #'(x ...))
+ "match clause pattern not compatible with given tuple"
+ #:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...) #'e_body)
+ #:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
+ #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))
+ #:with z (generate-temporary)
+ (⊢ (let ([z e-])
+ (let ([x- (acc z)] ...) e_body-))
+ : ty_body)])]
+ [(List? #'τ_e) ;; e is List
+ (syntax-parse #'clauses #:datum-literals (-> ::)
+ [([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
+ (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'())))
+ -> e_body] ...)
+ #:fail-unless (stx-ormap (lambda (xx) (and (brack? xx) (zero? (stx-length xx)))) #'(xs ...))
+ "match: missing empty list case"
+ #:fail-when (and (stx-andmap brack? #'(xs ...))
+ (= 1 (stx-length #'(xs ...))))
+ "match: missing non-empty list case"
+ #:with (~List ty) #'τ_e
+ #:with ([(x- ... rst-) e_body- ty_body] ...)
+ (stx-map (lambda (ctx e) (infer/ctx+erase ctx e))
+ #'(([x ty] ... [rst (List ty)]) ...) #'(e_body ...))
+ #:with τ_out (stx-car #'(ty_body ...))
+ #:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))
+ #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'= #'>=)) #'(xs ...))
+ #:with (pred? ...) (stx-map
+ (lambda (l lo) #`(λ (lst) (#,lo (length lst) #,l)))
+ #'(len ...) #'(lenop ...))
+ #:with ((acc1 ...) ...) (stx-map
+ (lambda (xs)
+ (for/list ([(x i) (in-indexed (syntax->list xs))])
+ #`(lambda (lst) (list-ref lst #,(datum->syntax #'here i)))))
+ #'((x ...) ...))
+ #:with (acc2 ...) (stx-map (lambda (l) #`(lambda (lst) (list-tail lst #,l))) #'(len ...))
+ (⊢ (let ([z e-])
+ (cond
+ [(pred? z)
+ (let ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))
+ : τ_out)])]
+ [else ;; e is variant
+ (syntax-parse #'clauses #:datum-literals (->)
+ [([Clause:id x:id ...
(~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
-> e_c_un] ...) ; un = unannotated with expected ty
- #'clauses ; clauses must stay in same order
- ;; len #'clauses maybe > len #'info, due to guards
- #:with ((~literal #%plain-lambda) (RecName)
- ((~literal let-values) ()
- ((~literal let-values) ()
- . info-body)))
- (get-extra-info #'τ_e)
- #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
- #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
- #:fail-unless (set=? (syntax->datum #'(Clause ...))
- (syntax->datum #'(ConsAll ...)))
- (string-append
- "clauses not exhaustive; missing: "
- (string-join
- (map symbol->string
- (set-subtract
- (syntax->datum #'(ConsAll ...))
- (syntax->datum #'(Clause ...))))
- ", "))
- #:with ((_ ((~literal quote) Cons) Cons? [_ acc τ] ...) ...)
- (map ; ok to compare symbols since clause names can't be rebound
- (lambda (Cl)
- (stx-findf
- (syntax-parser
- [((~literal #%plain-app) 'C . rst)
- (equal? Cl (syntax->datum #'C))])
- #'info-unfolded))
- (syntax->datum #'(Clause ...)))
- ;; this commented block experiments with expanding to unsafe ops
- ;; #:with ((acc ...) ...) (stx-map
- ;; (lambda (accs)
- ;; (for/list ([(a i) (in-indexed (syntax->list accs))])
- ;; #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
- ;; #'((acc-fn ...) ...))
- #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
- #:with (e_c ...) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))
- #:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
- (stx-map
- (λ (bs eg+ec) (infers/ctx+erase bs eg+ec))
- #'(([x : τ] ...) ...) #'((e_guard e_c) ...))
- #:fail-unless (and (same-types? #'(τ_guard ...))
- (Bool? (stx-car #'(τ_guard ...))))
- "guard expression(s) must have type bool"
- #:fail-unless (same-types? #'(τ_ec ...))
- (string-append "branches have different types, given: "
- (string-join (stx-map type->str #'(τ_ec ...)) ", "))
- #:with τ_out (stx-car #'(τ_ec ...))
- #:with z (generate-temporary) ; dont duplicate eval of test expr
- (⊢ (let ([z e-])
- (cond
- [(and (Cons? z)
- (let ([x- (acc z)] ...) e_guard-))
- (let ([x- (acc z)] ...) e_c-)] ...))
- : τ_out)]))
+ ;; len #'clauses maybe > len #'info, due to guards
+ #:with ((~literal #%plain-lambda) (RecName)
+ ((~literal let-values) ()
+ ((~literal let-values) ()
+ . info-body)))
+ (get-extra-info #'τ_e)
+ #:with info-unfolded (subst-special #'τ_e #'RecName #'info-body)
+ #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
+ #:fail-unless (set=? (syntax->datum #'(Clause ...))
+ (syntax->datum #'(ConsAll ...)))
+ (string-append
+ "clauses not exhaustive; missing: "
+ (string-join
+ (map symbol->string
+ (set-subtract
+ (syntax->datum #'(ConsAll ...))
+ (syntax->datum #'(Clause ...))))
+ ", "))
+ #:with ((_ ((~literal quote) Cons) Cons? [_ acc τ] ...) ...)
+ (map ; ok to compare symbols since clause names can't be rebound
+ (lambda (Cl)
+ (stx-findf
+ (syntax-parser
+ [((~literal #%plain-app) 'C . rst)
+ (equal? Cl (syntax->datum #'C))])
+ #'info-unfolded))
+ (syntax->datum #'(Clause ...)))
+ ;; this commented block experiments with expanding to unsafe ops
+ ;; #:with ((acc ...) ...) (stx-map
+ ;; (lambda (accs)
+ ;; (for/list ([(a i) (in-indexed (syntax->list accs))])
+ ;; #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
+ ;; #'((acc-fn ...) ...))
+ #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
+ #:with (e_c ...) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))
+ #:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
+ (stx-map
+ (λ (bs eg+ec) (infers/ctx+erase bs eg+ec))
+ #'(([x : τ] ...) ...) #'((e_guard e_c) ...))
+ #:fail-unless (and (same-types? #'(τ_guard ...))
+ (Bool? (stx-car #'(τ_guard ...))))
+ "guard expression(s) must have type bool"
+ #:fail-unless (same-types? #'(τ_ec ...))
+ (string-append "branches have different types, given: "
+ (string-join (stx-map type->str #'(τ_ec ...)) ", "))
+ #:with τ_out (stx-car #'(τ_ec ...))
+ #:with z (generate-temporary) ; dont duplicate eval of test expr
+ (⊢ (let ([z e-])
+ (cond
+ [(and (Cons? z)
+ (let ([x- (acc z)] ...) e_guard-))
+ (let ([x- (acc z)] ...) e_c-)] ...))
+ : τ_out)])])]))
(define-syntax → ; wrapping →
(syntax-parser
diff --git a/tapl/tests/mlish/listpats.mlish b/tapl/tests/mlish/listpats.mlish
@@ -0,0 +1,70 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; pattern matching for built-in lists
+
+(check-type
+ (match (list 1 2) with
+ [[] -> 0]
+ [[x y] -> (+ x y)]) : Int -> 3)
+
+(typecheck-fail
+ (match (list 1 2) with
+ [[x y] -> (+ x y)]) #:with-msg "missing empty list case")
+
+(typecheck-fail
+ (match (list 1 2) with
+ [[] -> 0]) #:with-msg "missing non\\-empty list case")
+
+(check-type
+ (match (list 1 2) with
+ [[] -> 0]
+ [[x y] -> (+ x y)]) : Int -> 3)
+
+(check-type
+ (match (list 1 2) with
+ [[x y] -> (+ x y)]
+ [[] -> 0]) : Int -> 3)
+
+(check-type
+ (match (nil {Int}) with
+ [[x y] -> (+ x y)]
+ [[] -> 0]) : Int -> 0)
+
+(check-type
+ (match (list 1 2 3) with
+ [[] -> (nil {Int})]
+ [x :: rst -> rst]) : (List Int) -> (list 2 3))
+
+(check-type
+ (match (list 1 2 3) with
+ [[] -> (nil {Int})]
+ [x :: y :: rst -> rst]) : (List Int) -> (list 3))
+
+(check-type
+ (match (nil {Int}) with
+ [[] -> (nil {Int})]
+ [x :: y :: rst -> rst]) : (List Int) -> (nil {Int}))
+
+(check-type
+ (match (list 1 2 3) with
+ [[] -> 0]
+ [x :: y :: rst -> (+ x y)]) : Int -> 3)
+
+(check-type
+ (match (list 1 2 3) with
+ [[] -> 0]
+ [[x] -> 2]
+ [x :: rst -> 3]) : Int -> 3)
+
+(check-type
+ (match (list 1) with
+ [[] -> 0]
+ [[x] -> 2]
+ [x :: rst -> 3]) : Int -> 2)
+
+(check-type
+ (match (list 1) with
+ [[] -> 0]
+ [x :: rst -> 3]
+ [[x] -> 2]) : Int -> 3)
diff --git a/tapl/tests/run-mlish-tests1.rkt b/tapl/tests/run-mlish-tests1.rkt
@@ -1,6 +1,8 @@
#lang racket
(require "mlish-tests.rkt")
(require "mlish/queens.mlish")
+(require "mlish/listpats.mlish")
+
;; (require "mlish/trees.mlish")
;; (require "mlish/chameneos.mlish")
;; (require "mlish/ack.mlish")
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -422,6 +422,9 @@
(define (brace? stx)
(define paren-shape/#f (syntax-property stx 'paren-shape))
(and paren-shape/#f (char=? paren-shape/#f #\{)))
+ (define (brack? stx)
+ (define paren-shape/#f (syntax-property stx 'paren-shape))
+ (and paren-shape/#f (char=? paren-shape/#f #\[)))
;; todo: abstract out the common shape of a type constructor,
;; i.e., the repeated pattern code in the functions below
(define (get-extra-info t)
