-- | Code which replaces pattern matching on record constructors with
-- uses of projection functions.

module Agda.TypeChecking.RecordPatterns
  ( translateCompiledClauses
  , translateSplitTree
  , recordPatternToProjections
  , recordRHSToCopatterns
  ) where

import Control.Arrow          ( first, second )
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Reader   ( MonadReader(..), ReaderT(..), runReaderT )
import Control.Monad.State    ( MonadState(..), StateT(..), runStateT )

import qualified Data.List as List
import Data.Maybe
import qualified Data.Map as Map

import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Common.Pretty (Pretty(..), prettyShow)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.Syntax.Info

import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty hiding (pretty)
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.Interaction.Options

import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Monad
import Agda.Utils.Permutation hiding (dropFrom)
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Update (MonadChange, tellDirty)

import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Record pattern translation for let bindings
---------------------------------------------------------------------------

-- | Take a record pattern @p@ and yield a list of projections
--   corresponding to the pattern variables, from left to right.
--
--   E.g. for @(x , (y , z))@ we return @[ fst, fst . snd, snd . snd ]@.
--
--   If it is not a record pattern, error 'ShouldBeRecordPattern' is raised.
recordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections DeBruijnPattern
p =
  case DeBruijnPattern
p of
    VarP{}       -> [Term -> Term] -> TCM [Term -> Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Term -> Term
forall a. a -> a
id ]
    LitP{}       -> TypeError -> TCM [Term -> Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM [Term -> Term])
-> TypeError -> TCM [Term -> Term]
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
    DotP{}       -> TypeError -> TCM [Term -> Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM [Term -> Term])
-> TypeError -> TCM [Term -> Term]
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
    ConP ConHead
c ConPatternInfo
ci [NamedArg DeBruijnPattern]
ps -> do
      Bool -> TCMT IO () -> TCMT IO ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (ConPatternInfo -> Bool
conPRecord ConPatternInfo
ci) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
      let t :: Type
