From eb3cba5f85ddf8e60f06724e398a4f597de42fdb Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 23 May 2020 11:03:54 +0100 Subject: [PATCH] Better checking for empty types This improves coverage checking, because it can now see that things like (Z = S x) and (x = S x) are empty. Previously, it only checked that all possible constructors had a disjoint index. Now, it looks for matches and checks for disjointness in the matches, which catches a lot more things especially with equality. --- src/Core/Coverage.idr | 119 +++++++++++++++++++++++------ src/TTImp/ProcessDef.idr | 3 +- tests/Main.idr | 2 +- tests/idris2/coverage005/expected | 3 +- tests/idris2/coverage006/Cover.idr | 20 ----- tests/idris2/coverage007/eq.idr | 30 ++++++++ tests/idris2/coverage007/expected | 3 + tests/idris2/coverage007/run | 3 + 8 files changed, 136 insertions(+), 47 deletions(-) delete mode 100644 tests/idris2/coverage006/Cover.idr create mode 100644 tests/idris2/coverage007/eq.idr create mode 100644 tests/idris2/coverage007/expected create mode 100755 tests/idris2/coverage007/run diff --git a/src/Core/Coverage.idr b/src/Core/Coverage.idr index 42e49f24c..fb672af20 100644 --- a/src/Core/Coverage.idr +++ b/src/Core/Coverage.idr @@ -7,59 +7,132 @@ import Core.Normalise import Core.TT import Core.Value +import Data.Bool.Extra import Data.List import Data.NameMap %default covering +-- Return whether any of the name matches conflict +conflictMatch : {vars : _} -> List (Name, Term vars) -> Bool +conflictMatch [] = False +conflictMatch ((x, tm) :: ms) + = if conflictArgs x tm ms + then True + else conflictMatch ms + where + clash : Term vars -> Term vars -> Bool + clash (Ref _ (DataCon t _) _) (Ref _ (DataCon t' _) _) + = t /= t' + clash _ _ = False + + findN : Nat -> Term vars -> Bool + findN i (Local _ _ i' _) = i == i' + findN i tm + = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm + | _ => False in + anyTrue (map (findN i) args) + + -- Assuming in normal form. Look for: mismatched constructors, or + -- a name appearing strong rigid in the other term + conflictTm : Term vars -> Term vars -> Bool + conflictTm (Local _ _ i _) tm + = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm + | _ => False in + anyTrue (map (findN i) args) + conflictTm tm (Local _ _ i _) + = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm + | _ => False in + anyTrue (map (findN i) args) + conflictTm tm tm' + = let (f, args) = getFnArgs tm + (f', args') = getFnArgs tm' in + if clash f f' + then True + else anyTrue (zipWith conflictTm args args') + + conflictArgs : Name -> Term vars -> List (Name, Term vars) -> Bool + conflictArgs n tm [] = False + conflictArgs n tm ((x, tm') :: ms) + = if n == x && conflictTm tm tm' + then True + else conflictArgs n tm ms + -- Return whether any part of the type conflicts in such a way that they -- can't possibly be equal (i.e. mismatched constructor) conflict : {vars : _} -> - Defs -> NF vars -> Name -> Core Bool -conflict defs nfty n + {auto c : Ref Ctxt Defs} -> + Defs -> Env Term vars -> NF vars -> Name -> Core Bool +conflict defs env nfty n = do Just gdef <- lookupCtxtExact n (gamma defs) | Nothing => pure False case (definition gdef, type gdef) of (DCon t arity _, dty) - => conflictNF nfty !(nf defs [] dty) + => do Nothing <- conflictNF 0 nfty !(nf defs [] dty) + | Just ms => pure $ conflictMatch ms + pure True _ => pure False where mutual - conflictArgs : List (Closure vars) -> List (Closure []) -> Core Bool - conflictArgs [] [] = pure False - conflictArgs (c :: cs) (c' :: cs') + conflictArgs : Int -> List (Closure vars) -> List (Closure []) -> + Core (Maybe (List (Name, Term vars))) + conflictArgs _ [] [] = pure (Just []) + conflictArgs i (c :: cs) (c' :: cs') = do cnf <- evalClosure defs c cnf' <- evalClosure defs c' - pure $ !(conflictNF cnf cnf') || !(conflictArgs cs cs') - conflictArgs _ _ = pure False + Just ms <- conflictNF i cnf cnf' + | Nothing => pure Nothing + Just ms' <- conflictArgs i cs cs' + | Nothing => pure Nothing + pure (Just (ms ++ ms')) + conflictArgs _ _ _ = pure (Just []) - conflictNF : NF vars -> NF [] -> Core Bool - conflictNF t (NBind fc x b sc) - = conflictNF t !(sc defs (toClosure defaultOpts [] (Erased fc False))) - conflictNF (NDCon _ n t a args) (NDCon _ n' t' a' args') + -- If the constructor type (the NF []) matches the variable type, + -- then there may be a way to construct it, so return the matches in + -- the indices. + -- If any of those matches clash, the constructor is not valid + -- e.g, Eq x x matches Eq Z (S Z), with x = Z and x = S Z + -- conflictNF returns the list of matches, for checking + conflictNF : Int -> NF vars -> NF [] -> + Core (Maybe (List (Name, Term vars))) + conflictNF i t (NBind fc x b sc) + -- invent a fresh name, in case a user has bound the same name + -- twice somehow both references appear in the result it's unlikely + -- put posslbe + = let x' = MN (show x) i in + conflictNF (i + 1) t + !(sc defs (toClosure defaultOpts [] (Ref fc Bound x'))) + conflictNF i nf (NApp _ (NRef Bound n) []) + = do empty <- clearDefs defs + pure (Just [(n, !(quote empty env nf))]) + conflictNF i (NDCon _ n t a args) (NDCon _ n' t' a' args') = if t == t' - then conflictArgs args args' - else pure True - conflictNF (NTCon _ n t a args) (NTCon _ n' t' a' args') + then conflictArgs i args args' + else pure Nothing + conflictNF i (NTCon _ n t a args) (NTCon _ n' t' a' args') = if n == n' - then conflictArgs args args' - else pure True - conflictNF (NPrimVal _ c) (NPrimVal _ c') = pure (c /= c') - conflictNF _ _ = pure False + then conflictArgs i args args' + else pure Nothing + conflictNF i (NPrimVal _ c) (NPrimVal _ c') + = if c == c' + then pure (Just []) + else pure Nothing + conflictNF _ _ _ = pure (Just []) -- Return whether the given type is definitely empty (due to there being -- no constructors which can possibly match it.) export isEmpty : {vars : _} -> - Defs -> NF vars -> Core Bool -isEmpty defs (NTCon fc n t a args) + {auto c : Ref Ctxt Defs} -> + Defs -> Env Term vars -> NF vars -> Core Bool +isEmpty defs env (NTCon fc n t a args) = case !(lookupDefExact n (gamma defs)) of Just (TCon _ _ _ _ flags _ cons _) => if not (external flags) - then allM (conflict defs (NTCon fc n t a args)) cons + then allM (conflict defs env (NTCon fc n t a args)) cons else pure False _ => pure False -isEmpty defs _ = pure False +isEmpty defs env _ = pure False -- Need this to get a NF from a Term; the names are free in any case freeEnv : FC -> (vs : List Name) -> Env Term vs diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index bc5a77c5d..7627fddec 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -329,9 +329,10 @@ bindReq fc (b :: env) (DropCons p) ns tm -- * Every constructor of the family has a return type which conflicts with -- the given constructor's type hasEmptyPat : {vars : _} -> + {auto c : Ref Ctxt Defs} -> Defs -> Env Term vars -> Term vars -> Core Bool hasEmptyPat defs env (Bind fc x (PVar c p ty) sc) - = pure $ !(isEmpty defs !(nf defs env ty)) + = pure $ !(isEmpty defs env !(nf defs env ty)) || !(hasEmptyPat defs (PVar c p ty :: env) sc) hasEmptyPat defs env _ = pure False diff --git a/tests/Main.idr b/tests/Main.idr index 074a86bd2..51d9f7f00 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -41,7 +41,7 @@ idrisTests "basic036", "basic037", "basic038", "basic039", "basic040", -- Coverage checking "coverage001", "coverage002", "coverage003", "coverage004", - "coverage005", "coverage006", + "coverage005", "coverage006", "coverage007", -- Error messages "error001", "error002", "error003", "error004", "error005", "error006", "error007", "error008", "error009", "error010", diff --git a/tests/idris2/coverage005/expected b/tests/idris2/coverage005/expected index ff248e5cb..c6440ab61 100644 --- a/tests/idris2/coverage005/expected +++ b/tests/idris2/coverage005/expected @@ -1,7 +1,6 @@ 1/1: Building Cover (Cover.idr) Main> Main.zsym is total -Main> Main.zsym': -zsym' (NS _) _ +Main> Main.zsym': All cases covered Main> Main.foo is total Main> Main.bar is total Main> Bye for now! diff --git a/tests/idris2/coverage006/Cover.idr b/tests/idris2/coverage006/Cover.idr deleted file mode 100644 index d4e53ab4c..000000000 --- a/tests/idris2/coverage006/Cover.idr +++ /dev/null @@ -1,20 +0,0 @@ -import Data.Fin - -data NNat = NZ | NS NNat - -zsym : (x : NNat) -> x = NZ -> NZ = x -zsym NZ Refl = Refl -zsym (NS _) Refl impossible - -zsym' : (x : NNat) -> x = NZ -> NZ = x -zsym' NZ Refl = Refl - -foo : Nat -> String -foo 0 = "zero" -foo 1 = "one" -foo x = "something else" - -bar : Fin (S (S (S Z))) -> String -bar 0 = "a" -bar 1 = "b" -bar 2 = "c" diff --git a/tests/idris2/coverage007/eq.idr b/tests/idris2/coverage007/eq.idr new file mode 100644 index 000000000..833f77a19 --- /dev/null +++ b/tests/idris2/coverage007/eq.idr @@ -0,0 +1,30 @@ + +eq1 : (x : Nat) -> (x = S x) -> Nat +eq1 x p impossible + +eq2 : (x : Nat) -> (S x = Z) -> Nat +eq2 x p impossible + +eq3 : (x : Nat) -> (S (S x) = (S x)) -> Nat +eq3 x p impossible + +eq4 : (x : Nat) -> (S x = x) -> Nat +eq4 x p impossible + +eq5 : (x : Nat) -> (Z = S x) -> Nat +eq5 x p impossible + +eq6 : (x : Nat) -> (S x = (S (S x))) -> Nat +eq6 x p impossible + +eqL1 : (xs : List a) -> (x :: xs = []) -> Nat +eqL1 xs p impossible + +eqL2 : (xs : List a) -> (x :: xs = x :: y :: xs) -> Nat +eqL2 xs p impossible + +badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat +badeq x y p impossible + +badeqL : (xs : List a) -> (ys : List a) -> (x :: xs = x :: y :: ys) -> Nat +badeql xs ys p impossible diff --git a/tests/idris2/coverage007/expected b/tests/idris2/coverage007/expected new file mode 100644 index 000000000..c140a4253 --- /dev/null +++ b/tests/idris2/coverage007/expected @@ -0,0 +1,3 @@ +1/1: Building eq (eq.idr) +eq.idr:27:1--29:1:badeq x y p is not a valid impossible case +eq.idr:30:1--31:1:No type declaration for Main.badeql diff --git a/tests/idris2/coverage007/run b/tests/idris2/coverage007/run new file mode 100755 index 000000000..25cac64e6 --- /dev/null +++ b/tests/idris2/coverage007/run @@ -0,0 +1,3 @@ +$1 --no-banner eq.idr --check + +rm -rf build