95d90f4 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+7−7

@@ -1086,13 +1086,13 @@ expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

10861086 where

10871087 -- just do the type decl, leave constructors alone (parameters will be

10881088 -- added implicitly)

1089− expandPData (PDatadecl n ty cons)

1089+ expandPData (PDatadecl n nfc ty cons)

10901090 = if n `elem` ns

1091− then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))

1091+ then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))

10921092 (map econ cons)

1093− else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

1094− econ (doc, argDocs, n, t, fc, fs)

1095− = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

1093+ else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)

1094+ econ (doc, argDocs, n, nfc, t, fc, fs)

1095+ = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

10961096expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name prs pdocs fls cn cdoc csyn)

10971097 = d

10981098expandParamsD rhs ist dec ps ns (PParams f params pds)

@@ -1550,9 +1550,9 @@ addImpl' inpat env infns imp_meths ist ptm

15501550 = let as' = map (ai qq env ds) as in

15511551 PAlternative a as'

15521552 ai qq env _ (PDisamb ds' as) = ai qq env ds' as

1553− ai qq env ds (PApp fc (PInferRef _ f) as)

1553+ ai qq env ds (PApp fc (PInferRef ffc f) as)

15541554 = let as' = map (fmap (ai qq env ds)) as in

1555− PApp fc (PInferRef fc f) as'

1555+ PApp fc (PInferRef ffc f) as'

15561556 ai qq env ds (PApp fc ftm@(PRef ffc f) as)

15571557 | f `elem` infns = ai qq env ds (PApp fc (PInferRef ffc f) as)

15581558 | not (f `elem` map fst env)

src/Idris/AbsSyntaxTree.hs+24−23

@@ -705,11 +705,12 @@ deriving instance NFData PClause'

705705

706706-- | Data declaration

707707data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

708+ d_name_fc :: FC, -- ^ The precise location of the type constructor name

708709 d_tcon :: t, -- ^ Type constructor

709− d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors

710+ d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors

710711 }

711712 -- ^ Data declaration

712− | PLaterdecl { d_name :: Name, d_tcon :: t }

713+ | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }

713714 -- ^ "Placeholder" for data whose constructors are defined later

714715 deriving Functor

715716{-!

@@ -732,9 +733,9 @@ declared (PTy _ _ _ _ _ n fc t) = [n]

732733declared (PPostulate _ _ _ _ _ n t) = [n]

733734declared (PClauses _ _ n _) = [] -- not a declaration

734735declared (PCAF _ n _) = [n]

735−declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

736− where fstt (_, _, a, _, _, _) = a

737−declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

736+declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

737+ where fstt (_, _, a, _, _, _, _) = a

738+declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]

738739declared (PParams _ _ ds) = concatMap declared ds

739740declared (PNamespace _ ds) = concatMap declared ds

740741declared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

@@ -753,8 +754,8 @@ tldeclared (PTy _ _ _ _ _ n _ t) = [n]

753754tldeclared (PPostulate _ _ _ _ _ n t) = [n]

754755tldeclared (PClauses _ _ n _) = [] -- not a declaration

755756tldeclared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

756−tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

757− where fstt (_, _, a, _, _, _) = a

757+tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

758+ where fstt (_, _, a, _, _, _, _) = a

758759tldeclared (PParams _ _ ds) = []

759760tldeclared (PMutual _ ds) = concatMap tldeclared ds

760761tldeclared (PNamespace _ ds) = concatMap tldeclared ds

@@ -768,9 +769,9 @@ defined (PTy _ _ _ _ _ n _ t) = []

768769defined (PPostulate _ _ _ _ _ n t) = []

769770defined (PClauses _ _ n _) = [n] -- not a declaration

770771defined (PCAF _ n _) = [n]

771−defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

772− where fstt (_, _, a, _, _, _) = a

773−defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

772+defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

773+ where fstt (_, _, a, _, _, _, _) = a

774+defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []

774775defined (PParams _ _ ds) = concatMap defined ds

775776defined (PNamespace _ ds) = concatMap defined ds

776777defined (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

@@ -1260,9 +1261,9 @@ bi = fileFC "builtin"

12601261

12611262inferTy = sMN 0 "__Infer"

12621263inferCon = sMN 0 "__infer"

1263−inferDecl = PDatadecl inferTy

1264+inferDecl = PDatadecl inferTy NoFC

12641265 (PType bi)

1265− [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") NoFC (PType bi) (

1266+ [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (

12661267 PPi expl (sMN 0 "ival") NoFC (PRef bi (sMN 0 "iType"))

12671268 (PRef bi inferTy)), bi, [])]

12681269inferOpts = []

@@ -1317,16 +1318,16 @@ eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

13171318 "\n\n" ++

13181319 "You may need to use `(~=~)` to explicitly request heterogeneous equality."

13191320

1320−eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType bi), (n "B", PType bi)]

