f226a47 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make coverage checker look inside pairs/dependent pairs

f226a47Edwin Brady13 years ago

lib/Data/Bits.idr+3

compare with master

unifiedsplit

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

307complement (MkBits x) = MkBits (complement' x)

308

309-- TODO: Prove

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

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

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

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

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

312 | (Z, Z) = believe_me x

313 | (Z, Z) = believe_me x

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

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

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

363

364

364-- TODO: Prove

365-- TODO: Prove

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

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

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

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

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

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

369 | (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))

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

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

397

399

398-- TODO: Prove

400-- TODO: Prove

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

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

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

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

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

401 | (Z, Z) = believe_me x

404 | (Z, Z) = believe_me x

src/Idris/Coverage.hs+17−1

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

142 otherPats :: PTerm -> [PTerm]

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

144 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

145 otherPats arg = return Placeholder

153 otherPats arg = return Placeholder

146

154

147 ops fc n xs_in o

155 ops fc n xs_in o

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

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

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

150 let xs = dropForce force xs_in 0

158 let xs = dropForce force xs_in 0

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

159 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))

153 let tyn = getTy n (tt_ctxt i)

161 let tyn = getTy n (tt_ctxt i)

154 case lookupCtxt tyn (idris_datatypes i) of

162 case lookupCtxt tyn (idris_datatypes i) of

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

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

156 _ -> [p]

164 _ -> [p]

157 ops fc n arg o = return Placeholder

165 ops fc n arg o = return Placeholder

158

166

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+

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

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

160 [Optimise _ fs _] -> fs

176 [Optimise _ fs _] -> fs

161 _ -> []

177 _ -> []

src/Idris/ElabDecls.hs+2−2

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

733 do let lhs_tm = orderPats (getInferTerm lhs')

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

735 OK _ -> return True

736− _ -> return False

736+ err -> return False

737

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

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

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

741− Error _ -> return False

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

742

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

744 Idris (Either Term (Term, Term))