improve how patterns can refer to each other
This commit is contained in:
AlexKnauth
parent
a4fd3312e5
commit
b5541ae278
|
|
@ -89,11 +89,11 @@
|
|||
(typecheck-fail
|
||||
(open [counter <= counterADT with Counter]
|
||||
(+ (proj counter new) 1))
|
||||
#:with-msg "expected: +Int, Int\n *given: +Counter, Int\n *expressions: +\\(proj counter new\\), 1")
|
||||
#:with-msg "expected Int, given Counter\n *expression: \\(proj counter new\\)")
|
||||
(typecheck-fail
|
||||
(open [counter <= counterADT with Counter]
|
||||
((λ ([x : Int]) x) (proj counter new)))
|
||||
#:with-msg "expected: +Int\n *given: +Counter\n *expressions: +\\(proj counter new\\)")
|
||||
#:with-msg "expected Int, given Counter\n *expression: \\(proj counter new\\)")
|
||||
(check-type
|
||||
(open [counter <= counterADT with Counter]
|
||||
((proj counter get) ((proj counter inc) (proj counter new))))
|
||||
|
|
|
|||
|
|
@ -14,10 +14,10 @@
|
|||
|
||||
(typecheck-fail
|
||||
((λ ([x : Unit]) x) 2)
|
||||
#:with-msg "expected: +Unit\n *given: +Int")
|
||||
#:with-msg "expected Unit, given Int\n *expression: 2")
|
||||
(typecheck-fail
|
||||
((λ ([x : Unit]) x) void)
|
||||
#:with-msg "expected: +Unit\n *given: +\\(→ Unit\\)")
|
||||
#:with-msg "expected Unit, given \\(→ Unit\\)\n *expression: void")
|
||||
|
||||
(check-type ((λ ([x : Unit]) x) (void)) : Unit)
|
||||
|
||||
|
|
@ -56,24 +56,32 @@
|
|||
(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
|
||||
(typecheck-fail
|
||||
(let ([x #f]) (+ x 1))
|
||||
#:with-msg "expected: +Int, Int\n *given: +Bool, Int\n *expressions: x, 1")
|
||||
#:with-msg "expected Int, given Bool\n *expression: x")
|
||||
(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))
|
||||
#:with-msg "x: unbound identifier")
|
||||
|
||||
(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
|
||||
(typecheck-fail
|
||||
(let* ([x #t] [y (+ x 1)]) 1)
|
||||
#:with-msg "expected: +Int, Int\n *given: +Bool, Int\n *expressions: x, 1")
|
||||
#:with-msg "expected Int, given Bool\n *expression: x")
|
||||
|
||||
; letrec
|
||||
(typecheck-fail
|
||||
(letrec ([(x : Int) #f] [(y : Int) 1]) y)
|
||||
#:with-msg
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1")
|
||||
"letrec: type mismatch: expected Int, given Bool\n *expression: #f")
|
||||
(typecheck-fail
|
||||
(letrec ([(y : Int) 1] [(x : Int) #f]) x)
|
||||
#:with-msg
|
||||
"letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f")
|
||||
"letrec: type mismatch: expected Int, given Bool\n *expression: #f")
|
||||
(typecheck-fail
|
||||
(ann (letrec ([(x : Int) #f] [(y : Int) 1]) y) : Int)
|
||||
#:with-msg
|
||||
"letrec: type mismatch: expected Int, given Bool\n *expression: #f")
|
||||
(typecheck-fail
|
||||
(ann (letrec ([(y : Int) 1] [(x : Int) #f]) x) : Int)
|
||||
#:with-msg
|
||||
"letrec: type mismatch: expected Int, given Bool\n *expression: #f")
|
||||
|
||||
(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
|
||||
|
||||
|
|
@ -110,11 +118,11 @@
|
|||
(typecheck-fail
|
||||
(or "1" #f)
|
||||
#:with-msg
|
||||
"or: type mismatch\n *expected: +Bool, Bool\n *given: +String, Bool\n *expressions: \"1\", #f")
|
||||
"or: type mismatch: expected Bool, given String\n *expression: \"1\"")
|
||||
(typecheck-fail
|
||||
(or #t "2")
|
||||
#:with-msg
|
||||
"or: type mismatch\n *expected: +Bool, Bool\n *given: +Bool, String\n *expressions: #t, \"2\"")
|
||||
"or: type mismatch: expected Bool, given String\n *expression: \"2\"")
|
||||
;; 2016-03-10: change if to work with non-false vals
|
||||
(check-type (if "true" 1 2) : Int -> 1)
|
||||
(typecheck-fail
|
||||
|
|
@ -136,7 +144,7 @@
|
|||
|
||||
(typecheck-fail
|
||||
((λ ([x : Bool]) x) 1)
|
||||
#:with-msg "expected: +Bool\n *given: +Int\n *expressions: +1")
|
||||
#:with-msg "expected Bool, given Int\n *expression: 1")
|
||||
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
|
||||
(typecheck-fail
|
||||
(λ ([f : Int]) (f 1 2))
|
||||
|
|
@ -150,10 +158,10 @@
|
|||
|
||||
(typecheck-fail
|
||||
(+ 1 (λ ([x : Int]) x))
|
||||
#:with-msg "expected: +Int, Int\n *given: +Int, \\(→ Int Int\\)")
|
||||
#:with-msg "expected Int, given \\(→ Int Int\\)\n *expression: \\(λ \\(\\(x : Int\\)\\) x\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (→ Int Int)]) (+ x x))
|
||||
#:with-msg "expected: +Int, Int\n *given: +\\(→ Int Int\\), \\(→ Int Int\\)\n *expressions: x, x")
|
||||
#:with-msg "expected Int, given \\(→ Int Int\\)\n *expression: x")
|
||||
(typecheck-fail
|
||||
((λ ([x : Int] [y : Int]) y) 1)
|
||||
#:with-msg "wrong number of arguments: expected 2, given 1")
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@
|
|||
: (→ (→ Int String) (→ Int String)))
|
||||
(typecheck-fail
|
||||
(inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)
|
||||
#:with-msg "inst: type mismatch\n *expected: +★\n *given: +Int\n *expressions: +1")
|
||||
#:with-msg "inst: type mismatch: expected ★, given Int\n *expression: 1")
|
||||
|
||||
(typecheck-fail
|
||||
(Λ ([tyf : (⇒ ★ ★)]) (λ ([f : (tyapp tyf String)]) (f 1)))
|
||||
|
|
|
|||
|
|
@ -44,10 +44,10 @@
|
|||
|
||||
(typecheck-fail
|
||||
(+ 1 (λ ([x : Int]) x))
|
||||
#:with-msg "expected: +Int, Int\n *given: +Int, \\(→ Int Int\\)")
|
||||
#:with-msg "expected Int, given \\(→ Int Int\\)\n *expression: \\(λ \\(\\(x : Int\\)\\) x\\)")
|
||||
(typecheck-fail
|
||||
(λ ([x : (→ Int Int)]) (+ x x))
|
||||
#:with-msg "expected: +Int, Int\n *given: +\\(→ Int Int\\), \\(→ Int Int\\)")
|
||||
#:with-msg "expected Int, given \\(→ Int Int\\)\n *expression: x")
|
||||
(typecheck-fail
|
||||
((λ ([x : Int] [y : Int]) y) 1)
|
||||
#:with-msg "wrong number of arguments: expected 2, given 1")
|
||||
|
|
@ -58,3 +58,8 @@
|
|||
(typecheck-fail (λ ([x : 1]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a valid type")
|
||||
(typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a valid type")
|
||||
|
||||
(typecheck-fail
|
||||
(ann (ann 5 : Int) : (→ Int))
|
||||
#:with-msg "expected \\(→ Int\\), given Int\n *expression: \\(ann 5 : Int\\)")
|
||||
|
||||
|
|
|
|||
|
|
@ -49,8 +49,8 @@
|
|||
(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])))
|
||||
#:with-msg (string-append "expected: +\\(∨ \\(coffee : Unit\\) \\(tea : Unit\\)\\)\n"
|
||||
" *given: +\\(∨ \\(coffee : Unit\\)\\)"))
|
||||
#:with-msg
|
||||
"expected \\(∨ \\(coffee : Unit\\) \\(tea : Unit\\)\\), given \\(∨ \\(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]))
|
||||
|
|
|
|||
|
|
@ -258,18 +258,10 @@
|
|||
"expected: \\(List Int\\)\n *given: \\(List Bool\\)")
|
||||
(typecheck-fail (Cons {Bool} 1 (Nil {Int}))
|
||||
#:with-msg
|
||||
(string-append
|
||||
"Cons: type mismatch\n"
|
||||
" *expected: +Bool, \\(List Bool\\)\n"
|
||||
" *given: +Int, \\(List Int\\)\n"
|
||||
" *expressions: 1, \\(Nil \\(Int\\)\\)"))
|
||||
"Cons: type mismatch: expected Bool, given Int\n *expression: 1")
|
||||
(typecheck-fail (Cons {Bool} 1 Nil)
|
||||
#:with-msg
|
||||
(string-append
|
||||
"Cons: type mismatch\n"
|
||||
" *expected: +Bool, \\(List Bool\\)\n"
|
||||
" *given: +Int, \\(List Bool\\)\n"
|
||||
" *expressions: 1, Nil"))
|
||||
"Cons: type mismatch: expected Bool, given Int\n *expression: 1")
|
||||
|
||||
(typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1])
|
||||
#:with-msg "Nil: no expected type, add annotations")
|
||||
|
|
|
|||
|
|
@ -175,15 +175,27 @@
|
|||
(set-stx-prop/preserved e 'expected-type τ) ; dont type-eval?, ie expand?
|
||||
e))
|
||||
(define (get-expected-type e)
|
||||
(syntax-property e 'expected-type))
|
||||
(get-stx-prop/cd*r e 'expected-type))
|
||||
(define (add-env e env) (set-stx-prop/preserved e 'env env))
|
||||
(define (get-env e) (syntax-property e 'env))
|
||||
|
||||
;; typeof : Syntax -> Type or #f
|
||||
;; Retrieves type of given stx, or #f if input has not been assigned a type.
|
||||
(define (typeof stx #:tag [tag ':])
|
||||
(define ty (syntax-property stx tag))
|
||||
(if (cons? ty) (car ty) ty))
|
||||
(get-stx-prop/car stx tag))
|
||||
|
||||
;; get-stx-prop/car : Syntax Any -> Any
|
||||
(define (get-stx-prop/car stx tag)
|
||||
(define v (syntax-property stx tag))
|
||||
(if (cons? v) (car v) v))
|
||||
|
||||
;; get-stx-prop/cd*r : Syntax Any -> Any
|
||||
(define (get-stx-prop/cd*r stx tag)
|
||||
(cd*r (syntax-property stx tag)))
|
||||
|
||||
;; cd*r : Any -> Any
|
||||
(define (cd*r v)
|
||||
(if (cons? v) (cd*r (cdr v)) v))
|
||||
|
||||
(define (tyvar? X) (syntax-property X 'tyvar))
|
||||
|
||||
|
|
@ -411,6 +423,8 @@
|
|||
(set-stx-prop/preserved stx 'orig (cons orig origs)))
|
||||
(define (get-orig τ)
|
||||
(car (reverse (or (syntax-property τ 'orig) (list τ)))))
|
||||
(define (pass-orig stx orig)
|
||||
(add-orig stx (get-orig orig)))
|
||||
(define (has-orig? stx)
|
||||
(and (syntax-property stx 'orig) #true))
|
||||
(define (type->str ty)
|
||||
|
|
|
|||
|
|
@ -56,8 +56,7 @@
|
|||
|
||||
(define-typed-syntax or
|
||||
[(or e ...) ▶
|
||||
[#:with [Bool* ...] (make-list (stx-length #'[e ...]) #'Bool)]
|
||||
[⊢ [[e ≫ e-] ⇐ (: Bool*)] ...]
|
||||
[⊢ [[e ≫ e-] ⇐ (: Bool)] ...]
|
||||
--------
|
||||
[⊢ [[_ ≫ (or- e- ...)] ⇒ (: Bool)]]])
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#lang macrotypes/tapl/typed-lang-builder
|
||||
(provide (for-syntax current-type=? types=?))
|
||||
(provide only-in (for-syntax current-type=? types=?))
|
||||
|
||||
(begin-for-syntax
|
||||
;; type eval
|
||||
|
|
|
|||
|
|
@ -35,223 +35,151 @@
|
|||
#:with [ctx ...] #'[ctx1.ctx ... ...]])
|
||||
(define-splicing-syntax-class inf
|
||||
#:datum-literals (⊢ ⇒ ⇐ ≫ :)
|
||||
#:attributes ([pre 1] [e-stx 1] [e-pat 1] τ-tagss [τ-pats 1] k-tagss [k-pats 1] [post 1])
|
||||
[pattern (~seq [[e-stx* ≫ e-pat*] ⇒ τ-props*])
|
||||
#:with [:inf] #'[[[e-stx* ≫ e-pat*] ⇒ τ-props* ⇒ ()]]]
|
||||
[pattern (~seq [[e-stx* ≫ e-pat*] ⇒ τ-props*] ooo:elipsis)
|
||||
#:with [:inf] #'[[[e-stx* ≫ e-pat*] ⇒ τ-props* ⇒ ()] ooo]]
|
||||
[pattern (~seq [[e-stx* ≫ e-pat*] ⇒ (τ-props:props) ⇒ (k-props:props)])
|
||||
#:with [pre ...] #'[]
|
||||
#:with [e-stx ...] #'[e-stx*]
|
||||
#:with [e-pat ...] #'[e-pat*]
|
||||
#:with τ-tagss #'(list (list 'τ-props.k ...))
|
||||
#:with [τ-pats ...] #'[[τ-props.v ...]]
|
||||
#:with k-tagss #'(list (list 'k-props.k ...))
|
||||
#:with [k-pats ...] #'[[k-props.v ...]]
|
||||
#:with [post ...] #'[]]
|
||||
[pattern (~seq [[e-stx* ≫ e-pat*] ⇒ (τ-props:props) ⇒ (k-props:props)] ooo:elipsis)
|
||||
#:with [pre ...] #'[]
|
||||
#:with [e-stx ...] #'[e-stx* ooo]
|
||||
#:with [e-pat ...] #'[e-pat* ooo]
|
||||
|
||||
#:with τ-tagss #'(map cdr (syntax->datum #'[[e-stx* τ-props.k ...] ooo]))
|
||||
#:with [τ-pats ...] #'[[τ-props.v ...] ooo]
|
||||
#:with k-tagss #'(map cdr (syntax->datum #'[[e-stx* k-props.k ...] ooo]))
|
||||
#:with [k-pats ...] #'[[k-props.v ...] ooo]
|
||||
#:with [post ...] #'[]]
|
||||
[pattern (~seq [[e-stx* ≫ e-pat*] ⇐ (: τ-stx*)])
|
||||
#:attributes ([e-stx 1] [e-stx-orig 1] [e-pat 1])
|
||||
[pattern (~seq [[e-stx* ≫ e-pat*] ⇒ τ-props*] ooo:elipsis ...)
|
||||
#:with [:inf] #'[[[e-stx* ≫ e-pat*] ⇒ τ-props* ⇒ ()] ooo ...]]
|
||||
[pattern (~seq [[e-stx* ≫ e-pat*] ⇒ (τ-props:props) ⇒ (k-props:props)] ooo:elipsis ...)
|
||||
#:with e-tmp (generate-temporary #'e-pat*)
|
||||
#:with τ-tmp (generate-temporary 'τ)
|
||||
#:with τ-stx-tmp (generate-temporary #'τ-stx*)
|
||||
#:with [pre ...] #'[#:with τ-stx-tmp ((current-type-eval) #'τ-stx*)]
|
||||
#:with [e-stx ...] #'[(add-expected e-stx* τ-stx-tmp)]
|
||||
#:with [e-pat ...] #'[e-pat*]
|
||||
#:with τ-tagss #'(list (list ':))
|
||||
#:with [τ-pats ...] #'[[τ-tmp]]
|
||||
#:with k-tagss #'(list (list))
|
||||
#:with [k-pats ...] #'[[]]
|
||||
#:with [post ...]
|
||||
#'[#:with
|
||||
(~and _
|
||||
(~post
|
||||
(~post
|
||||
(~fail
|
||||
#:unless (typecheck? #'τ-tmp #'τ-stx-tmp)
|
||||
(format "type mismatch: expected ~a, given ~a\n expression: ~s"
|
||||
(type->str #'τ-stx-tmp)
|
||||
(type->str #'τ-tmp)
|
||||
(syntax->datum #'e-stx*))))))
|
||||
this-syntax]]
|
||||
[pattern (~seq [[e-stx* ≫ e-pat*] ⇐ (: τ-stx*)] ooo:elipsis)
|
||||
#:with [e-stx ...] #'[e-stx* ooo ...]
|
||||
#:with [e-stx-orig ...] #'[e-stx* ooo ...]
|
||||
#:with [e-pat ...]
|
||||
#'[(~post
|
||||
(~seq
|
||||
(~and e-tmp
|
||||
(~parse τ-tmp (typeof #'e-tmp))
|
||||
(~parse τ-props.v (typeof #'e-tmp #:tag 'τ-props.k))
|
||||
...
|
||||
(~parse k-props.v (typeof #'τ-tmp #:tag 'k-props.k))
|
||||
...
|
||||
e-pat*)
|
||||
ooo ...))]]
|
||||
[pattern (~seq [[e-stx* ≫ e-pat*] ⇐ (: τ-stx*)] ooo:elipsis ...)
|
||||
#:with e-tmp (generate-temporary #'e-pat*)
|
||||
#:with τ-tmp (generate-temporary 'τ)
|
||||
#:with τ-stx-tmp (generate-temporary #'τ-stx*)
|
||||
#:with [pre ...] #'[#:with [τ-stx-tmp ooo]
|
||||
(stx-map (current-type-eval) #'[τ-stx* ooo])]
|
||||
#:with [e-stx ...] #'[(add-expected e-stx* τ-stx-tmp) ooo]
|
||||
#:with [e-pat ...] #'[e-pat* ooo]
|
||||
#:with τ-tagss #'(map cdr (syntax->datum #'[[τ-stx-tmp :] ooo]))
|
||||
#:with [τ-pats ...] #'[[τ-tmp] ooo]
|
||||
#:with k-tagss #'(list)
|
||||
#:with [k-pats ...] #'[]
|
||||
#:with [post ...]
|
||||
#'[#:with
|
||||
(~and _
|
||||
(~post
|
||||
(~post
|
||||
(~fail
|
||||
#:unless (typechecks? #'[τ-tmp ooo] #'[τ-stx-tmp ooo])
|
||||
(format (string-append "type mismatch\n"
|
||||
" expected: ~a\n"
|
||||
" given: ~a\n"
|
||||
" expressions: ~a")
|
||||
(string-join (stx-map type->str #'[τ-stx-tmp ooo]) ", ")
|
||||
(string-join (stx-map type->str #'[τ-tmp ooo]) ", ")
|
||||
(string-join (map ~s (stx-map syntax->datum #'[e-stx* ooo])) ", "))))))
|
||||
this-syntax]]
|
||||
#:with τ-exp-tmp (generate-temporary 'τ_expected)
|
||||
#:with [e-stx ...] #'[(add-expected e-stx* τ-stx*) ooo ...]
|
||||
#:with [e-stx-orig ...] #'[e-stx* ooo ...]
|
||||
#:with [e-pat ...]
|
||||
#'[(~post
|
||||
(~seq
|
||||
(~and e-tmp
|
||||
(~parse τ-exp-tmp (get-expected-type #'e-tmp))
|
||||
(~parse τ-tmp (typeof #'e-tmp))
|
||||
(~parse
|
||||
(~post
|
||||
(~fail #:when (and (not (typecheck? #'τ-tmp #'τ-exp-tmp))
|
||||
(get-orig #'e-tmp))
|
||||
(format "type mismatch: expected ~a, given ~a\n expression: ~s"
|
||||
(type->str #'τ-exp-tmp)
|
||||
(type->str #'τ-tmp)
|
||||
(syntax->datum (get-orig #'e-tmp)))))
|
||||
(get-orig #'e-tmp))
|
||||
e-pat*)
|
||||
ooo ...))]]
|
||||
)
|
||||
(define-splicing-syntax-class inf*
|
||||
[pattern (~seq inf:inf ...)
|
||||
#:with [pre ...] #'[inf.pre ... ...]
|
||||
#:with [e-stx ...] #'[inf.e-stx ... ...]
|
||||
#:with [e-pat ...] #'[inf.e-pat ... ...]
|
||||
#:with τ-tagss #'(append inf.τ-tagss ...)
|
||||
#:with [τ-pats ...] #'[inf.τ-pats ... ...]
|
||||
#:with k-tagss #'(append inf.k-tagss ...)
|
||||
#:with [k-pats ...] #'[inf.k-pats ... ...]
|
||||
#:with [post ...] #'[inf.post ... ...]])
|
||||
#:with [e-stx-orig ...] #'[inf.e-stx-orig ... ...]
|
||||
#:with [e-pat ...] #'[inf.e-pat ... ...]])
|
||||
(define-splicing-syntax-class clause
|
||||
#:attributes ([stuff 1])
|
||||
#:attributes ([pat 1])
|
||||
#:datum-literals (⊢ ⇒ ⇐ ≫ τ⊑ :)
|
||||
[pattern [⊢ (~and (~seq inf-stuff ...) (~seq inf:inf ...))]
|
||||
#:with [:clause] #'[[() () ⊢ inf-stuff ...]]]
|
||||
[pattern (~seq [⊢ (~and (~seq inf-stuff ...) (~seq inf:inf ...))] ooo:elipsis)
|
||||
#:with [:clause] #'[[() () ⊢ inf-stuff ...] ooo]]
|
||||
[pattern [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ inf:inf*]
|
||||
#:with e:id (generate-temporary)
|
||||
#:with τ:id (generate-temporary)
|
||||
#:with ooo (quote-syntax ...)
|
||||
#:with [stuff ...]
|
||||
#'[inf.pre ...
|
||||
#:with [(tvctx.x- ...) (ctx.x- ...) (e ooo) (τ ooo)]
|
||||
(infer #:tvctx #'(tvctx.ctx ...) #:ctx #'(ctx.ctx ...) #'(inf.e-stx ...))
|
||||
#:with [inf.e-pat ...] #'[e ooo]
|
||||
#:with [inf.τ-pats ...]
|
||||
(for/list ([e (in-list (syntax->list #'[e ooo]))]
|
||||
[tags (in-list inf.τ-tagss)])
|
||||
(for/list ([tag (in-list tags)])
|
||||
(typeof e #:tag tag)))
|
||||
#:with [inf.k-pats ...]
|
||||
(for/list ([τ (in-list (syntax->list #'[τ ooo]))]
|
||||
[tags (in-list inf.k-tagss)])
|
||||
(for/list ([tag (in-list tags)])
|
||||
(typeof τ #:tag tag)))
|
||||
inf.post ...]]
|
||||
[pattern (~seq [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ inf:inf*] ooo:elipsis)
|
||||
#:with e:id (generate-temporary)
|
||||
#:with τ:id (generate-temporary)
|
||||
;TODO: What should these do?
|
||||
#:fail-unless (stx-null? #'[inf.pre ...]) "this type of clause does not support elipses"
|
||||
#:fail-unless (stx-null? #'[inf.post ...]) "this type of clause does not support elipses"
|
||||
[pattern (~seq [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ inf:inf*] ooo:elipsis ...)
|
||||
#:with tvctxss (cond [(stx-null? #'[tvctx.ctx ...]) #'(in-cycle (in-value '()))]
|
||||
[else #'(in-list (syntax->list #'[(tvctx.ctx ...) ooo]))])
|
||||
[else #'(in-list (syntax->list #'[(tvctx.ctx ...) ooo ...]))])
|
||||
#:with ctxss (cond [(stx-null? #'[ctx.ctx ...]) #'(in-cycle (in-value '()))]
|
||||
[else #'(in-list (syntax->list #'[(ctx.ctx ...) ooo]))])
|
||||
#:with [stuff ...]
|
||||
#'[#:with [[(tvctx.x- ...) (ctx.x- ...) (e ooo) (τ ooo)] ooo]
|
||||
(for/list ([tvctxs tvctxss]
|
||||
[ctxs ctxss]
|
||||
[es (in-list (syntax->list #'[(inf.e-stx ...) ooo]))])
|
||||
(infer #:tvctx tvctxs #:ctx ctxs es))
|
||||
#:with [(inf.e-pat ...) ooo] #'[(e ooo) ooo]
|
||||
#:with [(inf.τ-pats ...) ooo]
|
||||
(for/list ([es (in-list (syntax->list #'[(e ooo) ooo]))])
|
||||
(for/list ([e (in-list (syntax->list es))]
|
||||
[tags (in-list inf.τ-tagss)])
|
||||
(for/list ([tag (in-list tags)])
|
||||
(typeof e #:tag tag))))
|
||||
#:with [(inf.k-pats ...) ooo]
|
||||
(for/list ([τs (in-list (syntax->list #'[(τ ooo) ooo]))])
|
||||
(for/list ([τ (in-list (syntax->list τs))]
|
||||
[tags (in-list inf.k-tagss)])
|
||||
(for/list ([tag (in-list tags)])
|
||||
(typeof τ #:tag tag))))]]
|
||||
[else #'(in-list (syntax->list #'[(ctx.ctx ...) ooo ...]))])
|
||||
#:with [pat ...]
|
||||
#'[(~post
|
||||
(~post
|
||||
(~parse
|
||||
[[(tvctx.x- ...) (ctx.x- ...) (inf.e-pat ...) _] ooo ...]
|
||||
(for/list ([tvctxs tvctxss]
|
||||
[ctxs ctxss]
|
||||
[es (in-list (syntax->list #'[(inf.e-stx ...) ooo ...]))]
|
||||
[origs (in-list (syntax->list #'[(inf.e-stx-orig ...) ooo ...]))])
|
||||
(infer #:tvctx tvctxs #:ctx ctxs (stx-map pass-orig es origs))))))]]
|
||||
[pattern [a τ⊑ b]
|
||||
#:with [stuff ...]
|
||||
#'[#:fail-unless (typecheck? #'a #'b)
|
||||
(format "type mismatch: expected ~a, given ~a"
|
||||
(type->str #'b)
|
||||
(type->str #'a))]]
|
||||
#:with [pat ...]
|
||||
#'[(~post
|
||||
(~fail #:unless (typecheck? #'a #'b)
|
||||
(format "type mismatch: expected ~a, given ~a"
|
||||
(type->str #'b)
|
||||
(type->str #'a))))]]
|
||||
[pattern (~seq [a τ⊑ b] ooo:elipsis)
|
||||
#:with [stuff ...]
|
||||
#'[#:fail-unless (typechecks? #'[a ooo] #'[b ooo])
|
||||
(format (string-append "type mismatch\n"
|
||||
" expected: ~a\n"
|
||||
" given: ~a")
|
||||
(string-join (stx-map type->str #'[b ooo]) ", ")
|
||||
(string-join (stx-map type->str #'[a ooo]) ", "))]]
|
||||
#:with [pat ...]
|
||||
#'[(~post
|
||||
(~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
|
||||
(format (string-append "type mismatch\n"
|
||||
" expected: ~a\n"
|
||||
" given: ~a")
|
||||
(string-join (stx-map type->str #'[b ooo]) ", ")
|
||||
(string-join (stx-map type->str #'[a ooo]) ", "))))]]
|
||||
[pattern [#:when condition:expr]
|
||||
#:with [stuff ...]
|
||||
#'[#:when condition]]
|
||||
[pattern [#:with pat:expr expr:expr]
|
||||
#:with [stuff ...]
|
||||
#'[#:with pat expr]]
|
||||
#:with [pat ...]
|
||||
#'[(~fail #:unless condition)]]
|
||||
[pattern [#:with pat*:expr expr:expr]
|
||||
#:with [pat ...]
|
||||
#'[(~post (~parse pat* expr))]]
|
||||
[pattern [#:fail-unless condition:expr message:expr]
|
||||
#:with [stuff ...]
|
||||
#'[#:fail-unless condition message]]
|
||||
#:with [pat ...]
|
||||
#'[(~post (~fail #:unless condition message))]]
|
||||
)
|
||||
(define-syntax-class last-clause
|
||||
#:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
|
||||
[pattern [⊢ [[pat ≫ e-stx] ⇒ (τ-props:props)]]
|
||||
#:with [pre ...]
|
||||
#'[]
|
||||
#:with [stuff ...]
|
||||
#'[(for/fold ([result (quasisyntax/loc this-syntax e-stx)])
|
||||
([tag (in-list (list 'τ-props.k ...))]
|
||||
[τ (in-list (list #`τ-props.v ...))])
|
||||
(assign-type result τ #:tag tag))]]
|
||||
[pattern [⊢ [[pat ≫ e-stx] ⇐ (: τ-pat)]]
|
||||
#:with τ
|
||||
(generate-temporary #'τ-pat)
|
||||
#:with [pre ...]
|
||||
#'[#:with τ (get-expected-type this-syntax)
|
||||
#:with (~and _ (~post (~fail #:unless (syntax-e #'τ)
|
||||
"no expected type, add annotations")))
|
||||
this-syntax
|
||||
#:with τ-pat #'τ]
|
||||
[pattern [⊢ [[pat* ≫ e-stx] ⇐ (: τ-pat)]]
|
||||
#:with stx (generate-temporary 'stx)
|
||||
#:with τ (generate-temporary #'τ-pat)
|
||||
#:with pat
|
||||
#'(~and stx
|
||||
pat*
|
||||
(~parse τ (get-expected-type #'stx))
|
||||
(~post (~post (~fail #:unless (syntax-e #'τ)
|
||||
"no expected type, add annotations")))
|
||||
(~parse τ-pat #'τ))
|
||||
#:with [stuff ...]
|
||||
#'[(assign-type (quasisyntax/loc this-syntax e-stx) #`τ)]]
|
||||
[pattern [pat ≻ e-stx]
|
||||
#:with [pre ...]
|
||||
#'[]
|
||||
#:with [stuff ...]
|
||||
#'[(quasisyntax/loc this-syntax e-stx)]]
|
||||
[pattern [pat #:error msg:expr]
|
||||
#:with [pre ...]
|
||||
#'[]
|
||||
#:with [stuff ...]
|
||||
#'[#:fail-unless #f msg
|
||||
;; should never get here
|
||||
(error msg)]])
|
||||
(define-splicing-syntax-class pat #:datum-literals (⇐ :)
|
||||
[pattern (~seq pat)
|
||||
#:with [stuff ...] #'[]]
|
||||
[pattern (~seq pat ⇐ (: τ-pat))
|
||||
[pattern (~seq pat)]
|
||||
[pattern (~seq pat* ⇐ (: τ-pat))
|
||||
#:with stx (generate-temporary 'stx)
|
||||
#:with τ (generate-temporary #'τ-pat)
|
||||
#:with [stuff ...]
|
||||
#'[#:with τ (get-expected-type this-syntax)
|
||||
#:with (~and _ (~post (~fail #:unless (syntax-e #'τ)
|
||||
"no expected type, add annotations")))
|
||||
this-syntax
|
||||
#:with τ-pat #'τ]])
|
||||
#:with pat
|
||||
#'(~and stx
|
||||
pat*
|
||||
(~parse τ (get-expected-type #'stx))
|
||||
(~post (~post (~fail #:unless (syntax-e #'τ)
|
||||
"no expected type, add annotations")))
|
||||
(~parse τ-pat #'τ))])
|
||||
(define-syntax-class rule #:datum-literals (▶)
|
||||
[pattern [pat:pat ▶
|
||||
clause:clause ...
|
||||
:---
|
||||
last-clause:last-clause]
|
||||
#:with norm
|
||||
#'[(~and pat.pat last-clause.pat)
|
||||
pat.stuff ...
|
||||
last-clause.pre ...
|
||||
clause.stuff ... ...
|
||||
#'[(~and pat.pat
|
||||
last-clause.pat
|
||||
clause.pat ... ...)
|
||||
last-clause.stuff ...]])
|
||||
)
|
||||
(require (for-meta 1 'syntax-classes)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user