fdb46c7 · Idris-dev · git.iko.soy

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

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

33import Language.Reflection

44

55data SourceLocation : Type where

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

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

77

88%name SourceLocation loc

99

src/Idris/AbsSyntax.hs+9−7

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

357357getHdrs :: Codegen -> Idris [String]

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

359359

360−setErrLine :: Int -> Idris ()

361−setErrLine x = do i <- getIState;

362− case (errLine i) of

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

360+setErrSpan :: FC -> Idris ()

361+setErrSpan x = do i <- getIState;

362+ case (errSpan i) of

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

364364 Just _ -> return ()

365365

366366clearErr :: Idris ()

367367clearErr = do i <- getIState

368− putIState $ i { errLine = Nothing }

368+ putIState $ i { errSpan = Nothing }

369369

370370getSO :: Idris (Maybe String)

371371getSO = do i <- getIState

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

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

393393 return idx

394394

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

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

396398addInternalApp fp l t

397399 = do i <- getIState

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

649651 IdeSlave n ->

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

651653 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

653655

654656setLogLevel :: Int -> Idris ()

655657setLogLevel l = do i <- getIState

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

906908

907909noErrors :: Idris Bool

908910noErrors = do i <- getIState

909− case errLine i of

911+ case errSpan i of

910912 Nothing -> return True

911913 _ -> return False

912914

src/Idris/AbsSyntaxTree.hs+3−2

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

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

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

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

138− errLine :: Maybe Int,

138+ errSpan :: Maybe FC,

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

140140 lastParse :: Maybe Name,

141141 indent_stack :: [Int],

142142 brace_stack :: [Maybe Int],

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

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

144145 default_access :: Accessibility,

145146 default_total :: Bool,

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

224225 emptyContext emptyContext emptyContext emptyContext

225226 emptyContext emptyContext

226227 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

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

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

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

229230 AutomaticWidth

230231

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

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

4444

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

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

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

48− fc_column :: Int -- ^ Column number

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

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

4949 }

5050

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

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

5757

5858instance Eq FC' where

5959 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'

6161

6262-- | Empty source location

6363emptyFC :: FC

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

6565

6666-- | Source location with file only

6767fileFC :: String -> FC

68−fileFC s = FC s 0 0

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

6969

7070{-!

7171deriving instance Binary FC

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

7373!-}

7474

7575instance Sized FC where

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

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

7777

7878instance 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

8083

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

8285data 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

108108 -- Add normalised type to internals

109109 rep <- useREPL

110110 when rep $ do

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

112− addIBC (IBCLineApp (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) (fst . fc_start $ fc) (mergeTy ty' (delab i nty')))

113113

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

115115 let corec = case t of

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

14081408

14091409 rep <- useREPL

14101410 when rep $ do

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

1412− addIBC (IBCLineApp (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) (fst . fc_start $ fc) (delabMV i clhs))

14131413

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

14151415 -- Elaborate where block

src/Idris/ElabTerm.hs+13−5

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

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

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

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

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

1624− [ RConstant (Str source)

1625− , RConstant (I line)

1626− , RConstant (I col)

1627− ]

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

1624+ [ RConstant (Str source)

1625+ , raw_apply (Var pairCon) [

1626+ RConstant (AType (ATInt ITNative)),

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

1633+ RConstant (I el),

1634+ RConstant (I ec)]

1635+ ]

16281636reflectErr (Elaborating str n e) =

16291637 raw_apply (Var $ reflErrName "Elaborating")

16301638 [ RConstant (Str str)

src/Idris/Error.hs+8−13

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

2323 when (not tit) $

2424 do ist <- getIState

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

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

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

2727 iputStrLn (pshow ist e))

2828

2929showErr :: Err -> Idris String

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

4343setAndReport e = do ist <- getIState

4444 let h = idris_outh ist

4545 case e of

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

47− ihWarn h fc $ pprintErr ist e

48− _ -> do setErrLine (getErrLine e)

46+ At fc e -> do setErrSpan fc

47+ ihWarn h fc $ pprintErr ist e

48+ _ -> do setErrSpan (getErrSpan e)

4949 ihputStrLn h $ pshow ist e

5050

5151ifail :: String -> Idris a

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

5656

5757tclift :: TC a -> Idris a

