add form for writing type to file
This commit is contained in:
parent
95699308dd
commit
45f140d642
|
@ -64,7 +64,7 @@
|
||||||
;; DEBUG and utilities
|
;; DEBUG and utilities
|
||||||
print-type print-role role-strings
|
print-type print-role role-strings
|
||||||
;; Behavioral Roles
|
;; Behavioral Roles
|
||||||
export-roles check-simulates lift+define-role
|
export-roles export-type check-simulates lift+define-role
|
||||||
;; Extensions
|
;; Extensions
|
||||||
match cond
|
match cond
|
||||||
submod for-syntax for-meta only-in except-in
|
submod for-syntax for-meta only-in except-in
|
||||||
|
@ -736,6 +736,13 @@
|
||||||
----------------------------------------
|
----------------------------------------
|
||||||
[⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
|
[⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
|
||||||
|
|
||||||
|
(define-typed-syntax (export-type dest:string τ:type) ≫
|
||||||
|
#:do [(with-output-to-file (syntax-e #'dest)
|
||||||
|
(thunk (pretty-write (synd->proto #'τ.norm)))
|
||||||
|
#:exists 'replace)]
|
||||||
|
----------------------------------------
|
||||||
|
[⊢ (#%app- void-) (⇒ : ★/t)])
|
||||||
|
|
||||||
(define-typed-syntax (lift+define-role x:id e:expr) ≫
|
(define-typed-syntax (lift+define-role x:id e:expr) ≫
|
||||||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs)) (⇒ ν-f ((~and r (~Role (_) _ ...)))) (⇒ ν-s (~effs))]
|
[⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs)) (⇒ ν-f ((~and r (~Role (_) _ ...)))) (⇒ ν-s (~effs))]
|
||||||
;; because turnstile introduces a lot of intdef scopes; ideally, we'd be able to synthesize somethign
|
;; because turnstile introduces a lot of intdef scopes; ideally, we'd be able to synthesize somethign
|
||||||
|
|
Loading…
Reference in New Issue