module Agda.TypeChecking.CompiledClause.Compile where

import Prelude hiding (null)

import Control.Applicative
import Control.Monad
import Control.Monad.Trans.Identity

import Data.Maybe
import qualified Data.Map as Map

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Monad
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Free.Precompute
import Agda.TypeChecking.Reduce

import Agda.Utils.Functor
import Agda.Utils.Maybe
import Agda.Utils.List
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Update

import Agda.Utils.Impossible

data RunRecordPatternTranslation = RunRecordPatternTranslation | DontRunRecordPatternTranslation
  deriving (RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
(RunRecordPatternTranslation
 -> RunRecordPatternTranslation -> Bool)
-> (RunRecordPatternTranslation
    -> RunRecordPatternTranslation -> Bool)
-> Eq RunRecordPatternTranslation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
$c/= :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
== :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
$c== :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
Eq)

compileClauses' :: RunRecordPatternTranslation -> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
compileClauses' :: RunRecordPatternTranslation
-> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
compileClauses' RunRecordPatternTranslation
recpat [Clause]
cs Maybe SplitTree
mSplitTree = do

  -- Throw away the unreachable clauses (#2723).
  let notUnreachable :: Clause -> Bool
notUnreachable = (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseUnreachable
  [Cl]
cs <- (Clause -> Cl) -> [Clause] -> [Cl]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Cl
unBruijn ([Clause] -> [Cl]) -> TCMT IO [Clause] -> TCMT IO [Cl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Clause] -> TCMT IO [Clause]
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP ((Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
filter Clause -> Bool
notUnreachable [Clause]
cs)

  let translate :: CompiledClauses -> TCM CompiledClauses
translate | RunRecordPatternTranslation
recpat RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool
forall a. Eq a => a -> a -> Bool
== RunRecordPatternTranslation
RunRecordPatternTranslation = IdentityT (TCMT IO) CompiledClauses -> TCM CompiledClauses
forall k (f :: k -> *) (a :: k). IdentityT f a -> f a
runIdentityT (IdentityT (TCMT IO) CompiledClauses -> TCM CompiledClauses)
-> (CompiledClauses -> IdentityT (TCMT IO) CompiledClauses)
-> CompiledClauses
-> TCM CompiledClauses
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompiledClauses -> IdentityT (TCMT IO) CompiledClauses
forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
translateCompiledClauses
                | Bool
otherwise                             = CompiledClauses -> TCM CompiledClauses
forall (m :: * -> *) a. Monad m => a -> m a
return

  CompiledClauses -> TCM CompiledClauses
translate (CompiledClauses -> TCM CompiledClauses)
-> CompiledClauses -> TCM CompiledClauses
forall a b. (a -> b) -> a -> b
$ Maybe SplitTree
-> CompiledClauses
-> (SplitTree -> CompiledClauses)
-> CompiledClauses
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe SplitTree
mSplitTree ([Cl] -> CompiledClauses
compile [Cl]
cs) ((SplitTree -> CompiledClauses) -> CompiledClauses)
-> (SplitTree -> CompiledClauses) -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ \SplitTree
splitTree ->
    SplitTree -> [Cl] -> CompiledClauses
compileWithSplitTree SplitTree
splitTree [Cl]
cs

-- | Process function clauses into case tree.
--   This involves:
--   1. Coverage checking, generating a split tree.
--   2. Translation of lhs record patterns into rhs uses of projection.
--      Update the split tree.
--   3. Generating a case tree from the split tree.
--   Phases 1. and 2. are skipped if @Nothing@.
compileClauses ::
  Maybe (QName, Type) -- ^ Translate record patterns and coverage check with given type?
  -> [Clause]
  -> TCM (Maybe SplitTree, Bool, CompiledClauses)
     -- ^ The 'Bool' indicates whether we turned a record expression into a copattern match.
compileClauses :: Maybe (QName, Type)
-> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
compileClauses Maybe (QName, Type)
mt [Clause]
cs = do
  -- Construct clauses with pattern variables bound in left-to-right order.
  -- Discard de Bruijn indices in patterns.
  case Maybe (QName, Type)
mt of
    Maybe (QName, Type)
Nothing -> (Maybe SplitTree
forall a. Maybe a
Nothing,Bool
False,) (CompiledClauses -> (Maybe SplitTree, Bool, CompiledClauses))
-> ([Clause] -> CompiledClauses)
-> [Clause]
-> (Maybe SplitTree, Bool, CompiledClauses)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Cl] -> CompiledClauses
compile ([Cl] -> CompiledClauses)
-> ([Clause] -> [Cl]) -> [Clause] -> CompiledClauses
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> Cl) -> [Clause] -> [Cl]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Cl
unBruijn ([Clause] -> (Maybe SplitTree, Bool, CompiledClauses))
-> TCMT IO [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Clause] -> TCMT IO [Clause]
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP [Clause]
cs
    Just (QName
q, Type
t)  -> do
      SplitTree
splitTree <- QName -> Type -> [Clause] -> TCM SplitTree
coverageCheck QName
q Type
t [Clause]
cs

      VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc.tree" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCM Doc
"split tree of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" from coverage check "
        , Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ SplitTree -> Doc
forall a. Pretty a => a -> Doc
P.pretty SplitTree
splitTree
        ]

      -- The coverage checker might have added some clauses (#2288)!
      -- Throw away the unreachable clauses (#2723).
      let notUnreachable :: Clause -> Bool
notUnreachable = (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/=) (Maybe Bool -> Bool) -> (Clause -> Maybe Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseUnreachable
      [Clause]
cs <- [Clause] -> TCMT IO [Clause]
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP ([Clause] -> TCMT IO [Clause])
-> TCMT IO [Clause] -> TCMT IO [Clause]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Clause] -> TCMT IO [Clause]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ([Clause] -> TCMT IO [Clause])
-> TCMT IO [Clause] -> TCMT IO [Clause]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
filter Clause -> Bool
notUnreachable ([Clause] -> [Clause])
-> (Definition -> [Clause]) -> Definition -> [Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> [Clause]
defClauses (Definition -> [Clause]) -> TCMT IO Definition -> TCMT IO [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q

      let cls :: [Cl]
cls = (Clause -> Cl) -> [Clause] -> [Cl]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Cl
unBruijn [Clause]
cs

      VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc" VerboseLevel
30 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
        (TCM Doc
"clauses patterns of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" before compilation") TCM Doc -> [TCM Doc] -> [TCM Doc]
forall a. a -> [a] -> [a]
: do
          (Cl -> TCM Doc) -> [Cl] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Pattern] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Pattern] -> TCM Doc) -> (Cl -> [Pattern]) -> Cl -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Pattern -> Pattern) -> [Arg Pattern] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map Arg Pattern -> Pattern
forall e. Arg e -> e
unArg ([Arg Pattern] -> [Pattern])
-> (Cl -> [Arg Pattern]) -> Cl -> [Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cl -> [Arg Pattern]
clPats) [Cl]
cls
      VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"clauses of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" before compilation" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [Clause] -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Clause]
cs
      let cc :: CompiledClauses
cc = SplitTree -> [Cl] -> CompiledClauses
compileWithSplitTree SplitTree
splitTree [Cl]
cls
      VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCM Doc
"compiled clauses of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" (still containing record splits)"
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ CompiledClauses -> Doc
forall a. Pretty a => a -> Doc
P.pretty CompiledClauses
cc
        ]
      (CompiledClauses
cc, Bool
becameCopatternLHS) <- ChangeT (TCMT IO) CompiledClauses
-> TCMT IO (CompiledClauses, Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT (TCMT IO) CompiledClauses
 -> TCMT IO (CompiledClauses, Bool))
