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

import Agda.Utils.Impossible

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

-- | Case tree with bodies.

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

type CompiledClauses = CompiledClauses' Term

litCase :: Literal -> c -> Case c
litCase :: forall c. Literal -> c -> Case c
litCase Literal
l c
x = forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
False forall k a. Map k a
Map.empty forall a. Maybe a
Nothing (forall k a. k -> a -> Map k a
Map.singleton Literal
l c
x) forall a. Maybe a
Nothing (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 = forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
False (forall k a. k -> a -> Map k a
Map.singleton QName
c WithArity c
x) forall a. Maybe a
Nothing forall k a. Map k a
Map.empty forall a. Maybe a
Nothing (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 = forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
False forall k a. Map k a
Map.empty (forall a. a -> Maybe a
Just (ConHead
c, WithArity c
x)) forall k a. Map k a
Map.empty forall a. Maybe a
Nothing (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 = forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
True (forall k a. k -> a -> Map k a
Map.singleton QName
c forall a b. (a -> b) -> a -> b
$ forall c. Int -> c -> WithArity c
WithArity Int
0 c
x) forall a. Maybe a
Nothing forall k a. Map k a
Map.empty forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just Bool
False) Bool
False

catchAll :: c -> Case c
catchAll :: forall c. c -> Case c
catchAll c
x = forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
False forall k a. Map k a
Map.empty forall a. Maybe a
Nothing forall k a. Map k a
Map.empty (forall a. a -> Maybe a
Just c
x) (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 :: Bool
lazyMatch = forall c. Case c -> Bool
lazyMatch Case c
b Bool -> Bool -> Bool
&& Bool
requirements }
  where
    requirements :: Bool
requirements = forall (t :: * -> *). Foldable t => t Bool -> Bool
and
      [ forall a. Null a => a -> Bool
null (forall c. Case c -> Maybe c
catchAllBranch Case c
b)
      , forall k a. Map k a -> Int
Map.size (forall c. Case c -> Map QName (WithArity c)
conBranches Case c
b) forall a. Ord a => a -> a -> Bool
<= Int
1
      , forall a. Null a => a -> Bool
null (forall c. Case c -> Map Literal c
litBranches Case c
b)
      , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. CompiledClauses' a -> Any
loop
  where
  loop :: CompiledClauses' a -> Any
loop CompiledClauses' a
cc = case CompiledClauses' a
cc of
    Fail{}    -> forall a. Monoid a => a
mempty
    Done{}    -> forall a. Monoid a => a
mempty
    Case Arg Int
_ Case (CompiledClauses' a)
br -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap CompiledClauses' a -> Any
loop Case (CompiledClauses' a)
br) (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True) forall a b. (a -> b) -> a -> b
$ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. CompiledClauses' a -> Any
loop
  where
  loop :: CompiledClauses' a -> Any
loop CompiledClauses' a
cc = case CompiledClauses' a
cc of
    Fail{}    -> forall a. Monoid a => a
mempty
    Done{}    -> forall a. Monoid a => a
mempty
    Case Arg Int
_ Case (CompiledClauses' a)
br -> Bool -> Any
Any (forall c. Case c -> Bool
projPatterns Case (CompiledClauses' a)
br) forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap CompiledClauses' a -> Any
loop Case (CompiledClauses' a)
br

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

instance (Semigroup c, Monoid c) => Monoid (WithArity c) where
  mempty :: WithArity c
mempty  = forall c. Int -> c -> WithArity c
WithArity forall a. HasCallStack => a
__IMPOSSIBLE__ forall a. Monoid a => a
mempty
  mappend :: WithArity c -> WithArity c -> WithArity c
mappend = 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' = forall c. Case c -> Case c
checkLazyMatch forall a b. (a -> b) -> a -> b
$
    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@
             (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>) Map QName (WithArity m)
cs Map QName (WithArity m)
cs')
             (forall {a}. Maybe a -> Maybe a -> Maybe a
unionEta Maybe (ConHead, WithArity m)
eta Maybe (ConHead, WithArity m)
eta')
             (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>) Map Literal m
ls Map Literal m
ls')
             (Maybe m
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') = forall a. a -> Maybe a
Just 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{} = forall a. HasCallStack => a
__IMPOSSIBLE__

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

instance Null (Case m) where
  empty :: Case m
empty = forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
False forall k a. Map k a
Map.empty forall a. Maybe a
Nothing forall k a. Map k a
Map.empty forall a. Maybe a
Nothing 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) = forall a. Null a => a -> Bool
null Map QName (WithArity m)
cs Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null Maybe (ConHead, WithArity m)
eta Bool -> Bool -> Bool
&& forall a. Null a => a -> Bool
null Map Literal m
ls Bool -> Bool -> 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 = forall a. Pretty a => a -> Doc
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$ forall {a}. (IsString a, Null a) => Bool -> a
prLazy Bool
lazy Doc -> Doc -> Doc
<+> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat (forall k v. (Pretty k, Pretty v) => Map k v -> [Doc]
prettyMap_ Map QName (WithArity a)
cs forall a. [a] -> [a] -> [a]
++ forall {a} {a}. (Pretty a, Pretty a) => Maybe (a, a) -> [Doc]
prEta Maybe (ConHead, WithArity a)
eta forall a. [a] -> [a] -> [a]
++ forall k v. (Pretty k, Pretty v) => Map k v -> [Doc]
prettyMap_ Map Literal a
ls forall a. [a] -> [a] -> [a]
++ forall {a}. Pretty a => Maybe a -> [Doc]
prC Maybe a
m)
    where
      prLazy :: Bool -> a
prLazy Bool
True  = a
"~"
      prLazy Bool
False = forall a. Null a => a
empty
      prC :: Maybe a -> [Doc]
prC Maybe a
Nothing = []
      prC (Just a
x) = [Doc
"_ ->" Doc -> Doc -> 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. Pretty a => a -> Doc
pretty a
c Doc -> Doc -> Doc
<+> Doc
"->") Doc -> Doc -> 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_ = forall a b. (a -> b) -> [a] -> [b]
map forall k v. (Pretty k, Pretty v) => (k, v) -> Doc
prettyAssign forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toList

instance Pretty CompiledClauses where
  pretty :: CompiledClauses -> Doc
pretty (Done [Arg ArgName]
hs Term
t) = (Doc
"done" forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
pretty [Arg ArgName]
hs) Doc -> Doc -> Doc
<?> forall a. Pretty a => a -> Doc
pretty Term
t
  pretty Fail{}      = Doc
"fail"
  pretty (Case Arg Int
n Case CompiledClauses
bs) | forall c. Case c -> Bool
projPatterns Case CompiledClauses
bs =
    forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"record"
        , Int -> Doc -> Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty Case CompiledClauses
bs
        ]
  pretty (Case Arg Int
n Case CompiledClauses
bs) =
    ArgName -> Doc
text (ArgName
"case " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow Arg Int
n forall a. [a] -> [a] -> [a]
++ ArgName
" of") Doc -> Doc -> 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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) = forall c.
Bool
-> Map QName (WithArity c)
-> Maybe (ConHead, WithArity c)
-> Map Literal c
-> Maybe c
-> Maybe Bool
-> Bool
-> Case c
Branches Bool
cop
    (forall k v. (KillRange k, KillRange v) => KillRangeT (Map k v)
killRangeMap Map QName (WithArity c)
con)
    (forall a. KillRange a => KillRangeT a
killRange Maybe (ConHead, WithArity c)
eta)
    (forall k v. (KillRange k, KillRange v) => KillRangeT (Map k v)
killRangeMap Map Literal c
lit)
    (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) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
i Case CompiledClauses
br
  killRange (Done [Arg ArgName]
xs Term
v) = forall a b c.
(KillRange a, KillRange b) =>
(a -> b -> c) -> a -> b -> c
killRange2 forall a. [Arg ArgName] -> a -> CompiledClauses' a
Done [Arg ArgName]
xs Term
v
  killRange (Fail [Arg ArgName]
xs)   = forall a b. KillRange a => (a -> b) -> a -> b
killRange1 forall a. [Arg ArgName] -> CompiledClauses' a
Fail [Arg ArgName]
xs

-- * TermLike instances

instance TermLike a => TermLike (WithArity a) where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> WithArity a -> m (WithArity a)
traverseTermM = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM
  foldTerm :: forall m. Monoid m => (Term -> m) -> WithArity a -> m
foldTerm      = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM
  foldTerm :: forall m. Monoid m => (Term -> m) -> Case a -> m
foldTerm      = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM
  foldTerm :: forall m. Monoid m => (Term -> m) -> CompiledClauses' a -> m
foldTerm      = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)