From b310e28fdf583cb8b286356def971b8f5695f6fc Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sat, 21 Mar 2020 14:27:03 +0000
Subject: [PATCH] Fix for resolved names

When we're checking if a definition is a hole and needs updating, when
loading ttc, the names might not fully resolved yet, so don't decode the
definition.
---
 src/Core/Binary.idr  |  8 +++++++-
 src/Core/Context.idr | 26 +++++++++++++++++++++-----
 src/Core/TTC.idr     |  8 ++++----
 3 files changed, 32 insertions(+), 10 deletions(-)

diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr
index b509a29..b0c403c 100644
--- a/src/Core/Binary.idr
+++ b/src/Core/Binary.idr
@@ -293,7 +293,13 @@ addGlobalDef : {auto c : Ref Ctxt Defs} ->
                (Name, Binary) -> Core ()
 addGlobalDef modns as (n, def)
     = do defs <- get Ctxt
-         entry <- lookupCtxtExact n (gamma defs)
+         codedentry <- lookupContextEntry n (gamma defs)
+         -- Don't update the coded entry because some names might not be
+         -- resolved yet
+         entry <- maybe (pure Nothing)
+                        (\ (i, d) => do x <- decode (gamma defs) i False d
+                                        pure (Just x))
+                        codedentry
          if completeDef entry
             then pure ()
             else do addContextEntry (asName modns as n) def
diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index d4d15c3..a578952 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -250,7 +250,7 @@ getContent = content
 -- Implemented later, once we can convert to and from full names
 -- Defined in Core.TTC
 export
-decode : Context -> Int -> ContextEntry -> Core GlobalDef
+decode : Context -> Int -> (update : Bool) -> ContextEntry -> Core GlobalDef
 
 initSize : Int
 initSize = 10000
@@ -352,13 +352,13 @@ lookupCtxtExactI : Name -> Context -> Core (Maybe (Int, GlobalDef))
 lookupCtxtExactI (Resolved idx) ctxt
     = case lookup idx (staging ctxt) of
            Just val =>
-                 pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx val)
+                 pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx True val)
            Nothing =>
               do let a = content ctxt
                  arr <- get Arr
                  Just def <- coreLift (readArray arr idx)
                       | Nothing => pure Nothing
-                 pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx def)
+                 pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx True def)
 lookupCtxtExactI n ctxt
     = do let Just idx = lookup n (resolvedAs ctxt)
                   | Nothing => pure Nothing
@@ -369,7 +369,7 @@ lookupCtxtExact : Name -> Context -> Core (Maybe GlobalDef)
 lookupCtxtExact (Resolved idx) ctxt
     = case lookup idx (staging ctxt) of
            Just res =>
-                do def <- decode ctxt idx res
+                do def <- decode ctxt idx True res
                    case returnDef (inlineOnly ctxt) idx def of
                         Nothing => pure Nothing
                         Just (_, def) => pure (Just def)
@@ -378,7 +378,7 @@ lookupCtxtExact (Resolved idx) ctxt
                  arr <- get Arr
                  Just res <- coreLift (readArray arr idx)
                       | Nothing => pure Nothing
-                 def <- decode ctxt idx res
+                 def <- decode ctxt idx True res
                  case returnDef (inlineOnly ctxt) idx def of
                       Nothing => pure Nothing
                       Just (_, def) => pure (Just def)
@@ -387,6 +387,22 @@ lookupCtxtExact n ctxt
               | Nothing => pure Nothing
          pure (Just def)
 
+export
+lookupContextEntry : Name -> Context -> Core (Maybe (Int, ContextEntry))
+lookupContextEntry (Resolved idx) ctxt
+    = case lookup idx (staging ctxt) of
+           Just res => pure (Just (idx, res))
+           Nothing =>
+              do let a = content ctxt
+                 arr <- get Arr
+                 Just res <- coreLift (readArray arr idx)
+                      | Nothing => pure Nothing
+                 pure (Just (idx, res))
+lookupContextEntry n ctxt
+    = do let Just idx = lookup n (resolvedAs ctxt)
+                  | Nothing => pure Nothing
+         lookupContextEntry (Resolved idx) ctxt
+
 export
 lookupCtxtName : Name -> Context -> Core (List (Name, Int, GlobalDef))
 lookupCtxtName n ctxt
diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr
index c851613..10eef50 100644
--- a/src/Core/TTC.idr
+++ b/src/Core/TTC.idr
@@ -943,14 +943,14 @@ TTC Transform where
            rhs <- fromBuf b
            pure (MkTransform {vars} env lhs rhs)
 
--- decode : Context -> Int -> ContextEntry -> Core GlobalDef
-Core.Context.decode gam idx (Coded bin)
+-- decode : Context -> Int -> (update : Bool) -> ContextEntry -> Core GlobalDef
+Core.Context.decode gam idx update (Coded bin)
     = do b <- newRef Bin bin
          def <- fromBuf b
          let a = getContent gam
          arr <- get Arr
          def' <- resolved gam def
-         coreLift $ writeArray arr idx (Decoded def')
+         when update $ coreLift $ writeArray arr idx (Decoded def')
          pure def'
-Core.Context.decode gam idx (Decoded def) = pure def
+Core.Context.decode gam idx update (Decoded def) = pure def