a2226ad · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'origin/error-reflection' into error-reflection

Conflicts: src/Idris/Delaborate.hs test/test038/expected

commita2226adf26358421916314c53004669d3cb8b622 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 28 Jan 2014, 15:06 (13 years ago) parent8c620dc f5974d9

11 files changed+60−40

compare with master

unifiedsplit

libs/base/Language/Reflection.idr+2−2 src/Idris/AbsSyntax.hs+11−1 src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/Completion.hs+1−1 src/Idris/Delaborate.hs+14−11 src/Idris/ElabTerm.hs+3−3 src/Idris/REPL.hs+10−4 src/Idris/REPLParser.hs+3−3 test/test037/expected−14 test/test039/FunErrTest.idr+8 test/test039/expected+4

libs/base/Language/Reflection.idr+2−2

@@ -23,7 +23,7 @@ data TTUExp = UVar Int

2323%name TTUExp uexp

2424

2525-- | Primitive constants

26−data Const = I Int | BI Nat | Fl Float | Ch Char | Str String

26+data Const = I Int | BI Integer | Fl Float | Ch Char | Str String

2828 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64

2929 | B8Type | B16Type | B32Type | B64Type

@@ -37,7 +37,7 @@ abstract class ReflConst (a : Type) where

3737instance ReflConst Int where

3838 toConst x = I x

3939

40−instance ReflConst Nat where

40+instance ReflConst Integer where

4141 toConst = BI

4242

4343instance ReflConst Float where

src/Idris/AbsSyntax.hs+11−1

@@ -515,10 +515,20 @@ setREPL t = do i <- getIState

515515 let opt' = opts { opt_repl = t }

516516 putIState $ i { idris_options = opt' }

517517

518+showOrigErr :: Idris Bool

519+showOrigErr = do i <- getIState

520+ return (opt_origerr (idris_options i))

521+

522+setShowOrigErr :: Bool -> Idris ()

523+setShowOrigErr b = do i <- getIState

524+ let opts = idris_options i

525+ let opt' = opts { opt_origerr = b }

526+ putIState $ i { idris_options = opt' }

527+

518528setNoBanner :: Bool -> Idris ()

519529setNoBanner n = do i <- getIState

520530 let opts = idris_options i

521− let opt' = opts {opt_nobanner = n}

531+ let opt' = opts { opt_nobanner = n }

522532 putIState $ i { idris_options = opt' }

523533

524534getNoBanner :: Idris Bool

src/Idris/AbsSyntaxTree.hs+4−1

@@ -49,7 +49,8 @@ data IOption = IOption { opt_logLevel :: Int,

4949 opt_triple :: String,

5050 opt_cpu :: String,

5151 opt_optLevel :: Word,

52− opt_cmdline :: [Opt] -- remember whole command line

52+ opt_cmdline :: [Opt], -- remember whole command line

53+ opt_origerr :: Bool

5354 }

5455 deriving (Show, Eq)

5556

@@ -71,6 +72,7 @@ defaultOpts = IOption { opt_logLevel = 0

7172 , opt_cpu = ""

7273 , opt_optLevel = 2

7374 , opt_cmdline = []

75+ , opt_origerr = False

7476 }

7577

7678data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

@@ -316,6 +318,7 @@ data Opt = Filename String

316318 | TargetCPU String

317319 | OptLevel Word

318320 | Client String

321+ | ShowOrigErr

319322 deriving (Show, Eq)

320323

321324-- Parsed declarations

src/Idris/Completion.hs+1−1

@@ -104,7 +104,7 @@ completeMetaVar = completeWord Nothing (" \t(){}:" ++ opChars) completeM

104104

105105completeOption :: CompletionFunc Idris

106106completeOption = completeWord Nothing " \t" completeOpt

107− where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])

107+ where completeOpt = return . completeWith ["errorcontext", "showimplicits", "originalerrors"]

108108

109109isWhitespace :: Char -> Bool

110110isWhitespace = (flip elem) " \t\n"

src/Idris/Delaborate.hs+14−11

@@ -201,18 +201,21 @@ pshow' i (Elaborating s n e) = "When elaborating " ++ s ++

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

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

203203pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in

204− concat (intersperse "\n" parts') ++

205− "\nOriginal error:\n" ++ indented (pshow' i orig)

206− where showPart :: ErrorReportPart -> String

207− showPart (TextPart str) = str

208− showPart (NamePart n) = let colour = idris_colourRepl i in

209− showName (Just i) [] False colour n

210− showPart (TermPart tm) = let colour = idris_colourRepl i

211− in showImp (Just i) False colour (delab i tm)

212− showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

204+ concat (intersperse "\n" parts') ++

205+ if (opt_origerr (idris_options i))

206+ then "\nOriginal error:\n" ++ indented (pshow i orig)

207+ else ""

208+ where showPart :: ErrorReportPart -> String

209+ showPart (TextPart str) = str

210+ showPart (NamePart n) = let colour = idris_colourRepl i in

211+ showName (Just i) [] False colour n

212+ showPart (TermPart tm) = let colour = idris_colourRepl i

213+ in showImp (Just i) False colour (delab i tm)

214+ showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

213215pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

214− indented (pshow' i err) ++

215− "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

216+ indented msg ++

217+ indented (pshow i err) ++

218+ "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr

216219

217220

218221showSc i [] = ""

src/Idris/ElabTerm.hs+3−3

@@ -1186,7 +1186,7 @@ reifyRawApp t [c]

11861186reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))

11871187

11881188reifyTTName :: Term -> ElabD Name

1189−reifyTTName t@(App _ _)

1189+reifyTTName t

11901190 | (P _ f _, args) <- unApply t = reifyTTNameApp f args

11911191reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

11921192

@@ -1575,7 +1575,7 @@ reifyReportPart (App (P (DCon _ _) n _) ttn)

15751575 Error e -> Left . InternalMsg $

15761576 "could not reify name term " ++

15771577 show ttn ++

1578− " when reflecting an error"

1578+ " when reflecting an error:" ++ show e

15791579 OK (n', _)-> Right $ NamePart n'

15801580reifyReportPart (App (P (DCon _ _) n _) tm)

15811581 | n == reflErrName "TermPart" =

@@ -1583,7 +1583,7 @@ reifyReportPart (App (P (DCon _ _) n _) tm)

15831583 Error e -> Left . InternalMsg $

15841584 "could not reify reflected term " ++

15851585 show tm ++

1586− " when reflecting an error"

1586+ " when reflecting an error:" ++ show e

15871587 OK (tm', _) -> Right $ TermPart tm'

15881588reifyReportPart (App (P (DCon _ _) n _) tm)

15891589 | n == reflErrName "SubReport" =

src/Idris/REPL.hs+10−4

@@ -312,6 +312,10 @@ ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)

312312 iPrintResult ""

313313ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)

314314 iPrintResult ""

315+ideslaveProcess fn (SetOpt ShowOrigErr) = do process stdout fn (SetOpt ShowOrigErr)

316+ iPrintResult ""

317+ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process stdout fn (UnsetOpt ShowOrigErr)

318+ iPrintResult ""

315319ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)

316320ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)

317321ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)

