890c6a7 · Idris-dev · git.iko.soy

1−{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

1+{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, TupleSections #-}

2module Idris.ParseExpr where

3

4import Prelude hiding (pi)

129 isValid (Rule _ _ PatternSyntax) = inPattern syn

130 isValid (Rule _ _ TermSyntax) = not (inPattern syn)

131

132−data SynMatch = SynTm PTerm | SynBind Name

132+data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information

133

134extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

135extension syn ns rules =

154 return $ Just (n, SynTm tm)

155 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn

156 return $ Just (n, SynTm tm)

157− extensionSymbol (Binding n) = do b <- fst <$> name

157+ extensionSymbol (Binding n) = do (b, fc) <- name

158− return $ Just (n, SynBind b)

158+ return $ Just (n, SynBind fc b)

159 extensionSymbol (Symbol s) = do fc <- symbolFC s

160 highlightP fc AnnKeyword

161 return Nothing

168 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

169 flatten t = t

170

171− updateB :: [(Name, SynMatch)] -> Name -> Name

171+ updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)

172− updateB ns n = case lookup n ns of

172+ updateB ns (n, fc) = case lookup n ns of

173− Just (SynBind t) -> t

173+ Just (SynBind tfc t) -> (t, tfc)

174− _ -> n

174+ _ -> (n, fc)

175

176 update :: [(Name, SynMatch)] -> PTerm -> PTerm

177 update ns (PRef fc hls n) = case lookup n ns of

178 Just (SynTm t) -> t

179 _ -> 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)

181 update ns (PLam fc n nfc ty sc)

182+ = let (n', nfc') = updateB ns (n, nfc)

182− = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)

183+ in PLam fc n' nfc' (update ns ty) (update (dropn n ns) sc)

183 update ns (PPi p n fc ty sc)

184 update ns (PPi p n fc ty sc)

185+ = let (n', nfc') = updateB ns (n, fc)

184− = PPi (updTacImp ns p) (updateB ns n) fc

186+ in PPi (updTacImp ns p) n' nfc'

185− (update ns ty) (update (dropn n ns) sc)

187+ (update ns ty) (update (dropn n ns) sc)

186− update ns (PLet fc n nfc ty val sc)

188+ update ns (PLet fc n nfc ty val sc)

189+ = let (n', nfc') = updateB ns (n, nfc)

187− = PLet fc (updateB ns n) nfc (update ns ty)

190+ in PLet fc n' nfc' (update ns ty)

188− (update ns val) (update (dropn n ns) sc)

191+ (update ns val) (update (dropn n ns) sc)

189 update ns (PApp fc t args)

192 update ns (PApp fc t args)

190 = PApp fc (update ns t) (map (fmap (update ns)) args)

193 = PApp fc (update ns t) (map (fmap (update ns)) args)

191 update ns (PAppBind fc t args)

194 update ns (PAppBind fc t args)

192 = PAppBind fc (update ns t) (map (fmap (update ns)) args)

195 = 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'

194 update ns (PIfThenElse fc c t f)

198 update ns (PIfThenElse fc c t f)

195 = PIfThenElse fc (update ns c) (update ns t) (update ns f)

199 = PIfThenElse fc (update ns c) (update ns t) (update ns f)

196 update ns (PCase fc c opts)

200 update ns (PCase fc c opts)

200 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)

204 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)

201 update ns (PDPair fc hls p l t r)

205 update ns (PDPair fc hls p l t r)

202 = PDPair fc hls p (update ns l) (update ns t) (update ns r)

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

204 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)

208 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)

205 update ns (PHidden t) = PHidden (update ns t)

209 update ns (PHidden t) = PHidden (update ns t)

206 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

210 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)

214 (map (\(l,r) -> (update ns l, update ns r)) ts)

218 (map (\(l,r) -> (update ns l, update ns r)) ts)

215 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)

219 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)

216 update ns (PIdiom fc t) = PIdiom fc $ update ns t

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

218 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs

222 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs

219 update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs

223 update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs

220 update ns (PDisamb nsps t) = PDisamb nsps $ update ns t

224 update ns (PDisamb nsps t) = PDisamb nsps $ update ns t

222 update ns (PNoImplicits t) = PNoImplicits $ update ns t

226 update ns (PNoImplicits t) = PNoImplicits $ update ns t

223 update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)

227 update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)

224 update ns (PUnquote t) = PUnquote $ update ns t

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

226 update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp

230 update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp

227 update ns (PConstSugar fc t) = PConstSugar fc $ update ns t

231 update ns (PConstSugar fc t) = PConstSugar fc $ update ns t

228 -- PConstSugar probably can't contain anything substitutable, but it's hard to track

232 -- PConstSugar probably can't contain anything substitutable, but it's hard to track

230

234

231 updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic

235 updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic

232 -- handle all the ones with Names explicitly, then use fmap for the rest with PTerms

236 -- 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'

237+ updTactic ns (Intro ns') = Intro $ map (fst . updateB ns . (, NoFC)) ns'

234− updTactic ns (Focus n) = Focus $ updateB ns n

238+ updTactic ns (Focus n) = Focus . fst $ updateB ns (n, NoFC)

235− updTactic ns (Refine n bs) = Refine (updateB ns n) bs

239+ updTactic ns (Refine n bs) = Refine (fst $ updateB ns (n, NoFC)) bs

236− updTactic ns (Claim n t) = Claim (updateB ns n) (update ns t)

240+ updTactic ns (Claim n t) = Claim (fst $ updateB ns (n, NoFC)) (update ns t)

237− updTactic ns (MatchRefine n) = MatchRefine (updateB ns n)

241+ updTactic ns (MatchRefine n) = MatchRefine (fst $ updateB ns (n, NoFC))

238− updTactic ns (LetTac n t) = LetTac (updateB ns n) (update ns t)

242+ updTactic ns (LetTac n t) = LetTac (fst $ updateB ns (n, NoFC)) (update ns t)

239− updTactic ns (LetTacTy n ty tm) = LetTacTy (updateB ns n) (update ns ty) (update ns tm)

243+ updTactic ns (LetTacTy n ty tm) = LetTacTy (fst $ updateB ns (n, NoFC)) (update ns ty) (update ns tm)

240 updTactic ns (ProofSearch rec prover depth top psns hints) = ProofSearch rec prover depth

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

242 updTactic ns (Try l r) = Try (updTactic ns l) (updTactic ns r)

246 updTactic ns (Try l r) = Try (updTactic ns l) (updTactic ns r)

243 updTactic ns (TSeq l r) = TSeq (updTactic ns l) (updTactic ns r)

247 updTactic ns (TSeq l r) = TSeq (updTactic ns l) (updTactic ns r)

244 updTactic ns (GoalType s tac) = GoalType s $ updTactic ns tac

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

246 updTactic ns t = fmap (update ns) t

250 updTactic ns t = fmap (update ns) t

247

251

248 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

252 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)