pretty print the result

Signed-off-by: Lîm Tsú-thuàn <[email protected]>

main.rkt

@@ -9,7 +9,8 @@
    #:program "whisper"
    #:args ()
    ; let Nat : U = (N : U) -> (N -> N) -> N -> N;
-   (define tm #'(let id : ((A : U) -> (A -> A)) = (lam A (lam x x))
-                  in (id U)))
-   (define ty (infer-empty (parse tm)))
-   (printf "type of term ~a is ~a~n" tm (readback '() ty))))
+   (define tm (parse
+               #'(let id : ((A : U) -> (A -> A)) = (lam A (lam x x))
+                   in (id U))))
+   (define ty (infer-empty tm))
+   (printf "type of term:~n~n~a~n~nis~n~n~a~n" tm (readback '() ty))))

term.rkt

@@ -2,11 +2,39 @@
 (provide (all-defined-out))
 (define-type Name Symbol)
 
-(struct Univ () #:transparent)
-(struct Var ([x : Name]) #:transparent)
-(struct App ([f : Tm] [arg : Tm]) #:transparent)
-(struct Lam ([x : Name] [body : Tm]) #:transparent)
-(struct Pi ([x : Name] [x-ty : Ty] [body : Ty]) #:transparent)
-(struct Let ([x : Name] [a : Ty] [t : Tm] [body : Tm]) #:transparent)
+(struct Univ ()
+  #:property prop:custom-write
+  (λ (_v port _mode)
+    (fprintf port "𝕌"))#:transparent)
+(struct Var ([x : Name])
+  #:property prop:custom-write
+  (λ (v port _mode)
+    (match-define (Var x) v)
+    (fprintf port "~a" x))
+  #:transparent)
+(struct App ([f : Tm] [arg : Tm])
+  #:property prop:custom-write
+  (λ (v port _mode)
+    (match-define (App t u) v)
+    (fprintf port "~a ~a" t u))
+  #:transparent)
+(struct Lam ([x : Name] [body : Tm])
+  #:property prop:custom-write
+  (λ (v port _mode)
+    (match-define (Lam x t) v)
+    (fprintf port "λ~a.~a" x t))
+  #:transparent)
+(struct Pi ([x : Name] [x-ty : Ty] [body : Ty])
+  #:property prop:custom-write
+  (λ (v port _mode)
+    (match-define (Pi x a b) v)
+    (fprintf port "Π(~a : ~a).~a" x a b))
+  #:transparent)
+(struct Let ([x : Name] [a : Ty] [t : Tm] [body : Tm])
+  #:property prop:custom-write
+  (λ (v port _mode)
+    (match-define (Let x a t u) v)
+    (fprintf port "let ~a : ~a = ~a;~n~a" x a t u))
+  #:transparent)
 (define-type Tm (U Univ Var App Lam Pi Let))
 (define-type Ty Tm)