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
  Cls
cs <- (Clause -> Cl) -> [Clause] -> Cls
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Cl
unBruijn ([Clause] -> Cls) -> TCMT IO [Clause] -> TCMT IO Cls
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 (Cls -> CompiledClauses
compile Cls
cs) ((SplitTree -> CompiledClauses) -> CompiledClauses)
-> (SplitTree -> CompiledClauses) -> CompiledClauses
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 -> (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
. Cls -> CompiledClauses
compile (Cls -> CompiledClauses)
-> ([Clause] -> Cls) -> [Clause] -> CompiledClauses
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> Cl) -> [Clause] -> Cls
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

      PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc.tree" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"split tree of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" from coverage check "
        , Doc -> TCMT IO Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO 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 :: Cls
cls = (Clause -> Cl) -> [Clause] -> Cls
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Cl
unBruijn [Clause]
cs

      PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc" Int
30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
        (TCMT IO Doc
"clauses patterns of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" before compilation") TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: do
          (Cl -> TCMT IO Doc) -> Cls -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Pattern' PatVarName] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ([Pattern' PatVarName] -> TCMT IO Doc)
-> (Cl -> [Pattern' PatVarName]) -> Cl -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
-> [Arg (Pattern' PatVarName)] -> [Pattern' PatVarName]
forall a b. (a -> b) -> [a] -> [b]
map Arg (Pattern' PatVarName) -> Pattern' PatVarName
forall e. Arg e -> e
unArg ([Arg (Pattern' PatVarName)] -> [Pattern' PatVarName])
-> (Cl -> [Arg (Pattern' PatVarName)])
-> Cl
-> [Pattern' PatVarName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cl -> [Arg (Pattern' PatVarName)]
clPats) Cls
cls
      PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc" Int
50 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"clauses of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" before compilation" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [Clause] -> TCMT IO 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
      PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc" Int
20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"compiled clauses of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" (still containing record splits)"
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Doc -> TCMT IO Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO 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
      PatVarName -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Int -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc" Int
12 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
        [ TCMT IO Doc
"compiled clauses of " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
        , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Doc -> TCMT IO Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO 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' 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
(Int -> Cl -> ShowS)
-> (Cl -> PatVarName) -> (Cls -> ShowS) -> Show Cl
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) = [Arg (Pattern' PatVarName)] -> Doc
forall a. Pretty a => [a] -> Doc
P.prettyList [Arg (Pattern' PatVarName)]
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' PatVarName)] -> Maybe Term -> Cl
Cl (Substitution' (SubstArg [Arg (Pattern' PatVarName)])
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg [Arg (Pattern' PatVarName)])
sub ([Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)])
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a b. (a -> b) -> a -> b
$ ((NamedArg DeBruijnPattern -> Arg (Pattern' PatVarName))
-> [NamedArg DeBruijnPattern] -> [Arg (Pattern' PatVarName)]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg DeBruijnPattern -> Arg (Pattern' PatVarName))
 -> [NamedArg DeBruijnPattern] -> [Arg (Pattern' PatVarName)])
-> ((Named_ DeBruijnPattern -> Pattern' PatVarName)
    -> NamedArg DeBruijnPattern -> Arg (Pattern' PatVarName))
-> (Named_ DeBruijnPattern -> Pattern' PatVarName)
-> [NamedArg DeBruijnPattern]
-> [Arg (Pattern' PatVarName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named_ DeBruijnPattern -> Pattern' PatVarName)
-> NamedArg DeBruijnPattern -> Arg (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) ((DBPatVar -> PatVarName) -> DeBruijnPattern -> Pattern' PatVarName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DBPatVar -> PatVarName
dbPatVarName (DeBruijnPattern -> Pattern' PatVarName)
-> (Named_ DeBruijnPattern -> DeBruijnPattern)
-> Named_ DeBruijnPattern
-> Pattern' PatVarName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) ([NamedArg DeBruijnPattern] -> [Arg (Pattern' PatVarName)])
-> [NamedArg DeBruijnPattern] -> [Arg (Pattern' PatVarName)]
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
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 -> Cls -> CompiledClauses
compileWithSplitTree SplitTree
t Cls
cs = case SplitTree
t of
  SplitAt Arg Int
i LazySplit
lz SplitTrees' SplitTag
ts -> Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
i (Case CompiledClauses -> CompiledClauses)
-> Case CompiledClauses -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ LazySplit
-> SplitTrees' SplitTag -> Case Cls -> Case CompiledClauses
compiles LazySplit
lz SplitTrees' SplitTag
ts (Case Cls -> Case CompiledClauses)
-> Case Cls -> Case CompiledClauses
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Cls -> Case Cls
splitOn (SplitTrees' SplitTag -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length SplitTrees' SplitTag
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (Arg Int -> Int
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      = Maybe (ConHead, WithArity CompiledClauses)
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 LazySplit -> LazySplit -> Bool
forall a. Eq a => a -> a -> Bool
== LazySplit
LazySplit
          }
      where
        updCons :: Map QName (WithArity Cls) -> Map QName (WithArity CompiledClauses)
updCons = (QName -> WithArity Cls -> WithArity CompiledClauses)
-> Map QName (WithArity Cls)
-> Map QName (WithArity CompiledClauses)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey ((QName -> WithArity Cls -> WithArity CompiledClauses)
 -> Map QName (WithArity Cls)
 -> Map QName (WithArity CompiledClauses))
-> (QName -> WithArity Cls -> WithArity CompiledClauses)
-> Map QName (WithArity Cls)
-> Map QName (WithArity CompiledClauses)
forall a b. (a -> b) -> a -> b
$ \ QName
c WithArity Cls
cl ->
         Maybe SplitTree
-> (Cls -> CompiledClauses)
-> (SplitTree -> Cls -> CompiledClauses)
-> Cls
-> 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) Cls -> CompiledClauses
compile SplitTree -> Cls -> CompiledClauses
compileWithSplitTree (Cls -> CompiledClauses)
-> WithArity Cls -> WithArity CompiledClauses
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 = (Literal -> Cls -> CompiledClauses)
-> Map Literal Cls -> Map Literal CompiledClauses
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey ((Literal -> Cls -> CompiledClauses)
 -> Map Literal Cls -> Map Literal CompiledClauses)
-> (Literal -> Cls -> CompiledClauses)
-> Map Literal Cls
-> Map Literal CompiledClauses
forall a b. (a -> b) -> a -> b
$ \ Literal
l Cls
cl ->
          Maybe SplitTree
-> (Cls -> CompiledClauses)
-> (SplitTree -> Cls -> CompiledClauses)
-> Cls
-> 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) Cls -> CompiledClauses
compile SplitTree -> Cls -> CompiledClauses
compileWithSplitTree Cls
cl
        updCatchall :: Maybe Cls -> Maybe CompiledClauses
updCatchall = (Cls -> CompiledClauses) -> Maybe Cls -> Maybe CompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Cls -> CompiledClauses) -> Maybe Cls -> Maybe CompiledClauses)
-> (Cls -> CompiledClauses) -> Maybe Cls -> Maybe CompiledClauses
forall a b. (a -> b) -> a -> b
$ Maybe SplitTree
-> (Cls -> CompiledClauses)
-> (SplitTree -> Cls -> CompiledClauses)
-> Cls
-> 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) Cls -> CompiledClauses
compile SplitTree -> Cls -> 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 :: Cls -> CompiledClauses
compile [] = [Arg PatVarName] -> CompiledClauses
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) -> Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
n (Case CompiledClauses -> CompiledClauses)
-> Case CompiledClauses -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Cls -> CompiledClauses
compile (Cls -> CompiledClauses) -> Case Cls -> Case CompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Int -> Cls -> Case Cls
splitOn Bool
isRecP (Arg Int -> Int
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  -> [Arg PatVarName] -> Term -> CompiledClauses
forall a. [Arg PatVarName] -> a -> CompiledClauses' a
Done ((Arg (Pattern' PatVarName) -> Arg PatVarName)
-> [Arg (Pattern' PatVarName)] -> [Arg PatVarName]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern' PatVarName -> PatVarName)
-> Arg (Pattern' PatVarName) -> Arg PatVarName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' PatVarName -> PatVarName
forall {x}. Underscore x => Pattern' x -> x
name) ([Arg (Pattern' PatVarName)] -> [Arg PatVarName])
-> [Arg (Pattern' PatVarName)] -> [Arg PatVarName]
forall a b. (a -> b) -> a -> b
$ Cl -> [Arg (Pattern' PatVarName)]
clPats Cl
c) Term
t
    Maybe Term
Nothing -> [Arg PatVarName] -> CompiledClauses
forall a. [Arg PatVarName] -> CompiledClauses' a
Fail ((Arg (Pattern' PatVarName) -> Arg PatVarName)
-> [Arg (Pattern' PatVarName)] -> [Arg PatVarName]
forall a b. (a -> b) -> [a] -> [b]
map ((Pattern' PatVarName -> PatVarName)
-> Arg (Pattern' PatVarName) -> Arg PatVarName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern' PatVarName -> PatVarName
forall {x}. Underscore x => Pattern' x -> x
name) ([Arg (Pattern' PatVarName)] -> [Arg PatVarName])
-> [Arg (Pattern' PatVarName)] -> [Arg PatVarName]
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 = Cl -> Cls -> Cl
forall a. a -> [a] -> a
headWithDefault Cl
forall a. HasCallStack => a
__IMPOSSIBLE__ Cls
cs
    name :: Pattern' x -> x
name (VarP PatternInfo
_ x
x) = x
x
    name (DotP PatternInfo
_ Term
_) = x
forall a. Underscore a => a
underscore
    name ConP{}  = x
forall a. HasCallStack => a
__IMPOSSIBLE__
    name DefP{}  = x
forall a. HasCallStack => a
__IMPOSSIBLE__
    name LitP{}  = x
forall a. HasCallStack => a
__IMPOSSIBLE__
    name ProjP{} = x
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 []             = Maybe (Bool, Arg Int)
forall a. HasCallStack => a
__IMPOSSIBLE__
nextSplit (Cl [Arg (Pattern' PatVarName)]
ps Maybe Term
_ : Cls
cs) = (Int -> Pattern' PatVarName -> Bool)
-> [Arg (Pattern' PatVarName)] -> Maybe (Bool, Arg Int)
forall {t} {a}.
(Num t, Enum t) =>
(t -> Pattern' a -> Bool)
-> [Arg (Pattern' a)] -> Maybe (Bool, Arg t)
findSplit Int -> Pattern' PatVarName -> Bool
forall {p} {x}. p -> Pattern' x -> Bool
nonLazy [Arg (Pattern' PatVarName)]
ps Maybe (Bool, Arg Int)
-> Maybe (Bool, Arg Int) -> Maybe (Bool, Arg Int)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Int -> Pattern' PatVarName -> Bool)
-> [Arg (Pattern' PatVarName)] -> Maybe (Bool, Arg Int)
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 (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 :: Int -> Pattern' PatVarName -> Bool
allAgree Int
i (ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' PatVarName)]
_) = (Cl -> Bool) -> Cls -> 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' PatVarName] -> Maybe QName
forall {x}. [Pattern' x] -> Maybe QName
getCon ([Pattern' PatVarName] -> Maybe QName)
-> (Cl -> [Pattern' PatVarName]) -> Cl -> Maybe QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
-> [Arg (Pattern' PatVarName)] -> [Pattern' PatVarName]
forall a b. (a -> b) -> [a] -> [b]
map Arg (Pattern' PatVarName) -> Pattern' PatVarName
forall e. Arg e -> e
unArg ([Arg (Pattern' PatVarName)] -> [Pattern' PatVarName])
-> (Cl -> [Arg (Pattern' PatVarName)])
-> Cl
-> [Pattern' PatVarName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. Int -> [a] -> [a]
drop Int
i ([Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)])
-> (Cl -> [Arg (Pattern' PatVarName)])
-> Cl
-> [Arg (Pattern' PatVarName)]
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]
_) = 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 :: forall a. 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 :: 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 = [Case Cls] -> Case Cls
forall a. Monoid a => [a] -> a
mconcat ([Case Cls] -> Case Cls) -> [Case Cls] -> Case Cls
forall a b. (a -> b) -> a -> b
$ (Cl -> Case Cls) -> Cls -> [Case Cls]
forall a b. (a -> b) -> [a] -> [b]
map ((Cl -> Cls) -> Case Cl -> Case Cls
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cl -> Cls -> Cls
forall a. a -> [a] -> [a]
:[]) (Case Cl -> Case Cls) -> (Cl -> Case Cl) -> Cl -> Case Cls
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Cl -> Case Cl
splitC Int
n) (Cls -> [Case Cls]) -> Cls -> [Case Cls]
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) = Maybe (Pattern' PatVarName)
-> Case Cl -> (Pattern' PatVarName -> Case Cl) -> Case Cl
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (Pattern' PatVarName)
mp Case Cl
fallback ((Pattern' PatVarName -> Case Cl) -> Case Cl)
-> (Pattern' PatVarName -> 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' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
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 -> (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
$ Int -> Cl -> WithArity Cl
forall c. Int -> c -> WithArity c
WithArity ([NamedArg (Pattern' PatVarName)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg (Pattern' PatVarName)]
qs) (Cl -> WithArity Cl) -> Cl -> WithArity Cl
forall a b. (a -> b) -> a -> b
$
                   [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. [a] -> [a] -> [a]
++ (NamedArg (Pattern' PatVarName) -> Arg (Pattern' PatVarName))
-> [NamedArg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName (Pattern' PatVarName) -> Pattern' PatVarName)
-> NamedArg (Pattern' PatVarName) -> Arg (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' PatVarName) -> Pattern' PatVarName
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' PatVarName)]
qs [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
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 -> (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
$ Int -> Cl -> WithArity Cl
forall c. Int -> c -> WithArity c
WithArity ([NamedArg (Pattern' PatVarName)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg (Pattern' PatVarName)]
qs) (Cl -> WithArity Cl) -> Cl -> WithArity Cl
forall a b. (a -> b) -> a -> b
$
                   [Arg (Pattern' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. [a] -> [a] -> [a]
++ (NamedArg (Pattern' PatVarName) -> Arg (Pattern' PatVarName))
-> [NamedArg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName (Pattern' PatVarName) -> Pattern' PatVarName)
-> NamedArg (Pattern' PatVarName) -> Arg (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' PatVarName) -> Pattern' PatVarName
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' PatVarName)]
qs [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
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' PatVarName)] -> Maybe Term -> Cl
Cl ([Arg (Pattern' PatVarName)]
ps0 [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
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) = Int
-> [Arg (Pattern' PatVarName)]
-> ([Arg (Pattern' PatVarName)], [Arg (Pattern' PatVarName)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Arg (Pattern' PatVarName)]
ps
    mp :: Maybe (Pattern' PatVarName)
mp          = Arg (Pattern' PatVarName) -> Pattern' PatVarName
forall e. Arg e -> e
unArg (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
-> Maybe (Arg (Pattern' PatVarName)) -> Maybe (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg (Pattern' PatVarName)] -> Maybe (Arg (Pattern' PatVarName))
forall a. [a] -> Maybe a
listToMaybe [Arg (Pattern' PatVarName)]
rest
    ps1 :: [Arg (Pattern' PatVarName)]
ps1         = Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. Int -> [a] -> [a]
drop Int
1 [Arg (Pattern' PatVarName)]
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' 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 (Cl -> Cls) -> Cls -> Cls
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Cls
cs else
  case Cls
cs of
  Cls
_                | (Cl -> Bool) -> Cls -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Arg (Pattern' PatVarName)] -> Bool
isCatchAllNth ([Arg (Pattern' PatVarName)] -> Bool)
-> (Cl -> [Arg (Pattern' PatVarName)]) -> Cl -> Bool
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 Cl -> Cls -> Cls
forall a. a -> [a] -> [a]
: Bool -> Int -> Cls -> Cls
expandCatchAlls Bool
False Int
n Cls
cs
                   | Bool
otherwise -> (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl)
-> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
-> Cls
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 Cls -> Cls -> Cls
forall a. [a] -> [a] -> [a]
++ Cl
c Cl -> Cls -> Cls
forall a. a -> [a] -> [a]
: Bool -> Int -> Cls -> Cls
expandCatchAlls Bool
False Int
n Cls
cs
  Cls
_ -> 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 = (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)) -> Cl)
-> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
-> Cls
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 Cls -> Cls -> Cls
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 = (Arg (Pattern' PatVarName) -> Bool)
-> [Arg (Pattern' PatVarName)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Pattern' PatVarName -> Bool
forall a. Pattern' a -> Bool
isVar (Pattern' PatVarName -> Bool)
-> (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
-> Arg (Pattern' PatVarName)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Pattern' PatVarName) -> Pattern' PatVarName
forall e. Arg e -> e
unArg) ([Arg (Pattern' PatVarName)] -> Bool)
-> [Arg (Pattern' PatVarName)] -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. Int -> [a] -> [a]
take Int
1 ([Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)])
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a b. (a -> b) -> a -> b
$ Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
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 = (Arg (Pattern' PatVarName) -> Bool)
-> [Arg (Pattern' PatVarName)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Pattern' PatVarName -> Bool
forall a. Pattern' a -> Bool
isVar (Pattern' PatVarName -> Bool)
-> (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
-> Arg (Pattern' PatVarName)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Pattern' PatVarName) -> Pattern' PatVarName
forall e. Arg e -> e
unArg) ([Arg (Pattern' PatVarName)] -> Bool)
-> [Arg (Pattern' PatVarName)] -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. Int -> [a] -> [a]
take Int
1 ([Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)])
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a b. (a -> b) -> a -> b
$ Int -> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
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)   = 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' PatVarName)], Arg (Pattern' PatVarName))]
expansions = (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
 -> Either Literal (Either ConHead QName))
-> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
-> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (Pattern' PatVarName -> Either Literal (Either ConHead QName)
forall {x}. Pattern' x -> Either Literal (Either ConHead QName)
classify (Pattern' PatVarName -> Either Literal (Either ConHead QName))
-> (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    -> Pattern' PatVarName)
-> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
-> Either Literal (Either ConHead QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Pattern' PatVarName) -> Pattern' PatVarName
forall e. Arg e -> e
unArg (Arg (Pattern' PatVarName) -> Pattern' PatVarName)
-> (([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
    -> Arg (Pattern' PatVarName))
-> ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
-> Pattern' PatVarName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
-> Arg (Pattern' PatVarName)
forall a b. (a, b) -> b
snd)
               ([([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
 -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))])
-> (Cls
    -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))])
-> Cls
-> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Cl
 -> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)))
-> Cls
-> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([Arg (Pattern' PatVarName)]
-> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
notVarNth ([Arg (Pattern' PatVarName)]
 -> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName)))
-> (Cl -> [Arg (Pattern' PatVarName)])
-> Cl
-> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cl -> [Arg (Pattern' PatVarName)]
clPats)
               (Cls -> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))])
-> Cls
-> [([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))]
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) = Int
-> [Arg (Pattern' PatVarName)]
-> ([Arg (Pattern' PatVarName)], [Arg (Pattern' PatVarName)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Arg (Pattern' PatVarName)]
ps
      Arg (Pattern' PatVarName)
p <- [Arg (Pattern' PatVarName)] -> Maybe (Arg (Pattern' PatVarName))
forall a. [a] -> Maybe a
listToMaybe [Arg (Pattern' PatVarName)]
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' PatVarName -> Bool
forall a. Pattern' a -> Bool
isVar (Pattern' PatVarName -> Bool) -> Pattern' PatVarName -> Bool
forall a b. (a -> b) -> a -> b
$ Arg (Pattern' PatVarName) -> Pattern' PatVarName
forall e. Arg e -> e
unArg Arg (Pattern' PatVarName)
p
      ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
-> Maybe ([Arg (Pattern' PatVarName)], Arg (Pattern' PatVarName))
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 Arg (Pattern' PatVarName) -> Pattern' PatVarName
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 [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)
q Arg (Pattern' PatVarName)
-> Pattern' PatVarName -> Arg (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' PatVarName)]
-> Pattern' PatVarName
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
mt [NamedArg (Pattern' PatVarName)]
conPArgs] [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1)
                            (Int -> Int -> SubstArg (Maybe Term) -> Maybe Term -> Maybe Term
forall a. Subst a => Int -> Int -> SubstArg a -> a -> a
substBody Int
n' Int
m (ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci ((Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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        = [NamedArg (Pattern' PatVarName)] -> Int
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 = (NamedArg (Pattern' PatVarName) -> NamedArg (Pattern' PatVarName))
-> [NamedArg (Pattern' PatVarName)]
-> [NamedArg (Pattern' PatVarName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName (Pattern' PatVarName)
 -> Named NamedName (Pattern' PatVarName))
-> NamedArg (Pattern' PatVarName) -> NamedArg (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Named NamedName (Pattern' PatVarName)
-> Pattern' PatVarName -> Named NamedName (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> PatVarName -> Pattern' PatVarName
forall a. a -> Pattern' a
varP PatVarName
"_")) [NamedArg (Pattern' PatVarName)]
qs'
            conArgs :: [Arg Term]
conArgs  = (NamedArg (Pattern' PatVarName) -> Int -> Arg Term)
-> [NamedArg (Pattern' PatVarName)] -> [Int] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ NamedArg (Pattern' PatVarName)
q' Int
i -> NamedArg (Pattern' PatVarName)
q' NamedArg (Pattern' PatVarName) -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
i) [NamedArg (Pattern' PatVarName)]
qs' ([Int] -> [Arg Term]) -> [Int] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
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 [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)
q Arg (Pattern' PatVarName)
-> Pattern' PatVarName -> Arg (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> PatternInfo -> Literal -> Pattern' PatVarName
forall x. PatternInfo -> Literal -> Pattern' x
LitP PatternInfo
i Literal
l] [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1) (Int -> Int -> SubstArg (Maybe Term) -> Maybe Term -> Maybe Term
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 [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)
q Arg (Pattern' PatVarName)
-> Pattern' PatVarName -> Arg (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> PatternInfo
-> QName -> [NamedArg (Pattern' PatVarName)] -> Pattern' PatVarName
forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
d [NamedArg (Pattern' PatVarName)]
conPArgs] [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' PatVarName)]
ps1)
                            (Int -> Int -> SubstArg (Maybe Term) -> Maybe Term -> Maybe Term
forall a. Subst a => Int -> Int -> SubstArg a -> a -> a
substBody Int
n' Int
m (QName -> Elims -> Term
Def QName
d ((Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
conArgs)) Maybe Term
b)
          where
            m :: Int
m        = [NamedArg (Pattern' PatVarName)] -> Int
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 = (NamedArg (Pattern' PatVarName) -> NamedArg (Pattern' PatVarName))
-> [NamedArg (Pattern' PatVarName)]
-> [NamedArg (Pattern' PatVarName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Named NamedName (Pattern' PatVarName)
 -> Named NamedName (Pattern' PatVarName))
-> NamedArg (Pattern' PatVarName) -> NamedArg (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Named NamedName (Pattern' PatVarName)
-> Pattern' PatVarName -> Named NamedName (Pattern' PatVarName)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> PatVarName -> Pattern' PatVarName
forall a. a -> Pattern' a
varP PatVarName
"_")) [NamedArg (Pattern' PatVarName)]
qs'
            conArgs :: [Arg Term]
conArgs  = (NamedArg (Pattern' PatVarName) -> Int -> Arg Term)
-> [NamedArg (Pattern' PatVarName)] -> [Int] -> [Arg Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ NamedArg (Pattern' PatVarName)
q' Int
i -> NamedArg (Pattern' PatVarName)
q' NamedArg (Pattern' PatVarName) -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Int -> Term
var Int
i) [NamedArg (Pattern' PatVarName)]
qs' ([Int] -> [Arg Term]) -> [Int] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
m
        Pattern' PatVarName
_ -> 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' PatVarName)]
ps Maybe Term
b = Int -> [ArgInfo] -> Cl -> Cl
ensureNPatterns (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ((Arg (Pattern' PatVarName) -> ArgInfo)
-> [Arg (Pattern' PatVarName)] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Arg (Pattern' PatVarName) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo ([Arg (Pattern' PatVarName)] -> [ArgInfo])
-> [Arg (Pattern' PatVarName)] -> [ArgInfo]
forall a b. (a -> b) -> a -> b
$ [Arg (Pattern' PatVarName)]
qs [Arg (Pattern' PatVarName)]
-> [Arg (Pattern' PatVarName)] -> [Arg (Pattern' PatVarName)]
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) = Int
-> [Arg (Pattern' PatVarName)]
-> ([Arg (Pattern' PatVarName)], [Arg (Pattern' PatVarName)])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Arg (Pattern' PatVarName)]
ps

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

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