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

src/Idris/Core/Binary.hs+8

compare with master

unifiedsplit

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

122 put t

123 put (CantMatch t) = do putWord8 35

124 put t

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

126+ put x1

127+ put x2

128+ put x3

125

129

126 get = do i <- getWord8

130 get = do i <- getWord8

127 case i of

131 case i of

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

177 return $ ReflectionFailed x y

181 return $ ReflectionFailed x y

178 34 -> fmap WithFnType get

182 34 -> fmap WithFnType get

179 35 -> fmap CantMatch get

183 35 -> fmap CantMatch get

184+ 36 -> do x1 <- get

185+ x2 <- get

186+ x3 <- get

187+ return (ElabDebug x1 x2 x3)

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

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

181----- Generated by 'derive'

189----- Generated by 'derive'

182

190

src/Idris/Core/DeepSeq.hs+1

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

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

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

90 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` ()

91

92

92instance NFData ImplicitInfo where

93instance NFData ImplicitInfo where

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

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

src/Idris/Core/Elaborate.hs+4

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

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

840 Error e -> Error e

841

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+

842qshow :: Fails -> String

846qshow :: Fails -> String

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

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

844

848

src/Idris/Core/TT.hs+2

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

162 | LoadingFailed String (Err' t)

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

164 | 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)

165 deriving (Eq, Functor, Data, Typeable)

167 deriving (Eq, Functor, Data, Typeable)

166

168

167type Err = Err' Term

169type Err = Err' Term

src/Idris/IBC.hs+1−1

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

37import Util.Zlib (decompressEither)

38

39ibcVersion :: Word8

40−ibcVersion = 98

40+ibcVersion = 99

41

42data IBCFile = IBCFile { ver :: Word8,

43 sourcefile :: FilePath,