From 45f140d6427e2a629c664b8f36561d890788ec0d Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Tue, 8 Dec 2020 10:47:23 -0500
Subject: [PATCH] add form for writing type to file

---
 racket/typed/roles.rkt | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index 8911521..ddac7f8 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -64,7 +64,7 @@
          ;; DEBUG and utilities
          print-type print-role role-strings
          ;; Behavioral Roles
-         export-roles check-simulates lift+define-role
+         export-roles export-type check-simulates lift+define-role
          ;; Extensions
          match cond
          submod for-syntax for-meta only-in except-in
@@ -736,6 +736,13 @@
   ----------------------------------------
   [⊢ 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) ≫
   [⊢ 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