idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-01 09:49:24 +03:00
Code Issues Projects Releases Wiki Activity

Fixes Issue #74. The problem is that if the function is defined in a sub

Browse Source 
module, then the current namespace (accessed by calling getNS) differs
from the function namespace, therefore it is not considered visible by
TTImp.Elab.App.checkVisibleNS
This commit is contained in:
Tim Engler 2020-11-09 10:06:55 +08:00 committed by G. Allais
parent 52ba8b00a6
commit 72af040e7e
2 changed files with 13 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/Core/Context.idr
View File

@ -336,8 +336,11 @@ record Context where
-- access in a program - in all other cases, we'll assume everything is
-- visible
visibleNS : List Namespace
allPublic : Bool -- treat everything as public. This is only intended
allPublic : Bool -- treat everything as public. This is intended
-- for checking partially evaluated definitions
-- or for use outside of the main compilation
-- process (e.g. when implementing interactive
-- features such as case splitting).
inlineOnly : Bool -- only return things with the 'alwaysReduce' flag
hidden : NameMap () -- Never return these

10
src/TTImp/Interactive/CaseSplit.idr
View File

@ -318,13 +318,21 @@ mkCase {c} {u} fn orig lhs_raw
defs <- get Ctxt
ust <- get UST
catch
(do -- Use 'Rig0' since it might be a type level function, or it might
(do
-- Fixes Issue #74. The problem is that if the function is defined in a sub module,
-- then the current namespace (accessed by calling getNS) differs from the function
-- namespace, therefore it is not considered visible by TTImp.Elab.App.checkVisibleNS
setAllPublic True
-- Use 'Rig0' since it might be a type level function, or it might
-- be an erased name in a case block (which will be bound elsewhere
-- once split and turned into a pattern)
(lhs, _) <- elabTerm {c} {m} {u}
fn (InLHS erased) [] (MkNested [])
[] (IBindHere (getFC lhs_raw) PATTERN lhs_raw)
Nothing
-- Revert all public back to false
setAllPublic False
put Ctxt defs -- reset the context, we don't want any updates
put UST ust
lhs' <- unelabNoSugar [] lhs