Fill in holes for reading/writing TTC

Tricky bit is the 'NameRefs'. When we load a file back in, we load a
mapping from resolved ids in the file to their full names, and
immediately resolve them in the current context so that we have the
correct ids after loading.

src/Core/Binary.idr

@@ -8,6 +8,8 @@ import Core.TT
 import Core.TTC
 import Core.UnifyState
 
+import Data.IntMap
+
 -- 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
@@ -39,113 +41,153 @@ record TTCFile extra where
   version : Int
   ifaceHash : Int
   importHashes : List (List String, Int)
+  nameMap : NameRefs -- All the names referenced in the file
+                     -- This is a mapping from the index used in the file
+                     -- to the actual name
   holes : List (Int, (FC, Name))
   guesses : List (Int, (FC, Name))
-  constraints : Context Constraint
+  constraints : List (Int, Constraint)
-  context : Defs
+  context : List GlobalDef
+  imported : List (List String, Bool, List String)
+  currentNS : List String
   extraData : extra
 
+asName : List String -> Maybe (List String) -> Name -> Name
+asName mod (Just ns) (NS oldns n) 
+    = if mod == oldns 
+         then NS ns n -- TODO: What about if there are nested namespaces in a module?
+         else NS oldns n
+asName _ _ n = n
+
+readNameMap : NameRefs -> Ref Bin Binary -> Core NameRefs
+readNameMap r b
+    = do ns <- fromBuf r b
+         coreLift $ fromList ns
+
+-- For every name we're going to read from the file, work out what it's
+-- new resolved name is going to be in the context and update the name
+-- map accordingly
+-- Also update namespace if we've done "import ... as ..."
+updateEntries : {auto c : Ref Ctxt Defs} ->
+                Context GlobalDef ->
+                List String -> Maybe (List String) ->
+                Int -> Int -> NameRefs -> Core (Context GlobalDef)
+updateEntries ctxt mod as pos end r
+    = if pos >= end
+         then pure ctxt
+         else do Just (n, Nothing) <- coreLift $ readArray r pos
+                      | _ => updateEntries ctxt mod as (pos+1) end r
+                 let n' = asName mod as n
+                 (idx, ctxt') <- getPosition n' ctxt
+                 coreLift $ writeArray r pos (n', Just idx)
+                 updateEntries ctxt' mod as (pos+1) end r
+
+writeNameMap : Ref Bin Binary -> NameRefs -> Core ()
+writeNameMap b r
+    = do ns <- coreLift $ toList r
+         toBuf b ns
+
 -- 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
+writeTTCFile : TTC extra => Ref Bin Binary -> TTCFile extra -> Core ()
-  toBuf b file
+writeTTCFile b file
       = do toBuf b "TTC"
            toBuf b (version file)
            toBuf b (ifaceHash file)
            toBuf b (importHashes file)
+           writeNameMap b (nameMap file)
            toBuf b (holes file)
            toBuf b (guesses file)
            toBuf b (constraints file)
            toBuf b (context file)
+           toBuf b (imported file)
+           toBuf b (currentNS file)
            toBuf b (extraData file)
 
-  fromBuf b
+readTTCFile : TTC extra => 
-      = do hdr <- fromBuf b
+              {auto c : Ref Ctxt Defs} ->
+              List String -> Maybe (List String) ->
+              NameRefs -> Ref Bin Binary -> Core (TTCFile extra)
+readTTCFile modns as r b
+      = do hdr <- fromBuf r b
            when (hdr /= "TTC") $ corrupt "TTC header"
-           ver <- fromBuf b
+           ver <- fromBuf r b
            checkTTCVersion ver ttcVersion
-           ifaceHash <- fromBuf b
+           ifaceHash <- fromBuf r b
-           importHashes <- fromBuf b
+           importHashes <- fromBuf r b
-           holes <- fromBuf b
+           -- Read in name map, update 'r'
-           guesses <- fromBuf b
+           r <- readNameMap r b
-           constraints <- fromBuf b
+           defs <- get Ctxt
-           defs <- fromBuf b
+           gam' <- updateEntries (gamma defs) modns as 0 (max r) r
-           ex <- fromBuf b
+           setCtxt gam' 
-           pure (MkTTCFile ver ifaceHash importHashes 
+           holes <- fromBuf r b
-                           holes guesses constraints defs ex)
+           guesses <- fromBuf r b
+           constraints <- fromBuf r b
+           defs <- fromBuf r b
+           imp <- fromBuf r b
+           cns <- fromBuf r b
+           ex <- fromBuf r b
+           pure (MkTTCFile ver ifaceHash importHashes r
+                           holes guesses constraints defs imp cns ex)
 
-{-
+-- Pull out the list of GlobalDefs that we want to save
--- Update the various fields in Defs affected by the name's flags
+getSaveDefs : List Name -> List GlobalDef -> Defs -> Core (List GlobalDef)
-processFlags : Name -> List DefFlag -> Defs -> Defs
+getSaveDefs [] acc _ = pure acc
-processFlags n [] defs = defs
+getSaveDefs (n :: ns) acc defs
-processFlags n (GlobalHint t :: fs) defs
+    = do Just gdef <- lookupCtxtExact n (gamma defs)
-  = processFlags n fs (record { autoHints $= ((t, n) ::) } defs)
+              | Nothing => getSaveDefs ns acc defs -- 'n' really should exist though!
-processFlags n (TypeHint ty d :: fs) defs
+         getSaveDefs ns (gdef :: acc) 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) =>
+writeToTTC : TTC extra =>
              {auto c : Ref Ctxt Defs} ->
-             {auto u : Ref UST (UState annot)} ->
+             {auto u : Ref UST UState} ->
-             extra ->
+             extra -> (fname : String) -> Core ()
-             (fname : String) ->
-             Core annot ()
 writeToTTC extradata fname
     = do buf <- initBinary
          defs <- get Ctxt
          ust <- get UST
-         let defs' = mkSaveDefs (getSave defs) 
+         gdefs <- getSaveDefs (getSave defs) [] 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)
+         r <- getNameRefs (gamma defs)
-                              (holes ust) (constraints ust) defs'
+         writeTTCFile buf 
+                   (MkTTCFile ttcVersion (ifaceHash defs) (importHashes defs)
+                              r
+                              (toList (holes ust)) 
+                              (toList (guesses ust)) 
+                              (toList (constraints ust))
+                              gdefs
+                              (imported defs)
+                              (currentNS defs)
                               extradata)
          Right ok <- coreLift $ writeToFile fname !(get Bin)
                | Left err => throw (InternalError (fname ++ ": " ++ show err))
          pure ()
 
+addGlobalDef : {auto c : Ref Ctxt Defs} ->
+               (modns : List String) -> (importAs : Maybe (List String)) ->
+               GlobalDef -> Core ()
+addGlobalDef modns as def 
+    = do let n = fullname def
+         addDef (asName modns as n) def
+         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
+-- hash 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) =>
+readFromTTC : TTC extra =>
               {auto c : Ref Ctxt Defs} ->
