suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

mlish define-type to more closely resemble paper

Browse Source
This commit is contained in:
Stephen Chang 2016-10-05 10:33:18 -04:00
parent 3ec2dfa431
commit cb36097f8d
1 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
turnstile/examples/mlish.rkt
View File

@ -458,23 +458,24 @@
#`(app
#,(assign-type #'Cons? #'(?∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))
. rst)])) ...
;; TODO: remove default provides to use define-typed-syntax here
(define-syntax (Cons stx)
(syntax-parse/typed-syntax stx
; no args and not polymorphic
[C:id ≫
#:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...)))
--------
[_ ≻ (C)]]
[≻ (C)]]
; no args but polymorphic, check expected type
[C:id ⇐ : (NameExpander τ-expected-arg (... ...)) ≫
[:id ⇐ (NameExpander τ-expected-arg (... ...)) ≫
#:when (stx-null? #'(τ ...))
--------
[⊢ [_ ≫ (StructName) ⇐ : _]]]
[⊢ (StructName)]]
; id with multiple expected args, HO fn
[C:id ≫
[:id ≫
#:when (not (stx-null? #'(τ ...)))
--------
[⊢ [_ ≫ StructName ⇒ : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]]]
[⊢ StructName ⇒ (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))]]
[(C τs e_arg ...) ≫
#:when (brace? #'τs) ; commit to this clause
#:with [X* (... ...)] #'[X ...]
@ -482,10 +483,11 @@
#:with {~! τ_X:type (... ...)} #'τs
#:with (τ_in:type (... ...)) ; instantiated types
(inst-types/cs #'(X ...) #'([X* τ_X.norm] (... ...)) #'(τ ...))
[⊢ [e_arg* ≫ e_arg*- ⇐ : τ_in.norm] (... ...)]
;; e_arg* helps align ellipses
[⊢ e_arg* ≫ e_arg*- ⇐ τ_in.norm] (... ...)
#:with [e_arg- ...] #'[e_arg*- (... ...)]
--------
[⊢ [_ ≫ (StructName e_arg- ...) ⇒ : (Name τ_X.norm (... ...))]]]
[⊢ (StructName e_arg- ...) ⇒ (Name τ_X.norm (... ...))]]
[(C . args) ≫ ; no type annotations, must infer instantiation
#:with StructName/ty
(set-stx-prop/preserved
@ -493,7 +495,7 @@
'orig
(list #'C))
--------
[_ ≻ (mlish:#%app StructName/ty . args)]]))
[≻ (mlish:#%app StructName/ty . args)]]))
...)]))
;; match --------------------------------------------------