edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-24 04:43:25 +03:00
Code Issues Projects Releases Wiki Activity

Fix for resolved names

Browse Source 
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.
This commit is contained in:
Edwin Brady 2020-03-21 14:27:03 +00:00
parent aaf6868bc7
commit b310e28fdf
3 changed files with 32 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/Core/Binary.idr
View File

@ -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

26
src/Core/Context.idr
View File

@ -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

8
src/Core/TTC.idr
View File

@ -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