@@ -177,6 +177,7 @@ extension syn ns rules =
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
180181 update ns (PLam fc n nfc ty sc)
181182 = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)
182183 update ns (PPi p n fc ty sc)
@@ -189,30 +190,61 @@ extension syn ns rules =
189190 = PApp fc (update ns t) (map (fmap (update ns)) args)
190191 update ns (PAppBind fc t args)
191192 = PAppBind fc (update ns t) (map (fmap (update ns)) args)
192− update ns (PCase fc c opts)
193− = PCase fc (update ns c) (map (pmap (update ns)) opts)
193+ update ns (PMatchApp fc n) = PMatchApp fc $ updateB ns n
194194 update ns (PIfThenElse fc c t f)
195195 = PIfThenElse fc (update ns c) (update ns t) (update ns f)
196+ update ns (PCase fc c opts)
197+ = PCase fc (update ns c) (map (pmap (update ns)) opts)
198+ update ns (PRewrite fc eq tm mty)
199+ = PRewrite fc (update ns eq) (update ns tm) (fmap (update ns) mty)
196200 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)
197201 update ns (PDPair fc hls p l t r)
198202 = 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)
199204 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)
200205 update ns (PHidden t) = PHidden (update ns t)
201− update ns (PDoBlock ds) = PDoBlock $ upd ns ds
202− where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]
203− upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
204− upd ns (DoBind fc n nfc t : ds) = DoBind fc n nfc (update ns t) : upd (dropn n ns) ds
205− upd ns (DoLet fc n nfc ty t : ds) = DoLet fc n nfc (update ns ty) (update ns t)
206− : upd (dropn n ns) ds
207− upd ns (DoBindP fc i t ts : ds)
208− = DoBindP fc (update ns i) (update ns t)
209− (map (\(l,r) -> (update ns l, update ns r)) ts)
210− : upd ns ds
211− upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
212− : upd ns ds
213206 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
207+ update ns (PDoBlock ds) = PDoBlock $ map (upd ns) ds
208+ where upd :: [(Name, SynMatch)] -> PDo -> PDo
209+ upd ns (DoExp fc t) = DoExp fc (update ns t)
210+ upd ns (DoBind fc n nfc t) = DoBind fc n nfc (update ns t)
211+ upd ns (DoLet fc n nfc ty t) = DoLet fc n nfc (update ns ty) (update ns t)
212+ upd ns (DoBindP fc i t ts)
213+ = DoBindP fc (update ns i) (update ns t)
214+ (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)
216+ update ns (PIdiom fc t) = PIdiom fc $ update ns t
217+ update ns (PMetavar fc n) = PMetavar fc $ updateB ns n
218+ update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
219+ update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs
220+ update ns (PDisamb nsps t) = PDisamb nsps $ update ns t
221+ update ns (PUnifyLog t) = PUnifyLog $ update ns t
222+ update ns (PNoImplicits t) = PNoImplicits $ update ns t
223+ update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)
224+ update ns (PUnquote t) = PUnquote $ update ns t
225+ update ns (PQuoteName n fc) = PQuoteName (updateB ns n) fc
226+ update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp
227+ update ns (PConstSugar fc t) = PConstSugar fc $ update ns t
228+ -- PConstSugar probably can't contain anything substitutable, but it's hard to track
214229 update ns t = t
215230
231+ updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
232+ -- 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)
240+ 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)
242+ 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)
244+ updTactic ns (GoalType s tac) = GoalType s $ updTactic ns tac
245+ updTactic ns (TDocStr (Left n)) = TDocStr . Left $ updateB ns n
246+ updTactic ns t = fmap (update ns) t
247+
216248 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)
217249 updTacImp _ x = x
218250