-> ChangeT (TCMT IO) CompiledClauses
-> TCMT IO (CompiledClauses, Bool)
forall a b. (a -> b) -> a -> b
$ CompiledClauses -> ChangeT (TCMT IO) CompiledClauses
forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
translateCompiledClauses CompiledClauses
cc
      VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc" VerboseLevel
12 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCM Doc
"compiled clauses of " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ CompiledClauses -> Doc
forall a. Pretty a => a -> Doc
P.pretty CompiledClauses
cc
        ]
      (Maybe SplitTree, Bool, CompiledClauses)
-> TCM (Maybe SplitTree, Bool, CompiledClauses)
forall (m :: * -> *) a. Monad m => a -> m a
return (SplitTree -> Maybe SplitTree
forall a. a -> Maybe a
Just SplitTree
splitTree, Bool
becameCopatternLHS, (Term -> Term) -> CompiledClauses -> CompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ CompiledClauses
cc)

-- | Stripped-down version of 'Agda.Syntax.Internal.Clause'
--   used in clause compiler.
data Cl = Cl
  { Cl -> [Arg Pattern]
clPats :: [Arg Pattern]
      -- ^ Pattern variables are considered in left-to-right order.
  , Cl -> Maybe Term
clBody :: Maybe Term
  } deriving (VerboseLevel -> Cl -> ShowS
[Cl] -> ShowS
Cl -> VerboseKey
(VerboseLevel -> Cl -> ShowS)
-> (Cl -> VerboseKey) -> ([Cl] -> ShowS) -> Show Cl
forall a.
(VerboseLevel -> a -> ShowS)
-> (a -> VerboseKey) -> ([a] -> ShowS) -> Show a
showList :: [Cl] -> ShowS
$cshowList :: [Cl] -> ShowS
show :: Cl -> VerboseKey
$cshow :: Cl -> VerboseKey
showsPrec :: VerboseLevel -> Cl -> ShowS
$cshowsPrec :: VerboseLevel -> Cl -> ShowS
Show)

instance P.Pretty Cl where
  pretty :: Cl -> Doc
pretty (Cl [Arg Pattern]
ps Maybe Term
b) = [Arg Pattern] -> Doc
forall a. Pretty a => [a] -> Doc
P.prettyList [Arg Pattern]
ps Doc -> Doc -> Doc
P.<+> Doc
"->" Doc -> Doc -> Doc
P.<+> Doc -> (Term -> Doc) -> Maybe Term -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"_|_" Term -> Doc
forall a. Pretty a => a -> Doc
P.pretty Maybe Term
b

type Cls = [Cl]

