-- |
-- Module      : AutoProof.Internal.Classical.CNF
-- Copyright   : (c) Artem Mavrin, 2021
-- License     : BSD3
-- Maintainer  : artemvmavrin@gmail.com
-- Stability   : experimental
-- Portability : POSIX
--
-- Functions and types related to conjunctive normal forms.
module AutoProof.Internal.Classical.CNF
  ( -- * Types
    CNF,
    Clause,
    Literal,

    -- * Conversion functions
    fromFormula,
    toFormula,
    canonicalCNF,

    -- * Operations
    substitute,
    substitutePure,
    unitLiteral,
    pureLiteral,
    getAnyLiteral,
  )
where

import AutoProof.Internal.Formula
  ( Formula
      ( And,
        Iff,
        Imp,
        Lit,
        Not,
        Or,
        Var
      ),
  )
import qualified AutoProof.Internal.Utils.DList as DList
  ( empty,
    singleton,
    toSet,
  )
import AutoProof.Internal.Utils.MapUtils (toMap)
import Control.Applicative ((<|>))
import qualified Data.List as List (find, lookup)
import Data.Map (Map)
import qualified Data.Map as Map (filterWithKey, lookup, null, toList)
import Data.Set (Set)
import qualified Data.Set as Set (filter, fromList, map, member, toList)

-- | Represents either a propositional variable or its negation, depending on
-- whether the boolean second component is 'True' or 'False', respectively.
type Literal a = (a, Bool)

-- | Represents a disjunction of literals.
type Clause a = Map a Bool

-- | Conjunctive normal form: represents a conjunction of clauses.
type CNF a = Set (Clause a)

-- | Convert a 'Formula' into conjunctive normal form.
--
-- Adapted from Figure 2.6 in
--
-- *  Samuel Mimram (2020)
--    /PROGRAM = PROOF/.
fromFormula :: Ord a => Formula a -> CNF a
fromFormula :: Formula a -> CNF a
fromFormula = (Set (a, Bool) -> Map a Bool) -> Set (Set (a, Bool)) -> CNF a
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Set (a, Bool) -> Map a Bool
forall k (t :: * -> *) v.
(Ord k, Foldable t) =>
t (k, v) -> Map k v
toMap (Set (Set (a, Bool)) -> CNF a)
-> (Formula a -> Set (Set (a, Bool))) -> Formula a -> CNF a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set (a, Bool)) -> Set (Set (a, Bool))
removeRedundantClauses (Set (Set (a, Bool)) -> Set (Set (a, Bool)))
-> (Formula a -> Set (Set (a, Bool)))
-> Formula a
-> Set (Set (a, Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DList (a, Bool)] -> Set (Set (a, Bool))
convert ([DList (a, Bool)] -> Set (Set (a, Bool)))
-> (Formula a -> [DList (a, Bool)])
-> Formula a
-> Set (Set (a, Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> [DList (a, Bool)]
forall a. Formula a -> [DList (a, Bool)]
pos
  where
    merge :: [a -> b] -> t (b -> c) -> [a -> c]
merge a :: [a -> b]
a b :: t (b -> c)
b = ((b -> c) -> [a -> c]) -> t (b -> c) -> [a -> c]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((((a -> b) -> a -> c) -> [a -> b] -> [a -> c])
-> [a -> b] -> ((a -> b) -> a -> c) -> [a -> c]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> b) -> a -> c) -> [a -> b] -> [a -> c]
forall a b. (a -> b) -> [a] -> [b]
map [a -> b]
a (((a -> b) -> a -> c) -> [a -> c])
-> ((b -> c) -> (a -> b) -> a -> c) -> (b -> c) -> [a -> c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)) t (b -> c)
b

    pos :: Formula a -> [DList (a, Bool)]
pos (Lit True) = []
    pos (Lit False) = [DList (a, Bool)
forall a. DList a
DList.empty]
    pos (Var x :: a
x) = [(a, Bool) -> DList (a, Bool)
forall a. a -> DList a
DList.singleton (a
x, Bool
True)]
    pos (Not a :: Formula a
a) = Formula a -> [DList (a, Bool)]
neg Formula a
a
    pos (Imp a :: Formula a
a b :: Formula a
b) = [DList (a, Bool)] -> [DList (a, Bool)] -> [DList (a, Bool)]
forall (t :: * -> *) a b c.
Foldable t =>
[a -> b] -> t (b -> c) -> [a -> c]
merge (Formula a -> [DList (a, Bool)]
neg Formula a
a) (Formula a -> [DList (a, Bool)]
pos Formula a
b)
    pos (Or a :: Formula a
a b :: Formula a
b) = [DList (a, Bool)] -> [DList (a, Bool)] -> [DList (a, Bool)]
forall (t :: * -> *) a b c.
Foldable t =>
[a -> b] -> t (b -> c) -> [a -> c]
merge (Formula a -> [DList (a, Bool)]
pos Formula a
a) (Formula a -> [DList (a, Bool)]
pos Formula a
b)
    pos (And a :: Formula a
a b :: Formula a
b) = Formula a -> [DList (a, Bool)]
pos Formula a
a [DList (a, Bool)] -> [DList (a, Bool)] -> [DList (a, Bool)]
forall a. [a] -> [a] -> [a]
++ Formula a -> [DList (a, Bool)]
pos Formula a
b
    pos (Iff a :: Formula a
a b :: Formula a
b) = Formula a -> [DList (a, Bool)]
pos (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
a Formula a
b) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
b Formula a
a))

    neg :: Formula a -> [DList (a, Bool)]
neg (Lit True) = [DList (a, Bool)
forall a. DList a
DList.empty]
    neg (Lit False) = []
    neg (Var x :: a
x) = [(a, Bool) -> DList (a, Bool)
forall a. a -> DList a
DList.singleton (a
x, Bool
False)]
    neg (Not a :: Formula a
a) = Formula a -> [DList (a, Bool)]
pos Formula a
a
    neg (Imp a :: Formula a
a b :: Formula a
b) = Formula a -> [DList (a, Bool)]
pos Formula a
a [DList (a, Bool)] -> [DList (a, Bool)] -> [DList (a, Bool)]
forall a. [a] -> [a] -> [a]
++ Formula a -> [DList (a, Bool)]
neg Formula a
b
    neg (Or a :: Formula a
a b :: Formula a
b) = Formula a -> [DList (a, Bool)]
neg Formula a
a [DList (a, Bool)] -> [DList (a, Bool)] -> [DList (a, Bool)]
forall a. [a] -> [a] -> [a]
++ Formula a -> [DList (a, Bool)]
neg Formula a
b
    neg (And a :: Formula a
a b :: Formula a
b) = [DList (a, Bool)] -> [DList (a, Bool)] -> [DList (a, Bool)]
forall (t :: * -> *) a b c.
Foldable t =>
[a -> b] -> t (b -> c) -> [a -> c]
merge (Formula a -> [DList (a, Bool)]
neg Formula a
a) (Formula a -> [DList (a, Bool)]
neg Formula a
b)
    neg (Iff a :: Formula a
a b :: Formula a
b) = Formula a -> [DList (a, Bool)]
neg (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
a Formula a
b) (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Imp Formula a
b Formula a
a))

    -- Convert from a list of difference lists of pairs to a set of sets of
    -- pairs.
    convert :: [DList (a, Bool)] -> Set (Set (a, Bool))
