fdb46c7 · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Errors.idr+1−1

compare with master

unifiedsplit

@@ -3,7 +3,7 @@ module Language.Reflection.Errors

3import Language.Reflection

4

5data SourceLocation : Type where

6− FileLoc : (filename : String) -> (line : Int) -> (col : Int) -> SourceLocation

6+ FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation

7

8%name SourceLocation loc

9

src/Idris/AbsSyntax.hs+9−7

@@ -357,15 +357,15 @@ addNameIdx' i n

357getHdrs :: Codegen -> Idris [String]

358getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

359

360−setErrLine :: Int -> Idris ()

360+setErrSpan :: FC -> Idris ()

361−setErrLine x = do i <- getIState;

361+setErrSpan x = do i <- getIState;

362− case (errLine i) of

362+ case (errSpan i) of

363− Nothing -> putIState $ i { errLine = Just x }

363+ Nothing -> putIState $ i { errSpan = Just x }

364 Just _ -> return ()

365

366clearErr :: Idris ()

367clearErr = do i <- getIState

368− putIState $ i { errLine = Nothing }

368+ putIState $ i { errSpan = Nothing }

369

370getSO :: Idris (Maybe String)

371getSO = do i <- getIState

@@ -392,6 +392,8 @@ getName = do i <- getIState;

392 putIState $ (i { idris_name = idx + 1 })

393 return idx

394

395+-- InternalApp keeps track of the real function application for making case splits from, not the application the

396+-- programmer wrote, which doesn't have the whole context in any case other than top level definitions

395addInternalApp :: FilePath -> Int -> PTerm -> Idris ()

397addInternalApp :: FilePath -> Int -> PTerm -> Idris ()

396addInternalApp fp l t

398addInternalApp fp l t

397 = do i <- getIState

399 = do i <- getIState

@@ -649,7 +651,7 @@ ihWarn h fc err = do i <- getIState

649 IdeSlave n ->

651 IdeSlave n ->

650 do let (str, spans) = displaySpans err'

652 do let (str, spans) = displaySpans err'

651 runIO . hPutStrLn h $

653 runIO . hPutStrLn h $

652− convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, str, spans) n

654+ convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

653

655

654setLogLevel :: Int -> Idris ()

656setLogLevel :: Int -> Idris ()

655setLogLevel l = do i <- getIState

657setLogLevel l = do i <- getIState

@@ -906,7 +908,7 @@ iLOG = logLvl 1

906

908

907noErrors :: Idris Bool

909noErrors :: Idris Bool

908noErrors = do i <- getIState

910noErrors = do i <- getIState

909− case errLine i of

911+ case errSpan i of

910 Nothing -> return True

912 Nothing -> return True

911 _ -> return False

913 _ -> return False

912

914

src/Idris/AbsSyntaxTree.hs+3−2

