bc0ebee · Idris-dev · git.iko.soy

src/Core/Constraints.hs+1−1

@@ -38,7 +38,7 @@ mkRels ((c, f) : cs) acc

3838

3939

4040acyclic :: Relations -> [UExp] -> TC ()

41−acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs

41+acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs

4242 where

4343 checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()

4444 checkCycle fc r path inc [] = return ()

src/Core/Evaluate.hs+5−5

@@ -700,10 +700,10 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)

700700 access = case lookupDefAcc n False uctxt of

701701 [(_, acc)] -> acc

702702 _ -> Public

703− ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps_tot,

704− simpleCase tcase covering reflect CompileTime (FC "" 0) ps_ct,

705− simpleCase tcase covering reflect CompileTime (FC "" 0) ps_inl,

706− simpleCase tcase covering reflect RunTime (FC "" 0) ps_rt) of

703+ ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC ps_tot,

704+ simpleCase tcase covering reflect CompileTime emptyFC ps_ct,

705+ simpleCase tcase covering reflect CompileTime emptyFC ps_inl,

706+ simpleCase tcase covering reflect RunTime emptyFC ps_rt) of

707707 (OK (CaseDef args_tot sc_tot _),

708708 OK (CaseDef args_ct sc_ct _),

709709 OK (CaseDef args_inl sc_inl _),

@@ -730,7 +730,7 @@ simplifyCasedef n uctxt

730730 [(CaseOp ci ty ps_in ps cd, acc, tot)] ->

731731 let ps_in' = map simpl ps_in

732732 pdef = map debind ps_in' in

733− case simpleCase False True False CompileTime (FC "" 0) pdef of

733+ case simpleCase False True False CompileTime emptyFC pdef of

734734 OK (CaseDef args sc _) ->

735735 addDef n (CaseOp ci

736736 ty ps_in' ps (cd { cases_totcheck = (args, sc) }),

src/Core/TT.hs+25−5

@@ -38,20 +38,40 @@ data Option = TTypeInTType

3838 | CheckConv

3939 deriving Eq

4040

41−-- | Source location. These are typically produced by the parser 'Idris.Parser.pfc'

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

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

43− fc_line :: Int -- ^ Line number

43+ fc_line :: Int, -- ^ Line number

44+ fc_column :: Int -- ^ Column number

4445 }

45− deriving Eq

46+

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

48+instance Eq FC where

49+ _ == _ = True

50+

51+-- | FC with equality

52+newtype FC' = FC' { unwrapFC :: FC }

53+

54+instance Eq FC' where

55+ FC' fc == FC' fc' = fcEq fc fc'

56+ where fcEq (FC n l c) (FC n' l' c') = n == n' && l == l' && c == c'

57+

58+-- | Empty source location

59+emptyFC :: FC

60+emptyFC = fileFC ""

61+

62+-- | Source location with file only

63+fileFC :: String -> FC

64+fileFC s = FC s 0 0

65+

4666{-!

4767deriving instance Binary FC

4868!-}

4969

5070instance Sized FC where

51− size (FC f l) = 1 + length f

71+ size (FC f l c) = 1 + length f

5272

5373instance Show FC where

54− show (FC f l) = f ++ ":" ++ show l

74+ show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c

5575

5676data Err = Msg String

5777 | InternalMsg String

src/Idris/AbsSyntax.hs+7−4

@@ -314,7 +314,10 @@ iputStrLn s = do i <- getIState

314314 (fn, ':':rest) -> case span isDigit rest of

315315 ([], ':':msg) -> write

316316 ([], msg) -> write

317− (num, ':':msg) -> iWarn (FC fn (read num)) msg

317+ (row, ':':rest') ->

318+ case span isDigit rest' of

319+ ([], msg) -> iWarn (FC fn (read row) 0) msg

320+ (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg

318321 _ -> write

319322 where write = runIO . putStrLn $ convSExp "write-string" s n

320323

@@ -576,7 +579,7 @@ setTypeCase t = do i <- getIState

576579

577580-- For inferring types of things

578581

579−bi = FC "builtin" 0

582+bi = fileFC "builtin"

580583

581584inferTy = MN 0 "__Infer"

582585inferCon = MN 0 "__infer"

@@ -1420,8 +1423,8 @@ substMatchShadow n shs tm t = sm shs t where

14201423 sm xs (PPi p x t sc)

14211424 | x `elem` xs

14221425 = let x' = nextName x in

1423− PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))

1424− (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))

1426+ PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))

1427+ (sm (x':xs) (substMatch x (PRef emptyFC x') sc))

14251428 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

14261429 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

14271430 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

src/Idris/AbsSyntaxTree.hs+4−2

@@ -561,7 +561,9 @@ data PTerm = PQuote Raw

