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

src/Idris/AbsSyntax.hs+7−7

compare with master

unifiedsplit

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

1086 where

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

1088 -- added implicitly)

1089− expandPData (PDatadecl n ty cons)

1089+ expandPData (PDatadecl n nfc ty cons)

1090 = 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))

1092 (map econ cons)

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

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

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

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

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

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

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

1097 = d

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

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

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

1551 PAlternative a as'

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

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

1555− PApp fc (PInferRef fc f) as'

1555+ PApp fc (PInferRef ffc f) as'

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

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

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

src/Idris/AbsSyntaxTree.hs+24−23

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

705

706-- | Data declaration

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

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

708 d_tcon :: t, -- ^ Type constructor

709 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

710 }

711 }

711 -- ^ Data declaration

712 -- ^ Data declaration

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

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

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

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

714 deriving Functor

715 deriving Functor

715{-!

716{-!

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

739declared (PNamespace _ ds) = concatMap declared ds

740declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

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

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

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

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

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

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

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

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

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

758tldeclared (PParams _ _ ds) = []

759tldeclared (PParams _ _ ds) = []

759tldeclared (PMutual _ ds) = concatMap tldeclared ds

760tldeclared (PMutual _ ds) = concatMap tldeclared ds

760tldeclared (PNamespace _ ds) = concatMap tldeclared ds

761tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

775defined (PNamespace _ ds) = concatMap defined ds

776defined (PNamespace _ ds) = concatMap defined ds

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

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

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

1260

1261

1261inferTy = sMN 0 "__Infer"

1262inferTy = sMN 0 "__Infer"

1262inferCon = sMN 0 "__infer"

1263inferCon = sMN 0 "__infer"

1263−inferDecl = PDatadecl inferTy

1264+inferDecl = PDatadecl inferTy NoFC

1264 (PType bi)

1265 (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) (

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

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

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

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

1268inferOpts = []

1269inferOpts = []

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

1317 "\n\n" ++

1318 "\n\n" ++

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

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

1319

1320

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

1321+eqDecl = PDatadecl eqTy NoFC (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+ (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1322− (PType bi)))

1323+ (PType bi)))

1323 [(reflDoc, reflParamDoc,

1324 [(reflDoc, reflParamDoc,

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

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

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

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

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

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

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

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

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

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

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

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

1330 where n a = sUN a

1331 where n a = sUN a

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

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

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

1333 "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)

1772

1773

1774

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

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

1775−showDImp ppo (PDatadecl n ty cons)

1776+showDImp ppo (PDatadecl n nfc ty cons)

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

1777 = 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))

1778

1779

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

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

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

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

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

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

49 deriving Eq

50

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

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

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

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

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

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

55 }

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

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

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

58 deriving (Data, Typeable, Ord)

59

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+

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

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

61spanFC :: FC -> FC -> FC

75spanFC :: FC -> FC -> FC

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

76spanFC (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

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

194

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

196− rnf (PDatadecl x1 x2 x3)

196+ rnf (PDatadecl x1 x2 x3 x4)

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

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

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

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

199

200instance NFData PTerm where

201 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

80 let cty = impbind ps $ conbind constraints

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

82 constraint

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

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

84− let ddecl = PDatadecl tn tty cons

84+ let ddecl = PDatadecl tn NoFC tty cons

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

86 -- Elaborate the data declaration

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

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

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

15import Idris.Inliner

16import Idris.PartialEval

17import Idris.DeepSeq

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

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

19import IRTS.Lang

20

21import Idris.Elab.Type

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

51import Util.Pretty(pretty, text)

52

53elabData :: 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)

55 = do let codata = Codata `elem` opts

56 iLOG (show (fc, doc))

57 checkUndefined fc n

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

59

60 addIBC (IBCDef n)

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

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

62

63

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)

64 = do let codata = Codata `elem` opts

65 = do let codata = Codata `elem` opts

65 iLOG (show fc)

66 iLOG (show fc)

66 undef <- isUndefined fc n

67 undef <- isUndefined fc n

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

116 -- create a case function

117 -- create a case function

117 when (DefaultCaseFun `elem` opts) $

118 when (DefaultCaseFun `elem` opts) $

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

119 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

119 where

125 where

120 setDetaggable :: Name -> Idris ()

126 setDetaggable :: Name -> Idris ()

121 setDetaggable n = do

127 setDetaggable n = do

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

194 | otherwise = count n ts

200 | otherwise = count n ts

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

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

196

202

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

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

198

204

199 -- Abuse of ElabInfo.

205 -- Abuse of ElabInfo.

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

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

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

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

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

213 Type -> -- for unique kind checking

219 Type -> -- for unique kind checking

214 Type -> -- data type's kind

220 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]) ->

