term.mlish (8639B)
1 #lang s-exp "../../mlish.rkt" 2 (require "../rackunit-typechecking.rkt") 3 4 ;; from chap 6 of RW OCaml 5 6 ;; checks: 7 ;; - nested recursive types (see expr) 8 ;; - labeled adts 9 ;; - records 10 ;; - ho polymorphic fn argument 11 12 (define-type BasicColor 13 Black 14 Red 15 Green 16 Yellow 17 Blue 18 Magenta 19 Cyan 20 White) 21 22 (check-type Cyan : BasicColor) 23 24 (check-type (list Blue Magenta Red) : (List BasicColor)) 25 26 (define (basic-color->int [c : BasicColor] -> Int) 27 (match c with 28 [Black -> 0] [Red -> 1] [Green -> 2] [Yellow -> 3] 29 [Blue -> 4] [Magenta -> 5] [Cyan -> 6] [White -> 7])) 30 31 (define (map [f : (→ X Y)] [lst : (List X)] -> (List Y)) 32 (if (isnil lst) 33 nil 34 (cons (f (head lst)) (map f (tail lst))))) 35 36 (check-type (map basic-color->int (list Blue Red)) 37 : (List Int) -> (list 4 1)) 38 39 (define (color-by-number [n : Int] [txt : String] -> String) 40 (format "\e[38;5;~am~a\e[0m" n txt)) 41 42 (define blue 43 (color-by-number (basic-color->int Blue) "Blue")) 44 45 (check-type blue : String -> "\e[38;5;4mBlue\e[0m") 46 47 (printf "Hello ~a World!\n" blue) 48 49 (define-type Weight Regular Bold) 50 (define-type Color 51 (Basic BasicColor Weight) 52 (RGB Int Int Int) 53 (Gray Int)) 54 55 (check-type (list (RGB 250 70 70) (Basic Green Regular)) 56 : (List Color)) 57 58 (define (color->int [c : Color] -> Int) 59 (match c with 60 [Basic bc w -> 61 (let ([base (match w with [Bold -> 8] [Regular -> 0])]) 62 (+ base (basic-color->int bc)))] 63 [RGB r g b -> 64 (+ 16 (+ b (+ (* g 6) (* r 36))))] 65 [Gray i -> (+ 232 i)])) 66 67 (define (color-print [c : Color] [s : String] -> Unit) 68 (printf "~a\n" (color-by-number (color->int c) s))) 69 70 (color-print (Basic Red Bold) "A bold red!") 71 (color-print (Gray 4) "A muted gray...") 72 73 ;; refactoring Color and Weight 74 (define-type NewColor 75 (NewBasic BasicColor) 76 (NewBold BasicColor) 77 (NewRGB Int Int Int) 78 (NewGray Int)) 79 80 (typecheck-fail 81 (match (NewGray 1) with 82 [Basic bc w -> 83 (let ([base (match w with [Bold -> 8] [Regular -> 0])]) 84 (+ base (basic-color->int bc)))] 85 [RGB r g b -> 86 (+ 16 (+ b (+ (* g 6) (* r 36))))] 87 [Gray i -> (+ 232 i)]) 88 #:with-msg 89 "clauses not exhaustive; missing: NewGray, NewRGB, NewBold, NewBasic") 90 91 (typecheck-fail 92 (match (NewGray 1) with 93 [NewBasic bc w -> 94 (let ([base (match w with [Bold -> 8] [Regular -> 0])]) 95 (+ base (basic-color->int bc)))] 96 [NewRGB r g b -> 97 (+ 16 (+ b (+ (* g 6) (* r 36))))] 98 [NewGray i -> (+ 232 i)]) 99 #:with-msg "clauses not exhaustive; missing: NewBold") 100 101 (typecheck-fail 102 (match (NewGray 1) with 103 [NewBasic bc w -> 104 (let ([base (match w with [Bold -> 8] [Regular -> 0])]) 105 (+ base (basic-color->int bc)))] 106 [NewBold bc -> 1] 107 [NewRGB r g b -> 108 (+ 16 (+ b (+ (* g 6) (* r 36))))] 109 [NewGray i -> (+ 232 i)])) ; todo: better err msg for arity 110 111 (check-type 112 (match (NewGray 1) with 113 [NewBasic bc -> (basic-color->int bc)] 114 [NewBold bc -> (+ 8 (basic-color->int bc))] 115 [NewRGB r g b -> 116 (+ 16 (+ b (+ (* g 6) (* r 36))))] 117 [NewGray i -> (+ 232 i)]) : Int) 118 119 ;; 2016-03-09: match currently does not support else 120 (define-type Details 121 (Logon [user : String] [credentials : String]) 122 (Heartbeat [status : String]) 123 (LogEntry [important? : Bool] [msg : String])) 124 125 (define-type-alias SessionID String) 126 (define-type-alias Time String) 127 (define-type-alias Common (× SessionID Time)) 128 129 (define-type-alias Msg (× Common Details)) 130 131 (define (foldl [f : (→ X Y Y)] [init : Y] [lst : (List X)] -> Y) 132 (if (isnil lst) 133 init 134 (foldl f (f (head lst) init) (tail lst)))) 135 136 (define (msgs-for-user [user : String] [msgs : (List Msg)] -> (List Msg)) 137 (match 138 (foldl 139 (λ ([m : Msg] [res : (× (List Msg) (List SessionID))]) 140 (match res with 141 [ms_out ids_out -> 142 (match m with 143 [common details -> 144 (match common with 145 [id t -> 146 (match details with 147 [Logon u c -> (if (string=? u user) 148 (tup (cons m ms_out) (cons id ids_out)) 149 res)] 150 [Heartbeat st -> (if (member id ids_out) 151 (tup (cons m ms_out) ids_out) 152 res)] 153 [LogEntry i? lmgs -> (if (member id ids_out) 154 (tup (cons m ms_out) ids_out) 155 res)])])])])) 156 (tup nil nil) 157 msgs) with 158 [msgs ids -> (reverse msgs)])) 159 160 ;; this is incomplete (and wrong, eg logentry has wrong arity) code in the book 161 (define (handle-msg [state : Int] [msg : Msg] -> String) 162 (match msg with 163 [common details -> 164 (match details with 165 [LogEntry i? lmsg -> lmsg] 166 [Logon u c -> u] 167 [Heartbeat s -> s])])) 168 169 ;; expr example 170 (define-type (Expr X) 171 (Base X) 172 (Const Bool) 173 (And (List (Expr X))) 174 (Or (List (Expr X))) 175 (Not (Expr X))) 176 177 (define-type MailField To From CC Date Subject) 178 179 (define-type-alias MailPred (×× [field : MailField] 180 [contains? : String])) 181 182 (define (test [f : MailField] [c? : String] -> (Expr MailPred)) 183 (Base (rec [field = f] [contains? = c?]))) 184 185 (check-type (rec [field = To] [contains = "doligez"]) 186 : (×× [field : MailField] [contains : String])) 187 188 (check-type (get (rec [field = To] [contains = "doligez"]) field) 189 : MailField -> To) 190 191 (check-type 192 (And (list (Or (list (Base (rec [field = To] [contains? = "doligez"])) 193 (Base (rec [field = CC] [contains? = "doligez"])))) 194 (Base (rec [field = Subject] [contains? = "runtime"])))) 195 : (Expr MailPred)) 196 197 (define (andmap [f : (→ X Bool)] [lst : (List X)] -> Bool) 198 (if (isnil lst) 199 #t 200 (and (f (head lst)) (andmap f (tail lst))))) 201 (define (ormap [f : (→ X Bool)] [lst : (List X)] -> Bool) 202 (if (isnil lst) 203 #f 204 (or (f (head lst)) (ormap f (tail lst))))) 205 206 (define (filter [p? : (→ X Bool)] [lst : (List X)] -> (List X)) 207 (if (isnil lst) 208 nil 209 (if (p? (head lst)) 210 (cons (head lst) (filter p? (tail lst))) 211 (filter p? (tail lst))))) 212 213 (define (eval [e : (Expr X)] [eval-base : (→ X Bool)] -> Bool) 214 (let ([eval2 (λ ([e : (Expr X)]) (eval e eval-base))]) 215 (match e with 216 [Base base -> (eval-base base)] 217 [Const b -> b] 218 [And es -> (andmap eval2 es)] 219 [Or es -> (ormap eval2 es)] 220 [Not e -> (not (eval2 e))]))) 221 222 (define (andfn [lst : (List (Expr X))] -> (Expr X)) 223 (if (member (Const #f) lst) 224 (Const #f) 225 (let ([lst2 226 (filter (λ ([x : (Expr X)]) (not (equal? x (Const #t)))) lst)]) 227 (if (isnil lst2) 228 (Const #t) 229 (if (isnil (tail lst2)) 230 (head lst2) 231 (And lst2)))))) 232 233 (define (orfn [lst : (List (Expr X))] -> (Expr X)) 234 (if (member (Const #t) lst) 235 (Const #t) 236 (let ([lst2 237 (filter (λ ([x : (Expr X)]) (not (equal? x (Const #f)))) lst)]) 238 (if (isnil lst2) 239 (Const #f) 240 (if (isnil (tail lst2)) 241 (head lst2) 242 (And lst2)))))) 243 244 (define (notfn [e : (Expr X)] -> (Expr X)) 245 (match e with 246 [Base b -> (Not e)] 247 [Const b -> (Const (not b))] 248 [And es -> (Not e)] 249 [Or es -> (Not e)] 250 [Not e2 -> (Not e)])) 251 252 (define (simplify [e : (Expr X)] -> (Expr X)) 253 (match e with 254 [Base b -> e] 255 [Const x -> e] 256 [And es -> (andfn (map (inst simplify X) es))] 257 [Or es -> (orfn (map (inst simplify X) es))] 258 [Not e -> (notfn (simplify e))])) 259 260 (check-type 261 (simplify (Not (And (list (Or (list (Base "it's snowing") 262 (Const #t))) 263 (Base "it's raining"))))) 264 : (Expr String) 265 -> (Not (Base "it's raining"))) 266 267 (check-type 268 (simplify (Not (And (list (Or (list (Base "it's snowing") 269 (Const #t))) 270 (Not (Not (Base "it's raining"))))))) 271 : (Expr String) 272 -> (Not (Not (Not (Base "it's raining"))))) 273 274 (define (notfn2 [e : (Expr X)] -> (Expr X)) 275 (match e with 276 [Const b -> (Const (not b))] 277 [Base b -> (Not e)] 278 [And es -> (Not e)] 279 [Or es -> (Not e)] 280 [Not e -> e])) 281 282 (define (simplify2 [e : (Expr X)] -> (Expr X)) 283 (match e with 284 [Base b -> e] 285 [Const x -> e] 286 [And es -> (andfn (map (inst simplify2 X) es))] 287 [Or es -> (orfn (map (inst simplify2 X) es))] 288 [Not e -> (notfn2 (simplify2 e))])) 289 290 (check-type 291 (simplify2 (Not (And (list (Or (list (Base "it's snowing") 292 (Const #t))) 293 (Not (Not (Base "it's raining"))))))) 294 : (Expr String) 295 -> (Not (Base "it's raining")))