@@ -135,11 +135,12 @@ data IState = IState {

135 idris_cgflags :: [(Codegen, String)],

136 idris_hdrs :: [(Codegen, String)],

137 proof_list :: [(Name, [String])],

138− errLine :: Maybe Int,

138+ errSpan :: Maybe FC,

139 parserWarnings :: [(FC, Err)],

140 lastParse :: Maybe Name,

141 indent_stack :: [Int],

142 brace_stack :: [Maybe Int],

143+ lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?

143 hide_list :: [(Name, Maybe Accessibility)],

144 hide_list :: [(Name, Maybe Accessibility)],

144 default_access :: Accessibility,

145 default_access :: Accessibility,

145 default_total :: Bool,

146 default_total :: Bool,

@@ -224,7 +225,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

224 emptyContext emptyContext emptyContext emptyContext

225 emptyContext emptyContext emptyContext emptyContext

225 emptyContext emptyContext

226 emptyContext emptyContext

226 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

227 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

227− [] Nothing [] Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

228+ [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

228 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

229 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

229 AutomaticWidth

230 AutomaticWidth

230

231

src/Idris/Core/TT.hs+9−6

@@ -44,8 +44,8 @@ data Option = TTypeInTType

44

45-- | Source location. These are typically produced by the parser 'Idris.Parser.getFC'

46data FC = FC { fc_fname :: String, -- ^ Filename

47− fc_line :: Int, -- ^ Line number

47+ fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span

48− fc_column :: Int -- ^ Column number

48+ fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span

49 }

50

51-- | Ignore source location equality (so deriving classes do not compare FCs)

@@ -57,7 +57,7 @@ newtype FC' = FC' { unwrapFC :: FC }

57

58instance Eq FC' where

59 FC' fc == FC' fc' = fcEq fc fc'

60− where fcEq (FC n l c) (FC n' l' c') = n == n' && l == l' && c == c'

60+ where fcEq (FC n s e) (FC n' s' e') = n == n' && s == s' && e == e'

61

62-- | Empty source location

63emptyFC :: FC

@@ -65,7 +65,7 @@ emptyFC = fileFC ""

65

66-- | Source location with file only

67fileFC :: String -> FC

68−fileFC s = FC s 0 0

68+fileFC s = FC s (0, 0) (0, 0)

69

70{-!

71deriving instance Binary FC

@@ -73,10 +73,13 @@ deriving instance NFData FC

73!-}

74

75instance Sized FC where

76− size (FC f l c) = 1 + length f

76+ size (FC f s e) = 4 + length f

77

78instance Show FC where

79− show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c

79+ show (FC f s e) = f ++ ":" ++ showLC s e

80+ where showLC (sl, sc) (el, ec) | sl == el && sc == ec = show sl ++ ":" ++ show sc

81+ | sl == el = show sl ++ ":" ++ show sc ++ "-" ++ show ec

82+ | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec

80

83

81-- | Output annotation for pretty-printed name - decides colour

84-- | Output annotation for pretty-printed name - decides colour

82data NameOutput = TypeOutput | FunOutput | DataOutput

85data NameOutput = TypeOutput | FunOutput | DataOutput

src/Idris/ElabDecls.hs+4−4

@@ -108,8 +108,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

108 -- Add normalised type to internals

109 rep <- useREPL

110 when rep $ do

111− addInternalApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty'))

111+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

112− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (mergeTy ty' (delab i nty')))

112+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')))

113

114 let (t, _) = unApply (getRetTy nty')

115 let corec = case t of

@@ -1408,8 +1408,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1408

1409 rep <- useREPL

1410 when rep $ do

1411− addInternalApp (fc_fname fc) (fc_line fc) (delabMV i clhs)

1411+ addInternalApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs) -- TODO: Should use span instead of line and filename?

1412− addIBC (IBCLineApp (fc_fname fc) (fc_line fc) (delabMV i clhs))

1412+ addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (delabMV i clhs))

1413

1414 logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

1415 -- Elaborate where block

src/Idris/ElabTerm.hs+13−5

@@ -1620,11 +1620,19 @@ reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [

1620reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]

1621reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]

1622reflectErr (At fc err) = raw_apply (Var $ reflErrName "At") [reflectFC fc, reflectErr err]

1623− where reflectFC (FC source line col) = raw_apply (Var $ reflErrName "FileLoc")

1623+ where reflectFC (FC source (sl, sc) (el, ec)) = raw_apply (Var $ reflErrName "FileLoc")

1624− [ RConstant (Str source)

1624+ [ RConstant (Str source)

1625+ , raw_apply (Var pairCon) [

1626+ RConstant (AType (ATInt ITNative)),

1625− , RConstant (I line)

1627+ RConstant (AType (ATInt ITNative)),

1628+ RConstant (I sl),

1629+ RConstant (I sc)]

1630+ , raw_apply (Var pairCon) [

1631+ RConstant (AType (ATInt ITNative)),

1632+ RConstant (AType (ATInt ITNative)),

1626− , RConstant (I col)

1633+ RConstant (I el),

1634+ RConstant (I ec)]

1627− ]

1635+ ]

1628reflectErr (Elaborating str n e) =