convert = [Set (a, Bool)] -> Set (Set (a, Bool))
forall a. Ord a => [a] -> Set a
Set.fromList ([Set (a, Bool)] -> Set (Set (a, Bool)))
-> ([DList (a, Bool)] -> [Set (a, Bool)])
-> [DList (a, Bool)]
-> Set (Set (a, Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DList (a, Bool) -> Set (a, Bool))
-> [DList (a, Bool)] -> [Set (a, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map DList (a, Bool) -> Set (a, Bool)
forall a. Ord a => DList a -> Set a
DList.toSet

    -- Remove redundant clauses from a CNF formula
    removeRedundantClauses :: Set (Set (a, Bool)) -> Set (Set (a, Bool))
removeRedundantClauses = (Set (a, Bool) -> Bool)
-> Set (Set (a, Bool)) -> Set (Set (a, Bool))
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Set (a, Bool) -> Bool
forall a. Ord a => Set (a, Bool) -> Bool
notRedundant

    -- Return whether a clause contains a literal and its negation
    notRedundant :: Set (a, Bool) -> Bool
notRedundant c :: Set (a, Bool)
c = Bool -> Bool
not (((a, Bool) -> Bool) -> Set (a, Bool) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Set (a, Bool) -> (a, Bool) -> Bool
forall a. Ord a => Set (a, Bool) -> (a, Bool) -> Bool
test Set (a, Bool)
c) Set (a, Bool)
c)

    -- Test whether a literal and its negation both occur in a clause
    test :: Set (a, Bool) -> (a, Bool) -> Bool
test c :: Set (a, Bool)
c (x :: a
x, b :: Bool
b) = (a
x, Bool -> Bool
not Bool
b) (a, Bool) -> Set (a, Bool) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (a, Bool)
c

-- | Convert a conjunctive normal form representation of a formula into a
-- formula.
toFormula :: CNF a -> Formula a
toFormula :: CNF a -> Formula a
toFormula clauses :: CNF a
clauses =
  if (Map a Bool -> Bool) -> CNF a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Map a Bool -> Bool
forall k a. Map k a -> Bool
Map.null CNF a
clauses
    then Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False
    else case CNF a -> [Map a Bool]
forall a. Set a -> [a]
Set.toList CNF a
clauses of
      [] -> Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
True
      (c :: Map a Bool
c : cs :: [Map a Bool]
cs) -> (Map a Bool -> Formula a -> Formula a)
-> Formula a -> [Map a Bool] -> Formula a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
And (Formula a -> Formula a -> Formula a)
-> (Map a Bool -> Formula a)
-> Map a Bool
-> Formula a
-> Formula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a Bool -> Formula a
forall a. Clause a -> Formula a
clauseToFormula) (Map a Bool -> Formula a
forall a. Clause a -> Formula a
clauseToFormula Map a Bool
c) [Map a Bool]
cs

clauseToFormula :: Clause a -> Formula a
clauseToFormula :: Clause a -> Formula a
clauseToFormula literals :: Clause a
literals = case Clause a -> [(a, Bool)]
forall k a. Map k a -> [(k, a)]
Map.toList Clause a
literals of
  [] -> Bool -> Formula a
forall a. Bool -> Formula a
Lit Bool
False
  (l :: (a, Bool)
l : ls :: [(a, Bool)]
ls) -> ((a, Bool) -> Formula a -> Formula a)
-> Formula a -> [(a, Bool)] -> Formula a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Formula a -> Formula a -> Formula a
forall a. Formula a -> Formula a -> Formula a
Or (Formula a -> Formula a -> Formula a)
-> ((a, Bool) -> Formula a) -> (a, Bool) -> Formula a -> Formula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Bool) -> Formula a
forall a. Literal a -> Formula a
literalToFormula) ((a, Bool) -> Formula a
forall a. Literal a -> Formula a
literalToFormula (a, Bool)
l) [(a, Bool)]
ls

literalToFormula :: Literal a -> Formula a
literalToFormula :: Literal a -> Formula a
literalToFormula (x :: a
x, False) = Formula a -> Formula a
forall a. Formula a -> Formula a
Not (a -> Formula a
forall a. a -> Formula a
Var a
x)
literalToFormula (x :: a
x, True) = a -> Formula a
forall a. a -> Formula a
Var a
x

-- | Convert a formula into a canonical conjunctive normal form.
--
-- ==== __Examples__
--
-- >>> import AutoProof.Internal.Formula
-- >>> canonicalCNF $ Or (Not (Imp (Var "a") (Var "b"))) (Var "c")
-- And (Or (Var "c") (Not (Var "b"))) (Or (Var "c") (Var "a"))
canonicalCNF :: Ord a => Formula a -> Formula a
canonicalCNF :: Formula a -> Formula a
canonicalCNF = CNF a -> Formula a
forall a. CNF a -> Formula a
toFormula (CNF a -> Formula a)
-> (Formula a -> CNF a) -> Formula a -> Formula a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula a -> CNF a
forall a. Ord a => Formula a -> CNF a
fromFormula

