ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

Added column name to source

Browse Source
This commit is contained in:
Ahmad Salim Al-Sibahi 2013-10-19 20:10:41 +02:00
parent d2f54804d7
commit 57c8657372
29 changed files with 94 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
idris.cabal
View File

@ -1,5 +1,5 @@
Name: idris
Version: 0.9.9.3
Version: 0.9.9.4
License: BSD3
License-file: LICENSE
Author: Edwin Brady

2
src/Core/Constraints.hs
View File

@ -38,7 +38,7 @@ mkRels ((c, f) : cs) acc
acyclic :: Relations -> [UExp] -> TC ()
acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs
where
checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
checkCycle fc r path inc [] = return ()

10
src/Core/Evaluate.hs
View File

@ -700,10 +700,10 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)
access = case lookupDefAcc n False uctxt of
[(_, acc)] -> acc
_ -> Public
ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps_tot,
simpleCase tcase covering reflect CompileTime (FC "" 0) ps_ct,
simpleCase tcase covering reflect CompileTime (FC "" 0) ps_inl,
simpleCase tcase covering reflect RunTime (FC "" 0) ps_rt) of
ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC ps_tot,
simpleCase tcase covering reflect CompileTime emptyFC ps_ct,
simpleCase tcase covering reflect CompileTime emptyFC ps_inl,
simpleCase tcase covering reflect RunTime emptyFC ps_rt) of
(OK (CaseDef args_tot sc_tot _),
OK (CaseDef args_ct sc_ct _),
OK (CaseDef args_inl sc_inl _),
@ -730,7 +730,7 @@ simplifyCasedef n uctxt
[(CaseOp ci ty ps_in ps cd, acc, tot)] ->
let ps_in' = map simpl ps_in
pdef = map debind ps_in' in
case simpleCase False True False CompileTime (FC "" 0) pdef of
case simpleCase False True False CompileTime emptyFC pdef of
OK (CaseDef args sc _) ->
addDef n (CaseOp ci
ty ps_in' ps (cd { cases_totcheck = (args, sc) }),

21
src/Core/TT.hs
View File

@ -38,20 +38,29 @@ data Option = TTypeInTType
| CheckConv
deriving Eq
-- | Source location. These are typically produced by the parser 'Idris.Parser.pfc'
-- | Source location. These are typically produced by the parser 'Idris.Parser.getFC'
data FC = FC { fc_fname :: String, -- ^ Filename
fc_line :: Int -- ^ Line number
}
deriving Eq
fc_line :: Int, -- ^ Line number
fc_column :: Int -- ^ Column number
} deriving Eq
-- | Empty source location
emptyFC :: FC
emptyFC = fileFC ""
-- | Source location with file only
fileFC :: String -> FC
fileFC s = FC s 0 0
{-!
deriving instance Binary FC
!-}
instance Sized FC where
size (FC f l) = 1 + length f
size (FC f l c) = 1 + length f
instance Show FC where
show (FC f l) = f ++ ":" ++ show l
show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c
data Err = Msg String
| InternalMsg String

11
src/Idris/AbsSyntax.hs
View File

@ -314,7 +314,10 @@ iputStrLn s = do i <- getIState
(fn, ':':rest) -> case span isDigit rest of
([], ':':msg) -> write
([], msg) -> write
(num, ':':msg) -> iWarn (FC fn (read num)) msg
(row, ':':rest') ->
case span isDigit rest' of
([], msg) -> iWarn (FC fn (read row) 0) msg
(col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg
_ -> write
where write = runIO . putStrLn $ convSExp "write-string" s n
@ -576,7 +579,7 @@ setTypeCase t = do i <- getIState
-- For inferring types of things
bi = FC "builtin" 0
bi = fileFC "builtin"
inferTy = MN 0 "__Infer"
inferCon = MN 0 "__infer"
@ -1417,8 +1420,8 @@ substMatchShadow n shs tm t = sm shs t where
sm xs (PPi p x t sc)
| x `elem` xs
= let x' = nextName x in
PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))
(sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))
PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
(sm (x':xs) (substMatch x (PRef emptyFC x') sc))
| otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

10
src/Idris/AbsSyntaxTree.hs
View File