1321− (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1322− (PType bi)))

1321+eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]

1322+ (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1323+ (PType bi)))

13231324 [(reflDoc, reflParamDoc,

1324− eqCon, PPi impl (n "A") NoFC (PType bi) (

1325− PPi impl (n "x") NoFC (PRef bi (n "A"))

1326− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1327− pimp (n "B") Placeholder False,

1328− pexp (PRef bi (n "x")),

1329− pexp (PRef bi (n "x"))])), bi, [])]

1325+ eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (

1326+ PPi impl (n "x") NoFC (PRef bi (n "A"))

1327+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1328+ pimp (n "B") Placeholder False,

1329+ pexp (PRef bi (n "x")),

1330+ pexp (PRef bi (n "x"))])), bi, [])]

13301331 where n a = sUN a

13311332 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $

13321333 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

@@ -1772,9 +1773,9 @@ showCImp ppo (PWith _ n l ws r pn w)

17721773

17731774

17741775showDImp :: PPOption -> PData -> Doc OutputAnnotation

1775−showDImp ppo (PDatadecl n ty cons)

1776+showDImp ppo (PDatadecl n nfc ty cons)

17761777 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>

1777− (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))

1778+ (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))

17781779

17791780showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

17801781showDecls o ds = vsep (map (showDeclImp o) ds)

src/Idris/Core/TT.hs+17−3

@@ -49,14 +49,28 @@ data Option = TTypeInTType

4949 deriving Eq

5050

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

