From 72af040e7e9dc4eb396712f44d2a80376beebe67 Mon Sep 17 00:00:00 2001 From: Tim Engler Date: Mon, 9 Nov 2020 10:06:55 +0800 Subject: [PATCH] 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 --- src/Core/Context.idr | 5 ++++- src/TTImp/Interactive/CaseSplit.idr | 10 +++++++++- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 37b115dc0..6ff51c9f7 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -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 diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index c704bac99..303055cf9 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/src/TTImp/Interactive/CaseSplit.idr @@ -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