1636reflectErr (Elaborating str n e) =

1629 raw_apply (Var $ reflErrName "Elaborating")

1637 raw_apply (Var $ reflErrName "Elaborating")

1630 [ RConstant (Str str)

1638 [ RConstant (Str str)

src/Idris/Error.hs+8−13

@@ -23,7 +23,7 @@ iucheck = do tit <- typeInType

23 when (not tit) $

24 do ist <- getIState

25 (tclift $ ucheck (idris_constraints ist)) `idrisCatch`

26− (\e -> do setErrLine (getErrLine e)

26+ (\e -> do setErrSpan (getErrSpan e)

27 iputStrLn (pshow ist e))

28

29showErr :: Err -> Idris String

@@ -43,9 +43,9 @@ setAndReport :: Err -> Idris ()

43setAndReport e = do ist <- getIState

44 let h = idris_outh ist

45 case e of

46− At fc@(FC f l c) e -> do setErrLine l

46+ At fc e -> do setErrSpan fc

47− ihWarn h fc $ pprintErr ist e

47+ ihWarn h fc $ pprintErr ist e

48− _ -> do setErrLine (getErrLine e)

48+ _ -> do setErrSpan (getErrSpan e)

49 ihputStrLn h $ pshow ist e

50

51ifail :: String -> Idris a

@@ -56,7 +56,7 @@ ierror = throwError

56

57tclift :: TC a -> Idris a

58tclift (OK v) = return v

59−tclift (Error err@(At (FC f l c) e)) = do setErrLine l ; throwError err

59+tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err

60tclift (Error err) = throwError err

61

62tctry :: TC a -> TC a -> Idris a

@@ -65,11 +65,6 @@ tctry tc1 tc2

65 OK v -> return v

66 Error err -> tclift tc2

67

68−getErrLine :: Err -> Int

68+getErrSpan :: Err -> FC

69−getErrLine (At (FC _ l _) _) = l

69+getErrSpan (At fc _) = fc

70−getErrLine _ = 0

70+getErrSpan _ = emptyFC

71−

72−getErrColumn :: Err -> Int

73−getErrColumn (At (FC _ _ c) _) = c

74−getErrColumn _ = 0

75−

src/Idris/IBC.hs+5−3

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

28import Util.Zlib (decompressEither)

29

30ibcVersion :: Word8

31−ibcVersion = 63

31+ibcVersion = 64

32

33

34data IBCFile = IBCFile { ver :: Word8,

@@ -577,13 +577,15 @@ instance Binary CGInfo where

577 return (CGInfo x1 x2 [] x4 x5)

578

579instance Binary FC where

580− put (FC x1 x2 x3)

580+ put (FC x1 (x2, x3) (x4, x5))

581 = do put x1

582 put (x2 * 65536 + x3)

583+ put (x4 * 65536 + x5)

583 get

584 get

584 = do x1 <- get

585 = do x1 <- get

585 x2x3 <- get

586 x2x3 <- get

587+ x4x5 <- get

586− return (FC x1 (x2x3 `div` 65536) (x2x3 `mod` 65536))

588+ return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))

587

589

588

590

589instance Binary Name where

591instance Binary Name where

src/Idris/IdeSlave.hs+4−4

@@ -89,10 +89,10 @@ instance SExpable OutputAnnotation where

89 (SymbolAtom "implicit", BoolAtom imp)]

90 toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]

91 toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]

92− toSExp (AnnFC (FC f l c)) = toSExp [(SymbolAtom "source-loc",

92+ toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",

93− ((SymbolAtom "filename", StringAtom f),

93+ ((SymbolAtom "filename", StringAtom f),

94− (SymbolAtom "line", IntegerAtom (toInteger l)),

94+ (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

95− (SymbolAtom "column", IntegerAtom (toInteger c))))]

95+ (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec))))]

96

97escape :: String -> String

98escape = concatMap escapeChar

src/Idris/ParseHelpers.hs+11−6

@@ -1,5 +1,4 @@

1−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

