23 lines
608 B
Racket
23 lines
608 B
Racket
#lang typed-scheme
|
|
#|
|
|
data Exp a =
|
|
Num :: Int -> Exp Int
|
|
Sum :: Int -> Int -> Exp Int
|
|
Zero :: Exp Int -> Exp Bool
|
|
|#
|
|
(define-type-alias number Number)
|
|
(define-type-alias boolean Boolean)
|
|
(define-type-alias top Any)
|
|
|
|
#;(define-typed-struct (a) Exp ([flag : a]))
|
|
(define-typed-struct (a) Num ([v : number]))
|
|
(define-typed-struct (a) Zero ([e : (Un (Num number) (Zero number))]))
|
|
|
|
(define-type-alias (Expr a) (Un (Num a) (Zero a)))
|
|
|
|
(pdefine: (a) (ev [x : (Expr a)]) : a
|
|
(cond
|
|
[(Num? x) (Num-v x)]
|
|
[(Zero? x) (= 0 #{(#{ev :: (All (b) ((Expr b) -> b))} #{(Zero-e x) :: (Expr number)}) :: number})]))
|
|
|