t = Arg Type -> Type
forall e. Arg e -> e
unArg (Arg Type -> Type) -> Arg Type -> Type
forall a b. (a -> b) -> a -> b
$ Arg Type -> Maybe (Arg Type) -> Arg Type
forall a. a -> Maybe a -> a
fromMaybe Arg Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg Type) -> Arg Type) -> Maybe (Arg Type) -> Arg Type
forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
ci
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.rec" Int
45 (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
"recordPatternToProjections: "
        , 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
$ TCMT IO Doc
"constructor pattern " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM DeBruijnPattern
p TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" has type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
        ]
      [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.rec" Int
70 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"  type raw: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall a. Show a => a -> [Char]
show Type
t
      fields <- Type -> TCM [Dom QName]
getRecordTypeFields Type
t
      concat <$> zipWithM comb (map proj fields) (map namedArg ps)
    ProjP{}      -> TCM [Term -> Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ -- copattern cannot appear here
    IApplyP{}    -> TypeError -> TCM [Term -> Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM [Term -> Term])
-> TypeError -> TCM [Term -> Term]
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
    DefP{}       -> TypeError -> TCM [Term -> Term]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM [Term -> Term])
-> TypeError -> TCM [Term -> Term]
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
  where
    proj :: Dom' t QName -> t -> t
proj Dom' t QName
p = (t -> Elims -> t
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim' Term
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem (QName -> Elim' Term) -> QName -> Elim' Term
forall a b. (a -> b) -> a -> b
$ Dom' t QName -> QName
forall t e. Dom' t e -> e
unDom Dom' t QName
p])
    comb :: (Term -> Term) -> DeBruijnPattern -> TCM [Term -> Term]
    comb :: (Term -> Term) -> DeBruijnPattern -> TCM [Term -> Term]
comb Term -> Term
prj DeBruijnPattern
p = ((Term -> Term) -> Term -> Term)
-> [Term -> Term] -> [Term -> Term]
forall a b. (a -> b) -> [a] -> [b]
map (\ Term -> Term
f -> Term -> Term
f (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
prj) ([Term -> Term] -> [Term -> Term])
-> TCM [Term -> Term] -> TCM [Term -> Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections DeBruijnPattern
p


---------------------------------------------------------------------------
-- * Record pattern translation for compiled clauses
---------------------------------------------------------------------------

-- | Take a matrix of booleans (at least one row!) and summarize the columns
--   using conjunction.
conjColumns :: [[Bool]] -> [Bool]
conjColumns :: [[Bool]] -> [Bool]
conjColumns =  ([Bool] -> [Bool] -> [Bool]) -> [[Bool]] -> [Bool]
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 ((Bool -> Bool -> Bool) -> [Bool] -> [Bool] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Bool -> Bool -> Bool
(&&))

-- UNUSED Liang-Ting 2019-07-16
---- | @insertColumn i a m@ inserts a column before the @i@th column in
----   matrix @m@ and fills it with value @a@.
--insertColumn :: Int -> a -> [[a]] -> [[a]]
--insertColumn i a rows = map ins rows where
--  ins row = let (init, last) = splitAt i row in init ++ a : last

{- UNUSED
-- | @cutColumn i m@ removes the @i@th column from matrix @m@.
cutColumn :: Int -> [[a]] -> [[a]]
cutColumn i rows = map cut rows where
  cut row = let (init, _:last) = splitAt i row in init ++ last

-- | @cutColumns i n xss = (yss, xss')@ cuts out a submatrix @yss@
--   of width @n@ from @xss@, starting at column @i@.
cutColumns :: Int -> Int -> [[a]] -> ([[a]], [[a]])
cutColumns i n rows = unzip (map (cutSublist i n) rows)
-}

-- UNUSED Liang-Ting 2019-07-16
---- | @cutSublist i n xs = (xs', ys, xs'')@ cuts out a sublist @ys@
----   of width @n@ from @xs@, starting at column @i@.
--cutSublist :: Int -> Int -> [a] -> ([a], [a], [a])
--cutSublist i n row =
--  let (init, rest) = splitAt i row
--      (mid , last) = splitAt n rest
--  in  (init, mid, last)

getEtaAndArity :: SplitTag -> TCM (Bool, Nat)
getEtaAndArity :: SplitTag -> TCM (Bool, Int)
getEtaAndArity (SplitCon QName
c) =
  QName -> TCMT IO ConstructorInfo
forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo QName
c TCMT IO ConstructorInfo
-> (ConstructorInfo -> (Bool, Int)) -> TCM (Bool, Int)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    DataCon Int
n           -> (Bool
False, Int
n)
    RecordCon PatternOrCopattern
_ HasEta
eta Int
n [Dom QName]
_ -> (HasEta
eta HasEta -> HasEta -> Bool
forall a. Eq a => a -> a -> Bool
== HasEta
forall a. HasEta' a
YesEta, Int
n)
getEtaAndArity (SplitLit Literal
l) = (Bool, Int) -> TCM (Bool, Int)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Int
0)
getEtaAndArity SplitTag
SplitCatchall = (Bool, Int) -> TCM (Bool, Int)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Int
1)

translateCompiledClauses
  :: forall m. (HasConstInfo m, MonadChange m)
  => CompiledClauses -> m CompiledClauses
translateCompiledClauses :: forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
translateCompiledClauses CompiledClauses
cc = m CompiledClauses -> m CompiledClauses
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (m CompiledClauses -> m CompiledClauses)
-> m CompiledClauses -> m CompiledClauses
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.cc.record" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
"translate record patterns in compiled clauses"
    , 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 a. a -> TCMT IO a
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
pretty CompiledClauses
cc
    ]
  cc <- CompiledClauses -> m CompiledClauses
loop CompiledClauses
cc
  reportSDoc "tc.cc.record" 20 $ vcat
    [ "translated compiled clauses (no eta record patterns):"
    , nest 2 $ return $ pretty cc
    ]
  cc <- recordExpressionsToCopatterns cc
  reportSDoc "tc.cc.record" 20 $ vcat
    [ "translated compiled clauses (record expressions to copatterns):"
    , nest 2 $ return $ pretty cc
    ]
  return cc
  where

    loop :: CompiledClauses -> m (CompiledClauses)
    loop :: CompiledClauses -> m CompiledClauses
loop CompiledClauses
cc = case CompiledClauses
cc of
      Fail{}    -> CompiledClauses -> m CompiledClauses
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
      Done{}    -> CompiledClauses -> m CompiledClauses
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
      Case Arg Int
i Case CompiledClauses
cs -> Arg Int -> Case CompiledClauses -> m CompiledClauses
loops Arg Int
i Case CompiledClauses
cs

    loops :: Arg Int               -- split variable
          -> Case CompiledClauses  -- original split tree
          -> m CompiledClauses
    loops :: Arg Int -> Case CompiledClauses -> m CompiledClauses
loops Arg Int
i cs :: Case CompiledClauses
cs@Branches{ projPatterns :: forall c. Case c -> Bool
projPatterns   = Bool
comatch
                       , conBranches :: forall c. Case c -> Map QName (WithArity c)
conBranches    = Map QName (WithArity CompiledClauses)
conMap
                       , etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
etaBranch      = Maybe (ConHead, WithArity CompiledClauses)
eta
                       , litBranches :: forall c. Case c -> Map Literal c
litBranches    = Map Literal CompiledClauses
litMap
                       , fallThrough :: forall c. Case c -> Maybe Bool
fallThrough    = Maybe Bool
fT
                       , catchAllBranch :: forall c. Case c -> Maybe c
catchAllBranch = Maybe CompiledClauses
catchAll
                       , lazyMatch :: forall c. Case c -> Bool
lazyMatch      = Bool
lazy } = do

      catchAll <- (CompiledClauses -> m CompiledClauses)
-> Maybe CompiledClauses -> m (Maybe CompiledClauses)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse CompiledClauses -> m CompiledClauses
loop Maybe CompiledClauses
catchAll
      litMap   <- traverse loop litMap
      (conMap, eta) <- do
        let noEtaCase = (, Maybe (ConHead, WithArity CompiledClauses)
forall a. Maybe a
Nothing) (Map QName (WithArity CompiledClauses)
 -> (Map QName (WithArity CompiledClauses),
     Maybe (ConHead, WithArity CompiledClauses)))
-> m (Map QName (WithArity CompiledClauses))
-> m (Map QName (WithArity CompiledClauses),
      Maybe (ConHead, WithArity CompiledClauses))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((WithArity CompiledClauses -> m (WithArity CompiledClauses))
-> Map QName (WithArity CompiledClauses)
-> m (Map QName (WithArity CompiledClauses))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map QName a -> f (Map QName b)
traverse ((WithArity CompiledClauses -> m (WithArity CompiledClauses))
 -> Map QName (WithArity CompiledClauses)
 -> m (Map QName (WithArity CompiledClauses)))
-> ((CompiledClauses -> m CompiledClauses)
    -> WithArity CompiledClauses -> m (WithArity CompiledClauses))
-> (CompiledClauses -> m CompiledClauses)
-> Map QName (WithArity CompiledClauses)
-> m (Map QName (WithArity CompiledClauses))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CompiledClauses -> m CompiledClauses)
-> WithArity CompiledClauses -> m (WithArity CompiledClauses)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> WithArity a -> f (WithArity b)
traverse) CompiledClauses -> m CompiledClauses
loop Map QName (WithArity CompiledClauses)
conMap
            yesEtaCase WithArity CompiledClauses
b ConHead
ch = (Map QName (WithArity CompiledClauses)
forall k a. Map k a
Map.empty,) (Maybe (ConHead, WithArity CompiledClauses)
 -> (Map QName (WithArity CompiledClauses),
     Maybe (ConHead, WithArity CompiledClauses)))
-> (WithArity CompiledClauses
    -> Maybe (ConHead, WithArity CompiledClauses))
-> WithArity CompiledClauses
-> (Map QName (WithArity CompiledClauses),
    Maybe (ConHead, WithArity CompiledClauses))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConHead, WithArity CompiledClauses)