561561 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice

562562 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

563563 | PNoImplicits PTerm -- ^ never run implicit converions on the term

564− deriving Eq

564+ deriving Eq

565+

566+

565567{-!

566568deriving instance Binary PTerm

567569!-}

@@ -774,7 +776,7 @@ initDSL = DSL (PRef f (UN ">>="))

774776 Nothing

775777 Nothing

776778 Nothing

777− where f = FC "(builtin)" 0

779+ where f = fileFC "(builtin)"

778780

779781data Using = UImplicit Name PTerm

780782 | UConstraint Name [Name]

src/Idris/DSL.hs+2−2

@@ -22,12 +22,12 @@ desugar syn i t = let t' = expandDo (dsl_info syn) t in

2222expandDo :: DSL -> PTerm -> PTerm

2323expandDo dsl (PLam n ty tm)

2424 | Just lam <- dsl_lambda dsl

25− = let sc = PApp (FC "(dsl)" 0) lam [pexp (var dsl n tm 0)] in

25+ = let sc = PApp (fileFC "(dsl)") lam [pexp (var dsl n tm 0)] in

2626 expandDo dsl sc

2727expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

2828expandDo dsl (PLet n ty v tm)

2929 | Just letb <- dsl_let dsl

30− = let sc = PApp (FC "(dsl)" 0) letb [pexp v, pexp (var dsl n tm 0)] in

30+ = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in

3131 expandDo dsl sc

3232expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

3333expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

src/Idris/Delaborate.hs+1−1

@@ -30,7 +30,7 @@ delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

3030 -> Term -> Bool -> PTerm

3131delabTy' ist imps tm fullname = de [] imps tm

3232 where

33− un = FC "(val)" 0

33+ un = fileFC "(val)"

3434

3535 de env _ (App f a) = deFn env f [a]

3636 de env _ (V i) | i < length env = PRef un (snd (env!!i))

src/Idris/ElabDecls.hs+7−7

@@ -220,7 +220,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

220220

221221elabPrims :: Idris ()

222222elabPrims = do mapM_ (elabDecl EAll toplevel)

223− (map (PData "" defaultSyntax (FC "builtin" 0) False)

223+ (map (PData "" defaultSyntax (fileFC "builtin") False)

224224 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

225225 mapM_ elabPrim primitives

226226 -- Special case prim__believe_me because it doesn't work on just constants

@@ -746,15 +746,15 @@ elabVal info aspat tm_in

746746-- (build i info aspat (MN 0 "val") tm))

747747 tclift (elaborate ctxt (MN 0 "val") infP []

748748 (build i info aspat (MN 0 "val") (infTerm tm)))

749− def' <- checkDef (FC "(input)" 0) defer

749+ def' <- checkDef (fileFC "(input)") defer

750750 addDeferred def'

751751 mapM_ (elabCaseBlock info []) is

752752

753753 logLvl 3 ("Value: " ++ show tm')

754− recheckC (FC "(input)" 0) [] tm'

754+ recheckC (fileFC "(input)") [] tm'

755755 let vtm = getInferTerm tm'

756756 logLvl 2 (show vtm)

757− recheckC (FC "(input)" 0) [] vtm

757+ recheckC (fileFC "(input)") [] vtm

758758

759759-- checks if the clause is a possible left hand side. Returns the term if

760760-- possible, otherwise Nothing.

@@ -1051,7 +1051,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

10511051 logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++

10521052 showImp Nothing True False toplhs)

10531053 case matchClause i toplhs tm of

1054− Left f -> ifail $ show fc ++ ":with clause does not match top level"

1054+ Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")

10551055 Right mvars ->

10561056 do logLvl 3 ("Match vars : " ++ show mvars)

10571057 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

@@ -1063,7 +1063,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

10631063 showImp Nothing True False toplhs)

10641064 withs' <- mapM (mkAuxC wname toplhs ns ns') withs

10651065 case matchClause i toplhs tm of

1066− Left _ -> ifail $ show fc ++ "with clause does not match top level"

1066+ Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")

10671067 Right mvars ->

10681068 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

10691069 return $ PWith fc wname lhs ws wval withs'

@@ -1190,7 +1190,7 @@ elabClass info syn doc fc constraints tn ps ds

11901190 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

11911191 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

11921192 let lhs = PApp fc (PRef fc cfn) [pconst capp]

1193− let rhs = PResolveTC (FC "HACK" 0)

1193+ let rhs = PResolveTC (fileFC "HACK")

11941194 let ty = PPi constraint (MN 0 "pc") c con

11951195 iLOG (showImp Nothing True False ty)

11961196 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

src/Idris/ElabTerm.hs+4−4

@@ -149,7 +149,7 @@ elab ist info pattern tcgen fn tm

