268296f · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3−3

compare with master

unifiedsplit

@@ -1028,12 +1028,12 @@ expandParams dec ps ns infs tm = en tm

1028expandParamsD :: Bool -> -- True = RHS only

1029 IState ->

1030 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

1031−expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)

1031+expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)

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

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

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

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

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

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+5−5

@@ -593,7 +593,7 @@ type ProvideWhat = ProvideWhat' PTerm

593-- datatypes and typeclasses.

594data PDecl' t

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

596− | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

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

597 | PPostulate Bool -- external def if true

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

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

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

728

729declared :: PDecl -> [Name]

730declared (PFix _ _ _) = []

731−declared (PTy _ _ _ _ _ n t) = [n]

731+declared (PTy _ _ _ _ _ n fc t) = [n]

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

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

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

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

749-- get the names declared, not counting nested parameter blocks

750tldeclared :: PDecl -> [Name]

751tldeclared (PFix _ _ _) = []

752−tldeclared (PTy _ _ _ _ _ n t) = [n]

752+tldeclared (PTy _ _ _ _ _ n _ t) = [n]

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

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

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

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

764

765defined :: PDecl -> [Name]

766defined (PFix _ _ _) = []

767−defined (PTy _ _ _ _ _ n t) = []

767+defined (PTy _ _ _ _ _ n _ t) = []

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

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

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

@@ -1780,7 +1780,7 @@ showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

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

1781

1782showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1783−showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

1783+showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

1784showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1785 indent 2 (vsep (map (showCImp o) cs))

1786showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

src/Idris/DeepSeq.hs+4−2

@@ -129,10 +129,12 @@ instance NFData DataOpt where

129

130instance (NFData t) => NFData (PDecl' t) where

131 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

132− rnf (PTy x1 x2 x3 x4 x5 x6 x7)

132+ rnf (PTy x1 x2 x3 x4 x5 x6 x7 x8)

133 = rnf x1 `seq`

134 rnf x2 `seq`

135+ rnf x3 `seq`

136+ rnf x4 `seq`

135− rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

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

136 rnf (PPostulate x1 x2 x3 x4 x5 x6 x7)

138 rnf (PPostulate x1 x2 x3 x4 x5 x6 x7)

137 = rnf x1 `seq`

139 = rnf x1 `seq`

138 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

140 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

src/Idris/Delaborate.hs+8−5

@@ -309,7 +309,7 @@ pprintErr' i (InvalidTCArg n t)

309 <> annName n <$>

310 text "(Type class arguments must be injective)"

311pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

312− align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

312+ align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i True) . annName) as)))

313pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

314pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

315pprintErr' i (WithFnType ty) =

@@ -558,8 +558,9 @@ annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

558annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation

559annTm tm = annotate (AnnTerm [] tm)

560

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

561−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

562+fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation

562−fancifyAnnots ist annot@(AnnName n _ _ _) =

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

563 do let ctxt = tt_ctxt ist

564 do let ctxt = tt_ctxt ist

564 docs = docOverview ist n

565 docs = docOverview ist n

565 ty = Just (getTy ist n)

566 ty = Just (getTy ist n)

@@ -567,7 +568,9 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

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

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

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

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

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

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

571+ _ | isMetavarName n ist -> if meta

570− _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

572+ then AnnName n (Just MetavarOutput) docs ty

573+ else AnnName n (Just FunOutput) docs ty

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

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

572 _ | otherwise -> annot

575 _ | otherwise -> annot

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

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

@@ -585,7 +588,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

585 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

588 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

586 delabTy ist n

589 delabTy ist n

587 in (displayS . renderPretty 1.0 50 $ theTy) ""

590 in (displayS . renderPretty 1.0 50 $ theTy) ""

588−fancifyAnnots _ annot = annot

591+fancifyAnnots _ _ annot = annot

589

592

590showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

593showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

591showSc i [] = empty

594showSc i [] = empty

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

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

140 conbind ((c, ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)

141 conbind [] x = x

142

143− getMName (PTy _ _ _ _ _ n _) = nsroot n

143+ getMName (PTy _ _ _ _ _ n nfc _) = nsroot n

144− tdecl allmeths (PTy doc _ syn _ o n t)

144+ tdecl allmeths (PTy doc _ syn _ o n nfc t)

145 = do t' <- implicit' info syn (map fst ps ++ allmeths) n t

146 logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

147 return ( (n, (toExp (map fst ps) Exp t')),

@@ -155,7 +155,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

155 case lookup n mtys of

156 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

157 let ds = map (decorateid defaultdec)

158− [PTy emptyDocstring [] syn fc [] n ty',

158+ [PTy emptyDocstring [] syn fc [] n NoFC ty',

159 PClauses fc (o ++ opts) n cs]

160 iLOG (show ds)

161 return (n, ((defaultdec n, ds!!1), ds))

@@ -165,7 +165,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

165 defaultdec (UN n) = sUN ("default#" ++ str n)

166 defaultdec (NS n ns) = NS (defaultdec n) ns

167

168− tydecl (PTy _ _ _ _ _ _ _) = True

168+ tydecl (PTy _ _ _ _ _ _ _ _) = True

169 tydecl _ = False

170 instdecl (PInstance _ _ _ _ _ _ _ _ _ _) = True

171 instdecl _ = False

@@ -194,7 +194,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

194 addInstance False conn' cfn

195 addIBC (IBCInstance False conn' cfn)

196-- iputStrLn ("Added " ++ show (conn, cfn, ty))

197− return [PTy emptyDocstring [] syn fc [] cfn ty,

197+ return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

198 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

199

200 -- Generate a top level function which looks up a method in a given

@@ -210,7 +210,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

210 logLvl 2 ("Top level type: " ++ showTmImpls ty')

211 iLOG (show (m, ty', capp, margs))

212 logLvl 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)

213− return [PTy doc [] syn fc o m ty',

213+ return [PTy doc [] syn fc o m NoFC ty',

214 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

215

216 getMArgs (PPi (Imp _ _ _ _) n _ ty sc) = IA n : getMArgs sc

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

@@ -374,7 +374,7 @@ elabPE info fc caller r =

374 logLvl 2 $ show n ++ " transformation rule: " ++

375 show rhs ++ " ==> " ++ show lhs

376

377− elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

377+ elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy

378 let def = map (\(lhs, rhs) ->

379 PClause fc newnm lhs [] rhs [])

380 (pe_clauses specdecl)

@@ -732,7 +732,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

732-- = NS (UN ('#':show x)) [show cnum, show fname]

733

734 sepBlocks bs = sepBlocks' [] bs where

735− sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)

735+ sepBlocks' ns (d@(PTy _ _ _ _ _ n _ t) : bs)

736 = let (bf, af) = sepBlocks' (n : ns) bs in

737 (d : bf, af)

738 sepBlocks' ns (d@(PClauses _ _ n _) : bs)

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

@@ -321,7 +321,7 @@ elabCaseFun ind paramPos n ty cons info = do

321 let motiveConstr = [(motiveName, expl, motive)]

322 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

323 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

324− let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

324+ let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName NoFC eliminatorTy

325 let clauseConsElimArgs = map getPiName consTerms

326 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

327 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

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

@@ -71,7 +71,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

71 let iname = mkiname n (namespace info) ps expn

72 let emptyclass = null (class_methods ci)

73 when (what /= EDefns || (null ds && not emptyclass)) $ do

74− nty <- elabType' True info syn doc argDocs fc [] iname t

74+ nty <- elabType' True info syn doc argDocs fc [] iname NoFC t

75 -- if the instance type matches any of the instances we have already,

76 -- and it's not a named instance, then it's overlapping, so report an error

77 case expn of

@@ -245,8 +245,8 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

245 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

246 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

247

248− mkTyDecl (n, op, t, _)

248+ mkTyDecl (n, op, t, _)

249− = PTy emptyDocstring [] syn fc op n

249+ = PTy emptyDocstring [] syn fc op n NoFC

250 (mkUniqueNames [] t)

251

252 conbind :: [(Name, PTerm)] -> PTerm -> PTerm

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

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

93 Provide tm

94 | ProvTerm ty _ <- what ->

95 do -- Finally add a top-level definition of the provided term

96− elabType info syn doc [] fc [] n ty

96+ elabType info syn doc [] fc [] n NoFC ty

97 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

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

99 | ProvPostulate _ <- what ->

src/Idris/Elab/Record.hs+5−2

@@ -313,7 +313,8 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f

313 where

314 -- | The type of the projection function.

315 generateTy :: PDecl

316+ generateTy = PTy pdoc [] psyn fc [] pname NoFC $

316− generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName NoFC targetTy projTy

317+ PPi expl recName NoFC targetTy projTy

317

318

318 -- | The left hand side of the projection function.

319 -- | The left hand side of the projection function.

319 generateLhs :: PTerm

320 generateLhs :: PTerm

@@ -375,7 +376,9 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option

375 where

376 where

376 -- | The type of the update function.

377 -- | The type of the update function.

377 generateTy :: PDecl

378 generateTy :: PDecl

379+ generateTy = PTy pdoc [] psyn fc [] set_pname NoFC $

380+ PPi expl (nsroot pname) NoFC pty $

378− generateTy = PTy pdoc [] psyn fc [] set_pname $ PPi expl (nsroot pname) NoFC pty (PPi expl recName NoFC sty (substInput sty))

381+ PPi expl recName NoFC sty (substInput sty)

379 where substInput = substMatches [(cname, PRef fc (nsroot pname))]

382 where substInput = substMatches [(cname, PRef fc (nsroot pname))]

380

383

381 -- | The "_set" name.

384 -- | The "_set" name.

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

@@ -120,14 +120,15 @@ buildType info syn fc opts n ty' = do

120-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

121elabType :: ElabInfo -> SyntaxInfo

122 -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))]

123+ -> FC -> FnOpts -> Name -> FC -- ^ The precise location of the name

123− -> FC -> FnOpts -> Name -> PTerm -> Idris Type

124+ -> PTerm -> Idris Type

124elabType = elabType' False

125elabType = elabType' False

125

126

126elabType' :: Bool -> -- normalise it

127elabType' :: Bool -> -- normalise it

127 ElabInfo -> SyntaxInfo ->

128 ElabInfo -> SyntaxInfo ->

128 Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

129 Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

129− FC -> FnOpts -> Name -> PTerm -> Idris Type

130+ FC -> FnOpts -> Name -> FC -> PTerm -> Idris Type

130−elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

131+elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (params info) ty_in

131 n = liftname info n_in in -}

132 n = liftname info n_in in -}

132 do checkUndefined fc n

133 do checkUndefined fc n

133 (cty, _, ty, inacc) <- buildType info syn fc opts n ty'

134 (cty, _, ty, inacc) <- buildType info syn fc opts n ty'

@@ -192,6 +193,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

192 addIBC (IBCErrorHandler n)

193 addIBC (IBCErrorHandler n)

193 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

194 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

194 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

195 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

196+ -- Send highlighting information about the name being declared

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

195 -- if it's an export list type, make a note of it

198 -- if it's an export list type, make a note of it

196 case (unApply usety) of

199 case (unApply usety) of

197 (P _ ut _, _)

200 (P _ ut _, _)

@@ -229,7 +232,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

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

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

230 FC -> FnOpts -> Name -> PTerm -> Idris ()

233 FC -> FnOpts -> Name -> PTerm -> Idris ()

231elabPostulate info syn doc fc opts n ty = do

234elabPostulate info syn doc fc opts n ty = do

232− elabType info syn doc [] fc opts n ty

235+ elabType info syn doc [] fc opts n NoFC ty

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

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

234 addIBC (IBCPostulate n)

237 addIBC (IBCPostulate n)

235

238

@@ -239,7 +242,7 @@ elabPostulate info syn doc fc opts n ty = do

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

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

240 FC -> FnOpts -> Name -> PTerm -> Idris ()

243 FC -> FnOpts -> Name -> PTerm -> Idris ()

241elabExtern info syn doc fc opts n ty = do

244elabExtern info syn doc fc opts n ty = do

242− cty <- elabType info syn doc [] fc opts n ty

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

243 ist <- getIState

246 ist <- getIState

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

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

245

248

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

@@ -124,7 +124,7 @@ checkDocs fc args tm = cd (Map.fromList args) tm

124 ++ (concat . intersperse ", " . map show . Map.keys) as

125 ++ " but they were not found."

126

127−decorateid decorate (PTy doc argdocs s f o n t) = PTy doc argdocs s f o (decorate n) t

127+decorateid decorate (PTy doc argdocs s f o n nfc t) = PTy doc argdocs s f o (decorate n) nfc t

128decorateid decorate (PClauses f o n cs)

129 = PClauses f o (decorate n) (map dc cs)

130 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

@@ -272,8 +272,8 @@ getStatics ns (Bind n (Pi _ _ _) t)

272getStatics _ _ = []

273

274mkStatic :: [Name] -> PDecl -> PDecl

275−mkStatic ns (PTy doc argdocs syn fc o n ty)

275+mkStatic ns (PTy doc argdocs syn fc o n nfc ty)

276− = PTy doc argdocs syn fc o n (mkStaticTy ns ty)

276+ = PTy doc argdocs syn fc o n nfc (mkStaticTy ns ty)

277mkStatic ns t = t

278

279mkStaticTy :: [Name] -> PTerm -> PTerm

src/Idris/ElabDecls.hs+2−2

@@ -156,10 +156,10 @@ elabDecl' _ info (PFix _ _ _)

156 = return () -- nothing to elaborate

157elabDecl' _ info (PSyntax _ p)

158 = return () -- nothing to elaborate

159−elabDecl' what info (PTy doc argdocs s f o n ty)

159+elabDecl' what info (PTy doc argdocs s f o n nfc ty)

160 | what /= EDefns

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

162− elabType info s doc argdocs f o n ty

162+ elabType info s doc argdocs f o n nfc ty

163 return ()

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

165 | what /= EDefns

src/Idris/IBC.hs+4−2

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

1144 put x1

1145 put x2

1146 put x3

1147− PTy x1 x2 x3 x4 x5 x6 x7

1147+ PTy x1 x2 x3 x4 x5 x6 x7 x8

1148 -> do putWord8 1

1149 put x1

1150 put x2

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

1153 put x5

1154 put x6

1155 put x7

1156+ put x8

1156 PClauses x1 x2 x3 x4 -> do putWord8 2

1157 PClauses x1 x2 x3 x4 -> do putWord8 2

1157 put x1

1158 put x1

1158 put x2

1159 put x2

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

1258 x5 <- get

1259 x5 <- get

1259 x6 <- get

1260 x6 <- get

1260 x7 <- get

1261 x7 <- get

1262+ x8 <- get

1261− return (PTy x1 x2 x3 x4 x5 x6 x7)

1263+ return (PTy x1 x2 x3 x4 x5 x6 x7 x8)

1262 2 -> do x1 <- get

1264 2 -> do x1 <- get

1263 x2 <- get

1265 x2 <- get

1264 x3 <- get

1266 x3 <- get

src/Idris/Output.hs+8−8

@@ -33,20 +33,20 @@ instance MonadException m => MonadException (ExceptT Err m) where

33pshow :: IState -> Err -> String

34pshow ist err = displayDecorated (consoleDecorate ist) .

35 renderPretty 1.0 80 .

36− fmap (fancifyAnnots ist) $ pprintErr ist err

36+ fmap (fancifyAnnots ist True) $ pprintErr ist err

37

38iWarn :: FC -> Doc OutputAnnotation -> Idris ()

39iWarn fc err =

40 do i <- getIState

41 case idris_outputmode i of

42 RawOutput h ->

43− do err' <- iRender . fmap (fancifyAnnots i) $

43+ do err' <- iRender . fmap (fancifyAnnots i True) $

44 case fc of

45 FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err

46 _ -> err

47 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

48 IdeMode n h ->

49− do err' <- iRender . fmap (fancifyAnnots i) $ err

49+ do err' <- iRender . fmap (fancifyAnnots i True) $ err

50 let (str, spans) = displaySpans err'

51 runIO . hPutStrLn h $

52 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

@@ -97,7 +97,7 @@ iRenderOutput doc =

97 RawOutput h -> do out <- iRender doc

98 runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

99 IdeMode n h ->

100− do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc

100+ do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i True) $ doc

101 let out = [toSExp str, toSExp spans]

102 runIO . hPutStrLn h $ convSExp "write-decorated" out n

103

@@ -112,7 +112,7 @@ ideModeReturnWithStatus status n h out = do

112 ist <- getIState

113 (str, spans) <- fmap displaySpans .

114 iRender .

115− fmap (fancifyAnnots ist) $

115+ fmap (fancifyAnnots ist True) $

116 out

117 let good = [SymbolAtom status, toSExp str, toSExp spans]

118 runIO . hPutStrLn h $ convSExp "return" good n

@@ -168,7 +168,7 @@ iputGoal g = do i <- getIState

168 case idris_outputmode i of

169 RawOutput h -> runIO $ hPutStrLn h (displayDecorated (consoleDecorate i) g)

170 IdeMode n h ->

171− let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g

171+ let (str, spans) = displaySpans . fmap (fancifyAnnots i True) $ g

172 goal = [toSExp str, toSExp spans]

173 in runIO . hPutStrLn h $ convSExp "write-goal" goal n

174

@@ -201,7 +201,7 @@ sendHighlighting highlights =

201 case idris_outputmode ist of

202 RawOutput _ -> return ()

203 IdeMode n h ->

204− let fancier = [toSExp (fc, fancifyAnnots ist annot) | (fc, annot) <- highlights]

204+ let fancier = [toSExp (fc, fancifyAnnots ist False annot) | (fc, annot) <- highlights]

205 in runIO . hPutStrLn h $

206 convSExp "output"

207 (SymbolAtom "ok",

@@ -217,7 +217,7 @@ renderExternal fmt width doc

217 return . wrap fmt .

218 displayDecorated (decorate fmt) .

219 renderPretty 1.0 width .

220− fmap (fancifyAnnots ist) $

220+ fmap (fancifyAnnots ist True) $

221 doc

222 where

223 decorate _ (AnnFC _) = id

src/Idris/Parser.hs+6−5

@@ -392,7 +392,7 @@ fnDecl syn = try (do notEndBlock

392-}

393fnDecl' :: SyntaxInfo -> IdrisParser PDecl

394fnDecl' syn = checkFixity $

395− do (doc, argDocs, fc, opts', n, acc) <- try (do

395+ do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do

396 pushIndent

397 (doc, argDocs) <- docstring syn

398 ist <- get

@@ -402,15 +402,15 @@ fnDecl' syn = checkFixity $

402 opts <- fnOpts initOpts

403 acc <- optional accessibility

404 opts' <- fnOpts opts

405− n_in <- fst <$> fnName

405+ (n_in, nfc) <- fnName

406 let n = expandNS syn n_in

407 fc <- getFC

408 lchar ':'

409− return (doc, argDocs, fc, opts', n, acc))

409+ return (doc, argDocs, fc, opts', n, nfc, acc))

410 ty <- typeExpr (allowImp syn)

411 terminator

412 addAcc n acc

413− return (PTy doc argDocs syn fc opts' n ty)

413+ return (PTy doc argDocs syn fc opts' n nfc ty)

414 <|> postulate syn

415 <|> caf syn

416 <|> pattern syn

@@ -423,7 +423,7 @@ fnDecl' syn = checkFixity $

423 unless fOk . fail $

424 "Missing fixity declaration for " ++ show n

425 return decl

426− getName (PTy _ _ _ _ _ n _) = Just n

426+ getName (PTy _ _ _ _ _ n _ _) = Just n

427 getName _ = Nothing

428 fixityOK (NS n _) = fixityOK n

429 fixityOK (UN n) | all (flip elem opChars) (str n) =

@@ -437,6 +437,7 @@ fnDecl' syn = checkFixity $

437@

438FnOpts ::= 'total'

439 | 'partial'

440+ | 'covering'

440 | 'implicit'

441 | 'implicit'

441 | '%' 'no_implicit'

442 | '%' 'no_implicit'

442 | '%' 'assert_total'

443 | '%' 'assert_total'

src/Idris/REPL.hs+11−11

@@ -438,7 +438,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

438 in

439 displaySpans .

440 renderPretty 0.9 cols .

441− fmap (fancifyAnnots ist) .

441+ fmap (fancifyAnnots ist True) .

442 annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $

443 prettyT

444

@@ -463,7 +463,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.WhoCalls n) =

463 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

464 where pn ist = displaySpans .

465 renderPretty 0.9 1000 .

466− fmap (fancifyAnnots ist) .

466+ fmap (fancifyAnnots ist True) .

467 prettyName True True []

468

469runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

@@ -476,7 +476,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

476 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

477 where pn ist = displaySpans .

478 renderPretty 0.9 1000 .

479− fmap (fancifyAnnots ist) .

479+ fmap (fancifyAnnots ist True) .

480 prettyName True True []

481

482runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) =

@@ -491,7 +491,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) =

491 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

492 where pn ist = displaySpans .

493 renderPretty 0.9 1000 .

494− fmap (fancifyAnnots ist) .

494+ fmap (fancifyAnnots ist True) .

495 prettyName True True []

496runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =

497 do ctxt <- getContext

@@ -506,7 +506,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =

506 msg = (IdeMode.SymbolAtom "ok",

507 displaySpans .

508 renderPretty 0.9 80 .

509− fmap (fancifyAnnots ist) $ ptm)

509+ fmap (fancifyAnnots ist True) $ ptm)

510 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

511runIdeModeCommand h id orig fn modes (IdeMode.TermShowImplicits bnd tm) =

512 ideModeForceTermImplicits h id bnd True tm

@@ -519,7 +519,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.TermElab bnd tm) =

519 msg = (IdeMode.SymbolAtom "ok",

520 displaySpans .

521 renderPretty 0.9 70 .

522− fmap (fancifyAnnots ist) $ ptm)

522+ fmap (fancifyAnnots ist True) $ ptm)

523 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

524runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =

525 case splitName name of

@@ -535,7 +535,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.ErrPPrint e) =

535 let (out, spans) =

536 displaySpans .

537 renderPretty 0.9 80 .

538− fmap (fancifyAnnots ist) $ pprintErr ist e

538+ fmap (fancifyAnnots ist True) $ pprintErr ist e

539 msg = (IdeMode.SymbolAtom "ok", out, spans)

540 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

541runIdeModeCommand h id orig fn modes IdeMode.GetIdrisVersion =

@@ -558,7 +558,7 @@ ideModeForceTermImplicits h id bnd impl tm =

558 msg = (IdeMode.SymbolAtom "ok",

559 displaySpans .

560 renderPretty 0.9 80 .

561− fmap (fancifyAnnots ist) $ expl)

561+ fmap (fancifyAnnots ist True) $ expl)

562 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

563

564splitName :: String -> Either String Name

@@ -788,7 +788,7 @@ process fn (NewDefn decls) = do

788 mapM_ defineName namedGroups where

789 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

790 getName :: PDecl -> Maybe Name

791− getName (PTy docs argdocs syn fc opts name ty) = Just name

791+ getName (PTy docs argdocs syn fc opts name _ ty) = Just name

792 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

793 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

794 getName (PClass doc syn fc constraints name parms parmdocs fds decls) = Just name

@@ -797,7 +797,7 @@ process fn (NewDefn decls) = do

797 getClauseName (PClause fc name whole with rhs whereBlock) = name

798 getClauseName (PWith fc name whole with rhs pn whereBlock) = name

799 defineName :: [PDecl] -> Idris ()

800− defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do

800+ defineName (tyDecl@(PTy docs argdocs syn fc opts name _ ty) : decls) = do

801 elabDecl EAll recinfo tyDecl

802 elabClauses recinfo fc opts name (concatMap getClauses decls)

803 setReplDefined (Just name)

@@ -896,7 +896,7 @@ process fn (Check (PRef _ n))

896 case lookupNames n ctxt of

897 ts@(t:_) ->

898 case lookup t (idris_metavars ist) of

899− Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $

899+ Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

900 showMetavarInfo ppo ist n i

901 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

902 [] -> iPrintError $ "No such variable " ++ show n

src/Idris/TypeSearch.hs+1−1

@@ -47,7 +47,7 @@ searchByType pkgs pterm = do

47 pterm' <- addUsingConstraints syn emptyFC pterm

48 pterm'' <- implicit toplevel syn name pterm'

49 let pterm''' = addImpl [] i pterm''

50− ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

50+ ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'

51 let names = searchUsing searchPred i ty

52 let names' = take numLimit names

53 let docs =