ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 14:38:20 +03:00
Code Issues Projects Releases Wiki Activity

Add tactic cases to syntax substitution

Browse Source
This commit is contained in:
Melvar Chen 2015-08-13 16:45:21 +02:00
parent 7c660c6ac4
commit 7f6aeab69c
1 changed files with 19 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/Idris/ParseExpr.hs
View File

@ -215,6 +215,8 @@ extension syn ns rules =
upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t) upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
update ns (PIdiom fc t) = PIdiom fc $ update ns t update ns (PIdiom fc t) = PIdiom fc $ update ns t
update ns (PMetavar fc n) = PMetavar fc $ updateB ns n update ns (PMetavar fc n) = PMetavar fc $ updateB ns n
update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs
update ns (PDisamb nsps t) = PDisamb nsps $ update ns t update ns (PDisamb nsps t) = PDisamb nsps $ update ns t
update ns (PUnifyLog t) = PUnifyLog $ update ns t update ns (PUnifyLog t) = PUnifyLog $ update ns t
update ns (PNoImplicits t) = PNoImplicits $ update ns t update ns (PNoImplicits t) = PNoImplicits $ update ns t
@ -226,6 +228,23 @@ extension syn ns rules =
-- PConstSugar probably can't contain anything substitutable, but it's hard to track -- PConstSugar probably can't contain anything substitutable, but it's hard to track
update ns t = t update ns t = t
updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
-- handle all the ones with Names explicitly, then use fmap for the rest with PTerms
updTactic ns (Intro ns') = Intro $ map (updateB ns) ns'
updTactic ns (Focus n) = Focus $ updateB ns n
updTactic ns (Refine n bs) = Refine (updateB ns n) bs
updTactic ns (Claim n t) = Claim (updateB ns n) (update ns t)
updTactic ns (MatchRefine n) = MatchRefine (updateB ns n)
updTactic ns (LetTac n t) = LetTac (updateB ns n) (update ns t)
updTactic ns (LetTacTy n ty tm) = LetTacTy (updateB ns n) (update ns ty) (update ns tm)
updTactic ns (ProofSearch rec prover depth top psns hints) = ProofSearch rec prover depth
(fmap (updateB ns) top) (map (updateB ns) psns) (map (updateB ns) hints)
updTactic ns (Try l r) = Try (updTactic ns l) (updTactic ns r)
updTactic ns (TSeq l r) = TSeq (updTactic ns l) (updTactic ns r)
updTactic ns (GoalType s tac) = GoalType s $ updTactic ns tac
updTactic ns (TDocStr (Left n)) = TDocStr . Left $ updateB ns n
updTactic ns t = fmap (update ns) t
updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr) updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)
updTacImp _ x = x updTacImp _ x = x