52−data FC = FC { fc_fname :: String, -- ^ Filename

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

52+data FC = FC { _fc_fname :: String, -- ^ Filename

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

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

5555 }

5656 | NoFC -- ^ Locations for machine-generated terms

57− | FileFC { fc_fname :: String } -- ^ Locations with file only

57+ | FileFC { _fc_fname :: String } -- ^ Locations with file only

5858 deriving (Data, Typeable, Ord)

5959

60+-- TODO: find uses and destroy them, doing this case analysis at call sites

61+-- | Give a notion of filename associated with an FC

62+fc_fname :: FC -> String

63+fc_fname (FC f _ _) = f

64+fc_fname NoFC = "(no file)"

65+fc_fname (FileFC f) = f

66+

67+-- TODO: find uses and destroy them, doing this case analysis at call sites

68+-- | Give a notion of filename associated with an FC

69+fc_start :: FC -> (Int, Int)

70+fc_start (FC _ start _) = start

71+fc_start NoFC = (0, 0)

72+fc_start (FileFC f) = (0, 0)

73+

6074-- | Get the largest span containing the two FCs

6175spanFC :: FC -> FC -> FC

6276spanFC (FC f start end) (FC f' start' end')

src/Idris/DeepSeq.hs+3−3

@@ -193,9 +193,9 @@ instance (NFData t) => NFData (PClause' t) where

193193 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

194194

195195instance (NFData t) => NFData (PData' t) where

196− rnf (PDatadecl x1 x2 x3)

197− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

198− rnf (PLaterdecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

196+ rnf (PDatadecl x1 x2 x3 x4)

197+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

198+ rnf (PLaterdecl x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

199199

200200instance NFData PTerm where

201201 rnf (PQuote x1) = rnf x1 `seq` ()

src/Idris/Elab/Class.hs+2−2

@@ -80,8 +80,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

8080 let cty = impbind ps $ conbind constraints

8181 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

8282 constraint

83− let cons = [(emptyDocstring, [], cn, cty, fc, [])]

84− let ddecl = PDatadecl tn tty cons

83+ let cons = [(emptyDocstring, [], cn, NoFC, cty, fc, [])]

84+ let ddecl = PDatadecl tn NoFC tty cons

8585 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

8686 -- Elaborate the data declaration

8787 elabData info (syn { no_imp = no_imp syn ++ mnames,

src/Idris/Elab/Data.hs+19−13

@@ -15,7 +15,7 @@ import Idris.Primitives

1515import Idris.Inliner

1616import Idris.PartialEval

1717import Idris.DeepSeq

18−import Idris.Output (iputStrLn, pshow, iWarn)

18+import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)

1919import IRTS.Lang

2020

2121import Idris.Elab.Type

@@ -51,7 +51,7 @@ import Data.List.Split (splitOn)

5151import Util.Pretty(pretty, text)

5252

5353elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()

54−elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

54+elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

5555 = do let codata = Codata `elem` opts

5656 iLOG (show (fc, doc))

5757 checkUndefined fc n

@@ -59,8 +59,9 @@ elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

5959

6060 addIBC (IBCDef n)

6161 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

62+ sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]

6263

63−elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

64+elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

6465 = do let codata = Codata `elem` opts

6566 iLOG (show fc)

6667 undef <- isUndefined fc n

@@ -116,6 +117,11 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

116117 -- create a case function

117118 when (DefaultCaseFun `elem` opts) $

118119 evalStateT (elabCaseFun False params n t dcons info) Map.empty

120+ -- Emit highlighting info

121+ sendHighlighting $ [(nfc, AnnName n Nothing Nothing Nothing)] ++

122+ map (\(_, _, n, nfc, _, _, _) ->

123+ (nfc, AnnName n Nothing Nothing Nothing))

124+ dcons

119125 where

120126 setDetaggable :: Name -> Idris ()

121127 setDetaggable n = do

@@ -194,7 +200,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

194200 | otherwise = count n ts

195201 mParam args (_ : rest) = Nothing : mParam args rest

196202

197− cname (_, _, n, _, _, _) = n

203+ cname (_, _, n, _, _, _, _) = n

198204

199205 -- Abuse of ElabInfo.

200206 -- TODO Contemplate whether the ElabInfo type needs modification.

@@ -212,9 +218,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

212218elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

213219 Type -> -- for unique kind checking

214220 Type -> -- data type's kind

215− (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->

221+ (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) ->

216222 Idris (Name, Type)

217−elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)

223+elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcenames)

218224 = do checkUndefined fc n

219225 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

220226 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

@@ -302,17 +308,17 @@ type EliminatorState = StateT (Map.Map String Int) Idris

302308-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

303309-- rename to caseFun to match updated intend

304310elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->

305− [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name])] ->

311+ [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])] ->

306312 ElabInfo -> EliminatorState ()

307313elabCaseFun ind paramPos n ty cons info = do

308314 elimLog $ "Elaborating case function"

309− put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

315+ put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

310316 let (cnstrs, _) = splitPi ty

311317 let (splittedTy@(pms, idxs)) = splitPms cnstrs

312318 generalParams <- namePis False pms

313319 motiveIdxs <- namePis False idxs

314320 let motive = mkMotive n paramPos generalParams motiveIdxs

315− consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do

321+ consTerms <- mapM (\(c@(_, _, cnm, _, _, _, _)) -> do

316322 let casefunt = if ind then "elim_" else "case_"

317323 name <- freshName $ casefunt ++ simpleName cnm

318324 consTerm <- extractConsTerm c generalParams

@@ -488,8 +494,8 @@ elabCaseFun ind paramPos n ty cons info = do

488494 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

489495 _ -> return implargs

490496

491− extractConsTerm :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

492− extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

497+ extractConsTerm :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

498+ extractConsTerm (doc, argDocs, cnm, _, ty, fc, fs) generalParameters = do

493499 let cons' = replaceParams paramPos generalParameters ty

494500 let (args, resTy) = splitPi cons'

495501 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

@@ -524,8 +530,8 @@ elabCaseFun ind paramPos n ty cons info = do

524530 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

525531 convertImplPi _ = Nothing

526532

527− generateEliminatorClauses :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

528− generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

533+ generateEliminatorClauses :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

534+ generateEliminatorClauses (doc, _, cnm, _, ty, fc, fs) cnsElim generalArgs generalParameters = do

529535 let cons' = replaceParams paramPos generalParameters ty

530536 let (args, resTy) = splitPi cons'

531537 i <- State.lift getIState

src/Idris/Elab/Record.hs+1−1

@@ -57,7 +57,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

5757

5858 -- Build data declaration for elaboration

5959 iLOG $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)

60− let datadecl = PDatadecl tyn tycon [(cdoc, dconsArgDocs, dconName, dconTy, fc, [])]

60+ let datadecl = PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

6161 elabData info rsyn doc paramDocs fc opts datadecl

6262

6363 iLOG $ "fieldsWithName " ++ show fieldsWithName

src/Idris/Elab/Term.hs+8−5

@@ -360,8 +360,8 @@ elab ist info emode opts fn tm

360360 claim tyn RType

361361 movelast tyn

362362 elab' ina (Just fc) (PApp fc (PRef fc eqTy)

363− [pimp (sUN "A") (PRef fc tyn) True,

364− pimp (sUN "B") (PRef fc tyn) False,

363+ [pimp (sUN "A") (PRef NoFC tyn) True,

364+ pimp (sUN "B") (PRef NoFC tyn) False,

365365 pexp l, pexp r]))

