infer a type for fields sans declared type
This commit is contained in:
parent
4cd90a6295
commit
e75af5ae1c
|
@ -156,17 +156,24 @@
|
||||||
(⇒ : ★/t)
|
(⇒ : ★/t)
|
||||||
(⇒ ν-f (τ))])
|
(⇒ ν-f (τ))])
|
||||||
|
|
||||||
(define-typed-syntax (field [x:id τ-f:type e:expr] ...) ≫
|
(define-typed-syntax field
|
||||||
#:fail-unless (stx-andmap flat-type? #'(τ-f ...)) "keep your uppity data outta my fields"
|
[(_ [x:id τ-f:type e:expr] ...) ≫
|
||||||
[⊢ e ≫ e- (⇐ : τ-f)] ...
|
#:cut
|
||||||
#:fail-unless (stx-andmap pure? #'(e- ...)) "field initializers not allowed to have effects"
|
#:fail-unless (stx-andmap flat-type? #'(τ-f ...)) "keep your uppity data outta my fields"
|
||||||
#:with (x- ...) (generate-temporaries #'(x ...))
|
[⊢ e ≫ e- (⇐ : τ-f)] ...
|
||||||
#:with (τ ...) (stx-map type-eval #'((Field τ-f.norm) ...))
|
#:fail-unless (stx-andmap pure? #'(e- ...)) "field initializers not allowed to have effects"
|
||||||
#:with MF (type-eval #'MakesField)
|
#:with (x- ...) (generate-temporaries #'(x ...))
|
||||||
----------------------------------------------------------------------
|
#:with (τ ...) (stx-map type-eval #'((Field τ-f.norm) ...))
|
||||||
[⊢ (erased (field/intermediate [x x- τ e-] ...))
|
#:with MF (type-eval #'MakesField)
|
||||||
(⇒ : ★/t)
|
----------------------------------------------------------------------
|
||||||
(⇒ ν-ep (MF))])
|
[⊢ (erased (field/intermediate [x x- τ e-] ...))
|
||||||
|
(⇒ : ★/t)
|
||||||
|
(⇒ ν-ep (MF))]]
|
||||||
|
[(_ flds ... [x:id e:expr] more-flds ...) ≫
|
||||||
|
#:cut
|
||||||
|
[⊢ e ≫ e- (⇒ : τ)]
|
||||||
|
--------------------
|
||||||
|
[≻ (field flds ... [x τ e-] more-flds ...)]])
|
||||||
|
|
||||||
(define-typed-syntax (assert e:expr) ≫
|
(define-typed-syntax (assert e:expr) ≫
|
||||||
[⊢ e ≫ e- (⇒ : τ)]
|
[⊢ e ≫ e- (⇒ : τ)]
|
||||||
|
|
Loading…
Reference in New Issue