-              {auto u : Ref UST (UState annot)} ->
+              {auto u : Ref UST UState} ->
-              annot ->
+              FC -> Bool ->
-              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)))
+              Core (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
@@ -156,42 +198,39 @@ readFromTTC loc reexp fname modNS importAs
          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
+         r <- initNameRefs 1 -- this will be updated when we read the name
-         ttc <- fromBuf sh bin
+                             -- map from the file
-         -- Rename everything in the ttc's context according to the namespace
+         let as = if importAs == modNS 
-         -- it was imported as
+                     then Nothing 
-         -- [TODO]
+                     else Just importAs
-         let renamed = context ttc
+         ttc <- readTTCFile modNS as r bin
-
+         traverse (addGlobalDef modNS as) (context ttc)
-         -- Extend the current context with the updated definitions from the ttc
+         setNS (currentNS 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,
+         put UST (record { holes = fromList (holes ttc),
-                           constraints = constraints ttc } ust)
+                           constraints = fromList (constraints ttc) } ust)
-         pure (Just (extraData ttc, ifaceHash ttc, imported (context ttc)))
+         pure (Just (extraData ttc, ifaceHash ttc, imported ttc))
-        -} 
 
-getImportHashes : Ref Bin Binary ->
+getImportHashes : NameRefs -> Ref Bin Binary ->
                   Core (List (List String, Int))
-getImportHashes b
+getImportHashes r b
-    = do hdr <- fromBuf {a = String} b
+    = do hdr <- fromBuf r {a = String} b
          when (hdr /= "TTC") $ corrupt "TTC header"
-         ver <- fromBuf {a = Int} b
+         ver <- fromBuf r {a = Int} b
          checkTTCVersion ver ttcVersion
-         ifaceHash <- fromBuf {a = Int} b
+         ifaceHash <- fromBuf r {a = Int} b
-         fromBuf b
+         fromBuf r b
 
-getHash : Ref Bin Binary -> Core Int
+getHash : NameRefs -> Ref Bin Binary -> Core Int
-getHash b
+getHash r b
-    = do hdr <- fromBuf {a = String} b
+    = do hdr <- fromBuf r {a = String} b
          when (hdr /= "TTC") $ corrupt "TTC header"
-         ver <- fromBuf {a = Int} b
+         ver <- fromBuf r {a = Int} b
          checkTTCVersion ver ttcVersion
-         fromBuf b
+         fromBuf r b
 
 export
 readIFaceHash : (fname : String) -> -- file containing the module
@@ -200,8 +239,8 @@ readIFaceHash fname
     = do Right buf <- coreLift $ readFromFile fname
             | Left err => pure 0
          b <- newRef Bin buf
-         
+         r <- initNameRefs 1
-         catch (getHash b)
+         catch (getHash r b)
                (\err => pure 0)
 
 export
@@ -211,6 +250,7 @@ readImportHashes fname
     = do Right buf <- coreLift $ readFromFile fname
             | Left err => pure []
          b <- newRef Bin buf
-         catch (getImportHashes b)
+         r <- initNameRefs 1
+         catch (getImportHashes r b)
                (\err => pure [])
 

src/Core/Context.idr

@@ -4,6 +4,7 @@ import public Core.Core
 import public Core.Name
 import Core.Options
 import public Core.TT
+import Core.TTC
 import Utils.Binary
 
 import Data.IOArray
@@ -32,10 +33,21 @@ record Context a where
     -- visible
     visibleNS : List (List String)
 
+-- Make an array which is a mapping from IDs to the names they represent
+-- (the reverse of 'resolvedAs') which we use when serialising to record which
+-- name each ID refers to. Then when we read references in terms, we'll know
+-- which name it really is and can update appropriately for the new context.
 export
-TTC a => TTC (Context a) where
+getNameRefs : Context a -> Core NameRefs
-  toBuf = ?tocontext
+getNameRefs gam
-  fromBuf = ?fromcontext
+    = do arr <- coreLift $ newArray (nextEntry gam)
+         traverse (addToMap arr) (toList (resolvedAs gam))
+         pure arr
+  where
+    addToMap : NameRefs -> (Name, Int) -> Core ()
+    addToMap arr (n, i)
+        = coreLift $ writeArray arr i (n, Nothing)
+
 
 initSize : Int
 initSize = 10000
@@ -67,6 +79,7 @@ addPossible n i ps
 -- Get the position of the next entry in the context array, growing the
 -- array if it's out of bounds.
 -- Updates the context with the mapping from name to index
+export
 getPosition : Name -> Context a -> Core (Int, Context a)
 getPosition (Resolved idx) ctxt = pure (idx, ctxt)
 getPosition n ctxt
@@ -182,6 +195,33 @@ Show Def where
   show (Hole inv) = "Hole"
   show (Guess tm cs) = "Guess " ++ show tm ++ " when " ++ show cs
 
+export
+TTC Def where
+  toBuf b None = tag 0
+  toBuf b (Fn x) = do tag 1; toBuf b x
+  toBuf b (DCon t arity) = do tag 2; toBuf b t; toBuf b arity
+  toBuf b (TCon t arity parampos detpos datacons) 
+      = do tag 3; toBuf b t; toBuf b arity; toBuf b parampos
+           toBuf b detpos; toBuf b datacons
+  toBuf b (Hole invertible) = do tag 4; toBuf b invertible
+  toBuf b (Guess guess constraints) = do tag 5; toBuf b guess; toBuf b constraints
+
+  fromBuf r b 
+      = case !getTag of
+             0 => pure None
+             1 => do x <- fromBuf r b 
+                     pure (Fn x)
+             2 => do t <- fromBuf r b; a <- fromBuf r b
+                     pure (DCon t a)
+             3 => do t <- fromBuf r b; a <- fromBuf r b
+                     ps <- fromBuf r b; dets <- fromBuf r b; cs <- fromBuf r b
+                     pure (TCon t a ps dets cs)
+             4 => do i <- fromBuf r b;
+                     pure (Hole i)
+             5 => do g <- fromBuf r b; cs <- fromBuf r b
+                     pure (Guess g cs)
+             _ => corrupt "Def"
+
 public export
 record Constructor where
   constructor MkCon
@@ -195,18 +235,108 @@ data DataDef : Type where
      MkData : (tycon : Constructor) -> (datacons : List Constructor) ->
               DataDef
 
