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

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

    import Control.Arrow          ( first, second )
    import Control.Monad          ( forM, unless, when, zipWithM )
    import Control.Monad.Fix      ( mfix )
    import Control.Monad.IO.Class ( MonadIO(..) )
    import Control.Monad.Reader   ( MonadReader(..), ReaderT(..), runReaderT )
    import Control.Monad.State    ( MonadState(..), StateT(..), runStateT )
    import Control.Monad.Trans    ( lift )

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

    import Agda.Syntax.Common
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.Pattern as I

    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.Functor
    import Agda.Utils.Permutation hiding (dropFrom)
    import Agda.Utils.Pretty (Pretty(..))
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.Size
    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 (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 NAPs
    ps -> do
          Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    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
          PatVarName -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.rec" Nat
    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: "
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    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
    prettyTCM Type
    t
            ]
          PatVarName -> Nat -> PatVarName -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Nat -> PatVarName -> m ()
    reportSLn PatVarName
    "tc.rec" Nat
    70 (PatVarName -> TCMT IO ()) -> PatVarName -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ PatVarName
    "  type raw: " PatVarName -> PatVarName -> PatVarName
    forall a. [a] -> [a] -> [a]
    ++ Type -> PatVarName
    forall a. Show a => a -> PatVarName
    show Type
    t
          [Dom QName]
    fields <- Type -> TCM [Dom QName]
    getRecordTypeFields Type
    t
          [[Term -> Term]] -> [Term -> Term]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Term -> Term]] -> [Term -> Term])
    -> TCMT IO [[Term -> Term]] -> TCM [Term -> Term]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Term -> Term) -> DeBruijnPattern -> TCM [Term -> Term])
    -> [Term -> Term] -> [DeBruijnPattern] -> TCMT IO [[Term -> Term]]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (Term -> Term) -> DeBruijnPattern -> TCM [Term -> Term]
    comb ((Dom QName -> Term -> Term) -> [Dom QName] -> [Term -> Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom QName -> Term -> Term
    forall {t} {t}. Apply t => Dom' t QName -> t -> t
    proj [Dom QName]
    fields) ((Arg (Named_ DeBruijnPattern) -> DeBruijnPattern)
    -> NAPs -> [DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
    forall a. NamedArg a -> a
    namedArg NAPs
    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 (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, Nat)
    getEtaAndArity (SplitCon QName
    c) =
      TCMT IO ConstructorInfo
    -> (ConstructorInfo -> (Bool, Nat)) -> TCM (Bool, Nat)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for (QName -> TCMT IO ConstructorInfo
    forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
    getConstructorInfo QName
    c) ((ConstructorInfo -> (Bool, Nat)) -> TCM (Bool, Nat))
    -> (ConstructorInfo -> (Bool, Nat)) -> TCM (Bool, Nat)
    forall a b. (a -> b) -> a -> b
    $ \case
        DataCon Nat
    n        -> (Bool
    False, Nat
    n)
        RecordCon PatternOrCopattern
    _ HasEta
    eta [Dom QName]
    fs -> (HasEta
    eta HasEta -> HasEta -> Bool
    forall a. Eq a => a -> a -> Bool
    == HasEta
    forall a. HasEta' a
    YesEta, [Dom QName] -> Nat
    forall a. Sized a => a -> Nat
    size [Dom QName]
    fs)
    getEtaAndArity (SplitLit Literal
    l) = (Bool, Nat) -> TCM (Bool, Nat)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, Nat
    0)
    getEtaAndArity SplitTag
    SplitCatchall = (Bool, Nat) -> TCM (Bool, Nat)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    False, Nat
    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
      PatVarName -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.cc.record" Nat
    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"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    pretty CompiledClauses
    cc
        ]
      CompiledClauses
    cc <- CompiledClauses -> m CompiledClauses
    loop CompiledClauses
    cc
      PatVarName -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.cc.record" Nat
    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
    "translated compiled clauses (no eta record patterns):"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    pretty CompiledClauses
    cc
        ]
      CompiledClauses
    cc <- CompiledClauses -> m CompiledClauses
    forall (m :: * -> *).
    (HasConstInfo m, MonadChange m) =>
    CompiledClauses -> m CompiledClauses
    recordExpressionsToCopatterns CompiledClauses
    cc
      PatVarName -> Nat -> TCMT IO Doc -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.cc.record" Nat
    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
    "translated compiled clauses (record expressions to copatterns):"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> TCMT IO Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ CompiledClauses -> Doc
    forall a. Pretty a => a -> Doc
    pretty CompiledClauses
    cc
        ]
      CompiledClauses -> m CompiledClauses
    forall (m :: * -> *) a. Monad m => a -> m a
    return CompiledClauses
    cc
      where

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

        loops :: Arg Int               -- split variable
              -> Case CompiledClauses  -- original split tree
              -> m CompiledClauses
        loops :: Arg Nat -> Case CompiledClauses -> m CompiledClauses
    loops Arg Nat
    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

          Maybe CompiledClauses
    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)
    traverse CompiledClauses -> m CompiledClauses
    loop Maybe CompiledClauses
    catchAll
          Map Literal CompiledClauses
    litMap   <- (CompiledClauses -> m CompiledClauses)
    -> Map Literal CompiledClauses -> m (Map Literal CompiledClauses)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse CompiledClauses -> m CompiledClauses
    loop Map Literal CompiledClauses
    litMap
          (Map QName (WithArity CompiledClauses)
    conMap, Maybe (ConHead, WithArity CompiledClauses)
    eta) <- do
            let noEtaCase :: m (Map QName (WithArity CompiledClauses),
       Maybe (ConHead, WithArity CompiledClauses))
    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)
    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)
    traverse) CompiledClauses -> m CompiledClauses
    loop Map QName (WithArity CompiledClauses)
    conMap
                yesEtaCase :: WithArity CompiledClauses
    -> ConHead
    -> m (Map QName (WithArity CompiledClauses),
          Maybe (ConHead, WithArity CompiledClauses))
    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)
    traverse CompiledClauses -> m CompiledClauses
    loop WithArity CompiledClauses
    b
            case Map QName (WithArity CompiledClauses)
    -> [(QName, WithArity CompiledClauses)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map QName (WithArity CompiledClauses)
    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 ConstructorInfo
    forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
    getConstructorInfo QName
    c m ConstructorInfo
    -> (ConstructorInfo
        -> m (Map QName (WithArity CompiledClauses),
              Maybe (ConHead, WithArity CompiledClauses)))
    -> m (Map QName (WithArity CompiledClauses),
          Maybe (ConHead, WithArity CompiledClauses))
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ case
                  RecordCon PatternOrCopattern
    pm HasEta
    YesEta [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
    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)
                  ConstructorInfo
    _ -> m (Map QName (WithArity CompiledClauses),
       Maybe (ConHead, WithArity CompiledClauses))
    noEtaCase
              [(QName, WithArity CompiledClauses)]
    _ -> m (Map QName (WithArity CompiledClauses),
       Maybe (ConHead, WithArity CompiledClauses))
    noEtaCase
          CompiledClauses -> m CompiledClauses
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CompiledClauses -> m CompiledClauses)
    -> CompiledClauses -> m CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ Arg Nat -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Nat -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case Arg Nat
    i Case CompiledClauses
    cs{ conBranches :: Map QName (WithArity CompiledClauses)
    conBranches    = Map QName (WithArity CompiledClauses)
    conMap
                            , etaBranch :: Maybe (ConHead, WithArity CompiledClauses)
    etaBranch      = Maybe (ConHead, WithArity CompiledClauses)
    eta
                            , litBranches :: Map Literal CompiledClauses
    litBranches    = Map Literal CompiledClauses
    litMap
                            , fallThrough :: Maybe Bool
    fallThrough    = Maybe Bool
    fT
                            , catchAllBranch :: Maybe CompiledClauses
    catchAllBranch = Maybe CompiledClauses
    catchAll
                            }

    {- UNUSED
    instance Monoid CompiledClauses where
      mempty = __IMPOSSIBLE__
      mappend (Case n c) (Case n' c') | n == n' = Case n $ mappend c c'
      mappend _ _ = __IMPOSSIBLE__

    mergeCatchAll :: CompiledClauses -> Maybe CompiledClauses -> CompiledClauses
    mergeCatchAll cc ca = maybe cc (mappend cc) ca
    {-
      case (cc, ca) of
        (_       , Nothing) -> cc
        (Case n c, Just (Case n' c')) | n == n' -> Case n $ mappend c c'
        _                   -> __IMPOSSIBLE__ -- this would mean non-determinism
    -}
    -}

    -- | 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 Nat
    i Case CompiledClauses
    bs -> Arg Nat -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Nat -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case Arg Nat
    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)
    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 (m :: * -> *) a. Monad m => a -> m a
    return CompiledClauses
    cc
        cc :: CompiledClauses
    cc@(Done [Arg PatVarName]
    xs (Con ConHead
    c ConOrigin
    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
          Constructor{ conArity :: Defn -> Nat
    conArity = Nat
    ar } <- Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (ConHead -> QName
    conName ConHead
    c)
          Bool
    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
          QName -> m ConstructorInfo
    forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
    getConstructorInfo (ConHead -> QName
    conName ConHead
    c) m ConstructorInfo
    -> (ConstructorInfo -> m CompiledClauses) -> m CompiledClauses
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ case
            RecordCon PatternOrCopattern
    CopatternMatching HasEta
    YesEta [Dom QName]
    fs
              | Nat
    ar <- [Dom QName] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Dom QName]
    fs, Nat
    ar Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    0,                   -- only for eta-records with at least one field
                [Term] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Term]
    vs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    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 Nat -> Case CompiledClauses -> CompiledClauses
    forall a.
    Arg Nat -> Case (CompiledClauses' a) -> CompiledClauses' a
    Case (Nat -> Arg Nat
    forall a. a -> Arg a
    defaultArg (Nat -> Arg Nat) -> Nat -> Arg Nat
    forall a b. (a -> b) -> a -> b
    $ [Arg PatVarName] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Arg PatVarName]
    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)
    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 :: forall c.
    Bool
    -> Map QName (WithArity c)
    -> Maybe (ConHead, WithArity c)
    -> Map Literal c
    -> Maybe c
    -> Maybe Bool
    -> Bool
    -> Case c
    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, Nat -> CompiledClauses -> WithArity CompiledClauses
    forall c. Nat -> c -> WithArity c
    WithArity Nat
    0 (CompiledClauses -> WithArity CompiledClauses)
    -> CompiledClauses -> WithArity CompiledClauses
    forall a b. (a -> b) -> a -> b
    $ [Arg PatVarName] -> Term -> CompiledClauses
    forall a. [Arg PatVarName] -> a -> CompiledClauses' a
    Done [Arg PatVarName]
    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 (m :: * -> *) a. Monad m => a -> m a
    return CompiledClauses
    cc
        cc :: CompiledClauses
    cc@Done{} -> CompiledClauses -> m CompiledClauses
    forall (m :: * -> *) a. Monad m => a -> m a
    return CompiledClauses
    cc

    -- UNUSED Liang-Ting Chen 2019-07-16
    ---- | @replaceByProjections i projs cc@ replaces variables @i..i+n-1@
    ----   (counted from left) by projections @projs_1 i .. projs_n i@.
    ----
    ----   If @n==0@, we matched on a zero-field record, which means that
    ----   we are actually introduce a new variable, increasing split
    ----   positions greater or equal to @i@ by one.
    ----   Otherwise, we have to lower
    ----
    --replaceByProjections :: Arg Int -> [QName] -> CompiledClauses -> CompiledClauses
    --replaceByProjections (Arg ai i) projs cc =
    --  let n = length projs
    --
    --      loop :: Int -> CompiledClauses -> CompiledClauses
    --      loop i cc = case cc of
    --        Case j cs
    --
    --        -- if j < i, we leave j untouched, but we increase i by the number
    --        -- of variables replacing j in the branches
    --          | unArg j < i -> Case j $ loops i cs
    --
    --        -- if j >= i then we shrink j by (n-1)
    --          | otherwise   -> Case (j <&> \ k -> k - (n-1)) $ fmap (loop i) cs
    --
    --        Done xs v ->
    --        -- we have to delete (n-1) variables from xs
    --        -- and instantiate v suitably with the projections
    --          let (xs0,xs1,xs2)     = cutSublist i n xs
    --              names | null xs1  = ["r"]
    --                    | otherwise = map unArg xs1
    --              x                 = Arg ai $ foldr1 appendArgNames names
    --              xs'               = xs0 ++ x : xs2
    --              us                = map (\ p -> Var 0 [Proj ProjSystem p]) (reverse projs)
    --              -- go from level (i + n - 1) to index (subtract from |xs|-1)
    --              index             = length xs - (i + n)
    --          in  Done xs' $ applySubst (liftS (length xs2) $ us ++# raiseS 1) v
    --          -- The body is NOT guarded by lambdas!
    --          -- WRONG: underLambdas i (flip apply) (map defaultArg us) v
    --
    --        Fail -> Fail
    --
    --      loops :: Int -> Case CompiledClauses -> Case CompiledClauses
    --      loops i bs@Branches{ conBranches    = conMap
    --                         , litBranches    = litMap
    --                         , catchAllBranch = catchAll } =
    --        bs{ conBranches    = fmap (\ (WithArity n c) -> WithArity n $ loop (i + n - 1) c) conMap
    --          , litBranches    = fmap (loop (i - 1)) litMap
    --          , catchAllBranch = fmap (loop i) catchAll
    --          }
    --  in  loop i cc

    -- UNUSED Liang-Ting 2019-07-16
    ---- | Check if a split is on a record constructor, and return the projections
    ----   if yes.
    --isRecordCase :: Case c -> TCM (Maybe ([QName], c))
    --isRecordCase (Branches { conBranches = conMap
    --                       , litBranches = litMap
    --                       , catchAllBranch = Nothing })
    --  | Map.null litMap
    --  , [(con, WithArity _ br)] <- Map.toList conMap = do
    --    isRC <- isRecordConstructor con
    --    case isRC of
    --      Just (r, Record { recFields = fs }) -> return $ Just (map unArg fs, br)
    --      Just (r, _) -> __IMPOSSIBLE__
    --      Nothing -> return Nothing
    --isRecordCase _ = return Nothing

    ---------------------------------------------------------------------------
    -- * Record pattern translation for split trees
    ---------------------------------------------------------------------------
    --UNUSED Liang-Ting Chen 2019-07-16
    ---- | Split tree annotation.
    --data RecordSplitNode = RecordSplitNode
    --  { _splitTag           :: SplitTag -- ^ Constructor name/literal for this branch.
    --  , _splitArity         :: Int      -- ^ Arity of the constructor.
    --  , _splitRecordPattern :: Bool     -- ^ Should we translate this split away?
    --  }

    -- | Split tree annotated for record pattern translation.
    --type RecordSplitTree  = SplitTree' RecordSplitNode
    --type RecordSplitTrees = SplitTrees' RecordSplitNode

    --UNUSED Liang-Ting Chen 2019-07-16
    ---- | Bottom-up procedure to annotate split tree.
    --recordSplitTree :: SplitTree -> TCM RecordSplitTree
    --recordSplitTree = snd <.> loop
    --  where
    --
    --    loop :: SplitTree -> TCM ([Bool], RecordSplitTree)
    --    loop = \case
    --      SplittingDone n -> return (replicate n True, SplittingDone n)
    --      SplitAt i ts    -> do
    --        (xs, ts) <- loops (unArg i) ts
    --        return (xs, SplitAt i ts)
    --
    --    loops :: Int -> SplitTrees -> TCM ([Bool], RecordSplitTrees)
    --    loops i ts = do
    --      (xss, ts) <- unzip <$> do
    --        forM ts $ \ (c, t) -> do
    --          (xs, t) <- loop t
    --          (isRC, n) <- getEtaAndArity c
    --          let (xs0, rest) = splitAt i xs
    --              (xs1, xs2)  = splitAt n rest
    --              x           = isRC && and xs1
    --              xs'         = xs0 ++ x : xs2
    --          return (xs, (RecordSplitNode c n x, t))
    --      return (foldl1 (zipWith (&&)) xss, ts)

    -- | 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 Nat
    n ->
            -- start with n virgin variables
            ([Bool], SplitTree) -> TCMT IO ([Bool], SplitTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Nat -> Bool -> [Bool]
    forall a. Nat -> a -> [a]
    replicate Nat
    n Bool
    True, Nat -> SplitTree
    forall a. Nat -> SplitTree' a
    SplittingDone Nat
    n)
          SplitAt Arg Nat
    i LazySplit
    lz SplitTrees' SplitTag
    ts    -> do
            (Bool
    x, [Bool]
    xs, SplitTrees' SplitTag
    ts) <- Nat
    -> SplitTrees' SplitTag -> TCM (Bool, [Bool], SplitTrees' SplitTag)
    loops (Arg Nat -> Nat
    forall e. Arg e -> e
    unArg Arg Nat
    i) SplitTrees' SplitTag
    ts
            -- if we case on record constructor, drop case
            let t' :: SplitTree
    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 Nat -> LazySplit -> SplitTrees' SplitTag -> SplitTree
    forall a. Arg Nat -> LazySplit -> SplitTrees' a -> SplitTree' a
    SplitAt Arg Nat
    i LazySplit
    lz SplitTrees' SplitTag
    ts
            ([Bool], SplitTree) -> TCMT IO ([Bool], SplitTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Bool]
    xs, SplitTree
    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 :: Nat
    -> SplitTrees' SplitTag -> TCM (Bool, [Bool], SplitTrees' SplitTag)
    loops Nat
    i SplitTrees' SplitTag
    ts = do
          -- note: ts not empty
          ([Bool]
    rs, [[Bool]]
    xss, SplitTrees' SplitTag
    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
              ([Bool]
    xs, SplitTree
    t) <- SplitTree -> TCMT IO ([Bool], SplitTree)
    loop SplitTree
    t
              (Bool
    isRC, Nat
    n) <- SplitTag -> TCM (Bool, Nat)
    getEtaAndArity SplitTag
    c
              -- now drop variables from i to i+n-1
              let ([Bool]
    xs0, [Bool]
    rest) = Nat -> [Bool] -> ([Bool], [Bool])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt Nat
    i [Bool]
    xs
                  ([Bool]
    xs1, [Bool]
    xs2)  = Nat -> [Bool] -> ([Bool], [Bool])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt Nat
    n [Bool]
    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
    x           = Bool
    isRC Bool -> Bool -> Bool
    && [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and [Bool]
    xs1
                  -- xs' = updated variables
                  xs' :: [Bool]
    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' :: SplitTree
    t'          = if Bool
    x then Nat -> Nat -> SplitTree -> SplitTree
    forall a. DropFrom a => Nat -> Nat -> a -> a
    dropFrom Nat
    i (Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1) SplitTree
    t else SplitTree
    t
              (Bool, [Bool], (SplitTag, SplitTree))
    -> TCMT IO (Bool, [Bool], (SplitTag, SplitTree))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    x, [Bool]
    xs', (SplitTag
    c, SplitTree
    t'))
          -- x = did we split on a record constructor?
          let x :: Bool
    x = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and [Bool]
    rs
          -- invariant: if record constructor, then exactly one constructor
          if Bool
    x then Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([Bool]
    rs [Bool] -> [Bool] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Bool
    True]) TCMT IO ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          -- else no record constructor
           else Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ([Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    or [Bool]
    rs) TCMT IO ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          (Bool, [Bool], SplitTrees' SplitTag)
    -> TCM (Bool, [Bool], SplitTrees' SplitTag)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool
    x, [[Bool]] -> [Bool]
    conjColumns [[Bool]]
    xss, SplitTrees' SplitTag
    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 :: Nat -> Nat -> SplitTree' c -> SplitTree' c
    dropFrom Nat
    i Nat
    n = \case
        SplittingDone Nat
    m -> Nat -> SplitTree' c
    forall a. Nat -> SplitTree' a
    SplittingDone (Nat
    m Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n)
        SplitAt x :: Arg Nat
    x@(Arg ArgInfo
    ai Nat
    j) LazySplit
    lz SplitTrees' c
    ts
          | Nat
    j Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    n -> Arg Nat -> LazySplit -> SplitTrees' c -> SplitTree' c
    forall a. Arg Nat -> LazySplit -> SplitTrees' a -> SplitTree' a
    SplitAt (ArgInfo -> Nat -> Arg Nat
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    ai (Nat -> Arg Nat) -> Nat -> Arg Nat
    forall a b. (a -> b) -> a -> b
    $ Nat
    j Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n) LazySplit
    lz (SplitTrees' c -> SplitTree' c) -> SplitTrees' c -> SplitTree' c
    forall a b. (a -> b) -> a -> b
    $ Nat -> Nat -> SplitTrees' c -> SplitTrees' c
    forall a. DropFrom a => Nat -> Nat -> a -> a
    dropFrom Nat
    i Nat
    n SplitTrees' c
    ts
          | Nat
    j Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    i      -> Arg Nat -> LazySplit -> SplitTrees' c -> SplitTree' c
    forall a. Arg Nat -> LazySplit -> SplitTrees' a -> SplitTree' a
    SplitAt Arg Nat
    x LazySplit
    lz (SplitTrees' c -> SplitTree' c) -> SplitTrees' c -> SplitTree' c
    forall a b. (a -> b) -> a -> b
    $ Nat -> Nat -> SplitTrees' c -> SplitTrees' c
    forall a. DropFrom a => Nat -> Nat -> a -> a
    dropFrom Nat
    i Nat
    n SplitTrees' c
    ts
          | Bool
    otherwise  -> SplitTree' c
    forall a. HasCallStack => a
    __IMPOSSIBLE__

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

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

    {-
    -- | Check if a split is on a record constructor, and return the projections
    --   if yes.
    isRecordSplit :: SplitTrees -> TCM (Maybe ([QName], c))
    isRecordSplit (Branches { conBranches = conMap
                           , litBranches = litMap
                           , catchAllBranch = Nothing })
      | Map.null litBranches
      , [(con,br)] <- Map.toList conMap = do
        isRC <- isRecordConstructor con
        case isRC of
          Just (r, Record { recFields = fs }) -> return $ Just (map unArg fs, br)
          Just (r, _) -> __IMPOSSIBLE__
          Nothing -> return Nothing
    isRecordSplit _ = return Nothing

    -}

    ---------------------------------------------------------------------------
    -- * Record pattern translation for function definitions
    ---------------------------------------------------------------------------

    -- | Replaces pattern matching on record constructors with uses of
    -- projection functions. Does not remove record constructor patterns
    -- which have sub-patterns containing non-record constructor or
    -- literal patterns.

    translateRecordPatterns :: Clause -> TCM Clause
    translateRecordPatterns :: Clause -> TCM Clause
    translateRecordPatterns Clause
    clause = do
      -- ps: New patterns, in left-to-right order, in the context of the
      -- old RHS.

      -- s: Partial substitution taking the old pattern variables
      -- (including dot patterns; listed from left to right) to terms in
      -- the context of the new RHS.

      -- cs: List of changes, with types in the context of the old
      -- telescope.

      ([NamedArg Pattern]
    ps, [Term]
    s, Changes
    cs) <- RecPatM ([NamedArg Pattern], [Term], Changes)
    -> TCM ([NamedArg Pattern], [Term], Changes)
    forall a. RecPatM a -> TCM a
    runRecPatM (RecPatM ([NamedArg Pattern], [Term], Changes)
     -> TCM ([NamedArg Pattern], [Term], Changes))
    -> RecPatM ([NamedArg Pattern], [Term], Changes)
    -> TCM ([NamedArg Pattern], [Term], Changes)
    forall a b. (a -> b) -> a -> b
    $ [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
    translatePatterns ([NamedArg Pattern]
     -> RecPatM ([NamedArg Pattern], [Term], Changes))
    -> [NamedArg Pattern]
    -> RecPatM ([NamedArg Pattern], [Term], Changes)
    forall a b. (a -> b) -> a -> b
    $ NAPs -> [NamedArg Pattern]
    forall a b. LabelPatVars a b => b -> a
    unnumberPatVars (NAPs -> [NamedArg Pattern]) -> NAPs -> [NamedArg Pattern]
    forall a b. (a -> b) -> a -> b
    $ Clause -> NAPs
    namedClausePats Clause
    clause

      let -- Number of variables + dot patterns in new clause.
          noNewPatternVars :: Nat
    noNewPatternVars = Changes -> Nat
    forall a. Sized a => a -> Nat
    size Changes
    cs

          s' :: [Term]
    s'   = [Term] -> [Term]
    forall a. [a] -> [a]
    reverse [Term]
    s
          mkSub :: [Term] -> Substitution' Term
    mkSub [Term]
    s = [Term]
    s [Term] -> Substitution' Term -> Substitution' Term
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Nat -> Substitution' Term
    forall a. Nat -> Substitution' a
    raiseS Nat
    noNewPatternVars

          -- Substitution used to convert terms in the old RHS's
          -- context to terms in the new RHS's context.
          rhsSubst :: Substitution' Term
    rhsSubst = [Term] -> Substitution' Term
    mkSub [Term]
    s' -- NB:: Defined but not used

          -- Substitution used to convert terms in the old telescope's
          -- context to terms in the new RHS's context.
          perm :: Permutation
    perm = Permutation -> Maybe Permutation -> Permutation
    forall a. a -> Maybe a -> a
    fromMaybe Permutation
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Permutation -> Permutation)
    -> Maybe Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Permutation
    clausePerm Clause
    clause
          rhsSubst' :: Substitution' Term
    rhsSubst' = [Term] -> Substitution' Term
    mkSub ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ Permutation -> [Term] -> [Term]
    forall a. Permutation -> [a] -> [a]
    permute (Permutation -> Permutation
    reverseP Permutation
    perm) [Term]
    s'
          -- TODO: Is it OK to replace the definition above with the
          -- following one?
          --
          --   rhsSubst' = mkSub $ permute (clausePerm clause) s

          -- The old telescope, flattened and in textual left-to-right
          -- order (i.e. the type signature for the variable which occurs
          -- first in the list of patterns comes first).
          flattenedOldTel :: [(PatVarName, Dom Type)]
    flattenedOldTel =
            Permutation -> [(PatVarName, Dom Type)] -> [(PatVarName, Dom Type)]
    forall a. Permutation -> [a] -> [a]
    permute (Nat -> Permutation -> Permutation
    invertP Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Permutation -> Permutation) -> Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $ Permutation -> Permutation
    compactP Permutation
    perm) ([(PatVarName, Dom Type)] -> [(PatVarName, Dom Type)])
    -> [(PatVarName, Dom Type)] -> [(PatVarName, Dom Type)]
    forall a b. (a -> b) -> a -> b
    $
            [PatVarName] -> [Dom Type] -> [(PatVarName, Dom Type)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Telescope -> [PatVarName]
    teleNames (Telescope -> [PatVarName]) -> Telescope -> [PatVarName]
    forall a b. (a -> b) -> a -> b
    $ Clause -> Telescope
    clauseTel Clause
    clause) ([Dom Type] -> [(PatVarName, Dom Type)])
    -> [Dom Type] -> [(PatVarName, Dom Type)]
    forall a b. (a -> b) -> a -> b
    $
            Telescope -> [Dom Type]
    forall a. TermSubst a => Tele (Dom a) -> [Dom a]
    flattenTel (Telescope -> [Dom Type]) -> Telescope -> [Dom Type]
    forall a b. (a -> b) -> a -> b
    $
            Clause -> Telescope
    clauseTel Clause
    clause

          -- The new telescope, still flattened, with types in the context
          -- of the new RHS, in textual left-to-right order, and with
          -- Nothing in place of dot patterns.
          substTel :: Substitution' (SubstArg (Dom Type))
    -> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
    substTel = (Maybe (d, Dom Type) -> Maybe (d, Dom Type))
    -> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Maybe (d, Dom Type) -> Maybe (d, Dom Type))
     -> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)])
    -> (Substitution' (SubstArg (Dom Type))
        -> Maybe (d, Dom Type) -> Maybe (d, Dom Type))
    -> Substitution' (SubstArg (Dom Type))
    -> [Maybe (d, Dom Type)]
    -> [Maybe (d, Dom Type)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((d, Dom Type) -> (d, Dom Type))
    -> Maybe (d, Dom Type) -> Maybe (d, Dom Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (((d, Dom Type) -> (d, Dom Type))
     -> Maybe (d, Dom Type) -> Maybe (d, Dom Type))
    -> (Substitution' (SubstArg (Dom Type))
        -> (d, Dom Type) -> (d, Dom Type))
    -> Substitution' (SubstArg (Dom Type))
    -> Maybe (d, Dom Type)
    -> Maybe (d, Dom Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Dom Type -> Dom Type) -> (d, Dom Type) -> (d, Dom Type)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ((Dom Type -> Dom Type) -> (d, Dom Type) -> (d, Dom Type))
    -> (Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type)
    -> Substitution' (SubstArg (Dom Type))
    -> (d, Dom Type)
    -> (d, Dom Type)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Substitution' (SubstArg (Dom Type)) -> Dom Type -> Dom Type
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst
          newTel' :: [Maybe (PatVarName, Dom Type)]
    newTel' =
            Substitution' (SubstArg (Dom Type))
    -> [Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall {d}.
    Substitution' (SubstArg (Dom Type))
    -> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
    substTel Substitution' Term
    Substitution' (SubstArg (Dom Type))
    rhsSubst' ([Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)])
    -> [Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall a b. (a -> b) -> a -> b
    $
            Changes
    -> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    translateTel Changes
    cs ([(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)])
    -> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall a b. (a -> b) -> a -> b
    $
            [(PatVarName, Dom Type)]
    flattenedOldTel

          -- Permutation taking the new variable and dot patterns to the
          -- new telescope.
          newPerm :: Permutation
    newPerm = Permutation -> Permutation
    adjustForDotPatterns (Permutation -> Permutation) -> Permutation -> Permutation
    forall a b. (a -> b) -> a -> b
    $
                      [Dom Type] -> Permutation
    reorderTel_ ([Dom Type] -> Permutation) -> [Dom Type] -> Permutation
    forall a b. (a -> b) -> a -> b
    $ (Maybe (PatVarName, Dom Type) -> Dom Type)
    -> [Maybe (PatVarName, Dom Type)] -> [Dom Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (Dom Type
    -> ((PatVarName, Dom Type) -> Dom Type)
    -> Maybe (PatVarName, Dom Type)
    -> Dom Type
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Dom Type
    HasCallStack => Dom Type
    __DUMMY_DOM__ (PatVarName, Dom Type) -> Dom Type
    forall a b. (a, b) -> b
    snd) [Maybe (PatVarName, Dom Type)]
    newTel'
            -- It is important that __DUMMY_DOM__ does not mention any variable
            -- (see the definition of reorderTel).
            where
            isDotP :: Nat -> Bool
    isDotP Nat
    n = case Changes
    -> Nat -> Either Pattern (Kind -> Nat, PatVarName, Dom Type)
    forall i a. Integral i => [a] -> i -> a
    List.genericIndex Changes
    cs Nat
    n of
                         Left DotP{} -> Bool
    True
                         Either Pattern (Kind -> Nat, PatVarName, Dom Type)
    _           -> Bool
    False

            adjustForDotPatterns :: Permutation -> Permutation
    adjustForDotPatterns (Perm Nat
    n [Nat]
    is) =
              Nat -> [Nat] -> Permutation
    Perm Nat
    n ((Nat -> Bool) -> [Nat] -> [Nat]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Nat -> Bool) -> Nat -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> Bool
    isDotP) [Nat]
    is)

          -- Substitution used to convert terms in the new RHS's context
          -- to terms in the new telescope's context.
          lhsSubst' :: Substitution' Term
    lhsSubst' = Impossible -> Permutation -> Substitution' Term
    forall a.
    DeBruijn a =>
    Impossible -> Permutation -> Substitution' a
    renaming Impossible
    HasCallStack => Impossible
    impossible (Permutation -> Permutation
    reverseP Permutation
    newPerm)

          -- Substitution used to convert terms in the old telescope's
          -- context to terms in the new telescope's context.
          lhsSubst :: Substitution' Term
    lhsSubst = Substitution' (SubstArg (Substitution' Term))
    -> Substitution' Term -> Substitution' Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (Substitution' Term))
    lhsSubst' Substitution' Term
    rhsSubst'

          -- The new telescope.
          newTel :: Telescope
    newTel =
            ([PatVarName] -> [Dom Type] -> Telescope)
    -> ([PatVarName], [Dom Type]) -> Telescope
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry [PatVarName] -> [Dom Type] -> Telescope
    unflattenTel (([PatVarName], [Dom Type]) -> Telescope)
    -> ([(PatVarName, Dom Type)] -> ([PatVarName], [Dom Type]))
    -> [(PatVarName, Dom Type)]
    -> Telescope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(PatVarName, Dom Type)] -> ([PatVarName], [Dom Type])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(PatVarName, Dom Type)] -> Telescope)
    -> [(PatVarName, Dom Type)] -> Telescope
    forall a b. (a -> b) -> a -> b
    $
            (Maybe (PatVarName, Dom Type) -> (PatVarName, Dom Type))
    -> [Maybe (PatVarName, Dom Type)] -> [(PatVarName, Dom Type)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((PatVarName, Dom Type)
    -> Maybe (PatVarName, Dom Type) -> (PatVarName, Dom Type)
    forall a. a -> Maybe a -> a
    fromMaybe (PatVarName, Dom Type)
    forall a. HasCallStack => a
    __IMPOSSIBLE__) ([Maybe (PatVarName, Dom Type)] -> [(PatVarName, Dom Type)])
    -> [Maybe (PatVarName, Dom Type)] -> [(PatVarName, Dom Type)]
    forall a b. (a -> b) -> a -> b
    $
            Permutation
    -> [Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall a. Permutation -> [a] -> [a]
    permute Permutation
    newPerm ([Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)])
    -> [Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall a b. (a -> b) -> a -> b
    $
            Substitution' (SubstArg (Dom Type))
    -> [Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall {d}.
    Substitution' (SubstArg (Dom Type))
    -> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
    substTel Substitution' Term
    Substitution' (SubstArg (Dom Type))
    lhsSubst' ([Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)])
    -> [Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall a b. (a -> b) -> a -> b
    $
            [Maybe (PatVarName, Dom Type)]
    newTel'

          -- New clause.
          c :: Clause
    c = Clause
    clause
                { clauseTel :: Telescope
    clauseTel       = Telescope
    newTel
                , namedClausePats :: NAPs
    namedClausePats = Nat -> Permutation -> [NamedArg Pattern] -> NAPs
    forall a b.
    (LabelPatVars a b, PatVarLabel b ~ Nat) =>
    Nat -> Permutation -> a -> b
    numberPatVars Nat
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Permutation
    newPerm ([NamedArg Pattern] -> NAPs) -> [NamedArg Pattern] -> NAPs
    forall a b. (a -> b) -> a -> b
    $ Substitution' (SubstArg [NamedArg Pattern])
    -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg [NamedArg Pattern])
    lhsSubst [NamedArg Pattern]
    ps
                , clauseBody :: Maybe Term
    clauseBody      = Substitution' (SubstArg (Maybe Term)) -> Maybe Term -> Maybe Term
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (Maybe Term))
    lhsSubst (Maybe Term -> Maybe Term) -> Maybe Term -> Maybe Term
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Term
    clauseBody Clause
    clause
                }

      PatVarName -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.lhs.recpat" Nat
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
          [ TCMT IO Doc
    "Original clause:"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> TCMT IO Doc
    forall (tcm :: * -> *) a.
    (MonadTCEnv tcm, ReadTCState tcm) =>
    tcm a -> tcm a
    inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    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
    "delta =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Clause -> Telescope
    clauseTel Clause
    clause)
            , TCMT IO Doc
    "pats  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> PatVarName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => PatVarName -> m Doc
    text ([Arg DeBruijnPattern] -> PatVarName
    forall a. Show a => a -> PatVarName
    show ([Arg DeBruijnPattern] -> PatVarName)
    -> [Arg DeBruijnPattern] -> PatVarName
    forall a b. (a -> b) -> a -> b
    $ Clause -> [Arg DeBruijnPattern]
    clausePats Clause
    clause)
            ]
          , TCMT IO Doc
    "Intermediate results:"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    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
    "ps        =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> PatVarName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => PatVarName -> m Doc
    text ([NamedArg Pattern] -> PatVarName
    forall a. Show a => a -> PatVarName
    show [NamedArg Pattern]
    ps)
            , TCMT IO Doc
    "s         =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> [Term] -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM [Term]
    s
            , TCMT IO Doc
    "cs        =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Changes -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Changes
    cs
            , TCMT IO Doc
    "flattenedOldTel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (PatVarName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => PatVarName -> m Doc
    text (PatVarName -> TCMT IO Doc)
    -> ([(PatVarName, Dom Type)] -> PatVarName)
    -> [(PatVarName, Dom Type)]
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(PatVarName, Dom Type)] -> PatVarName
    forall a. Show a => a -> PatVarName
    show) [(PatVarName, Dom Type)]
    flattenedOldTel
            , TCMT IO Doc
    "newTel'   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (PatVarName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => PatVarName -> m Doc
    text (PatVarName -> TCMT IO Doc)
    -> ([Maybe (PatVarName, Dom Type)] -> PatVarName)
    -> [Maybe (PatVarName, Dom Type)]
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Maybe (PatVarName, Dom Type)] -> PatVarName
    forall a. Show a => a -> PatVarName
    show) [Maybe (PatVarName, Dom Type)]
    newTel'
            , TCMT IO Doc
    "newPerm   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Permutation -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Permutation
    newPerm
            ]
          ]

      PatVarName -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.lhs.recpat" Nat
    20 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
            [ TCMT IO Doc
    "lhsSubst' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (PatVarName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => PatVarName -> m Doc
    text (PatVarName -> TCMT IO Doc)
    -> (Substitution' Term -> PatVarName)
    -> Substitution' Term
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Substitution' Term -> PatVarName
    forall a. Show a => a -> PatVarName
    show) Substitution' Term
    lhsSubst'
            , TCMT IO Doc
    "lhsSubst  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (PatVarName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => PatVarName -> m Doc
    text (PatVarName -> TCMT IO Doc)
    -> (Substitution' Term -> PatVarName)
    -> Substitution' Term
    -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Substitution' Term -> PatVarName
    forall a. Show a => a -> PatVarName
    show) Substitution' Term
    lhsSubst
            , TCMT IO Doc
    "newTel  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Telescope
    newTel
            ]

      PatVarName -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.lhs.recpat" Nat
    10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
        Impossible -> Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *) a.
    MonadAddContext m =>
    Impossible -> Nat -> m a -> m a
    escapeContext Impossible
    HasCallStack => Impossible
    impossible (Telescope -> Nat
    forall a. Sized a => a -> Nat
    size (Telescope -> Nat) -> Telescope -> Nat
    forall a b. (a -> b) -> a -> b
    $ Clause -> Telescope
    clauseTel Clause
    clause) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    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
    "Translated clause:"
          , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    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
    "delta =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Clause -> Telescope
    clauseTel Clause
    c)
            , TCMT IO Doc
    "ps    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> PatVarName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => PatVarName -> m Doc
    text ([Arg DeBruijnPattern] -> PatVarName
    forall a. Show a => a -> PatVarName
    show ([Arg DeBruijnPattern] -> PatVarName)
    -> [Arg DeBruijnPattern] -> PatVarName
    forall a b. (a -> b) -> a -> b
    $ Clause -> [Arg DeBruijnPattern]
    clausePats Clause
    c)
            , TCMT IO Doc
    "body  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> PatVarName -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => PatVarName -> m Doc
    text (Maybe Term -> PatVarName
    forall a. Show a => a -> PatVarName
    show (Maybe Term -> PatVarName) -> Maybe Term -> PatVarName
    forall a b. (a -> b) -> a -> b
    $ Clause -> Maybe Term
    clauseBody Clause
    c)
            , TCMT IO Doc
    "body  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Telescope -> TCMT IO Doc -> TCMT IO Doc
    forall b (m :: * -> *) a.
    (AddContext b, MonadAddContext m) =>
    b -> m a -> m a
    addContext (Clause -> Telescope
    clauseTel Clause
    c) (TCMT IO Doc -> (Term -> TCMT IO Doc) -> Maybe Term -> TCMT IO Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe TCMT IO Doc
    "_|_" Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM (Clause -> Maybe Term
    clauseBody Clause
    c))
            ]
          ]

      Clause -> TCM Clause
    forall (m :: * -> *) a. Monad m => a -> m a
    return Clause
    c

    ------------------------------------------------------------------------
    -- Record pattern monad

    -- | A monad used to translate record patterns.
    --
    -- The state records the number of variables produced so far, the
    -- reader records the total number of variables produced by the entire
    -- computation. Functions using this monad need to be sufficiently
    -- lazy in the reader component.

    newtype RecPatM a = RecPatM (TCMT (ReaderT Nat (StateT Nat IO)) a)
      deriving ((forall a b. (a -> b) -> RecPatM a -> RecPatM b)
    -> (forall a b. a -> RecPatM b -> RecPatM a) -> Functor RecPatM
    forall a b. a -> RecPatM b -> RecPatM a
    forall a b. (a -> b) -> RecPatM a -> RecPatM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> RecPatM b -> RecPatM a
    $c<$ :: forall a b. a -> RecPatM b -> RecPatM a
    fmap :: forall a b. (a -> b) -> RecPatM a -> RecPatM b
    $cfmap :: forall a b. (a -> b) -> RecPatM a -> RecPatM b
    Functor, Functor RecPatM
    Functor RecPatM
    -> (forall a. a -> RecPatM a)
    -> (forall a b. RecPatM (a -> b) -> RecPatM a -> RecPatM b)
    -> (forall a b c.
        (a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c)
    -> (forall a b. RecPatM a -> RecPatM b -> RecPatM b)
    -> (forall a b. RecPatM a -> RecPatM b -> RecPatM a)
    -> Applicative RecPatM
    forall a. a -> RecPatM a
    forall a b. RecPatM a -> RecPatM b -> RecPatM a
    forall a b. RecPatM a -> RecPatM b -> RecPatM b
    forall a b. RecPatM (a -> b) -> RecPatM a -> RecPatM b
    forall a b c. (a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c
    forall (f :: * -> *).
    Functor f
    -> (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    <* :: forall a b. RecPatM a -> RecPatM b -> RecPatM a
    $c<* :: forall a b. RecPatM a -> RecPatM b -> RecPatM a
    *> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
    $c*> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
    liftA2 :: forall a b c. (a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c
    $cliftA2 :: forall a b c. (a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c
    <*> :: forall a b. RecPatM (a -> b) -> RecPatM a -> RecPatM b
    $c<*> :: forall a b. RecPatM (a -> b) -> RecPatM a -> RecPatM b
    pure :: forall a. a -> RecPatM a
    $cpure :: forall a. a -> RecPatM a
    Applicative, Applicative RecPatM
    Applicative RecPatM
    -> (forall a b. RecPatM a -> (a -> RecPatM b) -> RecPatM b)
    -> (forall a b. RecPatM a -> RecPatM b -> RecPatM b)
    -> (forall a. a -> RecPatM a)
    -> Monad RecPatM
    forall a. a -> RecPatM a
    forall a b. RecPatM a -> RecPatM b -> RecPatM b
    forall a b. RecPatM a -> (a -> RecPatM b) -> RecPatM b
    forall (m :: * -> *).
    Applicative m
    -> (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    return :: forall a. a -> RecPatM a
    $creturn :: forall a. a -> RecPatM a
    >> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
    $c>> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
    >>= :: forall a b. RecPatM a -> (a -> RecPatM b) -> RecPatM b
    $c>>= :: forall a b. RecPatM a -> (a -> RecPatM b) -> RecPatM b
    Monad,
                Monad RecPatM
    Monad RecPatM -> (forall a. IO a -> RecPatM a) -> MonadIO RecPatM
    forall a. IO a -> RecPatM a
    forall (m :: * -> *).
    Monad m -> (forall a. IO a -> m a) -> MonadIO m
    liftIO :: forall a. IO a -> RecPatM a
    $cliftIO :: forall a. IO a -> RecPatM a
    MonadIO, Applicative RecPatM
    MonadIO RecPatM
    HasOptions RecPatM
    MonadTCState RecPatM
    MonadTCEnv RecPatM
    Applicative RecPatM
    -> MonadIO RecPatM
    -> MonadTCEnv RecPatM
    -> MonadTCState RecPatM
    -> HasOptions RecPatM
    -> (forall a. TCM a -> RecPatM a)
    -> MonadTCM RecPatM
    forall a. TCM a -> RecPatM a
    forall (tcm :: * -> *).
    Applicative tcm
    -> MonadIO tcm
    -> MonadTCEnv tcm
    -> MonadTCState tcm
    -> HasOptions tcm
    -> (forall a. TCM a -> tcm a)
    -> MonadTCM tcm
    liftTCM :: forall a. TCM a -> RecPatM a
    $cliftTCM :: forall a. TCM a -> RecPatM a
    MonadTCM, Monad RecPatM
    Functor RecPatM
    Applicative RecPatM
    RecPatM PragmaOptions
    RecPatM CommandLineOptions
    Functor RecPatM
    -> Applicative RecPatM
    -> Monad RecPatM
    -> RecPatM PragmaOptions
    -> RecPatM CommandLineOptions
    -> HasOptions RecPatM
    forall (m :: * -> *).
    Functor m
    -> Applicative m
    -> Monad m
    -> m PragmaOptions
    -> m CommandLineOptions
    -> HasOptions m
    commandLineOptions :: RecPatM CommandLineOptions
    $ccommandLineOptions :: RecPatM CommandLineOptions
    pragmaOptions :: RecPatM PragmaOptions
    $cpragmaOptions :: RecPatM PragmaOptions
    HasOptions,
                Monad RecPatM
    RecPatM TCEnv
    Monad RecPatM
    -> RecPatM TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a)
    -> MonadTCEnv RecPatM
    forall a. (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a
    forall (m :: * -> *).
    Monad m
    -> m TCEnv
    -> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
    -> MonadTCEnv m
    localTC :: forall a. (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a
    $clocalTC :: forall a. (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a
    askTC :: RecPatM TCEnv
    $caskTC :: RecPatM TCEnv
    MonadTCEnv, Monad RecPatM
    RecPatM TCState
    Monad RecPatM
    -> RecPatM TCState
    -> (TCState -> RecPatM ())
    -> ((TCState -> TCState) -> RecPatM ())
    -> MonadTCState RecPatM
    TCState -> RecPatM ()
    (TCState -> TCState) -> RecPatM ()
    forall (m :: * -> *).
    Monad m
    -> m TCState
    -> (TCState -> m ())
    -> ((TCState -> TCState) -> m ())
    -> MonadTCState m
    modifyTC :: (TCState -> TCState) -> RecPatM ()
    $cmodifyTC :: (TCState -> TCState) -> RecPatM ()
    putTC :: TCState -> RecPatM ()
    $cputTC :: TCState -> RecPatM ()
    getTC :: RecPatM TCState
    $cgetTC :: RecPatM TCState
    MonadTCState)

    -- | Runs a computation in the 'RecPatM' monad.

    runRecPatM :: RecPatM a -> TCM a
    runRecPatM :: forall a. RecPatM a -> TCM a
    runRecPatM (RecPatM TCMT (ReaderT Nat (StateT Nat IO)) a
    m) =
      (forall a1. ReaderT Nat (StateT Nat IO) a1 -> IO a1)
    -> TCMT (ReaderT Nat (StateT Nat IO)) a -> TCMT IO a
    forall (m :: * -> *) (n :: * -> *) a.
    (forall a1. m a1 -> n a1) -> TCMT m a -> TCMT n a
    mapTCMT (\ReaderT Nat (StateT Nat IO) a1
    m -> do
                 (a1
    x, Nat
    noVars) <- ((a1, Nat) -> IO (a1, Nat)) -> IO (a1, Nat)
    forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
    mfix (((a1, Nat) -> IO (a1, Nat)) -> IO (a1, Nat))
    -> ((a1, Nat) -> IO (a1, Nat)) -> IO (a1, Nat)
    forall a b. (a -> b) -> a -> b
    $ \ ~(a1
    _, Nat
    noVars) ->
                                  StateT Nat IO a1 -> Nat -> IO (a1, Nat)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (ReaderT Nat (StateT Nat IO) a1 -> Nat -> StateT Nat IO a1
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT ReaderT Nat (StateT Nat IO) a1
    m Nat
    noVars) Nat
    0
                 a1 -> IO a1
    forall (m :: * -> *) a. Monad m => a -> m a
    return a1
    x)
              TCMT (ReaderT Nat (StateT Nat IO)) a
    m

    -- | Returns the next pattern variable, and the corresponding term.

    nextVar :: RecPatM (Pattern, Term)
    nextVar :: RecPatM (Pattern, Term)
    nextVar = TCMT (ReaderT Nat (StateT Nat IO)) (Pattern, Term)
    -> RecPatM (Pattern, Term)
    forall a. TCMT (ReaderT Nat (StateT Nat IO)) a -> RecPatM a
    RecPatM (TCMT (ReaderT Nat (StateT Nat IO)) (Pattern, Term)
     -> RecPatM (Pattern, Term))
    -> TCMT (ReaderT Nat (StateT Nat IO)) (Pattern, Term)
    -> RecPatM (Pattern, Term)
    forall a b. (a -> b) -> a -> b
    $ do
      Nat
    n <- ReaderT Nat (StateT Nat IO) Nat
    -> TCMT (ReaderT Nat (StateT Nat IO)) Nat
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ReaderT Nat (StateT Nat IO) Nat
    forall s (m :: * -> *). MonadState s m => m s
    get
      ReaderT Nat (StateT Nat IO) ()
    -> TCMT (ReaderT Nat (StateT Nat IO)) ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (ReaderT Nat (StateT Nat IO) ()
     -> TCMT (ReaderT Nat (StateT Nat IO)) ())
    -> ReaderT Nat (StateT Nat IO) ()
    -> TCMT (ReaderT Nat (StateT Nat IO)) ()
    forall a b. (a -> b) -> a -> b
    $ Nat -> ReaderT Nat (StateT Nat IO) ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Nat -> ReaderT Nat (StateT Nat IO) ())
    -> Nat -> ReaderT Nat (StateT Nat IO) ()
    forall a b. (a -> b) -> a -> b
    $ Nat -> Nat
    forall a. Enum a => a -> a
    succ Nat
    n
      Nat
    noVars <- ReaderT Nat (StateT Nat IO) Nat
    -> TCMT (ReaderT Nat (StateT Nat IO)) Nat
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift ReaderT Nat (StateT Nat IO) Nat
    forall r (m :: * -> *). MonadReader r m => m r
    ask
      (Pattern, Term)
    -> TCMT (ReaderT Nat (StateT Nat IO)) (Pattern, Term)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PatVarName -> Pattern
    forall a. a -> Pattern' a
    varP PatVarName
    "r", Nat -> Term
    var (Nat -> Term) -> Nat -> Term
    forall a b. (a -> b) -> a -> b
    $ Nat
    noVars Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1)

    ------------------------------------------------------------------------
    -- Types used to record changes to a clause

    -- | @VarPat@ stands for variable patterns, and @DotPat@ for dot
    -- patterns.

    data Kind = VarPat | DotPat
      deriving Kind -> Kind -> Bool
    (Kind -> Kind -> Bool) -> (Kind -> Kind -> Bool) -> Eq Kind
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Kind -> Kind -> Bool
    $c/= :: Kind -> Kind -> Bool
    == :: Kind -> Kind -> Bool
    $c== :: Kind -> Kind -> Bool
    Eq

    -- | @'Left' p@ means that a variable (corresponding to the pattern
    -- @p@, a variable or dot pattern) should be kept unchanged. @'Right'
    -- (n, x, t)@ means that @n 'VarPat'@ variables, and @n 'DotPat'@ dot
    -- patterns, should be removed, and a new variable, with the name @x@,
    -- inserted instead. The type of the new variable is @t@.

    type Change  = Either Pattern (Kind -> Nat, ArgName, Dom Type)
    type Changes = [Change]

    instance Pretty (Kind -> Nat) where
      pretty :: (Kind -> Nat) -> Doc
    pretty Kind -> Nat
    f =
        (Doc
    "(VarPat:" Doc -> Doc -> Doc
    P.<+> PatVarName -> Doc
    P.text (Nat -> PatVarName
    forall a. Show a => a -> PatVarName
    show (Nat -> PatVarName) -> Nat -> PatVarName
    forall a b. (a -> b) -> a -> b
    $ Kind -> Nat
    f Kind
    VarPat) Doc -> Doc -> Doc
    P.<+>
        Doc
    "DotPat:"  Doc -> Doc -> Doc
    P.<+> PatVarName -> Doc
    P.text (Nat -> PatVarName
    forall a. Show a => a -> PatVarName
    show (Nat -> PatVarName) -> Nat -> PatVarName
    forall a b. (a -> b) -> a -> b
    $ Kind -> Nat
    f Kind
    DotPat)) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ")"

    instance PrettyTCM (Kind -> Nat) where
      prettyTCM :: forall (m :: * -> *). MonadPretty m => (Kind -> Nat) -> m Doc
    prettyTCM = Doc -> m Doc
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Doc -> m Doc) -> ((Kind -> Nat) -> Doc) -> (Kind -> Nat) -> m Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Kind -> Nat) -> Doc
    forall a. Pretty a => a -> Doc
    pretty

    instance PrettyTCM Change where
      prettyTCM :: forall (m :: * -> *).
    MonadPretty m =>
    Either Pattern (Kind -> Nat, PatVarName, Dom Type) -> m Doc
    prettyTCM (Left  Pattern
    p) = Pattern -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Pattern
    p
      prettyTCM (Right (Kind -> Nat
    f, PatVarName
    x, Dom Type
    t)) = m Doc
    "Change" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (Kind -> Nat) -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Kind -> Nat
    f m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> PatVarName -> m Doc
    forall (m :: * -> *). Applicative m => PatVarName -> m Doc
    text PatVarName
    x m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Dom Type -> m Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Dom Type
    t

    -- | Record pattern trees.

    data RecordTree
      = Leaf Pattern
        -- ^ Corresponds to variable and dot patterns; contains the
        -- original pattern.
      | RecCon (Arg Type) [(Term -> Term, RecordTree)]
        -- ^ @RecCon t args@ stands for a record constructor application:
        -- @t@ is the type of the application, and the list contains a
        -- projection function and a tree for every argument.

    ------------------------------------------------------------------------
    -- Record pattern trees

    -- | @projections t@ returns a projection for every non-dot leaf
    -- pattern in @t@. The term is the composition of the projection
    -- functions from the leaf to the root.
    --
    -- Every term is tagged with its origin: a variable pattern or a dot
    -- pattern.

    projections :: RecordTree -> [(Term -> Term, Kind)]
    projections :: RecordTree -> [(Term -> Term, Kind)]
    projections (Leaf (DotP{})) = [(Term -> Term
    forall a. a -> a
    id, Kind
    DotPat)]
    projections (Leaf (VarP{})) = [(Term -> Term
    forall a. a -> a
    id, Kind
    VarPat)]
    projections (Leaf Pattern
    _)        = [(Term -> Term, Kind)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    projections (RecCon Arg Type
    _ [(Term -> Term, RecordTree)]
    args) =
      ((Term -> Term, RecordTree) -> [(Term -> Term, Kind)])
    -> [(Term -> Term, RecordTree)] -> [(Term -> Term, Kind)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (\ (Term -> Term
    p, RecordTree
    t) -> ((Term -> Term, Kind) -> (Term -> Term, Kind))
    -> [(Term -> Term, Kind)] -> [(Term -> Term, Kind)]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Term -> Term) -> Term -> Term)
    -> (Term -> Term, Kind) -> (Term -> Term, Kind)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (b, d) (c, d)
    first ((Term -> Term) -> (Term -> Term) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Term
    p)) ([(Term -> Term, Kind)] -> [(Term -> Term, Kind)])
    -> [(Term -> Term, Kind)] -> [(Term -> Term, Kind)]
    forall a b. (a -> b) -> a -> b
    $ RecordTree -> [(Term -> Term, Kind)]
    projections RecordTree
    t)
                [(Term -> Term, RecordTree)]
    args

    -- | Converts a record tree to a single pattern along with information
    -- about the deleted pattern variables.

    removeTree :: RecordTree -> RecPatM (Pattern, [Term], Changes)
    removeTree :: RecordTree -> RecPatM (Pattern, [Term], Changes)
    removeTree RecordTree
    tree = do
      (Pattern
    pat, Term
    x) <- RecPatM (Pattern, Term)
    nextVar
      let ps :: [(Term -> Term, Kind)]
    ps = RecordTree -> [(Term -> Term, Kind)]
    projections RecordTree
    tree
          s :: [Term]
    s  = ((Term -> Term, Kind) -> Term) -> [(Term -> Term, Kind)] -> [Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Term -> Term
    p, Kind
    _) -> Term -> Term
    p Term
    x) [(Term -> Term, Kind)]
    ps

          count :: Kind -> Nat
    count Kind
    k = [(Term -> Term, Kind)] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length ([(Term -> Term, Kind)] -> Nat) -> [(Term -> Term, Kind)] -> Nat
    forall a b. (a -> b) -> a -> b
    $ ((Term -> Term, Kind) -> Bool)
    -> [(Term -> Term, Kind)] -> [(Term -> Term, Kind)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    == Kind
    k) (Kind -> Bool)
    -> ((Term -> Term, Kind) -> Kind) -> (Term -> Term, Kind) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> Term, Kind) -> Kind
    forall a b. (a, b) -> b
    snd) [(Term -> Term, Kind)]
    ps

      (Pattern, [Term], Changes) -> RecPatM (Pattern, [Term], Changes)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Pattern, [Term], Changes) -> RecPatM (Pattern, [Term], Changes))
    -> (Pattern, [Term], Changes) -> RecPatM (Pattern, [Term], Changes)
    forall a b. (a -> b) -> a -> b
    $ case RecordTree
    tree of
        Leaf Pattern
    p     -> (Pattern
    p,   [Term]
    s, [Pattern -> Either Pattern (Kind -> Nat, PatVarName, Dom Type)
    forall a b. a -> Either a b
    Left Pattern
    p])
        RecCon Arg Type
    t [(Term -> Term, RecordTree)]
    _ -> (Pattern
    pat, [Term]
    s, [(Kind -> Nat, PatVarName, Dom Type)
    -> Either Pattern (Kind -> Nat, PatVarName, Dom Type)
    forall a b. b -> Either a b
    Right (Kind -> Nat
    count, PatVarName
    "r", Arg Type -> Dom Type
    forall a. Arg a -> Dom a
    domFromArg Arg Type
    t)])

    ------------------------------------------------------------------------
    -- Translation of patterns

    -- | Removes record constructors from patterns.
    --
    -- Returns the following things:
    --
    -- * The new pattern.
    --
    -- * A substitution which maps the /old/ pattern variables (in the
    --   order they occurred in the pattern; not including dot patterns)
    --   to terms (either the new name of the variable, or a projection
    --   applied to a new pattern variable).
    --
    -- * A list explaining the changes to the variables bound in the
    --   pattern.
    --
    -- Record patterns containing non-record constructor patterns are not
    -- translated (though their sub-patterns may be).
    --
    -- Example: The pattern @rec1 (con1 a) (rec2 b c) (rec3 d)@ should
    -- yield the pattern @rec1 (con1 x) y z@, along with a substitution
    -- similar to @[x, proj2-1 y, proj2-2 y, proj3-1 z]@.
    --
    -- This function assumes that literals are never of record type.

    translatePattern :: Pattern -> RecPatM (Pattern, [Term], Changes)
    translatePattern :: Pattern -> RecPatM (Pattern, [Term], Changes)
    translatePattern p :: Pattern
    p@(ConP ConHead
    c ConPatternInfo
    ci [NamedArg Pattern]
    ps)
      -- Andreas, 2015-05-28 only translate implicit record patterns
      | ConPatternInfo -> Bool
    conPRecord ConPatternInfo
    ci , PatOrigin
    PatOSystem <- PatternInfo -> PatOrigin
    patOrigin (ConPatternInfo -> PatternInfo
    conPInfo ConPatternInfo
    ci) = do
          Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    r <- Pattern
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    recordTree Pattern
    p
          case Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    r of
            Left  RecPatM (Pattern, [Term], Changes)
    r -> RecPatM (Pattern, [Term], Changes)
    r
            Right RecordTree
    t -> RecordTree -> RecPatM (Pattern, [Term], Changes)
    removeTree RecordTree
    t
      | Bool
    otherwise = do
          ([NamedArg Pattern]
    ps, [Term]
    s, Changes
    cs) <- [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
    translatePatterns [NamedArg Pattern]
    ps
          (Pattern, [Term], Changes) -> RecPatM (Pattern, [Term], Changes)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConHead -> ConPatternInfo -> [NamedArg Pattern] -> Pattern
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    ci [NamedArg Pattern]
    ps, [Term]
    s, Changes
    cs)
    translatePattern p :: Pattern
    p@(DefP PatternInfo
    o QName
    q [NamedArg Pattern]
    ps) = do
          ([NamedArg Pattern]
    ps, [Term]
    s, Changes
    cs) <- [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
    translatePatterns [NamedArg Pattern]
    ps
          (Pattern, [Term], Changes) -> RecPatM (Pattern, [Term], Changes)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PatternInfo -> QName -> [NamedArg Pattern] -> Pattern
    forall x.
    PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
    DefP PatternInfo
    o QName
    q [NamedArg Pattern]
    ps, [Term]
    s, Changes
    cs)
    translatePattern p :: Pattern
    p@VarP{} = RecordTree -> RecPatM (Pattern, [Term], Changes)
    removeTree (Pattern -> RecordTree
    Leaf Pattern
    p)
    translatePattern p :: Pattern
    p@DotP{} = RecordTree -> RecPatM (Pattern, [Term], Changes)
    removeTree (Pattern -> RecordTree
    Leaf Pattern
    p)
    translatePattern p :: Pattern
    p@LitP{} = (Pattern, [Term], Changes) -> RecPatM (Pattern, [Term], Changes)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern
    p, [], [])
    translatePattern p :: Pattern
    p@ProjP{}= (Pattern, [Term], Changes) -> RecPatM (Pattern, [Term], Changes)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern
    p, [], [])
    translatePattern p :: Pattern
    p@IApplyP{}= (Pattern, [Term], Changes) -> RecPatM (Pattern, [Term], Changes)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Pattern
    p, [], [])

    translatePatterns :: [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
    translatePatterns :: [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
    translatePatterns [NamedArg Pattern]
    ps = do
      ([Pattern]
    ps', [[Term]]
    ss, [Changes]
    cs) <- [(Pattern, [Term], Changes)] -> ([Pattern], [[Term]], [Changes])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 ([(Pattern, [Term], Changes)] -> ([Pattern], [[Term]], [Changes]))
    -> RecPatM [(Pattern, [Term], Changes)]
    -> RecPatM ([Pattern], [[Term]], [Changes])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NamedArg Pattern -> RecPatM (Pattern, [Term], Changes))
    -> [NamedArg Pattern] -> RecPatM [(Pattern, [Term], Changes)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Pattern -> RecPatM (Pattern, [Term], Changes)
    translatePattern (Pattern -> RecPatM (Pattern, [Term], Changes))
    -> (NamedArg Pattern -> Pattern)
    -> NamedArg Pattern
    -> RecPatM (Pattern, [Term], Changes)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg) [NamedArg Pattern]
    ps
      ([NamedArg Pattern], [Term], Changes)
    -> RecPatM ([NamedArg Pattern], [Term], Changes)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Pattern -> NamedArg Pattern -> NamedArg Pattern)
    -> [Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\Pattern
    p -> (Named NamedName Pattern -> Named NamedName Pattern)
    -> NamedArg Pattern -> NamedArg Pattern
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Pattern
    p Pattern -> Named NamedName Pattern -> Named NamedName Pattern
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$)) [Pattern]
    ps' [NamedArg Pattern]
    ps, [[Term]] -> [Term]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Term]]
    ss, [Changes] -> Changes
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [Changes]
    cs)

    -- | Traverses a pattern and returns one of two things:
    --
    -- * If there is no non-record constructor in the pattern, then
    --   @'Right' ps@ is returned, where @ps@ contains one projection for
    --   every variable in the input pattern (in the order they are
    --   encountered).
    --
    -- * Otherwise the output is a computation returning the same kind of
    --   result as that coming from 'translatePattern'. (Computations are
    --   returned rather than values to ensure that variable numbers are
    --   allocated in the right order.)
    --
    -- Assumes that literals are never of record type.

    recordTree ::
      Pattern ->
      RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -- Andreas, 2015-05-28 only translate implicit record patterns
    recordTree :: Pattern
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    recordTree p :: Pattern
    p@(ConP ConHead
    c ConPatternInfo
    ci [NamedArg Pattern]
    ps) | ConPatternInfo -> Bool
    conPRecord ConPatternInfo
    ci , PatOrigin
    PatOSystem <- PatternInfo -> PatOrigin
    patOrigin (ConPatternInfo -> PatternInfo
    conPInfo ConPatternInfo
    ci) = do
      let t :: Arg Type
    t = 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
      [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
    rs <- (NamedArg Pattern
     -> RecPatM
          (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> [NamedArg Pattern]
    -> RecPatM [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Pattern
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    recordTree (Pattern
     -> RecPatM
          (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> (NamedArg Pattern -> Pattern)
    -> NamedArg Pattern
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedArg Pattern -> Pattern
    forall a. NamedArg a -> a
    namedArg) [NamedArg Pattern]
    ps
      case [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
    -> Maybe [RecordTree]
    forall a b. [Either a b] -> Maybe [b]
    allRight [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
    rs of
        Maybe [RecordTree]
    Nothing ->
          Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (RecPatM (Pattern, [Term], Changes)) RecordTree
     -> RecPatM
          (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall a b. (a -> b) -> a -> b
    $ RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. a -> Either a b
    Left (RecPatM (Pattern, [Term], Changes)
     -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -> RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. (a -> b) -> a -> b
    $ do
            ([Pattern]
    ps', [[Term]]
    ss, [Changes]
    cs) <- [(Pattern, [Term], Changes)] -> ([Pattern], [[Term]], [Changes])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 ([(Pattern, [Term], Changes)] -> ([Pattern], [[Term]], [Changes]))
    -> RecPatM [(Pattern, [Term], Changes)]
    -> RecPatM ([Pattern], [[Term]], [Changes])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Either (RecPatM (Pattern, [Term], Changes)) RecordTree
     -> RecPatM (Pattern, [Term], Changes))
    -> [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
    -> RecPatM [(Pattern, [Term], Changes)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((RecPatM (Pattern, [Term], Changes)
     -> RecPatM (Pattern, [Term], Changes))
    -> (RecordTree -> RecPatM (Pattern, [Term], Changes))
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Pattern, [Term], Changes)
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either RecPatM (Pattern, [Term], Changes)
    -> RecPatM (Pattern, [Term], Changes)
    forall a. a -> a
    id RecordTree -> RecPatM (Pattern, [Term], Changes)
    removeTree) [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
    rs
            (Pattern, [Term], Changes) -> RecPatM (Pattern, [Term], Changes)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConHead -> ConPatternInfo -> [NamedArg Pattern] -> Pattern
    forall x.
    ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
    ConP ConHead
    c ConPatternInfo
    ci ([Pattern]
    ps' [Pattern] -> [NamedArg Pattern] -> [NamedArg Pattern]
    forall a b. [a] -> [NamedArg b] -> [NamedArg a]
    `withNamedArgsFrom` [NamedArg Pattern]
    ps),
                    [[Term]] -> [Term]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Term]]
    ss, [Changes] -> Changes
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [Changes]
    cs)
        Just [RecordTree]
    ts -> TCM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
     -> RecPatM
          (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> TCM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall a b. (a -> b) -> a -> b
    $ do
          Arg Type
    t <- Arg Type -> TCMT IO (Arg Type)
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Arg Type
    t
          PatVarName -> Nat -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    PatVarName -> Nat -> TCMT IO Doc -> m ()
    reportSDoc PatVarName
    "tc.rec" Nat
    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
    "recordTree: "
            , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    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
    <+> Pattern -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Pattern
    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
    <+> Arg Type -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM Arg Type
    t
            ]
          -- Andreas, 2018-03-03, see #2989:
          -- The content of an @Arg@ might not be reduced (if @Arg@ is @Irrelevant@).
          [Dom QName]
    fields <- Type -> TCM [Dom QName]
    getRecordTypeFields (Type -> TCM [Dom QName]) -> TCMT IO Type -> TCM [Dom QName]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Type -> TCMT IO Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Arg Type -> Type
    forall e. Arg e -> e
    unArg Arg Type
    t)
    --      let proj p = \x -> Def (unArg p) [defaultArg x]
          let 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])
          Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> TCM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (RecPatM (Pattern, [Term], Changes)) RecordTree
     -> TCM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> TCM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall a b. (a -> b) -> a -> b
    $ RecordTree
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. b -> Either a b
    Right (RecordTree
     -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -> RecordTree
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. (a -> b) -> a -> b
    $ Arg Type -> [(Term -> Term, RecordTree)] -> RecordTree
    RecCon Arg Type
    t ([(Term -> Term, RecordTree)] -> RecordTree)
    -> [(Term -> Term, RecordTree)] -> RecordTree
    forall a b. (a -> b) -> a -> b
    $ [Term -> Term] -> [RecordTree] -> [(Term -> Term, RecordTree)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ((Dom QName -> Term -> Term) -> [Dom QName] -> [Term -> Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom QName -> Term -> Term
    forall {t} {t}. Apply t => Dom' t QName -> t -> t
    proj [Dom QName]
    fields) [RecordTree]
    ts
    recordTree p :: Pattern
    p@(ConP ConHead
    _ ConPatternInfo
    ci [NamedArg Pattern]
    _) = Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (RecPatM (Pattern, [Term], Changes)) RecordTree
     -> RecPatM
          (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall a b. (a -> b) -> a -> b
    $ RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. a -> Either a b
    Left (RecPatM (Pattern, [Term], Changes)
     -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -> RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. (a -> b) -> a -> b
    $ Pattern -> RecPatM (Pattern, [Term], Changes)
    translatePattern Pattern
    p
    recordTree p :: Pattern
    p@DefP{} = Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (RecPatM (Pattern, [Term], Changes)) RecordTree
     -> RecPatM
          (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall a b. (a -> b) -> a -> b
    $ RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. a -> Either a b
    Left (RecPatM (Pattern, [Term], Changes)
     -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -> RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. (a -> b) -> a -> b
    $ Pattern -> RecPatM (Pattern, [Term], Changes)
    translatePattern Pattern
    p
    recordTree p :: Pattern
    p@VarP{} = Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RecordTree
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. b -> Either a b
    Right (Pattern -> RecordTree
    Leaf Pattern
    p))
    recordTree p :: Pattern
    p@DotP{} = Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (RecordTree
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. b -> Either a b
    Right (Pattern -> RecordTree
    Leaf Pattern
    p))
    recordTree p :: Pattern
    p@LitP{} = Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (RecPatM (Pattern, [Term], Changes)) RecordTree
     -> RecPatM
          (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall a b. (a -> b) -> a -> b
    $ RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. a -> Either a b
    Left (RecPatM (Pattern, [Term], Changes)
     -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -> RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. (a -> b) -> a -> b
    $ Pattern -> RecPatM (Pattern, [Term], Changes)
    translatePattern Pattern
    p
    recordTree p :: Pattern
    p@ProjP{}= Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (RecPatM (Pattern, [Term], Changes)) RecordTree
     -> RecPatM
          (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall a b. (a -> b) -> a -> b
    $ RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. a -> Either a b
    Left (RecPatM (Pattern, [Term], Changes)
     -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -> RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. (a -> b) -> a -> b
    $ Pattern -> RecPatM (Pattern, [Term], Changes)
    translatePattern Pattern
    p
    recordTree p :: Pattern
    p@IApplyP{}= Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either (RecPatM (Pattern, [Term], Changes)) RecordTree
     -> RecPatM
          (Either (RecPatM (Pattern, [Term], Changes)) RecordTree))
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    -> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    forall a b. (a -> b) -> a -> b
    $ RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. a -> Either a b
    Left (RecPatM (Pattern, [Term], Changes)
     -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
    -> RecPatM (Pattern, [Term], Changes)
    -> Either (RecPatM (Pattern, [Term], Changes)) RecordTree
    forall a b. (a -> b) -> a -> b
    $ Pattern -> RecPatM (Pattern, [Term], Changes)
    translatePattern Pattern
    p

    ------------------------------------------------------------------------
    -- Translation of the clause telescope and body

    -- | Translates the telescope.

    translateTel
      :: Changes
         -- ^ Explanation of how the telescope should be changed. Types
         -- should be in the context of the old telescope.
      -> [(ArgName, Dom Type)]
         -- ^ Old telescope, flattened, in textual left-to-right
         -- order.
      -> [Maybe (ArgName, Dom Type)]
         -- ^ New telescope, flattened, in textual left-to-right order.
         -- 'Nothing' is used to indicate the locations of dot patterns.
    translateTel :: Changes
    -> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    translateTel (Left (DotP{}) : Changes
    rest)   [(PatVarName, Dom Type)]
    tel = Maybe (PatVarName, Dom Type)
    forall a. Maybe a
    Nothing Maybe (PatVarName, Dom Type)
    -> [Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall a. a -> [a] -> [a]
    : Changes
    -> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    translateTel Changes
    rest [(PatVarName, Dom Type)]
    tel
    translateTel (Right (Kind -> Nat
    n, PatVarName
    x, Dom Type
    t) : Changes
    rest) [(PatVarName, Dom Type)]
    tel = (PatVarName, Dom Type) -> Maybe (PatVarName, Dom Type)
    forall a. a -> Maybe a
    Just (PatVarName
    x, Dom Type
    t) Maybe (PatVarName, Dom Type)
    -> [Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall a. a -> [a] -> [a]
    :
                                                  Changes
    -> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    translateTel Changes
    rest
                                                    (Nat -> [(PatVarName, Dom Type)] -> [(PatVarName, Dom Type)]
    forall a. Nat -> [a] -> [a]
    drop (Kind -> Nat
    n Kind
    VarPat) [(PatVarName, Dom Type)]
    tel)
    translateTel (Left Pattern
    _ : Changes
    rest) ((PatVarName, Dom Type)
    t : [(PatVarName, Dom Type)]
    tel)    = (PatVarName, Dom Type) -> Maybe (PatVarName, Dom Type)
    forall a. a -> Maybe a
    Just (PatVarName, Dom Type)
    t Maybe (PatVarName, Dom Type)
    -> [Maybe (PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    forall a. a -> [a] -> [a]
    : Changes
    -> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
    translateTel Changes
    rest [(PatVarName, Dom Type)]
    tel
    translateTel []              []           = []
    translateTel (Left Pattern
    _ : Changes
    _)    []           = [Maybe (PatVarName, Dom Type)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    translateTel []              ((PatVarName, Dom Type)
    _ : [(PatVarName, Dom Type)]
    _)      = [Maybe (PatVarName, Dom Type)]
    forall a. HasCallStack => a
    __IMPOSSIBLE__