-- | Strip down a clause. Don't forget to apply the substitution to the dot
--   patterns!
unBruijn :: Clause -> Cl
unBruijn :: Clause -> Cl
unBruijn Clause
c = [Arg Pattern] -> Maybe Term -> Cl
Cl (Substitution' (SubstArg [Arg Pattern])
-> [Arg Pattern] -> [Arg Pattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [Arg Pattern])
sub ([Arg Pattern] -> [Arg Pattern]) -> [Arg Pattern] -> [Arg Pattern]
forall a b. (a -> b) -> a -> b
$ ((Arg (Named NamedName (Pattern' DBPatVar)) -> Arg Pattern)
-> [Arg (Named NamedName (Pattern' DBPatVar))] -> [Arg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Arg (Named NamedName (Pattern' DBPatVar)) -> Arg Pattern)
 -> [Arg (Named NamedName (Pattern' DBPatVar))] -> [Arg Pattern])
-> ((Named NamedName (Pattern' DBPatVar) -> Pattern)
    -> Arg (Named NamedName (Pattern' DBPatVar)) -> Arg Pattern)
-> (Named NamedName (Pattern' DBPatVar) -> Pattern)
-> [Arg (Named NamedName (Pattern' DBPatVar))]
-> [Arg Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (Pattern' DBPatVar) -> Pattern)
-> Arg (Named NamedName (Pattern' DBPatVar)) -> Arg Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ((DBPatVar -> VerboseKey) -> Pattern' DBPatVar -> Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DBPatVar -> VerboseKey
dbPatVarName (Pattern' DBPatVar -> Pattern)
-> (Named NamedName (Pattern' DBPatVar) -> Pattern' DBPatVar)
-> Named NamedName (Pattern' DBPatVar)
-> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named NamedName (Pattern' DBPatVar) -> Pattern' DBPatVar
forall name a. Named name a -> a
namedThing) ([Arg (Named NamedName (Pattern' DBPatVar))] -> [Arg Pattern])
-> [Arg (Named NamedName (Pattern' DBPatVar))] -> [Arg Pattern]
forall a b. (a -> b) -> a -> b
$ Clause -> [Arg (Named NamedName (Pattern' DBPatVar))]
namedClausePats Clause
c)
                (Substitution' (SubstArg (Maybe Term)) -> Maybe Term -> Maybe Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Maybe Term))
sub (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
c)
  where
    sub :: Substitution' Term
sub = Permutation -> Substitution' Term
forall a. DeBruijn a => Permutation -> Substitution' a
renamingR (Permutation -> Substitution' Term)
-> Permutation -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Clause -> Maybe Permutation
clausePerm Clause
c)

compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses
compileWithSplitTree :: SplitTree -> [Cl] -> CompiledClauses
compileWithSplitTree SplitTree
t [Cl]
cs = case SplitTree
t of
  SplitAt Arg VerboseLevel
i LazySplit
lz SplitTrees' SplitTag
ts -> Arg VerboseLevel -> Case CompiledClauses -> CompiledClauses
forall a.
Arg VerboseLevel -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg VerboseLevel
i (Case CompiledClauses -> CompiledClauses)
-> Case CompiledClauses -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ LazySplit
-> SplitTrees' SplitTag -> Case [Cl] -> Case CompiledClauses
compiles LazySplit
lz SplitTrees' SplitTag
ts (Case [Cl] -> Case CompiledClauses)
-> Case [Cl] -> Case CompiledClauses
forall a b. (a -> b) -> a -> b
$ Bool -> VerboseLevel -> [Cl] -> Case [Cl]
splitOn (SplitTrees' SplitTag -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length SplitTrees' SplitTag
ts VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
1) (Arg VerboseLevel -> VerboseLevel
forall e. Arg e -> e
unArg Arg VerboseLevel
i) [Cl]
cs
        -- if there is just one case, we force expansion of catch-alls
        -- this is needed to generate a sound tree on which we can
        -- collapse record pattern splits
  SplittingDone VerboseLevel
n -> [Cl] -> CompiledClauses
compile [Cl]
cs
    -- after end of split tree, continue with left-to-right strategy

  where
    compiles :: LazySplit -> SplitTrees -> Case Cls -> Case CompiledClauses
    compiles :: LazySplit
-> SplitTrees' SplitTag -> Case [Cl] -> Case CompiledClauses
compiles LazySplit
lz SplitTrees' SplitTag
ts br :: Case [Cl]
br@Branches{ projPatterns :: forall c. Case c -> Bool
projPatterns = Bool
cop
                              , conBranches :: forall c. Case c -> Map QName (WithArity c)
conBranches = Map QName (WithArity [Cl])
cons
                              , etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
etaBranch   = Maybe (ConHead, WithArity [Cl])
Nothing
                              , litBranches :: forall c. Case c -> Map Literal c
litBranches = Map Literal [Cl]
lits
                              , fallThrough :: forall c. Case c -> Maybe Bool
fallThrough = Maybe Bool
fT
                              , catchAllBranch :: forall c. Case c -> Maybe c
catchAllBranch = Maybe [Cl]
catchAll
                              , lazyMatch :: forall c. Case c -> Bool
lazyMatch = Bool
lazy }
      = Case [Cl]
br{ conBranches :: Map QName (WithArity CompiledClauses)
conBranches    = Map QName (WithArity [Cl]) -> Map QName (WithArity CompiledClauses)
updCons Map QName (WithArity [Cl])
cons
          , etaBranch :: Maybe (ConHead, WithArity CompiledClauses)
etaBranch      = Maybe (ConHead, WithArity CompiledClauses)
forall a. Maybe a
Nothing
          , litBranches :: Map Literal CompiledClauses
litBranches    = Map Literal [Cl] -> Map Literal CompiledClauses
updLits Map Literal [Cl]
lits
          , fallThrough :: Maybe Bool
fallThrough    = Maybe Bool
fT
          , catchAllBranch :: Maybe CompiledClauses
catchAllBranch = Maybe [Cl] -> Maybe CompiledClauses
updCatchall Maybe [Cl]
catchAll
          , lazyMatch :: Bool
lazyMatch      = Bool
lazy Bool -> Bool -> Bool
|| LazySplit
lz LazySplit -> LazySplit -> Bool
forall a. Eq a => a -> a -> Bool
== LazySplit
LazySplit
          }
      where
        updCons :: Map QName (WithArity [Cl]) -> Map QName (WithArity CompiledClauses)
updCons = (QName -> WithArity [Cl] -> WithArity CompiledClauses)
-> Map QName (WithArity [Cl])
-> Map QName (WithArity CompiledClauses)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey ((QName -> WithArity [Cl] -> WithArity CompiledClauses)
 -> Map QName (WithArity [Cl])
 -> Map QName (WithArity CompiledClauses))
-> (QName -> WithArity [Cl] -> WithArity CompiledClauses)
-> Map QName (WithArity [Cl])
-> Map QName (WithArity CompiledClauses)
forall a b. (a -> b) -> a -> b
$ \ QName
c WithArity [Cl]
cl ->
         Maybe SplitTree
-> ([Cl] -> CompiledClauses)
-> (SplitTree -> [Cl] -> CompiledClauses)
-> [Cl]
-> CompiledClauses
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (SplitTag -> SplitTrees' SplitTag -> Maybe SplitTree
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (QName -> SplitTag
SplitCon QName
c) SplitTrees' SplitTag
ts) [Cl] -> CompiledClauses
compile SplitTree -> [Cl] -> CompiledClauses
compileWithSplitTree ([Cl] -> CompiledClauses)
-> WithArity [Cl] -> WithArity CompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WithArity [Cl]
cl
         -- When the split tree is finished, we continue with @compile@.
        updLits :: Map Literal [Cl] -> Map Literal CompiledClauses
updLits = (Literal -> [Cl] -> CompiledClauses)
-> Map Literal [Cl] -> Map Literal CompiledClauses
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey ((Literal -> [Cl] -> CompiledClauses)
 -> Map Literal [Cl] -> Map Literal CompiledClauses)
-> (Literal -> [Cl] -> CompiledClauses)
-> Map Literal [Cl]
-> Map Literal CompiledClauses
forall a b. (a -> b) -> a -> b
$ \ Literal
l [Cl]
cl ->
          Maybe SplitTree
-> ([Cl] -> CompiledClauses)
-> (SplitTree -> [Cl] -> CompiledClauses)
-> [Cl]
-> CompiledClauses
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (SplitTag -> SplitTrees' SplitTag -> Maybe SplitTree
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Literal -> SplitTag
SplitLit Literal
l) SplitTrees' SplitTag
ts) [Cl] -> CompiledClauses
compile SplitTree -> [Cl] -> CompiledClauses
compileWithSplitTree [Cl]
cl
        updCatchall :: Maybe [Cl] -> Maybe CompiledClauses
updCatchall = ([Cl] -> CompiledClauses) -> Maybe [Cl] -> Maybe CompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Cl] -> CompiledClauses) -> Maybe [Cl] -> Maybe CompiledClauses)
-> ([Cl] -> CompiledClauses) -> Maybe [Cl] -> Maybe CompiledClauses
forall a b. (a -> b) -> a -> b
$ Maybe SplitTree
-> ([Cl] -> CompiledClauses)
-> (SplitTree -> [Cl] -> CompiledClauses)
-> [Cl]
-> CompiledClauses
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (SplitTag -> SplitTrees' SplitTag -> Maybe SplitTree
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup SplitTag
SplitCatchall SplitTrees' SplitTag
ts) [Cl] -> CompiledClauses
compile SplitTree -> [Cl] -> CompiledClauses
compileWithSplitTree
    compiles LazySplit
_ SplitTrees' SplitTag
_ Branches{etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
etaBranch = Just{}} = Case CompiledClauses
forall a. HasCallStack => a
__IMPOSSIBLE__  -- we haven't inserted eta matches yet

compile :: Cls -> CompiledClauses
compile :: [Cl] -> CompiledClauses
compile [] = [Arg VerboseKey] -> CompiledClauses
forall a. [Arg VerboseKey] -> CompiledClauses' a
Fail []
compile [Cl]
cs = case [Cl] -> Maybe (Bool, Arg VerboseLevel)
nextSplit [Cl]
cs of
  Just (Bool
isRecP, Arg VerboseLevel
n) -> Arg VerboseLevel -> Case CompiledClauses -> CompiledClauses
forall a.
Arg VerboseLevel -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg VerboseLevel
n (Case CompiledClauses -> CompiledClauses)
-> Case CompiledClauses -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ [Cl] -> CompiledClauses
compile ([Cl] -> CompiledClauses) -> Case [Cl] -> Case CompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> VerboseLevel -> [Cl] -> Case [Cl]
splitOn Bool
isRecP (Arg VerboseLevel -> VerboseLevel
forall e. Arg e -> e
unArg Arg VerboseLevel
n) [Cl]
cs
  Maybe (Bool, Arg VerboseLevel)
Nothing -> case Cl -> Maybe Term
clBody Cl
c of
    -- It's possible to get more than one clause here due to
    -- catch-all expansion.
    Just Term
t  -> [Arg VerboseKey] -> Term -> CompiledClauses
forall a. [Arg VerboseKey] -> a -> CompiledClauses' a
Done ((Arg Pattern -> Arg VerboseKey)
-> [Arg Pattern] -> [Arg VerboseKey]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern -> VerboseKey) -> Arg Pattern -> Arg VerboseKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> VerboseKey
forall p. Underscore p => Pattern' p -> p
name) ([Arg Pattern] -> [Arg VerboseKey])
-> [Arg Pattern] -> [Arg VerboseKey]
forall a b. (a -> b) -> a -> b
$ Cl -> [Arg Pattern]
clPats Cl
c) Term
t
    Maybe Term
Nothing -> [Arg VerboseKey] -> CompiledClauses
forall a. [Arg VerboseKey] -> CompiledClauses' a
Fail ((Arg Pattern -> Arg VerboseKey)
-> [Arg Pattern] -> [Arg VerboseKey]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern -> VerboseKey) -> Arg Pattern -> Arg VerboseKey
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> VerboseKey
forall p. Underscore p => Pattern' p -> p
name) ([Arg Pattern] -> [Arg VerboseKey])
-> [Arg Pattern] -> [Arg VerboseKey]
forall a b. (a -> b) -> a -> b
$ Cl -> [Arg Pattern]
clPats Cl
c)
  where
    -- If there are more than one clauses, take the first one.
    c :: Cl
c = Cl -> [Cl] -> Cl
forall a. a -> [a] -> a
headWithDefault Cl
forall a. HasCallStack => a
__IMPOSSIBLE__ [Cl]
cs
    name :: Pattern' p -> p
name (VarP PatternInfo
_ p
x) = p
x
    name (DotP PatternInfo
_ Term
_) = p
forall a. Underscore a => a
underscore
    name ConP{}  = p
forall a. HasCallStack => a
__IMPOSSIBLE__
    name DefP{}  = p
forall a. HasCallStack => a
__IMPOSSIBLE__
    name LitP{}  = p
forall a. HasCallStack => a
__IMPOSSIBLE__
    name ProjP{} = p
forall a. HasCallStack => a
__IMPOSSIBLE__
    name (IApplyP PatternInfo
_ Term
_ Term
_ p
x) = p
x

-- | Get the index of the next argument we need to split on.
--   This the number of the first pattern that does a (non-lazy) match in the first clause.
--   Or the first lazy match where all clauses agree on the constructor, if there are no
--   non-lazy matches.
nextSplit :: Cls -> Maybe (Bool, Arg Int)
nextSplit :: [Cl] -> Maybe (Bool, Arg VerboseLevel)
nextSplit []             = Maybe (Bool, Arg VerboseLevel)
forall a. HasCallStack => a
__IMPOSSIBLE__
nextSplit (Cl [Arg Pattern]
ps Maybe Term
_ : [Cl]
cs) = (VerboseLevel -> Pattern -> Bool)
-> [Arg Pattern] -> Maybe (Bool, Arg VerboseLevel)
forall t a.
(Num t, Enum t) =>
(t -> Pattern' a -> Bool)
-> [Arg (Pattern' a)] -> Maybe (Bool, Arg t)
findSplit VerboseLevel -> Pattern -> Bool
forall p x. p -> Pattern' x -> Bool
nonLazy [Arg Pattern]
ps Maybe (Bool, Arg VerboseLevel)
-> Maybe (Bool, Arg VerboseLevel) -> Maybe (Bool, Arg VerboseLevel)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (VerboseLevel -> Pattern -> Bool)
-> [Arg Pattern] -> Maybe (Bool, Arg VerboseLevel)
forall t a.
(Num t, Enum t) =>
(t -> Pattern' a -> Bool)
-> [Arg (Pattern' a)] -> Maybe (Bool, Arg t)
findSplit VerboseLevel -> Pattern -> Bool
allAgree [Arg Pattern]
ps
  where
    nonLazy :: p -> Pattern' x -> Bool
nonLazy p
_ (ConP ConHead
_ ConPatternInfo
cpi [NamedArg (Pattern' x)]
_) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Bool
conPLazy ConPatternInfo
cpi
    nonLazy p
_ Pattern' x
_              = Bool
True

    findSplit :: (t -> Pattern' a -> Bool)
-> [Arg (Pattern' a)] -> Maybe (Bool, Arg t)
findSplit t -> Pattern' a -> Bool
okPat [Arg (Pattern' a)]
ps = [(Bool, Arg t)] -> Maybe (Bool, Arg t)
forall a. [a] -> Maybe a
listToMaybe ([Maybe (Bool, Arg t)] -> [(Bool, Arg t)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Bool, Arg t)] -> [(Bool, Arg t)])
-> [Maybe (Bool, Arg t)] -> [(Bool, Arg t)]
forall a b. (a -> b) -> a -> b
$
      (Arg (Pattern' a) -> t -> Maybe (Bool, Arg t))
-> [Arg (Pattern' a)] -> [t] -> [Maybe (Bool, Arg t)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ (Arg ArgInfo
ai Pattern' a
p) t
n -> (, ArgInfo -> t -> Arg t
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai t
n) (Bool -> (Bool, Arg t)) -> Maybe Bool -> Maybe (Bool, Arg t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern' a -> Maybe Bool
forall a. Pattern' a -> Maybe Bool
properSplit Pattern' a
p Maybe (Bool, Arg t) -> Maybe () -> Maybe (Bool, Arg t)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t -> Pattern' a -> Bool
okPat t
n Pattern' a
p)) [Arg (Pattern' a)]
ps [t
0..])

    allAgree :: VerboseLevel -> Pattern -> Bool
allAgree VerboseLevel
i (ConP ConHead
c ConPatternInfo
_ [NamedArg Pattern]
_) = (Cl -> Bool) -> [Cl] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
c)) (Maybe QName -> Bool) -> (Cl -> Maybe QName) -> Cl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pattern] -> Maybe QName
forall x. [Pattern' x] -> Maybe QName
getCon ([Pattern] -> Maybe QName)
-> (Cl -> [Pattern]) -> Cl -> Maybe QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Pattern -> Pattern) -> [Arg Pattern] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map Arg Pattern -> Pattern
forall e. Arg e -> e
unArg ([Arg Pattern] -> [Pattern])
-> (Cl -> [Arg Pattern]) -> Cl -> [Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> [Arg Pattern] -> [Arg Pattern]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
i ([Arg Pattern] -> [Arg Pattern])
-> (Cl -> [Arg Pattern]) -> Cl -> [Arg Pattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cl -> [Arg Pattern]
clPats) [Cl]
cs
    allAgree VerboseLevel
_ Pattern
_            = Bool
False

    getCon :: [Pattern' x] -> Maybe QName
getCon (ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' x)]
_ : [Pattern' x]
_) = QName -> Maybe QName
forall a. a -> Maybe a
Just (QName -> Maybe QName) -> QName -> Maybe QName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
    getCon [Pattern' x]
_                = Maybe QName
forall a. Maybe a
Nothing

-- | Is is not a variable pattern?
--   And if yes, is it a record pattern and/or a fallThrough one?
properSplit :: Pattern' a -> Maybe Bool
properSplit :: Pattern' a -> Maybe Bool
properSplit (ConP ConHead
_ ConPatternInfo
cpi [NamedArg (Pattern' a)]
_) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just ((ConPatternInfo -> Bool
conPRecord ConPatternInfo
cpi Bool -> Bool -> Bool
&& PatternInfo -> PatOrigin
patOrigin (ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) PatOrigin -> PatOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== PatOrigin
PatORec) Bool -> Bool -> Bool
|| ConPatternInfo -> Bool
conPFallThrough ConPatternInfo
cpi)
properSplit DefP{}    = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
properSplit LitP{}    = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
properSplit ProjP{}   = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
properSplit IApplyP{} = Maybe Bool
forall a. Maybe a
Nothing
properSplit VarP{}    = Maybe Bool
forall a. Maybe a
Nothing
properSplit DotP{}    = Maybe Bool
forall a. Maybe a
Nothing

-- | Is this a variable pattern?
--
--   Maintain invariant: @isVar = isNothing . properSplit@!
isVar :: Pattern' a -> Bool
isVar :: Pattern' a -> Bool
isVar IApplyP{} = Bool
True
isVar VarP{}    = Bool
True
isVar DotP{}    = Bool
True
isVar ConP{}    = Bool
False
isVar DefP{}    = Bool
False
isVar LitP{}    = Bool
False
isVar ProjP{}   = Bool
False

-- | @splitOn single n cs@ will force expansion of catch-alls
--   if @single@.
splitOn :: Bool -> Int -> Cls -> Case Cls
splitOn :: Bool -> VerboseLevel -> [Cl] -> Case [Cl]
splitOn Bool
single VerboseLevel
n [Cl]
cs = [Case [Cl]] -> Case [Cl]
forall a. Monoid a => [a] -> a
mconcat ([Case [Cl]] -> Case [Cl]) -> [Case [Cl]] -> Case [Cl]
forall a b. (a -> b) -> a -> b
$ (Cl -> Case [Cl]) -> [Cl] -> [Case [Cl]]
forall a b. (a -> b) -> [a] -> [b]
map ((Cl -> [Cl]) -> Case Cl -> Case [Cl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cl -> [Cl] -> [Cl]
forall a. a -> [a] -> [a]
:[]) (Case Cl -> Case [Cl]) -> (Cl -> Case Cl) -> Cl -> Case [Cl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> Cl -> Case Cl
splitC VerboseLevel
n) ([Cl] -> [Case [Cl]]) -> [Cl] -> [Case [Cl]]
forall a b. (a -> b) -> a -> b
$
  -- (\ cs -> trace ("splitting on " ++ show n ++ " after expandCatchAlls " ++ show single ++ ": " ++ prettyShow (P.prettyList cs)) cs) $
    Bool -> VerboseLevel -> [Cl] -> [Cl]
expandCatchAlls Bool
single VerboseLevel
n [Cl]
cs

splitC :: Int -> Cl -> Case Cl
splitC :: VerboseLevel -> Cl -> Case Cl
splitC VerboseLevel
n (Cl [Arg Pattern]
ps Maybe Term
b) = Maybe Pattern -> Case Cl -> (Pattern -> Case Cl) -> Case Cl
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Pattern
mp Case Cl
fallback ((Pattern -> Case Cl) -> Case Cl)
-> (Pattern -> Case Cl) -> Case Cl
forall a b. (a -> b) -> a -> b
$ \case
  ProjP ProjOrigin
_ QName
d   -> QName -> Cl -> Case Cl
forall c. QName -> c -> Case c
projCase QName
d (Cl -> Case Cl) -> Cl -> Case Cl
forall a b. (a -> b) -> a -> b
$ [Arg Pattern] -> Maybe Term -> Cl
Cl ([Arg Pattern]
ps0 [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern]
ps1) Maybe Term
b
  IApplyP{}   -> Case Cl
fallback
  ConP ConHead
c ConPatternInfo
i [NamedArg Pattern]
qs -> (QName -> Bool -> WithArity Cl -> Case Cl
forall c. QName -> Bool -> WithArity c -> Case c
conCase (ConHead -> QName
conName ConHead
c) (ConPatternInfo -> Bool
conPFallThrough ConPatternInfo
i) (WithArity Cl -> Case Cl) -> WithArity Cl -> Case Cl
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Cl -> WithArity Cl
forall c. VerboseLevel -> c -> WithArity c
WithArity ([NamedArg Pattern] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [NamedArg Pattern]
qs) (Cl -> WithArity Cl) -> Cl -> WithArity Cl
forall a b. (a -> b) -> a -> b
$
                   [Arg Pattern] -> Maybe Term -> Cl
Cl ([Arg Pattern]
ps0 [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ (NamedArg Pattern -> Arg Pattern)
-> [NamedArg Pattern] -> [Arg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName Pattern -> Pattern)
-> NamedArg Pattern -> Arg Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName Pattern -> Pattern
forall name a. Named name a -> a
namedThing) [NamedArg Pattern]
qs [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern]
ps1) Maybe Term
b) { lazyMatch :: Bool
lazyMatch = ConPatternInfo -> Bool
conPLazy ConPatternInfo
i }
  DefP PatternInfo
o QName
q [NamedArg Pattern]
qs -> (QName -> Bool -> WithArity Cl -> Case Cl
forall c. QName -> Bool -> WithArity c -> Case c
conCase QName
q Bool
False (WithArity Cl -> Case Cl) -> WithArity Cl -> Case Cl
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Cl -> WithArity Cl
forall c. VerboseLevel -> c -> WithArity c
WithArity ([NamedArg Pattern] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [NamedArg Pattern]
qs) (Cl -> WithArity Cl) -> Cl -> WithArity Cl
forall a b. (a -> b) -> a -> b
$
                   [Arg Pattern] -> Maybe Term -> Cl
Cl ([Arg Pattern]
ps0 [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ (NamedArg Pattern -> Arg Pattern)
-> [NamedArg Pattern] -> [Arg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName Pattern -> Pattern)
-> NamedArg Pattern -> Arg Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName Pattern -> Pattern
forall name a. Named name a -> a
namedThing) [NamedArg Pattern]
qs [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern]
ps1) Maybe Term
b) { lazyMatch :: Bool
lazyMatch = Bool
False }
  LitP PatternInfo
_ Literal
l    -> Literal -> Cl -> Case Cl
forall c. Literal -> c -> Case c
litCase Literal
l (Cl -> Case Cl) -> Cl -> Case Cl
forall a b. (a -> b) -> a -> b
$ [Arg Pattern] -> Maybe Term -> Cl
Cl ([Arg Pattern]
ps0 [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern]
ps1) Maybe Term
b
  VarP{}      -> Case Cl
fallback
  DotP{}      -> Case Cl
fallback
  where
    ([Arg Pattern]
ps0, [Arg Pattern]
rest) = VerboseLevel -> [Arg Pattern] -> ([Arg Pattern], [Arg Pattern])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
n [Arg Pattern]
ps
    mp :: Maybe Pattern
mp          = Arg Pattern -> Pattern
forall e. Arg e -> e
unArg (Arg Pattern -> Pattern) -> Maybe (Arg Pattern) -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Pattern] -> Maybe (Arg Pattern)
forall a. [a] -> Maybe a
listToMaybe [Arg Pattern]
rest
    ps1 :: [Arg Pattern]
ps1         = VerboseLevel -> [Arg Pattern] -> [Arg Pattern]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
1 [Arg Pattern]
rest
    fallback :: Case Cl
fallback    = Cl -> Case Cl
forall c. c -> Case c
catchAll (Cl -> Case Cl) -> Cl -> Case Cl
forall a b. (a -> b) -> a -> b
$ [Arg Pattern] -> Maybe Term -> Cl
Cl [Arg Pattern]
ps Maybe Term
b

-- | Expand catch-alls that appear before actual matches.
--
-- Example:
--
-- @
--    true  y
--    x     false
--    false y
-- @
--
-- will expand the catch-all @x@ to @false@.
--
-- Catch-alls need also to be expanded if
-- they come before/after a record pattern, otherwise we get into
-- trouble when we want to eliminate splits on records later.
--
-- Another example (see Issue 1650):
-- @
--   f (x, (y, z)) true  = a
--   f _           false = b
-- @
-- Split tree:
-- @
--   0 (first argument of f)
--    \- 1 (second component of the pair)
--        \- 3 (last argument of f)
--            \-- true  -> a
--             \- false -> b
-- @
-- We would like to get the following case tree:
-- @
--   case 0 of
--   _,_ -> case 1 of
--          _,_ -> case 3 of true  -> a; false -> b
--          _   -> case 3 of true  -> a; false -> b
--   _          -> case 3 of true  -> a; false -> b
-- @
--
-- Example from issue #2168:
-- @
--   f x     false = a
--   f false       = \ _ -> b
--   f x     true  = c
-- @
-- case tree:
-- @
--   f x y = case y of
--     true  -> case x of
--       true  -> c
--       false -> b
--     false -> a
-- @
--
-- Example from issue #3628:
-- @
--   f i j k (i = i0)(k = i1) = base
--   f i j k (j = i1)         = base
-- @
-- case tree:
-- @
--   f i j k o = case i of
--     i0 -> case k of
--             i1 -> base
--             _  -> case j of
--                     i1 -> base
--     _  -> case j of
--             i1 -> base
-- @
expandCatchAlls :: Bool -> Int -> Cls -> Cls
expandCatchAlls :: Bool -> VerboseLevel -> [Cl] -> [Cl]
expandCatchAlls Bool
single VerboseLevel
n [Cl]
cs =
  -- Andreas, 2013-03-22
  -- if there is a single case (such as for record splits)
  -- we force expansion
  if Bool
single then Cl -> [Cl]
doExpand (Cl -> [Cl]) -> [Cl] -> [Cl]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Cl]
cs else
  case [Cl]
cs of
  [Cl]
_                | (Cl -> Bool) -> [Cl] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Arg Pattern] -> Bool
isCatchAllNth ([Arg Pattern] -> Bool) -> (Cl -> [Arg Pattern]) -> Cl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cl -> [Arg Pattern]
clPats) [Cl]
cs -> [Cl]
cs
  c :: Cl
c@(Cl [Arg Pattern]
ps Maybe Term
b) : [Cl]
cs | Bool -> Bool
not ([Arg Pattern] -> Bool
isCatchAllNth [Arg Pattern]
ps) -> Cl
c Cl -> [Cl] -> [Cl]
forall a. a -> [a] -> [a]
: Bool -> VerboseLevel -> [Cl] -> [Cl]
expandCatchAlls Bool
False VerboseLevel
n [Cl]
cs
                   | Bool
otherwise -> (([Arg Pattern], Arg Pattern) -> Cl)
-> [([Arg Pattern], Arg Pattern)] -> [Cl]
forall a b. (a -> b) -> [a] -> [b]
map (Cl -> ([Arg Pattern], Arg Pattern) -> Cl
expand Cl
c) [([Arg Pattern], Arg Pattern)]
expansions [Cl] -> [Cl] -> [Cl]
forall a. [a] -> [a] -> [a]
++ Cl
c Cl -> [Cl] -> [Cl]
forall a. a -> [a] -> [a]
: Bool -> VerboseLevel -> [Cl] -> [Cl]
expandCatchAlls Bool
False VerboseLevel
n [Cl]
cs
  [Cl]
_ -> [Cl]
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    -- In case there is only one branch in the split tree, we expand all
    -- catch-alls for this position
    -- The @expansions@ are collected from all the clauses @cs@ then.
    -- Note: @expansions@ could be empty, so we keep the orignal clause.
    doExpand :: Cl -> [Cl]
doExpand c :: Cl
c@(Cl [Arg Pattern]
ps Maybe Term
_)
      | [Arg Pattern] -> Bool
exCatchAllNth [Arg Pattern]
ps = (([Arg Pattern], Arg Pattern) -> Cl)
-> [([Arg Pattern], Arg Pattern)] -> [Cl]
forall a b. (a -> b) -> [a] -> [b]
map (Cl -> ([Arg Pattern], Arg Pattern) -> Cl
expand Cl
c) [([Arg Pattern], Arg Pattern)]
expansions [Cl] -> [Cl] -> [Cl]
forall a. [a] -> [a] -> [a]
++ [Cl
c]
      | Bool
otherwise = [Cl
c]

    -- True if nth pattern is variable or there are less than n patterns.
    isCatchAllNth :: [Arg Pattern] -> Bool
isCatchAllNth [Arg Pattern]
ps = (Arg Pattern -> Bool) -> [Arg Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern -> Bool
forall a. Pattern' a -> Bool
isVar (Pattern -> Bool)
-> (Arg Pattern -> Pattern) -> Arg Pattern -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Pattern -> Pattern
forall e. Arg e -> e
unArg) ([Arg Pattern] -> Bool) -> [Arg Pattern] -> Bool
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [Arg Pattern] -> [Arg Pattern]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
1 ([Arg Pattern] -> [Arg Pattern]) -> [Arg Pattern] -> [Arg Pattern]
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [Arg Pattern] -> [Arg Pattern]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
n [Arg Pattern]
ps

    -- True if nth pattern exists and is variable.
    exCatchAllNth :: [Arg Pattern] -> Bool
exCatchAllNth [Arg Pattern]
ps = (Arg Pattern -> Bool) -> [Arg Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Pattern -> Bool
forall a. Pattern' a -> Bool
isVar (Pattern -> Bool)
-> (Arg Pattern -> Pattern) -> Arg Pattern -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Pattern -> Pattern
forall e. Arg e -> e
unArg) ([Arg Pattern] -> Bool) -> [Arg Pattern] -> Bool
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [Arg Pattern] -> [Arg Pattern]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
1 ([Arg Pattern] -> [Arg Pattern]) -> [Arg Pattern] -> [Arg Pattern]
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [Arg Pattern] -> [Arg Pattern]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
n [Arg Pattern]
ps

    classify :: Pattern' x -> Either Literal (Either ConHead QName)
classify (LitP PatternInfo
_ Literal
l)   = Literal -> Either Literal (Either ConHead QName)
forall a b. a -> Either a b
Left Literal
l
    classify (ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' x)]
_) = Either ConHead QName -> Either Literal (Either ConHead QName)
forall a b. b -> Either a b
Right (ConHead -> Either ConHead QName
forall a b. a -> Either a b
Left ConHead
c)
    classify (DefP PatternInfo
_ QName
q [NamedArg (Pattern' x)]
_) = Either ConHead QName -> Either Literal (Either ConHead QName)
forall a b. b -> Either a b
Right (QName -> Either ConHead QName
forall a b. b -> Either a b
Right QName
q)
    classify Pattern' x
_            = Either Literal (Either ConHead QName)
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- All non-catch-all patterns following this one (at position n).
    -- These are the cases the wildcard needs to be expanded into.
    expansions :: [([Arg Pattern], Arg Pattern)]
expansions = (([Arg Pattern], Arg Pattern)
 -> Either Literal (Either ConHead QName))
-> [([Arg Pattern], Arg Pattern)] -> [([Arg Pattern], Arg Pattern)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (Pattern -> Either Literal (Either ConHead QName)
forall x. Pattern' x -> Either Literal (Either ConHead QName)
classify (Pattern -> Either Literal (Either ConHead QName))
-> (([Arg Pattern], Arg Pattern) -> Pattern)
-> ([Arg Pattern], Arg Pattern)
-> Either Literal (Either ConHead QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Pattern -> Pattern
forall e. Arg e -> e
unArg (Arg Pattern -> Pattern)
-> (([Arg Pattern], Arg Pattern) -> Arg Pattern)
-> ([Arg Pattern], Arg Pattern)
-> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Arg Pattern], Arg Pattern) -> Arg Pattern
forall a b. (a, b) -> b
snd)
               ([([Arg Pattern], Arg Pattern)] -> [([Arg Pattern], Arg Pattern)])
-> ([Cl] -> [([Arg Pattern], Arg Pattern)])
-> [Cl]
-> [([Arg Pattern], Arg Pattern)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cl -> Maybe ([Arg Pattern], Arg Pattern))
-> [Cl] -> [([Arg Pattern], Arg Pattern)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([Arg Pattern] -> Maybe ([Arg Pattern], Arg Pattern)
notVarNth ([Arg Pattern] -> Maybe ([Arg Pattern], Arg Pattern))
-> (Cl -> [Arg Pattern])
-> Cl
-> Maybe ([Arg Pattern], Arg Pattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cl -> [Arg Pattern]
clPats)
               ([Cl] -> [([Arg Pattern], Arg Pattern)])
-> [Cl] -> [([Arg Pattern], Arg Pattern)]
forall a b. (a -> b) -> a -> b
$ [Cl]
cs
    notVarNth
      :: [Arg Pattern]
      -> Maybe ([Arg Pattern]  -- First @n@ patterns.
               , Arg Pattern)  -- @n+1@st pattern, not a variable
    notVarNth :: [Arg Pattern] -> Maybe ([Arg Pattern], Arg Pattern)
notVarNth [Arg Pattern]
ps = do
      let ([Arg Pattern]
ps1, [Arg Pattern]
ps2) = VerboseLevel -> [Arg Pattern] -> ([Arg Pattern], [Arg Pattern])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
n [Arg Pattern]
ps
      Arg Pattern
p <- [Arg Pattern] -> Maybe (Arg Pattern)
forall a. [a] -> Maybe a
listToMaybe [Arg Pattern]
ps2
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Pattern -> Bool
forall a. Pattern' a -> Bool
isVar (Pattern -> Bool) -> Pattern -> Bool
forall a b. (a -> b) -> a -> b
$ Arg Pattern -> Pattern
forall e. Arg e -> e
unArg Arg Pattern
p
      ([Arg Pattern], Arg Pattern) -> Maybe ([Arg Pattern], Arg Pattern)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Pattern]
ps1, Arg Pattern
p)

    expand :: Cl -> ([Arg Pattern], Arg Pattern) -> Cl
expand Cl
cl ([Arg Pattern]
qs, Arg Pattern
q) =
      case Arg Pattern -> Pattern
forall e. Arg e -> e
unArg Arg Pattern
q of
        ConP ConHead
c ConPatternInfo
mt [NamedArg Pattern]
qs' -> [Arg Pattern] -> Maybe Term -> Cl
Cl ([Arg Pattern]
ps0 [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern
q Arg Pattern -> Pattern -> Arg Pattern
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ConHead -> ConPatternInfo -> [NamedArg Pattern] -> Pattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
mt [NamedArg Pattern]
conPArgs] [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern]
ps1)
                            (VerboseLevel
-> VerboseLevel
-> SubstArg (Maybe Term)
-> Maybe Term
-> Maybe Term
forall a.
Subst a =>
VerboseLevel -> VerboseLevel -> SubstArg a -> a -> a
substBody VerboseLevel
n' VerboseLevel
m (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
conArgs)) Maybe Term
b)
          where
            ci :: ConInfo
ci       = ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
mt
            m :: VerboseLevel
m        = [NamedArg Pattern] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [NamedArg Pattern]
qs'
            -- replace all direct subpatterns of q by _
            -- TODO Andrea: might need these to sometimes be IApply?
            conPArgs :: [NamedArg Pattern]
conPArgs = (NamedArg Pattern -> NamedArg Pattern)
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName Pattern -> Named NamedName Pattern)
-> NamedArg Pattern -> NamedArg Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Named NamedName Pattern -> Pattern -> Named NamedName Pattern
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> VerboseKey -> Pattern
forall a. a -> Pattern' a
varP VerboseKey
"_")) [NamedArg Pattern]
qs'
            conArgs :: [Arg Term]
conArgs  = (NamedArg Pattern -> VerboseLevel -> Arg Term)
-> [NamedArg Pattern] -> [VerboseLevel] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ NamedArg Pattern
q' VerboseLevel
i -> NamedArg Pattern
q' NamedArg Pattern -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> VerboseLevel -> Term
var VerboseLevel
i) [NamedArg Pattern]
qs' ([VerboseLevel] -> [Arg Term]) -> [VerboseLevel] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
m
        LitP PatternInfo
i Literal
l -> [Arg Pattern] -> Maybe Term -> Cl
Cl ([Arg Pattern]
ps0 [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern
q Arg Pattern -> Pattern -> Arg Pattern
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> PatternInfo -> Literal -> Pattern
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
i Literal
l] [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern]
ps1) (VerboseLevel
-> VerboseLevel
-> SubstArg (Maybe Term)
-> Maybe Term
-> Maybe Term
forall a.
Subst a =>
VerboseLevel -> VerboseLevel -> SubstArg a -> a -> a
substBody VerboseLevel
n' VerboseLevel
0 (Literal -> Term
Lit Literal
l) Maybe Term
b)
        DefP PatternInfo
o QName
d [NamedArg Pattern]
qs' -> [Arg Pattern] -> Maybe Term -> Cl
Cl ([Arg Pattern]
ps0 [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern
q Arg Pattern -> Pattern -> Arg Pattern
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> PatternInfo -> QName -> [NamedArg Pattern] -> Pattern
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
d [NamedArg Pattern]
conPArgs] [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern]
ps1)
                            (VerboseLevel
-> VerboseLevel
-> SubstArg (Maybe Term)
-> Maybe Term
-> Maybe Term
forall a.
Subst a =>
VerboseLevel -> VerboseLevel -> SubstArg a -> a -> a
substBody VerboseLevel
n' VerboseLevel
m (QName -> Elims -> Term
Def QName
d ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
conArgs)) Maybe Term
b)
          where
            m :: VerboseLevel
m        = [NamedArg Pattern] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [NamedArg Pattern]
qs'
            -- replace all direct subpatterns of q by _
            conPArgs :: [NamedArg Pattern]
conPArgs = (NamedArg Pattern -> NamedArg Pattern)
-> [NamedArg Pattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName Pattern -> Named NamedName Pattern)
-> NamedArg Pattern -> NamedArg Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Named NamedName Pattern -> Pattern -> Named NamedName Pattern
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> VerboseKey -> Pattern
forall a. a -> Pattern' a
varP VerboseKey
"_")) [NamedArg Pattern]
qs'
            conArgs :: [Arg Term]
conArgs  = (NamedArg Pattern -> VerboseLevel -> Arg Term)
-> [NamedArg Pattern] -> [VerboseLevel] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ NamedArg Pattern
q' VerboseLevel
i -> NamedArg Pattern
q' NamedArg Pattern -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> VerboseLevel -> Term
var VerboseLevel
i) [NamedArg Pattern]
qs' ([VerboseLevel] -> [Arg Term]) -> [VerboseLevel] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
m
        Pattern
_ -> Cl
forall a. HasCallStack => a
__IMPOSSIBLE__
      where
        -- Andreas, 2016-09-19 issue #2168
        -- Due to varying function arity, some clauses might be eta-contracted.
        -- Thus, we eta-expand them.
        Cl [Arg Pattern]
ps Maybe Term
b = VerboseLevel -> [ArgInfo] -> Cl -> Cl
ensureNPatterns (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1) ((Arg Pattern -> ArgInfo) -> [Arg Pattern] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Arg Pattern -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo ([Arg Pattern] -> [ArgInfo]) -> [Arg Pattern] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ [Arg Pattern]
qs [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern
q]) Cl
cl
        -- The following pattern match cannot fail (by construction of @ps@).
        ([Arg Pattern]
ps0, Arg Pattern
_:[Arg Pattern]
ps1) = VerboseLevel -> [Arg Pattern] -> ([Arg Pattern], [Arg Pattern])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
n [Arg Pattern]
ps

        n' :: VerboseLevel
n' = [Arg Pattern] -> VerboseLevel
forall a. CountPatternVars a => a -> VerboseLevel
countPatternVars [Arg Pattern]
ps1

-- | Make sure (by eta-expansion) that clause has arity at least @n@
--   where @n@ is also the length of the provided list.
ensureNPatterns :: Int -> [ArgInfo] -> Cl -> Cl
ensureNPatterns :: VerboseLevel -> [ArgInfo] -> Cl -> Cl
ensureNPatterns VerboseLevel
n [ArgInfo]
ais0 cl :: Cl
cl@(Cl [Arg Pattern]
ps Maybe Term
b)
  | VerboseLevel
m VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
0    = Cl
cl
  | Bool
otherwise = [Arg Pattern] -> Maybe Term -> Cl
Cl ([Arg Pattern]
ps [Arg Pattern] -> [Arg Pattern] -> [Arg Pattern]
forall a. [a] -> [a] -> [a]
++ [Arg Pattern]
ps') (VerboseLevel -> Maybe Term -> Maybe Term
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
m Maybe Term
b Maybe Term -> [Arg Term] -> Maybe Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args)
  where
  k :: VerboseLevel
k    = [Arg Pattern] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Arg Pattern]
ps
  ais :: [ArgInfo]
ais  = VerboseLevel -> [ArgInfo] -> [ArgInfo]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
k [ArgInfo]
ais0
  -- m = Number of arguments to add
  m :: VerboseLevel
m    = VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
k
  ps' :: [Arg Pattern]
ps'  = [ArgInfo] -> (ArgInfo -> Arg Pattern) -> [Arg Pattern]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [ArgInfo]
ais ((ArgInfo -> Arg Pattern) -> [Arg Pattern])
-> (ArgInfo -> Arg Pattern) -> [Arg Pattern]
forall a b. (a -> b) -> a -> b
$ \ ArgInfo
ai -> ArgInfo -> Pattern -> Arg Pattern
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Pattern -> Arg Pattern) -> Pattern -> Arg Pattern
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Pattern
forall a. a -> Pattern' a
varP VerboseKey
"_"
  args :: [Arg Term]
args = (VerboseLevel -> ArgInfo -> Arg Term)
-> [VerboseLevel] -> [ArgInfo] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ VerboseLevel
i ArgInfo
ai -> ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term
var VerboseLevel
i) (VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
m) [ArgInfo]
ais

substBody :: Subst a => Int -> Int -> SubstArg a -> a -> a
substBody :: VerboseLevel -> VerboseLevel -> SubstArg a -> a -> a
substBody VerboseLevel
n VerboseLevel
m SubstArg a
v = Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution' (SubstArg a) -> a -> a)
-> Substitution' (SubstArg a) -> a -> a
forall a b. (a -> b) -> a -> b
$ VerboseLevel
-> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
forall a. VerboseLevel -> Substitution' a -> Substitution' a
liftS VerboseLevel
n (Substitution' (SubstArg a) -> Substitution' (SubstArg a))
-> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
forall a b. (a -> b) -> a -> b
$ SubstArg a
v SubstArg a
-> Substitution' (SubstArg a) -> Substitution' (SubstArg a)
forall a. a -> Substitution' a -> Substitution' a
:# VerboseLevel -> Substitution' (SubstArg a)
forall a. VerboseLevel -> Substitution' a
raiseS VerboseLevel
m

instance PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a) where