9e5c96f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add error object for failure to load file

9e5c96fDavid Christiansen13 years ago

src/Core/TT.hs+4

compare with master

unifiedsplit

@@ -101,6 +101,7 @@ data Err = Msg String

101 | At FC Err

102 | Elaborating String Name Err

103 | ProviderError String

104+ | LoadingFailed String Err

104 deriving Eq

105 deriving Eq

105

106

106instance Sized Err where

107instance Sized Err where

@@ -122,6 +123,7 @@ instance Sized Err where

122 size (At fc err) = size fc + size err

123 size (At fc err) = size fc + size err

123 size (Elaborating _ n err) = size err

124 size (Elaborating _ n err) = size err

124 size (ProviderError msg) = length msg

125 size (ProviderError msg) = length msg

126+ size (LoadingFailed fn e) = 1 + length fn + size e

125 size _ = 1

127 size _ = 1

126

128

127score :: Err -> Int

129score :: Err -> Int

@@ -139,6 +141,7 @@ instance Show Err where

139 ++ show e ++ " in " ++ show sc ++ " " ++ show i

141 ++ show e ++ " in " ++ show sc ++ " " ++ show i

140 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

142 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

141 show (ProviderError msg) = "Type provider error: " ++ msg

143 show (ProviderError msg) = "Type provider error: " ++ msg

144+ show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ show e

142 show _ = "Error"

145 show _ = "Error"

143

146

144instance Pretty Err where

147instance Pretty Err where

@@ -152,6 +155,7 @@ instance Pretty Err where

152 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$

155 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$

153 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

156 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

154 pretty (ProviderError msg) = text msg

157 pretty (ProviderError msg) = text msg

158+ pretty err@(LoadingFailed _ _) = text (show err)

155 pretty _ = text "Error"

159 pretty _ = text "Error"

156

160

157instance Error Err where

161instance Error Err where

src/Idris/Delaborate.hs+1

@@ -163,6 +163,7 @@ pshow i (At f e) = show f ++ ":" ++ pshow i e

163pshow i (Elaborating s n e) = "When elaborating " ++ s ++

164 showqual i n ++ ":\n" ++ pshow i e

165pshow i (ProviderError msg) = "Type provider error: " ++ msg

166+pshow i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow i e

166

167

167showSc i [] = ""

168showSc i [] = ""

168showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

169showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

src/Idris/Parser.hs+1−1

@@ -952,7 +952,7 @@ loadFromIFile :: IFileType -> Idris ()

952loadFromIFile i@(IBC fn src)

953 = do iLOG $ "Skipping " ++ getSrcFile i

954 idrisCatch (loadIBC fn)

955− (\c -> do fail $ fn ++ " failed " ++ show c)

955+ (\err -> ierror $ LoadingFailed fn err)

956 where

957 getSrcFile (IDR fn) = fn

958 getSrcFile (LIDR fn) = fn