types.sire (11885B)
1 ; Copyright 2023 The Plunder Authors 2 ; Use of this source code is governed by a BSD-style license that can be 3 ; found in the LICENSE file. 4 5 #### types <- type_machinery 6 7 :| sire 8 :| type_syntax 9 :| type_machinery 10 11 12 ;;; Utilities ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 13 14 ; TODO: Move these into sire_13_exp (or wherever). 15 16 = (defC sig bodyExp) 17 | OPEN {#=} (sigE sig, bodyExp) 0 18 19 = (defKC key sig bodyExp) 20 | OPEN {#=} (natE key, sigE sig, bodyExp) 0 21 22 = (defKPC key props sig bodyExp) 23 | OPEN {#=} (natE key, cnsE props, sigE sig, bodyExp) 0 24 25 26 ;;; #abstype ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 27 28 ;; {#abstype} is used to backfill things that were earlier in the 29 ;; bootstrapping process than the type system, and things that are 30 ;; built using PLAN primitives (instead of typed-sire constructucts). 31 ;; 32 ;; Pins, Functions, Rows, Tabs, etc. 33 ;; 34 ;; {#abstype} simply defines a new type with no operations, and 35 ;; operations are backfilled retroactivly using {#backfill}. This can 36 ;; be abused to create bindings that don't match their declared types, 37 ;; so don't do that. 38 ;; 39 ;; {#abstype} is also used internally by the versions of {#record}, 40 ;; and {#data} that are exported by this modules. 41 42 = ({#abstype} ss rex err ok) 43 : @(ABSTYPE name args) < parseAbsType rex err 44 @ (_type, ss) | mkNewType name (len args) ss 45 | ok ss `(#*) 46 47 ;;; This section redefines {#record} and {#data} to also generate 48 ;;; a new opaque type. 49 ;;; 50 ;;; TODO This is jank af, break {#record} and {#abstype} into re-usable 51 ;;; parser + code generated and use those here (instead of just manually 52 ;;; expanding both macros and combining the result). 53 54 oldRecord=(.{#record}) 55 oldDataType=(.{#data}) 56 57 = ({#record} st rex err ok) 58 : st tCmd < .{#abstype} st `(abstype#($(idx 1 | rexKids rex))) err 59 : st rCmd < oldRecord st rex err 60 | ok st 61 ` #* $tCmd 62 #* $rCmd 63 64 = ({#data} st rex err ok) 65 : st tCmd < .{#abstype} st `(abstype#($(idx 1 | rexKids rex))) err 66 : st dCmd < oldDataType st rex err 67 | ok st 68 ` #* $tCmd 69 #* $dCmd 70 71 72 ;;; Declare Basic Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 73 74 abstype#Type 75 abstype#TNode 76 abstype#Void 77 abstype#Any 78 abstype#Nat 79 abstype#Pad 80 abstype#(Pin a) 81 abstype#(Fun a b) 82 abstype#Bar 83 abstype#BarTree 84 abstype#Bit 85 abstype#Char 86 abstype#Str 87 abstype#Ordering 88 abstype#Word8 89 abstype#Word16 90 abstype#Word32 91 abstype#Word48 92 abstype#Word64 93 abstype#Rex 94 abstype#(Read a) 95 abstype#(Read2 a b) 96 abstype#(Read3 a b c) 97 abstype#(Read4 a b c d) 98 abstype#(Tab k v) 99 abstype#(Set k) 100 abstype#(Row a) 101 abstype#(Maybe a) 102 abstype#(List a) 103 abstype#(Either a b) 104 105 * # record Unit | UNIT 106 * # record (Sing a) | SING p:a 107 * # record (Pair a b) | PAIR p:a q:b 108 * # record (Trip a b c) | TRIP p:a q:b r:c 109 * # record (Quad a b c d) | QUAD p:a q:b r:c s:d 110 * # record (Pent a b c d e) | PENT p:a q:b r:c s:d t:e 111 * # record (Octo a b c d e f g h) | OCTO p:a q:b r:c s:d t:e u:f v:g w:h 112 113 # record (Row8 a) 114 | ROW8 _:a _:a _:a _:a _:a _:a _:a _:a 115 116 # record (Row16 a) 117 | ROW16 _:a _:a _:a _:a _:a _:a _:a _:a 118 _:a _:a _:a _:a _:a _:a _:a _:a 119 120 abstype#Txp 121 122 = ({#getTypeRoot} ss rex err ok) 123 : _ symbol < rexParseKids rex [readRex readSymbol] err 124 : _ _ bindRow < getBind symbol ss rex err 125 @ [_ v _ _ _ p] | bindRow 126 @ [arity tree] | v 127 | ok ss (cnsE | head tree) 128 129 = anyRoot | getTypeRoot#Any 130 = funRoot | getTypeRoot#Fun 131 = natRoot | getTypeRoot#Nat 132 = typeRoot | getTypeRoot#Type 133 = bitRoot | getTypeRoot#Bit 134 = listRoot | getTypeRoot#List 135 136 = unitRoot | getTypeRoot#Unit 137 = boxRoot | getTypeRoot#Sing 138 = pairRoot | getTypeRoot#Pair 139 = tripRoot | getTypeRoot#Trip 140 = quadRoot | getTypeRoot#Quad 141 = pentRoot | getTypeRoot#Pent 142 143 = (getTypeScheme bind@(PIN [_ val _ _ _ props])) 144 # case (btSearch {isType} props) 145 - NONE | die ({is not a type!}, bind) 146 - SOME _ | val 147 148 =?= Any | FORALL 0 (TCON getTypeRoot#Any []) 149 =?= Fun | FORALL 2 (TCON getTypeRoot#Fun [0 1]) 150 =?= Any | FORALL 0 getTypeRoot#Any 151 =?= Fun | FORALL 2 (getTypeRoot#Fun 0 1) 152 153 =?= 1 | getProp#(Any.isType) 154 155 = (showTypeTree vars x) 156 ^ _ x 157 ? (loop x) 158 | if isNat-x 159 | varE (idx x vars) 160 @ root (head x) 161 @ nam (| lawName | pinItem root) 162 | ifz nam 163 | die [{Is not a type} x] 164 | if (null x) 165 | if (eql root unitRoot) '() 166 | varE nam 167 @ kids (map loop tnodeParams-x) 168 | if (eql root funRoot) 169 @ [x y] kids 170 | if ({>} == rexRune y) 171 @ ySons (rexSons y) 172 | rexSetSons (rowCons x ySons) y 173 | `($x > $y) 174 | if (eql root pairRoot) 175 @ [p q] kids | `($p , $q) 176 | if (eql root tripRoot) 177 @ [p q r] kids | `($p , $q , $r) 178 | if (eql root quadRoot) 179 @ [p q r s] kids | `($p , $q , $r , $s) 180 | if (eql root pentRoot) 181 @ [p q r s t] kids | `($p , $q , $r , $s , $t) 182 | else 183 ^ NEST {|} _ 0 184 | rowCons (varE nam) kids 185 186 = (showType scheme@[arity x]) 187 | showTypeTree (gen arity | add {a}) x 188 189 = (readDefinedSymbol ss rex err ok) 190 : sym < readSymbol rex err 191 : _ _ bind < getBind sym ss rex err 192 | ok sym bind 193 194 = ({#showType} ss rex err ok) 195 @ kids (rexKids rex) 196 | if (len kids /= 2) 197 | err rex {Usage: printType#Type} 198 : symbol < readSymbol (snd kids) err 199 : scheme < lookupType symbol ss err 200 | ok ss | cnsE | OPEN {=} [(varE symbol)] (showType scheme) 201 202 = ({#printType} ss rex err ok) 203 @ kids (rexKids rex) 204 | if (len kids /= 2) 205 | die {Usage: printType#Type} 206 : symbol < readSymbol (snd kids) err 207 : scheme < lookupType symbol ss err 208 | trk 209 | OPEN {=} [(varE symbol)] 210 | showType scheme 211 | ok ss '(#*) 212 213 = (tyApp name scheme params err ok) 214 @ @(FORALL arity topTy) scheme 215 | if (arity /= len params) 216 | err (varE name) {Bad arity in type application} 217 ^ ok (_ topTy) 218 ? (subst x) 219 | if isNat-x (idx x params) 220 | tnodeMapParams subst x 221 222 = (tupleType n) 223 # switch n 224 * 0 | Unit 225 * 1 | Sing 226 * 2 | Pair 227 * 3 | Trip 228 * 4 | Quad 229 * 5 | Pent 230 * 8 | Octo 231 * _ | {todo support bigger tuples: } n 232 233 > SireState > Row Str > Txp > Read Type 234 = (compileType ss vars tExp err ok) 235 ^ : tree < _ tExp 236 | ok (FORALL (len vars) tree) 237 ? (go tExp ret) 238 | tyExpCase tExp 239 * ? (onVAR sym) 240 # case (elemIdx sym vars NONE SOME) 241 - NONE | err varE-sym {unbound type variable} 242 - SOME i | ret (TVAR i) 243 * ? (onTUP exps) 244 : params < rowTraverse go exps 245 @ scheme | tupleType (len exps) 246 : result < tyApp {TUP} scheme params err 247 | ret result 248 * ? (onFUN a b) 249 : x < go a 250 : y < go b 251 : r < tyApp {Fun} Fun [x y] err 252 | ret r 253 * ? (onREF cnstr args) 254 : params < rowTraverse go args 255 : scheme < lookupType cnstr ss err 256 : result < tyApp cnstr scheme params err 257 | ret result 258 259 260 ;;; Parsing ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 261 262 ;;; Type := 263 ;;; 264 ;;; | TyCon 265 ;;; | tyVar 266 ;;; | (Row a) 267 ;;; | Row-a 268 ;;; | (Type > Type) 269 ;;; | (Type > Type > Type) 270 ;;; | (Type > Type > Type > ...) 271 ;;; 272 ;;; | () ;; UNIT=0 273 ;;; | (,) ;; UNIT=0 274 ;;; | ,a [a] ;; *FORBIDDEN* (looks like list type) 275 ;;; | (a, b) ;; Pair a b 276 ;;; | (a, b, c) ;; Trip a b c 277 ;;; | ... 278 279 280 ;;; Macros ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 281 282 ;;; {#typedef} creates a named type based on a type-expression. 283 284 = ({#typedef} ss rex err ok) 285 : @(TYPEDEF name vars expr) < parseTypeDef rex err 286 : scheme < compileType ss vars expr err 287 : ss key < generateUniqueKey ss 288 @ ss | bindTypeAlias key name scheme ss 289 | ok ss `(#*) 290 291 typedef#Symbol#Nat 292 typedef#RexKey#Nat 293 294 typedef#(Key a)#Nat 295 296 # typedef NatOp2 297 (Nat > Nat > Nat) 298 299 # typedef (Foo z) 300 > z > List z > Nat > Nat 301 302 # typedef (Zaz a b c d) 303 > Foo (a,b) 304 > Foo (c,d) 305 > (a,b,c,d) 306 307 printType#NatOp2 308 printType#Foo 309 printType#Zaz 310 printType#Quad 311 printType#Pent 312 printType#Unit 313 printType#Fun 314 315 316 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 317 318 ;;; {>} is the type-annotation rune. It is prefixed directly onto the 319 ;;; same block as the definition it annotates 320 ;;; 321 ;;; > Nat > Nat 322 ;;; (add3 x)=(add 3 x) 323 ;;; 324 ;;; TODO: Support separate blocks for annotation and binding. 325 ;;; 326 ;;; \ add3 : Nat > Nat 327 ;;; 328 ;;; add2:(Nat > Nat) 329 ;;; 330 ;;; (add3 x)=(add 3 x) 331 ;;; 332 ;;; (add2 x)=(add 2 x) 333 ;;; 334 335 = (bindKeyHack ss bindRex err ok) 336 @ sons (rexSons bindRex) 337 @ kids (rexKids bindRex) 338 | if (len kids == 3) 339 : key < readKey (fst kids) err 340 | ok ss key bindRex 341 | if (len kids == 2) 342 : ss key < generateUniqueKey ss 343 | ok ss key | rexSetSons (rowCons natE-key sons) bindRex 344 | else 345 | err bindRex {Wait, this is not a binder??} 346 347 = (loadAnnBindWithHack ss rex err ok) 348 : tExp bindRex < parseTypeAnnotatedBinding rex err 349 @ vars | setToRow (txpFree tExp) 350 : type < compileType ss vars tExp err 351 : ss k bindRex < bindKeyHack ss bindRex err 352 | ok ss type vars k bindRex 353 354 = ({>} ss rex err ok) 355 : ss type _ k bRex < loadAnnBindWithHack ss rex err 356 ; TODO: How to fill the type with this new approach? 357 ; ss | addPropsToLocalBindingByKey ss k #[=type] 358 | ok ss bRex 359 360 ;;; 361 ;;; {#backfill} assigns a type to an existing binding without checking it. 362 ;;; 363 ;;; This is intended as a way to retroactively assign types to things 364 ;;; that we defined before the type system was built, and to give types 365 ;;; to things that are defined directly in terms of PLAN primitives. 366 ;;; 367 ;;; (At the moment, nothing is checked at all, so this isn't actually 368 ;;; different from `>`. In the future it will be, though. 369 ;;; 370 371 = backfillExpected 372 } Expected something like: 373 } 374 } # backfill main 375 } > Int > Ptr (Ptr Char) > IO () 376 377 = ({#backfill} ss rex err ok) 378 @ kids | rexKids rex 379 | if (3 /= len kids) | err rex backfillExpected 380 @ [_ valRex typRex] | kids 381 ; 382 : sym bindRow < readDefinedSymbol ss valRex err 383 : typExp < parseType typRex err 384 @ tyVars | setToRow (txpFree typExp) 385 : scheme < compileType ss tyVars typExp err 386 ; 387 ^ ok _ '(#*) 388 @ [k c bs ms] | ss 389 @ [bk v e bm bn ps] | bindRow 390 ^ (inc k, c, tabPut bs bn _, ms) 391 | PIN [k v e bn c (btPut ps {type} scheme)] 392 393 ;;; {#typeof} prints the type of a binding. It is meant to be used 394 ;;; interactively from the REPL. 395 396 = ({#typeof} ss rex err ok) 397 @ kids@[_ nameRex] (rexKids rex) 398 | if (len kids /= 2) | err rex {Usage: typeof#var} 399 : name < readSymbol nameRex err 400 : type < lookupTypeOf ss name rex err 401 | trk ` \ $(varE name) 402 $(showType type) 403 | ok ss '(#*) 404 405 = ({#showTypeOf} ss rex err ok) 406 @ kids@[_ nameRex] (rexKids rex) 407 | if (len kids /= 2) | err rex {Usage: typeof#var} 408 : name < readSymbol nameRex err 409 : type < lookupTypeOf ss name rex err 410 ^ ok ss (cnsE _) 411 ` \ $(varE name) 412 $(showType type) 413 414 415 ;;; Backfill Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 416 417 * # backfill TRUE Bit 418 * # backfill FALSE Bit 419 * # backfill bit (a > Bit) 420 * # backfill not (Bit > Bit) 421 * # backfill inc (Nat > Nat) 422 * # backfill add (Nat > Nat > Nat) 423 * # backfill div (Nat > Nat > Nat) 424 425 426 ;;; Tests ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 427 428 =?= showType#NatOp2 429 ` = NatOp2 430 (Nat > Nat > Nat) 431 432 =?= showTypeOf#add 433 ` \ add 434 (Nat > Nat > Nat) 435 436 437 ;;; Exports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 438 439 ^-^ 440 ^-^ TNode TCON TVAR 441 ^-^ Type FORALL 442 ^-^ 443 ^-^ showType parseType parseTypeAnnotatedBinding compileType 444 ^-^ txpFree 445 ^-^ bindKeyHack loadAnnBindWithHack 446 ^-^ tnodeMapParams tnodeParams 447 ^-^ 448 ^-^ {#typedef} {#abstype} {#printType} {#typeof} {#backfill} 449 ^-^ {#getTypeRoot} 450 ^-^ 451 ^-^ {#record} {#data} {#case} 452 ^-^ 453 ^-^ {>} 454 ^-^ 455 ^-^ Void Any Type 456 ^-^ Nat Pin Fun 457 ^-^ Ordering 458 ^-^ Bit Pad Char Str 459 ^-^ Word8 Word16 Word32 Word48 Word64 460 ^-^ Rex Read Read2 Read3 Read4 461 ^-^ Row List Set Tab 462 ^-^ Maybe Either 463 ^-^ Bar BarTree 464 ^-^ 465 ^-^ Unit Sing Pair Trip Quad Octo 466 ^-^ Row8 Row16 467 ^-^ 468 ^-^ TRUE FALSE bit not inc add div 469 ^-^ 470 ^-^ funRoot natRoot bitRoot typeRoot listRoot 471 ^-^ tupleType 472 ^-^