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

Fix coverage checker for sigma types

Browse Source 
Using the old name meant it checked the wrong thing so always reported
covering cases
This commit is contained in:
Edwin Brady 2015-08-20 11:43:16 +02:00
parent 0140e67bc9
commit 3288a6c8b0
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Idris/Coverage.hs
View File

@ -222,7 +222,7 @@ genAll i args
pimp (sUN "B") Placeholder True] ++ pimp (sUN "B") Placeholder True] ++
[pexp l, pexp r]) o [pexp l, pexp r]) o
otherPats o@(PDPair fc hls p t _ v) otherPats o@(PDPair fc hls p t _ v)
= ops fc (sUN "Ex_intro") = ops fc sigmaCon
([pimp (sUN "a") Placeholder True, ([pimp (sUN "a") Placeholder True,
pimp (sUN "P") Placeholder True] ++ pimp (sUN "P") Placeholder True] ++
[pexp t,pexp v]) o [pexp t,pexp v]) o
@ -243,8 +243,8 @@ genAll i args
getExpTm t = getTm t getExpTm t = getTm t
-- put it back to its original form -- put it back to its original form
resugar (PApp _ (PRef fc hl (UN ei)) [_,_,t,v]) resugar (PApp _ (PRef fc hl n) [_,_,t,v])
| ei == txt "Ex_intro" | n == sigmaCon
= PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v) = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)
resugar (PApp _ (PRef fc hl n) [_,_,l,r]) resugar (PApp _ (PRef fc hl n) [_,_,l,r])
| n == pairCon | n == pairCon