-> Maybe (ConHead, WithArity CompiledClauses)
forall a. a -> Maybe a
Just ((ConHead, WithArity CompiledClauses)
 -> Maybe (ConHead, WithArity CompiledClauses))
-> (WithArity CompiledClauses
    -> (ConHead, WithArity CompiledClauses))
-> WithArity CompiledClauses
-> Maybe (ConHead, WithArity CompiledClauses)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConHead
ch,) (WithArity CompiledClauses
 -> (Map QName (WithArity CompiledClauses),
     Maybe (ConHead, WithArity CompiledClauses)))
-> m (WithArity CompiledClauses)
-> m (Map QName (WithArity CompiledClauses),
      Maybe (ConHead, WithArity CompiledClauses))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CompiledClauses -> m CompiledClauses)
-> WithArity CompiledClauses -> m (WithArity CompiledClauses)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> WithArity a -> f (WithArity b)
traverse CompiledClauses -> m CompiledClauses
loop WithArity CompiledClauses
b
        case Map.toList conMap of
              -- This is already an eta match. Still need to recurse though.
              -- This can happen (#2981) when we
              -- 'revisitRecordPatternTranslation' in Rules.Decl, due to
              -- inferred eta.
          [(QName, WithArity CompiledClauses)]
_ | Just (ConHead
ch, WithArity CompiledClauses
b) <- Maybe (ConHead, WithArity CompiledClauses)
eta -> WithArity CompiledClauses
-> ConHead
-> m (Map QName (WithArity CompiledClauses),
      Maybe (ConHead, WithArity CompiledClauses))
yesEtaCase WithArity CompiledClauses
b ConHead
ch
          [(QName
c, WithArity CompiledClauses
b)] | Bool -> Bool
not Bool
comatch -> -- possible eta-match
            QName -> m (Maybe ConstructorInfo)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe ConstructorInfo)
