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
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 = (forall a. a -> Maybe a
Just Bool
True forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseUnreachable
  Cls
cs <- forall a b. (a -> b) -> [a] -> [b]
map Clause -> Cl
unBruijn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP (forall a. (a -> Bool) -> [a] -> [a]
filter Clause -> Bool
notUnreachable [Clause]
cs)

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

  CompiledClauses -> TCM CompiledClauses
translate forall a b. (a -> b) -> a -> b
$ forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe SplitTree
mSplitTree (Cls -> CompiledClauses
compile Cls
cs) forall a b. (a -> b) -> a -> b
$ \SplitTree
splitTree ->
    SplitTree -> Cls -> CompiledClauses
compileWithSplitTree SplitTree
splitTree Cls
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 -> (forall a. Maybe a
Nothing,Bool
False,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cls -> CompiledClauses
compile forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Clause -> Cl
unBruijn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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

      forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc.tree" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"split tree of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" from coverage check "
        , forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = (forall a. a -> Maybe a
Just Bool
True forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Bool
clauseUnreachable
      [Clause]
cs <- forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. (a -> Bool) -> [a] -> [a]
filter Clause -> Bool
notUnreachable forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> [Clause]
defClauses forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q

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

      forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc" Int
30 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep forall a b. (a -> b) -> a -> b
$ do
        (TCMT IO Doc
"clauses patterns of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" before compilation") forall a. a -> [a] -> [a]
: do
          forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cl -> [Arg (Pattern' PatVarName)]
clPats) Cls
cls
      forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc" Int
50 forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"clauses of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" before compilation" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Clause]
cs
      let cc :: CompiledClauses
cc = SplitTree -> Cls -> CompiledClauses
compileWithSplitTree SplitTree
splitTree Cls
cls
      forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"compiled clauses of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" (still containing record splits)"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
P.pretty CompiledClauses
cc
        ]
      (CompiledClauses
cc, Bool
becameCopatternLHS) <- forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
translateCompiledClauses CompiledClauses
cc
      forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc" Int
12 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"compiled clauses of " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
P.pretty CompiledClauses
cc
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just SplitTree
splitTree, Bool
becameCopatternLHS, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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' PatVarName)]
clPats :: [Arg Pattern]
      -- ^ Pattern variables are considered in left-to-right order.
  , Cl -> Maybe Term
clBody :: Maybe Term
  } deriving (Int -> Cl -> ShowS
Cls -> ShowS
Cl -> PatVarName
forall a.
(Int -> a -> ShowS)
-> (a -> PatVarName) -> ([a] -> ShowS) -> Show a
showList :: Cls -> ShowS
$cshowList :: Cls -> ShowS
show :: Cl -> PatVarName
$cshow :: Cl -> PatVarName
showsPrec :: Int -> Cl -> ShowS
$cshowsPrec :: Int -> Cl -> ShowS
Show)

instance P.Pretty Cl where
  pretty :: Cl -> Doc
pretty (Cl [Arg (Pattern' PatVarName)]
ps Maybe Term
b) = forall a. Pretty a => [a] -> Doc
P.prettyList [Arg (Pattern' PatVarName)]
ps Doc -> Doc -> Doc
P.<+> Doc
"->" Doc -> Doc -> Doc
P.<+> forall b a. b -> (a -> b) -> Maybe a -> b
maybe 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' PatVarName)] -> Maybe Term -> Cl
Cl (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sub forall a b. (a -> b) -> a -> b
$ (forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DBPatVar -> PatVarName
dbPatVarName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name a. Named name a -> a
namedThing) forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
c)
                (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sub forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
c)
  where
    sub :: Substitution' Term
sub = forall a. DeBruijn a => Permutation -> Substitution' a
renamingR forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ (Clause -> Maybe Permutation
clausePerm Clause
c)

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

compile :: Cls -> CompiledClauses
compile :: Cls -> CompiledClauses
compile [] = forall a. [Arg PatVarName] -> CompiledClauses' a
Fail []
compile Cls
cs = case Cls -> Maybe (Bool, Arg Int)
nextSplit Cls
cs of
  Just (Bool
isRecP, Arg Int
n) -> forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
n forall a b. (a -> b) -> a -> b
$ Cls -> CompiledClauses
compile forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Int -> Cls -> Case Cls
splitOn Bool
isRecP (forall e. Arg e -> e
unArg Arg Int
n) Cls
cs
  Maybe (Bool, Arg Int)
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  -> forall a. [Arg PatVarName] -> a -> CompiledClauses' a
Done (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {x}. Underscore x => Pattern' x -> x
name) forall a b. (a -> b) -> a -> b
$ Cl -> [Arg (Pattern' PatVarName)]
clPats Cl
c) Term
t
    Maybe Term
Nothing -> forall a. [Arg PatVarName] -> CompiledClauses' a
Fail (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {x}. Underscore x => Pattern' x -> x
name) forall a b. (a -> b) -> a -> b
$ Cl -> [Arg (Pattern' PatVarName)]
clPats Cl
c)
  where
    -- If there are more than one clauses, take the first one.
    c :: Cl
c = forall a. a -> [a] -> a
headWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ Cls
cs
    name :: Pattern' x -> x
name (VarP PatternInfo
_ x
x) = x
x
    name (DotP PatternInfo
_ Term
_) = forall a. Underscore a => a
underscore
    name ConP{}  = forall a. HasCallStack => a
__IMPOSSIBLE__
    name DefP{}  = forall a. HasCallStack => a
__IMPOSSIBLE__
    name LitP{}  = forall a. HasCallStack => a
__IMPOSSIBLE__
    name ProjP{} = forall a. HasCallStack => a
__IMPOSSIBLE__
    name (IApplyP PatternInfo
_ Term
_ Term
_ x
x) = x
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 :: Cls -> Maybe (Bool, Arg Int)
nextSplit []             = forall a. HasCallStack => a
__IMPOSSIBLE__
nextSplit (Cl [Arg (Pattern' PatVarName)]
ps Maybe Term
_ : Cls
cs) = forall {t} {a}.
(Num t, Enum t) =>
(t -> Pattern' a -> Bool)
-> [Arg (Pattern' a)] -> Maybe (Bool, Arg t)
findSplit forall {p} {x}. p -> Pattern' x -> Bool
nonLazy [Arg (Pattern' PatVarName)]
ps forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {t} {a}.
(Num t, Enum t) =>
(t -> Pattern' a -> Bool)
-> [Arg (Pattern' a)] -> Maybe (Bool, Arg t)
findSplit Int -> Pattern' PatVarName -> Bool
allAgree [Arg (Pattern' PatVarName)]
ps
  where
    nonLazy :: p -> Pattern' x -> Bool
nonLazy p
_ (ConP ConHead
_ ConPatternInfo
cpi [NamedArg (Pattern' x)]
_) = Bool -> Bool
not 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 = forall a. [a] -> Maybe a
listToMaybe (forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$
      forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ (Arg ArgInfo
ai Pattern' a
p) t
n -> (, forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai t
n) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Pattern' a -> Maybe Bool
properSplit Pattern' a
p forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (f :: * -> *). Alternative f => Bool -> f ()
guard (t -> Pattern' a -> Bool
okPat t
n Pattern' a
p)) [Arg (Pattern' a)]
ps [t
0..])

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

    getCon :: [Pattern' x] -> Maybe QName
getCon (ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' x)]
_ : [Pattern' x]
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c
    getCon [Pattern' x]
_                = 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 :: forall a. Pattern' a -> Maybe Bool
properSplit (ConP ConHead
_ ConPatternInfo
cpi [NamedArg (Pattern' a)]
_) = forall a. a -> Maybe a
Just ((ConPatternInfo -> Bool
conPRecord ConPatternInfo
cpi Bool -> Bool -> Bool
&& PatternInfo -> PatOrigin
patOrigin (ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
cpi) forall a. Eq a => a -> a -> Bool
== PatOrigin
PatORec) Bool -> Bool -> Bool
|| ConPatternInfo -> Bool
conPFallThrough ConPatternInfo
cpi)
properSplit DefP{}    = forall a. a -> Maybe a
Just Bool
False
properSplit LitP{}    = forall a. a -> Maybe a
Just Bool
False
properSplit ProjP{}   = forall a. a -> Maybe a
Just Bool
False
properSplit IApplyP{} = forall a. Maybe a
Nothing
properSplit VarP{}    = forall a. Maybe a
Nothing
properSplit DotP{}    = forall a. Maybe a
Nothing

-- | Is this a variable pattern?
--
--   Maintain invariant: @isVar = isNothing . properSplit@!
isVar :: Pattern' a -> Bool
isVar :: forall a. 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 -> Int -> Cls -> Case Cls
splitOn Bool
single Int
n Cls
cs = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Cl -> Case Cl
splitC Int
n) forall a b. (a -> b) -> a -> b
$
  -- (\ cs -> trace ("splitting on " ++ show n ++ " after expandCatchAlls " ++ show single ++ ": " ++ prettyShow (P.prettyList cs)) cs) $
    Bool -> Int -> Cls -> Cls
expandCatchAlls Bool
single Int
n Cls
cs

splitC :: Int -> Cl -> Case Cl
splitC :: Int -> Cl -> Case Cl
splitC Int
n (Cl [Arg (Pattern' PatVarName)]
ps Maybe Term
b) = forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Pattern' PatVarName)
mp Case Cl
fallback forall a b. (a -> b) -> a -> b
$ \case
  ProjP ProjOrigin
_ QName
d   -> forall c. QName -> c -> Case c
projCase QName
d forall a b. (a -> b) -> a -> b
$ [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1) Maybe Term
b
  IApplyP{}   -> Case Cl
fallback
  ConP ConHead
c ConPatternInfo
i [NamedArg (Pattern' PatVarName)]
qs -> (forall c. QName -> Bool -> WithArity c -> Case c
conCase (ConHead -> QName
conName ConHead
c) (ConPatternInfo -> Bool
conPFallThrough ConPatternInfo
i) forall a b. (a -> b) -> a -> b
$ forall c. Int -> c -> WithArity c
WithArity (forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg (Pattern' PatVarName)]
qs) forall a b. (a -> b) -> a -> b
$
                   [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' PatVarName)]
qs forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1) Maybe Term
b) { lazyMatch :: Bool
lazyMatch = ConPatternInfo -> Bool
conPLazy ConPatternInfo
i }
  DefP PatternInfo
o QName
q [NamedArg (Pattern' PatVarName)]
qs -> (forall c. QName -> Bool -> WithArity c -> Case c
conCase QName
q Bool
False forall a b. (a -> b) -> a -> b
$ forall c. Int -> c -> WithArity c
WithArity (forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg (Pattern' PatVarName)]
qs) forall a b. (a -> b) -> a -> b
$
                   [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' PatVarName)]
qs forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1) Maybe Term
b) { lazyMatch :: Bool
lazyMatch = Bool
False }
  LitP PatternInfo
_ Literal
l    -> forall c. Literal -> c -> Case c
litCase Literal
l forall a b. (a -> b) -> a -> b
$ [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1) Maybe Term
b
  VarP{}      -> Case Cl
fallback
  DotP{}      -> Case Cl
fallback
  where
    ([Arg (Pattern' PatVarName)]
ps0, [Arg (Pattern' PatVarName)]
rest) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Arg (Pattern' PatVarName)]
ps
    mp :: Maybe (Pattern' PatVarName)
mp          = forall e. Arg e -> e
unArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> Maybe a
listToMaybe [Arg (Pattern' PatVarName)]
rest
    ps1 :: [Arg (Pattern' PatVarName)]
ps1         = forall a. Int -> [a] -> [a]
drop Int
1 [Arg (Pattern' PatVarName)]
rest
    fallback :: Case Cl
fallback    = forall c. c -> Case c
catchAll forall a b. (a -> b) -> a -> b
$ [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl [Arg (Pattern' PatVarName)]
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 -> Int -> Cls -> Cls
expandCatchAlls Bool
single Int
n Cls
cs =
  -- Andreas, 2013-03-22
  -- if there is a single case (such as for record splits)
  -- we force expansion
  if Bool
single then Cl -> Cls
doExpand forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Cls
cs else
  case Cls
cs of
  Cls
_                | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Arg (Pattern' PatVarName)] -> Bool
isCatchAllNth forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cl -> [Arg (Pattern' PatVarName)]
clPats) Cls
cs -> Cls
cs
  c :: Cl
c@(Cl [Arg (Pattern' PatVarName)]
ps Maybe Term
b) : Cls
cs | Bool -> Bool
not ([Arg (Pattern' PatVarName)] -> Bool
isCatchAllNth [Arg (Pattern' PatVarName)]
ps) -> Cl
c forall a. a -> [a] -> [a]
: Bool -> Int -> Cls -> Cls
expandCatchAlls Bool
False Int
n Cls
cs
                   | Bool
otherwise -> forall a b. (a -> b) -> [a] -> [b]
map (Cl
-> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl
expand Cl
c) [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
expansions forall a. [a] -> [a] -> [a]
++ Cl
c forall a. a -> [a] -> [a]
: Bool -> Int -> Cls -> Cls
expandCatchAlls Bool
False Int
n Cls
cs
  Cls
_ -> 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 -> Cls
doExpand c :: Cl
c@(Cl [Arg (Pattern' PatVarName)]
ps Maybe Term
_)
      | [Arg (Pattern' PatVarName)] -> Bool
exCatchAllNth [Arg (Pattern' PatVarName)]
ps = forall a b. (a -> b) -> [a] -> [b]
map (Cl
-> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl
expand Cl
c) [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
expansions 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' PatVarName)] -> Bool
isCatchAllNth [Arg (Pattern' PatVarName)]
ps = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Pattern' a -> Bool
isVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
1 forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
n [Arg (Pattern' PatVarName)]
ps

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

    classify :: Pattern' x -> Either Literal (Either ConHead QName)
classify (LitP PatternInfo
_ Literal
l)   = forall a b. a -> Either a b
Left Literal
l
    classify (ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' x)]
_) = forall a b. b -> Either a b
Right (forall a b. a -> Either a b
Left ConHead
c)
    classify (DefP PatternInfo
_ QName
q [NamedArg (Pattern' x)]
_) = forall a b. b -> Either a b
Right (forall a b. b -> Either a b
Right QName
q)
    classify Pattern' x
_            = 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' PatVarName)], Arg (Pattern' PatVarName))]
expansions = forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (forall {x}. Pattern' x -> Either Literal (Either ConHead QName)
classify forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)
               forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([Arg (Pattern' PatVarName)]
-> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
notVarNth forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cl -> [Arg (Pattern' PatVarName)]
clPats)
               forall a b. (a -> b) -> a -> b
$ Cls
cs
    notVarNth
      :: [Arg Pattern]
      -> Maybe ([Arg Pattern]  -- First @n@ patterns.
               , Arg Pattern)  -- @n+1@st pattern, not a variable
    notVarNth :: [Arg (Pattern' PatVarName)]
-> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
notVarNth [Arg (Pattern' PatVarName)]
ps = do
      let ([Arg (Pattern' PatVarName)]
ps1, [Arg (Pattern' PatVarName)]
ps2) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Arg (Pattern' PatVarName)]
ps
      Arg (Pattern' PatVarName)
p <- forall a. [a] -> Maybe a
listToMaybe [Arg (Pattern' PatVarName)]
ps2
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Pattern' a -> Bool
isVar forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg (Pattern' PatVarName)
p
      forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg (Pattern' PatVarName)]
ps1, Arg (Pattern' PatVarName)
p)

    expand :: Cl
-> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl
expand Cl
cl ([Arg (Pattern' PatVarName)]
qs, Arg (Pattern' PatVarName)
q) =
      case forall e. Arg e -> e
unArg Arg (Pattern' PatVarName)
q of
        ConP ConHead
c ConPatternInfo
mt [NamedArg (Pattern' PatVarName)]
qs' -> [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)
q forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
mt [NamedArg (Pattern' PatVarName)]
conPArgs] forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1)
                            (forall a. Subst a => Int -> Int -> SubstArg a -> a -> a
substBody Int
n' Int
m (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg Term]
conArgs)) Maybe Term
b)
          where
            ci :: ConInfo
ci       = ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
mt
            m :: Int
m        = forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg (Pattern' PatVarName)]
qs'
            -- replace all direct subpatterns of q by _
            -- TODO Andrea: might need these to sometimes be IApply?
            conPArgs :: [NamedArg (Pattern' PatVarName)]
conPArgs = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall a. a -> Pattern' a
varP PatVarName
"_")) [NamedArg (Pattern' PatVarName)]
qs'
            conArgs :: [Arg Term]
conArgs  = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ NamedArg (Pattern' PatVarName)
q' Int
i -> NamedArg (Pattern' PatVarName)
q' forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
i) [NamedArg (Pattern' PatVarName)]
qs' forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom Int
m
        LitP PatternInfo
i Literal
l -> [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)
q forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
i Literal
l] forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1) (forall a. Subst a => Int -> Int -> SubstArg a -> a -> a
substBody Int
n' Int
0 (Literal -> Term
Lit Literal
l) Maybe Term
b)
        DefP PatternInfo
o QName
d [NamedArg (Pattern' PatVarName)]
qs' -> [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)
q forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
d [NamedArg (Pattern' PatVarName)]
conPArgs] forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1)
                            (forall a. Subst a => Int -> Int -> SubstArg a -> a -> a
substBody Int
n' Int
m (QName -> Elims -> Term
Def QName
d (forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg Term]
conArgs)) Maybe Term
b)
          where
            m :: Int
m        = forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg (Pattern' PatVarName)]
qs'
            -- replace all direct subpatterns of q by _
            conPArgs :: [NamedArg (Pattern' PatVarName)]
conPArgs = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall a. a -> Pattern' a
varP PatVarName
"_")) [NamedArg (Pattern' PatVarName)]
qs'
            conArgs :: [Arg Term]
conArgs  = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ NamedArg (Pattern' PatVarName)
q' Int
i -> NamedArg (Pattern' PatVarName)
q' forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
i) [NamedArg (Pattern' PatVarName)]
qs' forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom Int
m
        Pattern' PatVarName
_ -> 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' PatVarName)]
ps Maybe Term
b = Int -> [ArgInfo] -> Cl -> Cl
ensureNPatterns (Int
n forall a. Num a => a -> a -> a
+ Int
1) (forall a b. (a -> b) -> [a] -> [b]
map forall a. LensArgInfo a => a -> ArgInfo
getArgInfo forall a b. (a -> b) -> a -> b
$ [Arg (Pattern' PatVarName)]
qs forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)
q]) Cl
cl
        -- The following pattern match cannot fail (by construction of @ps@).
        ([Arg (Pattern' PatVarName)]
ps0, Arg (Pattern' PatVarName)
_:[Arg (Pattern' PatVarName)]
ps1) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Arg (Pattern' PatVarName)]
ps

        n' :: Int
n' = forall a. CountPatternVars a => a -> Int
countPatternVars [Arg (Pattern' PatVarName)]
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 :: Int -> [ArgInfo] -> Cl -> Cl
ensureNPatterns Int
n [ArgInfo]
ais0 cl :: Cl
cl@(Cl [Arg (Pattern' PatVarName)]
ps Maybe Term
b)
  | Int
m forall a. Ord a => a -> a -> Bool
<= Int
0    = Cl
cl
  | Bool
otherwise = [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps') (forall a. Subst a => Int -> a -> a
raise Int
m Maybe Term
b forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args)
  where
  k :: Int
k    = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg (Pattern' PatVarName)]
ps
  ais :: [ArgInfo]
ais  = forall a. Int -> [a] -> [a]
drop Int
k [ArgInfo]
ais0
  -- m = Number of arguments to add
  m :: Int
m    = Int
n forall a. Num a => a -> a -> a
- Int
k
  ps' :: [Arg (Pattern' PatVarName)]
ps'  = forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [ArgInfo]
ais forall a b. (a -> b) -> a -> b
$ \ ArgInfo
ai -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ forall a. a -> Pattern' a
varP PatVarName
"_"
  args :: [Arg Term]
args = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Int
i ArgInfo
ai -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i) (forall a. Integral a => a -> [a]
downFrom Int
m) [ArgInfo]
ais

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

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