Strip current namespace when writing out defs

This saves writing the same strings over and over again in the body of a
definition. At the cost of a traversal on reading and writing the ttcs,
there is a good bit less to write out.

Author: edwinb

src/Compiler/Common.idr

@@ -110,9 +110,9 @@ execute {c} cg tm
 -- If an entry isn't already decoded, get the minimal entry we need for
 -- compilation, and record the Binary so that we can put it back when we're
 -- done (so that we don't obliterate the definition)
-getMinimalDef : ContextEntry -> Core (GlobalDef, Maybe Binary)
+getMinimalDef : ContextEntry -> Core (GlobalDef, Maybe (Namespace, Binary))
 getMinimalDef (Decoded def) = pure (def, Nothing)
-getMinimalDef (Coded bin)
+getMinimalDef (Coded ns bin)
     = do b <- newRef Bin bin
          cdef <- fromBuf b
          refsRList <- fromBuf b
@@ -125,12 +125,12 @@ getMinimalDef (Coded bin)
                            [] Public (MkTotality Unchecked IsCovering)
                            [] Nothing refsR False False True
                            None cdef Nothing []
-         pure (def, Just bin)
+         pure (def, Just (ns, bin))
 
 -- ||| Recursively get all calls in a function definition
 getAllDesc : {auto c : Ref Ctxt Defs} ->
              List Name -> -- calls to check
-             IOArray (Int, Maybe Binary) ->
+             IOArray (Int, Maybe (Namespace, Binary)) ->
                             -- which nodes have been visited. If the entry is
                             -- present, it's visited. Keep the binary entry, if
                             -- we partially decoded it, so that we can put back
@@ -174,10 +174,10 @@ getNamedDef n
                                             pure (Just (n, location def, d))
 
 replaceEntry : {auto c : Ref Ctxt Defs} ->
-               (Int, Maybe Binary) -> Core ()
+               (Int, Maybe (Namespace, Binary)) -> Core ()
 replaceEntry (i, Nothing) = pure ()
-replaceEntry (i, Just b)
-    = ignore $ addContextEntry (Resolved i) b
+replaceEntry (i, Just (ns, b))
+    = ignore $ addContextEntry ns (Resolved i) b
 
 natHackNames : List Name
 natHackNames

src/Core/Binary.idr

@@ -251,13 +251,13 @@ getSaveDefs modns (n :: ns) acc defs
          case definition gdef of
               Builtin _ => getSaveDefs modns ns acc defs
               _ => do bin <- initBinaryS 16384
-                      toBuf bin !(full (gamma defs) gdef)
+                      toBuf bin (trimNS modns !(full (gamma defs) gdef))
                       b <- get Bin
-                      getSaveDefs modns ns ((trimNS (fullname gdef), b) :: acc) defs
+                      getSaveDefs modns ns ((trimName (fullname gdef), b) :: acc) defs
   where
-    trimNS : Name -> Name
-    trimNS n@(NS defns d) = if defns == modns then d else n
-    trimNS n = n
+    trimName : Name -> Name
+    trimName n@(NS defns d) = if defns == modns then d else n
+    trimName n = n
 
 -- Write out the things in the context which have been defined in the
 -- current source file
@@ -295,9 +295,10 @@ writeToTTC extradata fname
          pure ()
 
 addGlobalDef : {auto c : Ref Ctxt Defs} ->
-               (modns : ModuleIdent) -> (importAs : Maybe Namespace) ->
+               (modns : ModuleIdent) -> Namespace ->
+               (importAs : Maybe Namespace) ->
                (Name, Binary) -> Core ()
-addGlobalDef modns asm (n, def)
+addGlobalDef modns filens asm (n, def)
     = do defs <- get Ctxt
          codedentry <- lookupContextEntry n (gamma defs)
          -- Don't update the coded entry because some names might not be
@@ -307,7 +308,7 @@ addGlobalDef modns asm (n, def)
                                    pure (Just x))
                         codedentry
          unless (completeDef entry) $
-           ignore $ addContextEntry n def
+           ignore $ addContextEntry filens n def
 
          whenJust asm $ \ as => addContextAlias (asName modns as n) n
 