1+{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, OverlappingInstances, StandaloneDeriving #-}

2−{-# LANGUAGE StandaloneDeriving #-}

3module Idris.ParseHelpers where

2module Idris.ParseHelpers where

4

3

5import Prelude hiding (pi)

4import Prelude hiding (pi)

@@ -43,13 +42,19 @@ import Debug.Trace

43type IdrisParser = StateT IState IdrisInnerParser

42type IdrisParser = StateT IState IdrisInnerParser

44

43

45newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

44newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }

46− deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing{-, Parsing-}, DeltaParsing, MarkParsing Delta, Monoid)

45+ deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, DeltaParsing, MarkParsing Delta, Monoid, TokenParsing)

47

46

48deriving instance Parsing IdrisInnerParser

47deriving instance Parsing IdrisInnerParser

49

48

50−instance TokenParsing IdrisInnerParser where

49+instance TokenParsing IdrisParser where

51 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

50 someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()

52−

51+ token p = do s <- get

52+ (FC fn (sl, sc) _) <- getFC --TODO: Update after fixing getFC

53+ r <- p

54+ (FC fn _ (el, ec)) <- getFC

55+ whiteSpace

56+ put (s { lastTokenSpan = Just (FC fn (sl, sc) (el, ec)) })

57+ return r

53-- | Generalized monadic parsing constraint type

58-- | Generalized monadic parsing constraint type

54type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

59type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)

55

60

@@ -333,7 +338,7 @@ getFC :: MonadicParsing m => m FC

333getFC = do s <- position

338getFC = do s <- position

334 let (dir, file) = splitFileName (fileName s)

339 let (dir, file) = splitFileName (fileName s)

335 let f = if dir == addTrailingPathSeparator "." then file else fileName s

340 let f = if dir == addTrailingPathSeparator "." then file else fileName s

336− return $ FC f (lineNum s) (columnNum s)

341+ return $ FC f (lineNum s, columnNum s) (lineNum s, columnNum s) -- TODO: Change to actual spanning

337

342

338{-* Syntax helpers-}

343{-* Syntax helpers-}

339-- | Bind constraints to term

344-- | Bind constraints to term

src/Idris/Parser.hs+3−3

@@ -1131,7 +1131,7 @@ parseProg syn fname input mrk

1131 case idris_outputmode i of

1132 RawOutput -> ihputStrLn (idris_outh i) (show doc)

1133 IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

1134− putIState (i { errLine = Just (fc_line fc) }) -- Just errl })

1134+ putIState (i { errSpan = Just fc })

1135 return []

1136 Success (x, i) -> do putIState i

1137 reportParserWarnings

@@ -1149,7 +1149,7 @@ parseProg syn fname input mrk

1149loadModule :: Handle -> FilePath -> Idris String

1150loadModule outh f