@ -561,7 +561,7 @@ data PTerm = PQuote Raw
| PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
| PUnifyLog PTerm -- ^ dump a trace of unifications when building term
| PNoImplicits PTerm -- ^ never run implicit converions on the term
deriving Eq
deriving (Eq, Show)
{-!
deriving instance Binary PTerm
!-}
@ -642,7 +642,7 @@ data PDo' t = DoExp FC t
| DoBindP FC t t
| DoLet FC Name t t
| DoLetP FC t t
deriving (Eq, Functor)
deriving (Eq, Functor, Show)
{-!
deriving instance Binary PDo'
!-}
@ -774,7 +774,7 @@ initDSL = DSL (PRef f (UN ">>="))
Nothing
Nothing
Nothing
where f = FC "(builtin)" 0
where f = fileFC "(builtin)"
data Using = UImplicit Name PTerm
| UConstraint Name [Name]
@ -807,8 +807,8 @@ expandNS syn n = case syn_namespace syn of
--- Pretty printing declarations and terms
instance Show PTerm where
show tm = showImp Nothing False False tm
{-instance Show PTerm where-}
{-show tm = showImp Nothing False False tm-}
instance Pretty PTerm where
pretty = prettyImp False

4
src/Idris/DSL.hs
View File

@ -22,12 +22,12 @@ desugar syn i t = let t' = expandDo (dsl_info syn) t in
expandDo :: DSL -> PTerm -> PTerm
expandDo dsl (PLam n ty tm)
| Just lam <- dsl_lambda dsl
= let sc = PApp (FC "(dsl)" 0) lam [pexp (var dsl n tm 0)] in
= let sc = PApp (fileFC "(dsl)") lam [pexp (var dsl n tm 0)] in
expandDo dsl sc
expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)
expandDo dsl (PLet n ty v tm)
| Just letb <- dsl_let dsl
= let sc = PApp (FC "(dsl)" 0) letb [pexp v, pexp (var dsl n tm 0)] in
= let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in
expandDo dsl sc
expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

2
src/Idris/Delaborate.hs
View File

@ -30,7 +30,7 @@ delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any
-> Term -> Bool -> PTerm
delabTy' ist imps tm fullname = de [] imps tm
where
un = FC "(val)" 0
un = fileFC "(val)"
de env _ (App f a) = deFn env f [a]
de env _ (V i) | i < length env = PRef un (snd (env!!i))

14
src/Idris/ElabDecls.hs
View File

@ -220,7 +220,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
elabPrims :: Idris ()
elabPrims = do mapM_ (elabDecl EAll toplevel)
(map (PData "" defaultSyntax (FC "builtin" 0) False)
(map (PData "" defaultSyntax (fileFC "builtin") False)
[inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
mapM_ elabPrim primitives
-- Special case prim__believe_me because it doesn't work on just constants
@ -746,15 +746,15 @@ elabVal info aspat tm_in
-- (build i info aspat (MN 0 "val") tm))
tclift (elaborate ctxt (MN 0 "val") infP []
(build i info aspat (MN 0 "val") (infTerm tm)))
def' <- checkDef (FC "(input)" 0) defer
def' <- checkDef (fileFC "(input)") defer
addDeferred def'
mapM_ (elabCaseBlock info []) is
logLvl 3 ("Value: " ++ show tm')
recheckC (FC "(input)" 0) [] tm'
recheckC (fileFC "(input)") [] tm'
let vtm = getInferTerm tm'
logLvl 2 (show vtm)
recheckC (FC "(input)" 0) [] vtm
recheckC (fileFC "(input)") [] vtm
-- checks if the clause is a possible left hand side. Returns the term if
-- possible, otherwise Nothing.
@ -1051,7 +1051,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
showImp Nothing True False toplhs)
case matchClause i toplhs tm of
Left f -> ifail $ show fc ++ ":with clause does not match top level"
Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")
Right mvars ->
do logLvl 3 ("Match vars : " ++ show mvars)
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)
showImp Nothing True False toplhs)
withs' <- mapM (mkAuxC wname toplhs ns ns') withs
case matchClause i toplhs tm of
Left _ -> ifail $ show fc ++ "with clause does not match top level"
Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")
Right mvars ->
do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w
return $ PWith fc wname lhs ws wval withs'
@ -1190,7 +1190,7 @@ elabClass info syn doc fc constraints tn ps ds
let mnames = take (length all) $ map (\x -> MN x "meth") [0..]
let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
let lhs = PApp fc (PRef fc cfn) [pconst capp]
let rhs = PResolveTC (FC "HACK" 0)
let rhs = PResolveTC (fileFC "HACK")
let ty = PPi constraint (MN 0 "pc") c con
iLOG (showImp Nothing True False ty)
iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

