9107357 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+4−4

compare with master

unifiedsplit

@@ -1058,13 +1058,13 @@ expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)

1058 PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))

1059 else --trace (show (n, expandParams dec ps ns ty)) $

1060 PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)

1061−expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc o n ty)

1061+expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)

1062 = if n `elem` ns && (not rhsonly)

1063 then -- trace (show (n, expandParams dec ps ns ty)) $

1064− PPostulate e doc syn fc o (dec n) (piBind ps

1064+ PPostulate e doc syn fc nfc o (dec n)

1065− (expandParams dec ps ns [] ty))

1065+ (piBind ps (expandParams dec ps ns [] ty))

1066 else --trace (show (n, expandParams dec ps ns ty)) $

1067− PPostulate e doc syn fc o n (expandParams dec ps ns [] ty)

1067+ PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)

1068expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

1069 = let n' = if n `elem` ns then dec n else n in

1070 PClauses fc opts n' (map expandParamsC cs)

src/Idris/AbsSyntaxTree.hs+5−5

@@ -607,7 +607,7 @@ data PDecl' t

607 = PFix FC Fixity [String] -- ^ Fixity declaration

608 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)

609 | PPostulate Bool -- external def if true

610− (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate

610+ (Docstring (Either Err PTerm)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location

611 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

612 | PCAF FC Name t -- ^ Top level constant

613 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

@@ -655,7 +655,7 @@ data PDecl' t

655 | PSyntax FC Syntax -- ^ Syntax definition

656 | PMutual FC [PDecl' t] -- ^ Mutual block

657 | PDirective Directive -- ^ Compiler directive.

658− | PProvider (Docstring (Either Err PTerm)) SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term

658+ | PProvider (Docstring (Either Err PTerm)) SyntaxInfo FC FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location.

659 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

660 -- bool is True, lhs and rhs must be convertible

661 deriving Functor

@@ -750,7 +750,7 @@ type PClause = PClause' PTerm

750declared :: PDecl -> [Name]

751declared (PFix _ _ _) = []

752declared (PTy _ _ _ _ _ n fc t) = [n]

753−declared (PPostulate _ _ _ _ _ n t) = [n]

753+declared (PPostulate _ _ _ _ _ _ n t) = [n]

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

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

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

@@ -771,7 +771,7 @@ declared _ = []

771tldeclared :: PDecl -> [Name]

772tldeclared (PFix _ _ _) = []

773tldeclared (PTy _ _ _ _ _ n _ t) = [n]

774−tldeclared (PPostulate _ _ _ _ _ n t) = [n]

774+tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]

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

776tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

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

@@ -786,7 +786,7 @@ tldeclared _ = []

786defined :: PDecl -> [Name]

787defined (PFix _ _ _) = []

788defined (PTy _ _ _ _ _ n _ t) = []

789−defined (PPostulate _ _ _ _ _ n t) = []

789+defined (PPostulate _ _ _ _ _ _ n t) = []

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

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

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

src/Idris/DeepSeq.hs+11−4

@@ -136,9 +136,12 @@ instance (NFData t) => NFData (PDecl' t) where

136 rnf x3 `seq`

137 rnf x4 `seq`

138 rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

139− rnf (PPostulate x1 x2 x3 x4 x5 x6 x7)

139+ rnf (PPostulate x1 x2 x3 x4 x5 x6 x7 x8)

140 = rnf x1 `seq`

141+ rnf x2 `seq`

142+ rnf x3 `seq`

143+ rnf x4 `seq`

141− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

144+ rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

142 rnf (PClauses x1 x2 x3 x4)

145 rnf (PClauses x1 x2 x3 x4)

143 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

146 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

144 rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

147 rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

@@ -185,8 +188,12 @@ instance (NFData t) => NFData (PDecl' t) where

185 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

188 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

186 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

189 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

187 rnf (PDirective x1) = ()

190 rnf (PDirective x1) = ()

188− rnf (PProvider x1 x2 x3 x4 x5)

191+ rnf (PProvider x1 x2 x3 x4 x5 x6)

192+ = rnf x1 `seq`

193+ rnf x2 `seq`

194+ rnf x3 `seq`

195+ rnf x4 `seq`

189− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

196+ rnf x5 `seq` rnf x6 `seq` ()

190 rnf (PTransform x1 x2 x3 x4)

197 rnf (PTransform x1 x2 x3 x4)

191 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

198 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

192

199

src/Idris/Delaborate.hs+8−7

@@ -19,6 +19,7 @@ import Data.Generics.Uniplate.Data (transform)

19import Data.Maybe (mapMaybe)

20import Data.List (intersperse, nub)

21import qualified Data.Text as T

22+import Control.Applicative (Alternative((<|>)))

22import Control.Monad.State

23import Control.Monad.State

23

24

24import Debug.Trace

25import Debug.Trace

@@ -566,18 +567,18 @@ annTm tm = annotate (AnnTerm [] tm)

566

567

567-- | Add extra metadata to an output annotation, optionally marking metavariables.

568-- | Add extra metadata to an output annotation, optionally marking metavariables.

568fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation

569fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation

569−fancifyAnnots ist meta annot@(AnnName n _ _ _) =

570+fancifyAnnots ist meta annot@(AnnName n nt _ _) =

570 do let ctxt = tt_ctxt ist

571 do let ctxt = tt_ctxt ist

571 docs = docOverview ist n

572 docs = docOverview ist n

572 ty = Just (getTy ist n)

573 ty = Just (getTy ist n)

573 case () of

574 case () of

574− _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty

575+ _ | isDConName n ctxt -> AnnName n (nt <|> Just DataOutput) docs ty

575− _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty

576+ _ | isFnName n ctxt -> AnnName n (nt <|> Just FunOutput) docs ty

576− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

577+ _ | isTConName n ctxt -> AnnName n (nt <|> Just TypeOutput) docs ty

577 _ | isMetavarName n ist -> if meta

578 _ | isMetavarName n ist -> if meta

578− then AnnName n (Just MetavarOutput) docs ty

579+ then AnnName n (nt <|> Just MetavarOutput) docs ty

579− else AnnName n (Just FunOutput) docs ty

580+ else AnnName n (nt <|> Just FunOutput) docs ty

580− _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty

581+ _ | isPostulateName n ist -> AnnName n (nt <|> Just PostulateOutput) docs ty

581 _ | otherwise -> annot

582 _ | otherwise -> annot

582 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

583 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

583 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

584 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

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

@@ -290,7 +290,7 @@ mdec x = x

290-- | Get the docstring corresponding to a member, if one exists

291memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

292memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

293−memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)

293+memberDocs (PPostulate _ d _ _ _ _ n _) = Just (basename n, d)

294memberDocs (PData d _ _ _ _ pdata) = Just (basename $ d_name pdata, d)

295memberDocs (PRecord d _ _ _ n _ _ _ _ _ _ _ ) = Just (basename n, d)

296memberDocs (PClass d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)

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

@@ -483,7 +483,7 @@ propagateParams i ps t tm@(PApp _ (PRef fc n) args)

483 | Placeholder <- getTm t,

484 n `elem` ps,

485 not (n `elem` allNamesIn tm)

486− = t { getTm = PRef fc n } : addP sc ts

486+ = t { getTm = PRef NoFC n } : addP sc ts

487 addP (Bind n _ sc) (t : ts) = t : addP sc ts

488 addP _ ts = ts

489propagateParams i ps t (PRef fc n)

src/Idris/Elab/Provider.hs+3−3

@@ -52,8 +52,8 @@ import Data.List.Split (splitOn)

52import Util.Pretty(pretty, text)

53

54-- | Elaborate a type provider

55−elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

55+elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris ()

56−elabProvider doc info syn fc what n

56+elabProvider doc info syn fc nfc what n

57 = do i <- getIState

58 -- Ensure that the experimental extension is enabled

59 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -98,7 +98,7 @@ elabProvider doc info syn fc what n

98 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

99 | ProvPostulate _ <- what ->

100 do -- Add the postulate

101− elabPostulate info syn doc fc [] n (delab i tm)

101+ elabPostulate info syn doc fc nfc [] n (delab i tm)

102 logLvl 3 $ "Elaborated provided postulate " ++ show n

103 | otherwise ->

104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

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

@@ -1191,7 +1191,7 @@ elab ist info emode opts fn tm

1191 -- old ones with an _

1192 mkClause args (l, r)

1193 = let args' = map (shadowed (allNamesIn l)) args

1194− lhs = PApp (getFC fc l) (PRef (getFC fc l) n)

1194+ lhs = PApp (getFC fc l) (PRef NoFC n)

1195 (map (mkLHSarg l) args') in

1196 PClause (getFC fc l) n lhs [] r []

1197

src/Idris/Elab/Type.hs+5−4

@@ -232,18 +232,19 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

232 tyIsHandler _ = False

233

234elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

235− FC -> FnOpts -> Name -> PTerm -> Idris ()

235+ FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()

236−elabPostulate info syn doc fc opts n ty = do

236+elabPostulate info syn doc fc nfc opts n ty = do

237 elabType info syn doc [] fc opts n NoFC ty

238 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState

239 addIBC (IBCPostulate n)

240+ sendHighlighting [(nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]

240

241

241 -- remove it from the deferred definitions list

242 -- remove it from the deferred definitions list

242 solveDeferred n

243 solveDeferred n

243

244

244elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

245elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

245− FC -> FnOpts -> Name -> PTerm -> Idris ()

246+ FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()

246−elabExtern info syn doc fc opts n ty = do

247+elabExtern info syn doc fc nfc opts n ty = do

247 cty <- elabType info syn doc [] fc opts n NoFC ty

248 cty <- elabType info syn doc [] fc opts n NoFC ty

248 ist <- getIState

249 ist <- getIState

249 let arity = length (getArgTys (normalise (tt_ctxt ist) [] cty))

250 let arity = length (getArgTys (normalise (tt_ctxt ist) [] cty))

src/Idris/ElabDecls.hs+5−5

@@ -161,12 +161,12 @@ elabDecl' what info (PTy doc argdocs s f o n nfc ty)

161 = do logLvl 1 $ "Elaborating type decl " ++ show n ++ show o

162 elabType info s doc argdocs f o n nfc ty

163 return ()

164−elabDecl' what info (PPostulate b doc s f o n ty)

164+elabDecl' what info (PPostulate b doc s f nfc o n ty)

165 | what /= EDefns

166 = do logLvl 1 $ "Elaborating postulate " ++ show n ++ show o

167 if b

168− then elabExtern info s doc f o n ty

168+ then elabExtern info s doc f nfc o n ty

169− else elabPostulate info s doc f o n ty

169+ else elabPostulate info s doc f nfc o n ty

170elabDecl' what info (PData doc argDocs s f co d)

171 | what /= ETypes

172 = do logLvl 1 $ "Elaborating " ++ show (d_name d)

@@ -259,10 +259,10 @@ elabDecl' _ info (PDSL n dsl)

259 addIBC (IBCDSL n)

260elabDecl' what info (PDirective i)

261 | what /= EDefns = directiveAction i

262−elabDecl' what info (PProvider doc syn fc provWhat n)

262+elabDecl' what info (PProvider doc syn fc nfc provWhat n)

263 | what /= EDefns

264 = do logLvl 1 $ "Elaborating type provider " ++ show n

265− elabProvider doc info syn fc provWhat n

265+ elabProvider doc info syn fc nfc provWhat n

266elabDecl' what info (PTransform fc safety old new)

267 = do elabTransform info fc safety old new

268 return ()

src/Idris/IBC.hs+8−4

@@ -1232,7 +1232,7 @@ instance (Binary t) => Binary (PDecl' t) where

1232 PMutual x1 x2 -> do putWord8 11

1233 put x1

1234 put x2

1235− PPostulate x1 x2 x3 x4 x5 x6 x7

1235+ PPostulate x1 x2 x3 x4 x5 x6 x7 x8

1236 -> do putWord8 12

1237 put x1

1238 put x2

@@ -1241,17 +1241,19 @@ instance (Binary t) => Binary (PDecl' t) where

1241 put x5

1242 put x6

1243 put x7

1244+ put x8

1244 PSyntax x1 x2 -> do putWord8 13

1245 PSyntax x1 x2 -> do putWord8 13

1245 put x1

1246 put x1

1246 put x2

1247 put x2

1247 PDirective x1 -> error "Cannot serialize PDirective"

1248 PDirective x1 -> error "Cannot serialize PDirective"

1248− PProvider x1 x2 x3 x4 x5 ->

1249+ PProvider x1 x2 x3 x4 x5 x6 ->

1249 do putWord8 15

1250 do putWord8 15

1250 put x1

1251 put x1

1251 put x2

1252 put x2

1252 put x3

1253 put x3

1253 put x4

1254 put x4

1254 put x5

1255 put x5

1256+ put x6

1255 PTransform x1 x2 x3 x4 -> do putWord8 16

1257 PTransform x1 x2 x3 x4 -> do putWord8 16

1256 put x1

1258 put x1

1257 put x2

1259 put x2

@@ -1348,7 +1350,8 @@ instance (Binary t) => Binary (PDecl' t) where

1348 x5 <- get

1350 x5 <- get

1349 x6 <- get

1351 x6 <- get

1350 x7 <- get

1352 x7 <- get

1353+ x8 <- get

1351− return (PPostulate x1 x2 x3 x4 x5 x6 x7)

1354+ return (PPostulate x1 x2 x3 x4 x5 x6 x7 x8)

1352 13 -> do x1 <- get

1355 13 -> do x1 <- get

1353 x2 <- get

1356 x2 <- get

1354 return (PSyntax x1 x2)

1357 return (PSyntax x1 x2)

@@ -1358,7 +1361,8 @@ instance (Binary t) => Binary (PDecl' t) where

1358 x3 <- get

1361 x3 <- get

1359 x4 <- get

1362 x4 <- get

1360 x5 <- get

1363 x5 <- get

1364+ x6 <- get

1361− return (PProvider x1 x2 x3 x4 x5)

1365+ return (PProvider x1 x2 x3 x4 x5 x6)

1362 16 -> do x1 <- get

1366 16 -> do x1 <- get

1363 x2 <- get

1367 x2 <- get

1364 x3 <- get

1368 x3 <- get

src/Idris/Parser.hs+6−6

@@ -533,14 +533,14 @@ postulate syn = do (doc, ext)

533 opts <- fnOpts initOpts

534 acc <- optional accessibility

535 opts' <- fnOpts opts

536− n_in <- fst <$> fnName

536+ (n_in, nfc) <- fnName

537 let n = expandNS syn n_in

538 lchar ':'

539 ty <- typeExpr (allowImp syn)

540 fc <- getFC

541 terminator

542 addAcc n acc

543− return (PPostulate ext doc syn fc opts' n ty)

543+ return (PPostulate ext doc syn fc nfc opts' n ty)

544 <?> "postulate"

545 where ppostDecl = do reserved "postulate"; return False

546 <|> do lchar '%'; reserved "extern"; return True

@@ -1193,18 +1193,18 @@ provider syn = do doc <- try (do (doc, _) <- docstring syn

1193 provideTerm doc <|> providePostulate doc

1194 <?> "type provider"

1195 where provideTerm doc =

1196− do lchar '('; n <- fst <$> fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1196+ do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1197 fc <- getFC

1198 reserved "with"

1199 e <- expr syn <?> "provider expression"

1200− return [PProvider doc syn fc (ProvTerm t e) n]

1200+ return [PProvider doc syn fc nfc (ProvTerm t e) n]

1201 providePostulate doc =

1202 do reserved "postulate"

1203− n <- fst <$> fnName

1203+ (n, nfc) <- fnName

1204 fc <- getFC

1205 reserved "with"

1206 e <- expr syn <?> "provider expression"

1207− return [PProvider doc syn fc (ProvPostulate e) n]

1207+ return [PProvider doc syn fc nfc (ProvPostulate e) n]

1208

1209{- | Parses a transform

1210