1151 = idrisCatch (loadModule' outh f)

1152− (\e -> do setErrLine (getErrLine e)

1152+ (\e -> do setErrSpan (getErrSpan e)

1153 ist <- getIState

1154 msg <- showErr e

1155 ihputStrLn outh msg

@@ -1197,7 +1197,7 @@ loadFromIFile h (LIDR fn) = loadSource' h True fn

1197loadSource' :: Handle -> Bool -> FilePath -> Idris ()

1198loadSource' h lidr r

1199 = idrisCatch (loadSource h lidr r)

1200− (\e -> do setErrLine (getErrLine e)

1200+ (\e -> do setErrSpan (getErrSpan e)

1201 ist <- getIState

1202 ihRenderError h (pprintErr ist e))

1203

src/Idris/REPL.hs+6−6

@@ -238,7 +238,7 @@ ideslave orig mods

238 isetPrompt (mkPrompt [filename])

239 -- Report either success or failure

240 i <- getIState

241− case (errLine i) of

241+ case (errSpan i) of

242 Nothing -> iPrintResult $ "loaded " ++ filename

243 Just x -> iPrintError $ "didn't load " ++ filename

244 ideslave orig [filename]

@@ -246,7 +246,7 @@ ideslave orig mods

246 case splitName name of

247 Left err -> iPrintError err

248 Right n -> process stdout "(ideslave)"

249− (Check (PRef (FC "(ideslave)" 0 0) n))

249+ (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

250 Just (IdeSlave.DocsFor name) ->

251 case splitName name of

252 Left err -> iPrintError err

@@ -412,7 +412,7 @@ edit f orig

412 = do i <- getIState

413 env <- runIO $ getEnvironment

414 let editor = getEditor env

415− let line = case errLine i of

415+ let line = case errSpan i of

416 Just l -> " +" ++ show l ++ " "

417 Nothing -> " "

418 let cmd = editor ++ line ++ fixName f

@@ -1125,7 +1125,7 @@ loadInputs h inputs

1125 -- to check everything worked consistently (in particular, will catch

1126 -- if the ibc version is out of date) if we weren't loading per

1127 -- module

1128− case errLine inew of

1128+ case errSpan inew of

1129 Nothing ->

1130 do putIState ist

1131 when (not loadCode) $ tryLoad $ nub (concat ifiles)

@@ -1133,10 +1133,10 @@ loadInputs h inputs

1133 putIState inew)

1134 (\e -> do i <- getIState

1135 case e of

1136− At f _ -> do setErrLine (fc_line f)

1136+ At f _ -> do setErrSpan f

1137 ihRenderError stdout $ pprintErr i e

1138 ProgramLineComment -> return () -- fail elsewhere

1139− _ -> do setErrLine 3 -- FIXME! Propagate it

1139+ _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1140 iputStrLn (pshow i e))

1141 where -- load all files, stop if any fail

1142 tryLoad :: [IFileType] -> Idris ()

src/Idris/Unlit.hs+2−2

@@ -24,8 +24,8 @@ check f l [x] = return ()

24check f l [] = return ()

25

26chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()

27−chkAdj f l Prog Comm = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column?

27+chkAdj f l Prog Comm = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

28−chkAdj f l Comm Prog = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column?

28+chkAdj f l Comm Prog = tfail $ At (FC f (l, 0) (l, 0)) ProgramLineComment --TODO: Span correctly

29chkAdj f l _ _ = return ()

30

31

src/Pkg/Package.hs+2−2

@@ -52,7 +52,7 @@ buildPkg warnonly (install, fp)

52 Nothing -> exitWith (ExitFailure 1)

53 Just ist -> do

54 -- Quit with error code if there was a problem

55− case errLine ist of

55+ case errSpan ist of

56 Just _ -> exitWith (ExitFailure 1)

57 _ -> return ()

58 -- Also give up if there are metavariables to solve

@@ -85,7 +85,7 @@ checkPkg warnonly quit fpath

85 when quit $ case res of

86 Nothing -> exitWith (ExitFailure 1)

87 Just res' -> do

88− case errLine res' of

88+ case errSpan res' of

89 Just _ -> exitWith (ExitFailure 1)

90 _ -> return ()

91

test/error003/ErrorReflection.idr+3−3

@@ -59,11 +59,11 @@ dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1

59 ty1 <- reifyTy tm1'

60 ty2 <- reifyTy tm2'

61 return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]

62−dslerr (At (FileLoc f l c) err) = do err' <- dslerr err

62+dslerr (At (FileLoc f s e) err) = do err' <- dslerr err

63 return [ TextPart "In file"

64 , TextPart f

65− , TextPart "line", TextPart (cast l)

65+ , TextPart "start", TextPart (show s)

66− , TextPart "column", TextPart (cast c)

66+ , TextPart "end", TextPart (show e)

67 , SubReport err']

68dslerr (Elaborating s n err) = do err' <- dslerr err

69 return ([ TextPart $ "When elaborating " ++ s

test/error003/expected+1−1

@@ -1,3 +1,3 @@

1−In file ErrorReflection.idr line 78 column 5

1+In file ErrorReflection.idr start (78, 5) end (78, 5)

2 When elaborating right hand side of Main.bad :

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