getConstructorInfo' QName
c m (Maybe ConstructorInfo)
-> (Maybe ConstructorInfo
    -> m (Map QName (WithArity CompiledClauses),
          Maybe (ConHead, WithArity CompiledClauses)))
-> m (Map QName (WithArity CompiledClauses),
      Maybe (ConHead, WithArity CompiledClauses))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
              Just (RecordCon PatternOrCopattern
pm HasEta
YesEta Int
_ar [Dom QName]
fs) -> WithArity CompiledClauses
-> ConHead
-> m (Map QName (WithArity CompiledClauses),
      Maybe (ConHead, WithArity CompiledClauses))
yesEtaCase WithArity CompiledClauses
b (ConHead
 -> m (Map QName (WithArity CompiledClauses),
       Maybe (ConHead, WithArity CompiledClauses)))
-> ConHead
-> m (Map QName (WithArity CompiledClauses),
      Maybe (ConHead, WithArity CompiledClauses))
forall a b. (a -> b) -> a -> b
$
                QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c (PatternOrCopattern -> DataOrRecord
forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
pm) Induction
Inductive ((Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom [Dom QName]
fs)
              Maybe ConstructorInfo
_ -> m (Map QName (WithArity CompiledClauses),
   Maybe (ConHead, WithArity CompiledClauses))
noEtaCase
          [(QName, WithArity CompiledClauses)]
_ -> m (Map QName (WithArity CompiledClauses),
   Maybe (ConHead, WithArity CompiledClauses))
noEtaCase
      return $ Case i cs{ conBranches    = conMap
                        , etaBranch      = eta
                        , litBranches    = litMap
                        , fallThrough    = fT
                        , catchAllBranch = catchAll
                        }


-- | Transform definitions returning record values to use copatterns instead.
--   This allows e.g. termination-checking constructor-style coinduction.
--
--   For example:
--
--   @
--     nats : Nat → Stream Nat
--     nats n = n ∷ nats (1 + n)
--   @
--
--   The clause is translated to:
--
--   @
--     nats n .head = n
--     nats n .tail = nats (1 + n)
--   @
--
--   A change is signalled if definitional equalities might not hold after the
--   translation, e.g. if a non-eta constructor was turned to copattern matching.
recordRHSsToCopatterns ::
     forall m. (MonadChange m, PureTCM m)
  => [Clause]
  -> m [Clause]
recordRHSsToCopatterns :: forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
[Clause] -> m [Clause]
recordRHSsToCopatterns [Clause]
cls = do
  [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inline.con" Int
40 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"enter recordRHSsToCopatterns with " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([Clause] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
cls) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" clauses"
  (Clause -> m [Clause]) -> [Clause] -> m [Clause]
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM Clause -> m [Clause]
forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
Clause -> m [Clause]
recordRHSToCopatterns [Clause]
cls

recordRHSToCopatterns ::
     forall m. (MonadChange m, PureTCM m)
  => Clause
  -> m [Clause]
recordRHSToCopatterns :: forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
Clause -> m [Clause]
recordRHSToCopatterns Clause
cl = do
  [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inline.con" Int
40 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"enter recordRHSToCopatterns"

  case Clause
cl of

    -- RHS must be fully applied coinductive constructor/record expression.
    cl :: Clause
cl@Clause{ namedClausePats :: Clause -> [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps
             , clauseBody :: Clause -> Maybe Term
clauseBody      = Just v0 :: Term
v0@(Con con :: ConHead
con@(ConHead QName
c DataOrRecord
_ Induction
_ind [Arg QName]
fs) ConInfo
_ci Elims
es)
             , clauseType :: Clause -> Maybe (Arg Type)
clauseType      = Maybe (Arg Type)
mt
             }
      | Bool -> Bool
not ([Arg QName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Arg QName]
fs)           -- at least one field
      , [Arg QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg QName]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es  -- fully applied
      , Just [Arg Term]
vs <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es

          -- Only expand constructors labelled @{-# INLINE c #-}@.
      -> QName -> m (Maybe Bool)
inlineConstructor QName
c m (Maybe Bool) -> (Maybe Bool -> m [Clause]) -> m [Clause]
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe Bool
Nothing  -> [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Clause
cl]
        Just Bool
eta -> do

          mt <- (Arg Type -> m (Arg Type))
-> Maybe (Arg Type) -> m (Maybe (Arg Type))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse Arg Type -> m (Arg Type)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Maybe (Arg Type)
mt

          -- If it may change definitional equality,
          -- announce that the translation actually fired.
          unless eta tellDirty

          -- Iterate the translation for nested constructor rhss.
          recordRHSsToCopatterns =<< do

            -- Create one clause per projection.
            forM (zip fs vs) $ \ (Arg QName
f, Arg Term
v) -> do

              -- Get the type of the field.
              let inst :: Type -> m (Maybe Type)
                  inst :: Type -> m (Maybe Type)
inst Type
t = ((Dom Type, Term, Type) -> Type)
-> Maybe (Dom Type, Term, Type) -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Dom Type, Term, Type) -> Type
forall a b c. (a, b, c) -> c
thd3 (Maybe (Dom Type, Term, Type) -> Maybe Type)
-> m (Maybe (Dom Type, Term, Type)) -> m (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
v0 Type
t ProjOrigin
ProjSystem (Arg QName -> QName
forall e. Arg e -> e
unArg Arg QName
f)

              let fuse :: Maybe (Arg (Maybe a)) -> Maybe (Arg a)
                  fuse :: forall a. Maybe (Arg (Maybe a)) -> Maybe (Arg a)
fuse = Maybe (Maybe (Arg a)) -> Maybe (Arg a)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe (Arg a)) -> Maybe (Arg a))
-> (Maybe (Arg (Maybe a)) -> Maybe (Maybe (Arg a)))
-> Maybe (Arg (Maybe a))
-> Maybe (Arg a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg (Maybe a) -> Maybe (Arg a))
-> Maybe (Arg (Maybe a)) -> Maybe (Maybe (Arg a))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg (Maybe a) -> Maybe (Arg a)
forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Functor m => Arg (m a) -> m (Arg a)
distributeF

              mt' :: Maybe (Arg Type) <- Maybe (Arg (Maybe Type)) -> Maybe (Arg Type)
forall a. Maybe (Arg (Maybe a)) -> Maybe (Arg a)
fuse (Maybe (Arg (Maybe Type)) -> Maybe (Arg Type))
-> m (Maybe (Arg (Maybe Type))) -> m (Maybe (Arg Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg Type -> m (Arg (Maybe Type)))
-> Maybe (Arg Type) -> m (Maybe (Arg (Maybe Type)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse ((Type -> m (Maybe Type)) -> Arg Type -> m (Arg (Maybe Type))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg b)
traverse Type -> m (Maybe Type)
inst) Maybe (Arg Type)
mt

              -- Make clause ... .f = v
              return cl
                { namedClausePats = ps ++ [ unnamed . ProjP ProjSystem <$> f ]
                , clauseBody      = Just $ unArg v
                , clauseType      = mt'
                }

    -- Otherwise: no change.
    Clause
cl -> [Clause] -> m [Clause]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Clause
cl]

  where
    -- @Nothing@ means do not inline, @Just eta@ means inline.
    inlineConstructor :: QName -> m (Maybe Bool)
    inlineConstructor :: QName -> m (Maybe Bool)
inlineConstructor QName
c = QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c m Definition -> (Definition -> Defn) -> m Defn
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Definition -> Defn
theDef m Defn -> (Defn -> m (Maybe Bool)) -> m (Maybe Bool)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Constructor { QName
conData :: QName
conData :: Defn -> QName
conData, Bool
conInline :: Bool
conInline :: Defn -> Bool
conInline } -> do
        [Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.inline.con" Int
80 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$
          ([Char]
"can" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless Bool
conInline ([Char]
"not" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
" inline constructor " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
c
        if Bool -> Bool
not Bool
conInline then Maybe Bool -> m (Maybe Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
forall a. Maybe a
Nothing else Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> m Bool -> m (Maybe Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
conData
      Defn
_ -> Maybe Bool -> m (Maybe Bool)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
forall a. Maybe a
Nothing

-- | Transform definitions returning record expressions to use copatterns
--   instead. This prevents terms from blowing up when reduced.
recordExpressionsToCopatterns
  :: (HasConstInfo m, MonadChange m)
  => CompiledClauses
  -> m CompiledClauses
recordExpressionsToCopatterns :: forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns = \case
    Case Arg Int
i Case CompiledClauses
bs -> Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Int
i (Case CompiledClauses -> CompiledClauses)
-> m (Case CompiledClauses) -> m CompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CompiledClauses -> m CompiledClauses)
-> Case CompiledClauses -> m (Case CompiledClauses)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Case a -> f (Case b)
traverse CompiledClauses -> m CompiledClauses
forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns Case CompiledClauses
bs
    cc :: CompiledClauses
cc@Fail{} -> CompiledClauses -> m CompiledClauses
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
    cc :: CompiledClauses
cc@(Done [Arg [Char]]
xs (Con ConHead
c ConInfo
co Elims
es))
      | ConInfo -> [ConInfo] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ConInfo
co [ConInfo
ConORec, ConInfo
ConORecWhere] -> do  -- don't translate if using the record /constructor/
      let vs :: [Term]
vs = (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      irrProj <- PragmaOptions -> Bool
optIrrelevantProjections (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      getConstructorInfo (conName c) >>= \ case
        RecordCon PatternOrCopattern
CopatternMatching HasEta
YesEta Int
ar [Dom QName]
fs
          | Int
ar Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0                                     -- only for eta-records with at least one field
          , [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ar                            -- where the constructor application is saturated
          , Bool
irrProj Bool -> Bool -> Bool
|| Bool -> Bool
not ((Dom QName -> Bool) -> [Dom QName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Dom QName -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant [Dom QName]
fs) -> do -- and irrelevant projections (if any) are allowed
              m ()
forall (m :: * -> *). MonadChange m => m ()
tellDirty
              Arg Int -> Case CompiledClauses -> CompiledClauses
forall a.
Arg Int -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (Int -> Arg Int
forall a. a -> Arg a
defaultArg (Int -> Arg Int) -> Int -> Arg Int
forall a b. (a -> b) -> a -> b
$ [Arg [Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg [Char]]
xs) (Case CompiledClauses -> CompiledClauses)
-> m (Case CompiledClauses) -> m CompiledClauses
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
                -- translate new cases recursively (there might be nested record expressions)
                (CompiledClauses -> m CompiledClauses)
-> Case CompiledClauses -> m (Case CompiledClauses)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Case a -> f (Case b)
traverse CompiledClauses -> m CompiledClauses
forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns (Case CompiledClauses -> m (Case CompiledClauses))
-> Case CompiledClauses -> m (Case CompiledClauses)
forall a b. (a -> b) -> a -> b
$ Branches
                  { projPatterns :: Bool
projPatterns   = Bool
True
                  , conBranches :: Map QName (WithArity CompiledClauses)
conBranches    = (WithArity CompiledClauses
 -> WithArity CompiledClauses -> WithArity CompiledClauses)
-> [(QName, WithArity CompiledClauses)]
-> Map QName (WithArity CompiledClauses)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith WithArity CompiledClauses
-> WithArity CompiledClauses -> WithArity CompiledClauses
forall a. HasCallStack => a
__IMPOSSIBLE__ ([(QName, WithArity CompiledClauses)]
 -> Map QName (WithArity CompiledClauses))
-> [(QName, WithArity CompiledClauses)]
-> Map QName (WithArity CompiledClauses)
forall a b. (a -> b) -> a -> b
$
                      (Dom QName -> Term -> (QName, WithArity CompiledClauses))
-> [Dom QName] -> [Term] -> [(QName, WithArity CompiledClauses)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Dom QName
f Term
v -> (Dom QName -> QName
forall t e. Dom' t e -> e
unDom Dom QName
f, Int -> CompiledClauses -> WithArity CompiledClauses
forall c. Int -> c -> WithArity c
WithArity Int
0 (CompiledClauses -> WithArity CompiledClauses)
-> CompiledClauses -> WithArity CompiledClauses
forall a b. (a -> b) -> a -> b
$ [Arg [Char]] -> Term -> CompiledClauses
forall a. [Arg [Char]] -> a -> CompiledClauses' a
Done [Arg [Char]]
xs Term
v)) [Dom QName]
fs [Term]
vs
                  , etaBranch :: Maybe (ConHead, WithArity CompiledClauses)
etaBranch      = Maybe (ConHead, WithArity CompiledClauses)
forall a. Maybe a
Nothing
                  , litBranches :: Map Literal CompiledClauses
litBranches    = Map Literal CompiledClauses
forall k a. Map k a
Map.empty
                  , catchAllBranch :: Maybe CompiledClauses
catchAllBranch = Maybe CompiledClauses
forall a. Maybe a
Nothing
                  , fallThrough :: Maybe Bool
fallThrough    = Maybe Bool
forall a. Maybe a
Nothing
                  , lazyMatch :: Bool
lazyMatch      = Bool
False
                  }
        ConstructorInfo
_ -> CompiledClauses -> m CompiledClauses
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
    cc :: CompiledClauses
cc@Done{} -> CompiledClauses -> m CompiledClauses
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc

---------------------------------------------------------------------------
-- * Record pattern translation for split trees
---------------------------------------------------------------------------

-- | Bottom-up procedure to record-pattern-translate split tree.
translateSplitTree :: SplitTree -> TCM SplitTree
translateSplitTree :: SplitTree -> TCM SplitTree
translateSplitTree = ([Bool], SplitTree) -> SplitTree
forall a b. (a, b) -> b
snd (([Bool], SplitTree) -> SplitTree)
-> (SplitTree -> TCMT IO ([Bool], SplitTree))
-> SplitTree
-> TCM SplitTree
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> SplitTree -> TCMT IO ([Bool], SplitTree)
loop
  where

    -- @loop t = return (xs, t')@ returns the translated split tree @t'@
    -- plus the status @xs@ of the clause variables
    --   True  = variable will never be split on in @t'@ (virgin variable)
    --   False = variable will be spilt on in @t'@
    loop :: SplitTree -> TCM ([Bool], SplitTree)
    loop :: SplitTree -> TCMT IO ([Bool], SplitTree)
loop = \case
      SplittingDone Int
n ->
        -- start with n virgin variables
        ([Bool], SplitTree) -> TCMT IO ([Bool], SplitTree)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Bool -> [Bool]
forall a. Int -> a -> [a]
replicate Int
n Bool
True, Int -> SplitTree
forall a. Int -> SplitTree' a
SplittingDone Int
n)
      SplitAt Arg Int
i LazySplit
lz SplitTrees' SplitTag
ts    -> do
        (x, xs, ts) <- Int
-> SplitTrees' SplitTag -> TCM (Bool, [Bool], SplitTrees' SplitTag)
loops (Arg Int -> Int
forall e. Arg e -> e
unArg Arg Int
i) SplitTrees' SplitTag
ts
        -- if we case on record constructor, drop case
        let t' = if Bool
x then
                   case SplitTrees' SplitTag
ts of
                     [(SplitTag
c,SplitTree
t)] -> SplitTree
t
                     SplitTrees' SplitTag
_       -> SplitTree
forall a. HasCallStack => a
__IMPOSSIBLE__
                  -- else retain case
                  else Arg Int -> LazySplit -> SplitTrees' SplitTag -> SplitTree
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
i LazySplit
lz SplitTrees' SplitTag
ts
        return (xs, t')

    -- @loops i ts = return (x, xs, ts')@ cf. @loop@
    -- @x@ says wether at arg @i@ we have a record pattern split
    -- that can be removed
    loops :: Int -> SplitTrees -> TCM (Bool, [Bool], SplitTrees)
    loops :: Int
-> SplitTrees' SplitTag -> TCM (Bool, [Bool], SplitTrees' SplitTag)
loops Int
i SplitTrees' SplitTag
ts = do
      -- note: ts not empty
      (rs, xss, ts) <- [(Bool, [Bool], (SplitTag, SplitTree))]
-> ([Bool], [[Bool]], SplitTrees' SplitTag)
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([(Bool, [Bool], (SplitTag, SplitTree))]
 -> ([Bool], [[Bool]], SplitTrees' SplitTag))
-> TCMT IO [(Bool, [Bool], (SplitTag, SplitTree))]
-> TCMT IO ([Bool], [[Bool]], SplitTrees' SplitTag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        SplitTrees' SplitTag
-> ((SplitTag, SplitTree)
    -> TCMT IO (Bool, [Bool], (SplitTag, SplitTree)))
-> TCMT IO [(Bool, [Bool], (SplitTag, SplitTree))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM SplitTrees' SplitTag
ts (((SplitTag, SplitTree)
  -> TCMT IO (Bool, [Bool], (SplitTag, SplitTree)))
 -> TCMT IO [(Bool, [Bool], (SplitTag, SplitTree))])
-> ((SplitTag, SplitTree)
    -> TCMT IO (Bool, [Bool], (SplitTag, SplitTree)))
-> TCMT IO [(Bool, [Bool], (SplitTag, SplitTree))]
forall a b. (a -> b) -> a -> b
$ \ (SplitTag
c, SplitTree
t) -> do
          (xs, t) <- SplitTree -> TCMT IO ([Bool], SplitTree)
loop SplitTree
t
          (isRC, n) <- getEtaAndArity c
          -- now drop variables from i to i+n-1
          let (xs0, rest) = splitAt i xs
              (xs1, xs2)  = splitAt n rest
              -- if all dropped variables are virgins and we are record cons.
              -- then new variable x is also virgin
              -- and we can translate away the split
              x           = Bool
isRC Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
xs1
              -- xs' = updated variables
              xs'         = [Bool]
xs0 [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool
x Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: [Bool]
xs2
              -- delete splits from t if record match
              t'          = if Bool
x then Int -> Int -> SplitTree -> SplitTree
forall a. DropFrom a => Int -> Int -> a -> a
dropFrom Int
i (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) SplitTree
t else SplitTree
t
          return (x, xs', (c, t'))
      -- x = did we split on a record constructor?
      let x = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
rs
      -- invariant: if record constructor, then exactly one constructor
      if x then unless (rs == [True]) __IMPOSSIBLE__
      -- else no record constructor
       else when (or rs) __IMPOSSIBLE__
      return (x, conjColumns xss, ts)

-- | @dropFrom i n@ drops arguments @j@  with @j < i + n@ and @j >= i@.
--   NOTE: @n@ can be negative, in which case arguments are inserted.
class DropFrom a where
  dropFrom :: Int -> Int -> a -> a

instance DropFrom (SplitTree' c) where
  dropFrom :: Int -> Int -> SplitTree' c -> SplitTree' c
dropFrom Int
i Int
n = \case
    SplittingDone Int
m -> Int -> SplitTree' c
forall a. Int -> SplitTree' a
SplittingDone (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n)
    SplitAt x :: Arg Int
x@(Arg ArgInfo
ai Int
j) LazySplit
lz SplitTrees' c
ts
      | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n -> Arg Int -> LazySplit -> SplitTrees' c -> SplitTree' c
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt (ArgInfo -> Int -> Arg Int
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Int -> Arg Int) -> Int -> Arg Int
forall a b. (a -> b) -> a -> b
$ Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) LazySplit
lz (SplitTrees' c -> SplitTree' c) -> SplitTrees' c -> SplitTree' c
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SplitTrees' c -> SplitTrees' c
forall a. DropFrom a => Int -> Int -> a -> a
dropFrom Int
i Int
n SplitTrees' c
ts
      | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i      -> Arg Int -> LazySplit -> SplitTrees' c -> SplitTree' c
forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
x LazySplit
lz (SplitTrees' c -> SplitTree' c) -> SplitTrees' c -> SplitTree' c
forall a b. (a -> b) -> a -> b
$ Int -> Int -> SplitTrees' c -> SplitTrees' c
forall a. DropFrom a => Int -> Int -> a -> a
dropFrom Int
i Int
n SplitTrees' c
ts
      | Bool
otherwise  -> SplitTree' c
forall a. HasCallStack => a
__IMPOSSIBLE__

instance DropFrom (c, SplitTree' c) where
  dropFrom :: Int -> Int -> (c, SplitTree' c) -> (c, SplitTree' c)
dropFrom Int
i Int
n (c
c, SplitTree' c
t) = (c
c, Int -> Int -> SplitTree' c -> SplitTree' c
forall a. DropFrom a => Int -> Int -> a -> a
dropFrom Int
i Int
n SplitTree' c
t)

instance DropFrom a => DropFrom [a] where
  dropFrom :: Int -> Int -> [a] -> [a]
dropFrom Int
i Int
n [a]
ts = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> a -> a
forall a. DropFrom a => Int -> Int -> a -> a
dropFrom Int
i Int
n) [a]
ts