-- | Substitute a truth value for a variable in a CNF formula.
--
-- @('substitute' a x 'True')@ and @('substitute' a x 'False')@ represent the
-- substitutions \(a[\top/x]\) and \(a[\bot/x]\), respectively.
--
-- ==== __Examples__
--
-- >>> a = And (Imp (Var "a") (Not (And (Var "b") (Not (Var "c"))))) (Var "a")
-- >>> cnf = CNF.fromFormula a
-- >>> cnf
-- fromList [fromList [("a",False),("b",False),("c",True)],fromList [("a",True)]]
-- >>> cnf2 = CNF.substitute cnf "a" True
-- >>> cnf2
-- fromList [fromList [("b",False),("c",True)]]
-- >>> a2 = CNF.toFormula cnf2
-- >>> a2
-- Or (Var "c") (Not (Var "b"))
substitute :: Ord a => CNF a -> a -> Bool -> CNF a
substitute :: CNF a -> a -> Bool -> CNF a
substitute a :: CNF a
a x :: a
x b :: Bool
b =
  (Map a Bool -> Map a Bool) -> CNF a -> CNF a
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map
    ((a -> Bool -> Bool) -> Map a Bool -> Map a Bool
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (((a, Bool) -> Bool) -> a -> Bool -> Bool
forall a b c. ((a, b) -> c) -> a -> b -> c
curry ((a, Bool) -> (a, Bool) -> Bool
forall a. Eq a => a -> a -> Bool
/= (a
x, Bool -> Bool
not Bool
b))))
    ((Map a Bool -> Bool) -> CNF a -> CNF a
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b) (Maybe Bool -> Bool)
-> (Map a Bool -> Maybe Bool) -> Map a Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Map a Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
x) CNF a
a)

-- | Substitute a truth value for a variable that occurs as a pure literal
-- within a CNF formula with the same polarity as the truth value. This
-- precondition is /not/ checked.
substitutePure :: Ord a => CNF a -> a -> Bool -> CNF a
substitutePure :: CNF a -> a -> Bool -> CNF a
substitutePure a :: CNF a
a x :: a
x b :: Bool
b = (Map a Bool -> Bool) -> CNF a -> CNF a
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b) (Maybe Bool -> Bool)
-> (Map a Bool -> Maybe Bool) -> Map a Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Map a Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
x) CNF a
a

-- | Obtain the literal of a unitary clause of a CNF formula, if there is one.
--
-- A /unitary clause/ is one in which exactly one literal occurs.
unitLiteral :: CNF a -> Maybe (Literal a)
unitLiteral :: CNF a -> Maybe (Literal a)
unitLiteral = (Map a Bool -> Maybe (Literal a) -> Maybe (Literal a))
-> Maybe (Literal a) -> CNF a -> Maybe (Literal a)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Maybe (Literal a) -> Maybe (Literal a) -> Maybe (Literal a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Maybe (Literal a) -> Maybe (Literal a) -> Maybe (Literal a))
-> (Map a Bool -> Maybe (Literal a))
-> Map a Bool
-> Maybe (Literal a)
-> Maybe (Literal a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a Bool -> Maybe (Literal a)
forall k a. Map k a -> Maybe (k, a)
f) Maybe (Literal a)
forall a. Maybe a
Nothing
  where
    f :: Map k a -> Maybe (k, a)