149149 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))

150150 (elab' ina (PRef fc unitTy))

151151 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

152− elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes

152+ elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

153153 = resolveTC 5 fn ist

154154 elab' ina (PResolveTC fc)

155155 | True = do c <- unique_hole (MN 0 "class")

@@ -548,7 +548,7 @@ elab ist info pattern tcgen fn tm

548548 PAlternative True (map (mkCoerce t) cs)]

549549 return t'

550550 where

551− mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears!

551+ mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!

552552 addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

553553

554554 elabArgs ina failed fc retry [] _

@@ -633,7 +633,7 @@ pruneByType t _ as = as

633633

634634trivial :: IState -> ElabD ()

635635trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

636− (PRefl (FC "prf" 0) Placeholder)

636+ (PRefl (fileFC "prf") Placeholder)

637637 return ())

638638 (do env <- get_env

639639 g <- goal

@@ -647,7 +647,7 @@ trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

647647 g <- goal

648648 if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))

649649 then try' (elab ist toplevel False False

650− (MN 0 "tac") (PRef (FC "prf" 0) x))

650+ (MN 0 "tac") (PRef (fileFC "prf") x))

651651 (tryAll xs) True

652652 else tryAll xs

653653

src/Idris/Error.hs+5−3

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

5050

5151tclift :: TC a -> Idris a

5252tclift (OK v) = return v

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

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

5454tclift (Error err) = throwError err

5555

5656tctry :: TC a -> TC a -> Idris a

@@ -60,7 +60,9 @@ tctry tc1 tc2

6060 Error err -> tclift tc2

6161

6262getErrLine :: Err -> Int

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

63+getErrLine (At (FC _ l _) _) = l

6464getErrLine _ = 0

6565

66−

66+getErrColumn :: Err -> Int

67+getErrColumn (At (FC _ _ c) _) = c

68+getErrColumn _ = 0

src/Idris/IBC.hs+5−3

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 41

26+ibcVersion = 42

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

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

346346 return (CGInfo x1 x2 x3 x4 x5)

347347

348348instance Binary FC where

349− put (FC x1 x2)

349+ put (FC x1 x2 x3)

350350 = do put x1

351351 put x2

352+ put x3

352353 get

353354 = do x1 <- get

354355 x2 <- get

355− return (FC x1 x2)

356+ x3 <- get

357+ return (FC x1 x2 x3)

356358

357359

358360instance Binary Name where

src/Idris/ParseHelpers.hs+7−1

@@ -254,13 +254,19 @@ fileName _ = "(interactive)"

254254lineNum :: Delta -> Int

255255lineNum (Lines l _ _ _) = fromIntegral l + 1

256256lineNum (Directed _ l _ _ _) = fromIntegral l + 1

257+lineNum _ = 0

258+

259+{- | Get column number from position -}

260+columnNum :: Delta -> Int

261+columnNum pos = fromIntegral (column pos) + 1

262+

257263

258264{- | Get file position as FC -}

259265getFC :: MonadicParsing m => m FC

260266getFC = do s <- position

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

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

263− return $ FC f (lineNum s)

269+ return $ FC f (lineNum s) (columnNum s)

264270

265271{-* Syntax helpers-}

266272-- | Bind constraints to term

src/Idris/Parser.hs+1−1

@@ -1032,7 +1032,7 @@ loadSource lidr f

10321032 toMutual :: PDecl -> PDecl

10331033 toMutual m@(PMutual _ d) = m

10341034 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

1035− toMutual x = let r = PMutual (FC "single mutual" 0) [x] in

1035+ toMutual x = let r = PMutual (fileFC "single mutual") [x] in

10361036 case x of

10371037 PClauses _ _ _ _ -> r

10381038 PClass _ _ _ _ _ _ _ -> r

src/Idris/Prover.hs+2−2

@@ -65,9 +65,9 @@ prove ctxt lit n ty

6565 ideslavePutSExp "end-proof-mode" n

6666 let proofs = proof_list i

6767 putIState (i { proof_list = (n, prf) : proofs })

68− let tree = simpleCase False True False CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]

68+ let tree = simpleCase False True False CompileTime (fileFC "proof") [([], P Ref n ty, tm)]

6969 logLvl 3 (show tree)

70− (ptm, pty) <- recheckC (FC "proof" 0) [] tm

70+ (ptm, pty) <- recheckC (fileFC "proof") [] tm

7171 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

7272 "Expected type:" ++ show ty)

7373 case converts ctxt [] ty pty of

src/Idris/REPL.hs+3−3

