idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-27 21:55:19 +03:00
Code Issues Projects Releases Wiki Activity

Better implementation of %hide

Browse Source 
Instead of setting the name as private, make sure it doesn't appear in
lookups at all. That is, truly hide it!
This commit is contained in:
Edwin Brady 2020-07-04 21:38:35 +01:00
parent c1ed3c2fc8
commit f60ae32242
1 changed files with 22 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
src/Core/Context.idr
View File

@ -333,6 +333,7 @@ record Context where
allPublic : Bool -- treat everything as public. This is only intended
-- for checking partially evaluated definitions
inlineOnly : Bool -- only return things with the 'alwaysReduce' flag
hidden : NameMap () -- Never return these
export
getContent : Context -> Ref Arr (IOArray ContextEntry)
@ -354,7 +355,7 @@ initCtxtS : Int -> Core Context
initCtxtS s
= do arr <- coreLift $ newArray s
aref <- newRef Arr arr
pure (MkContext 0 0 empty empty aref 0 empty [["_PE"]] False False)
pure (MkContext 0 0 empty empty aref 0 empty [["_PE"]] False False empty)
export
initCtxt : Core Context
@ -534,17 +535,26 @@ lookupCtxtName n ctxt
Core (List (Name, Int, GlobalDef))
lookupPossibles acc [] = pure (reverse acc)
lookupPossibles acc (Direct fulln i :: ps)
= do Just res <- lookupCtxtExact (Resolved i) ctxt
| Nothing => lookupPossibles acc ps
if (matches n fulln) && not (i `elem` map resn acc)
then lookupPossibles ((fulln, i, res) :: acc) ps
else lookupPossibles acc ps
= case lookup fulln (hidden ctxt) of
Nothing =>
do Just res <- lookupCtxtExact (Resolved i) ctxt
| Nothing => lookupPossibles acc ps
if matches n fulln && not (i `elem` map resn acc)
then lookupPossibles ((fulln, i, res) :: acc) ps
else lookupPossibles acc ps
_ => lookupPossibles acc ps
lookupPossibles acc (Alias asn fulln i :: ps)
= do Just res <- lookupCtxtExact (Resolved i) ctxt
| Nothing => lookupPossibles acc ps
if (matches n asn) && not (i `elem` map resn acc)
then lookupPossibles ((fulln, i, res) :: acc) ps
else lookupPossibles acc ps
= case lookup fulln (hidden ctxt) of
Nothing =>
do Just res <- lookupCtxtExact (Resolved i) ctxt
| Nothing => lookupPossibles acc ps
if (matches n asn) && not (i `elem` map resn acc)
then lookupPossibles ((fulln, i, res) :: acc) ps
else lookupPossibles acc ps
_ => lookupPossibles acc ps
hideName : Name -> Context -> Context
hideName n ctxt = record { hidden $= insert n () } ctxt
branchCtxt : Context -> Core Context
branchCtxt ctxt = pure (record { branchDepth $= S } ctxt)
@ -1413,7 +1423,7 @@ hide fc n
[(nsn, _)] <- lookupCtxtName n (gamma defs)
| [] => throw (UndefinedName fc n)
| res => throw (AmbiguousName fc (map fst res))
setVisibility fc nsn Private
put Ctxt (record { gamma $= hideName nsn } defs)
export
getVisibility : {auto c : Ref Ctxt Defs} ->