f clause :: Map k a
clause = case Map k a -> [(k, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k a
clause of
      [l :: (k, a)
l] -> (k, a) -> Maybe (k, a)
forall a. a -> Maybe a
Just (k, a)
l
      _ -> Maybe (k, a)
forall a. Maybe a
Nothing

-- | Obtain a pure literal of a CNF formula, if there is one.
--
-- A /pure literal/ is one which only occurs with the a single polarity in the
-- formula.
pureLiteral :: Ord a => CNF a -> Maybe (Literal a)
pureLiteral :: CNF a -> Maybe (Literal a)
pureLiteral a :: CNF a
a = case ((a, Maybe Bool) -> Bool)
-> [(a, Maybe Bool)] -> Maybe (a, Maybe Bool)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (a, Maybe Bool) -> Bool
forall a a. (a, Maybe a) -> Bool
isPure [(a, Maybe Bool)]
variables of
  Just (x :: a
x, Just b :: Bool
b) -> Literal a -> Maybe (Literal a)
forall a. a -> Maybe a
Just (a
x, Bool
b)
  _ -> Maybe (Literal a)
forall a. Maybe a
Nothing
  where
    isPure :: (a, Maybe a) -> Bool
isPure (_, Just _) = Bool
True
    isPure _ = Bool
False

    -- Variables together with their polarities
    variables :: [(a, Maybe Bool)]
variables = (Map a Bool -> [(a, Maybe Bool)] -> [(a, Maybe Bool)])
-> [(a, Maybe Bool)] -> CNF a -> [(a, Maybe Bool)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Literal a] -> [(a, Maybe Bool)] -> [(a, Maybe Bool)]
forall a a.
(Eq a, Eq a) =>
[(a, a)] -> [(a, Maybe a)] -> [(a, Maybe a)]
findVariables ([Literal a] -> [(a, Maybe Bool)] -> [(a, Maybe Bool)])
-> (Map a Bool -> [Literal a])
-> Map a Bool
-> [(a, Maybe Bool)]
-> [(a, Maybe Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a Bool -> [Literal a]
forall k a. Map k a -> [(k, a)]
Map.toList) [] CNF a
a

    findVariables :: [(a, a)] -> [(a, Maybe a)] -> [(a, Maybe a)]
findVariables [] vs :: [(a, Maybe a)]
vs = [(a, Maybe a)]
vs
    findVariables ((x :: a
x, b :: a
b) : ls :: [(a, a)]
ls) vs :: [(a, Maybe a)]
vs = case a -> [(a, Maybe a)] -> Maybe (Maybe a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
List.lookup a
x [(a, Maybe a)]
vs of
      -- We previously encountered x with just the polarity b
      Just (Just b' :: a
b')
        -- The current polarity agrees with the previous polarity, so we keep
        -- looking
        | a
b' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b -> [(a, a)] -> [(a, Maybe a)] -> [(a, Maybe a)]
findVariables [(a, a)]
ls [(a, Maybe a)]
vs
        -- We now saw both polarities
        | Bool
otherwise -> [(a, a)] -> [(a, Maybe a)] -> [(a, Maybe a)]
findVariables [(a, a)]
ls ((a
x, Maybe a
forall a. Maybe a
Nothing) (a, Maybe a) -> [(a, Maybe a)] -> [(a, Maybe a)]
forall a. a -> DList a
: [(a, Maybe a)]
vs')
        where
          vs' :: [(a, Maybe a)]
vs' = ((a, Maybe a) -> Bool) -> [(a, Maybe a)] -> [(a, Maybe a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(y :: a
y, _) -> a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
x) [(a, Maybe a)]
vs
      -- We previously encountered both polarities of x
      Just Nothing -> [(a, a)] -> [(a, Maybe a)] -> [(a, Maybe a)]
findVariables [(a, a)]
ls [(a, Maybe a)]
vs
      -- This is the first time we see x
      Nothing -> [(a, a)] -> [(a, Maybe a)] -> [(a, Maybe a)]
findVariables [(a, a)]
ls ((a
x, a -> Maybe a
forall a. a -> Maybe a
Just a
b) (a, Maybe a) -> [(a, Maybe a)] -> [(a, Maybe a)]
forall a. a -> DList a
: [(a, Maybe a)]
vs)

-- | Obtain a literal from a CNF formula, if there is one.
getAnyLiteral :: CNF a -> Maybe (Literal a)
getAnyLiteral :: CNF a -> Maybe (Literal a)
getAnyLiteral = [Map a Bool] -> Maybe (Literal a)
forall k a. [Map k a] -> Maybe (k, a)
f ([Map a Bool] -> Maybe (Literal a))
-> (CNF a -> [Map a Bool]) -> CNF a -> Maybe (Literal a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CNF a -> [Map a Bool]
forall a. Set a -> [a]
Set.toList
  where
    f :: [Map k a] -> Maybe (k, a)
f [] = Maybe (k, a)
forall a. Maybe a
Nothing
    f (c :: Map k a
c : cs :: [Map k a]
cs) = case Map k a -> [(k, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k a
c of
      [] -> [Map k a] -> Maybe (k, a)
f [Map k a]
cs
      l :: (k, a)
l : _ -> (k, a) -> Maybe (k, a)
forall a. a -> Maybe a
Just (k, a)
l