@@ -908,10 +912,12 @@ process h fn Metavars

908912 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs

909913process h fn NOP = return ()

910914

911−process h fn (SetOpt ErrContext) = setErrContext True

912−process h fn (UnsetOpt ErrContext) = setErrContext False

913−process h fn (SetOpt ShowImpl) = setImpShow True

914−process h fn (UnsetOpt ShowImpl) = setImpShow False

915+process h fn (SetOpt ErrContext) = setErrContext True

916+process h fn (UnsetOpt ErrContext) = setErrContext False

917+process h fn (SetOpt ShowImpl) = setImpShow True

918+process h fn (UnsetOpt ShowImpl) = setImpShow False

919+process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

920+process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

915921

916922process h fn (SetOpt _) = iPrintError "Not a valid option"

917923process h fn (UnsetOpt _) = iPrintError "Not a valid option"

src/Idris/REPLParser.hs+3−3

@@ -61,8 +61,8 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

6161 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

6262 <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))

6363 <|> try (do cmd ["color", "colour"]; pSetColourCmd)

64− <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

65− <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

64+ <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))

65+ <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))

6666 <|> try (do cmd ["s", "search"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Search t))

6767 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

6868 upd <- option False (do P.lchar '!'; return True)

@@ -105,7 +105,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

105105pOption :: P.IdrisParser Opt

106106pOption = do discard (P.symbol "errorcontext"); return ErrContext

107107 <|> do discard (P.symbol "showimplicits"); return ShowImpl

108−

108+ <|> do discard (P.symbol "originalerrors"); return ShowOrigErr

109109

110110colours :: [(String, Maybe Color)]

111111colours = [ ("black", Just Black)

test/test037/expected−14

@@ -2,17 +2,3 @@ In file ErrorReflection.idr line 78 column 5

22 When elaborating right hand side of Main.bad :

33 DSL type error: (t'(504) => t'(504)) doesn't match ()

5−Original error:

6−

7− ErrorReflection.idr:78:5:When elaborating right hand side of bad:

8− Can't unify

9− Tm [] (Main.TFun t' t')

10− with

11− Tm [] Main.TUnit

12−

13− Specifically:

14− Can't unify

15− Main.TFun t' t'

16− with

17− Main.TUnit

18−

test/test039/FunErrTest.idr+8

@@ -31,3 +31,11 @@ has2elts e = Just [TextPart (show e)]

3131%error_handlers cadr cons1 has2elts

3232%error_handlers cadr cons2 has2elts

3333

34+badCadr1 : Int

35+badCadr1 = cadr []

36+

37+badCadr2 : Int

38+badCadr2 = cadr [1]

39+

40+goodCadr : Int

41+goodCadr = cadr [1, 2]

test/test039/expected+4

@@ -0,0 +1,4 @@

1+FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:

2+Could not prove that [] has at least two elements.

3+FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

4+Could not prove that Prelude.List.tail [(Prelude.Classes.fromInteger 1)] refl has at least two elements.