+public export
+data TotalReq = Total | CoveringOnly | PartialOK
+
+public export
+data DefFlag 
+    = TypeHint Name Bool -- True == direct hint
+    | GlobalHint Bool -- True == always search (not a default hint)
+    | Inline
+    | Invertible -- assume safe to cancel arguments in unification
+    | Overloadable -- allow ad-hoc overloads
+    | TCInline -- always inline before totality checking
+         -- (in practice, this means it's reduced in 'normaliseHoles')
+         -- This means the function gets inlined when calculating the size
+         -- change graph, but otherwise not. It's only safe if the function
+         -- being inlined is terminating no matter what, and is really a bit
+         -- of a hack to make sure interface dictionaries are properly inlined
+         -- (otherwise they look potentially non terminating) so use with
+         -- care!
+    | SetTotal TotalReq
+
+export
+Eq TotalReq where
+    (==) Total Total = True
+    (==) CoveringOnly CoveringOnly = True
+    (==) PartialOK PartialOK = True
+    (==) _ _ = False
+
+export
+Eq DefFlag where
+    (==) (TypeHint ty x) (TypeHint ty' y) = ty == ty' && x == y
+    (==) (GlobalHint x) (GlobalHint y) = x == y
+    (==) Inline Inline = True
+    (==) Invertible Invertible = True
+    (==) Overloadable Overloadable = True
+    (==) TCInline TCInline = True
+    (==) (SetTotal x) (SetTotal y) = x == y
+    (==) _ _ = False
+
+TTC TotalReq where
+  toBuf b Total = tag 0
+  toBuf b CoveringOnly = tag 1
+  toBuf b PartialOK = tag 2
+
+  fromBuf s b
+      = case !getTag of
+             0 => pure Total
+             1 => pure CoveringOnly
+             2 => pure PartialOK
+             _ => corrupt "TotalReq"
+
+TTC DefFlag where
+  toBuf b (TypeHint x y) = do tag 0; toBuf b x; toBuf b y
+  toBuf b (GlobalHint t) = do tag 1; toBuf b t
+  toBuf b Inline = tag 2
+  toBuf b Invertible = tag 3
+  toBuf b Overloadable = tag 4
+  toBuf b TCInline = tag 5
+  toBuf b (SetTotal x) = do tag 6; toBuf b x
+
+  fromBuf s b
+      = case !getTag of
+             0 => do x <- fromBuf s b; y <- fromBuf s b; pure (TypeHint x y)
+             1 => do t <- fromBuf s b; pure (GlobalHint t)
+             2 => pure Inline
+             3 => pure Invertible
+             4 => pure Overloadable
+             5 => pure TCInline
+             6 => do x <- fromBuf s b; pure (SetTotal x)
+             _ => corrupt "DefFlag"
+
 public export
 record GlobalDef where
   constructor MkGlobalDef
   location : FC
+  fullname : Name -- original unresolved name
   type : ClosedTerm
   multiplicity : RigCount
   visibility : Visibility
+  flags : List DefFlag
   definition : Def
 
 export
-newDef : FC -> RigCount -> ClosedTerm -> Visibility -> Def -> GlobalDef
+TTC GlobalDef where
-newDef fc rig ty vis def = MkGlobalDef fc ty rig vis def
+  toBuf b gdef 
+      = do toBuf b (location gdef)
+           toBuf b (fullname gdef)
+           toBuf b (type gdef)
+           toBuf b (multiplicity gdef)
+           toBuf b (visibility gdef)
+           toBuf b (flags gdef)
+           toBuf b (definition gdef)
+
+  fromBuf r b 
+      = do loc <- fromBuf r b; name <- fromBuf r b
+           ty <- fromBuf r b; mul <- fromBuf r b
+           vis <- fromBuf r b; fl <- fromBuf r b
+           def <- fromBuf r b
+           pure (MkGlobalDef loc name ty mul vis fl def)
+
+export
+newDef : FC -> Name -> RigCount -> ClosedTerm -> Visibility -> Def -> GlobalDef
+newDef fc n rig ty vis def = MkGlobalDef fc n ty rig vis [] def
 
 public export
 record Defs where
@@ -214,9 +344,17 @@ record Defs where
   gamma : Context GlobalDef
   currentNS : List String -- namespace for current definitions
   options : Options
---   toSave : SortedSet
+  toSave : NameMap ()
   nextTag : Int
   ifaceHash : Int
+  -- interface hashes of imported modules
+  importHashes : List (List String, Int)
+  -- imported modules, whether to rexport, as namespace
+  imported : List (List String, Bool, List String)
+  -- all imported filenames/namespaces, just to avoid loading something
+  -- twice unnecessarily (this is a record of all the things we've
+  -- called 'readFromTTC' with, in practice)
+  allImported : List (String, List String)
 
 export
 clearDefs : Defs -> Core Defs
@@ -228,12 +366,11 @@ export
 initDefs : Core Defs
 initDefs 
     = do gam <- initCtxt
-         pure (MkDefs gam ["Main"] defaults 100 5381)
+         pure (MkDefs gam ["Main"] defaults empty 100 5381 [] [] [])
       
 export
-TTC Defs where
+getSave : Defs -> List Name
-  toBuf = ?todefs
+getSave = map Basics.fst . toList . toSave
-  fromBuf = ?fromdefs
 
 -- Label for context references
 export
@@ -248,6 +385,28 @@ addDef n def
          put Ctxt (record { gamma = gam' } defs)
          pure idx
 
+export
+setCtxt : {auto c : Ref Ctxt Defs} -> Context GlobalDef -> Core ()
+setCtxt gam
+    = do defs <- get Ctxt
+         put Ctxt (record { gamma = gam } defs)
+
+-- Set the default namespace for new definitions
+export
+setNS : {auto c : Ref Ctxt Defs} ->
+        List String -> Core ()
+setNS ns
+    = do defs <- get Ctxt
+         put Ctxt (record { currentNS = ns } defs)
+
+-- Get the default namespace for new definitions
+export
+getNS : {auto c : Ref Ctxt Defs} ->
+        Core (List String)
+getNS
+    = do defs <- get Ctxt
+         pure (currentNS defs)
+
 getNextTypeTag : {auto c : Ref Ctxt Defs} ->
                  Core Int
 getNextTypeTag
@@ -264,7 +423,7 @@ addData : {auto c : Ref Ctxt Defs} ->
 addData vis (MkData (MkCon dfc tyn arity tycon) datacons)
     = do defs <- get Ctxt 
          tag <- getNextTypeTag 
-         let tydef = newDef dfc RigW tycon vis 
+         let tydef = newDef dfc tyn RigW tycon vis 
                             (TCon tag arity 
                                   (paramPos tyn (map type datacons))
                                   (allDet arity)
@@ -286,7 +445,7 @@ addData vis (MkData (MkCon dfc tyn arity tycon) datacons)
                           Context GlobalDef -> Core (Context GlobalDef)
     addDataConstructors tag [] gam = pure gam
     addDataConstructors tag (MkCon fc n a ty :: cs) gam
-        = do let condef = newDef fc RigW ty (conVisibility vis) (DCon tag a)
+        = do let condef = newDef fc n RigW ty (conVisibility vis) (DCon tag a)
              (idx, gam') <- addCtxt n condef gam
              addDataConstructors (tag + 1) cs gam'
 

src/Core/Hash.idr

@@ -3,7 +3,7 @@ module Core.Hash
 import Core.TT
 import Data.List
 
-%default total
+%default covering
 
 -- 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.
@@ -18,10 +18,20 @@ interface Hashable a where
   hash = hashWithSalt 5381
   hashWithSalt h i = h * 33 + hash i
 
+infixl 5 `hashWithSalt`
+
 export
 Hashable Int where
   hash = id
 
+export
+Hashable Integer where
+  hash = fromInteger
+
+export
+Hashable Nat where
+  hash = cast
+
 export
 Hashable Char where
   hash = cast
@@ -31,6 +41,11 @@ Hashable a => Hashable (List a) where
   hashWithSalt h [] = abs h
   hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs
 
+export
+Hashable a => Hashable (Maybe a) where
+  hashWithSalt h Nothing = abs h
+  hashWithSalt h (Just x) = hashWithSalt h x
+
 export
 Hashable String where
   hashWithSalt h str = hashChars h 0 (cast (length str)) str
@@ -46,47 +61,104 @@ Hashable String where
 export
 Hashable Name where
   hashWithSalt h (MN s _) = hashWithSalt h s
+  hashWithSalt h (Resolved i) = i
   hashWithSalt h n = hashWithSalt h (show n)
 
-count : RigCount -> String
+export
-count Rig0 = "0"
+Hashable RigCount where
-count Rig1 = "1"
+  hashWithSalt h Rig0 = hashWithSalt h 0
-count RigW = "w"
+  hashWithSalt h Rig1 = hashWithSalt h 1
-
+  hashWithSalt h RigW = hashWithSalt h 2
-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
+Hashable PiInfo where
-  hashWithSalt h tm 
+  hashWithSalt h Implicit = hashWithSalt h 0
-     = hashWithSalt h (hshow tm)
+  hashWithSalt h Explicit = hashWithSalt h 1
+  hashWithSalt h AutoImplicit = hashWithSalt h 2
+
+export
+Hashable ty => Hashable (Binder ty) where
+  hashWithSalt h (Lam c p ty) 
+      = h `hashWithSalt` 0 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
+  hashWithSalt h (Let c val ty)
+      = h `hashWithSalt` 1 `hashWithSalt` c `hashWithSalt` val `hashWithSalt` ty
+  hashWithSalt h (Pi c p ty)
+      = h `hashWithSalt` 2 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
+  hashWithSalt h (PVar c ty)
+      = h `hashWithSalt` 3 `hashWithSalt` c `hashWithSalt` ty
+  hashWithSalt h (PVTy c ty)
+      = h `hashWithSalt` 4 `hashWithSalt` c `hashWithSalt` ty
+
+Hashable (Var vars) where
+  hashWithSalt h (MkVar {i} _) = hashWithSalt h i
+
+mutual
+  export
+  Hashable (Term vars) where
+    hashWithSalt h (Local fc x idx y) 
+        = h `hashWithSalt` 0 `hashWithSalt` idx
+    hashWithSalt h (Ref fc x name) 
+        = h `hashWithSalt` 1 `hashWithSalt` name
+    hashWithSalt h (Meta fc x y xs) 
+        = h `hashWithSalt` 2 `hashWithSalt` y `hashWithSalt` xs
+    hashWithSalt h (Bind fc x b scope) 
+        = h `hashWithSalt` 3 `hashWithSalt` b `hashWithSalt` scope
+    hashWithSalt h (App fc fn p arg) 
+        = h `hashWithSalt` 4 `hashWithSalt` fn `hashWithSalt` arg
+    hashWithSalt h (Case fc cs ty tree  alts) 
+        = h `hashWithSalt` 5 `hashWithSalt` cs `hashWithSalt` ty
+            `hashWithSalt` tree `hashWithSalt` alts
+    hashWithSalt h (TDelayed fc x y) 
+        = h `hashWithSalt` 6 `hashWithSalt` y
+    hashWithSalt h (TDelay fc x y)
+        = h `hashWithSalt` 7 `hashWithSalt` y
+    hashWithSalt h (TForce fc x)
+        = h `hashWithSalt` 8 `hashWithSalt` x
+    hashWithSalt h (PrimVal fc c) 
+        = h `hashWithSalt` 9 `hashWithSalt` (show c)
+    hashWithSalt h (Erased fc) 
+        = hashWithSalt h 10
+    hashWithSalt h (TType fc)
+        = hashWithSalt h 11
+
+  export
+  Hashable (Pat vars) where
+    hashWithSalt h (PAs fc idx x y) 
+        = h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` y
+    hashWithSalt h (PCon fc x tag arity xs) 
+        = h `hashWithSalt` 1 `hashWithSalt` x `hashWithSalt` xs
+    hashWithSalt h (PLoc fc idx x) 
+        = h `hashWithSalt` 2 `hashWithSalt` idx
+    hashWithSalt h (PUnmatchable fc x) 
+        = h `hashWithSalt` 3 `hashWithSalt` x
+
+  export
+  Hashable (PatAlt vars) where
+    hashWithSalt h (CBind c n ty p) 
+        = h `hashWithSalt` 0 `hashWithSalt` c `hashWithSalt` n
+            `hashWithSalt` p
+    hashWithSalt h (CPats xs x) 
+        = h `hashWithSalt` 1 `hashWithSalt` xs `hashWithSalt` x
+
+  export
+  Hashable (CaseTree vars) where
+    hashWithSalt h (Switch idx x scTy xs) 
+        = h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` xs
+    hashWithSalt h (STerm x) 
+        = h `hashWithSalt` 1 `hashWithSalt` x
+    hashWithSalt h (Unmatched msg) 
+        = h `hashWithSalt` 2
+    hashWithSalt h Impossible
+        = h `hashWithSalt` 3
+
+  export
+  Hashable (CaseAlt vars) where
+    hashWithSalt h (ConCase x tag args y) 
+        = h `hashWithSalt` 0 `hashWithSalt` x `hashWithSalt` args
+            `hashWithSalt` y
+    hashWithSalt h (ConstCase x y) 
+        = h `hashWithSalt` 1 `hashWithSalt` (show x) `hashWithSalt` y
+    hashWithSalt h (DefaultCase x) 
+        = h `hashWithSalt` 2 `hashWithSalt` x
+
 

src/Core/Options.idr

@@ -41,7 +41,7 @@ TTC CG where
   toBuf b Chicken = tag 1
   toBuf b Racket = tag 2
 
-  fromBuf b
+  fromBuf r b
       = case !getTag of
              0 => pure Chez
              1 => pure Chicken

src/Core/TT.idr

@@ -237,7 +237,7 @@ data IsVar : Name -> Nat -> List Name -> Type where
 
 public export
 data Var : List Name -> Type where
-     MkVar : {i : Nat} -> IsVar n i vars -> Var vars
+     MkVar : {i : Nat} -> {n : _} -> IsVar n i vars -> Var vars
 
 export
 sameVar : {i, j : _} -> IsVar n i xs -> IsVar m j xs -> Bool
@@ -300,10 +300,12 @@ mutual
 
   public export
   data Pat : List Name -> Type where
-       PAs : FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars -> Pat vars
+       PAs : {name : _} ->
+             FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars -> Pat vars
        PCon : FC -> Name -> (tag : Int) -> (arity : Nat) ->
               List (Pat vars) -> Pat vars
-       PLoc : FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars
+       PLoc : {name : _} ->
+              FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars
        PUnmatchable : FC -> Term vars -> Pat vars
 
   public export
@@ -314,7 +316,8 @@ mutual
 
   public export
   data CaseTree : List Name -> Type where
-       Switch : (idx : Nat) -> IsVar name idx vars ->
+       Switch : {name : _} ->
+                (idx : Nat) -> IsVar name idx vars ->
                 (scTy : Term vars) -> List (CaseAlt vars) ->
                 CaseTree vars
        STerm : Term vars -> CaseTree vars

src/Core/TTC.idr

@@ -1,18 +1,362 @@
 module Core.TTC
 
 import Core.Core
+import Core.Env
 import Core.FC
 import Core.TT
 
 import Utils.Binary
 
+%default covering
+
 export
 TTC FC where
-  toBuf = ?tofc
+  toBuf b (MkFC file startPos endPos) 
-  fromBuf = ?fromfc
+      = do toBuf b file; toBuf b startPos; toBuf b endPos
+  fromBuf r b
+      = do f <- fromBuf r b; s <- fromBuf r b; e <- fromBuf r b
+           pure (MkFC f s e)
 
 export
 TTC Name where
-  toBuf = ?toName
+  toBuf b (NS xs x) = do tag 0; toBuf b xs; toBuf b x
-  fromBuf = ?fromName
+  toBuf b (UN x) = do tag 1; toBuf b x
+  toBuf b (MN x y) = do tag 2; toBuf b x; toBuf b y
+  toBuf b (PV x y) = do tag 3; toBuf b x; toBuf b y
+  toBuf b (Nested x y) = do tag 4; toBuf b x; toBuf b y
+  toBuf b (Resolved x) = do tag 5; toBuf b x
+
+  fromBuf r b
+      = case !getTag of
+             0 => do xs <- fromBuf r b
+                     x <- fromBuf r b
+                     pure (NS xs x)
+             1 => do x <- fromBuf r b
+                     pure (UN x)
+             2 => do x <- fromBuf r b
+                     y <- fromBuf r b
+                     pure (MN x y)
+             3 => do x <- fromBuf r b
+                     y <- fromBuf r b
+                     pure (PV x y)
+             4 => do x <- fromBuf r b
+                     y <- fromBuf r b
+                     pure (Nested x y)
+             5 => do x <- fromBuf r b
+                     Just (n, Just idx) <- coreLift $ readArray r x
+                          | Just (n, Nothing) => pure n
+                          | Nothing => corrupt "Name index"
+                     pure (Resolved idx)
+             _ => corrupt "Name"
+            
+export 
+TTC RigCount where
+  toBuf b Rig0 = tag 0
+  toBuf b Rig1 = tag 1
+  toBuf b RigW = tag 2
+
+  fromBuf r b
+      = case !getTag of
+             0 => pure Rig0
+             1 => pure Rig1
+             2 => pure RigW
+             _ => corrupt "RigCount"
+
+export
+TTC PiInfo where
+  toBuf b Implicit = tag 0
+  toBuf b Explicit = tag 1
+  toBuf b AutoImplicit = tag 2
+
+  fromBuf r b
+      = case !getTag of
+             0 => pure Implicit
+             1 => pure Explicit
+             2 => pure AutoImplicit
+             _ => corrupt "PiInfo"
+
+export
+TTC ty => TTC (Binder ty) where
+  toBuf b (Lam c x ty) = do tag 0; toBuf b c; toBuf b x; toBuf b ty
+  toBuf b (Let c val ty) = do tag 1; toBuf b c; toBuf b val; toBuf b ty
+  toBuf b (Pi c x ty) = do tag 2; toBuf b c; toBuf b x; toBuf b ty
+  toBuf b (PVar c ty) = do tag 3; toBuf b c; toBuf b ty
+  toBuf b (PVTy c ty) = do tag 4; toBuf b c; toBuf b ty
+
+  fromBuf r b
+      = case !getTag of
+             0 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Lam c x y)
+             1 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Let c x y)
+             2 => do c <- fromBuf r b; x <- fromBuf r b; y <- fromBuf r b; pure (Pi c x y)
+             3 => do c <- fromBuf r b; x <- fromBuf r b; pure (PVar c x)
+             4 => do c <- fromBuf r b; x <- fromBuf r b; pure (PVTy c x)
+             _ => corrupt "Binder"
+
+export
+TTC Visibility where
+  toBuf b Private = tag 0
+  toBuf b Export = tag 1
+  toBuf b Public = tag 2
+
+  fromBuf s b 
+      = case !getTag of
+             0 => pure Private
+             1 => pure Export
+             2 => pure Public
+             _ => corrupt "Visibility"
+
+export
+TTC Constant where
+  toBuf b (I x) = do tag 0; toBuf b x
+  toBuf b (BI x) = do tag 1; toBuf b x
+  toBuf b (Str x) = do tag 2; toBuf b x
+  toBuf b (Ch x) = do tag 3; toBuf b x
+  toBuf b (Db x) = do tag 4; toBuf b x
+  
+  toBuf b WorldVal = tag 5
+  toBuf b IntType = tag 6
+  toBuf b IntegerType = tag 7 
+  toBuf b StringType = tag 8
+  toBuf b CharType = tag 9
+  toBuf b DoubleType = tag 10
+  toBuf b WorldType = tag 11
+
+  fromBuf r b
+      = case !getTag of
+             0 => do x <- fromBuf r b; pure (I x)
+             1 => do x <- fromBuf r b; pure (BI x)
+             2 => do x <- fromBuf r b; pure (Str x)
+             3 => do x <- fromBuf r b; pure (Ch x)
+             4 => do x <- fromBuf r b; pure (Db x)
+             5 => pure WorldVal
+             6 => pure IntType
+             7 => pure IntegerType
+             8 => pure StringType
+             9 => pure CharType
+             10 => pure DoubleType
+             11 => pure WorldType
+             _ => corrupt "Constant"
+
+export
+TTC LazyReason where
+  toBuf b LInf = tag 0
+  toBuf b LLazy = tag 1
+
+  fromBuf r b
+      = case !getTag of
+             0 => pure LInf
+             1 => pure LLazy
+             _ => corrupt "LazyReason"
+
+export
+TTC NameType where
+  toBuf b Bound = tag 0
+  toBuf b Func = tag 1
+  toBuf b (DataCon t arity) = do tag 2; toBuf b t; toBuf b arity
+  toBuf b (TyCon t arity) = do tag 3; toBuf b t; toBuf b arity
+
+  fromBuf r b
+      = case !getTag of
+             0 => pure Bound
+             1 => pure Func
+             2 => do x <- fromBuf r b; y <- fromBuf r b; pure (DataCon x y)
+             3 => do x <- fromBuf r b; y <- fromBuf r b; pure (TyCon x y)
+             _ => corrupt "NameType"
+
+export
+TTC AppInfo where
+  toBuf b (MkAppInfo an p)
+      = do toBuf b an; toBuf b p
+  fromBuf r b
+      = do an <- fromBuf r b; p <- fromBuf r b
+           pure (MkAppInfo an p)
+
+-- Assumption is that it was type safe when we wrote it out, so believe_me
+-- to rebuild proofs is fine.
+-- We're just making up the implicit arguments - this is only fine at run
+-- time because those arguments get erased!
+-- (Indeed, we're expecting the whole IsVar proof to be erased because
+-- we have the idx...)
+mkPrf : (idx : Nat) -> IsVar n idx ns
+mkPrf {n} {ns} Z = believe_me (First {n} {ns = n :: ns})
+mkPrf {n} {ns} (S k) = believe_me (Later {m=n} (mkPrf {n} {ns} k))
+
+export
+TTC (Var vars) where
+  toBuf b (MkVar {i} {n} v) = do toBuf b n; toBuf b i
+  fromBuf r b
+      = do n <- fromBuf r b
+           i <- fromBuf r b
+           pure (MkVar {n} (mkPrf i))
+
+mutual
+  export
+  TTC (Term vars) where
+    toBuf b (Local {name} fc c idx y) 
+        = do tag 0;
+             toBuf b fc; toBuf b name
+             toBuf b c; toBuf b idx
+    toBuf b (Ref fc nt name) 
+        = do tag 1;
+             toBuf b fc; toBuf b nt; toBuf b name
+    toBuf b (Meta fc n i xs) 
+        = do tag 2;
+             toBuf b fc; toBuf b n; toBuf b i; toBuf b xs
+    toBuf b (Bind fc x bnd scope) 
+        = do tag 3;
+             toBuf b fc; toBuf b bnd; toBuf b scope
+    toBuf b (App fc fn p arg) 
+        = do tag 4;
+             toBuf b fc; toBuf b fn; toBuf b p; toBuf b arg
+    toBuf b (Case fc cs ty tree alts) 
+        = do tag 5;
+             toBuf b fc; toBuf b cs; toBuf b ty; toBuf b tree; toBuf b alts
+    toBuf b (TDelayed fc r tm) 
+        = do tag 6;
+             toBuf b fc; toBuf b r; toBuf b tm
+    toBuf b (TDelay fc r tm)
+        = do tag 7;
+             toBuf b fc; toBuf b r; toBuf b tm
+    toBuf b (TForce fc tm)
+        = do tag 8;
+             toBuf b fc; toBuf b tm
+    toBuf b (PrimVal fc c) 
+        = do tag 9;
+             toBuf b fc; toBuf b c
+    toBuf b (Erased fc) 
+        = do tag 10;
+             toBuf b fc
+    toBuf b (TType fc)
+        = do tag 11;
+             toBuf b fc
+
+    fromBuf r b 
+        = case !getTag of
+               0 => do fc <- fromBuf r b; name <- fromBuf r b
+                       c <- fromBuf r b; idx <- fromBuf r b
+                       pure (Local {name} fc c idx (mkPrf idx))
+               1 => do fc <- fromBuf r b; nt <- fromBuf r b; name <- fromBuf r b
+                       pure (Ref fc nt name)
+               2 => do fc <- fromBuf r b; n <- fromBuf r b; i <- fromBuf r b
+                       xs <- fromBuf r b
+                       pure (Meta fc n i xs)
+               3 => do fc <- fromBuf r b; x <- fromBuf r b
+                       bnd <- fromBuf r b; scope <- fromBuf r b
+                       pure (Bind fc x bnd scope)
+               4 => do fc <- fromBuf r b; fn <- fromBuf r b
+                       p <- fromBuf r b; arg <- fromBuf r b
+                       pure (App fc fn p arg)
+               5 => do fc <- fromBuf r b; cs <- fromBuf r b
+                       ty <- fromBuf r b; tree <- fromBuf r b
+                       alts <- fromBuf r b
+                       pure (Case fc cs ty tree alts)
+               6 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
+                       pure (TDelayed fc lr tm)
+               7 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
+                       pure (TDelay fc lr tm)
+               8 => do fc <- fromBuf r b; tm <- fromBuf r b
+                       pure (TForce fc tm)
+               9 => do fc <- fromBuf r b; c <- fromBuf r b
+                       pure (PrimVal fc c)
+               10 => do fc <- fromBuf r b; pure (Erased fc)
+               11 => do fc <- fromBuf r b; pure (TType fc)
+               _ => corrupt "Term"
+
+  export
+  TTC (Pat vars) where
+    toBuf b (PAs {name} fc idx x y) 
+        = do tag 0; toBuf b fc; toBuf b name; toBuf b idx; toBuf b y
+    toBuf b (PCon fc x t arity xs) 
+        = do tag 1; toBuf b fc; toBuf b t; toBuf b arity; toBuf b xs
+    toBuf b (PLoc {name} fc idx x) 
+        = do tag 2; toBuf b fc; toBuf b name; toBuf b idx
+    toBuf b (PUnmatchable fc x) 
+        = do tag 3; toBuf b fc; toBuf b x
+
+    fromBuf r b 
+        = case !getTag of
+               0 => do fc <- fromBuf r b; name <- fromBuf r b;
+                       idx <- fromBuf r b; y <- fromBuf r b
+                       pure (PAs {name} fc idx (mkPrf idx) y)
+               1 => do fc <- fromBuf r b; x <- fromBuf r b
+                       t <- fromBuf r b; arity <- fromBuf r b
+                       xs <- fromBuf r b
+                       pure (PCon fc x t arity xs)
+               2 => do fc <- fromBuf r b; name <- fromBuf r b
+                       idx <- fromBuf r b
+                       pure (PLoc {name} fc idx (mkPrf idx))
+               3 => do fc <- fromBuf r b; x <- fromBuf r b
+                       pure (PUnmatchable fc x)
+               _ => corrupt "Pat"
+
+  export
+  TTC (PatAlt vars) where
+    toBuf b (CBind c x ty alt) 
+        = do tag 0; toBuf b c; toBuf b x; toBuf b ty; toBuf b alt
+    toBuf b (CPats xs tm) 
+        = do tag 1; toBuf b xs; toBuf b tm
+
+    fromBuf r b 
+        = case !getTag of
+               0 => do c <- fromBuf r b; x <- fromBuf r b
+                       ty <- fromBuf r b; alt <- fromBuf r b
+                       pure (CBind c x ty alt)
+               1 => do xs <- fromBuf r b; tm <- fromBuf r b
+                       pure (CPats xs tm)
+               _ => corrupt "PatAlt"
+
+  export
+  TTC (CaseTree vars) where
+    toBuf b (Switch {name} idx x scTy xs) 
+        = do tag 0; toBuf b name; toBuf b idx; toBuf b scTy; toBuf b xs
+    toBuf b (STerm x) 
+        = do tag 1; toBuf b x
+    toBuf b (Unmatched msg) 
+        = do tag 2; toBuf b msg
+    toBuf b Impossible = tag 3
+
+    fromBuf r b 
+        = case !getTag of
+               0 => do name <- fromBuf r b; idx <- fromBuf r b
+                       scTy <- fromBuf r b; xs <- fromBuf r b
+                       pure (Switch {name} idx (mkPrf idx) scTy xs)
+               1 => do x <- fromBuf r b
+                       pure (STerm x)
+               2 => do msg <- fromBuf r b
+                       pure (Unmatched msg)
+               3 => pure Impossible
+               _ => corrupt "CaseTree"
+
+  export
+  TTC (CaseAlt vars) where
+    toBuf b (ConCase x t args y) 
+        = do tag 0; toBuf b x; toBuf b t; toBuf b args; toBuf b y
+    toBuf b (ConstCase x y)
+        = do tag 1; toBuf b x; toBuf b y
+    toBuf b (DefaultCase x)
+        = do tag 2; toBuf b x
+
+    fromBuf r b 
+        = case !getTag of
+               0 => do x <- fromBuf r b; t <- fromBuf r b
+                       args <- fromBuf r b; y <- fromBuf r b
+                       pure (ConCase x t args y)
+               1 => do x <- fromBuf r b; y <- fromBuf r b
+                       pure (ConstCase x y)
+               2 => do x <- fromBuf r b
+                       pure (DefaultCase x)
+               _ => corrupt "CaseAlt"
+
+export
+TTC (Env Term vars) where
+  toBuf b [] = pure ()
+  toBuf b ((::) bnd env) 
+      = do toBuf b bnd; toBuf b env
+
+  -- Length has to correspond to length of 'vars'
+  fromBuf s {vars = []} b = pure Nil
+  fromBuf s {vars = x :: xs} b
+      = do bnd <- fromBuf s b
+           env <- fromBuf s b
+           pure (bnd :: env)
 

src/Core/UnifyState.idr

@@ -16,14 +16,16 @@ public export
 data Constraint : Type where
      -- An unsolved constraint, noting two terms which need to be convertible
      -- in a particular environment
-     MkConstraint : FC -> 
+     MkConstraint : {vars : _} ->
+                    FC -> 
                     (env : Env Term vars) ->
                     (x : Term vars) -> (y : Term vars) -> 
                     Constraint
      -- An unsolved sequence of constraints, arising from arguments in an
      -- application where solving later constraints relies on solving earlier
      -- ones
-     MkSeqConstraint : FC ->
+     MkSeqConstraint : {vars : _} ->
+                       FC ->
                        (env : Env Term vars) ->
                        (xs : List (Term vars)) ->
                        (ys : List (Term vars)) ->
@@ -33,8 +35,24 @@ data Constraint : Type where
 
 export
 TTC Constraint where
-  toBuf = ?toconstraint
+  toBuf b (MkConstraint {vars} fc env x y) 
-  fromBuf = ?fromconstraint
+     = do tag 0; toBuf b vars; toBuf b fc; toBuf b env; toBuf b x; toBuf b y
+  toBuf b (MkSeqConstraint {vars} fc env xs ys)
+     = do tag 1; toBuf b vars; toBuf b fc; toBuf b env; toBuf b xs; toBuf b ys
+  toBuf b Resolved = tag 2
+
+  fromBuf r b 
+      = case !getTag of
+             0 => do vars <- fromBuf r b
+                     fc <- fromBuf r b; env <- fromBuf r b
+                     x <- fromBuf r b; y <- fromBuf r b
+                     pure (MkConstraint {vars} fc env x y)
+             1 => do vars <- fromBuf r b
+                     fc <- fromBuf r b; env <- fromBuf r b
+                     xs <- fromBuf r b; ys <- fromBuf r b
+                     pure (MkSeqConstraint {vars} fc env xs ys)
+             2 => pure Resolved
+             _ => corrupt "Constraint"
 
 public export
 record UState where
@@ -157,7 +175,7 @@ newMeta : {auto c : Ref Ctxt Defs} ->
           Env Term vars -> Name -> Term vars -> Core (Term vars)
 newMeta {vars} fc rig env n ty
     = do let hty = abstractEnvType fc env ty
-         let hole = newDef fc rig hty Public (Hole False)
+         let hole = newDef fc n rig hty Public (Hole False)
          idx <- addDef n hole 
          addHoleName fc n idx
          pure (Meta fc n idx envArgs)
@@ -187,8 +205,8 @@ newConstant : {auto u : Ref UST UState} ->
 newConstant fc rig env tm ty constrs
     = do let def = mkConstant fc env tm
          let defty = abstractEnvType fc env ty
-         let guess = newDef fc rig defty Public (Guess def constrs)
          cn <- genName "p"
+         let guess = newDef fc cn rig defty Public (Guess def constrs)
          idx <- addDef cn guess
          addGuessName fc cn idx
          pure (applyTo fc (Ref fc Func (Resolved idx)) env)

src/Data/IOArray.idr

@@ -94,3 +94,29 @@ newArrayCopy newsize arr
                      unsafeWriteArray new pos el
                      assert_total (copyFrom old new (pos - 1))
 
+export
+toList : IOArray elem -> IO (List (Maybe elem))
+toList arr = iter 0 (max arr) []
+  where
+    iter : Int -> Int -> List (Maybe elem) -> IO (List (Maybe elem))
+    iter pos end acc
+         = if pos >= end
+              then pure (reverse acc)
+              else do el <- readArray arr pos
+                      assert_total (iter (pos + 1) end (el :: acc))
+
+export
+fromList : List (Maybe elem) -> IO (IOArray elem)
+fromList ns
+    = do arr <- newArray (cast (length ns))
+         addToArray 0 ns arr
+         pure arr
+  where
+    addToArray : Int -> List (Maybe elem) -> IOArray elem -> IO ()
+    addToArray loc [] arr = pure ()
+    addToArray loc (Nothing :: ns) arr 
+        = assert_total (addToArray (loc + 1) ns arr)
+    addToArray loc (Just el :: ns) arr
+        = do unsafeWriteArray (content arr) loc (Just el)
+             assert_total (addToArray (loc + 1) ns arr)
+

src/TTImp/ProcessData.idr

@@ -76,7 +76,7 @@ processData env fc vis (MkImpLater dfc n_in ty_raw)
 
          -- Add the type constructor as a placeholder while checking
          -- data constructors
-         tidx <- addDef n (newDef fc Rig1 fullty vis
+         tidx <- addDef n (newDef fc n Rig1 fullty vis
                           (TCon 0 arity [] [] []))
          pure ()
 processData env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
@@ -105,7 +105,7 @@ processData env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
 
          -- Add the type constructor as a placeholder while checking
          -- data constructors
-         tidx <- addDef n (newDef fc Rig1 fullty vis
+         tidx <- addDef n (newDef fc n Rig1 fullty vis
                           (TCon 0 arity [] [] []))
 
          -- Constructors are private if the data type as a whole is

src/TTImp/ProcessType.idr

@@ -26,7 +26,7 @@ processType env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          -- TODO: Check name visibility
          let def = None -- TODO: External definitions
 
-         addDef n (newDef fc rig (abstractEnvType tfc env ty) vis def)
+         addDef n (newDef fc n rig (abstractEnvType tfc env ty) vis def)
 
          -- TODO: Interface hash and saving
          pure ()

src/Utils/Binary.idr

@@ -1,10 +1,14 @@
 module Utils.Binary
 
 import Core.Core
+import Core.Name
+
 import Data.Buffer
+import public Data.IOArray
 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.
@@ -15,9 +19,9 @@ import Data.Vect
 export 
 data Bin : Type where
 
--- A label for storing shared strings
+-- A label for storing resolved name ids
 export
-data Share : Type where
+data ResID : Type where
 
 -- A component of the serialised data.
 record Chunk where
@@ -122,13 +126,23 @@ readFromFile fname
          b <- readBufferFromFile h b max
          pure (Right (MkBin [] (MkChunk b 0 max max) []))
 
+-- A mapping from the resolved name ids encountered in a TTC file to the
+-- name they represent, and (if known) the new resolved id it'll be after
+-- reading
+-- (We need this because files will be used in different contexts and resolved
+-- name ids are not going to be unique, so we need to recalculate them when
+-- loading from TTC)
+public export
+NameRefs : Type
+NameRefs = IOArray (Name, Maybe Int)
+
 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
+  fromBuf : NameRefs -> Ref Bin Binary -> Core a
 
 -- Create a new list of chunks, initialised with one 64k chunk
 export
@@ -138,6 +152,11 @@ initBinary
              | Nothing => throw (InternalError "Buffer creation failed")
          newRef Bin (MkBin [] (newChunk buf) [])
 
+export
+initNameRefs : Int -> Core NameRefs
+initNameRefs num 
+    = coreLift $ newArray num
+
 export
 corrupt : String -> Core a
 corrupt ty = throw (TTCError (Corrupt ty))
@@ -161,7 +180,7 @@ TTC Bits8 where
                                 (MkChunk newbuf 1 (size newbuf) 1)
                                 rest)
 
-  fromBuf b
+  fromBuf s b
     = do MkBin done chunk rest <- get Bin
          if toRead chunk >= 1
             then
@@ -181,8 +200,9 @@ tag : {auto b : Ref Bin Binary} -> Bits8 -> Core ()
 tag {b} val = toBuf b val
 
 export
-getTag : {auto b : Ref Bin Binary} -> Core Bits8
+getTag : {auto r : NameRefs} ->
-getTag {b} = fromBuf b
+         {auto b : Ref Bin Binary} -> Core Bits8
+getTag {r} {b} = fromBuf r b
 
 -- Some useful types from the prelude
 
@@ -201,7 +221,7 @@ TTC Int where
                  put Bin (MkBin (chunk :: done)
                                 (MkChunk newbuf 4 (size newbuf) 4)
                                 rest)
-  fromBuf b 
+  fromBuf r b 
     = do MkBin done chunk rest <- get Bin
          if toRead chunk >= 4
             then
@@ -234,8 +254,8 @@ TTC String where
                                   (MkChunk newbuf req (size newbuf) req)
                                   rest)
 
-  fromBuf b 
+  fromBuf r b 
-      = do len <- fromBuf {a = Int} b
+      = do len <- fromBuf {a = Int} r b
            MkBin done chunk rest <- get Bin
            if toRead chunk >= len
               then
@@ -255,7 +275,7 @@ export
 TTC Bool where
   toBuf b False = tag 0
   toBuf b True = tag 1
-  fromBuf b
+  fromBuf r b
       = case !getTag of
              0 => pure False
              1 => pure True
@@ -264,8 +284,8 @@ TTC Bool where
 export
 TTC Char where
   toBuf b c = toBuf b (cast {to=Int} c)
-  fromBuf b
+  fromBuf r b
-      = do i <- fromBuf b
+      = do i <- fromBuf r b
            pure (cast {from=Int} i)
 
 export
@@ -283,7 +303,7 @@ TTC Double where
                  put Bin (MkBin (chunk :: done)
                                 (MkChunk newbuf 8 (size newbuf) 8)
                                 rest)
-  fromBuf b 
+  fromBuf r b 
     = do MkBin done chunk rest <- get Bin
          if toRead chunk >= 8
             then
@@ -303,15 +323,15 @@ export
   toBuf b (x, y)
      = do toBuf b x
           toBuf b y
-  fromBuf b
+  fromBuf r b
-     = do x <- fromBuf b
+     = do x <- fromBuf r b
-          y <- fromBuf b
+          y <- fromBuf r b
           pure (x, y)
 
 export
 TTC () where
   toBuf b () = pure ()
-  fromBuf b = pure ()
+  fromBuf r b = pure ()
 
 export
 (TTC a, {y : a} -> TTC (p y)) => TTC (DPair a p) where
@@ -319,9 +339,9 @@ export
       = do toBuf b vs
            toBuf b tm
 
-  fromBuf b
+  fromBuf r b
-      = do x <- fromBuf b
+      = do x <- fromBuf r b
-           p <- fromBuf b
+           p <- fromBuf r b
            pure (x ** p)
 
 export
@@ -332,10 +352,10 @@ TTC a => TTC (Maybe a) where
      = do tag 1
           toBuf b val
 
-  fromBuf b
+  fromBuf r b
      = case !getTag of
             0 => pure Nothing
-            1 => do val <- fromBuf b
+            1 => do val <- fromBuf r b
                     pure (Just val)
             _ => corrupt "Maybe"
 
@@ -348,11 +368,11 @@ export
      = do tag 1
           toBuf b val
 
-  fromBuf b
+  fromBuf r b
      = case !getTag of
-            0 => do val <- fromBuf b
+            0 => do val <- fromBuf r b
                     pure (Left val)
-            1 => do val <- fromBuf b
+            1 => do val <- fromBuf r b
                     pure (Right val)
             _ => corrupt "Either"
 
@@ -362,14 +382,14 @@ TTC a => TTC (List a) where
       = do toBuf b (cast {to=Int} (length xs))
            traverse (toBuf b) xs
            pure ()
-  fromBuf b 
+  fromBuf r b 
-      = do len <- fromBuf b {a = Int}
+      = do len <- fromBuf r 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
+          = do val <- fromBuf r b
                readElems (val :: xs) k
 
 export
@@ -380,13 +400,13 @@ TTC a => TTC (Vect n a) where
       writeAll [] = pure ()
       writeAll (x :: xs) = do toBuf b x; writeAll xs
 
-  fromBuf {n} b = rewrite sym (plusZeroRightNeutral n) in readElems [] n
+  fromBuf {n} r 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
+          = do val <- fromBuf r b
                rewrite (plusSuccRightSucc k done)
                readElems (val :: xs) k
 
@@ -414,18 +434,18 @@ TTC Integer where
                  toBuf b (toLimbs (-val))
          else do toBuf b (the Bits8 1)
                  toBuf b (toLimbs val)
-  fromBuf b 
+  fromBuf r b 
-    = do val <- fromBuf b {a = Bits8}
+    = do val <- fromBuf r b {a = Bits8}
          case val of
-              0 => do val <- fromBuf b
+              0 => do val <- fromBuf r b
                       pure (-(fromLimbs val))
-              1 => do val <- fromBuf b
+              1 => do val <- fromBuf r b
                       pure (fromLimbs val)
               _ => corrupt "Integer"
 
 export
 TTC Nat where
   toBuf b val = toBuf b (cast {to=Integer} val)
-  fromBuf b 
+  fromBuf r b 
-     = do val <- fromBuf b
+     = do val <- fromBuf r b
           pure (fromInteger val)