Make a start on TTC reading/writing

src/Core/Binary.idr

@@ -0,0 +1,216 @@
+module Core.Binary
+
+import Core.Context
+import Core.Core
+import Core.Hash
+import Core.Normalise
+import Core.TT
+import Core.TTC
+import Core.UnifyState
+
+-- Reading and writing 'Defs' from/to  a binary file
+-- In order to be saved, a name must have been flagged using 'toSave'.
+-- (Otherwise we'd save out everything, not just the things in the current
+-- file).
+
+import public Utils.Binary
+
+import Data.Buffer
+
+%default covering
+
+-- increment this when changing anything in the data format
+-- TTC files can only be compatible if the version number is the same
+export
+ttcVersion : Int
+ttcVersion = 1
+
+export
+checkTTCVersion : Int -> Int -> Core ()
+checkTTCVersion ver exp
+  = if ver < exp
+       then throw (TTCError FormatOlder)
+       else if ver > exp
+            then throw (TTCError FormatNewer)
+            else pure ()
+
+record TTCFile extra where
+  constructor MkTTCFile
+  version : Int
+  ifaceHash : Int
+  importHashes : List (List String, Int)
+  holes : List (Int, (FC, Name))
+  guesses : List (Int, (FC, Name))
+  constraints : Context Constraint
+  context : Defs
+  extraData : extra
+
+-- NOTE: TTC files are only compatible if the version number is the same,
+-- *and* the 'annot/extra' type are the same, or there are no holes/constraints
+TTC extra => TTC (TTCFile extra) where
+  toBuf b file
+      = do toBuf b "TTC"
+           toBuf b (version file)
+           toBuf b (ifaceHash file)
+           toBuf b (importHashes file)
+           toBuf b (holes file)
+           toBuf b (guesses file)
+           toBuf b (constraints file)
+           toBuf b (context file)
+           toBuf b (extraData file)
+
+  fromBuf b
+      = do hdr <- fromBuf b
+           when (hdr /= "TTC") $ corrupt "TTC header"
+           ver <- fromBuf b
+           checkTTCVersion ver ttcVersion
+           ifaceHash <- fromBuf b
+           importHashes <- fromBuf b
+           holes <- fromBuf b
+           guesses <- fromBuf b
+           constraints <- fromBuf b
+           defs <- fromBuf b
+           ex <- fromBuf b
+           pure (MkTTCFile ver ifaceHash importHashes 
+                           holes guesses constraints defs ex)
+
+{-
+-- Update the various fields in Defs affected by the name's flags
+processFlags : Name -> List DefFlag -> Defs -> Defs
+processFlags n [] defs = defs
+processFlags n (GlobalHint t :: fs) defs
+  = processFlags n fs (record { autoHints $= ((t, n) ::) } defs)
+processFlags n (TypeHint ty d :: fs) defs
+  = processFlags n fs (addToTypeHints ty n d defs)
+processFlags n (Inline :: fs) defs = processFlags n fs defs
+processFlags n (TCInline :: fs) defs = processFlags n fs defs
+processFlags n (Invertible :: fs) defs = processFlags n fs defs
+processFlags n (Overloadable :: fs) defs = processFlags n fs defs
+processFlags n (SetTotal t :: fs) defs = processFlags n fs defs
+
+-- For every name (from 'toSave' in defs), add its definition and any
+-- information from its flags to the new set of Defs that we'll write out
+-- as Binary.
+mkSaveDefs : List Name -> Defs -> Defs -> Defs
+mkSaveDefs [] acc _ = acc
+mkSaveDefs (n :: ns) acc defs
+    = case lookupGlobalExact n (gamma defs) of
+           Nothing => mkSaveDefs ns acc defs -- 'n' really should exist though!
+           Just gdef =>
+                let gdef' = record { type $= normaliseHoles defs [] } gdef
+                    gam' = addCtxt n gdef' (gamma acc) 
+                    defs' = processFlags n (flags gdef) defs in
+                    mkSaveDefs ns (record { gamma = gam' } acc) defs'
+
+-- Write out the things in the context which have been defined in the
+-- current source file
+export
+writeToTTC : (TTC annot annot, TTC annot extra) =>
+             {auto c : Ref Ctxt Defs} ->
+             {auto u : Ref UST (UState annot)} ->
+             extra ->
+             (fname : String) ->
+             Core annot ()
+writeToTTC extradata fname
+    = do buf <- initBinary
+         defs <- get Ctxt
+         ust <- get UST
+         let defs' = mkSaveDefs (getSave defs) 
+                         (record { options = options defs,
+                                   imported = imported defs,
+                                   currentNS = currentNS defs,
+                                   hiddenNames = hiddenNames defs,
+                                   cgdirectives = cgdirectives defs
+                                 } initCtxt)
+                         defs
+         log 5 $ "Writing " ++ fname ++ " with hash " ++ show (ifaceHash defs)
+         toBuf buf (MkTTCFile ttcVersion (ifaceHash defs) (importHashes defs)
+                              (holes ust) (constraints ust) defs'
+                              extradata)
+         Right ok <- coreLift $ writeToFile fname !(get Bin)
+               | Left err => throw (InternalError (fname ++ ": " ++ show err))
+         pure ()
+
+-- Add definitions from a binary file to the current context
+-- Returns the "extra" section of the file (user defined data), the interface
+-- has and the list of additional TTCs that need importing
+-- (we need to return these, rather than do it here, because after loading
+-- the data that's when we process the extra data...)
+export
+readFromTTC : (TTC annot annot, TTC annot extra) =>
+              {auto c : Ref Ctxt Defs} ->
+              {auto u : Ref UST (UState annot)} ->
+              annot ->
+              Bool ->
+              (fname : String) -> -- file containing the module
+              (modNS : List String) -> -- module namespace
+              (importAs : List String) -> -- namespace to import as
+              Core annot (Maybe (extra, Int, List (List String, Bool, List String)))
+readFromTTC loc reexp fname modNS importAs
+    = do defs <- get Ctxt
+         -- If it's already in the context, don't load it again
+         let False = (fname, importAs) `elem` allImported defs
+              | True => pure Nothing
+         put Ctxt (record { allImported $= ((fname, importAs) :: ) } defs)
+
+         Right buf <- coreLift $ readFromFile fname
+               | Left err => throw (InternalError (fname ++ ": " ++ show err))
+         bin <- newRef Bin buf -- for reading the file into
+         sh <- initShare -- for recording string sharing
+         ttc <- fromBuf sh bin
+         -- Rename everything in the ttc's context according to the namespace
+         -- it was imported as
+         -- [TODO]
+         let renamed = context ttc
+
+         -- Extend the current context with the updated definitions from the ttc
+         extendAs loc reexp modNS importAs renamed
+         setNS (currentNS (context ttc))
+
+         -- Finally, update the unification state with the holes from the
+         -- ttc
+         ust <- get UST
+         put UST (record { holes = holes ttc,
+                           constraints = constraints ttc } ust)
+         pure (Just (extraData ttc, ifaceHash ttc, imported (context ttc)))
+        -} 
+
+getImportHashes : Ref Bin Binary ->
+                  Core (List (List String, Int))
+getImportHashes b
+    = do hdr <- fromBuf {a = String} b
+         when (hdr /= "TTC") $ corrupt "TTC header"
+         ver <- fromBuf {a = Int} b
+         checkTTCVersion ver ttcVersion
+         ifaceHash <- fromBuf {a = Int} b
+         fromBuf b
+
+getHash : Ref Bin Binary -> Core Int
+getHash b
+    = do hdr <- fromBuf {a = String} b
+         when (hdr /= "TTC") $ corrupt "TTC header"
+         ver <- fromBuf {a = Int} b
+         checkTTCVersion ver ttcVersion
+         fromBuf b
+
+export
+readIFaceHash : (fname : String) -> -- file containing the module
+                Core Int
+readIFaceHash fname
+    = do Right buf <- coreLift $ readFromFile fname
+            | Left err => pure 0
+         b <- newRef Bin buf
+         
+         catch (getHash b)
+               (\err => pure 0)
+
+export
+readImportHashes : (fname : String) -> -- file containing the module
+                   Core (List (List String, Int))
+readImportHashes fname
+    = do Right buf <- coreLift $ readFromFile fname
+            | Left err => pure []
+         b <- newRef Bin buf
+         catch (getImportHashes b)
+               (\err => pure [])
+

src/Core/Context.idr

@@ -2,7 +2,9 @@ module Core.Context
 
 import public Core.Core
 import public Core.Name
+import Core.Options
 import public Core.TT
+import Utils.Binary
 
 import Data.IOArray
 import Data.NameMap
@@ -30,6 +32,11 @@ record Context a where
     -- visible
     visibleNS : List (List String)
 
+export
+TTC a => TTC (Context a) where
+  toBuf = ?tocontext
+  fromBuf = ?fromcontext
+
 initSize : Int
 initSize = 10000
 
@@ -206,7 +213,10 @@ record Defs where
   constructor MkDefs
   gamma : Context GlobalDef
   currentNS : List String -- namespace for current definitions
+  options : Options
+--   toSave : SortedSet
   nextTag : Int
+  ifaceHash : Int
 
 export
 clearDefs : Defs -> Core Defs
@@ -218,8 +228,13 @@ export
 initDefs : Core Defs
 initDefs 
     = do gam <- initCtxt
-         pure (MkDefs gam ["Main"] 100)
+         pure (MkDefs gam ["Main"] defaults 100 5381)
       
+export
+TTC Defs where
+  toBuf = ?todefs
+  fromBuf = ?fromdefs
+
 -- Label for context references
 export
 data Ctxt : Type where

src/Core/Hash.idr

@@ -0,0 +1,92 @@
+module Core.Hash
+
+import Core.TT
+import Data.List
+
+%default total
+
+-- This is so that we can store a hash of the interface in ttc files, to avoid
+-- the need for reloading modules when no interfaces have changed in imports.
+-- As you can probably tell, I know almost nothing about writing good hash
+-- functions, so better implementations will be very welcome...
+
+public export
+interface Hashable a where
+  hash : a -> Int
+  hashWithSalt : Int -> a -> Int
+  
+  hash = hashWithSalt 5381
+  hashWithSalt h i = h * 33 + hash i
+
+export
+Hashable Int where
+  hash = id
+
+export
+Hashable Char where
+  hash = cast
+
+export
+Hashable a => Hashable (List a) where
+  hashWithSalt h [] = abs h
+  hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs
+
+export
+Hashable String where
+  hashWithSalt h str = hashChars h 0 (cast (length str)) str
+    where
+      hashChars : Int -> Int -> Int -> String -> Int
+      hashChars h p len str
+          = assert_total $
+              if p == len 
+                 then h
+                 else hashChars (h * 33 + cast (strIndex str p)) 
+                                (p + 1) len str
+
+export
+Hashable Name where
+  hashWithSalt h (MN s _) = hashWithSalt h s
+  hashWithSalt h n = hashWithSalt h (show n)
+
+count : RigCount -> String
+count Rig0 = "0"
+count Rig1 = "1"
+count RigW = "w"
+
+plicity : PiInfo -> String
+plicity Implicit = "{}"
+plicity Explicit = "()"
+plicity AutoImplicit = "{a}"
+
+-- I suppose this'll do for now... TODO: Write a proper one!
+-- Converting to a string (and indeed, however we do the hash function...)
+-- we need to ignore machine generated names because they'll have different
+-- numbers depending on implementations of functions, and that doesn't affect
+-- the exported interface.
+hshow : Term vars -> String
+-- hshow (Local {x} _ _) = nameRoot x
+-- hshow (Ref _ n) = nameRoot n
+-- hshow (Bind x (Lam c p ty) sc) 
+--    = "\\" ++ nameRoot x ++ count c ++ plicity p ++ hshow ty ++ "." ++ hshow sc
+-- hshow (Bind x (Let c val ty) sc) 
+--    = "let " ++ nameRoot x ++ count c ++ " " ++ hshow val ++ " " ++ hshow ty ++ "."
+--             ++ hshow sc
+-- hshow (Bind x (Pi c p ty) sc) 
+--    = "pi." ++ nameRoot x ++ count c ++ plicity p ++ hshow ty ++ "." ++ hshow sc
+-- hshow (Bind x (PVar c ty) sc)
+--    = "pvar." ++ nameRoot x ++ count c ++ hshow ty ++ "." ++ hshow sc
+-- hshow (Bind x (PLet c val ty) sc)
+--    = "plet " ++ nameRoot x ++ count c ++ " " ++ hshow val ++ " " ++ hshow ty ++ "."
+--              ++ hshow sc
+-- hshow (Bind x (PVTy c ty) sc)
+--    = "pty." ++ nameRoot x ++ count c ++ hshow ty ++ "." ++ hshow sc
+-- hshow (App f a) = "(" ++ hshow f ++ " " ++ hshow a ++ ")"
+-- hshow (PrimVal x) = show x
+-- hshow TType = "#"
+-- hshow Erased = "_"
+
+export
+Hashable (Term vars) where
+  hashWithSalt h tm 
+     = hashWithSalt h (hshow tm)
+

src/Core/Options.idr

@@ -0,0 +1,92 @@
+module Core.Options
+
+import Core.Core
+import Core.Name
+import Core.TTC
+import Utils.Binary
+
+public export
+record Dirs where
+  constructor MkDirs
+  working_dir : String
+  build_dir : String -- build directory, relative to working directory
+  dir_prefix : String -- installation prefix, for finding data files (e.g. run time support)
+  extra_dirs : List String -- places to look for import files
+  data_dirs : List String -- places to look for data file
+
+public export
+toString : Dirs -> String
+toString (MkDirs wdir bdir dfix edirs ddirs) =
+  unlines [ "+ Working Directory   :: " ++ show wdir
+          , "+ Build Directory     :: " ++ show bdir
+          , "+ Installation Prefix :: " ++ show dfix
+          , "+ Extra Directories :: " ++ show edirs
+          , "+ Data Directories :: " ++ show ddirs]
+
+public export
+data CG = Chez
+        | Chicken
+        | Racket
+
+export
+Eq CG where
+  Chez == Chez = True
+  Chicken == Chicken = True
+  Racket == Racket = True
+  _ == _ = False
+
+export
+TTC CG where
+  toBuf b Chez = tag 0
+  toBuf b Chicken = tag 1
+  toBuf b Racket = tag 2
+
+  fromBuf b
+      = case !getTag of
+             0 => pure Chez
+             1 => pure Chicken
+             2 => pure Racket
+             _ => corrupt "CG"
+
+export
+availableCGs : List (String, CG)
+availableCGs = [("chez", Chez), ("chicken", Chicken), ("racket", Racket)]
+
+export
+getCG : String -> Maybe CG
+getCG cg = lookup (toLower cg) availableCGs
+
+-- Other options relevant to the current session (so not to be saved in a TTC)
+public export
+record Session where
+  constructor MkSessionOpts
+  noprelude : Bool
+  codegen : CG
+
+public export
+record PPrinter where
+  constructor MkPPOpts
+  showImplicits : Bool
+  showFullEnv : Bool
+  fullNamespace : Bool
+
+public export
+record Options where
+  constructor MkOptions
+  dirs : Dirs
+  printing : PPrinter
+  session : Session
+
+defaultDirs : Dirs
+defaultDirs = MkDirs "." "build" "/usr/local" ["."] []
+
+defaultPPrint : PPrinter
+defaultPPrint = MkPPOpts False True False
+
+defaultSession : Session
+defaultSession = MkSessionOpts False Chez
+
+export
+defaults : Options
+defaults = MkOptions defaultDirs defaultPPrint defaultSession
+

src/Core/TTC.idr

@@ -0,0 +1,18 @@
+module Core.TTC
+
+import Core.Core
+import Core.FC
+import Core.TT
+
+import Utils.Binary
+
+export
+TTC FC where
+  toBuf = ?tofc
+  fromBuf = ?fromfc
+
+export
+TTC Name where
+  toBuf = ?toName
+  fromBuf = ?fromName
+

src/Core/UnifyState.idr

@@ -5,6 +5,8 @@ import Core.Core
 import Core.Env
 import Core.FC
 import Core.TT
+import Core.TTC
+import Utils.Binary
 
 import Data.IntMap
 
@@ -29,6 +31,11 @@ data Constraint : Type where
      -- A resolved constraint
      Resolved : Constraint
 
+export
+TTC Constraint where
+  toBuf = ?toconstraint
+  fromBuf = ?fromconstraint
+
 public export
 record UState where
   constructor MkUState

src/Utils/Binary.idr

@@ -0,0 +1,431 @@
+module Utils.Binary
+
+import Core.Core
+import Data.Buffer
+import Data.List
+import Data.Vect
+
+-- Serialising data as binary. Provides an interface TTC which allows
+-- reading and writing to chunks of memory, "Binary", which can be written
+-- to and read from files.
+
+%default covering
+
+-- A label for binary states
+export 
+data Bin : Type where
+
+-- A label for storing shared strings
+export
+data Share : Type where
+
+-- A component of the serialised data.
+record Chunk where
+  constructor MkChunk
+  buf : Buffer
+  loc : Int
+  size : Int -- Capacity
+  used : Int -- Amount used
+
+newChunk : Buffer -> Chunk
+newChunk b = MkChunk b 0 (size b) 0
+
+avail : Chunk -> Int
+avail c = size c - loc c
+
+toRead : Chunk -> Int
+toRead c = used c - loc c
+
+appended : Int -> Chunk -> Chunk
+appended i c = record { loc $= (+i),
+                        used $= (+i) } c
+
+incLoc : Int -> Chunk -> Chunk
+incLoc i c = record { loc $= (+i) } c
+
+-- Serialised data is stored as a list of chunks, in a zipper.
+-- i.e. processed chunks, chunk we're working on, chunks to do
+export
+data Binary = MkBin (List Chunk) Chunk (List Chunk)
+
+dumpBin : Binary -> IO ()
+dumpBin (MkBin done chunk rest)
+   = do printLn !(traverse bufferData (map buf done))
+        printLn !(bufferData (buf chunk))
+        printLn !(traverse bufferData (map buf rest))
+
+nonEmptyRev : NonEmpty (xs ++ y :: ys)
+nonEmptyRev {xs = []} = IsNonEmpty
+nonEmptyRev {xs = (x :: xs)} = IsNonEmpty
+
+reset : Binary -> Binary
+reset (MkBin done cur rest) 
+    = setBin (reverse done ++ cur :: rest) nonEmptyRev
+  where
+    setBin : (xs : List Chunk) -> (prf : NonEmpty xs) -> Binary
+    setBin (chunk :: rest) IsNonEmpty 
+        = MkBin [] (record { loc = 0 } chunk)
+                   (map (record { loc = 0 }) rest)
+
+req : List Chunk -> Int
+req [] = 0
+req (c :: cs)
+    = used c + req cs
+
+-- Take all the data from the chunks in a 'Binary' and copy them into one
+-- single buffer, ready for writing to disk.
+-- TODO: YAGNI? Delete if so...
+toBuffer : Binary -> IO (Maybe Buffer)
+toBuffer (MkBin done cur rest)
+    = do let chunks = reverse done ++ cur :: rest
+         Just b <- newBuffer (req chunks)
+              | Nothing => pure Nothing
+         copyToBuf 0 b chunks
+         pure (Just b)
+  where
+    copyToBuf : (pos : Int) -> Buffer -> List Chunk -> IO ()
+    copyToBuf pos b [] = pure ()
+    copyToBuf pos b (c :: cs)
+        = do copyData (buf c) 0 (used c) b pos
+             copyToBuf (pos + used c) b cs
+
+fromBuffer : Buffer -> IO Binary
+fromBuffer buf
+    = do len <- rawSize buf
+         pure (MkBin [] (MkChunk buf 0 len len) []) -- assume all used
+
+export
+writeToFile : (fname : String) -> Binary -> IO (Either FileError ())
+writeToFile fname (MkBin done cur rest)
+    = do Right h <- openFile fname WriteTruncate
+               | Left err => pure (Left err)
+         let chunks = reverse done ++ cur :: rest
+         writeChunks h chunks
+         closeFile h
+         pure (Right ())
+  where
+    writeChunks : File -> List Chunk -> IO ()
+    writeChunks h [] = pure ()
+    writeChunks h (c :: cs)
+        = do writeBufferToFile h (resetBuffer (buf c)) (used c)
+             writeChunks h cs
+
+export
+readFromFile : (fname : String) -> IO (Either FileError Binary)
+readFromFile fname
+    = do Right h <- openFile fname Read
+               | Left err => pure (Left err)
+         Right max <- fileSize h
+               | Left err => pure (Left err)
+         Just b <- newBuffer max
+               | Nothing => pure (Left (GenericFileError 0)) --- um, not really
+         b <- readBufferFromFile h b max
+         pure (Right (MkBin [] (MkChunk b 0 max max) []))
+
+public export
+interface TTC a where -- TTC = TT intermediate code/interface file
+  -- Add binary data representing the value to the given buffer
+  toBuf : Ref Bin Binary -> a -> Core ()
+  -- Return the data representing a thing of type 'a' from the given buffer.
+  -- Throws if the data can't be parsed as an 'a'
+  fromBuf : Ref Bin Binary -> Core a
+
+-- Create a new list of chunks, initialised with one 64k chunk
+export
+initBinary : Core (Ref Bin Binary)
+initBinary
+    = do Just buf <- coreLift $ newBuffer 65536
+             | Nothing => throw (InternalError "Buffer creation failed")
+         newRef Bin (MkBin [] (newChunk buf) [])
+
+export
+corrupt : String -> Core a
+corrupt ty = throw (TTCError (Corrupt ty))
+
+-- Primitives; these are the only things that have to deal with growing
+-- the buffer list
+
+export
+TTC Bits8 where
+  toBuf b val 
+    = do MkBin done chunk rest <- get Bin
+         if avail chunk >= 1
+            then
+              do coreLift $ setByte (buf chunk) (loc chunk) val
+                 put Bin (MkBin done (appended 1 chunk) rest)
+            else 
+              do Just newbuf <- coreLift $ newBuffer 65536
+                    | Nothing => throw (InternalError "Buffer expansion failed")
+                 coreLift $ setByte newbuf 0 val
+                 put Bin (MkBin (chunk :: done)
+                                (MkChunk newbuf 1 (size newbuf) 1)
+                                rest)
+
+  fromBuf b
+    = do MkBin done chunk rest <- get Bin
+         if toRead chunk >= 1
+            then
+              do val <- coreLift $ getByte (buf chunk) (loc chunk)
+                 put Bin (MkBin done (incLoc 1 chunk) rest)
+                 pure val
+              else
+                case rest of
+                     [] => throw (TTCError (EndOfBuffer "Byte"))
+                     (next :: rest) =>
+                        do val <- coreLift $ getByte (buf next) 0
+                           put Bin (MkBin (chunk :: done) (incLoc 1 next) rest)
+                           pure val
+
+export
+tag : {auto b : Ref Bin Binary} -> Bits8 -> Core ()
+tag {b} val = toBuf b val
+
+export
+getTag : {auto b : Ref Bin Binary} -> Core Bits8
+getTag {b} = fromBuf b
+
+-- Some useful types from the prelude
+
+export
+TTC Int where
+  toBuf b val
+    = do MkBin done chunk rest <- get Bin
+         if avail chunk >= 4
+            then 
+              do coreLift $ setInt (buf chunk) (loc chunk) val
+                 put Bin (MkBin done (appended 4 chunk) rest)
+            else 
+              do Just newbuf <- coreLift $ newBuffer 65536
+                    | Nothing => throw (InternalError "Buffer expansion failed")
+                 coreLift $ setInt newbuf 0 val
+                 put Bin (MkBin (chunk :: done)
+                                (MkChunk newbuf 4 (size newbuf) 4)
+                                rest)
+  fromBuf b 
+    = do MkBin done chunk rest <- get Bin
+         if toRead chunk >= 4
+            then
+              do val <- coreLift $ getInt (buf chunk) (loc chunk)
+                 put Bin (MkBin done (incLoc 4 chunk) rest)
+                 pure val
+              else
+                case rest of
+                     [] => throw (TTCError (EndOfBuffer "Int"))
+                     (next :: rest) =>
+                        do val <- coreLift $ getInt (buf next) 0
+                           put Bin (MkBin (chunk :: done) (incLoc 4 next) rest)
+                           pure val
+
+export
+TTC String where
+  toBuf b val
+      = do let req : Int = cast (length val)
+           toBuf b req
+           MkBin done chunk rest <- get Bin
+           if avail chunk >= req
+              then
+                do coreLift $ setString (buf chunk) (loc chunk) val
+                   put Bin (MkBin done (appended req chunk) rest)
+              else 
+                do Just newbuf <- coreLift $ newBuffer 65536
+                      | Nothing => throw (InternalError "Buffer expansion failed")
+                   coreLift $ setString newbuf 0 val
+                   put Bin (MkBin (chunk :: done)
+                                  (MkChunk newbuf req (size newbuf) req)
+                                  rest)
+
+  fromBuf b 
+      = do len <- fromBuf {a = Int} b
+           MkBin done chunk rest <- get Bin
+           if toRead chunk >= len
+              then
+                do val <- coreLift $ getString (buf chunk) (loc chunk) len
+                   put Bin (MkBin done (incLoc len chunk) rest)
+                   pure val
+              else 
+                case rest of
+                     [] => throw (TTCError (EndOfBuffer "String"))
+                     (next :: rest) =>
+                        do val <- coreLift $ getString (buf next) 0 len
+                           put Bin (MkBin (chunk :: done)
+                                          (incLoc len next) rest)
+                           pure val
+
+export
+TTC Bool where
+  toBuf b False = tag 0
+  toBuf b True = tag 1
+  fromBuf b
+      = case !getTag of
+             0 => pure False
+             1 => pure True
+             _ => corrupt "Bool"
+
+export
+TTC Char where
+  toBuf b c = toBuf b (cast {to=Int} c)
+  fromBuf b
+      = do i <- fromBuf b
+           pure (cast {from=Int} i)
+
+export
+TTC Double where
+  toBuf b val
+    = do MkBin done chunk rest <- get Bin
+         if avail chunk >= 8
+            then 
+              do coreLift $ setDouble (buf chunk) (loc chunk) val
+                 put Bin (MkBin done (appended 8 chunk) rest)
+            else 
+              do Just newbuf <- coreLift $ newBuffer 65536
+                    | Nothing => throw (InternalError "Buffer expansion failed")
+                 coreLift $ setDouble newbuf 0 val
+                 put Bin (MkBin (chunk :: done)
+                                (MkChunk newbuf 8 (size newbuf) 8)
+                                rest)
+  fromBuf b 
+    = do MkBin done chunk rest <- get Bin
+         if toRead chunk >= 8
+            then
+              do val <- coreLift $ getDouble (buf chunk) (loc chunk)
+                 put Bin (MkBin done (incLoc 8 chunk) rest)
+                 pure val
+              else
+                case rest of
+                     [] => throw (TTCError (EndOfBuffer "Double"))
+                     (next :: rest) =>
+                        do val <- coreLift $ getDouble (buf next) 0
+                           put Bin (MkBin (chunk :: done) (incLoc 8 next) rest)
+                           pure val
+
+export
+(TTC a, TTC b) => TTC (a, b) where
+  toBuf b (x, y)
+     = do toBuf b x
+          toBuf b y
+  fromBuf b
+     = do x <- fromBuf b
+          y <- fromBuf b
+          pure (x, y)
+
+export
+TTC () where
+  toBuf b () = pure ()
+  fromBuf b = pure ()
+
+export
+(TTC a, {y : a} -> TTC (p y)) => TTC (DPair a p) where
+  toBuf b (vs ** tm)
+      = do toBuf b vs
+           toBuf b tm
+
+  fromBuf b
+      = do x <- fromBuf b
+           p <- fromBuf b
+           pure (x ** p)
+
+export
+TTC a => TTC (Maybe a) where
+  toBuf b Nothing
+     = tag 0
+  toBuf b (Just val)
+     = do tag 1
+          toBuf b val
+
+  fromBuf b
+     = case !getTag of
+            0 => pure Nothing
+            1 => do val <- fromBuf b
+                    pure (Just val)
+            _ => corrupt "Maybe"
+
+export
+(TTC a, TTC b) => TTC (Either a b) where
+  toBuf b (Left val)
+     = do tag 0
+          toBuf b val
+  toBuf b (Right val)
+     = do tag 1
+          toBuf b val
+
+  fromBuf b
+     = case !getTag of
+            0 => do val <- fromBuf b
+                    pure (Left val)
+            1 => do val <- fromBuf b
+                    pure (Right val)
+            _ => corrupt "Either"
+
+export
+TTC a => TTC (List a) where
+  toBuf b xs
+      = do toBuf b (cast {to=Int} (length xs))
+           traverse (toBuf b) xs
+           pure ()
+  fromBuf b 
+      = do len <- fromBuf b {a = Int}
+           readElems [] (cast len)
+    where
+      readElems : List a -> Nat -> Core (List a)
+      readElems xs Z = pure (reverse xs)
+      readElems xs (S k)
+          = do val <- fromBuf b
+               readElems (val :: xs) k
+
+export
+TTC a => TTC (Vect n a) where
+  toBuf b xs = writeAll xs
+    where
+      writeAll : Vect n a -> Core ()
+      writeAll [] = pure ()
+      writeAll (x :: xs) = do toBuf b x; writeAll xs
+
+  fromBuf {n} b = rewrite sym (plusZeroRightNeutral n) in readElems [] n
+    where
+      readElems : Vect done a -> (todo : Nat) -> Core (Vect (todo + done) a)
+      readElems {done} xs Z 
+          = pure (reverse xs)
+      readElems {done} xs (S k)
+          = do val <- fromBuf b
+               rewrite (plusSuccRightSucc k done)
+               readElems (val :: xs) k
+
+count : List.Elem x xs -> Int
+count Here = 0
+count (There p) = 1 + count p
+
+toLimbs : Integer -> List Int
+toLimbs x
+    = if x == 0 
+         then []
+         else if x == -1 then [-1]
+              else fromInteger (prim__andBigInt x 0xff) ::
+                    toLimbs (prim__ashrBigInt x 8)
+
+fromLimbs : List Int -> Integer
+fromLimbs [] = 0
+fromLimbs (x :: xs) = cast x + prim__shlBigInt (fromLimbs xs) 8
+
+export
+TTC Integer where
+  toBuf b val
+    = assert_total $ if val < 0
+         then do toBuf b (the Bits8 0)
+                 toBuf b (toLimbs (-val))
+         else do toBuf b (the Bits8 1)
+                 toBuf b (toLimbs val)
+  fromBuf b 
+    = do val <- fromBuf b {a = Bits8}
+         case val of
+              0 => do val <- fromBuf b
+                      pure (-(fromLimbs val))
+              1 => do val <- fromBuf b
+                      pure (fromLimbs val)
+              _ => corrupt "Integer"
+
+export
+TTC Nat where
+  toBuf b val = toBuf b (cast {to=Integer} val)
+  fromBuf b 
+     = do val <- fromBuf b
+          pure (fromInteger val)

yaffle.ipkg

@@ -3,13 +3,17 @@ package yaffle
 modules = 
     Control.Delayed,
 
+    Core.Binary,
     Core.Context,
     Core.Core,
     Core.Env,
-    Core.Normalise,
     Core.FC,
+    Core.Hash,
     Core.Name,
+    Core.Normalise,
+    Core.Options,
     Core.TT,
+    Core.TTC,
     Core.Unify,
     Core.UnifyState,
     Core.Value,
@@ -40,7 +44,9 @@ modules =
     TTImp.ProcessDecls,
     TTImp.ProcessDef,
     TTImp.ProcessType,
-    TTImp.TTImp
+    TTImp.TTImp,
+
+    Utils.Binary
 
 sourcedir = src
 executable = yaffle