8
src/Idris/ElabTerm.hs
View File

@ -149,7 +149,7 @@ elab ist info pattern tcgen fn tm
elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
(elab' ina (PRef fc unitTy))
elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes
elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
= resolveTC 5 fn ist
elab' ina (PResolveTC fc)
| True = do c <- unique_hole (MN 0 "class")
@ -548,7 +548,7 @@ elab ist info pattern tcgen fn tm
PAlternative True (map (mkCoerce t) cs)]
return t'
where
mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears!
mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!
addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])
elabArgs ina failed fc retry [] _
@ -633,7 +633,7 @@ pruneByType t _ as = as
trivial :: IState -> ElabD ()
trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")
(PRefl (FC "prf" 0) Placeholder)
(PRefl (fileFC "prf") Placeholder)
return ())
(do env <- get_env
g <- goal
@ -647,7 +647,7 @@ trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")
g <- goal
if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))
then try' (elab ist toplevel False False
(MN 0 "tac") (PRef (FC "prf" 0) x))
(MN 0 "tac") (PRef (fileFC "prf") x))
(tryAll xs) True
else tryAll xs

8
src/Idris/Error.hs
View File

@ -50,7 +50,7 @@ ierror = throwError
tclift :: TC a -> Idris a
tclift (OK v) = return v
tclift (Error err@(At (FC f l) e)) = do setErrLine l ; throwError err
tclift (Error err@(At (FC f l c) e)) = do setErrLine l ; throwError err
tclift (Error err) = throwError err
tctry :: TC a -> TC a -> Idris a
@ -60,7 +60,9 @@ tctry tc1 tc2
Error err -> tclift tc2
getErrLine :: Err -> Int
getErrLine (At (FC _ l) _) = l
getErrLine (At (FC _ l _) _) = l
getErrLine _ = 0
getErrColumn :: Err -> Int
getErrColumn (At (FC _ _ c) _) = c
getErrColumn _ = 0

6
src/Idris/IBC.hs
View File

@ -346,13 +346,15 @@ instance Binary CGInfo where
return (CGInfo x1 x2 x3 x4 x5)
instance Binary FC where
put (FC x1 x2)
put (FC x1 x2 x3)
= do put x1
put x2
put x3
get
= do x1 <- get
x2 <- get
return (FC x1 x2)
x3 <- get
return (FC x1 x2 x3)
instance Binary Name where

8
src/Idris/ParseHelpers.hs
View File

@ -254,13 +254,19 @@ fileName _ = "(interactive)"
lineNum :: Delta -> Int
lineNum (Lines l _ _ _) = fromIntegral l + 1
lineNum (Directed _ l _ _ _) = fromIntegral l + 1
lineNum _ = 0
{- | Get column number from position -}
columnNum :: Delta -> Int
columnNum pos = fromIntegral (column pos) + 1
{- | Get file position as FC -}
getFC :: MonadicParsing m => m FC
getFC = do s <- position
let (dir, file) = splitFileName (fileName s)
let f = if dir == addTrailingPathSeparator "." then file else fileName s
return $ FC f (lineNum s)
return $ FC f (lineNum s) (columnNum s)
{-* Syntax helpers-}
-- | Bind constraints to term

2
src/Idris/Parser.hs
View File

@ -1032,7 +1032,7 @@ loadSource lidr f
toMutual :: PDecl -> PDecl
toMutual m@(PMutual _ d) = m
toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
toMutual x = let r = PMutual (fileFC "single mutual") [x] in
case x of
PClauses _ _ _ _ -> r
PClass _ _ _ _ _ _ _ -> r

4
src/Idris/Prover.hs
View File

@ -65,9 +65,9 @@ prove ctxt lit n ty
ideslavePutSExp "end-proof-mode" n
let proofs = proof_list i
putIState (i { proof_list = (n, prf) : proofs })
let tree = simpleCase False True False CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
let tree = simpleCase False True False CompileTime (fileFC "proof") [([], P Ref n ty, tm)]
logLvl 3 (show tree)
(ptm, pty) <- recheckC (FC "proof" 0) [] tm
(ptm, pty) <- recheckC (fileFC "proof") [] tm
logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
"Expected type:" ++ show ty)
case converts ctxt [] ty pty of

6
src/Idris/REPL.hs
View File

