3288a6c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix coverage checker for sigma types

Using the old name meant it checked the wrong thing so always reported covering cases

commit3288a6c8b0a3b7c8f894d31f81700a556c4e6ed8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 20 Aug 2015, 11:43 (11 years ago) parent0140e67

1 file changed+3−3

unifiedsplit

src/Idris/Coverage.hs+3−3

@@ -222,7 +222,7 @@ genAll i args

222222 pimp (sUN "B") Placeholder True] ++

223223 [pexp l, pexp r]) o

224224 otherPats o@(PDPair fc hls p t _ v)

225− = ops fc (sUN "Ex_intro")

225+ = ops fc sigmaCon

226226 ([pimp (sUN "a") Placeholder True,

227227 pimp (sUN "P") Placeholder True] ++

228228 [pexp t,pexp v]) o

@@ -243,8 +243,8 @@ genAll i args

243243 getExpTm t = getTm t

244244

245245 -- put it back to its original form

246− resugar (PApp _ (PRef fc hl (UN ei)) [_,_,t,v])

247− | ei == txt "Ex_intro"

246+ resugar (PApp _ (PRef fc hl n) [_,_,t,v])

247+ | n == sigmaCon

248248 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)

249249 resugar (PApp _ (PRef fc hl n) [_,_,l,r])

250250 | n == pairCon