02d0078 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add beginning of elaborator debugging errors

commit02d007871ae62978a5a3343ed13825319cc0cd5c authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 9 Mar 2015, 21:01 (12 years ago) parente39a9a2

5 files changed+16−1

compare with master

unifiedsplit

src/Idris/Core/Binary.hs+8 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/Elaborate.hs+4 src/Idris/Core/TT.hs+2 src/Idris/IBC.hs+1−1

src/Idris/Core/Binary.hs+8

@@ -122,6 +122,10 @@ instance Binary a => Binary (Err' a) where

122122 put t

123123 put (CantMatch t) = do putWord8 35

124124 put t

125+ put (ElabDebug x1 x2 x3) = do putWord8 36

126+ put x1

127+ put x2

128+ put x3

125129

126130 get = do i <- getWord8

127131 case i of

@@ -177,6 +181,10 @@ instance Binary a => Binary (Err' a) where

177181 return $ ReflectionFailed x y

178182 34 -> fmap WithFnType get

179183 35 -> fmap CantMatch get

184+ 36 -> do x1 <- get

185+ x2 <- get

186+ x3 <- get

187+ return (ElabDebug x1 x2 x3)

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

181189----- Generated by 'derive'

182190

src/Idris/Core/DeepSeq.hs+1

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

8888 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

8989 rnf (ProviderError x1) = rnf x1 `seq` ()

9090 rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

91+ rnf (ElabDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

9192

9293instance NFData ImplicitInfo where

9394 rnf (Impl x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+4

@@ -839,6 +839,10 @@ prunStateT pmax zok ps x s

839839 else OK ((v, newpmax, problems p), s')

840840 Error e -> Error e

841841

842+debugElaborator :: Maybe String -> Elab' aux a

843+debugElaborator msg = do ps <- fmap proof get

844+ lift . Error $ ElabDebug msg (getProofTerm (pterm ps)) [] -- TODO hole info

845+

842846qshow :: Fails -> String

843847qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)

844848

src/Idris/Core/TT.hs+2

@@ -162,6 +162,8 @@ data Err' t

162162 | LoadingFailed String (Err' t)

163163 | ReflectionError [[ErrorReportPart]] (Err' t)

164164 | ReflectionFailed String (Err' t)

165+ | ElabDebug (Maybe String) t [(Name, t, [(Name, Binder t)])]

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

165167 deriving (Eq, Functor, Data, Typeable)

166168

167169type Err = Err' Term

src/Idris/IBC.hs+1−1

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 98

40+ibcVersion = 99

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,