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

src/Idris/Core/Binary.hs+3

compare with master

unifiedsplit

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

188 put ns

189 put (RunningElabScript e) = do putWord8 42

190 put e

191+ put (ElabScriptStaging n) = do putWord8 43

192+ put n

191

193

192 get = do i <- getWord8

194 get = do i <- getWord8

193 case i of

195 case i of

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

259 return $ UnknownImplicit x y

261 return $ UnknownImplicit x y

260 41 -> fmap NoValidAlts get

262 41 -> fmap NoValidAlts get

261 42 -> fmap RunningElabScript get

263 42 -> fmap RunningElabScript get

264+ 43 -> fmap ElabScriptStaging get

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

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

263----- Generated by 'derive'

266----- Generated by 'derive'

264

267

src/Idris/Core/DeepSeq.hs+1

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

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

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

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

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

157

158

158instance NFData ErrorReportPart where

159instance NFData ErrorReportPart where

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

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

src/Idris/Core/TT.hs+1

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

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

294 | ElabScriptStuck t

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

296+ | ElabScriptStaging Name

296 deriving (Eq, Functor, Data, Typeable)

297 deriving (Eq, Functor, Data, Typeable)

297

298

298type Err = Err' Term

299type Err = Err' Term

src/Idris/Delaborate.hs+4

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

503 text "Is it a stuck term?"

504pprintErr' i (RunningElabScript e) =

505 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

506

510

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

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

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

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

src/Idris/Elab/Term.hs+15

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

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

29import Control.Monad

30import Control.Monad.State.Strict

31+import Data.Foldable (for_)

31import Data.List

32import Data.List

32import qualified Data.Map as M

33import qualified Data.Map as M

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

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

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

1245 attack -- to get an extra hole

1246 attack -- to get an extra hole

1246 elab' ina (Just fc') tm

1247 elab' ina (Just fc') tm

1247 script <- get_guess

1248 script <- get_guess

1249+ fullyElaborated script

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

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

1249 env <- get_env

1251 env <- get_env

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

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

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

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

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

1361 getFC d x = d

1363 getFC d x = d

1362

1364

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+

1363 insertLazy :: PTerm -> ElabD PTerm

1378 insertLazy :: PTerm -> ElabD PTerm

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

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

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

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

src/Idris/IBC.hs+1−1

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 121

43+ibcVersion = 122

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,