5858tclift (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

6060tclift (Error err) = throwError err

6161

6262tctry :: TC a -> TC a -> Idris a

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

6565 OK v -> return v

6666 Error err -> tclift tc2

6767

68−getErrLine :: Err -> Int

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

70−getErrLine _ = 0

71−

72−getErrColumn :: Err -> Int

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

74−getErrColumn _ = 0

75−

68+getErrSpan :: Err -> FC

69+getErrSpan (At fc _) = fc

70+getErrSpan _ = emptyFC

src/Idris/IBC.hs+5−3

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

2828import Util.Zlib (decompressEither)

2929

3030ibcVersion :: Word8

31−ibcVersion = 63

31+ibcVersion = 64

3232

3333

3434data IBCFile = IBCFile { ver :: Word8,

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

577577 return (CGInfo x1 x2 [] x4 x5)

578578

579579instance Binary FC where

580− put (FC x1 x2 x3)

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

581581 = do put x1

582582 put (x2 * 65536 + x3)

583+ put (x4 * 65536 + x5)

583584 get

584585 = do x1 <- get

585586 x2x3 <- get

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

587+ x4x5 <- get

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

587589

588590

589591instance Binary Name where

src/Idris/IdeSlave.hs+4−4

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

8989 (SymbolAtom "implicit", BoolAtom imp)]

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

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

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

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

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

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

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

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

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

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

9696

9797escape :: String -> String

9898escape = concatMap escapeChar

src/Idris/ParseHelpers.hs+11−6

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

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

2−{-# LANGUAGE StandaloneDeriving #-}

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

32module Idris.ParseHelpers where

43

54import Prelude hiding (pi)

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

4342type IdrisParser = StateT IState IdrisInnerParser

4443

4544newtype 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)

4746

4847deriving instance Parsing IdrisInnerParser

4948

50−instance TokenParsing IdrisInnerParser where

49+instance TokenParsing IdrisParser where

5150 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

5358-- | Generalized monadic parsing constraint type

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

5560

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

333338getFC = do s <- position

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

335340 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

337342

338343{-* Syntax helpers-}

339344-- | Bind constraints to term

src/Idris/Parser.hs+3−3

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

11311131 case idris_outputmode i of

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

11331133 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 })

11351135 return []

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

11371137 reportParserWarnings

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

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

11501150loadModule outh f

11511151 = idrisCatch (loadModule' outh f)

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

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

11531153 ist <- getIState

11541154 msg <- showErr e

11551155 ihputStrLn outh msg

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

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

11981198loadSource' h lidr r

11991199 = idrisCatch (loadSource h lidr r)

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

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

12011201 ist <- getIState

12021202 ihRenderError h (pprintErr ist e))

12031203

src/Idris/REPL.hs+6−6

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

238238 isetPrompt (mkPrompt [filename])

239239 -- Report either success or failure

240240 i <- getIState

241− case (errLine i) of

241+ case (errSpan i) of

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

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

244244 ideslave orig [filename]

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

246246 case splitName name of

247247 Left err -> iPrintError err

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

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

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

250250 Just (IdeSlave.DocsFor name) ->

251251 case splitName name of

252252 Left err -> iPrintError err

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

412412 = do i <- getIState

413413 env <- runIO $ getEnvironment

414414 let editor = getEditor env

415− let line = case errLine i of

415+ let line = case errSpan i of

416416 Just l -> " +" ++ show l ++ " "

417417 Nothing -> " "

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

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

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

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

11271127 -- module

1128− case errLine inew of

1128+ case errSpan inew of

11291129 Nothing ->

11301130 do putIState ist

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

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

11331133 putIState inew)

11341134 (\e -> do i <- getIState

11351135 case e of

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

1136+ At f _ -> do setErrSpan f

11371137 ihRenderError stdout $ pprintErr i e

11381138 ProgramLineComment -> return () -- fail elsewhere

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

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

11401140 iputStrLn (pshow i e))

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

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

src/Idris/Unlit.hs+2−2

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

2424check f l [] = return ()

2525

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

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

28−chkAdj f l Comm Prog = 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) (l, 0)) ProgramLineComment --TODO: Span correctly

2929chkAdj f l _ _ = return ()

3030

3131

src/Pkg/Package.hs+2−2

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

5252 Nothing -> exitWith (ExitFailure 1)

5353 Just ist -> do

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

55− case errLine ist of

55+ case errSpan ist of

5656 Just _ -> exitWith (ExitFailure 1)

5757 _ -> return ()

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

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

8585 when quit $ case res of

8686 Nothing -> exitWith (ExitFailure 1)

8787 Just res' -> do

88− case errLine res' of

88+ case errSpan res' of

8989 Just _ -> exitWith (ExitFailure 1)

9090 _ -> return ()

9191

test/error003/ErrorReflection.idr+3−3

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

5959 ty1 <- reifyTy tm1'

6060 ty2 <- reifyTy tm2'

6161 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

6363 return [ TextPart "In file"

6464 , TextPart f

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

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

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

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

6767 , SubReport err']

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

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

22 When elaborating right hand side of Main.bad :

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