@ -491,7 +491,7 @@ process fn (Prove n')
prover (lit fn) n
-- recheck totality
i <- getIState
totcheck (FC "(input)" 0, n)
totcheck (fileFC "(input)", n)
mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)
mapM_ checkDeclTotality (idris_totcheck i)
@ -522,13 +522,13 @@ process fn Execute = do (m, _) <- elabVal toplevel False
compile t tmpn m
runIO $ system tmpn
return ()
where fc = FC "main" 0
where fc = fileFC "main"
process fn (Compile codegen f)
= do (m, _) <- elabVal toplevel False
(PApp fc (PRef fc (UN "run__IO"))
[pexp $ PRef fc (NS (UN "main") ["Main"])])
compile codegen f m
where fc = FC "main" 0
where fc = fileFC "main"
process fn (LogLvl i) = setLogLevel i
-- Elaborate as if LHS of a pattern (debug command)
process fn (Pattelab t)

4
src/Idris/Unlit.hs
View File

@ -24,8 +24,8 @@ check f l [x] = return ()
check f l [] = return ()
chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()
chkAdj f l Prog Comm = tfail $ At (FC f l) ProgramLineComment
chkAdj f l Comm Prog = tfail $ At (FC f l) ProgramLineComment
chkAdj f l Prog Comm = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column?
chkAdj f l Comm Prog = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column?
chkAdj f l _ _ = return ()

8
test/reg003/expected
View File

@ -1,7 +1,7 @@
reg003a.idr:4:When elaborating constructor ECons:
reg003a.idr:4:20:When elaborating constructor ECons:
No such variable OddList
reg003a.idr:7:When elaborating constructor OCons:
reg003a.idr:7:20:When elaborating constructor OCons:
No such variable EvenList
reg003a.idr:9:When elaborating type of test:
reg003a.idr:9:8:When elaborating type of test:
No such variable EvenList
reg003a.idr:10:No type declaration for test
reg003a.idr:10:1:No type declaration for test

2
test/reg006/expected
View File

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

4
test/reg007/expected
View File

@ -1,5 +1,5 @@
reg007.lidr:8:A.n is already defined
reg007.lidr:12:When elaborating right hand side of hurrah:
reg007.lidr:8:1:A.n is already defined
reg007.lidr:12:9:When elaborating right hand side of hurrah:
Can't unify
n = A.lala
with

2
test/reg010/expected
View File

@ -1,4 +1,4 @@
reg010.idr:5:When elaborating right hand side of usubst.unsafeSubst:
reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst:
Can't unify
P x
with

8
test/reg018/expected
View File

@ -1,4 +1,4 @@
reg018a.idr:16:conat.minusCoNat is not productive
reg018b.idr:8:A.showB is possibly not total due to recursive path A.showB
reg018c.idr:19:CodataTest.inf is not productive
reg018d.idr:5:Main.pull is not total as there are missing cases
reg018a.idr:16:1:conat.minusCoNat is not productive
reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB
reg018c.idr:19:1:CodataTest.inf is not productive
reg018d.idr:5:1:Main.pull is not total as there are missing cases

2
test/reg023/expected
View File

@ -1,4 +1,4 @@
reg023.idr:7:When elaborating right hand side of bad:
reg023.idr:7:5:When elaborating right hand side of bad:
Can't unify
Nat
with

2
test/test003/expected
View File

@ -1,4 +1,4 @@
./test003a.lidr:1:Program line next to comment
./test003a.lidr:1:0:Program line next to comment
a
d
zabcdefg

6
test/test010/expected
View File

@ -1,3 +1,3 @@
test010.idr:13:foo is possibly not total due to: MkBad
test010a.idr:9:main.bar is possibly not total due to: main.MkBad
test010b.idr:9:main.bar is possibly not total due to: main.MkBad
test010.idr:13:1:foo is possibly not total due to: MkBad
test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad
test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad

2
test/test012/expected
View File

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

4
test/test017/expected
View File

@ -1,2 +1,2 @@
test017a.idr:5:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
test017b.idr:4:foo.foo is possibly not total due to recursive path foo.foo
test017a.idr:5:1:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
test017b.idr:4:1:foo.foo is possibly not total due to recursive path foo.foo

2
test/test020/expected
View File

@ -1,5 +1,5 @@
When elaborating right hand side of foo:
test020a.idr:14:Can't unify
test020a.idr:14:18:Can't unify
Vect n a
with
List a

2
test/test030/expected
View File

@ -1,4 +1,4 @@
test030a.idr:12:When elaborating right hand side of testReflect1:
test030a.idr:12:14:When elaborating right hand side of testReflect1:
Can't unify
IsJust (Just x)
with