@@ -491,7 +491,7 @@ process fn (Prove n')

491491 prover (lit fn) n

492492 -- recheck totality

493493 i <- getIState

494− totcheck (FC "(input)" 0, n)

494+ totcheck (fileFC "(input)", n)

495495 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

496496 mapM_ checkDeclTotality (idris_totcheck i)

497497

@@ -522,13 +522,13 @@ process fn Execute = do (m, _) <- elabVal toplevel False

522522 compile t tmpn m

523523 runIO $ system tmpn

524524 return ()

525− where fc = FC "main" 0

525+ where fc = fileFC "main"

526526process fn (Compile codegen f)

527527 = do (m, _) <- elabVal toplevel False

528528 (PApp fc (PRef fc (UN "run__IO"))

529529 [pexp $ PRef fc (NS (UN "main") ["Main"])])

530530 compile codegen f m

531− where fc = FC "main" 0

531+ where fc = fileFC "main"

532532process fn (LogLvl i) = setLogLevel i

533533-- Elaborate as if LHS of a pattern (debug command)

534534process fn (Pattelab t)

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

28−chkAdj f l Comm Prog = tfail $ At (FC f l) ProgramLineComment

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?

2929chkAdj f l _ _ = return ()

3030

3131

test/reg003/expected+4−4

@@ -1,7 +1,7 @@

1−reg003a.idr:4:When elaborating constructor ECons:

1+reg003a.idr:4:20:When elaborating constructor ECons:

22No such variable OddList

3−reg003a.idr:7:When elaborating constructor OCons:

3+reg003a.idr:7:20:When elaborating constructor OCons:

44No such variable EvenList

5−reg003a.idr:9:When elaborating type of test:

5+reg003a.idr:9:8:When elaborating type of test:

66No such variable EvenList

7−reg003a.idr:10:No type declaration for test

7+reg003a.idr:10:1:No type declaration for test

test/reg006/expected+1−1

@@ -1 +1 @@

1−reg006.idr:17:RBTree.lookup is possibly not total due to: RBTree.case block in lookup

1+reg006.idr:17:1:RBTree.lookup is possibly not total due to: RBTree.case block in lookup

test/reg007/expected+2−2

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

1−reg007.lidr:8:A.n is already defined

2−reg007.lidr:12:When elaborating right hand side of hurrah:

1+reg007.lidr:8:1:A.n is already defined

2+reg007.lidr:12:9:When elaborating right hand side of hurrah:

33Can't unify

44 [92mn[0m[94m = [0m[92mA.lala[0m

55with

test/reg010/expected+1−1

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

1−reg010.idr:5:When elaborating right hand side of usubst.unsafeSubst:

1+reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst:

22Can't unify

33 P x

44with

test/reg018/expected+4−4

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

1−reg018a.idr:16:conat.minusCoNat is not productive

2−reg018b.idr:8:A.showB is possibly not total due to recursive path A.showB

3−reg018c.idr:19:CodataTest.inf is not productive

4−reg018d.idr:5:Main.pull is not total as there are missing cases

1+reg018a.idr:16:1:conat.minusCoNat is not productive

2+reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

3+reg018c.idr:19:1:CodataTest.inf is not productive

4+reg018d.idr:5:1:Main.pull is not total as there are missing cases

test/reg023/expected+1−1

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

1−reg023.idr:7:When elaborating right hand side of bad:

1+reg023.idr:7:5:When elaborating right hand side of bad:

22Can't unify

33 [94mNat[0m

44with

test/test003/expected+1−1

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

1−./test003a.lidr:1:Program line next to comment

1+./test003a.lidr:1:0:Program line next to comment

22a

33d

44zabcdefg

test/test010/expected+3−3

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

1−test010.idr:13:foo is possibly not total due to: MkBad

2−test010a.idr:9:main.bar is possibly not total due to: main.MkBad

3−test010b.idr:9:main.bar is possibly not total due to: main.MkBad

1+test010.idr:13:1:foo is possibly not total due to: MkBad

2+test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad

3+test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad

test/test012/expected+1−1

@@ -1 +1 @@

1−test012a.idr:7:x is not an accessible pattern variable

1+test012a.idr:7:1:x is not an accessible pattern variable

test/test017/expected+2−2

@@ -1,2 +1,2 @@

1−test017a.idr:5:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

2−test017b.idr:4:foo.foo is possibly not total due to recursive path foo.foo

1+test017a.idr:5:1:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

2+test017b.idr:4:1:foo.foo is possibly not total due to recursive path foo.foo

test/test020/expected+1−1

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

11When elaborating right hand side of foo:

2−test020a.idr:14:Can't unify

2+test020a.idr:14:18:Can't unify

33 Vect n a

44with

55 List a

test/test030/expected+1−1

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

1−test030a.idr:12:When elaborating right hand side of testReflect1:

1+test030a.idr:12:14:When elaborating right hand side of testReflect1:

22Can't unify

33 IsJust (Just x)

44with