f226a47 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make coverage checker look inside pairs/dependent pairs

Fixes #446

commitf226a474d95fb0c6b60d3d3f0590a70a654a087f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 7 Aug 2013, 17:54 (13 years ago) parent9d8916c

3 files changed+22−3

compare with master

unifiedsplit

lib/Data/Bits.idr+3 src/Idris/Coverage.hs+17−1 src/Idris/ElabDecls.hs+2−2

lib/Data/Bits.idr+3

@@ -307,6 +307,7 @@ complement : Bits n -> Bits n

307307complement (MkBits x) = MkBits (complement' x)

308308

309309-- TODO: Prove

310+%assert_total -- can't verify coverage of with block

310311zext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

311312zext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

312313 | (Z, Z) = believe_me x

@@ -362,6 +363,7 @@ bitsToInt (MkBits x) = bitsToInt' x

362363-- cast x = MkBits (zeroUnused (natToBits n))

363364

364365-- TODO: Prove

366+%assert_total -- can't verify coverage of with block

365367sext' : machineTy (nextBytes n) -> machineTy (nextBytes (n+m))

366368sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

367369 | (Z, Z) = let pad = getPad {n=0} n in

@@ -396,6 +398,7 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

396398--signExtend {m=m} (MkBits x) = MkBits (zeroUnused (sext' x))

397399

398400-- TODO: Prove

401+%assert_total -- can't verify coverage of with block

399402trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)

400403trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))

401404 | (Z, Z) = believe_me x

src/Idris/Coverage.hs+17−1

@@ -142,6 +142,14 @@ genAll i args

142142 otherPats :: PTerm -> [PTerm]

143143 otherPats o@(PRef fc n) = ops fc n [] o

144144 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o

145+ otherPats o@(PPair fc l r)

146+ = ops fc pairCon

147+ ([pimp (UN "A") Placeholder, pimp (UN "B") Placeholder] ++

148+ [pexp l, pexp r]) o

149+ otherPats o@(PDPair fc t _ v)

150+ = ops fc (UN "Ex_intro")

151+ ([pimp (UN "a") Placeholder, pimp (UN "P") Placeholder] ++

152+ [pexp t,pexp v]) o

145153 otherPats arg = return Placeholder

146154

147155 ops fc n xs_in o

@@ -149,13 +157,21 @@ genAll i args

149157 = do let force = getForceable i n -- no need to generate forceable positions

150158 let xs = dropForce force xs_in 0

151159 xs' <- mapM otherPats (map getTm xs)

152− let p = PApp fc (PRef fc n) (zipWith upd xs' xs)

160+ let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

153161 let tyn = getTy n (tt_ctxt i)

154162 case lookupCtxt tyn (idris_datatypes i) of

155163 (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

156164 _ -> [p]

157165 ops fc n arg o = return Placeholder

158166

167+ -- put it back to its original form

168+ resugar (PApp _ (PRef fc (UN "Ex_intro")) [_,_,t,v])

169+ = PDPair fc (getTm t) Placeholder (getTm v)

170+ resugar (PApp _ (PRef fc n) [_,_,l,r])

171+ | n == pairCon

172+ = PPair fc (getTm l) (getTm r)

173+ resugar t = t

174+

159175 getForceable i n = case lookupCtxt n (idris_optimisation i) of

160176 [Optimise _ fs _] -> fs

161177 _ -> []

src/Idris/ElabDecls.hs+2−2

@@ -733,12 +733,12 @@ checkPossible info fc tcgen fname lhs_in

733733 do let lhs_tm = orderPats (getInferTerm lhs')

734734 case recheck ctxt [] (forget lhs_tm) lhs_tm of

735735 OK _ -> return True

736− _ -> return False

736+ err -> return False

737737

738738-- b <- inferredDiff fc (delab' i lhs_tm True) lhs

739739-- return (not b) -- then return (Just lhs_tm) else return Nothing

740740-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

741− Error _ -> return False

741+ err@(Error _) -> return False

742742

743743elabClause :: ElabInfo -> Bool -> (Int, PClause) ->

744744 Idris (Either Term (Term, Term))