@@ -450,7 +451,7 @@ readFromTTC nestedns loc reexp fname modNS importAs
             else do
                ttc <- readTTCFile True fname as bin
                let ex = extraData ttc
-               traverse_ (addGlobalDef modNS as) (context ttc)
+               traverse_ (addGlobalDef modNS (currentNS ttc) as) (context ttc)
                traverse_ addUserHole (userHoles ttc)
                setNS (currentNS ttc)
                when nestedns $ setNestedNS (nestedNS ttc)

src/Core/CaseTree.idr

@@ -50,6 +50,32 @@ isDefault : CaseAlt vars -> Bool
 isDefault (DefaultCase _) = True
 isDefault _ = False
 
+mutual
+  export
+  StripNamespace (CaseTree vars) where
+    trimNS ns (Case idx p scTy xs)
+        = Case idx p (trimNS ns scTy) (map (trimNS ns) xs)
+    trimNS ns (STerm x t) = STerm x (trimNS ns t)
+    trimNS ns c = c
+
+    restoreNS ns (Case idx p scTy xs)
+        = Case idx p (restoreNS ns scTy) (map (restoreNS ns) xs)
+    restoreNS ns (STerm x t) = STerm x (restoreNS ns t)
+    restoreNS ns c = c
+
+  export
+  StripNamespace (CaseAlt vars) where
+    trimNS ns (ConCase x tag args t) = ConCase x tag args (trimNS ns t)
+    trimNS ns (DelayCase ty arg t) = DelayCase ty arg (trimNS ns t)
+    trimNS ns (ConstCase x t) = ConstCase x (trimNS ns t)
+    trimNS ns (DefaultCase t) = DefaultCase (trimNS ns t)
+
+    restoreNS ns (ConCase x tag args t) = ConCase x tag args (restoreNS ns t)
+    restoreNS ns (DelayCase ty arg t) = DelayCase ty arg (restoreNS ns t)
+    restoreNS ns (ConstCase x t) = ConstCase x (restoreNS ns t)
+    restoreNS ns (DefaultCase t) = DefaultCase (restoreNS ns t)
+
+
 public export
 data Pat : Type where
      PAs : FC -> Name -> Pat -> Pat

src/Core/Context.idr

@@ -311,7 +311,8 @@ data Arr : Type where
 -- binary blob yet, so decode it first time
 public export
 data ContextEntry : Type where
-     Coded : Binary -> ContextEntry
+     Coded : Namespace -> -- namespace for decoding into, with restoreNS
+             Binary -> ContextEntry
      Decoded : GlobalDef -> ContextEntry
 
 data PossibleName : Type where
@@ -791,7 +792,6 @@ HasNames (Term vars) where
 
 export
 HasNames Pat where
-
   full gam (PAs fc n p)
      = [| PAs (pure fc) (full gam n) (full gam p) |]
   full gam (PCon fc n i ar ps)
@@ -918,6 +918,31 @@ HasNames Def where
       = pure $ Guess !(resolved gam tm) b cs
   resolved gam t = pure t
 
+export
+StripNamespace Def where
+  trimNS ns (PMDef i args ct rt pats)
+      = PMDef i args (trimNS ns ct) rt (map trimNSpat pats)
+    where
+      trimNSpat : (vs ** (Env Term vs, Term vs, Term vs)) ->
+                  (vs ** (Env Term vs, Term vs, Term vs))
+      trimNSpat (vs ** (env, lhs, rhs))
+          = (vs ** (env, trimNS ns lhs, trimNS ns rhs))
+  trimNS ns d = d
+
+  restoreNS ns (PMDef i args ct rt pats)
+      = PMDef i args (restoreNS ns ct) rt (map restoreNSpat pats)
+    where
+      restoreNSpat : (vs ** (Env Term vs, Term vs, Term vs)) ->
+                  (vs ** (Env Term vs, Term vs, Term vs))
+      restoreNSpat (vs ** (env, lhs, rhs))
+          = (vs ** (env, restoreNS ns lhs, restoreNS ns rhs))
+  restoreNS ns d = d
+
+export
+StripNamespace GlobalDef where
+  trimNS ns def = record { definition $= trimNS ns } def
+  restoreNS ns def = record { definition $= restoreNS ns } def
+
 HasNames (NameMap a) where
   full gam nmap
       = insertAll empty (toList nmap)
