    -- | 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.Functions ( etaExpandClause )
    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 qualified Agda.Utils.SmallSet as SmallSet
    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)
      => QName
      -> CompiledClauses
      -> m CompiledClauses
    translateCompiledClauses :: forall (m :: * -> *).
    (HasConstInfo m, MonadChange m) =>
    QName -> CompiledClauses -> m CompiledClauses
    translateCompiledClauses QName
    defn 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
        ]

      -- If the function these clauses belong to is marked INLINE then we do
      -- not perform record expression to copattern translation.
      isinl <- isInlineFun . theDef <$> getConstInfo defn
      if
        | isinl -> cc <$ do
          reportSDoc "tc.cc.record" 20 $ "record expressions to copatterns skipped because" <+> prettyTCM defn <+> "is inline"
        | otherwise -> do
          cc <- recordExpressionsToCopatterns cc
          reportSDoc "tc.cc.record" 20 $ vcat
            [ "translated compiled clauses (record expressions to copatterns):"
            , nest 2 $ return $ pretty cc
            ]
          pure 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
    cl0 = 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"

      Clause -> m Clause
    forall (tcm :: * -> *). PureTCM tcm => Clause -> tcm Clause
    etaExpandClause Clause
    cl0 m Clause -> (Clause -> 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

        -- 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
    cl0]
            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

                  reportSDoc "tc.inline.con" 50 $ vcat
                    [ "for field" <+> prettyTCM (unArg f) <+> ": "
                    , "  mt  =" <+> prettyTCM mt
                    , "  mt' =" <+> prettyTCM mt'
                    ]

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

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

      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
    ConORec Elims
    es)) -> 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 whether 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