216 Idris (Name, Type)

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

218 = do checkUndefined fc n

224 = do checkUndefined fc n

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

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

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

226 (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

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

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

303-- rename to caseFun to match updated intend

309-- rename to caseFun to match updated intend

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

310elabCaseFun :: 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])] ->

306 ElabInfo -> EliminatorState ()

312 ElabInfo -> EliminatorState ()

307elabCaseFun ind paramPos n ty cons info = do

313elabCaseFun ind paramPos n ty cons info = do

308 elimLog $ "Elaborating case function"

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

310 let (cnstrs, _) = splitPi ty

316 let (cnstrs, _) = splitPi ty

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

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

312 generalParams <- namePis False pms

318 generalParams <- namePis False pms

313 motiveIdxs <- namePis False idxs

319 motiveIdxs <- namePis False idxs

314 let motive = mkMotive n paramPos generalParams motiveIdxs

320 let motive = mkMotive n paramPos generalParams motiveIdxs

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

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

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

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

317 name <- freshName $ casefunt ++ simpleName cnm

323 name <- freshName $ casefunt ++ simpleName cnm

318 consTerm <- extractConsTerm c generalParams

324 consTerm <- extractConsTerm c generalParams

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

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

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

489 _ -> return implargs

495 _ -> return implargs

490

496

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

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

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

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

493 let cons' = replaceParams paramPos generalParameters ty

499 let cons' = replaceParams paramPos generalParameters ty

494 let (args, resTy) = splitPi cons'

500 let (args, resTy) = splitPi cons'

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

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

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

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

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

525 convertImplPi _ = Nothing

531 convertImplPi _ = Nothing

526

532

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

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

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

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

529 let cons' = replaceParams paramPos generalParameters ty

535 let cons' = replaceParams paramPos generalParameters ty

530 let (args, resTy) = splitPi cons'

536 let (args, resTy) = splitPi cons'

531 i <- State.lift getIState

537 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

57

58 -- Build data declaration for elaboration

59 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, [])]

61 elabData info rsyn doc paramDocs fc opts datadecl

62

63 iLOG $ "fieldsWithName " ++ show fieldsWithName

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

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

360 claim tyn RType

361 movelast tyn

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

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

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

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

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

365 pexp l, pexp r]))

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

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

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

370 claim btyn RType

371 movelast btyn

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

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

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

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

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

375 pexp l, pexp r]))

376

377 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

1080 end_unify

1081

1082 -- 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

1084 env <- get_env

1085+ EState _ _ _ hs <- getAux

1085 loadState

1086 loadState

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

1088+

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

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

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

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

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

1091 (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)

173 elabData info s doc argDocs f co d

174 | otherwise

175 = 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))

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

178 | what /= ETypes

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

src/Idris/IBC.hs+13−9

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

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

1456 put x

1457 = case x of

1458− PDatadecl x1 x2 x3 -> do putWord8 0

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

1459− put x1

1459+ put x1

1460− put x2

1460+ put x2

1461− put x3

1461+ put x3

1462+ put x4

1462− PLaterdecl x1 x2 -> do putWord8 1

1463+ PLaterdecl x1 x2 x3 -> do putWord8 1

1463− put x1

1464+ put x1

1464− put x2

1465+ put x2

1466+ put x3

1465 get

1467 get

1466 = do i <- getWord8

1468 = do i <- getWord8

1467 case i of

1469 case i of

1468 0 -> do x1 <- get

1470 0 -> do x1 <- get

1469 x2 <- get

1471 x2 <- get

1470 x3 <- get

1472 x3 <- get