366366 (do atyn <- getNameFrom (sMN 0 "aqty")

367367 btyn <- getNameFrom (sMN 0 "bqty")

@@ -370,8 +370,8 @@ elab ist info emode opts fn tm

370370 claim btyn RType

371371 movelast btyn

372372 elab' ina (Just fc) (PApp fc (PRef fc eqTy)

373− [pimp (sUN "A") (PRef fc atyn) True,

374− pimp (sUN "B") (PRef fc btyn) False,

373+ [pimp (sUN "A") (PRef NoFC atyn) True,

374+ pimp (sUN "B") (PRef NoFC btyn) False,

375375 pexp l, pexp r]))

376376

377377 elab' ina _ (PEq fc lt rt l r) = elab' ina (Just fc) (PApp fc (PRef fc eqTy)

@@ -1080,9 +1080,12 @@ elab ist info emode opts fn tm

10801080 end_unify

10811081

10821082 -- We now have an elaborated term. Reflect it and solve the

1083− -- original goal in the original proof state.

1083+ -- original goal in the original proof state, preserving highlighting

10841084 env <- get_env

1085+ EState _ _ _ hs <- getAux

10851086 loadState

1087+ updateAux (\aux -> aux { highlighting = hs })

1088+

10861089 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

10871090 isRaw = case unApply (normaliseAll ctxt env finalTy) of

10881091 (P _ n _, []) | n == reflm "Raw" -> True

src/Idris/ElabDecls.hs+1−1

@@ -173,7 +173,7 @@ elabDecl' what info (PData doc argDocs s f co d)

173173 elabData info s doc argDocs f co d

174174 | otherwise

175175 = do iLOG $ "Elaborating [type of] " ++ show (d_name d)

176− elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_tcon d))

176+ elabData info s doc argDocs f co (PLaterdecl (d_name d) (d_name_fc d) (d_tcon d))

177177elabDecl' what info d@(PClauses f o n ps)

178178 | what /= ETypes

179179 = do iLOG $ "Elaborating clause " ++ show n

src/Idris/IBC.hs+13−9

@@ -1455,23 +1455,27 @@ instance (Binary t) => Binary (PClause' t) where

14551455instance (Binary t) => Binary (PData' t) where

14561456 put x

14571457 = case x of

1458− PDatadecl x1 x2 x3 -> do putWord8 0

1459− put x1

1460− put x2

1461− put x3

1462− PLaterdecl x1 x2 -> do putWord8 1

1463− put x1

1464− put x2

1458+ PDatadecl x1 x2 x3 x4 -> do putWord8 0

1459+ put x1

1460+ put x2

1461+ put x3

1462+ put x4

1463+ PLaterdecl x1 x2 x3 -> do putWord8 1

1464+ put x1

1465+ put x2

1466+ put x3

14651467 get

14661468 = do i <- getWord8

14671469 case i of

14681470 0 -> do x1 <- get

14691471 x2 <- get

14701472 x3 <- get

1471− return (PDatadecl x1 x2 x3)

1473+ x4 <- get

1474+ return (PDatadecl x1 x2 x3 x4)

14721475 1 -> do x1 <- get

14731476 x2 <- get

1474− return (PLaterdecl x1 x2)

1477+ x3 <- get

1478+ return (PLaterdecl x1 x2 x3)

14751479 _ -> error "Corrupted binary data for PData'"

14761480

14771481instance Binary PunInfo where

src/Idris/ParseData.hs+15−15

@@ -191,20 +191,20 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

191191 | (n, d) <- argDocs ]

192192 return (doc', argDocs', acc, dataOpts))

193193 fc <- getFC

194− tyn_in <- fst <$> fnName

194+ (tyn_in, nfc) <- fnName

195195 (do try (lchar ':')

196196 popIndent

197197 ty <- typeExpr (allowImp syn)

198198 let tyn = expandNS syn tyn_in

199− option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

199+ option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

200200 reserved "where"

201201 cons <- indentedBlock (constructor syn)

202− accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons)

203− return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

202+ accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)

