git.iko.soy/Idris-dev
on master help sign in
Error when using empty namespace for disambiguation at REPL

Fixes #1497.

commitce7dff963edfe6988417c3ad542fedd5605384c7 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 30 Aug 2014, 20:37 (12 years ago) parent8fadb31
3 files changed+81−1
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/Error.hs+76 src/Idris/REPL.hs+1
src/Idris/AbsSyntaxTree.hs+4−1
@@ -30,6 +30,8 @@ import Data.Either
3030import qualified Data.Set as S
3131import Data.Word (Word)
3232import Data.Maybe (fromMaybe)
33+import Data.Traversable (Traversable)
34+import Data.Foldable (Foldable)
3335
3436import Debug.Trace
3537
@@ -792,7 +794,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
792794 | Skip
793795 | TFail [ErrorReportPart]
794796 | Qed | Abandon
795− deriving (Show, Eq, Functor)
797+ deriving (Show, Eq, Functor, Foldable, Traversable)
796798{-!
797799deriving instance Binary PTactic'
798800deriving instance NFData PTactic'
@@ -1820,3 +1822,4 @@ getErasureInfo ist n =
18201822 case lookupCtxtExact n (idris_optimisation ist) of
18211823 Just (Optimise inacc detagg) -> map fst inacc
18221824 Nothing -> []
1825+
src/Idris/Error.hs+76
@@ -7,17 +7,24 @@ import Idris.AbsSyntax
77import Idris.Delaborate
88import Idris.Output
99
10+import Idris.Core.Evaluate (ctxtAlist)
1011import Idris.Core.TT
1112import Idris.Core.Typecheck
1213import Idris.Core.Constraints
14+import Idris.Output
1315
1416import System.Console.Haskeline
1517import System.Console.Haskeline.MonadException
18+import Control.Monad (when)
1619import Control.Monad.State.Strict
1720import Control.Monad.Error (throwError, catchError)
1821import System.IO.Error(isUserError, ioeGetErrorString)
1922import Data.Char
23+import Data.List (intercalate, isPrefixOf)
24+import qualified Data.Text as T
2025import Data.Typeable
26+import qualified Data.Traversable as Traversable
27+import qualified Data.Foldable as Foldable
2128
2229iucheck :: Idris ()
2330iucheck = do tit <- typeInType
@@ -70,3 +77,72 @@ tctry tc1 tc2
7077getErrSpan :: Err -> FC
7178getErrSpan (At fc _) = fc
7279getErrSpan _ = emptyFC
80+
81+--------------------------------------------------------------------
82+-- Specific warnings not included in elaborator
83+--------------------------------------------------------------------
84+-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent
85+warnDisamb :: IState -> PTerm -> Idris ()
86+warnDisamb ist (PQuote _) = return ()
87+warnDisamb ist (PRef _ _) = return ()
88+warnDisamb ist (PInferRef _ _) = return ()
89+warnDisamb ist (PPatvar _ _) = return ()
90+warnDisamb ist (PLam _ t b) = warnDisamb ist t >> warnDisamb ist b
91+warnDisamb ist (PPi _ _ t b) = warnDisamb ist t >> warnDisamb ist b
92+warnDisamb ist (PLet _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b
93+warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t
94+warnDisamb ist (PApp _ t args) = warnDisamb ist t >>
95+ mapM_ (warnDisamb ist . getTm) args
96+warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>
97+ mapM_ (warnDisamb ist . getTm) args
98+warnDisamb ist (PMatchApp _ _) = return ()
99+warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>
100+ mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases
101+warnDisamb ist (PTrue _ _) = return ()
102+warnDisamb ist (PFalse _) = return ()
103+warnDisamb ist (PRefl _ tm) = warnDisamb ist tm
104+warnDisamb ist (PResolveTC _) = return ()
105+warnDisamb ist (PEq _ a b x y) = warnDisamb ist a >> warnDisamb ist b >>
106+ warnDisamb ist x >> warnDisamb ist y
107+warnDisamb ist (PRewrite _ x y z) = warnDisamb ist x >> warnDisamb ist y >>
108+ Foldable.mapM_ (warnDisamb ist) z
109+warnDisamb ist (PPair _ _ x y) = warnDisamb ist x >> warnDisamb ist y
110+warnDisamb ist (PDPair _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z
111+warnDisamb ist (PAlternative _ tms) = mapM_ (warnDisamb ist) tms
112+warnDisamb ist (PHidden tm) = warnDisamb ist tm
113+warnDisamb ist PType = return ()
114+warnDisamb ist (PUniverse _) = return ()
115+warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y
116+warnDisamb ist (PConstant _) = return ()
117+warnDisamb ist Placeholder = return ()
118+warnDisamb ist (PDoBlock steps) = mapM_ wStep steps
119+ where wStep (DoExp _ x) = warnDisamb ist x
120+ wStep (DoBind _ _ x) = warnDisamb ist x
121+ wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>
122+ mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cs
123+ wStep (DoLet _ _ x y) = warnDisamb ist x >> warnDisamb ist y
124+ wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y
125+warnDisamb ist (PIdiom _ x) = warnDisamb ist x
126+warnDisamb ist (PReturn _) = return ()
127+warnDisamb ist (PMetavar _) = return ()
128+warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
129+warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs
130+warnDisamb ist (PElabError _) = return ()
131+warnDisamb ist PImpossible = return ()
132+warnDisamb ist (PCoerced tm) = warnDisamb ist tm
133+warnDisamb ist (PDisamb ds tm) = warnDisamb ist tm >>
134+ mapM_ warnEmpty ds
135+ where warnEmpty d =
136+ when (null (filter (isIn d . fst) (ctxtAlist (tt_ctxt ist)))) $
137+ ierror . Msg $
138+ "Nothing found in namespace \"" ++
139+ intercalate "." (map T.unpack d) ++
140+ "\"."
141+ isIn d (NS _ ns) = isPrefixOf d ns
142+ isIn d _ = False
143+
144+warnDisamb ist (PUnifyLog tm) = warnDisamb ist tm
145+warnDisamb ist (PNoImplicits tm) = warnDisamb ist tm
146+warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>
147+ Foldable.mapM_ (warnDisamb ist) goal
148+warnDisamb ist (PUnquote tm) = warnDisamb ist tm
src/Idris/REPL.hs+1
@@ -689,6 +689,7 @@ process fn (ChangeDirectory f)
689689 return ()
690690process fn (Eval t)
691691 = withErrorReflection $ do logLvl 5 $ show t
692+ getIState >>= flip warnDisamb t
692693 (tm, ty) <- elabVal recinfo ERHS t
693694 ctxt <- getContext
694695 let tm' = force (normaliseAll ctxt [] tm)