@@ -1294,10 +1319,10 @@ addDef n def
 
 export
 addContextEntry : {auto c : Ref Ctxt Defs} ->
-                  Name -> Binary -> Core Int
-addContextEntry n def
+                  Namespace -> Name -> Binary -> Core Int
+addContextEntry ns n def
     = do defs <- get Ctxt
-         (idx, gam') <- addEntry n (Coded def) (gamma defs)
+         (idx, gam') <- addEntry n (Coded ns def) (gamma defs)
          put Ctxt (record { gamma = gam' } defs)
          pure idx
 

src/Core/TT.idr

@@ -743,6 +743,56 @@ data Term : List Name -> Type where
               Term vars
      TType : FC -> Term vars
 
+-- Remove/restore the given namespace from all Refs. This is to allow
+-- writing terms and case trees to disk without repeating the same namespace
+-- all over the place.
+public export
+interface StripNamespace a where
+  trimNS : Namespace -> a -> a
+  restoreNS : Namespace -> a -> a
+
+export
+StripNamespace (Term vars) where
+  trimNS ns tm@(Ref fc x (NS tns n))
+      = if ns == tns then Ref fc x (NS (unsafeFoldNamespace []) n) else tm
+        -- ^ A blank namespace, rather than a UN, so we don't catch primitive 
+        -- names which are represented as UN.
+  trimNS ns (Meta fc x y xs)
+      = Meta fc x y (map (trimNS ns) xs)
+  trimNS ns (Bind fc x b scope)
+      = Bind fc x (map (trimNS ns) b) (trimNS ns scope)
+  trimNS ns (App fc fn arg)
+      = App fc (trimNS ns fn) (trimNS ns arg)
+  trimNS ns (As fc s p tm)
+      = As fc s (trimNS ns p) (trimNS ns tm)
+  trimNS ns (TDelayed fc x y)
+      = TDelayed fc x (trimNS ns y)
+  trimNS ns (TDelay fc x t y)
+      = TDelay fc x (trimNS ns t) (trimNS ns y)
+  trimNS ns (TForce fc r y)
+      = TForce fc r (trimNS ns y)
+  trimNS ns tm = tm
+
+  restoreNS ns tm@(Ref fc x (NS tmns n))
+      = if isNil (unsafeUnfoldNamespace tmns)
+            then Ref fc x (NS ns n)
+            else tm
+  restoreNS ns (Meta fc x y xs)
+      = Meta fc x y (map (restoreNS ns) xs)
+  restoreNS ns (Bind fc x b scope)
+      = Bind fc x (map (restoreNS ns) b) (restoreNS ns scope)
+  restoreNS ns (App fc fn arg)
+      = App fc (restoreNS ns fn) (restoreNS ns arg)
+  restoreNS ns (As fc s p tm)
+      = As fc s (restoreNS ns p) (restoreNS ns tm)
+  restoreNS ns (TDelayed fc x y)
+      = TDelayed fc x (restoreNS ns y)
+  restoreNS ns (TDelay fc x t y)
+      = TDelay fc x (restoreNS ns t) (restoreNS ns y)
+  restoreNS ns (TForce fc r y)
+      = TForce fc r (restoreNS ns y)
+  restoreNS ns tm = tm
+
 export
 isErased : Term vars -> Bool
 isErased (Erased _ _) = True

src/Core/TTC.idr

@@ -1079,12 +1079,12 @@ TTC Transform where
            pure (MkTransform {vars} n env lhs rhs)
 
 -- decode : Context -> Int -> (update : Bool) -> ContextEntry -> Core GlobalDef
-Core.Context.decode gam idx update (Coded bin)
+Core.Context.decode gam idx update (Coded ns bin)
     = do b <- newRef Bin bin
          def <- fromBuf b
          let a = getContent gam
          arr <- get Arr
-         def' <- resolved gam def
+         def' <- resolved gam (restoreNS ns def)
          when update $ coreLift $ writeArray arr idx (Decoded def')
          pure def'
 Core.Context.decode gam idx update (Decoded def) = pure def