a2226ad · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

23%name TTUExp uexp

24

25-- | 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

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

29 | B8Type | B16Type | B32Type | B64Type

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

37instance ReflConst Int where

38 toConst x = I x

39

40−instance ReflConst Nat where

40+instance ReflConst Integer where

41 toConst = BI

42

43instance ReflConst Float where

src/Idris/AbsSyntax.hs+11−1

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

515 let opt' = opts { opt_repl = t }

516 putIState $ i { idris_options = opt' }

517

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+

518setNoBanner :: Bool -> Idris ()

528setNoBanner :: Bool -> Idris ()

519setNoBanner n = do i <- getIState

529setNoBanner n = do i <- getIState

520 let opts = idris_options i

530 let opts = idris_options i

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

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

522 putIState $ i { idris_options = opt' }

532 putIState $ i { idris_options = opt' }

523

533

524getNoBanner :: Idris Bool

534getNoBanner :: Idris Bool

src/Idris/AbsSyntaxTree.hs+4−1

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

49 opt_triple :: String,

50 opt_cpu :: String,

51 opt_optLevel :: Word,

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

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

53+ opt_origerr :: Bool

53 }

54 }

54 deriving (Show, Eq)

55 deriving (Show, Eq)

55

56

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

71 , opt_cpu = ""

72 , opt_cpu = ""

72 , opt_optLevel = 2

73 , opt_optLevel = 2

73 , opt_cmdline = []

74 , opt_cmdline = []

75+ , opt_origerr = False

74 }

76 }

75

77

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

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

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

316 | TargetCPU String

318 | TargetCPU String

317 | OptLevel Word

319 | OptLevel Word

318 | Client String

320 | Client String

321+ | ShowOrigErr

319 deriving (Show, Eq)

322 deriving (Show, Eq)

320

323

321-- Parsed declarations

324-- Parsed declarations

src/Idris/Completion.hs+1−1

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

104

105completeOption :: CompletionFunc Idris

106completeOption = completeWord Nothing " \t" completeOpt

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

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

108

109isWhitespace :: Char -> Bool

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

src/Idris/Delaborate.hs+14−11

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

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

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

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

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

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

205+ if (opt_origerr (idris_options i))

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

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

207+ else ""

206− where showPart :: ErrorReportPart -> String

208+ where showPart :: ErrorReportPart -> String

207− showPart (TextPart str) = str

209+ showPart (TextPart str) = str

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

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

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

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

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

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

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

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

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

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

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

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

216+ indented msg ++

214− indented (pshow' i err) ++

217+ indented (pshow i err) ++

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

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

216

219

217

220

218showSc i [] = ""

221showSc i [] = ""

src/Idris/ElabTerm.hs+3−3

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

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

1187

1188reifyTTName :: Term -> ElabD Name

1189−reifyTTName t@(App _ _)

1189+reifyTTName t

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

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

1192

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

1575 Error e -> Left . InternalMsg $

1576 "could not reify name term " ++

1577 show ttn ++

1578− " when reflecting an error"

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

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

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

1581 | n == reflErrName "TermPart" =

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

1583 Error e -> Left . InternalMsg $

1584 "could not reify reflected term " ++

1585 show tm ++

1586− " when reflecting an error"

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

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

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

1589 | n == reflErrName "SubReport" =

src/Idris/REPL.hs+10−4

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

312 iPrintResult ""

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

314 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 ""

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

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

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

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

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

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

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

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

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

909process h fn NOP = return ()

913process h fn NOP = return ()

910

914

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

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

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

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

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

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

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

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

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

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

915

921

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

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

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

923process 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)

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

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

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

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

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

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

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

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

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

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

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

105pOption :: P.IdrisParser Opt

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

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

108−

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

109

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

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

test/test037/expected−14

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

2 When elaborating right hand side of Main.bad :

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

4

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

31%error_handlers cadr cons1 has2elts

32%error_handlers cadr cons2 has2elts

33

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.