32ce95f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better error on staging problem for Elab scripts

Now, Elab scripts are pre-analyzed to see if they contain unelaborated case splits. If so, they are not executed, and a suggestion is made as to how to fix it.

commit32ce95ff805a796edffbf047ddf4e71aa1c74c96 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 8 Oct 2015, 22:50 (11 years ago) parentd244c04

6 files changed+25−1

compare with master

unifiedsplit

src/Idris/Core/Binary.hs+3 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+4 src/Idris/Elab/Term.hs+15 src/Idris/IBC.hs+1−1

src/Idris/Core/Binary.hs+3

@@ -188,6 +188,8 @@ instance Binary a => Binary (Err' a) where

188188 put ns

189189 put (RunningElabScript e) = do putWord8 42

190190 put e

191+ put (ElabScriptStaging n) = do putWord8 43

192+ put n

191193

192194 get = do i <- getWord8

193195 case i of

@@ -259,6 +261,7 @@ instance Binary a => Binary (Err' a) where

259261 return $ UnknownImplicit x y

260262 41 -> fmap NoValidAlts get

261263 42 -> fmap RunningElabScript get

264+ 43 -> fmap ElabScriptStaging get

262265 _ -> error "Corrupted binary data for Err'"

263266----- Generated by 'derive'

264267

src/Idris/Core/DeepSeq.hs+1

@@ -154,6 +154,7 @@ instance NFData Err where

154154 rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

155155 rnf (ElabScriptStuck x1) = rnf x1 `seq` ()

156156 rnf (RunningElabScript x1) = rnf x1 `seq` ()

157+ rnf (ElabScriptStaging x1) = rnf x1 `seq` ()

157158

158159instance NFData ErrorReportPart where

159160 rnf (TextPart x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs+1

@@ -293,6 +293,7 @@ data Err' t

293293 -- ^ User-specified message, proof term, goals with context (first goal is focused)

294294 | ElabScriptStuck t

295295 | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script

296+ | ElabScriptStaging Name

296297 deriving (Eq, Functor, Data, Typeable)

297298

298299type Err = Err' Term

src/Idris/Delaborate.hs+4

@@ -503,6 +503,10 @@ pprintErr' i (ElabScriptStuck tm) =

503503 text "Is it a stuck term?"

504504pprintErr' i (RunningElabScript e) =

505505 text "While running an elaboration script, the following error occurred" <> colon <$> pprintErr' i e

506+pprintErr' i (ElabScriptStaging n) =

507+ text "Can't run elaboration script because it contains pattern matching that has not yet been elaborated." <$>

508+ text "Try lifting the script to a top-level definition." <$>

509+ text "In particular, the problem is caused by:" <+> annName n

506510

507511showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation

508512showPart ist (TextPart str) = fillSep . map text . words $ str

src/Idris/Elab/Term.hs+15

@@ -28,6 +28,7 @@ import qualified Util.Pretty as U

2828import Control.Applicative ((<$>))

2929import Control.Monad

3030import Control.Monad.State.Strict

31+import Data.Foldable (for_)

3132import Data.List

3233import qualified Data.Map as M

3334import Data.Maybe (mapMaybe, fromMaybe, catMaybes)

@@ -1245,6 +1246,7 @@ elab ist info emode opts fn tm

12451246 attack -- to get an extra hole

12461247 elab' ina (Just fc') tm

12471248 script <- get_guess

1249+ fullyElaborated script

12481250 solve -- eliminate the hole. Becuase there are no references, the script is only in the binding

12491251 env <- get_env

12501252 runElabAction ist (maybe fc' id fc) env script ns

@@ -1360,6 +1362,19 @@ elab ist info emode opts fn tm

13601362 getFC d (PAlternative _ _ (x:_)) = getFC d x

13611363 getFC d x = d

13621364

1365+ -- Fail if a term is not yet fully elaborated (e.g. if it contains

1366+ -- case block functions that don't yet exist)

1367+ fullyElaborated :: Term -> ElabD ()

1368+ fullyElaborated (P _ n _) =

1369+ do EState cases _ _ _ <- getAux

1370+ case lookup n cases of

1371+ Nothing -> return ()

1372+ Just _ -> lift . tfail $ ElabScriptStaging n

1373+ fullyElaborated (Bind n b body) = fullyElaborated body >> for_ b fullyElaborated

1374+ fullyElaborated (App _ l r) = fullyElaborated l >> fullyElaborated r

1375+ fullyElaborated (Proj t _) = fullyElaborated t

1376+ fullyElaborated _ = return ()

1377+

13631378 insertLazy :: PTerm -> ElabD PTerm

13641379 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

13651380 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 121

43+ibcVersion = 122

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,