{-# 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

-- | The number of a 'Clause' (starting with 0) in the clause list of a 'FunctionData'.
type ClauseNumber = Int

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)

type CompiledClauses = CompiledClauses' Term

-- | 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_ (CCDone a)
  | 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)

{-# COMPLETE Case, Done, Fail #-}

-- | Data stored in 'Done' nodes of the case tree.
--  @CCDone no mr 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.
--   The @no@ is the number of the original 'Clause' this case tree leaf comes from.
--   @mr@ tells whether this body contains calls to the mutually recursive functions.
data CCDone a = CCDone
  { forall a. CCDone a -> Int
ccClauseNumber    :: ClauseNumber
  , forall a. CCDone a -> ClauseRecursive
ccClauseRecursive :: ClauseRecursive
  , forall a. CCDone a -> [Arg String]
ccBoundVars       :: [Arg ArgName]
  , forall a. CCDone a -> a
ccBody            :: a
  }
  deriving ((forall a b. (a -> b) -> CCDone a -> CCDone b)
-> (forall a b. a -> CCDone b -> CCDone a) -> Functor CCDone
forall a b. a -> CCDone b -> CCDone a
forall a b. (a -> b) -> CCDone a -> CCDone 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) -> CCDone a -> CCDone b
fmap :: forall a b. (a -> b) -> CCDone a -> CCDone b
$c<$ :: forall a b. a -> CCDone b -> CCDone a
<$ :: forall a b. a -> CCDone b -> CCDone a
Functor, Functor CCDone
Foldable CCDone
(Functor CCDone, Foldable CCDone) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> CCDone a -> f (CCDone b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    CCDone (f a) -> f (CCDone a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> CCDone a -> m (CCDone b))
-> (forall (m :: * -> *) a.
    Monad m =>
    CCDone (m a) -> m (CCDone a))
-> Traversable CCDone
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 => CCDone (m a) -> m (CCDone a)
forall (f :: * -> *) a.
Applicative f =>
CCDone (f a) -> f (CCDone a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> CCDone a -> m (CCDone b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> CCDone a -> f (CCDone b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> CCDone a -> f (CCDone b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> CCDone a -> f (CCDone b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
CCDone (f a) -> f (CCDone a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
CCDone (f a) -> f (CCDone a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> CCDone a -> m (CCDone b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> CCDone a -> m (CCDone b)
$csequence :: forall (m :: * -> *) a. Monad m => CCDone (m a) -> m (CCDone a)
sequence :: forall (m :: * -> *) a. Monad m => CCDone (m a) -> m (CCDone a)
Traversable, (forall m. Monoid m => CCDone m -> m)
-> (forall m a. Monoid m => (a -> m) -> CCDone a -> m)
-> (forall m a. Monoid m => (a -> m) -> CCDone a -> m)
-> (forall a b. (a -> b -> b) -> b -> CCDone a -> b)
-> (forall a b. (a -> b -> b) -> b -> CCDone a -> b)
-> (forall b a. (b -> a -> b) -> b -> CCDone a -> b)
-> (forall b a. (b -> a -> b) -> b -> CCDone a -> b)
-> (forall a. (a -> a -> a) -> CCDone a -> a)
-> (forall a. (a -> a -> a) -> CCDone a -> a)
-> (forall a. CCDone a -> [a])
-> (forall a. CCDone a -> Bool)
-> (forall a. CCDone a -> Int)
-> (forall a. Eq a => a -> CCDone a -> Bool)
-> (forall a. Ord a => CCDone a -> a)
-> (forall a. Ord a => CCDone a -> a)
-> (forall a. Num a => CCDone a -> a)
-> (forall a. Num a => CCDone a -> a)
-> Foldable CCDone
forall a. Eq a => a -> CCDone a -> Bool
forall a. Num a => CCDone a -> a
forall a. Ord a => CCDone a -> a
forall m. Monoid m => CCDone m -> m
forall a. CCDone a -> Bool
forall a. CCDone a -> Int
forall a. CCDone a -> [a]
forall a. (a -> a -> a) -> CCDone a -> a
forall m a. Monoid m => (a -> m) -> CCDone a -> m
forall b a. (b -> a -> b) -> b -> CCDone a -> b
forall a b. (a -> b -> b) -> b -> CCDone 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 => CCDone m -> m
fold :: forall m. Monoid m => CCDone m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> CCDone a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> CCDone a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> CCDone a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> CCDone a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> CCDone a -> b
foldr :: forall a b. (a -> b -> b) -> b -> CCDone a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> CCDone a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> CCDone a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> CCDone a -> b
foldl :: forall b a. (b -> a -> b) -> b -> CCDone a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> CCDone a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> CCDone a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> CCDone a -> a
foldr1 :: forall a. (a -> a -> a) -> CCDone a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> CCDone a -> a
foldl1 :: forall a. (a -> a -> a) -> CCDone a -> a
$ctoList :: forall a. CCDone a -> [a]
toList :: forall a. CCDone a -> [a]
$cnull :: forall a. CCDone a -> Bool
null :: forall a. CCDone a -> Bool
$clength :: forall a. CCDone a -> Int
length :: forall a. CCDone a -> Int
$celem :: forall a. Eq a => a -> CCDone a -> Bool
elem :: forall a. Eq a => a -> CCDone a -> Bool
$cmaximum :: forall a. Ord a => CCDone a -> a
maximum :: forall a. Ord a => CCDone a -> a
$cminimum :: forall a. Ord a => CCDone a -> a
minimum :: forall a. Ord a => CCDone a -> a
$csum :: forall a. Num a => CCDone a -> a
sum :: forall a. Num a => CCDone a -> a
$cproduct :: forall a. Num a => CCDone a -> a
product :: forall a. Num a => CCDone a -> a
Foldable, Int -> CCDone a -> ShowS
[CCDone a] -> ShowS
CCDone a -> String
(Int -> CCDone a -> ShowS)
-> (CCDone a -> String) -> ([CCDone a] -> ShowS) -> Show (CCDone a)
forall a. Show a => Int -> CCDone a -> ShowS
forall a. Show a => [CCDone a] -> ShowS
forall a. Show a => CCDone a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> CCDone a -> ShowS
showsPrec :: Int -> CCDone a -> ShowS
$cshow :: forall a. Show a => CCDone a -> String
show :: CCDone a -> String
$cshowList :: forall a. Show a => [CCDone a] -> ShowS
showList :: [CCDone a] -> ShowS
Show, (forall x. CCDone a -> Rep (CCDone a) x)
-> (forall x. Rep (CCDone a) x -> CCDone a) -> Generic (CCDone a)
forall x. Rep (CCDone a) x -> CCDone a
forall x. CCDone a -> Rep (CCDone a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (CCDone a) x -> CCDone a
forall a x. CCDone a -> Rep (CCDone a) x
$cfrom :: forall a x. CCDone a -> Rep (CCDone a) x
from :: forall x. CCDone a -> Rep (CCDone a) x
$cto :: forall a x. Rep (CCDone a) x -> CCDone a
to :: forall x. Rep (CCDone a) x -> CCDone a
Generic)

pattern Done :: ClauseNumber -> ClauseRecursive -> [Arg ArgName] -> a -> CompiledClauses' a
pattern $mDone :: forall {r} {a}.
CompiledClauses' a
-> (Int -> ClauseRecursive -> [Arg String] -> a -> r)
-> ((# #) -> r)
-> r
$bDone :: forall a.
Int -> ClauseRecursive -> [Arg String] -> a -> CompiledClauses' a
Done no mr xs b = Done_ (CCDone no mr xs b)

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

---------------------------------------------------------------------------
-- * Traversing the 'Done' leaves

class MapDone f where
  mapDone :: (CCDone a -> CCDone b) -> f a -> f b

-- instance MapDone CCDone where
--   mapDone = id

instance MapDone CompiledClauses' where
  mapDone :: forall a b.
(CCDone a -> CCDone b) -> CompiledClauses' a -> CompiledClauses' b
mapDone CCDone a -> CCDone b
f = \case
    Case Arg Int
n Case (CompiledClauses' a)
bs  -> Arg Int -> Case (CompiledClauses' b) -> CompiledClauses' b
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
n (Case (CompiledClauses' b) -> CompiledClauses' b)
-> Case (CompiledClauses' b) -> CompiledClauses' b
forall a b. (a -> b) -> a -> b
$ (CompiledClauses' a -> CompiledClauses' b)
-> Case (CompiledClauses' a) -> Case (CompiledClauses' b)
forall a b. (a -> b) -> Case a -> Case b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((CCDone a -> CCDone b) -> CompiledClauses' a -> CompiledClauses' b
forall a b.
(CCDone a -> CCDone b) -> CompiledClauses' a -> CompiledClauses' b
forall (f :: * -> *) a b.
MapDone f =>
(CCDone a -> CCDone b) -> f a -> f b
mapDone CCDone a -> CCDone b
f) Case (CompiledClauses' a)
bs
    Done_ CCDone a
done -> CCDone b -> CompiledClauses' b
forall a. CCDone a -> CompiledClauses' a
Done_ (CCDone b -> CompiledClauses' b) -> CCDone b -> CompiledClauses' b
forall a b. (a -> b) -> a -> b
$ CCDone a -> CCDone b
f CCDone a
done
    Fail [Arg String]
xs    -> [Arg String] -> CompiledClauses' b
forall a. [Arg String] -> CompiledClauses' a
Fail [Arg String]
xs

---------------------------------------------------------------------------
-- Collection instances

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 a => Pretty (CompiledClauses' a) where
  pretty :: CompiledClauses' a -> Doc
pretty (Done_ CCDone a
done) = CCDone a -> Doc
forall a. Pretty a => a -> Doc
pretty CCDone a
done
  pretty Fail{}       = Doc
"fail"
  pretty (Case Arg Int
n Case (CompiledClauses' a)
bs) | Case (CompiledClauses' a) -> Bool
forall c. Case c -> Bool
projPatterns Case (CompiledClauses' a)
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' a) -> Doc
forall a. Pretty a => a -> Doc
pretty Case (CompiledClauses' a)
bs
        ]
  pretty (Case Arg Int
n Case (CompiledClauses' a)
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' a) -> Doc
forall a. Pretty a => a -> Doc
pretty Case (CompiledClauses' a)
bs

instance Pretty a => Pretty (CCDone a) where
  pretty :: CCDone a -> Doc
pretty (CCDone Int
no ClauseRecursive
mr [Arg String]
xs a
t) = (Doc
"done" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
no Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> ClauseRecursive -> Doc
forall a. Pretty a => a -> Doc
pretty ClauseRecursive
mr Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
":") Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Arg String] -> Doc
forall a. Pretty a => a -> Doc
pretty [Arg String]
xs) Doc -> Doc -> Doc
<?> Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 a
t

---------------------------------------------------------------------------
-- 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 Int
no ClauseRecursive
mr [Arg String]
xs Term
v) = (Int -> ClauseRecursive -> [Arg String] -> Term -> CompiledClauses)
-> Int
-> ClauseRecursive
-> [Arg String]
-> Term
-> CompiledClauses
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Int -> ClauseRecursive -> [Arg String] -> Term -> CompiledClauses
forall a.
Int -> ClauseRecursive -> [Arg String] -> a -> CompiledClauses' a
Done Int
no ClauseRecursive
mr [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

instance TermLike a => TermLike (CCDone a) where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> CCDone a -> m (CCDone a)
traverseTermM = (a -> m a) -> CCDone a -> m (CCDone 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) -> CCDone a -> f (CCDone b)
traverse ((a -> m a) -> CCDone a -> m (CCDone a))
-> ((Term -> m Term) -> a -> m a)
-> (Term -> m Term)
-> CCDone a
-> m (CCDone 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) -> CCDone a -> m
foldTerm      = (a -> m) -> CCDone a -> m
forall m a. Monoid m => (a -> m) -> CCDone a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> CCDone a -> m)
-> ((Term -> m) -> a -> m) -> (Term -> m) -> CCDone 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)
instance NFData a => NFData (CCDone a)