@@ -1,4 +1,4 @@
1−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
1+{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, TupleSections #-}
22module Idris.ParseExpr where
33
44import Prelude hiding (pi)
@@ -129,7 +129,7 @@ extensions syn rules = extension syn [] (filter isValid rules)
129129 isValid (Rule _ _ PatternSyntax) = inPattern syn
130130 isValid (Rule _ _ TermSyntax) = not (inPattern syn)
131131
132−data SynMatch = SynTm PTerm | SynBind Name
132+data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information
133133
134134extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
135135extension syn ns rules =
@@ -154,8 +154,8 @@ extension syn ns rules =
154154 return $ Just (n, SynTm tm)
155155 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
156156 return $ Just (n, SynTm tm)
157− extensionSymbol (Binding n) = do b <- fst <$> name
158− return $ Just (n, SynBind b)
157+ extensionSymbol (Binding n) = do (b, fc) <- name
158+ return $ Just (n, SynBind fc b)
159159 extensionSymbol (Symbol s) = do fc <- symbolFC s
160160 highlightP fc AnnKeyword
161161 return Nothing
@@ -168,29 +168,33 @@ extension syn ns rules =
168168 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
169169 flatten t = t
170170
171− updateB :: [(Name, SynMatch)] -> Name -> Name
172− updateB ns n = case lookup n ns of
173− Just (SynBind t) -> t
174− _ -> n
171+ updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
172+ updateB ns (n, fc) = case lookup n ns of
173+ Just (SynBind tfc t) -> (t, tfc)
174+ _ -> (n, fc)
175175
176176 update :: [(Name, SynMatch)] -> PTerm -> PTerm
177177 update ns (PRef fc hls n) = case lookup n ns of
178178 Just (SynTm t) -> t
179179 _ -> PRef fc hls n
180− update ns (PPatvar fc n) = PPatvar fc $ updateB ns n
180+ update ns (PPatvar fc n) = uncurry (flip PPatvar) $ updateB ns (n, fc)
181181 update ns (PLam fc n nfc ty sc)
182− = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)
182+ = let (n', nfc') = updateB ns (n, nfc)
183+ in PLam fc n' nfc' (update ns ty) (update (dropn n ns) sc)
183184 update ns (PPi p n fc ty sc)
184− = PPi (updTacImp ns p) (updateB ns n) fc
185− (update ns ty) (update (dropn n ns) sc)
186− update ns (PLet fc n nfc ty val sc)
187− = PLet fc (updateB ns n) nfc (update ns ty)
188− (update ns val) (update (dropn n ns) sc)
185+ = let (n', nfc') = updateB ns (n, fc)
186+ in PPi (updTacImp ns p) n' nfc'
187+ (update ns ty) (update (dropn n ns) sc)
188+ update ns (PLet fc n nfc ty val sc)
189+ = let (n', nfc') = updateB ns (n, nfc)
190+ in PLet fc n' nfc' (update ns ty)
191+ (update ns val) (update (dropn n ns) sc)
189192 update ns (PApp fc t args)
190193 = PApp fc (update ns t) (map (fmap (update ns)) args)
191194 update ns (PAppBind fc t args)
192195 = PAppBind fc (update ns t) (map (fmap (update ns)) args)
193− update ns (PMatchApp fc n) = PMatchApp fc $ updateB ns n
196+ update ns (PMatchApp fc n) = let (n', nfc') = updateB ns (n, fc)
197+ in PMatchApp nfc' n'
194198 update ns (PIfThenElse fc c t f)
195199 = PIfThenElse fc (update ns c) (update ns t) (update ns f)
196200 update ns (PCase fc c opts)
@@ -200,7 +204,7 @@ extension syn ns rules =
200204 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)
201205 update ns (PDPair fc hls p l t r)
202206 = PDPair fc hls p (update ns l) (update ns t) (update ns r)
203− update ns (PAs fc n t) = PAs fc (updateB ns n) (update ns t)
207+ update ns (PAs fc n t) = PAs fc (fst $ updateB ns (n, NoFC)) (update ns t)
204208 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)
205209 update ns (PHidden t) = PHidden (update ns t)
206210 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
@@ -214,7 +218,7 @@ extension syn ns rules =
214218 (map (\(l,r) -> (update ns l, update ns r)) ts)
215219 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
216220 update ns (PIdiom fc t) = PIdiom fc $ update ns t
217− update ns (PMetavar fc n) = PMetavar fc $ updateB ns n
221+ update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)
218222 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
219223 update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs
220224 update ns (PDisamb nsps t) = PDisamb nsps $ update ns t
@@ -222,7 +226,7 @@ extension syn ns rules =
222226 update ns (PNoImplicits t) = PNoImplicits $ update ns t
223227 update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)
224228 update ns (PUnquote t) = PUnquote $ update ns t
225− update ns (PQuoteName n fc) = PQuoteName (updateB ns n) fc
229+ update ns (PQuoteName n fc) = uncurry PQuoteName (updateB ns (n, fc))
226230 update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp
227231 update ns (PConstSugar fc t) = PConstSugar fc $ update ns t
228232 -- PConstSugar probably can't contain anything substitutable, but it's hard to track
@@ -230,19 +234,19 @@ extension syn ns rules =
230234
231235 updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
232236 -- handle all the ones with Names explicitly, then use fmap for the rest with PTerms
233− updTactic ns (Intro ns') = Intro $ map (updateB ns) ns'
234− updTactic ns (Focus n) = Focus $ updateB ns n
235− updTactic ns (Refine n bs) = Refine (updateB ns n) bs
236− updTactic ns (Claim n t) = Claim (updateB ns n) (update ns t)
237− updTactic ns (MatchRefine n) = MatchRefine (updateB ns n)
238− updTactic ns (LetTac n t) = LetTac (updateB ns n) (update ns t)
239− updTactic ns (LetTacTy n ty tm) = LetTacTy (updateB ns n) (update ns ty) (update ns tm)
237+ updTactic ns (Intro ns') = Intro $ map (fst . updateB ns . (, NoFC)) ns'
238+ updTactic ns (Focus n) = Focus . fst $ updateB ns (n, NoFC)
239+ updTactic ns (Refine n bs) = Refine (fst $ updateB ns (n, NoFC)) bs
240+ updTactic ns (Claim n t) = Claim (fst $ updateB ns (n, NoFC)) (update ns t)
241+ updTactic ns (MatchRefine n) = MatchRefine (fst $ updateB ns (n, NoFC))
242+ updTactic ns (LetTac n t) = LetTac (fst $ updateB ns (n, NoFC)) (update ns t)
243+ updTactic ns (LetTacTy n ty tm) = LetTacTy (fst $ updateB ns (n, NoFC)) (update ns ty) (update ns tm)
240244 updTactic ns (ProofSearch rec prover depth top psns hints) = ProofSearch rec prover depth
241− (fmap (updateB ns) top) (map (updateB ns) psns) (map (updateB ns) hints)
245+ (fmap (fst . updateB ns . (, NoFC)) top) (map (fst . updateB ns . (, NoFC)) psns) (map (fst . updateB ns . (, NoFC)) hints)
242246 updTactic ns (Try l r) = Try (updTactic ns l) (updTactic ns r)
243247 updTactic ns (TSeq l r) = TSeq (updTactic ns l) (updTactic ns r)
244248 updTactic ns (GoalType s tac) = GoalType s $ updTactic ns tac
245− updTactic ns (TDocStr (Left n)) = TDocStr . Left $ updateB ns n
249+ updTactic ns (TDocStr (Left n)) = TDocStr . Left . fst $ updateB ns (n, NoFC)
246250 updTactic ns t = fmap (update ns) t
247251
248252 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)