diff --git a/racket/typed/core.rkt b/racket/typed/core.rkt index e06e701..04c0e75 100644 --- a/racket/typed/core.rkt +++ b/racket/typed/core.rkt @@ -560,7 +560,10 @@ (define-typed-syntax (transition e-s e-as) ≫ [⊢ e-s ≫ e-s- ⇒ τ-s] - [⊢ e-as ≫ e-as- ⇒ (~List (~Action τ-o τ-a))] + [⊢ e-as ≫ e-as- ⇒ (~List τ)] + ;; this parsing of actions is getting realllly hacky + #:with (~or (~Action τ-o τ-a) + (~parse (τ-o τ-a) #'(⊥ ⊥))) #'τ ----------------------------------------- [⊢ (syndicate:transition e-s- e-as-) ⇒ (Instruction τ-s τ-o τ-a)]) @@ -569,7 +572,10 @@ ------------------------------------- [⊢ (syndicate:quit) ⇒ (Instruction (U) (U) (U))]] [(quit as) ≫ - [⊢ as ≫ as- ⇒ (~List (~Action τ-o τ-a))] + [⊢ as ≫ as- ⇒ (~List τ)] + ;; this parsing of actions is getting realllly hacky + #:with (~or (~Action τ-o τ-a) + (~parse (τ-o τ-a) (stx-map type-eval #'(⊥ ⊥)))) #'τ ---------------------------------------- [⊢ (syndicate:quit as-) ⇒ (Instruction (U) τ-o τ-a)]]) @@ -1164,4 +1170,10 @@ (check-type (lambda ([e : (Event ⊥)] [s : ★/t]) idle) - : (→ (Event ⊥) ★/t (Instruction ⊥ ⊥ ⊥)))) \ No newline at end of file + : (→ (Event ⊥) ★/t (Instruction ⊥ ⊥ ⊥)))) + +;; transition +(module+ test + (check-type (transition #f (list)) + : (Instruction Bool ⊥ ⊥) + -> (syndicate:transition #f (list-)))) \ No newline at end of file