    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Case trees.
    --
    --   After coverage checking, pattern matching is translated
    --   to case trees, i.e., a tree of successive case splits
    --   on one variable at a time.

    module Agda.TypeChecking.CompiledClause where

    import Prelude hiding (null)

    import Control.DeepSeq

    import qualified Data.Map as Map
    import Data.Map (Map)
    import Data.Semigroup hiding (Arg(..))

    import GHC.Generics (Generic)

    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.Syntax.Internal.Generic
    import Agda.Syntax.Literal
    import Agda.Syntax.Position

    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty

    import Agda.Utils.Impossible

    data WithArity c = WithArity { forall c. WithArity c -> Int
    arity :: Int, forall c. WithArity c -> c
    content :: c }
      deriving ((forall a b. (a -> b) -> WithArity a -> WithArity b)
    -> (forall a b. a -> WithArity b -> WithArity a)
    -> Functor WithArity
    forall a b. a -> WithArity b -> WithArity a
    forall a b. (a -> b) -> WithArity a -> WithArity b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> WithArity a -> WithArity b
    fmap :: forall a b. (a -> b) -> WithArity a -> WithArity b
    $c<$ :: forall a b. a -> WithArity b -> WithArity a
    <$ :: forall a b. a -> WithArity b -> WithArity a
    Functor, (forall m. Monoid m => WithArity m -> m)
    -> (forall m a. Monoid m => (a -> m) -> WithArity a -> m)
    -> (forall m a. Monoid m => (a -> m) -> WithArity a -> m)
    -> (forall a b. (a -> b -> b) -> b -> WithArity a -> b)
    -> (forall a b. (a -> b -> b) -> b -> WithArity a -> b)
    -> (forall b a. (b -> a -> b) -> b -> WithArity a -> b)
    -> (forall b a. (b -> a -> b) -> b -> WithArity a -> b)
    -> (forall a. (a -> a -> a) -> WithArity a -> a)
    -> (forall a. (a -> a -> a) -> WithArity a -> a)
    -> (forall a. WithArity a -> [a])
    -> (forall a. WithArity a -> Bool)
    -> (forall c. WithArity c -> Int)
    -> (forall a. Eq a => a -> WithArity a -> Bool)
    -> (forall a. Ord a => WithArity a -> a)
    -> (forall a. Ord a => WithArity a -> a)
    -> (forall a. Num a => WithArity a -> a)
    -> (forall a. Num a => WithArity a -> a)
    -> Foldable WithArity
    forall a. Eq a => a -> WithArity a -> Bool
    forall a. Num a => WithArity a -> a
    forall a. Ord a => WithArity a -> a
    forall m. Monoid m => WithArity m -> m
    forall a. WithArity a -> Bool
    forall c. WithArity c -> Int
    forall a. WithArity a -> [a]
    forall a. (a -> a -> a) -> WithArity a -> a
    forall m a. Monoid m => (a -> m) -> WithArity a -> m
    forall b a. (b -> a -> b) -> b -> WithArity a -> b
    forall a b. (a -> b -> b) -> b -> WithArity a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => WithArity m -> m
    fold :: forall m. Monoid m => WithArity m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> WithArity a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> WithArity a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> WithArity a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> WithArity a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> WithArity a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> WithArity a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> WithArity a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> WithArity a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> WithArity a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> WithArity a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> WithArity a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> WithArity a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> WithArity a -> a
    foldr1 :: forall a. (a -> a -> a) -> WithArity a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> WithArity a -> a
    foldl1 :: forall a. (a -> a -> a) -> WithArity a -> a
    $ctoList :: forall a. WithArity a -> [a]
    toList :: forall a. WithArity a -> [a]
    $cnull :: forall a. WithArity a -> Bool
    null :: forall a. WithArity a -> Bool
    $clength :: forall c. WithArity c -> Int
    length :: forall c. WithArity c -> Int
    $celem :: forall a. Eq a => a -> WithArity a -> Bool
    elem :: forall a. Eq a => a -> WithArity a -> Bool
    $cmaximum :: forall a. Ord a => WithArity a -> a
    maximum :: forall a. Ord a => WithArity a -> a
    $cminimum :: forall a. Ord a => WithArity a -> a
    minimum :: forall a. Ord a => WithArity a -> a
    $csum :: forall a. Num a => WithArity a -> a
    sum :: forall a. Num a => WithArity a -> a
    $cproduct :: forall a. Num a => WithArity a -> a
    product :: forall a. Num a => WithArity a -> a
    Foldable, Functor WithArity
    Foldable WithArity
    (Functor WithArity, Foldable WithArity) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> WithArity a -> f (WithArity b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        WithArity (f a) -> f (WithArity a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> WithArity a -> m (WithArity b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        WithArity (m a) -> m (WithArity a))
    -> Traversable WithArity
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    WithArity (m a) -> m (WithArity a)
    forall (f :: * -> *) a.
    Applicative f =>
    WithArity (f a) -> f (WithArity a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> WithArity a -> m (WithArity b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> WithArity a -> f (WithArity b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> WithArity a -> f (WithArity b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> WithArity a -> f (WithArity b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    WithArity (f a) -> f (WithArity a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    WithArity (f a) -> f (WithArity a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> WithArity a -> m (WithArity b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> WithArity a -> m (WithArity b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    WithArity (m a) -> m (WithArity a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    WithArity (m a) -> m (WithArity a)
    Traversable, Int -> WithArity c -> ShowS
    [WithArity c] -> ShowS
    WithArity c -> String
    (Int -> WithArity c -> ShowS)
    -> (WithArity c -> String)
    -> ([WithArity c] -> ShowS)
    -> Show (WithArity c)
    forall c. Show c => Int -> WithArity c -> ShowS
    forall c. Show c => [WithArity c] -> ShowS
    forall c. Show c => WithArity c -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall c. Show c => Int -> WithArity c -> ShowS
    showsPrec :: Int -> WithArity c -> ShowS
    $cshow :: forall c. Show c => WithArity c -> String
    show :: WithArity c -> String
    $cshowList :: forall c. Show c => [WithArity c] -> ShowS
    showList :: [WithArity c] -> ShowS
    Show, (forall x. WithArity c -> Rep (WithArity c) x)
    -> (forall x. Rep (WithArity c) x -> WithArity c)
    -> Generic (WithArity c)
    forall x. Rep (WithArity c) x -> WithArity c
    forall x. WithArity c -> Rep (WithArity c) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall c x. Rep (WithArity c) x -> WithArity c
    forall c x. WithArity c -> Rep (WithArity c) x
    $cfrom :: forall c x. WithArity c -> Rep (WithArity c) x
    from :: forall x. WithArity c -> Rep (WithArity c) x
    $cto :: forall c x. Rep (WithArity c) x -> WithArity c
    to :: forall x. Rep (WithArity c) x -> WithArity c
    Generic)

    -- | Branches in a case tree.

    data Case c = Branches
      { forall c. Case c -> Bool
    projPatterns   :: Bool
        -- ^ We are constructing a record here (copatterns).
        --   'conBranches' lists projections.
      , forall c. Case c -> Map QName (WithArity c)
    conBranches    :: Map QName (WithArity c)
        -- ^ Map from constructor (or projection) names to their arity
        --   and the case subtree.  (Projections have arity 0.)
      , forall c. Case c -> Maybe (ConHead, WithArity c)
    etaBranch      :: Maybe (ConHead, WithArity c)
        -- ^ Eta-expand with the given (eta record) constructor. If this is
        --   present, there should not be any conBranches or litBranches.
      , forall c. Case c -> Map Literal c
    litBranches    :: Map Literal c
        -- ^ Map from literal to case subtree.
      , forall c. Case c -> Maybe c
    catchallBranch :: Maybe c
        -- ^ (Possibly additional) catch-all clause.
      , forall c. Case c -> Maybe Bool
    fallThrough :: Maybe Bool
        -- ^ (if True) In case of non-canonical argument use catchallBranch.
      , forall c. Case c -> Bool
    lazyMatch :: Bool
        -- ^ Lazy pattern match. Requires single (non-copattern) branch with no lit
        --   branches and no catch-all.
      }
      deriving ((forall a b. (a -> b) -> Case a -> Case b)
    -> (forall a b. a -> Case b -> Case a) -> Functor Case
    forall a b. a -> Case b -> Case a
    forall a b. (a -> b) -> Case a -> Case b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Case a -> Case b
    fmap :: forall a b. (a -> b) -> Case a -> Case b
    $c<$ :: forall a b. a -> Case b -> Case a
    <$ :: forall a b. a -> Case b -> Case a
    Functor, (forall m. Monoid m => Case m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Case a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Case a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Case a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Case a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Case a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Case a -> b)
    -> (forall a. (a -> a -> a) -> Case a -> a)
    -> (forall a. (a -> a -> a) -> Case a -> a)
    -> (forall a. Case a -> [a])
    -> (forall c. Case c -> Bool)
    -> (forall a. Case a -> Int)
    -> (forall a. Eq a => a -> Case a -> Bool)
    -> (forall a. Ord a => Case a -> a)
    -> (forall a. Ord a => Case a -> a)
    -> (forall a. Num a => Case a -> a)
    -> (forall a. Num a => Case a -> a)
    -> Foldable Case
    forall a. Eq a => a -> Case a -> Bool
    forall a. Num a => Case a -> a
    forall a. Ord a => Case a -> a
    forall m. Monoid m => Case m -> m
    forall c. Case c -> Bool
    forall a. Case a -> Int
    forall a. Case a -> [a]
    forall a. (a -> a -> a) -> Case a -> a
    forall m a. Monoid m => (a -> m) -> Case a -> m
    forall b a. (b -> a -> b) -> b -> Case a -> b
    forall a b. (a -> b -> b) -> b -> Case a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => Case m -> m
    fold :: forall m. Monoid m => Case m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Case a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Case a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Case a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Case a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Case a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Case a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Case a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Case a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Case a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Case a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Case a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Case a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Case a -> a
    foldr1 :: forall a. (a -> a -> a) -> Case a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Case a -> a
    foldl1 :: forall a. (a -> a -> a) -> Case a -> a
    $ctoList :: forall a. Case a -> [a]
    toList :: forall a. Case a -> [a]
    $cnull :: forall c. Case c -> Bool
    null :: forall c. Case c -> Bool
    $clength :: forall a. Case a -> Int
    length :: forall a. Case a -> Int
    $celem :: forall a. Eq a => a -> Case a -> Bool
    elem :: forall a. Eq a => a -> Case a -> Bool
    $cmaximum :: forall a. Ord a => Case a -> a
    maximum :: forall a. Ord a => Case a -> a
    $cminimum :: forall a. Ord a => Case a -> a
    minimum :: forall a. Ord a => Case a -> a
    $csum :: forall a. Num a => Case a -> a
    sum :: forall a. Num a => Case a -> a
    $cproduct :: forall a. Num a => Case a -> a
    product :: forall a. Num a => Case a -> a
    Foldable, Functor Case
    Foldable Case
    (Functor Case, Foldable Case) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Case a -> f (Case b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Case (f a) -> f (Case a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Case a -> m (Case b))
    -> (forall (m :: * -> *) a. Monad m => Case (m a) -> m (Case a))
    -> Traversable Case
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => Case (m a) -> m (Case a)
    forall (f :: * -> *) a. Applicative f => Case (f a) -> f (Case a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Case a -> m (Case b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Case a -> f (Case b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Case a -> f (Case b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Case a -> f (Case b)
    $csequenceA :: forall (f :: * -> *) a. Applicative f => Case (f a) -> f (Case a)
    sequenceA :: forall (f :: * -> *) a. Applicative f => Case (f a) -> f (Case a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Case a -> m (Case b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Case a -> m (Case b)
    $csequence :: forall (m :: * -> *) a. Monad m => Case (m a) -> m (Case a)
    sequence :: forall (m :: * -> *) a. Monad m => Case (m a) -> m (Case a)
    Traversable, Int -> Case c -> ShowS
    [Case c] -> ShowS
    Case c -> String
    (Int -> Case c -> ShowS)
    -> (Case c -> String) -> ([Case c] -> ShowS) -> Show (Case c)
    forall c. Show c => Int -> Case c -> ShowS
    forall c. Show c => [Case c] -> ShowS
    forall c. Show c => Case c -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall c. Show c => Int -> Case c -> ShowS
    showsPrec :: Int -> Case c -> ShowS
    $cshow :: forall c. Show c => Case c -> String
    show :: Case c -> String
    $cshowList :: forall c. Show c => [Case c] -> ShowS
    showList :: [Case c] -> ShowS
    Show, (forall x. Case c -> Rep (Case c) x)
    -> (forall x. Rep (Case c) x -> Case c) -> Generic (Case c)
    forall x. Rep (Case c) x -> Case c
    forall x. Case c -> Rep (Case c) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall c x. Rep (Case c) x -> Case c
    forall c x. Case c -> Rep (Case c) x
    $cfrom :: forall c x. Case c -> Rep (Case c) x
    from :: forall x. Case c -> Rep (Case c) x
    $cto :: forall c x. Rep (Case c) x -> Case c
    to :: forall x. Rep (Case c) x -> Case c
    Generic)

    -- | Case tree with bodies.

    data CompiledClauses' a
      = Case (Arg Int) (Case (CompiledClauses' a))
        -- ^ @Case n bs@ stands for a match on the @n@-th argument
        -- (counting from zero) with @bs@ as the case branches.
        -- If the @n@-th argument is a projection, we have only 'conBranches'
        -- with arity 0.
      | Done [Arg ArgName] a
        -- ^ @Done xs b@ stands for the body @b@ where the @xs@ contains hiding
        --   and name suggestions for the free variables. This is needed to build
        --   lambdas on the right hand side for partial applications which can
        --   still reduce.
      | Fail [Arg ArgName]
        -- ^ Absurd case. Add the free variables here as well so we can build correct
        --   number of lambdas for strict backends. (#4280)
      deriving ((forall a b. (a -> b) -> CompiledClauses' a -> CompiledClauses' b)
    -> (forall a b. a -> CompiledClauses' b -> CompiledClauses' a)
    -> Functor CompiledClauses'
    forall a b. a -> CompiledClauses' b -> CompiledClauses' a
    forall a b. (a -> b) -> CompiledClauses' a -> CompiledClauses' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> CompiledClauses' a -> CompiledClauses' b
    fmap :: forall a b. (a -> b) -> CompiledClauses' a -> CompiledClauses' b
    $c<$ :: forall a b. a -> CompiledClauses' b -> CompiledClauses' a
    <$ :: forall a b. a -> CompiledClauses' b -> CompiledClauses' a
    Functor, Functor CompiledClauses'
    Foldable CompiledClauses'
    (Functor CompiledClauses', Foldable CompiledClauses') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        CompiledClauses' (f a) -> f (CompiledClauses' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> CompiledClauses' a -> m (CompiledClauses' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        CompiledClauses' (m a) -> m (CompiledClauses' a))
    -> Traversable CompiledClauses'
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    CompiledClauses' (m a) -> m (CompiledClauses' a)
    forall (f :: * -> *) a.
    Applicative f =>
    CompiledClauses' (f a) -> f (CompiledClauses' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> CompiledClauses' a -> m (CompiledClauses' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    CompiledClauses' (f a) -> f (CompiledClauses' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    CompiledClauses' (f a) -> f (CompiledClauses' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> CompiledClauses' a -> m (CompiledClauses' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> CompiledClauses' a -> m (CompiledClauses' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    CompiledClauses' (m a) -> m (CompiledClauses' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    CompiledClauses' (m a) -> m (CompiledClauses' a)
    Traversable, (forall m. Monoid m => CompiledClauses' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> CompiledClauses' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> CompiledClauses' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> CompiledClauses' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> CompiledClauses' a -> b)
    -> (forall a. (a -> a -> a) -> CompiledClauses' a -> a)
    -> (forall a. (a -> a -> a) -> CompiledClauses' a -> a)
    -> (forall a. CompiledClauses' a -> [a])
    -> (forall a. CompiledClauses' a -> Bool)
    -> (forall a. CompiledClauses' a -> Int)
    -> (forall a. Eq a => a -> CompiledClauses' a -> Bool)
    -> (forall a. Ord a => CompiledClauses' a -> a)
    -> (forall a. Ord a => CompiledClauses' a -> a)
    -> (forall a. Num a => CompiledClauses' a -> a)
    -> (forall a. Num a => CompiledClauses' a -> a)
    -> Foldable CompiledClauses'
    forall a. Eq a => a -> CompiledClauses' a -> Bool
    forall a. Num a => CompiledClauses' a -> a
    forall a. Ord a => CompiledClauses' a -> a
    forall m. Monoid m => CompiledClauses' m -> m
    forall a. CompiledClauses' a -> Bool
    forall a. CompiledClauses' a -> Int
    forall a. CompiledClauses' a -> [a]
    forall a. (a -> a -> a) -> CompiledClauses' a -> a
    forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m
    forall b a. (b -> a -> b) -> b -> CompiledClauses' a -> b
    forall a b. (a -> b -> b) -> b -> CompiledClauses' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => CompiledClauses' m -> m
    fold :: forall m. Monoid m => CompiledClauses' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> CompiledClauses' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> CompiledClauses' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> CompiledClauses' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> CompiledClauses' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> CompiledClauses' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> CompiledClauses' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> CompiledClauses' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> CompiledClauses' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> CompiledClauses' a -> a
    foldr1 :: forall a. (a -> a -> a) -> CompiledClauses' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> CompiledClauses' a -> a
    foldl1 :: forall a. (a -> a -> a) -> CompiledClauses' a -> a
    $ctoList :: forall a. CompiledClauses' a -> [a]
    toList :: forall a. CompiledClauses' a -> [a]
    $cnull :: forall a. CompiledClauses' a -> Bool
    null :: forall a. CompiledClauses' a -> Bool
    $clength :: forall a. CompiledClauses' a -> Int
    length :: forall a. CompiledClauses' a -> Int
    $celem :: forall a. Eq a => a -> CompiledClauses' a -> Bool
    elem :: forall a. Eq a => a -> CompiledClauses' a -> Bool
    $cmaximum :: forall a. Ord a => CompiledClauses' a -> a
    maximum :: forall a. Ord a => CompiledClauses' a -> a
    $cminimum :: forall a. Ord a => CompiledClauses' a -> a
    minimum :: forall a. Ord a => CompiledClauses' a -> a
    $csum :: forall a. Num a => CompiledClauses' a -> a
    sum :: forall a. Num a => CompiledClauses' a -> a
    $cproduct :: forall a. Num a => CompiledClauses' a -> a
    product :: forall a. Num a => CompiledClauses' a -> a
    Foldable, Int -> CompiledClauses' a -> ShowS
    [CompiledClauses' a] -> ShowS
    CompiledClauses' a -> String
    (Int -> CompiledClauses' a -> ShowS)
    -> (CompiledClauses' a -> String)
    -> ([CompiledClauses' a] -> ShowS)
    -> Show (CompiledClauses' a)
    forall a. Show a => Int -> CompiledClauses' a -> ShowS
    forall a. Show a => [CompiledClauses' a] -> ShowS
    forall a. Show a => CompiledClauses' a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> CompiledClauses' a -> ShowS
    showsPrec :: Int -> CompiledClauses' a -> ShowS
    $cshow :: forall a. Show a => CompiledClauses' a -> String
    show :: CompiledClauses' a -> String
    $cshowList :: forall a. Show a => [CompiledClauses' a] -> ShowS
    showList :: [CompiledClauses' a] -> ShowS
    Show, (forall x. CompiledClauses' a -> Rep (CompiledClauses' a) x)
    -> (forall x. Rep (CompiledClauses' a) x -> CompiledClauses' a)
    -> Generic (CompiledClauses' a)
    forall x. Rep (CompiledClauses' a) x -> CompiledClauses' a
    forall x. CompiledClauses' a -> Rep (CompiledClauses' a) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall a x. Rep (CompiledClauses' a) x -> CompiledClauses' a
    forall a x. CompiledClauses' a -> Rep (CompiledClauses' a) x
    $cfrom :: forall a x. CompiledClauses' a -> Rep (CompiledClauses' a) x
    from :: forall x. CompiledClauses' a -> Rep (CompiledClauses' a) x
    $cto :: forall a x. Rep (CompiledClauses' a) x -> CompiledClauses' a
    to :: forall x. Rep (CompiledClauses' a) x -> CompiledClauses' a
    Generic)

    type CompiledClauses = CompiledClauses' Term

    litCase :: Literal -> c -> Case c
    litCase :: forall c. Literal -> c -> Case c
    litCase Literal
    l c
    x = Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    False Map QName (WithArity c)
    forall k a. Map k a
    Map.empty Maybe (ConHead, WithArity c)
    forall a. Maybe a
    Nothing (Literal -> c -> Map Literal c
    forall k a. k -> a -> Map k a
    Map.singleton Literal
    l c
    x) Maybe c
    forall a. Maybe a
    Nothing (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False) Bool
    False

    conCase :: QName -> Bool -> WithArity c -> Case c
    conCase :: forall c. QName -> Bool -> WithArity c -> Case c
    conCase QName
    c Bool
    b WithArity c
    x = Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    False (QName -> WithArity c -> Map QName (WithArity c)
    forall k a. k -> a -> Map k a
    Map.singleton QName
    c WithArity c
    x) Maybe (ConHead, WithArity c)
    forall a. Maybe a
    Nothing Map Literal c
    forall k a. Map k a
    Map.empty Maybe c
    forall a. Maybe a
    Nothing (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    b) Bool
    False

    etaCase :: ConHead -> WithArity c -> Case c
    etaCase :: forall c. ConHead -> WithArity c -> Case c
    etaCase ConHead
    c WithArity c
    x = Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    False Map QName (WithArity c)
    forall k a. Map k a
    Map.empty ((ConHead, WithArity c) -> Maybe (ConHead, WithArity c)
    forall a. a -> Maybe a
    Just (ConHead
    c, WithArity c
    x)) Map Literal c
    forall k a. Map k a
    Map.empty Maybe c
    forall a. Maybe a
    Nothing (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False) Bool
    True

    projCase :: QName -> c -> Case c
    projCase :: forall c. QName -> c -> Case c
    projCase QName
    c c
    x = Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    True (QName -> WithArity c -> Map QName (WithArity c)
    forall k a. k -> a -> Map k a
    Map.singleton QName
    c (WithArity c -> Map QName (WithArity c))
    -> WithArity c -> Map QName (WithArity c)
    forall a b. (a -> b) -> a -> b
    $ Int -> c -> WithArity c
    forall c. Int -> c -> WithArity c
    WithArity Int
    0 c
    x) Maybe (ConHead, WithArity c)
    forall a. Maybe a
    Nothing Map Literal c
    forall k a. Map k a
    Map.empty Maybe c
    forall a. Maybe a
    Nothing (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    False) Bool
    False

    catchall :: c -> Case c
    catchall :: forall c. c -> Case c
    catchall c
    x = Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    False Map QName (WithArity c)
    forall k a. Map k a
    Map.empty Maybe (ConHead, WithArity c)
    forall a. Maybe a
    Nothing Map Literal c
    forall k a. Map k a
    Map.empty (c -> Maybe c
    forall a. a -> Maybe a
    Just c
    x) (Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    True) Bool
    False

    -- | Check that the requirements on lazy matching (single inductive case) are
    --   met, and set lazy to False otherwise.
    checkLazyMatch :: Case c -> Case c
    checkLazyMatch :: forall c. Case c -> Case c
    checkLazyMatch Case c
    b = Case c
    b { lazyMatch = lazyMatch b && requirements }
      where
        requirements :: Bool
    requirements = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and
          [ Maybe c -> Bool
    forall a. Null a => a -> Bool
    null (Case c -> Maybe c
    forall c. Case c -> Maybe c
    catchallBranch Case c
    b)
          , Map QName (WithArity c) -> Int
    forall k a. Map k a -> Int
    Map.size (Case c -> Map QName (WithArity c)
    forall c. Case c -> Map QName (WithArity c)
    conBranches Case c
    b) Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    1
          , Map Literal c -> Bool
    forall a. Null a => a -> Bool
    null (Case c -> Map Literal c
    forall c. Case c -> Map Literal c
    litBranches Case c
    b)
          , Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Case c -> Bool
    forall c. Case c -> Bool
    projPatterns Case c
    b ]

    -- | Check whether a case tree has a catch-all clause.
    hasCatchall :: CompiledClauses -> Bool
    hasCatchall :: CompiledClauses -> Bool
    hasCatchall = Any -> Bool
    getAny (Any -> Bool)
    -> (CompiledClauses -> Any) -> CompiledClauses -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CompiledClauses -> Any
    forall {a}. CompiledClauses' a -> Any
    loop
      where
      loop :: CompiledClauses' a -> Any
    loop CompiledClauses' a
    cc = case CompiledClauses' a
    cc of
        Fail{}    -> Any
    forall a. Monoid a => a
    mempty
        Done{}    -> Any
    forall a. Monoid a => a
    mempty
        Case Arg Int
    _ Case (CompiledClauses' a)
    br -> Any
    -> (CompiledClauses' a -> Any) -> Maybe (CompiledClauses' a) -> Any
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe ((CompiledClauses' a -> Any) -> Case (CompiledClauses' a) -> Any
    forall m a. Monoid m => (a -> m) -> Case a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap CompiledClauses' a -> Any
    loop Case (CompiledClauses' a)
    br) (Any -> CompiledClauses' a -> Any
    forall a b. a -> b -> a
    const (Any -> CompiledClauses' a -> Any)
    -> Any -> CompiledClauses' a -> Any
    forall a b. (a -> b) -> a -> b
    $ Bool -> Any
    Any Bool
    True) (Maybe (CompiledClauses' a) -> Any)
    -> Maybe (CompiledClauses' a) -> Any
    forall a b. (a -> b) -> a -> b
    $ Case (CompiledClauses' a) -> Maybe (CompiledClauses' a)
    forall c. Case c -> Maybe c
    catchallBranch Case (CompiledClauses' a)
    br

    -- | Check whether a case tree has any projection patterns
    hasProjectionPatterns :: CompiledClauses -> Bool
    hasProjectionPatterns :: CompiledClauses -> Bool
    hasProjectionPatterns = Any -> Bool
    getAny (Any -> Bool)
    -> (CompiledClauses -> Any) -> CompiledClauses -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CompiledClauses -> Any
    forall {a}. CompiledClauses' a -> Any
    loop
      where
      loop :: CompiledClauses' a -> Any
    loop CompiledClauses' a
    cc = case CompiledClauses' a
    cc of
        Fail{}    -> Any
    forall a. Monoid a => a
    mempty
        Done{}    -> Any
    forall a. Monoid a => a
    mempty
        Case Arg Int
    _ Case (CompiledClauses' a)
    br -> Bool -> Any
    Any (Case (CompiledClauses' a) -> Bool
    forall c. Case c -> Bool
    projPatterns Case (CompiledClauses' a)
    br) Any -> Any -> Any
    forall a. Semigroup a => a -> a -> a
    <> (CompiledClauses' a -> Any) -> Case (CompiledClauses' a) -> Any
    forall m a. Monoid m => (a -> m) -> Case a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap CompiledClauses' a -> Any
    loop Case (CompiledClauses' a)
    br

    instance Semigroup c => Semigroup (WithArity c) where
      WithArity Int
    n1 c
    c1 <> :: WithArity c -> WithArity c -> WithArity c
    <> WithArity Int
    n2 c
    c2
        | Int
    n1 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n2  = Int -> c -> WithArity c
    forall c. Int -> c -> WithArity c
    WithArity Int
    n1 (c
    c1 c -> c -> c
    forall a. Semigroup a => a -> a -> a
    <> c
    c2)
        | Bool
    otherwise = WithArity c
    forall a. HasCallStack => a
    __IMPOSSIBLE__   -- arity must match!

    instance (Semigroup c, Monoid c) => Monoid (WithArity c) where
      mempty :: WithArity c
    mempty  = Int -> c -> WithArity c
    forall c. Int -> c -> WithArity c
    WithArity Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__ c
    forall a. Monoid a => a
    mempty
      mappend :: WithArity c -> WithArity c -> WithArity c
    mappend = WithArity c -> WithArity c -> WithArity c
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance Semigroup m => Semigroup (Case m) where
      Branches Bool
    cop Map QName (WithArity m)
    cs Maybe (ConHead, WithArity m)
    eta Map Literal m
    ls Maybe m
    m Maybe Bool
    b Bool
    lazy <> :: Case m -> Case m -> Case m
    <> Branches Bool
    cop' Map QName (WithArity m)
    cs' Maybe (ConHead, WithArity m)
    eta' Map Literal m
    ls' Maybe m
    m' Maybe Bool
    b' Bool
    lazy' = Case m -> Case m
    forall c. Case c -> Case c
    checkLazyMatch (Case m -> Case m) -> Case m -> Case m
    forall a b. (a -> b) -> a -> b
    $
        Bool
    -> Map QName (WithArity m)
    -> Maybe (ConHead, WithArity m)
    -> Map Literal m
    -> Maybe m
    -> Maybe Bool
    -> Bool
    -> Case m
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches (Bool
    cop Bool -> Bool -> Bool
    || Bool
    cop') -- for @projCase <> mempty@
                 ((WithArity m -> WithArity m -> WithArity m)
    -> Map QName (WithArity m)
    -> Map QName (WithArity m)
    -> Map QName (WithArity m)
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith WithArity m -> WithArity m -> WithArity m
    forall a. Semigroup a => a -> a -> a
    (<>) Map QName (WithArity m)
    cs Map QName (WithArity m)
    cs')
                 (Maybe (ConHead, WithArity m)
    -> Maybe (ConHead, WithArity m) -> Maybe (ConHead, WithArity m)
    forall {a}. Maybe a -> Maybe a -> Maybe a
    unionEta Maybe (ConHead, WithArity m)
    eta Maybe (ConHead, WithArity m)
    eta')
                 ((m -> m -> m) -> Map Literal m -> Map Literal m -> Map Literal m
    forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
    Map.unionWith m -> m -> m
    forall a. Semigroup a => a -> a -> a
    (<>) Map Literal m
    ls Map Literal m
    ls')
                 (Maybe m
    m Maybe m -> Maybe m -> Maybe m
    forall a. Semigroup a => a -> a -> a
    <> Maybe m
    m')
                 (Maybe Bool -> Maybe Bool -> Maybe Bool
    combine Maybe Bool
    b Maybe Bool
    b')
                 (Bool
    lazy Bool -> Bool -> Bool
    && Bool
    lazy')
       where
         combine :: Maybe Bool -> Maybe Bool -> Maybe Bool
    combine Maybe Bool
    Nothing  Maybe Bool
    b'        = Maybe Bool
    b
         combine Maybe Bool
    b        Maybe Bool
    Nothing   = Maybe Bool
    b
         combine (Just Bool
    b) (Just Bool
    b') = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
    forall a b. (a -> b) -> a -> b
    $ Bool
    b Bool -> Bool -> Bool
    && Bool
    b'

         unionEta :: Maybe a -> Maybe a -> Maybe a
    unionEta Maybe a
    Nothing Maybe a
    b = Maybe a
    b
         unionEta Maybe a
    b Maybe a
    Nothing = Maybe a
    b
         unionEta Just{} Just{} = Maybe a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance (Semigroup m, Monoid m) => Monoid (Case m) where
      mempty :: Case m
    mempty  = Case m
    forall a. Null a => a
    empty
      mappend :: Case m -> Case m -> Case m
    mappend = Case m -> Case m -> Case m
    forall a. Semigroup a => a -> a -> a
    (<>)

    instance Null (Case m) where
      empty :: Case m
    empty = Bool
    -> Map QName (WithArity m)
    -> Maybe (ConHead, WithArity m)
    -> Map Literal m
    -> Maybe m
    -> Maybe Bool
    -> Bool
    -> Case m
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    False Map QName (WithArity m)
    forall k a. Map k a
    Map.empty Maybe (ConHead, WithArity m)
    forall a. Maybe a
    Nothing Map Literal m
    forall k a. Map k a
    Map.empty Maybe m
    forall a. Maybe a
    Nothing Maybe Bool
    forall a. Maybe a
    Nothing Bool
    True
      null :: Case m -> Bool
    null (Branches Bool
    _cop Map QName (WithArity m)
    cs Maybe (ConHead, WithArity m)
    eta Map Literal m
    ls Maybe m
    mcatch Maybe Bool
    _b Bool
    _lazy) = Map QName (WithArity m) -> Bool
    forall a. Null a => a -> Bool
    null Map QName (WithArity m)
    cs Bool -> Bool -> Bool
    && Maybe (ConHead, WithArity m) -> Bool
    forall a. Null a => a -> Bool
    null Maybe (ConHead, WithArity m)
    eta Bool -> Bool -> Bool
    && Map Literal m -> Bool
    forall a. Null a => a -> Bool
    null Map Literal m
    ls Bool -> Bool -> Bool
    && Maybe m -> Bool
    forall a. Null a => a -> Bool
    null Maybe m
    mcatch

    -- * Pretty instances.

    instance Pretty a => Pretty (WithArity a) where
      pretty :: WithArity a -> Doc
    pretty = a -> Doc
    forall a. Pretty a => a -> Doc
    pretty (a -> Doc) -> (WithArity a -> a) -> WithArity a -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . WithArity a -> a
    forall c. WithArity c -> c
    content

    instance Pretty a => Pretty (Case a) where
      prettyPrec :: Int -> Case a -> Doc
    prettyPrec Int
    p (Branches Bool
    _cop Map QName (WithArity a)
    cs Maybe (ConHead, WithArity a)
    eta Map Literal a
    ls Maybe a
    m Maybe Bool
    b Bool
    lazy) =
        Bool -> Doc -> Doc
    mparens (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Bool -> Doc
    forall {a}. (IsString a, Null a) => Bool -> a
    prLazy Bool
    lazy Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    vcat (Map QName (WithArity a) -> [Doc]
    forall k v. (Pretty k, Pretty v) => Map k v -> [Doc]
    prettyMap_ Map QName (WithArity a)
    cs [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Maybe (ConHead, WithArity a) -> [Doc]
    forall {a} {a}. (Pretty a, Pretty a) => Maybe (a, a) -> [Doc]
    prEta Maybe (ConHead, WithArity a)
    eta [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Map Literal a -> [Doc]
    forall k v. (Pretty k, Pretty v) => Map k v -> [Doc]
    prettyMap_ Map Literal a
    ls [Doc] -> [Doc] -> [Doc]
    forall a. [a] -> [a] -> [a]
    ++ Maybe a -> [Doc]
    forall {a}. Pretty a => Maybe a -> [Doc]
    prC Maybe a
    m)
        where
          prLazy :: Bool -> a
    prLazy Bool
    True  = a
    "~"
          prLazy Bool
    False = a
    forall a. Null a => a
    empty
          prC :: Maybe a -> [Doc]
    prC Maybe a
    Nothing = []
          prC (Just a
    x) = [Doc
    "_ ->" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    x]
          prEta :: Maybe (a, a) -> [Doc]
    prEta Maybe (a, a)
    Nothing = []
          prEta (Just (a
    c, a
    cc)) = [(Doc
    "eta" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    c Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    "->") Doc -> Doc -> Doc
    <?> a -> Doc
    forall a. Pretty a => a -> Doc
    pretty a
    cc]

    prettyMap_ :: (Pretty k, Pretty v) => Map k v -> [Doc]
    prettyMap_ :: forall k v. (Pretty k, Pretty v) => Map k v -> [Doc]
    prettyMap_ = ((k, v) -> Doc) -> [(k, v)] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (k, v) -> Doc
    forall k v. (Pretty k, Pretty v) => (k, v) -> Doc
    prettyAssign ([(k, v)] -> [Doc]) -> (Map k v -> [(k, v)]) -> Map k v -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map k v -> [(k, v)]
    forall k a. Map k a -> [(k, a)]
    Map.toList

    instance Pretty CompiledClauses where
      pretty :: CompiledClauses -> Doc
    pretty (Done [Arg String]
    hs Term
    t) = (Doc
    "done" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> [Arg String] -> Doc
    forall a. Pretty a => a -> Doc
    pretty [Arg String]
    hs) Doc -> Doc -> Doc
    <?> Term -> Doc
    forall a. Pretty a => a -> Doc
    pretty Term
    t
      pretty Fail{}      = Doc
    "fail"
      pretty (Case Arg Int
    n Case CompiledClauses
    bs) | Case CompiledClauses -> Bool
    forall c. Case c -> Bool
    projPatterns Case CompiledClauses
    bs =
        [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    sep [ Doc
    "record"
            , Int -> Doc -> Doc
    forall a. Int -> Doc a -> Doc a
    nest Int
    2 (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Case CompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    pretty Case CompiledClauses
    bs
            ]
      pretty (Case Arg Int
    n Case CompiledClauses
    bs) =
        String -> Doc
    forall a. String -> Doc a
    text (String
    "case " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Arg Int -> String
    forall a. Pretty a => a -> String
    prettyShow Arg Int
    n String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " of") Doc -> Doc -> Doc
    <?> Case CompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    pretty Case CompiledClauses
    bs

    -- * KillRange instances.

    instance KillRange c => KillRange (WithArity c) where
      killRange :: KillRangeT (WithArity c)
    killRange = (c -> c) -> KillRangeT (WithArity c)
    forall a b. (a -> b) -> WithArity a -> WithArity b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap c -> c
    forall a. KillRange a => KillRangeT a
    killRange

    instance KillRange c => KillRange (Case c) where
      killRange :: KillRangeT (Case c)
    killRange (Branches Bool
    cop Map QName (WithArity c)
    con Maybe (ConHead, WithArity c)
    eta Map Literal c
    lit Maybe c
    all Maybe Bool
    b Bool
    lazy) = Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    Branches Bool
    cop
        (KillRangeT (Map QName (WithArity c))
    forall k v. (KillRange k, KillRange v) => KillRangeT (Map k v)
    killRangeMap Map QName (WithArity c)
    con)
        (KillRangeT (Maybe (ConHead, WithArity c))
    forall a. KillRange a => KillRangeT a
    killRange Maybe (ConHead, WithArity c)
    eta)
        (KillRangeT (Map Literal c)
    forall k v. (KillRange k, KillRange v) => KillRangeT (Map k v)
    killRangeMap Map Literal c
    lit)
        (KillRangeT (Maybe c)
    forall a. KillRange a => KillRangeT a
    killRange Maybe c
    all)
        Maybe Bool
    b Bool
    lazy

    instance KillRange CompiledClauses where
      killRange :: KillRangeT CompiledClauses
    killRange (Case Arg Int
    i Case CompiledClauses
    br) = (Arg Int -> Case CompiledClauses -> CompiledClauses)
    -> Arg Int -> Case CompiledClauses -> CompiledClauses
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN Arg Int -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case Arg Int
    i Case CompiledClauses
    br
      killRange (Done [Arg String]
    xs Term
    v) = ([Arg String] -> Term -> CompiledClauses)
    -> [Arg String] -> Term -> CompiledClauses
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN [Arg String] -> Term -> CompiledClauses
    forall a. [Arg String] -> a -> CompiledClauses' a
    Done [Arg String]
    xs Term
    v
      killRange (Fail [Arg String]
    xs)   = ([Arg String] -> CompiledClauses)
    -> [Arg String] -> CompiledClauses
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN [Arg String] -> CompiledClauses
    forall a. [Arg String] -> CompiledClauses' a
    Fail [Arg String]
    xs

    -- * TermLike instances

    instance TermLike a => TermLike (WithArity a) where
      traverseTermM :: forall (m :: * -> *).
    Monad m =>
    (Term -> m Term) -> WithArity a -> m (WithArity a)
    traverseTermM = (a -> m a) -> WithArity a -> m (WithArity a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> WithArity a -> f (WithArity b)
    traverse ((a -> m a) -> WithArity a -> m (WithArity a))
    -> ((Term -> m Term) -> a -> m a)
    -> (Term -> m Term)
    -> WithArity a
    -> m (WithArity a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> m Term) -> a -> m a
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    forall (m :: * -> *). Monad m => (Term -> m Term) -> a -> m a
    traverseTermM
      foldTerm :: forall m. Monoid m => (Term -> m) -> WithArity a -> m
    foldTerm      = (a -> m) -> WithArity a -> m
    forall m a. Monoid m => (a -> m) -> WithArity a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((a -> m) -> WithArity a -> m)
    -> ((Term -> m) -> a -> m) -> (Term -> m) -> WithArity a -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> m) -> a -> m
    forall m. Monoid m => (Term -> m) -> a -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm

    instance TermLike a => TermLike (Case a) where
      traverseTermM :: forall (m :: * -> *).
    Monad m =>
    (Term -> m Term) -> Case a -> m (Case a)
    traverseTermM = (a -> m a) -> Case a -> m (Case a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Case a -> f (Case b)
    traverse ((a -> m a) -> Case a -> m (Case a))
    -> ((Term -> m Term) -> a -> m a)
    -> (Term -> m Term)
    -> Case a
    -> m (Case a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> m Term) -> a -> m a
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    forall (m :: * -> *). Monad m => (Term -> m Term) -> a -> m a
    traverseTermM
      foldTerm :: forall m. Monoid m => (Term -> m) -> Case a -> m
    foldTerm      = (a -> m) -> Case a -> m
    forall m a. Monoid m => (a -> m) -> Case a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((a -> m) -> Case a -> m)
    -> ((Term -> m) -> a -> m) -> (Term -> m) -> Case a -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> m) -> a -> m
    forall m. Monoid m => (Term -> m) -> a -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm

    instance TermLike a => TermLike (CompiledClauses' a) where
      traverseTermM :: forall (m :: * -> *).
    Monad m =>
    (Term -> m Term) -> CompiledClauses' a -> m (CompiledClauses' a)
    traverseTermM = (a -> m a) -> CompiledClauses' a -> m (CompiledClauses' a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b)
    traverse ((a -> m a) -> CompiledClauses' a -> m (CompiledClauses' a))
    -> ((Term -> m Term) -> a -> m a)
    -> (Term -> m Term)
    -> CompiledClauses' a
    -> m (CompiledClauses' a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> m Term) -> a -> m a
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    forall (m :: * -> *). Monad m => (Term -> m Term) -> a -> m a
    traverseTermM
      foldTerm :: forall m. Monoid m => (Term -> m) -> CompiledClauses' a -> m
    foldTerm      = (a -> m) -> CompiledClauses' a -> m
    forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((a -> m) -> CompiledClauses' a -> m)
    -> ((Term -> m) -> a -> m)
    -> (Term -> m)
    -> CompiledClauses' a
    -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> m) -> a -> m
    forall m. Monoid m => (Term -> m) -> a -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm

    -- NFData instances

    instance NFData c => NFData (WithArity c)
    instance NFData a => NFData (Case a)
    instance NFData a => NFData (CompiledClauses' a)