203+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))) <|> (do

204204 args <- many (fst <$> name)

205205 let ty = bindArgs (map (const (PType fc)) args) (PType fc)

206206 let tyn = expandNS syn tyn_in

207− option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

207+ option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

208208 try (lchar '=') <|> do reserved "where"

209209 let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

210210 let n = show tyn_in ++ " "

@@ -219,11 +219,11 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

219219 cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")

220220 terminator

221221 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

222− cons' <- mapM (\ (doc, argDocs, x, cargs, cfc, fs) ->

222+ cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

223223 do let cty = bindArgs cargs conty

224− return (doc, argDocs, x, cty, cfc, fs)) cons

225− accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons')

226− return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons')))

224+ return (doc, argDocs, x, xfc, cty, cfc, fs)) cons

225+ accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons')

226+ return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons')))

227227 <?> "data type declaration"

228228 where

229229 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

@@ -240,10 +240,10 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

240240{- | Parses a type constructor declaration

241241 Constructor ::= DocComment? FnName TypeSig;

242242-}

243−constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name])

243+constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])

244244constructor syn

245245 = do (doc, argDocs) <- option noDocs docComment

246− cn_in <- fst <$> fnName; fc <- getFC

246+ (cn_in, nfc) <- fnName; fc <- getFC

247247 let cn = expandNS syn cn_in

248248 lchar ':'

249249 fs <- option [] (do lchar '%'; reserved "erase"

@@ -253,23 +253,23 @@ constructor syn

253253 let doc' = annotCode (tryFullExpr syn ist) doc

254254 argDocs' = [ (n, annotCode (tryFullExpr syn ist) d)

255255 | (n, d) <- argDocs ]

256− return (doc', argDocs', cn, ty, fc, fs)

256+ return (doc', argDocs', cn, nfc, ty, fc, fs)

257257 <?> "constructor"

258258

259259{- | Parses a constructor for simple discriminated union data types

260260 SimpleConstructor ::= FnName SimpleExpr* DocComment?

261261-}

262−simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, [PTerm], FC, [Name])

262+simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name])

263263simpleConstructor syn

264264 = do (doc, _) <- option noDocs (try docComment)

265265 ist <- get

266266 let doc' = annotCode (tryFullExpr syn ist) doc

267− cn_in <- fst <$> fnName

267+ (cn_in, nfc) <- fnName

268268 let cn = expandNS syn cn_in

269269 fc <- getFC

270270 args <- many (do notEndApp

271271 simpleExpr syn)

272− return (doc', [], cn, args, fc, [])

272+ return (doc', [], cn, nfc, args, fc, [])

273273 <?> "constructor"

274274

275275{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+19−14

@@ -1082,23 +1082,28 @@ ExprList ::=

10821082@

10831083 -}

10841084listExpr :: SyntaxInfo -> IdrisParser PTerm

1085−listExpr syn = do lchar '['; fc <- getFC;

1086− try ((lchar ']' <?> "end of list expression") *> return (mkList fc [])) <|> (do

1087− x <- expr syn <?> "expression"

1088− (do try (lchar '|') <?> "list comprehension"

1089− qs <- sepBy1 (do_ syn) (lchar ',')

1090− lchar ']'

1091− return (PDoBlock (map addGuard qs ++

1092− [DoExp fc (PApp fc (PRef fc (sUN "return"))

1093− [pexp x])]))) <|> (do

1094− xs <- many ((lchar ',' <?> "list element") *> expr syn)

1095− lchar ']' <?> "end of list expression"

1096− return (mkList fc (x:xs))))

1085+listExpr syn = do (FC f (l, c) _) <- getFC

1086+ lchar '['; fc <- getFC;

1087+ (try . token $ do (char ']' <?> "end of list expression")

1088+ (FC _ _ (l', c')) <- getFC

1089+ return (mkNil (FC f (l, c) (l', c'))))

1090+ <|> (do x <- expr syn <?> "expression"

1091+ (do try (lchar '|') <?> "list comprehension"

1092+ qs <- sepBy1 (do_ syn) (lchar ',')

1093+ lchar ']'

1094+ return (PDoBlock (map addGuard qs ++

1095+ [DoExp fc (PApp fc (PRef fc (sUN "return"))

1096+ [pexp x])]))) <|>

1097+ (do xs <- many ((lchar ',' <?> "list element") *> expr syn)

1098+ lchar ']' <?> "end of list expression"

1099+ return (mkList fc (x:xs))))

10971100 <?> "list expression"

10981101 where

1102+ mkNil :: FC -> PTerm

1103+ mkNil fc = PRef fc (sUN "Nil")

10991104 mkList :: FC -> [PTerm] -> PTerm

1100− mkList fc [] = PRef fc (sUN "Nil")

1101− mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]

1105+ mkList fc [] = PRef NoFC (sUN "Nil")

1106+ mkList fc (x : xs) = PApp fc (PRef NoFC (sUN "::")) [pexp x, pexp (mkList fc xs)]

11021107 addGuard :: PDo -> PDo

11031108 addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))