1473+ x4 <- get

1471− return (PDatadecl x1 x2 x3)

1474+ return (PDatadecl x1 x2 x3 x4)

1472 1 -> do x1 <- get

1475 1 -> do x1 <- get

1473 x2 <- get

1476 x2 <- get

1477+ x3 <- get

1474− return (PLaterdecl x1 x2)

1478+ return (PLaterdecl x1 x2 x3)

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

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

1476

1480

1477instance Binary PunInfo where

1481instance Binary PunInfo where

src/Idris/ParseData.hs+15−15

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

191 | (n, d) <- argDocs ]

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

193 fc <- getFC

194− tyn_in <- fst <$> fnName

194+ (tyn_in, nfc) <- fnName

195 (do try (lchar ':')

196 popIndent

197 ty <- typeExpr (allowImp syn)

198 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

200 reserved "where"

201 cons <- indentedBlock (constructor syn)

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

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

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

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

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

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

206 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

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

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

210 let n = show tyn_in ++ " "

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

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

220 terminator

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

223 do let cty = bindArgs cargs conty

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

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

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

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

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

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

227 <?> "data type declaration"

228 where

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

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

240{- | Parses a type constructor declaration

241 Constructor ::= DocComment? FnName TypeSig;

242-}

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

244constructor syn

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

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

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

247 let cn = expandNS syn cn_in

248 lchar ':'

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

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

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

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

255 | (n, d) <- argDocs ]

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

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

257 <?> "constructor"

258

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

260 SimpleConstructor ::= FnName SimpleExpr* DocComment?

261-}

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

263simpleConstructor syn

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

265 ist <- get

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

267− cn_in <- fst <$> fnName

267+ (cn_in, nfc) <- fnName

268 let cn = expandNS syn cn_in

269 fc <- getFC

270 args <- many (do notEndApp

271 simpleExpr syn)

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

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

273 <?> "constructor"

274

275{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+19−14

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

1082@

1083 -}

1084listExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

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

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

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

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

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

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

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

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

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

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

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

1090− lchar ']'

1093+ lchar ']'

1091− return (PDoBlock (map addGuard qs ++

1094+ return (PDoBlock (map addGuard qs ++

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

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

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

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

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

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

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

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

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

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

1097 <?> "list expression"

1100 <?> "list expression"

1098 where

1101 where

1102+ mkNil :: FC -> PTerm

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

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

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

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

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

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

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

1102 addGuard :: PDo -> PDo

1107 addGuard :: PDo -> PDo

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

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

1104 [pexp e])

1109 [pexp e])

src/Idris/ParseHelpers.hs+9

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

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

374 return op

375

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+

376{- * Position helpers -}

385{- * Position helpers -}

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

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

378fileName :: Delta -> String

387fileName :: Delta -> String

src/Idris/Parser.hs+6−6

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

924 ist <- get

925 put (ist { lastParse = Just n })

926 return $ PClause fc n capp [] r wheres

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

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

928 pushIndent

929 l <- argExpr syn

930− op <- operator

930+ (op, nfc) <- operatorFC

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

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

933− return (l, op))

933+ return (l, op, nfc))

934 let n = expandNS syn (sUN op)

935 r <- argExpr syn

936 fc <- getFC

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

943 do terminator

944 return ([], [])]

945 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]

947 put (ist { lastParse = Just n })

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

949 popIndent

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

959 put (ist { lastParse = Just n })

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

961 <|> do pushIndent

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

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

963 cargs <- many (constraintArg syn)

964 fc <- getFC

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

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

967 wargs <- many (wExpr syn)

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

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

969 (cargs ++ args)

970 (do r <- rhs syn n

971 ist <- get

test/reg007/expected+1−1

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

1reg007.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:

3Can't unify

4 n = lala (Type of isSame)

5with

test/sourceLocation001/expected+2−2

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

1Testing using definition

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

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

3Testing using inline tactics

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

5Testing using metavariable with later definition

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

7-----------------------

8Success!

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

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

10Success!

11Success!

test/tutorial006/expected+2−1

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

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

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

2+When elaborating right hand side of vapp:

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

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

3 Can't unify

4 Can't unify

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

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