{-# OPTIONS_GHC -Wunused-imports #-}

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

module Agda.TypeChecking.CompiledClause where

import Prelude hiding (null)

import Control.DeepSeq

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

import GHC.Generics (Generic)

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

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

import Agda.Utils.Impossible

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

-- | Branches in a case tree.

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

-- | Case tree with bodies.

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

type CompiledClauses = CompiledClauses' Term

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- * Pretty instances.

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

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

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

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

-- * KillRange instances.

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

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

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

-- * TermLike instances

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

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

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

-- NFData instances

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