0 | module Core.TTC

   2 | import Core.Binary.Prims

   3 | import Core.Case.CaseTree

   4 | import Core.CompileExpr

   5 | import Core.Context

   6 | import Core.Env

   7 | import Core.Options

   9 | import Data.IOArray

  10 | import Data.List1

  11 | import Data.Vect

  12 | import Libraries.Data.NameMap

  13 | import Libraries.Data.NatSet

  14 | import Libraries.Data.SparseMatrix

  15 | import Libraries.Data.WithDefault

  17 | import Libraries.Utils.Binary

  18 | import Libraries.Utils.Scheme

  20 | %default covering

  23 | TTC InlineOk where

  24 |   toBuf = toBuf . (YesInline ==)

  25 |   fromBuf = Core.map (\ b => ifThenElse b YesInline NotInline) $ fromBuf

  28 | TTC Namespace where

  29 |   toBuf = toBuf . unsafeUnfoldNamespace

  30 |   fromBuf = Core.map unsafeFoldNamespace $ fromBuf

  33 | TTC ModuleIdent where

  34 |   toBuf = toBuf . unsafeUnfoldModuleIdent

  35 |   fromBuf = Core.map unsafeFoldModuleIdent $ fromBuf

  38 | TTC VirtualIdent where

  39 |   toBuf Interactive = tag 0

  40 |   fromBuf =

  41 |     case !getTag of

  42 |       0 => pure Interactive

  43 |       _ => corrupt "VirtualIdent"

  46 | TTC OriginDesc where

  47 |   toBuf (PhysicalIdrSrc ident) = do tag 0; toBuf ident

  48 |   toBuf (PhysicalPkgSrc fname) = do tag 1; toBuf fname

  49 |   toBuf (Virtual ident) = do tag 2; toBuf ident

  51 |   fromBuf =

  52 |     case !getTag of

  53 |       0 => [| PhysicalIdrSrc (fromBuf) |]

  54 |       1 => [| PhysicalPkgSrc (fromBuf) |]

  55 |       2 => [| Virtual        (fromBuf) |]

  56 |       _ => corrupt "OriginDesc"

  59 | TTC FC where

  60 |   toBuf (MkFC file startPos endPos)

  61 |       = do tag 0; toBuf file; toBuf startPos; toBuf endPos

  62 |   toBuf (MkVirtualFC file startPos endPos)

  63 |       = do tag 2; toBuf file; toBuf startPos; toBuf endPos

  64 |   toBuf EmptyFC = tag 1

  66 |   fromBuf

  67 |       = case !getTag of

  68 |              0 => do f <- fromBuf;

  69 |                      s <- fromBuf; e <- fromBuf

  70 |                      pure (MkFC f s e)

  71 |              1 => pure EmptyFC

  72 |              2 => do f <- fromBuf;

  73 |                      s <- fromBuf; e <- fromBuf

  74 |                      pure (MkVirtualFC f s e)

  75 |              _ => corrupt "FC"

  78 | TTC Name where

  79 |   -- for efficiency reasons we do not encode UserName separately

  80 |   -- hence the nested pattern matches on UN (Basic/Hole/Field)

  81 |   toBuf (NS xs x) = do tag 0; toBuf xs; toBuf x

  82 |   toBuf (UN (Basic x)) = do tag 1; toBuf x

  83 |   toBuf (MN x y) = do tag 2; toBuf x; toBuf y

  84 |   toBuf (PV x y) = do tag 3; toBuf x; toBuf y

  85 |   toBuf (DN x y) = do tag 4; toBuf x; toBuf y

  86 |   toBuf (UN (Field x)) = do tag 5; toBuf x

  87 |   toBuf (Nested x y) = do tag 6; toBuf x; toBuf y

  88 |   toBuf (CaseBlock x y) = do tag 7; toBuf x; toBuf y

  89 |   toBuf (WithBlock x y) = do tag 8; toBuf x; toBuf y

  90 |   toBuf (Resolved x)

  91 |       = throw (InternalError ("Can't write resolved name " ++ show x))

  92 |   toBuf (UN Underscore) = tag 9

  94 |   fromBuf

  95 |       = case !getTag of

  96 |              0 => do xs <- fromBuf

  97 |                      x <- fromBuf

  98 |                      pure (NS xs x)

  99 |              1 => do x <- fromBuf

 100 |                      pure (UN $ Basic x)

 101 |              2 => do x <- fromBuf

 102 |                      y <- fromBuf

 103 |                      pure (MN x y)

 104 |              3 => do x <- fromBuf

 105 |                      y <- fromBuf

 106 |                      pure (PV x y)

 107 |              4 => do x <- fromBuf

 108 |                      y <- fromBuf

 109 |                      pure (DN x y)

 110 |              5 => do x <- fromBuf

 111 |                      pure (UN $ Field x)

 112 |              6 => do x <- fromBuf

 113 |                      y <- fromBuf

 114 |                      pure (Nested x y)

 115 |              7 => do x <- fromBuf

 116 |                      y <- fromBuf

 117 |                      pure (CaseBlock x y)

 118 |              8 => do x <- fromBuf

 119 |                      y <- fromBuf

 120 |                      pure (WithBlock x y)

 121 |              9 => pure (UN Underscore)

 122 |              _ => corrupt "Name"

 125 | TTC RigCount where

 126 |   toBuf = elimSemi

 127 |               (tag 0)

 128 |               (tag 1)

 129 |               (const $ tag 2)

 131 |   fromBuf

 132 |       = case !getTag of

 133 |              0 => pure erased

 134 |              1 => pure linear

 135 |              2 => pure top

 136 |              _ => corrupt "RigCount"

 139 | TTC t => TTC (PiInfo t) where

 140 |   toBuf Implicit = tag 0

 141 |   toBuf Explicit = tag 1

 142 |   toBuf AutoImplicit = tag 2

 143 |   toBuf (DefImplicit r) = do tag 3; toBuf r

 145 |   fromBuf

 146 |       = case !getTag of

 147 |              0 => pure Implicit

 148 |              1 => pure Explicit

 149 |              2 => pure AutoImplicit

 150 |              3 => do t <- fromBuf; pure (DefImplicit t)

 151 |              _ => corrupt "PiInfo"

 154 | TTC t => TTC (PiBindData t) where

 155 |   toBuf (MkPiBindData info ty)

 156 |     = do toBuf info

 157 |          toBuf ty

 158 |   fromBuf

 159 |     = do info <- fromBuf

 160 |          ty <- fromBuf

 161 |          pure (MkPiBindData info ty)

 164 | {fs : _} -> (ev : All (TTC . KeyVal.type) fs) => TTC (Record fs) where

 165 |   toBuf [] = tag 0

 166 |   toBuf {ev = _ :: _} ((lbl :- v) :: y)

 167 |     = do tag 1

 168 |        ; toBuf v ; toBuf y

 170 |   fromBuf {fs = []}

 171 |     = case !getTag of

 172 |            0 => pure []

 173 |            _ => corrupt "Record"

 174 |   fromBuf {fs = (str :-: v :: xs)} {ev = ba :: bs}

 175 |     = case !getTag of

 176 |            1 => do val <- fromBuf @{ba}

 177 |                    tail <- the (Core (Record xs)) fromBuf

 178 |                    pure ((str :- val) :: tail)

 179 |            _ => corrupt "Record"

 182 | {fs : _} -> All (TTC . KeyVal.type) fs => TTC a => TTC (WithData fs a) where

 183 |   toBuf (MkWithData extra val)

 184 |     = do toBuf extra

 185 |          toBuf val

 186 |   fromBuf

 187 |     = do nm <- fromBuf

 188 |          val <- fromBuf

 189 |          pure $ MkWithData nm val

 193 | TTC PrimType where

 194 |   toBuf IntType     = tag 0

 195 |   toBuf Int8Type    = tag 1

 196 |   toBuf Int16Type   = tag 2

 197 |   toBuf Int32Type   = tag 3

 198 |   toBuf Int64Type   = tag 4

 199 |   toBuf IntegerType = tag 5

 200 |   toBuf Bits8Type   = tag 6

 201 |   toBuf Bits16Type  = tag 7

 202 |   toBuf Bits32Type  = tag 8

 203 |   toBuf Bits64Type  = tag 9

 204 |   toBuf StringType  = tag 10

 205 |   toBuf CharType    = tag 11

 206 |   toBuf DoubleType  = tag 12

 207 |   toBuf WorldType   = tag 13

 209 |   fromBuf = case !getTag of

 210 |     0  => pure IntType

 211 |     1  => pure Int8Type

 212 |     2  => pure Int16Type

 213 |     3  => pure Int32Type

 214 |     4  => pure Int64Type

 215 |     5  => pure IntegerType

 216 |     6  => pure Bits8Type

 217 |     7  => pure Bits16Type

 218 |     8  => pure Bits32Type

 219 |     9  => pure Bits64Type

 220 |     10 => pure StringType

 221 |     11 => pure CharType

 222 |     12 => pure DoubleType

 223 |     13 => pure WorldType

 224 |     _  => corrupt "PrimType"

 227 | TTC Constant where

 228 |   toBuf (I x)    = do tag 0;  toBuf x

 229 |   toBuf (I8 x)   = do tag 1;  toBuf x

 230 |   toBuf (I16 x)  = do tag 2;  toBuf x

 231 |   toBuf (I32 x)  = do tag 3;  toBuf x

 232 |   toBuf (I64 x)  = do tag 4;  toBuf x

 233 |   toBuf (BI x)   = do tag 5;  toBuf x

 234 |   toBuf (B8 x)   = do tag 6;  toBuf x

 235 |   toBuf (B16 x)  = do tag 7;  toBuf x

 236 |   toBuf (B32 x)  = do tag 8;  toBuf x

 237 |   toBuf (B64 x)  = do tag 9;  toBuf x

 238 |   toBuf (Str x)  = do tag 10; toBuf x

 239 |   toBuf (Ch x)   = do tag 11; toBuf x

 240 |   toBuf (Db x)   = do tag 12; toBuf x

 241 |   toBuf (PrT x)  = do tag 13; toBuf x

 242 |   toBuf WorldVal = tag 14

 244 |   fromBuf

 245 |       = case !getTag of

 246 |              0  => do x <- fromBuf; pure (I x)

 247 |              1  => do x <- fromBuf; pure (I8 x)

 248 |              2  => do x <- fromBuf; pure (I16 x)

 249 |              3  => do x <- fromBuf; pure (I32 x)

 250 |              4  => do x <- fromBuf; pure (I64 x)

 251 |              5  => do x <- fromBuf; pure (BI x)

 252 |              6  => do x <- fromBuf; pure (B8 x)

 253 |              7  => do x <- fromBuf; pure (B16 x)

 254 |              8  => do x <- fromBuf; pure (B32 x)

 255 |              9  => do x <- fromBuf; pure (B64 x)

 256 |              10 => do x <- fromBuf; pure (Str x)

 257 |              11 => do x <- fromBuf; pure (Ch x)

 258 |              12 => do x <- fromBuf; pure (Db x)

 259 |              13 => do x <- fromBuf; pure (PrT x)

 260 |              14 => pure WorldVal

 261 |              _ => corrupt "Constant"

 264 | TTC LazyReason where

 265 |   toBuf LInf = tag 0

 266 |   toBuf LLazy = tag 1

 267 |   toBuf LUnknown = tag 2

 269 |   fromBuf

 270 |       = case !getTag of

 271 |              0 => pure LInf

 272 |              1 => pure LLazy

 273 |              2 => pure LUnknown

 274 |              _ => corrupt "LazyReason"

 277 | TTC NameType where

 278 |   toBuf Bound = tag 0

 279 |   toBuf Func = tag 1

 280 |   toBuf (DataCon t arity) = do tag 2; toBuf t; toBuf arity

 281 |   toBuf (TyCon arity) = do tag 3; toBuf arity

 283 |   fromBuf

 284 |       = case !getTag of

 285 |              0 => pure Bound

 286 |              1 => pure Func

 287 |              2 => do x <- fromBuf; y <- fromBuf; pure (DataCon x y)

 288 |              3 => do y <- fromBuf; pure (TyCon y)

 289 |              _ => corrupt "NameType"

 297 | mkPrf : (idx : Nat) -> IsVar n idx ns

 298 | mkPrf {n} {ns} Z = believe_me (First {n} {ns = n :: ns})

 299 | mkPrf {n} {ns} (S k) = believe_me (Later {m=n} (mkPrf {n} {ns} k))

 302 |   export

 303 |   {vars : _} -> TTC (Binder (Term vars)) where

 304 |     toBuf (Lam _ c x ty) = do tag 0; toBuf c; toBuf x; toBuf ty

 305 |     toBuf (Let _ c val ty) = do tag 1; toBuf c; toBuf val -- ; toBuf ty

 306 |     toBuf (Pi _ c x ty) = do tag 2; toBuf c; toBuf x; toBuf ty

 307 |     toBuf (PVar _ c p ty) = do tag 3; toBuf c; toBuf p; toBuf ty

 308 |     toBuf (PLet _ c val ty) = do tag 4; toBuf c; toBuf val -- ; toBuf ty

 309 |     toBuf (PVTy _ c ty) = do tag 5; toBuf c -- ; toBuf ty

 311 |     fromBuf

 312 |         = case !getTag of

 313 |                0 => do c <- fromBuf; x <- fromBuf; ty <- fromBuf; pure (Lam emptyFC c x ty)

 314 |                1 => do c <- fromBuf; x <- fromBuf; pure (Let emptyFC c x (Erased emptyFC Placeholder))

 315 |                2 => do c <- fromBuf; x <- fromBuf; y <- fromBuf; pure (Pi emptyFC c x y)

 316 |                3 => do c <- fromBuf; p <- fromBuf; ty <- fromBuf; pure (PVar emptyFC c p ty)

 317 |                4 => do c <- fromBuf; x <- fromBuf; pure (PLet emptyFC c x (Erased emptyFC Placeholder))

 318 |                5 => do c <- fromBuf; pure (PVTy emptyFC c (Erased emptyFC Placeholder))

 319 |                _ => corrupt "Binder"

 321 |   export

 322 |   TTC UseSide where

 323 |     toBuf UseLeft = tag 0

 324 |     toBuf UseRight = tag 1

 326 |     fromBuf

 327 |         = case !getTag of

 328 |                0 => pure UseLeft

 329 |                1 => pure UseRight

 330 |                _ => corrupt "UseSide"

 333 |   export

 334 |   {vars : _} -> TTC (Term vars) where

 335 |     toBuf (Local {name} fc c idx y)

 336 |         = if idx < 243

 337 |              then do tag (13 + cast idx)

 338 |                      toBuf c

 339 |              else do tag 0

 340 |                      toBuf c

 341 |                      toBuf idx

 342 |     toBuf (Ref fc nt name)

 343 |         = do tag 1;

 344 |              toBuf nt; toBuf name

 345 |     toBuf (Meta fc n i xs)

 346 |         = do tag 2;

 347 |              toBuf n; toBuf xs

 348 |     toBuf (Bind fc x bnd scope)

 349 |         = do tag 3;

 350 |              toBuf x;

 351 |              toBuf bnd; toBuf scope

 352 |     toBuf (App fc fn arg)

 353 |         = do let (fn, args) = getFnArgs (App fc fn arg)

 354 |              case args of

 355 |                   [arg] => do tag 4

 356 |                               toBuf fn

 357 |                               toBuf arg

 358 |                   args => do tag 12

 359 |                              toBuf fn

 360 |                              toBuf args

 361 |     toBuf (As fc s as tm)

 362 |         = do tag 5;

 363 |              toBuf as; toBuf s; toBuf tm

 364 |     toBuf (TDelayed fc r tm)

 365 |         = do tag 6;

 366 |              toBuf r; toBuf tm

 367 |     toBuf (TDelay fc r ty tm)

 368 |         = do tag 7;

 369 |              toBuf r; toBuf ty; toBuf tm

 370 |     toBuf (TForce fc r tm)

 371 |         = do tag 8;

 372 |              toBuf r; toBuf tm

 373 |     toBuf (PrimVal fc c)

 374 |         = do tag 9;

 375 |              toBuf c

 376 |     toBuf (Erased fc _)

 377 |         = tag 10

 378 |     toBuf (TType fc u)

 379 |         = do tag 11; toBuf u

 381 |     fromBuf {vars}

 382 |         = case !getTag of

 383 |                0 => do c <- fromBuf

 384 |                        idx <- fromBuf

 385 |                        name <- maybe (corrupt "Term") pure

 386 |                                      (getAt idx vars)

 387 |                        pure (Local {name} emptyFC c idx (mkPrf idx))

 388 |                1 => do nt <- fromBuf; name <- fromBuf

 389 |                        pure (Ref emptyFC nt name)

 390 |                2 => do n <- fromBuf

 391 |                        xs <- fromBuf

 392 |                        pure (Meta emptyFC n 0 xs) -- needs resolving

 393 |                3 => do x <- fromBuf

 394 |                        bnd <- fromBuf; scope <- fromBuf

 395 |                        pure (Bind emptyFC x bnd scope)

 396 |                4 => do fn <- fromBuf

 397 |                        arg <- fromBuf

 398 |                        pure (App emptyFC fn arg)

 399 |                5 => do as <- fromBuf; s <- fromBuf; tm <- fromBuf

 400 |                        pure (As emptyFC s as tm)

 401 |                6 => do lr <- fromBuf; tm <- fromBuf

 402 |                        pure (TDelayed emptyFC lr tm)

 403 |                7 => do lr <- fromBuf;

 404 |                        ty <- fromBuf; tm <- fromBuf

 405 |                        pure (TDelay emptyFC lr ty tm)

 406 |                8 => do lr <- fromBuf; tm <- fromBuf

 407 |                        pure (TForce emptyFC lr tm)

 408 |                9 => do c <- fromBuf

 409 |                        pure (PrimVal emptyFC c)

 410 |                10 => pure (Erased emptyFC Placeholder)

 411 |                11 => do u <- fromBuf; pure (TType emptyFC u)

 412 |                12 => do fn <- fromBuf

 413 |                         args <- fromBuf

 414 |                         pure (apply emptyFC fn args)

 415 |                idxp => do c <- fromBuf

 416 |                           let idx : Nat = fromInteger (cast (idxp - 13))

 417 |                           let Just name = getAt idx vars

 418 |                               | Nothing => corrupt "Term"

 419 |                           pure (Local {name} emptyFC c idx (mkPrf idx))

 422 | TTC Pat where

 423 |   toBuf (PAs fc x y)

 424 |       = do tag 0; toBuf fc; toBuf x; toBuf y

 425 |   toBuf (PCon fc x t arity xs)

 426 |       = do tag 1; toBuf fc; toBuf x; toBuf t; toBuf arity; toBuf xs

 427 |   toBuf (PTyCon fc x arity xs)

 428 |       = do tag 2; toBuf fc; toBuf x; toBuf arity; toBuf xs

 429 |   toBuf (PConst fc c)

 430 |       = do tag 3; toBuf fc; toBuf c

 431 |   toBuf (PArrow fc x s t)

 432 |       = do tag 4; toBuf fc; toBuf x; toBuf s; toBuf t

 433 |   toBuf (PDelay fc x t y)

 434 |       = do tag 5; toBuf fc; toBuf x; toBuf t; toBuf y

 435 |   toBuf (PLoc fc x)

 436 |       = do tag 6; toBuf fc; toBuf x

 437 |   toBuf (PUnmatchable fc x)

 438 |       = do tag 7; toBuf fc; toBuf x

 440 |   fromBuf

 441 |       = case !getTag of

 442 |              0 => do fc <- fromBuf; x <- fromBuf;

 443 |                      y <- fromBuf

 444 |                      pure (PAs fc x y)

 445 |              1 => do fc <- fromBuf; x <- fromBuf

 446 |                      t <- fromBuf; arity <- fromBuf

 447 |                      xs <- fromBuf

 448 |                      pure (PCon fc x t arity xs)

 449 |              2 => do fc <- fromBuf; x <- fromBuf

 450 |                      arity <- fromBuf

 451 |                      xs <- fromBuf

 452 |                      pure (PTyCon fc x arity xs)

 453 |              3 => do fc <- fromBuf; c <- fromBuf

 454 |                      pure (PConst fc c)

 455 |              4 => do fc <- fromBuf; x <- fromBuf

 456 |                      s <- fromBuf; t <- fromBuf

 457 |                      pure (PArrow fc x s t)

 458 |              5 => do fc <- fromBuf; x <- fromBuf;

 459 |                      t <- fromBuf; y <- fromBuf

 460 |                      pure (PDelay fc x t y)

 461 |              6 => do fc <- fromBuf; x <- fromBuf

 462 |                      pure (PLoc fc x)

 463 |              7 => do fc <- fromBuf; x <- fromBuf

 464 |                      pure (PUnmatchable fc x)

 465 |              _ => corrupt "Pat"

 468 |   export

 469 |   {vars : _} -> TTC (CaseTree vars) where

 470 |     toBuf (Case {name} idx x scTy xs)

 471 |         = do tag 0; toBuf name; toBuf idx; toBuf xs

 472 |     toBuf (STerm _ x)

 473 |         = do tag 1; toBuf x

 474 |     toBuf (Unmatched msg)

 475 |         = do tag 2; toBuf msg

 476 |     toBuf Impossible = tag 3

 478 |     fromBuf

 479 |         = case !getTag of

 480 |                0 => do name <- fromBuf; idx <- fromBuf

 481 |                        xs <- fromBuf

 482 |                        pure (Case {name} idx (mkPrf idx) (Erased emptyFC Placeholder) xs)

 483 |                1 => do x <- fromBuf

 484 |                        pure (STerm 0 x)

 485 |                2 => do msg <- fromBuf

 486 |                        pure (Unmatched msg)

 487 |                3 => pure Impossible

 488 |                _ => corrupt "CaseTree"

 490 |   export

 491 |   {vars : _} -> TTC (CaseAlt vars) where

 492 |     toBuf (ConCase x t args y)

 493 |         = do tag 0; toBuf x; toBuf t; toBuf args; toBuf y

 494 |     toBuf (DelayCase ty arg y)

 495 |         = do tag 1; toBuf ty; toBuf arg; toBuf y

 496 |     toBuf (ConstCase x y)

 497 |         = do tag 2; toBuf x; toBuf y

 498 |     toBuf (DefaultCase x)

 499 |         = do tag 3; toBuf x

 501 |     fromBuf

 502 |         = case !getTag of

 503 |                0 => do x <- fromBuf; t <- fromBuf

 504 |                        args <- fromBuf; y <- fromBuf

 505 |                        pure (ConCase x t args y)

 506 |                1 => do ty <- fromBuf; arg <- fromBuf; y <- fromBuf

 507 |                        pure (DelayCase ty arg y)

 508 |                2 => do x <- fromBuf; y <- fromBuf

 509 |                        pure (ConstCase x y)

 510 |                3 => do x <- fromBuf

 511 |                        pure (DefaultCase x)

 512 |                _ => corrupt "CaseAlt"

 515 | {vars : _} -> TTC (Env Term vars) where

 516 |   toBuf [] = pure ()

 517 |   toBuf ((::) bnd env)

 518 |       = do toBuf bnd; toBuf env

 520 |   -- Length has to correspond to length of 'vars'

 521 |   fromBuf {vars = []} = pure []

 522 |   fromBuf {vars = x :: xs}

 523 |       = do bnd <- fromBuf

 524 |            env <- fromBuf

 525 |            pure (bnd :: env)

 528 | TTC Visibility where

 529 |   toBuf Private = tag 0

 530 |   toBuf Export = tag 1

 531 |   toBuf Public = tag 2

 533 |   fromBuf

 534 |       = case !getTag of

 535 |              0 => pure Private

 536 |              1 => pure Export

 537 |              2 => pure Public

 538 |              _ => corrupt "Visibility"

 541 | TTC PartialReason where

 542 |   toBuf NotStrictlyPositive = tag 0

 543 |   toBuf (BadCall xs) = do tag 1; toBuf xs

 544 |   toBuf (BadPath xs n) = do tag 2; toBuf xs; toBuf n

 545 |   toBuf (RecPath xs) = do tag 3; toBuf xs

 547 |   fromBuf

 548 |       = case !getTag of

 549 |              0 => pure NotStrictlyPositive

 550 |              1 => do xs <- fromBuf

 551 |                      pure (BadCall xs)

 552 |              2 => do xs <- fromBuf

 553 |                      n <- fromBuf

 554 |                      pure (BadPath xs n)

 555 |              3 => do xs <- fromBuf

 556 |                      pure (RecPath xs)

 557 |              _ => corrupt "PartialReason"

 560 | TTC Terminating where

 561 |   toBuf Unchecked = tag 0

 562 |   toBuf IsTerminating = tag 1

 563 |   toBuf (NotTerminating p) = do tag 2; toBuf p

 565 |   fromBuf

 566 |       = case !getTag of

 567 |              0 => pure Unchecked

 568 |              1 => pure IsTerminating

 569 |              2 => do p <- fromBuf

 570 |                      pure (NotTerminating p)

 571 |              _ => corrupt "Terminating"

 574 | TTC Covering where

 575 |   toBuf IsCovering = tag 0

 576 |   toBuf (MissingCases ms)

 577 |       = do tag 1

 578 |            toBuf ms

 579 |   toBuf (NonCoveringCall ns)

 580 |       = do tag 2

 581 |            toBuf ns

 583 |   fromBuf

 584 |       = case !getTag of

 585 |              0 => pure IsCovering

 586 |              1 => do ms <- fromBuf

 587 |                      pure (MissingCases ms)

 588 |              2 => do ns <- fromBuf

 589 |                      pure (NonCoveringCall ns)

 590 |              _ => corrupt "Covering"

 593 | TTC Totality where

 594 |   toBuf (MkTotality term cov) = do toBuf term; toBuf cov

 596 |   fromBuf

 597 |       = do term <- fromBuf

 598 |            cov <- fromBuf

 599 |            pure (MkTotality term cov)

 602 | {n : _} -> TTC (PrimFn n) where

 603 |   toBuf (Add ty) = do tag 0; toBuf ty

 604 |   toBuf (Sub ty) = do tag 1; toBuf ty

 605 |   toBuf (Mul ty) = do tag 2; toBuf ty

 606 |   toBuf (Div ty) = do tag 3; toBuf ty

 607 |   toBuf (Mod ty) = do tag 4; toBuf ty

 608 |   toBuf (Neg ty) = do tag 5; toBuf ty

 609 |   toBuf (ShiftL ty) = do tag 35; toBuf ty

 610 |   toBuf (ShiftR ty) = do tag 36; toBuf ty

 611 |   toBuf (BAnd ty) = do tag 37; toBuf ty

 612 |   toBuf (BOr ty) = do tag 38; toBuf ty

 613 |   toBuf (BXOr ty) = do tag 39; toBuf ty

 614 |   toBuf (LT ty) = do tag 6; toBuf ty

 615 |   toBuf (LTE ty) = do tag 7; toBuf ty

 616 |   toBuf (EQ ty) = do tag 8; toBuf ty

 617 |   toBuf (GTE ty) = do tag 9; toBuf ty

 618 |   toBuf (GT ty) = do tag 10; toBuf ty

 619 |   toBuf StrLength = tag 11

 620 |   toBuf StrHead = tag 12

 621 |   toBuf StrTail = tag 13

 622 |   toBuf StrIndex = tag 14

 623 |   toBuf StrCons = tag 15

 624 |   toBuf StrAppend = tag 16

 625 |   toBuf StrReverse = tag 17

 626 |   toBuf StrSubstr = tag 18

 628 |   toBuf DoubleExp = tag 19

 629 |   toBuf DoubleLog = tag 20

 630 |   toBuf DoublePow = tag 21

 631 |   toBuf DoubleSin = tag 22

 632 |   toBuf DoubleCos = tag 23

 633 |   toBuf DoubleTan = tag 24

 634 |   toBuf DoubleASin = tag 25

 635 |   toBuf DoubleACos = tag 26

 636 |   toBuf DoubleATan = tag 27

 637 |   toBuf DoubleSqrt = tag 32

 638 |   toBuf DoubleFloor = tag 33

 639 |   toBuf DoubleCeiling = tag 34

 641 |   toBuf (Cast x y) = do tag 99; toBuf x; toBuf y

 642 |   toBuf BelieveMe = tag 100

 643 |   toBuf Crash = tag 101

 645 |   fromBuf {n}

 646 |       = case n of

 647 |              S Z => fromBuf1

 648 |              S (S Z) => fromBuf2

 649 |              S (S (S Z)) => fromBuf3

 650 |              _ => corrupt "PrimFn"

 651 |     where

 652 |       fromBuf1 : Core (PrimFn 1)

 653 |       fromBuf1

 654 |           = case !getTag of

 655 |                  5 => do ty <- fromBuf; pure (Neg ty)

 656 |                  11 => pure StrLength

 657 |                  12 => pure StrHead

 658 |                  13 => pure StrTail

 659 |                  17 => pure StrReverse

 660 |                  19 => pure DoubleExp

 661 |                  20 => pure DoubleLog

 662 |                  22 => pure DoubleSin

 663 |                  23 => pure DoubleCos

 664 |                  24 => pure DoubleTan

 665 |                  25 => pure DoubleASin

 666 |                  26 => pure DoubleACos

 667 |                  27 => pure DoubleATan

 668 |                  32 => pure DoubleSqrt

 669 |                  33 => pure DoubleFloor

 670 |                  34 => pure DoubleCeiling

 672 |                  99 => do x <- fromBuf; y <- fromBuf; pure (Cast x y)

 673 |                  _ => corrupt "PrimFn 1"

 675 |       fromBuf2 : Core (PrimFn 2)

 676 |       fromBuf2

 677 |           = case !getTag of

 678 |                  0 => do ty <- fromBuf; pure (Add ty)

 679 |                  1 => do ty <- fromBuf; pure (Sub ty)

 680 |                  2 => do ty <- fromBuf; pure (Mul ty)

 681 |                  3 => do ty <- fromBuf; pure (Div ty)

 682 |                  4 => do ty <- fromBuf; pure (Mod ty)

 683 |                  6 => do ty <- fromBuf; pure (LT ty)

 684 |                  7 => do ty <- fromBuf; pure (LTE ty)

 685 |                  8 => do ty <- fromBuf; pure (EQ ty)

 686 |                  9 => do ty <- fromBuf; pure (GTE ty)

 687 |                  10 => do ty <- fromBuf; pure (GT ty)

 688 |                  14 => pure StrIndex

 689 |                  15 => pure StrCons

 690 |                  16 => pure StrAppend

 691 |                  21 => pure DoublePow

 692 |                  35 => do ty <- fromBuf; pure (ShiftL ty)

 693 |                  36 => do ty <- fromBuf; pure (ShiftR ty)

 694 |                  37 => do ty <- fromBuf; pure (BAnd ty)

 695 |                  38 => do ty <- fromBuf; pure (BOr ty)

 696 |                  39 => do ty <- fromBuf; pure (BXOr ty)

 697 |                  101 => pure Crash

 698 |                  _ => corrupt "PrimFn 2"

 700 |       fromBuf3 : Core (PrimFn 3)

 701 |       fromBuf3

 702 |           = case !getTag of

 703 |                  18 => pure StrSubstr

 704 |                  100 => pure BelieveMe

 705 |                  _ => corrupt "PrimFn 3"

 708 | TTC ConInfo where

 709 |   toBuf DATACON = tag 0

 710 |   toBuf TYCON = tag 1

 711 |   toBuf NIL = tag 2

 712 |   toBuf CONS = tag 3

 713 |   toBuf (ENUM n) = do tag 4; toBuf n

 714 |   toBuf NOTHING = tag 5

 715 |   toBuf JUST = tag 6

 716 |   toBuf RECORD = tag 7

 717 |   toBuf ZERO = tag 8

 718 |   toBuf SUCC = tag 9

 719 |   toBuf UNIT = tag 10

 721 |   fromBuf

 722 |       = case !getTag of

 723 |              0 => pure DATACON

 724 |              1 => pure TYCON

 725 |              2 => pure NIL

 726 |              3 => pure CONS

 727 |              4 => do n <- fromBuf; pure (ENUM n)

 728 |              5 => pure NOTHING

 729 |              6 => pure JUST

 730 |              7 => pure RECORD

 731 |              8 => pure ZERO

 732 |              9 => pure SUCC

 733 |              10 => pure UNIT

 734 |              _ => corrupt "ConInfo"

 737 |   export

 738 |   {vars : _} -> TTC (CExp vars) where

 739 |     toBuf (CLocal fc {x} {idx} h) = do tag 0; toBuf fc; toBuf idx

 740 |     toBuf (CRef fc n) = do tag 1; toBuf fc; toBuf n

 741 |     toBuf (CLam fc x sc) = do tag 2; toBuf fc; toBuf x; toBuf sc

 742 |     toBuf (CLet fc x inl val sc) = do tag 3; toBuf fc; toBuf x; toBuf inl; toBuf val; toBuf sc

 743 |     toBuf (CApp fc f as) = assert_total $ do tag 4; toBuf fc; toBuf f; toBuf as

 744 |     toBuf (CCon fc t n ci as) = assert_total $ do tag 5; toBuf fc; toBuf t; toBuf n; toBuf ci; toBuf as

 745 |     toBuf (COp {arity} fc op as) = assert_total $ do tag 6; toBuf fc; toBuf arity; toBuf op; toBuf as

 746 |     toBuf (CExtPrim fc f as) = assert_total $ do tag 7; toBuf fc; toBuf f; toBuf as

 747 |     toBuf (CForce fc lr x) = assert_total $ do tag 8; toBuf fc; toBuf lr; toBuf x

 748 |     toBuf (CDelay fc lr x) = assert_total $ do tag 9; toBuf fc; toBuf lr; toBuf x

 749 |     toBuf (CConCase fc sc alts def) = assert_total $ do tag 10; toBuf fc; toBuf sc; toBuf alts; toBuf def

 750 |     toBuf (CConstCase fc sc alts def) = assert_total $ do tag 11; toBuf fc; toBuf sc; toBuf alts; toBuf def

 751 |     toBuf (CPrimVal fc c) = do tag 12; toBuf fc; toBuf c

 752 |     toBuf (CErased fc) = do tag 13; toBuf fc

 753 |     toBuf (CCrash fc msg) = do tag 14; toBuf fc; toBuf msg

 755 |     fromBuf

 756 |         = assert_total $ case !getTag of

 757 |                0 => do fc <- fromBuf

 758 |                        idx <- fromBuf

 759 |                        let Just x = getAt idx vars

 760 |                            | Nothing => corrupt "CExp"

 761 |                        pure (CLocal {x} fc (mkPrf idx))

 762 |                1 => do fc <- fromBuf

 763 |                        n <- fromBuf

 764 |                        pure (CRef fc n)

 765 |                2 => do fc <- fromBuf

 766 |                        x <- fromBuf; sc <- fromBuf

 767 |                        pure (CLam fc x sc)

 768 |                3 => do fc <- fromBuf

 769 |                        x <- fromBuf; inl <- fromBuf; val <- fromBuf; sc <- fromBuf

 770 |                        pure (CLet fc x inl val sc)

 771 |                4 => do fc <- fromBuf

 772 |                        f <- fromBuf; as <- fromBuf

 773 |                        pure (CApp fc f as)

 774 |                5 => do fc <- fromBuf

 775 |                        t <- fromBuf; n <- fromBuf; ci <- fromBuf; as <- fromBuf

 776 |                        pure (CCon fc t n ci as)

 777 |                6 => do fc <- fromBuf

 778 |                        arity <- fromBuf; op <- fromBuf; args <- fromBuf

 779 |                        pure (COp {arity} fc op args)

 780 |                7 => do fc <- fromBuf

 781 |                        p <- fromBuf; as <- fromBuf

 782 |                        pure (CExtPrim fc p as)

 783 |                8 => do fc <- fromBuf

 784 |                        lr <- fromBuf

 785 |                        x <- fromBuf

 786 |                        pure (CForce fc lr x)

 787 |                9 => do fc <- fromBuf

 788 |                        lr <- fromBuf

 789 |                        x <- fromBuf

 790 |                        pure (CDelay fc lr x)

 791 |                10 => do fc <- fromBuf

 792 |                         sc <- fromBuf; alts <- fromBuf; def <- fromBuf

 793 |                         pure (CConCase fc sc alts def)

 794 |                11 => do fc <- fromBuf

 795 |                         sc <- fromBuf; alts <- fromBuf; def <- fromBuf

 796 |                         pure (CConstCase fc sc alts def)

 797 |                12 => do fc <- fromBuf

 798 |                         c <- fromBuf

 799 |                         pure (CPrimVal fc c)

 800 |                13 => do fc <- fromBuf

 801 |                         pure (CErased fc)

 802 |                14 => do fc <- fromBuf

 803 |                         msg <- fromBuf

 804 |                         pure (CCrash fc msg)

 805 |                _ => corrupt "CExp"

 807 |   export

 808 |   {vars : _} -> TTC (CConAlt vars) where

 809 |     toBuf (MkConAlt n ci t as sc) = do toBuf n; toBuf ci; toBuf t; toBuf as; toBuf sc

 811 |     fromBuf

 812 |         = do n <- fromBuf; ci <- fromBuf; t <- fromBuf

 813 |              as <- fromBuf; sc <- fromBuf

 814 |              pure (MkConAlt n ci t as sc)

 816 |   export

 817 |   {vars : _} -> TTC (CConstAlt vars) where

 818 |     toBuf (MkConstAlt c sc) = do toBuf c; toBuf sc

 820 |     fromBuf

 821 |         = do c <- fromBuf; sc <- fromBuf

 822 |              pure (MkConstAlt c sc)

 825 | TTC CFType where

 826 |   toBuf CFUnit = tag 0

 827 |   toBuf CFInt = tag 1

 828 |   toBuf CFUnsigned8 = tag 2

 829 |   toBuf CFUnsigned16 = tag 3

 830 |   toBuf CFUnsigned32 = tag 4

 831 |   toBuf CFUnsigned64 = tag 5

 832 |   toBuf CFString = tag 6

 833 |   toBuf CFDouble = tag 7

 834 |   toBuf CFChar = tag 8

 835 |   toBuf CFPtr = tag 9

 836 |   toBuf CFWorld = tag 10

 837 |   toBuf (CFFun s t) = do tag 11; toBuf s; toBuf t

 838 |   toBuf (CFIORes t) = do tag 12; toBuf t

 839 |   toBuf (CFStruct n a) = do tag 13; toBuf n; toBuf a

 840 |   toBuf (CFUser n a) = do tag 14; toBuf n; toBuf a

 841 |   toBuf CFGCPtr = tag 15

 842 |   toBuf CFBuffer = tag 16

 843 |   toBuf CFInt8 = tag 17

 844 |   toBuf CFInt16 = tag 18

 845 |   toBuf CFInt32 = tag 19

 846 |   toBuf CFInt64 = tag 20

 847 |   toBuf CFForeignObj = tag 21

 848 |   toBuf CFInteger = tag 22

 850 |   fromBuf

 851 |       = case !getTag of

 852 |              0 => pure CFUnit

 853 |              1 => pure CFInt

 854 |              2 => pure CFUnsigned8

 855 |              3 => pure CFUnsigned16

 856 |              4 => pure CFUnsigned32

 857 |              5 => pure CFUnsigned64

 858 |              6 => pure CFString

 859 |              7 => pure CFDouble

 860 |              8 => pure CFChar

 861 |              9 => pure CFPtr

 862 |              10 => pure CFWorld

 863 |              11 => do s <- fromBuf; t <- fromBuf; pure (CFFun s t)

 864 |              12 => do t <- fromBuf; pure (CFIORes t)

 865 |              13 => do n <- fromBuf; a <- fromBuf; pure (CFStruct n a)

 866 |              14 => do n <- fromBuf; a <- fromBuf; pure (CFUser n a)

 867 |              15 => pure CFGCPtr

 868 |              16 => pure CFBuffer

 869 |              17 => pure CFInt8

 870 |              18 => pure CFInt16

 871 |              19 => pure CFInt32

 872 |              20 => pure CFInt64

 873 |              21 => pure CFForeignObj

 874 |              22 => pure CFInteger

 875 |              _ => corrupt "CFType"

 878 | TTC CDef where

 879 |   toBuf (MkFun args cexpr) = do tag 0; toBuf args; toBuf cexpr

 880 |   toBuf (MkCon t arity pos) = do tag 1; toBuf t; toBuf arity; toBuf pos

 881 |   toBuf (MkForeign cs args ret) = do tag 2; toBuf cs; toBuf args; toBuf ret

 882 |   toBuf (MkError cexpr) = do tag 3; toBuf cexpr

 884 |   fromBuf

 885 |       = case !getTag of

 886 |              0 => do args <- fromBuf; cexpr <- fromBuf

 887 |                      pure (MkFun args cexpr)

 888 |              1 => do t <- fromBuf; arity <- fromBuf; pos <- fromBuf

 889 |                      pure (MkCon t arity pos)

 890 |              2 => do cs <- fromBuf; args <- fromBuf; ret <- fromBuf

 891 |                      pure (MkForeign cs args ret)

 892 |              3 => do cexpr <- fromBuf

 893 |                      pure (MkError cexpr)

 894 |              _ => corrupt "CDef"

 897 | TTC CG where

 898 |   toBuf Chez = tag 0

 899 |   toBuf ChezSep = tag 1

 900 |   toBuf Racket = tag 2

 901 |   toBuf Gambit = tag 3

 902 |   toBuf (Other s) = do tag 4; toBuf s

 903 |   toBuf Node = tag 5

 904 |   toBuf Javascript = tag 6

 905 |   toBuf RefC = tag 7

 906 |   toBuf VMCodeInterp = tag 8

 908 |   fromBuf

 909 |       = case !getTag of

 910 |              0 => pure Chez

 911 |              1 => pure ChezSep

 912 |              2 => pure Racket

 913 |              3 => pure Gambit

 914 |              4 => do s <- fromBuf

 915 |                      pure (Other s)

 916 |              5 => pure Node

 917 |              6 => pure Javascript

 918 |              7 => pure RefC

 919 |              8 => pure VMCodeInterp

 920 |              _ => corrupt "CG"

 923 | TTC PairNames where

 924 |   toBuf l

 925 |       = do toBuf (pairType l)

 926 |            toBuf (fstName l)

 927 |            toBuf (sndName l)

 928 |   fromBuf

 929 |       = do ty <- fromBuf

 930 |            d <- fromBuf

 931 |            f <- fromBuf

 932 |            pure (MkPairNs ty d f)

 935 | TTC RewriteNames where

 936 |   toBuf l

 937 |       = do toBuf (equalType l)

 938 |            toBuf (rewriteName l)

 939 |   fromBuf

 940 |       = do ty <- fromBuf

 941 |            l <- fromBuf

 942 |            pure (MkRewriteNs ty l)

 945 | TTC PrimNames where

 946 |   toBuf l

 947 |       = do toBuf (fromIntegerName l)

 948 |            toBuf (fromStringName l)

 949 |            toBuf (fromCharName l)

 950 |            toBuf (fromDoubleName l)

 951 |            toBuf (fromTTImpName l)

 952 |            toBuf (fromNameName l)

 953 |            toBuf (fromDeclsName l)

 954 |   fromBuf

 955 |       = do i <- fromBuf

 956 |            str <- fromBuf

 957 |            c <- fromBuf

 958 |            d <- fromBuf

 959 |            t <- fromBuf

 960 |            n <- fromBuf

 961 |            dl <- fromBuf

 962 |            pure (MkPrimNs i str c d t n dl)

 965 | TTC HoleInfo where

 966 |   toBuf NotHole = tag 0

 967 |   toBuf (SolvedHole n) = do tag 1; toBuf n

 969 |   fromBuf

 970 |       = case !getTag of

 971 |              0 => pure NotHole

 972 |              1 => do n <- fromBuf; pure (SolvedHole n)

 973 |              _ => corrupt "HoleInfo"

 976 | TTC PMDefInfo where

 977 |   toBuf l

 978 |       = do toBuf (holeInfo l)

 979 |            toBuf (alwaysReduce l)

 980 |            toBuf (externalDecl l)

 981 |   fromBuf

 982 |       = do h <- fromBuf

 983 |            r <- fromBuf

 984 |            e <- fromBuf

 985 |            pure (MkPMDefInfo h r e)

 988 | TTC TypeFlags where

 989 |   toBuf l

 990 |       = do toBuf (uniqueAuto l)

 991 |            toBuf (external l)

 992 |   fromBuf

 993 |       = do u <- fromBuf

 994 |            e <- fromBuf

 995 |            pure (MkTypeFlags u e)

 998 | TTC Def where

 999 |   toBuf None = tag 0

1000 |   toBuf (PMDef pi args ct rt pats)

1001 |       = do tag 1; toBuf pi; toBuf args; toBuf ct; toBuf pats

1002 |   toBuf (ExternDef a)

1003 |       = do tag 2; toBuf a

1004 |   toBuf (ForeignDef a cs)

1005 |       = do tag 3; toBuf a; toBuf cs

1006 |   toBuf (Builtin a)

1007 |       = throw (InternalError "Trying to serialise a Builtin")

1008 |   toBuf (DCon t arity nt) = do tag 4; toBuf t; toBuf arity; toBuf nt

1009 |   toBuf (TCon arity parampos detpos u ms datacons dets)

1010 |       = do tag 5; toBuf arity; toBuf parampos

1011 |            toBuf detpos; toBuf u; toBuf ms; toBuf datacons

1012 |            toBuf dets

1013 |   toBuf (Hole locs p)

1014 |       = do tag 6; toBuf locs; toBuf (implbind p)

1015 |   toBuf (BySearch c depth def)

1016 |       = do tag 7; toBuf c; toBuf depth; toBuf def

1017 |   toBuf (Guess guess envb constraints)

1018 |       = do tag 8; toBuf guess; toBuf envb; toBuf constraints

1019 |   toBuf ImpBind = tag 9

1020 |   toBuf Delayed = tag 10

1021 |   toBuf (UniverseLevel i) = do tag 11; toBuf i

1023 |   fromBuf

1024 |       = case !getTag of

1025 |              0 => pure None

1026 |              1 => do pi <- fromBuf

1027 |                      args <- fromBuf

1028 |                      ct <- fromBuf

1029 |                      pats <- fromBuf

1030 |                      pure (PMDef pi args ct (Unmatched "") pats)

1031 |              2 => do a <- fromBuf

1032 |                      pure (ExternDef a)

1033 |              3 => do a <- fromBuf

1034 |                      cs <- fromBuf

1035 |                      pure (ForeignDef a cs)

1036 |              4 => do t <- fromBuf; a <- fromBuf; nt <- fromBuf

1037 |                      pure (DCon t a nt)

1038 |              5 => do a <- fromBuf

1039 |                      ps <- fromBuf; dets <- fromBuf;

1040 |                      u <- fromBuf

1041 |                      ms <- fromBuf; cs <- fromBuf

1042 |                      detags <- fromBuf

1043 |                      pure (TCon a ps dets u ms cs detags)