STLC+Nat Exhaustivity Checking

AST.hs

module AST where

-- | Name binding association
data Binder = NullBinder       -- Wildcard binder
            | Zero             -- Zero binder
            | Succ Binder      -- Nat binder
  deriving (Show, Eq)

-- | Basic representations of cases
type Case = [Binder]

type Cases = [Case]

-- | Result
type Result = Cases

-- | Pattern Matching definition 
type DefPm = Cases

Checker.hs

module Checker where

import AST

-- | unmatched: returns the list
--   * of `_` for the first uncovered set
unmatched :: Case -> Cases
unmatched c = [unmatched' c]

unmatched' :: Case -> Case
unmatched' = foldr op []
  where
  op :: Binder -> Case -> Case
  op _ c = NullBinder:c

-- | check: given a pattern matching definition
--   * we check whether or not it is exhaustive
--   * giving the resultant non-covered cases
check :: DefPm -> Result
check [] = []
check pmdef@(pm:_) =
  check_uncovers unm pmdef
  where
  unm = unmatched pm

-- | uncover: single binder uncovering
--   * this returns the difference between
--   * two single binders
uncover :: Binder -> Binder -> Case
uncover Zero Zero = []
uncover _ NullBinder = []
uncover NullBinder b =
  let all_pat = [Zero, Succ NullBinder]
  in concat $ map (\cp -> uncover cp b) all_pat
uncover (Succ n) (Succ m) =
  let ucs = uncover n m
  in (zip_con Succ) ucs
  where
    zip_con :: (Binder -> Binder) -> Case -> Case
    zip_con _ [] = []
    zip_con b bs = (b hps):rest
      where
      (hps, rest) = (head bs, tail bs)
uncover b _ = [b]

-- | uncovers: given an uncovered case and a clause
--   * of a pattern match definition,
--   * returns the uncovered cases
uncovers :: Case -> Case -> Cases
-- empty case
uncovers [] [] = []
-- any-var
uncovers (u:us) (NullBinder:ps) =
  map (u:) (uncovers us ps)
-- zero-zero
uncovers (Zero:us) (Zero:ps) =
  map (Zero:) (uncovers us ps)
-- succ-zero
uncovers ucs@((Succ _):_) (Zero:_) =
  [ucs]
-- zero-succ
uncovers ucs@(Zero:_) ((Succ _):_) =
  [ucs]
-- succ-succ
uncovers ((Succ n):us) ((Succ m):ps) =
  let ucs = uncovers (n:us) (m:ps)
  in map (zip_con Succ) ucs
    where
    -- This *must* be generalized for all constructors
    zip_con :: (Binder -> Binder) -> Case -> Case
    zip_con _ [] = []
    zip_con b xs = (b hps):rest
      where
      (hps, rest) = (head xs, tail xs)
-- var-nat
uncovers (NullBinder:us) pats@(_:_) =
  -- This must be something that traverse all constructors of a type
  let all_pat = [Zero, Succ NullBinder]
      uncovered = map (\cp -> uncovers (cp:us) pats) all_pat
  in concat uncovered
-- I guess other cases must fail inside a monad
uncovers _ _ = []

-- | uncovering: returns the cases
--   * that are not covered by a single clause
uncovering :: Cases -> Case -> Cases
uncovering unc clause =
  concat $ map (\u -> uncovers u clause) unc

-- | check_uncovers: Given an uncovered set and a full pm definition
--   * this calculates the cases that are not covered by
--   * the pattern matching definition
check_uncovers :: Cases -> Cases -> Cases
check_uncovers ucs [] = ucs
check_uncovers ucs (c:cs) =
  let ucs' = uncovering ucs c
  in check_uncovers ucs' cs

-- | is_exhaustive: returns whether or not
--   * the given definition is exhaustive
is_exhaustive :: DefPm -> Bool
is_exhaustive = null . check

Tests.hs

module Tests where

import AST
import Checker
import Data.List

type TestCase = Cases

n = NullBinder

-- | test: Testing function
test :: DefPm -> TestCase -> Bool
test f tc = null $ (\\) (check f) tc

-- | f: simple non-exhaustive
--   * function
f :: DefPm 
f = [[Zero]]

-- | g: another non-exhaustive
--   * function
g :: DefPm
g = [[Succ $ Succ $ Succ Zero]]

-- | exh: simple exhaustive definition
exh :: DefPm
exh = [[Succ n], [Zero]]

-- | min: the patterns of 
--   * a `min` function
_min :: DefPm
_min = [[Zero, n], [n, Zero], [Succ n, Succ n]]

-- | crazy: some crazy function
crazy :: DefPm
crazy = [[Zero, Succ n, Succ Zero], [Succ n, Zero, Succ $ Succ Zero]]

-- | Checking the results of the above definitions
--   * The uncovered cases for each definition were taken by executing
--   * those definitions in Haskell with -Wall

-- * f : should not be exhaustive
-- * the missing case is [Succ _]
test_f :: Bool
test_f = test f [[Succ n]]

-- * g: should not be exhaustive
-- * the missing cases are [Zero, Succ Zero, Succ (Succ Zero), Succ (Succ (Succ (Succ _)))]
test_g :: Bool
test_g = test g [[Zero], [Succ Zero], [Succ (Succ Zero)], [Succ (Succ (Succ (Succ n)))]]

-- * exh: should be exhaustive
test_exh :: Bool
test_exh = test exh []

-- * min: should be exhaustive
test_min :: Bool
test_min = test _min []

-- * crazy: should not be exhaustive
-- * the missing cases are:
-- * *Main> let f Zero (Succ _) (Succ Zero) = Zero; f (Succ _) Zero (Succ (Succ Zero)) = Zero
-- *
-- *Pattern match(es) are non-exhaustive
-- *In an equation for ‘f’:
-- *    Patterns not matched:
-- *        Zero Zero _
-- *        Zero (Succ _) Zero
-- *        Zero (Succ _) (Succ (Succ _))
-- *        (Succ _) (Succ _) _
-- *        (Succ _) Zero Zero
-- *        (Succ _) Zero (Succ Zero)
-- *        (Succ _) Zero (Succ (Succ (Succ _)))
test_crazy :: Bool
test_crazy = test crazy [[Zero, Zero, n], [Zero, Succ n, Zero], [Zero, Succ n, Succ $ Succ n], [Succ n, Succ n, n],
                         [Succ n, Zero, Zero], [Succ n, Zero, Succ Zero], [Succ n, Zero, Succ $ Succ $ Succ n]]