{-# LANGUAGE DeriveDataTypeable #-}

-- | 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 qualified Data.Map as Map
import Data.Map (Map)
import Data.Semigroup hiding (Arg(..))




import Data.Data (Data)

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.Utils.Pretty

import Agda.Utils.Impossible

data WithArity c = WithArity { WithArity c -> Int
arity :: Int, WithArity c -> c
content :: c }
  deriving (Typeable (WithArity c)
Constr
DataType
Typeable (WithArity c) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> WithArity c -> c (WithArity c))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (WithArity c))
-> (WithArity c -> Constr)
-> (WithArity c -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (WithArity c)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (WithArity c)))
-> ((forall b. Data b => b -> b) -> WithArity c -> WithArity c)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> WithArity c -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> WithArity c -> r)
-> (forall u. (forall d. Data d => d -> u) -> WithArity c -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> WithArity c -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c))
-> Data (WithArity c)
WithArity c -> Constr
WithArity c -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (WithArity c))
(forall b. Data b => b -> b) -> WithArity c -> WithArity c
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> WithArity c -> c (WithArity c)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (WithArity c)
forall c. Data c => Typeable (WithArity c)
forall c. Data c => WithArity c -> Constr
forall c. Data c => WithArity c -> DataType
forall c.
Data c =>
(forall b. Data b => b -> b) -> WithArity c -> WithArity c
forall c u.
Data c =>
Int -> (forall d. Data d => d -> u) -> WithArity c -> u
forall c u.
Data c =>
(forall d. Data d => d -> u) -> WithArity c -> [u]
forall c r r'.
Data c =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> WithArity c -> r
forall c r r'.
Data c =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> WithArity c -> r
forall c (m :: * -> *).
(Data c, Monad m) =>
(forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
forall c (m :: * -> *).
(Data c, MonadPlus m) =>
(forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
forall c (c :: * -> *).
Data c =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (WithArity c)
forall c (c :: * -> *).
Data c =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> WithArity c -> c (WithArity c)
forall c (t :: * -> *) (c :: * -> *).
(Data c, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (WithArity c))
forall c (t :: * -> * -> *) (c :: * -> *).
(Data c, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (WithArity c))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> WithArity c -> u
forall u. (forall d. Data d => d -> u) -> WithArity c -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> WithArity c -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> WithArity c -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (WithArity c)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> WithArity c -> c (WithArity c)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (WithArity c))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (WithArity c))
$cWithArity :: Constr
$tWithArity :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
$cgmapMo :: forall c (m :: * -> *).
(Data c, MonadPlus m) =>
(forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
gmapMp :: (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
$cgmapMp :: forall c (m :: * -> *).
(Data c, MonadPlus m) =>
(forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
gmapM :: (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
$cgmapM :: forall c (m :: * -> *).
(Data c, Monad m) =>
(forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c)
gmapQi :: Int -> (forall d. Data d => d -> u) -> WithArity c -> u
$cgmapQi :: forall c u.
Data c =>
Int -> (forall d. Data d => d -> u) -> WithArity c -> u
gmapQ :: (forall d. Data d => d -> u) -> WithArity c -> [u]
$cgmapQ :: forall c u.
Data c =>
(forall d. Data d => d -> u) -> WithArity c -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> WithArity c -> r
$cgmapQr :: forall c r r'.
Data c =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> WithArity c -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> WithArity c -> r
$cgmapQl :: forall c r r'.
Data c =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> WithArity c -> r
gmapT :: (forall b. Data b => b -> b) -> WithArity c -> WithArity c
$cgmapT :: forall c.
Data c =>
(forall b. Data b => b -> b) -> WithArity c -> WithArity c
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (WithArity c))
$cdataCast2 :: forall c (t :: * -> * -> *) (c :: * -> *).
(Data c, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (WithArity c))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (WithArity c))
$cdataCast1 :: forall c (t :: * -> *) (c :: * -> *).
(Data c, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (WithArity c))
dataTypeOf :: WithArity c -> DataType
$cdataTypeOf :: forall c. Data c => WithArity c -> DataType
toConstr :: WithArity c -> Constr
$ctoConstr :: forall c. Data c => WithArity c -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (WithArity c)
$cgunfold :: forall c (c :: * -> *).
Data c =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (WithArity c)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> WithArity c -> c (WithArity c)
$cgfoldl :: forall c (c :: * -> *).
Data c =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> WithArity c -> c (WithArity c)
$cp1Data :: forall c. Data c => Typeable (WithArity c)
Data, a -> WithArity b -> WithArity a
(a -> b) -> WithArity a -> WithArity b
(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
<$ :: a -> WithArity b -> WithArity a
$c<$ :: forall a b. a -> WithArity b -> WithArity a
fmap :: (a -> b) -> WithArity a -> WithArity b
$cfmap :: forall a b. (a -> b) -> WithArity a -> WithArity b
Functor, WithArity a -> Bool
(a -> m) -> WithArity a -> m
(a -> b -> b) -> b -> WithArity a -> b
(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 a. WithArity a -> 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 a. WithArity a -> 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
product :: WithArity a -> a
$cproduct :: forall a. Num a => WithArity a -> a
sum :: WithArity a -> a
$csum :: forall a. Num a => WithArity a -> a
minimum :: WithArity a -> a
$cminimum :: forall a. Ord a => WithArity a -> a
maximum :: WithArity a -> a
$cmaximum :: forall a. Ord a => WithArity a -> a
elem :: a -> WithArity a -> Bool
$celem :: forall a. Eq a => a -> WithArity a -> Bool
length :: WithArity a -> Int
$clength :: forall a. WithArity a -> Int
null :: WithArity a -> Bool
$cnull :: forall a. WithArity a -> Bool
toList :: WithArity a -> [a]
$ctoList :: forall a. WithArity a -> [a]
foldl1 :: (a -> a -> a) -> WithArity a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> WithArity a -> a
foldr1 :: (a -> a -> a) -> WithArity a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> WithArity a -> a
foldl' :: (b -> a -> b) -> b -> WithArity a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> WithArity a -> b
foldl :: (b -> a -> b) -> b -> WithArity a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> WithArity a -> b
foldr' :: (a -> b -> b) -> b -> WithArity a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> WithArity a -> b
foldr :: (a -> b -> b) -> b -> WithArity a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> WithArity a -> b
foldMap' :: (a -> m) -> WithArity a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> WithArity a -> m
foldMap :: (a -> m) -> WithArity a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> WithArity a -> m
fold :: WithArity m -> m
$cfold :: forall m. Monoid m => WithArity m -> m
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
(a -> f b) -> WithArity a -> f (WithArity b)
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)
sequence :: WithArity (m a) -> m (WithArity a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
WithArity (m a) -> m (WithArity a)
mapM :: (a -> m b) -> WithArity a -> m (WithArity b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> WithArity a -> m (WithArity b)
sequenceA :: WithArity (f a) -> f (WithArity a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
WithArity (f a) -> f (WithArity a)
traverse :: (a -> f b) -> WithArity a -> f (WithArity b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> WithArity a -> f (WithArity b)
$cp2Traversable :: Foldable WithArity
$cp1Traversable :: Functor WithArity
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
showList :: [WithArity c] -> ShowS
$cshowList :: forall c. Show c => [WithArity c] -> ShowS
show :: WithArity c -> String
$cshow :: forall c. Show c => WithArity c -> String
showsPrec :: Int -> WithArity c -> ShowS
$cshowsPrec :: forall c. Show c => Int -> WithArity c -> ShowS
Show)

-- | Branches in a case tree.

data Case c = Branches
  { Case c -> Bool
projPatterns   :: Bool
    -- ^ We are constructing a record here (copatterns).
    --   'conBranches' lists projections.
  , 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.)
  , 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.
  , Case c -> Map Literal c
litBranches    :: Map Literal c
    -- ^ Map from literal to case subtree.
  , Case c -> Maybe c
catchAllBranch :: Maybe c
    -- ^ (Possibly additional) catch-all clause.
  , Case c -> Maybe Bool
fallThrough :: Maybe Bool
    -- ^ (if True) In case of non-canonical argument use catchAllBranch.
  , Case c -> Bool
lazyMatch :: Bool
    -- ^ Lazy pattern match. Requires single (non-copattern) branch with no lit
    --   branches and no catch-all.
  }
  deriving (Typeable (Case c)
Constr
DataType
Typeable (Case c) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Case c -> c (Case c))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Case c))
-> (Case c -> Constr)
-> (Case c -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Case c)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Case c)))
-> ((forall b. Data b => b -> b) -> Case c -> Case c)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Case c -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Case c -> r)
-> (forall u. (forall d. Data d => d -> u) -> Case c -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Case c -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Case c -> m (Case c))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Case c -> m (Case c))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Case c -> m (Case c))
-> Data (Case c)
Case c -> Constr
Case c -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (Case c))
(forall b. Data b => b -> b) -> Case c -> Case c
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Case c -> c (Case c)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Case c)
forall c. Data c => Typeable (Case c)
forall c. Data c => Case c -> Constr
forall c. Data c => Case c -> DataType
forall c.
Data c =>
(forall b. Data b => b -> b) -> Case c -> Case c
forall c u.
Data c =>
Int -> (forall d. Data d => d -> u) -> Case c -> u
forall c u. Data c => (forall d. Data d => d -> u) -> Case c -> [u]
forall c r r'.
Data c =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r
forall c r r'.
Data c =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r
forall c (m :: * -> *).
(Data c, Monad m) =>
(forall d. Data d => d -> m d) -> Case c -> m (Case c)
forall c (m :: * -> *).
(Data c, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Case c -> m (Case c)
forall c (c :: * -> *).
Data c =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Case c)
forall c (c :: * -> *).
Data c =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Case c -> c (Case c)
forall c (t :: * -> *) (c :: * -> *).
(Data c, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Case c))
forall c (t :: * -> * -> *) (c :: * -> *).
(Data c, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Case c))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Case c -> u
forall u. (forall d. Data d => d -> u) -> Case c -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Case c -> m (Case c)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Case c -> m (Case c)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Case c)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Case c -> c (Case c)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Case c))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Case c))
$cBranches :: Constr
$tCase :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Case c -> m (Case c)
$cgmapMo :: forall c (m :: * -> *).
(Data c, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Case c -> m (Case c)
gmapMp :: (forall d. Data d => d -> m d) -> Case c -> m (Case c)
$cgmapMp :: forall c (m :: * -> *).
(Data c, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Case c -> m (Case c)
gmapM :: (forall d. Data d => d -> m d) -> Case c -> m (Case c)
$cgmapM :: forall c (m :: * -> *).
(Data c, Monad m) =>
(forall d. Data d => d -> m d) -> Case c -> m (Case c)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Case c -> u
$cgmapQi :: forall c u.
Data c =>
Int -> (forall d. Data d => d -> u) -> Case c -> u
gmapQ :: (forall d. Data d => d -> u) -> Case c -> [u]
$cgmapQ :: forall c u. Data c => (forall d. Data d => d -> u) -> Case c -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r
$cgmapQr :: forall c r r'.
Data c =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r
$cgmapQl :: forall c r r'.
Data c =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r
gmapT :: (forall b. Data b => b -> b) -> Case c -> Case c
$cgmapT :: forall c.
Data c =>
(forall b. Data b => b -> b) -> Case c -> Case c
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Case c))
$cdataCast2 :: forall c (t :: * -> * -> *) (c :: * -> *).
(Data c, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Case c))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Case c))
$cdataCast1 :: forall c (t :: * -> *) (c :: * -> *).
(Data c, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Case c))
dataTypeOf :: Case c -> DataType
$cdataTypeOf :: forall c. Data c => Case c -> DataType
toConstr :: Case c -> Constr
$ctoConstr :: forall c. Data c => Case c -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Case c)
$cgunfold :: forall c (c :: * -> *).
Data c =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Case c)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Case c -> c (Case c)
$cgfoldl :: forall c (c :: * -> *).
Data c =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Case c -> c (Case c)
$cp1Data :: forall c. Data c => Typeable (Case c)
Data, a -> Case b -> Case a
(a -> b) -> Case a -> Case b
(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
<$ :: a -> Case b -> Case a
$c<$ :: forall a b. a -> Case b -> Case a
fmap :: (a -> b) -> Case a -> Case b
$cfmap :: forall a b. (a -> b) -> Case a -> Case b
Functor, Case a -> Bool
(a -> m) -> Case a -> m
(a -> b -> b) -> b -> Case a -> b
(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 a. Case a -> 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 a. Case a -> 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
product :: Case a -> a
$cproduct :: forall a. Num a => Case a -> a
sum :: Case a -> a
$csum :: forall a. Num a => Case a -> a
minimum :: Case a -> a
$cminimum :: forall a. Ord a => Case a -> a
maximum :: Case a -> a
$cmaximum :: forall a. Ord a => Case a -> a
elem :: a -> Case a -> Bool
$celem :: forall a. Eq a => a -> Case a -> Bool
length :: Case a -> Int
$clength :: forall a. Case a -> Int
null :: Case a -> Bool
$cnull :: forall a. Case a -> Bool
toList :: Case a -> [a]
$ctoList :: forall a. Case a -> [a]
foldl1 :: (a -> a -> a) -> Case a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Case a -> a
foldr1 :: (a -> a -> a) -> Case a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Case a -> a
foldl' :: (b -> a -> b) -> b -> Case a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Case a -> b
foldl :: (b -> a -> b) -> b -> Case a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Case a -> b
foldr' :: (a -> b -> b) -> b -> Case a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Case a -> b
foldr :: (a -> b -> b) -> b -> Case a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Case a -> b
foldMap' :: (a -> m) -> Case a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Case a -> m
foldMap :: (a -> m) -> Case a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Case a -> m
fold :: Case m -> m
$cfold :: forall m. Monoid m => Case m -> m
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
(a -> f b) -> Case a -> f (Case b)
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)
sequence :: Case (m a) -> m (Case a)
$csequence :: forall (m :: * -> *) a. Monad m => Case (m a) -> m (Case a)
mapM :: (a -> m b) -> Case a -> m (Case b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Case a -> m (Case b)
sequenceA :: Case (f a) -> f (Case a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Case (f a) -> f (Case a)
traverse :: (a -> f b) -> Case a -> f (Case b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Case a -> f (Case b)
$cp2Traversable :: Foldable Case
$cp1Traversable :: Functor Case
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
showList :: [Case c] -> ShowS
$cshowList :: forall c. Show c => [Case c] -> ShowS
show :: Case c -> String
$cshow :: forall c. Show c => Case c -> String
showsPrec :: Int -> Case c -> ShowS
$cshowsPrec :: forall c. Show c => Int -> Case c -> ShowS
Show)

-- | 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
    -- ^ Absurd case.
  deriving (Typeable (CompiledClauses' a)
Constr
DataType
Typeable (CompiledClauses' a) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> CompiledClauses' a
 -> c (CompiledClauses' a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (CompiledClauses' a))
-> (CompiledClauses' a -> Constr)
-> (CompiledClauses' a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (CompiledClauses' a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (CompiledClauses' a)))
-> ((forall b. Data b => b -> b)
    -> CompiledClauses' a -> CompiledClauses' a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> CompiledClauses' a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> CompiledClauses' a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> CompiledClauses' a -> m (CompiledClauses' a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> CompiledClauses' a -> m (CompiledClauses' a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> CompiledClauses' a -> m (CompiledClauses' a))
-> Data (CompiledClauses' a)
CompiledClauses' a -> Constr
CompiledClauses' a -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (CompiledClauses' a))
(forall b. Data b => b -> b)
-> CompiledClauses' a -> CompiledClauses' a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompiledClauses' a
-> c (CompiledClauses' a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompiledClauses' a)
forall a. Data a => Typeable (CompiledClauses' a)
forall a. Data a => CompiledClauses' a -> Constr
forall a. Data a => CompiledClauses' a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b)
-> CompiledClauses' a -> CompiledClauses' a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> CompiledClauses' a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> CompiledClauses' a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompiledClauses' a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompiledClauses' a
-> c (CompiledClauses' a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (CompiledClauses' a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CompiledClauses' a))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> CompiledClauses' a -> u
forall u. (forall d. Data d => d -> u) -> CompiledClauses' a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompiledClauses' a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompiledClauses' a
-> c (CompiledClauses' a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (CompiledClauses' a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CompiledClauses' a))
$cFail :: Constr
$cDone :: Constr
$cCase :: Constr
$tCompiledClauses' :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
gmapMp :: (forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
gmapM :: (forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> CompiledClauses' a -> m (CompiledClauses' a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> CompiledClauses' a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> CompiledClauses' a -> u
gmapQ :: (forall d. Data d => d -> u) -> CompiledClauses' a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> CompiledClauses' a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r
gmapT :: (forall b. Data b => b -> b)
-> CompiledClauses' a -> CompiledClauses' a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b)
-> CompiledClauses' a -> CompiledClauses' a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CompiledClauses' a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (CompiledClauses' a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (CompiledClauses' a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (CompiledClauses' a))
dataTypeOf :: CompiledClauses' a -> DataType
$cdataTypeOf :: forall a. Data a => CompiledClauses' a -> DataType
toConstr :: CompiledClauses' a -> Constr
$ctoConstr :: forall a. Data a => CompiledClauses' a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompiledClauses' a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CompiledClauses' a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompiledClauses' a
-> c (CompiledClauses' a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> CompiledClauses' a
-> c (CompiledClauses' a)
$cp1Data :: forall a. Data a => Typeable (CompiledClauses' a)
Data, a -> CompiledClauses' b -> CompiledClauses' a
(a -> b) -> CompiledClauses' a -> CompiledClauses' b
(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
<$ :: a -> CompiledClauses' b -> CompiledClauses' a
$c<$ :: forall a b. a -> CompiledClauses' b -> CompiledClauses' a
fmap :: (a -> b) -> CompiledClauses' a -> CompiledClauses' b
$cfmap :: forall a b. (a -> b) -> CompiledClauses' a -> CompiledClauses' b
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'
(a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b)
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)
sequence :: CompiledClauses' (m a) -> m (CompiledClauses' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
CompiledClauses' (m a) -> m (CompiledClauses' a)
mapM :: (a -> m b) -> CompiledClauses' a -> m (CompiledClauses' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> CompiledClauses' a -> m (CompiledClauses' b)
sequenceA :: CompiledClauses' (f a) -> f (CompiledClauses' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
CompiledClauses' (f a) -> f (CompiledClauses' a)
traverse :: (a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b)
$cp2Traversable :: Foldable CompiledClauses'
$cp1Traversable :: Functor CompiledClauses'
Traversable, CompiledClauses' a -> Bool
(a -> m) -> CompiledClauses' a -> m
(a -> b -> b) -> b -> CompiledClauses' a -> b
(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
product :: CompiledClauses' a -> a
$cproduct :: forall a. Num a => CompiledClauses' a -> a
sum :: CompiledClauses' a -> a
$csum :: forall a. Num a => CompiledClauses' a -> a
minimum :: CompiledClauses' a -> a
$cminimum :: forall a. Ord a => CompiledClauses' a -> a
maximum :: CompiledClauses' a -> a
$cmaximum :: forall a. Ord a => CompiledClauses' a -> a
elem :: a -> CompiledClauses' a -> Bool
$celem :: forall a. Eq a => a -> CompiledClauses' a -> Bool
length :: CompiledClauses' a -> Int
$clength :: forall a. CompiledClauses' a -> Int
null :: CompiledClauses' a -> Bool
$cnull :: forall a. CompiledClauses' a -> Bool
toList :: CompiledClauses' a -> [a]
$ctoList :: forall a. CompiledClauses' a -> [a]
foldl1 :: (a -> a -> a) -> CompiledClauses' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> CompiledClauses' a -> a
foldr1 :: (a -> a -> a) -> CompiledClauses' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> CompiledClauses' a -> a
foldl' :: (b -> a -> b) -> b -> CompiledClauses' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> CompiledClauses' a -> b
foldl :: (b -> a -> b) -> b -> CompiledClauses' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> CompiledClauses' a -> b
foldr' :: (a -> b -> b) -> b -> CompiledClauses' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> CompiledClauses' a -> b
foldr :: (a -> b -> b) -> b -> CompiledClauses' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> CompiledClauses' a -> b
foldMap' :: (a -> m) -> CompiledClauses' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m
foldMap :: (a -> m) -> CompiledClauses' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> CompiledClauses' a -> m
fold :: CompiledClauses' m -> m
$cfold :: forall m. Monoid m => CompiledClauses' m -> m
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
showList :: [CompiledClauses' a] -> ShowS
$cshowList :: forall a. Show a => [CompiledClauses' a] -> ShowS
show :: CompiledClauses' a -> String
$cshow :: forall a. Show a => CompiledClauses' a -> String
showsPrec :: Int -> CompiledClauses' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> CompiledClauses' a -> ShowS
Show)

type CompiledClauses = CompiledClauses' Term

litCase :: Literal -> c -> Case c
litCase :: Literal -> c -> Case c
litCase l :: Literal
l x :: 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 :: QName -> Bool -> WithArity c -> Case c
conCase c :: QName
c b :: Bool
b x :: 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 :: ConHead -> WithArity c -> Case c
etaCase c :: ConHead
c x :: 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 :: QName -> c -> Case c
projCase c :: QName
c x :: 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 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 :: c -> Case c
catchAll x :: 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 :: Case c -> Case c
checkLazyMatch b :: Case c
b = Case c
b { lazyMatch :: Bool
lazyMatch = Case c -> Bool
forall a. Case a -> Bool
lazyMatch Case c
b Bool -> Bool -> Bool
&& Bool
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
<= 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 a. Case a -> 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 cc :: 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 _ br :: 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 (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 cc :: 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 _ br :: Case (CompiledClauses' a)
br -> Bool -> Any
Any (Case (CompiledClauses' a) -> Bool
forall a. Case a -> Bool
projPatterns Case (CompiledClauses' a)
br) Any -> Any -> Any
forall a. Semigroup a => a -> a -> a
<> (CompiledClauses' a -> Any) -> Case (CompiledClauses' a) -> Any
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 n1 :: Int
n1 c1 :: c
c1 <> :: WithArity c -> WithArity c -> WithArity c
<> WithArity n2 :: Int
n2 c2 :: 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 cop :: Bool
cop cs :: Map QName (WithArity m)
cs eta :: Maybe (ConHead, WithArity m)
eta ls :: Map Literal m
ls m :: Maybe m
m b :: Maybe Bool
b lazy :: Bool
lazy <> :: Case m -> Case m -> Case m
<> Branches cop' :: Bool
cop' cs' :: Map QName (WithArity m)
cs' eta' :: Maybe (ConHead, WithArity m)
eta' ls' :: Map Literal m
ls' m' :: Maybe m
m' b' :: Maybe Bool
b' lazy' :: 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 Nothing  b' :: Maybe Bool
b'        = Maybe Bool
b
     combine b :: Maybe Bool
b        Nothing   = Maybe Bool
b
     combine (Just b :: Bool
b) (Just b' :: 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 Nothing b :: Maybe a
b = Maybe a
b
     unionEta b :: Maybe a
b 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 _cop :: Bool
_cop cs :: Map QName (WithArity m)
cs eta :: Maybe (ConHead, WithArity m)
eta ls :: Map Literal m
ls mcatch :: Maybe m
mcatch _b :: Maybe Bool
_b _lazy :: 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 p :: Int
p (Branches _cop :: Bool
_cop cs :: Map QName (WithArity a)
cs eta :: Maybe (ConHead, WithArity a)
eta ls :: Map Literal a
ls m :: Maybe a
m b :: Maybe Bool
b lazy :: Bool
lazy) =
    Bool -> Doc -> Doc
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Bool -> Doc
forall p. (IsString p, Null p) => Bool -> p
prLazy Bool
lazy Doc -> Doc -> Doc
<+> [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 -> p
prLazy True  = "~"
      prLazy False = p
forall a. Null a => a
empty
      prC :: Maybe a -> [Doc]
prC Nothing = []
      prC (Just x :: a
x) = ["_ ->" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x]
      prEta :: Maybe (a, a) -> [Doc]
prEta Nothing = []
      prEta (Just (c :: a
c, cc :: a
cc)) = [("eta" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
c Doc -> Doc -> 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 :: Map k v -> [Doc]
prettyMap m :: Map k v
m = [ [Doc] -> Doc
sep [ k -> Doc
forall a. Pretty a => a -> Doc
pretty k
k Doc -> Doc -> Doc
<+> "->"
                    , Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ v -> Doc
forall a. Pretty a => a -> Doc
pretty v
v ]
              | (k :: k
k, v :: v
v) <- Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
m ]

instance Pretty CompiledClauses where
  pretty :: CompiledClauses -> Doc
pretty (Done hs :: [Arg String]
hs t :: Term
t) = ("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        = "fail"
  pretty (Case n :: Arg Int
n bs :: Case CompiledClauses
bs) | Case CompiledClauses -> Bool
forall a. Case a -> Bool
projPatterns Case CompiledClauses
bs =
    [Doc] -> Doc
sep [ "record"
        , Int -> Doc -> Doc
nest 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 n :: Arg Int
n bs :: Case CompiledClauses
bs) =
    String -> Doc
text ("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]
++ " 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 (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 cop :: Bool
cop con :: Map QName (WithArity c)
con eta :: Maybe (ConHead, WithArity c)
eta lit :: Map Literal c
lit all :: Maybe c
all b :: Maybe Bool
b lazy :: 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 i :: Arg Int
i br :: Case CompiledClauses
br) = (Arg Int -> Case CompiledClauses -> CompiledClauses)
-> Arg Int -> Case CompiledClauses -> CompiledClauses
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
i Case CompiledClauses
br
  killRange (Done xs :: [Arg String]
xs v :: Term
v) = ([Arg String] -> Term -> CompiledClauses)
-> [Arg String] -> Term -> CompiledClauses
forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 [Arg String] -> Term -> CompiledClauses
forall a. [Arg String] -> a -> CompiledClauses' a
Done [Arg String]
xs Term
v
  killRange Fail        = CompiledClauses
forall a. CompiledClauses' a
Fail

-- * TermLike instances

instance TermLike a => TermLike (WithArity a) where
  traverseTermM :: (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)
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
traverseTermM
  foldTerm :: (Term -> m) -> WithArity a -> m
foldTerm      = (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 a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm

instance TermLike a => TermLike (Case a) where
  traverseTermM :: (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)
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
traverseTermM
  foldTerm :: (Term -> m) -> Case a -> m
foldTerm      = (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 a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm

instance TermLike a => TermLike (CompiledClauses' a) where
  traverseTermM :: (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)
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
traverseTermM
  foldTerm :: (Term -> m) -> CompiledClauses' a -> m
foldTerm      = (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 a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm