9107357 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+4−4

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

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

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

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

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

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

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

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

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

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

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

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

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

10701070 PClauses fc opts n' (map expandParamsC cs)

src/Idris/AbsSyntaxTree.hs+5−5

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

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

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

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

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

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

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

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

655655 | PSyntax FC Syntax -- ^ Syntax definition

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

657657 | 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.

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

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

661661 deriving Functor

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

750750declared :: PDecl -> [Name]

751751declared (PFix _ _ _) = []

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

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

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

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

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

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

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

771771tldeclared :: PDecl -> [Name]

772772tldeclared (PFix _ _ _) = []

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

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

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

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

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

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

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

786786defined :: PDecl -> [Name]

787787defined (PFix _ _ _) = []

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

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

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

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

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

792792defined (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

136136 rnf x3 `seq`

137137 rnf x4 `seq`

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

140140 = rnf x1 `seq`

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

141+ rnf x2 `seq`

142+ rnf x3 `seq`

143+ rnf x4 `seq`

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

142145 rnf (PClauses x1 x2 x3 x4)

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

144147 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

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

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

187190 rnf (PDirective x1) = ()

188− rnf (PProvider x1 x2 x3 x4 x5)

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

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`

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

190197 rnf (PTransform x1 x2 x3 x4)

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

192199

src/Idris/Delaborate.hs+8−7

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

1919import Data.Maybe (mapMaybe)

2020import Data.List (intersperse, nub)

2121import qualified Data.Text as T

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

2223import Control.Monad.State

2324

2425import Debug.Trace

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

566567

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

568569fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation

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

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

570571 do let ctxt = tt_ctxt ist

571572 docs = docOverview ist n

572573 ty = Just (getTy ist n)

573574 case () of

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

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

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

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

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

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

577578 _ | isMetavarName n ist -> if meta

578− then AnnName n (Just MetavarOutput) docs ty

579− else AnnName n (Just FunOutput) docs ty

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

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

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

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

581582 _ | otherwise -> annot

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

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

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

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

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

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

292292memberDocs (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)

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

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

296296memberDocs (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)

483483 | Placeholder <- getTm t,

484484 n `elem` ps,

485485 not (n `elem` allNamesIn tm)

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

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

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

488488 addP _ ts = ts

489489propagateParams i ps t (PRef fc n)

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

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

5252import Util.Pretty(pretty, text)

5353

5454-- | Elaborate a type provider

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

56−elabProvider doc info syn fc what n

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

56+elabProvider doc info syn fc nfc what n

5757 = do i <- getIState

5858 -- Ensure that the experimental extension is enabled

5959 unless (TypeProviders `elem` idris_language_extensions i) $

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

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

9999 | ProvPostulate _ <- what ->

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

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

103103 | otherwise ->

104104 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

11911191 -- old ones with an _

11921192 mkClause args (l, r)

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

11951195 (map (mkLHSarg l) args') in

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

11971197

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

232232 tyIsHandler _ = False

233233

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

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

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

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

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

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

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

239239 addIBC (IBCPostulate n)

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

240241

241242 -- remove it from the deferred definitions list

242243 solveDeferred n

243244

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

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

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

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

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

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

248249 ist <- getIState

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

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

162162 elabType info s doc argdocs f o n nfc ty

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

165165 | what /= EDefns

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

167167 if b

168− then elabExtern info s doc f o n ty

169− else elabPostulate 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 nfc o n ty

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

171171 | what /= ETypes

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

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

259259 addIBC (IBCDSL n)

260260elabDecl' what info (PDirective i)

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

263263 | what /= EDefns

264264 = 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

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

267267 = do elabTransform info fc safety old new

268268 return ()

src/Idris/IBC.hs+8−4

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

12321232 PMutual x1 x2 -> do putWord8 11

12331233 put x1

12341234 put x2

1235− PPostulate x1 x2 x3 x4 x5 x6 x7

1235+ PPostulate x1 x2 x3 x4 x5 x6 x7 x8

12361236 -> do putWord8 12

12371237 put x1

12381238 put x2

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

12411241 put x5

12421242 put x6

12431243 put x7

1244+ put x8

12441245 PSyntax x1 x2 -> do putWord8 13

12451246 put x1

12461247 put x2

12471248 PDirective x1 -> error "Cannot serialize PDirective"

1248− PProvider x1 x2 x3 x4 x5 ->

1249+ PProvider x1 x2 x3 x4 x5 x6 ->

12491250 do putWord8 15

12501251 put x1

12511252 put x2

12521253 put x3

12531254 put x4

12541255 put x5

1256+ put x6

12551257 PTransform x1 x2 x3 x4 -> do putWord8 16

12561258 put x1

12571259 put x2

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

13481350 x5 <- get

13491351 x6 <- get

13501352 x7 <- get

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

1353+ x8 <- get

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

13521355 13 -> do x1 <- get

13531356 x2 <- get

13541357 return (PSyntax x1 x2)

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

13581361 x3 <- get

13591362 x4 <- get

13601363 x5 <- get

1361− return (PProvider x1 x2 x3 x4 x5)

1364+ x6 <- get

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

13621366 16 -> do x1 <- get

13631367 x2 <- get

13641368 x3 <- get

src/Idris/Parser.hs+6−6

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

533533 opts <- fnOpts initOpts

534534 acc <- optional accessibility

535535 opts' <- fnOpts opts

536− n_in <- fst <$> fnName

536+ (n_in, nfc) <- fnName

537537 let n = expandNS syn n_in

538538 lchar ':'

539539 ty <- typeExpr (allowImp syn)

540540 fc <- getFC

541541 terminator

542542 addAcc n acc

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

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

544544 <?> "postulate"

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

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

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

11931193 provideTerm doc <|> providePostulate doc

11941194 <?> "type provider"

11951195 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 ')'

11971197 fc <- getFC

11981198 reserved "with"

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

12011201 providePostulate doc =

12021202 do reserved "postulate"

1203− n <- fst <$> fnName

1203+ (n, nfc) <- fnName

12041204 fc <- getFC

12051205 reserved "with"

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

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

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

12081208

12091209{- | Parses a transform

12101210