11041109 [pexp e])

src/Idris/ParseHelpers.hs+9

@@ -373,6 +373,15 @@ operator = do op <- token . some $ operatorLetter

373373 fail $ op ++ " is not a valid operator"

374374 return op

375375

376+-- | Parses an operator

377+operatorFC :: MonadicParsing m => m (String, FC)

378+operatorFC = do (op, fc) <- token $ do (FC f (l, c) _) <- getFC

379+ op <- some operatorLetter

380+ return (op, FC f (l, c) (l, c + length op))

381+ when (op `elem` (invalidOperators ++ commentMarkers)) $

382+ fail $ op ++ " is not a valid operator"

383+ return (op, fc)

384+

376385{- * Position helpers -}

377386{- | Get filename from position (returns "(interactive)" when no source file is given) -}

378387fileName :: Delta -> String

src/Idris/Parser.hs+6−6

@@ -924,13 +924,13 @@ clause syn

924924 ist <- get

925925 put (ist { lastParse = Just n })

926926 return $ PClause fc n capp [] r wheres

927− <|> do (l, op) <- try (do

927+ <|> do (l, op, nfc) <- try (do

928928 pushIndent

929929 l <- argExpr syn

930− op <- operator

930+ (op, nfc) <- operatorFC

931931 when (op == "=" || op == "?=" ) $

932932 fail "infix clause definition with \"=\" and \"?=\" not supported "

933− return (l, op))

933+ return (l, op, nfc))

934934 let n = expandNS syn (sUN op)

935935 r <- argExpr syn

936936 fc <- getFC

@@ -943,7 +943,7 @@ clause syn

943943 do terminator

944944 return ([], [])]

945945 ist <- get

946− let capp = PApp fc (PRef fc n) [pexp l, pexp r]

946+ let capp = PApp fc (PRef nfc n) [pexp l, pexp r]

947947 put (ist { lastParse = Just n })

948948 return $ PClause fc n capp wargs rs wheres) <|> (do

949949 popIndent

@@ -959,13 +959,13 @@ clause syn

959959 put (ist { lastParse = Just n })

960960 return $ PWith fc n capp wargs wval pn withs)

961961 <|> do pushIndent

962− n_in <- fst <$> fnName; let n = expandNS syn n_in

962+ (n_in, nfc) <- fnName; let n = expandNS syn n_in

963963 cargs <- many (constraintArg syn)

964964 fc <- getFC

965965 args <- many (try (implicitArg (syn { inPattern = True } ))

966966 <|> (fmap pexp (argExpr syn)))

967967 wargs <- many (wExpr syn)

968− let capp = PApp fc (PRef fc n)

968+ let capp = PApp fc (PRef nfc n)

969969 (cargs ++ args)

970970 (do r <- rhs syn n

971971 ist <- get

test/reg007/expected+1−1

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

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

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

2+reg007.lidr:12:11-17:When elaborating right hand side of hurrah:

33Can't unify

44 n = lala (Type of isSame)

55with

test/sourceLocation001/expected+2−2

@@ -1,11 +1,11 @@

11Testing using definition

2−FileLoc "SourceLoc.idr" (16, 11) (16, 11)

2+FileLoc "SourceLoc.idr" (16, 11) (16, 17)

33Testing using inline tactics

44FileLoc "SourceLoc.idr" (20, 17) (20, 17)

55Testing using metavariable with later definition

66FileLoc "SourceLoc.idr" (98, 16) (98, 16)

77-----------------------

88Success!

9−Error at FileLoc "SourceLoc.idr" (72, 23) (72, 23)

9+Error at FileLoc "SourceLoc.idr" (72, 23) (72, 26)

1010Success!

1111Success!

test/tutorial006/expected+2−1

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

1−tutorial006a.idr:5:23:When elaborating right hand side of vapp:

1+tutorial006a.idr:5:23-25:

2+When elaborating right hand side of vapp:

23When elaborating argument xs to constructor Data.VectType.Vect.:::

34 Can't unify

45 Vect (n + n) a (Type of vapp xs xs)