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

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

import Control.Arrow          ( first, second )
import Control.Monad          ( forM, join, 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 qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Common.Pretty (Pretty(..), prettyShow)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I

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

import Agda.Interaction.Options

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

import Agda.Utils.Impossible

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

-- | Take a record pattern @p@ and yield a list of projections
--   corresponding to the pattern variables, from left to right.
--
--   E.g. for @(x , (y , z))@ we return @[ fst, fst . snd, snd . snd ]@.
--
--   If it is not a record pattern, error 'ShouldBeRecordPattern' is raised.
recordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections DeBruijnPattern
p =
  case DeBruijnPattern
p of
    VarP{}       -> forall (m :: * -> *) a. Monad m => a -> m a
return [ forall a. a -> a
id ]
    LitP{}       -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
    DotP{}       -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
    ConP ConHead
c ConPatternInfo
ci NAPs
ps -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ConPatternInfo -> Bool
conPRecord ConPatternInfo
ci) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
      let t :: Type
t = forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
ci
      forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.rec" Nat
45 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"recordPatternToProjections: "
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"constructor pattern " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DeBruijnPattern
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" has type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        ]
      forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> PatVarName -> m ()
reportSLn PatVarName
"tc.rec" Nat
70 forall a b. (a -> b) -> a -> b
$ PatVarName
"  type raw: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> PatVarName
show Type
t
      [Dom QName]
fields <- Type -> TCM [Dom QName]
getRecordTypeFields Type
t
      forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Term -> Term) -> DeBruijnPattern -> TCM [Term -> Term]
comb (forall a b. (a -> b) -> [a] -> [b]
map forall {t} {t}. Apply t => Dom' t QName -> t -> t
proj [Dom QName]
fields) (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg NAPs
ps)
    ProjP{}      -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- copattern cannot appear here
    IApplyP{}    -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
    DefP{}       -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
  where
    proj :: Dom' t QName -> t -> t
proj Dom' t QName
p = (forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem forall a b. (a -> b) -> a -> b
$ 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 = forall a b. (a -> b) -> [a] -> [b]
map (\ Term -> Term
f -> Term -> Term
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
prj) 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 =  forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (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) =
  forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo QName
c forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
    DataCon Nat
n           -> (Bool
False, Nat
n)
    RecordCon PatternOrCopattern
_ HasEta
eta Nat
n [Dom QName]
_ -> (HasEta
eta forall a. Eq a => a -> a -> Bool
== forall a. HasEta' a
YesEta, Nat
n)
getEtaAndArity (SplitLit Literal
l) = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Nat
0)
getEtaAndArity SplitTag
SplitCatchall = 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 = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc.record" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"translate record patterns in compiled clauses"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty CompiledClauses
cc
    ]
  CompiledClauses
cc <- CompiledClauses -> m CompiledClauses
loop CompiledClauses
cc
  forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc.record" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"translated compiled clauses (no eta record patterns):"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty CompiledClauses
cc
    ]
  CompiledClauses
cc <- forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns CompiledClauses
cc
  forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc.record" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"translated compiled clauses (record expressions to copatterns):"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty CompiledClauses
cc
    ]
  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{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
      Done{}    -> 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 <- 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   <- 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 = (, forall a. Maybe a
Nothing) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = (forall k a. Map k a
Map.empty,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConHead
ch,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 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
            forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe ConstructorInfo)
getConstructorInfo' QName
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
              Just (RecordCon PatternOrCopattern
pm HasEta
YesEta Nat
_ar [Dom QName]
fs) -> WithArity CompiledClauses
-> ConHead
-> m (Map QName (WithArity CompiledClauses),
      Maybe (ConHead, WithArity CompiledClauses))
yesEtaCase WithArity CompiledClauses
b forall a b. (a -> b) -> a -> b
$
                QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c (forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
pm) Induction
Inductive (forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom QName]
fs)
              Maybe ConstructorInfo
_ -> m (Map QName (WithArity CompiledClauses),
   Maybe (ConHead, WithArity CompiledClauses))
noEtaCase
          [(QName, WithArity CompiledClauses)]
_ -> m (Map QName (WithArity CompiledClauses),
   Maybe (ConHead, WithArity CompiledClauses))
noEtaCase
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 values to use copatterns instead.
--   This allows e.g. termination-checking constructor-style coinduction.
--
--   For example:
--
--   @
--     nats : Nat → Stream Nat
--     nats n = n ∷ nats (1 + n)
--   @
--
--   The clause is translated to:
--
--   @
--     nats n .head = n
--     nats n .tail = nats (1 + n)
--   @
--
--   A change is signalled if definitional equalities might not hold after the
--   translation, e.g. if a non-eta constructor was turned to copattern matching.
recordRHSsToCopatterns ::
     forall m. (MonadChange m, PureTCM m)
  => [Clause]
  -> m [Clause]
recordRHSsToCopatterns :: forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
[Clause] -> m [Clause]
recordRHSsToCopatterns [Clause]
cls = do
  forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> PatVarName -> m ()
reportSLn PatVarName
"tc.inline.con" Nat
40 forall a b. (a -> b) -> a -> b
$ PatVarName
"enter recordRHSsToCopatterns with " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> PatVarName
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Clause]
cls) forall a. [a] -> [a] -> [a]
++ PatVarName
" clauses"
  forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
Clause -> m [Clause]
recordRHSToCopatterns [Clause]
cls

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

  case Clause
cl of

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

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

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

          -- If it may change definitional equality,
          -- announce that the translation actually fired.
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
eta forall (m :: * -> *). MonadChange m => m ()
tellDirty

          -- Iterate the translation for nested constructor rhss.
          forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
[Clause] -> m [Clause]
recordRHSsToCopatterns forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do

            -- Create one clause per projection.
            forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip [Arg QName]
fs [Arg Term]
vs) forall a b. (a -> b) -> a -> b
$ \ (Arg QName
f, Arg Term
v) -> do

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

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

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

              -- Make clause ... .f = v
              forall (m :: * -> *) a. Monad m => a -> m a
return Clause
cl
                { namedClausePats :: NAPs
namedClausePats = NAPs
ps forall a. [a] -> [a] -> [a]
++ [ forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
ProjSystem forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg QName
f ]
                , clauseBody :: Maybe Term
clauseBody      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
v
                , clauseType :: Maybe (Arg Type)
clauseType      = Maybe (Arg Type)
mt'
                }

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

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

-- | Transform definitions returning record expressions to use copatterns
--   instead. This prevents terms from blowing up when reduced.
recordExpressionsToCopatterns
  :: (HasConstInfo m, MonadChange m)
  => CompiledClauses
  -> m CompiledClauses
recordExpressionsToCopatterns :: forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns = \case
    Case Arg Nat
i Case CompiledClauses
bs -> forall a.
Arg Nat -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Nat
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns Case CompiledClauses
bs
    cc :: CompiledClauses
cc@Fail{} -> forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
    cc :: CompiledClauses
cc@(Done [Arg PatVarName]
xs (Con ConHead
c ConInfo
ConORec Elims
es)) -> do  -- don't translate if using the record /constructor/
      let vs :: [Term]
vs = forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      Bool
irrProj <- PragmaOptions -> Bool
optIrrelevantProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo (ConHead -> QName
conName ConHead
c) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
        RecordCon PatternOrCopattern
CopatternMatching HasEta
YesEta Nat
ar [Dom QName]
fs
          | Nat
ar forall a. Ord a => a -> a -> Bool
> Nat
0                                     -- only for eta-records with at least one field
          , forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Term]
vs forall a. Eq a => a -> a -> Bool
== Nat
ar                            -- where the constructor application is saturated
          , Bool
irrProj Bool -> Bool -> Bool
|| Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. LensRelevance a => a -> Bool
isIrrelevant [Dom QName]
fs) -> do -- and irrelevant projections (if any) are allowed
              forall (m :: * -> *). MonadChange m => m ()
tellDirty
              forall a.
Arg Nat -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg PatVarName]
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
                -- translate new cases recursively (there might be nested record expressions)
                forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns forall a b. (a -> b) -> a -> b
$ Branches
                  { projPatterns :: Bool
projPatterns   = Bool
True
                  , conBranches :: Map QName (WithArity CompiledClauses)
conBranches    = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$
                      forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Dom QName
f Term
v -> (forall t e. Dom' t e -> e
unDom Dom QName
f, forall c. Nat -> c -> WithArity c
WithArity Nat
0 forall a b. (a -> b) -> a -> b
$ forall a. [Arg PatVarName] -> a -> CompiledClauses' a
Done [Arg PatVarName]
xs Term
v)) [Dom QName]
fs [Term]
vs
                  , etaBranch :: Maybe (ConHead, WithArity CompiledClauses)
etaBranch      = forall a. Maybe a
Nothing
                  , litBranches :: Map Literal CompiledClauses
litBranches    = forall k a. Map k a
Map.empty
                  , catchAllBranch :: Maybe CompiledClauses
catchAllBranch = forall a. Maybe a
Nothing
                  , fallThrough :: Maybe Bool
fallThrough    = forall a. Maybe a
Nothing
                  , lazyMatch :: Bool
lazyMatch      = Bool
False
                  }
        ConstructorInfo
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
    cc :: CompiledClauses
cc@Done{} -> 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 = forall a b. (a, b) -> b
snd forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> SplitTree -> TCM ([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 -> TCM ([Bool], SplitTree)
loop = \case
      SplittingDone Nat
n ->
        -- start with n virgin variables
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Nat -> a -> [a]
replicate Nat
n Bool
True, 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 (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
_       -> forall a. HasCallStack => a
__IMPOSSIBLE__
                  -- else retain case
                  else forall a. Arg Nat -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Nat
i LazySplit
lz SplitTrees' SplitTag
ts
        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) <- forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM SplitTrees' SplitTag
ts forall a b. (a -> b) -> a -> b
$ \ (SplitTag
c, SplitTree
t) -> do
          ([Bool]
xs, SplitTree
t) <- SplitTree -> TCM ([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) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
i [Bool]
xs
              ([Bool]
xs1, [Bool]
xs2)  = 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
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
xs1
              -- xs' = updated variables
              xs' :: [Bool]
xs'         = [Bool]
xs0 forall a. [a] -> [a] -> [a]
++ Bool
x forall a. a -> [a] -> [a]
: [Bool]
xs2
              -- delete splits from t if record match
              t' :: SplitTree
t'          = if Bool
x then forall a. DropFrom a => Nat -> Nat -> a -> a
dropFrom Nat
i (Nat
n forall a. Num a => a -> a -> a
- Nat
1) SplitTree
t else SplitTree
t
          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 = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
rs
      -- invariant: if record constructor, then exactly one constructor
      if Bool
x then forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Bool]
rs forall a. Eq a => a -> a -> Bool
== [Bool
True]) forall a. HasCallStack => a
__IMPOSSIBLE__
      -- else no record constructor
       else forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
rs) forall a. HasCallStack => a
__IMPOSSIBLE__
      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 -> forall a. Nat -> SplitTree' a
SplittingDone (Nat
m 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 forall a. Ord a => a -> a -> Bool
>= Nat
i forall a. Num a => a -> a -> a
+ Nat
n -> forall a. Arg Nat -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Nat
j forall a. Num a => a -> a -> a
- Nat
n) LazySplit
lz forall a b. (a -> b) -> a -> b
$ forall a. DropFrom a => Nat -> Nat -> a -> a
dropFrom Nat
i Nat
n SplitTrees' c
ts
      | Nat
j forall a. Ord a => a -> a -> Bool
< Nat
i      -> forall a. Arg Nat -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Nat
x LazySplit
lz forall a b. (a -> b) -> a -> b
$ forall a. DropFrom a => Nat -> Nat -> a -> a
dropFrom Nat
i Nat
n SplitTrees' c
ts
      | Bool
otherwise  -> 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, 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 = forall a b. (a -> b) -> [a] -> [b]
map (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) <- forall a. RecPatM a -> TCM a
runRecPatM forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
translatePatterns forall a b. (a -> b) -> a -> b
$ forall a b. LabelPatVars a b => b -> a
unnumberPatVars forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
clause

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

      s' :: [Term]
s'   = forall a. [a] -> [a]
reverse [Term]
s
      mkSub :: [Term] -> Substitution' Term
mkSub [Term]
s = [Term]
s forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Permutation
clausePerm Clause
clause
      rhsSubst' :: Substitution' Term
rhsSubst' = [Term] -> Substitution' Term
mkSub forall a b. (a -> b) -> a -> b
$ 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 =
        forall a. Permutation -> [a] -> [a]
permute (Nat -> Permutation -> Permutation
invertP forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
compactP Permutation
perm) forall a b. (a -> b) -> a -> b
$
        forall a b. [a] -> [b] -> [(a, b)]
zip (Telescope -> [PatVarName]
teleNames forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
clause) forall a b. (a -> b) -> a -> b
$
        forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel 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 = forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst
      newTel' :: [Maybe (PatVarName, Dom Type)]
newTel' =
        forall {d}.
Substitution' (SubstArg (Dom Type))
-> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
substTel Substitution' Term
rhsSubst' forall a b. (a -> b) -> a -> b
$
        Changes
-> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
translateTel Changes
cs 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 forall a b. (a -> b) -> a -> b
$
                  [Dom Type] -> Permutation
reorderTel_ forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall b a. b -> (a -> b) -> Maybe a -> b
maybe HasCallStack => Dom Type
__DUMMY_DOM__ 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 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 (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not 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' = forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming 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 = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
lhsSubst' Substitution' Term
rhsSubst'

      -- The new telescope.
      newTel :: Telescope
newTel =
        forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [PatVarName] -> [Dom Type] -> Telescope
unflattenTel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$
        forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__) forall a b. (a -> b) -> a -> b
$
        forall a. Permutation -> [a] -> [a]
permute Permutation
newPerm forall a b. (a -> b) -> a -> b
$
        forall {d}.
Substitution' (SubstArg (Dom Type))
-> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
substTel Substitution' Term
lhsSubst' 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 = forall a b.
(LabelPatVars a b, PatVarLabel b ~ Nat) =>
Nat -> Permutation -> a -> b
numberPatVars forall a. HasCallStack => a
__IMPOSSIBLE__ Permutation
newPerm forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
lhsSubst [NamedArg Pattern]
ps
            , clauseBody :: Maybe Term
clauseBody      = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
lhsSubst forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
clause
            }

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

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

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

  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 -> 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
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
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
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
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
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
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
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 (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) <- forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix forall a b. (a -> b) -> a -> b
$ \ ~(a1
_, Nat
noVars) ->
                              forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Nat (StateT Nat IO) a1
m Nat
noVars) Nat
0
             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 = forall a. TCMT (ReaderT Nat (StateT Nat IO)) a -> RecPatM a
RecPatM forall a b. (a -> b) -> a -> b
$ do
  Nat
n <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall s (m :: * -> *). MonadState s m => m s
get
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
succ Nat
n
  Nat
noVars <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall r (m :: * -> *). MonadReader r m => m r
ask
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Pattern' a
varP PatVarName
"r", Nat -> Term
var forall a b. (a -> b) -> a -> b
$ Nat
noVars forall a. Num a => a -> a -> a
- Nat
n 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
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:" forall a. Doc a -> Doc a -> Doc a
P.<+> forall a. PatVarName -> Doc a
P.text (forall a. Show a => a -> PatVarName
show forall a b. (a -> b) -> a -> b
$ Kind -> Nat
f Kind
VarPat) forall a. Doc a -> Doc a -> Doc a
P.<+>
    Doc
"DotPat:"  forall a. Doc a -> Doc a -> Doc a
P.<+> forall a. PatVarName -> Doc a
P.text (forall a. Show a => a -> PatVarName
show forall a b. (a -> b) -> a -> b
$ Kind -> Nat
f Kind
DotPat)) forall a. Semigroup a => a -> a -> a
<> Doc
")"

instance PrettyTCM (Kind -> Nat) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => (Kind -> Nat) -> m Doc
prettyTCM = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = 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" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Kind -> Nat
f forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text PatVarName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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{})) = [(forall a. a -> a
id, Kind
DotPat)]
projections (Leaf (VarP{})) = [(forall a. a -> a
id, Kind
VarPat)]
projections (Leaf Pattern
_)        = forall a. HasCallStack => a
__IMPOSSIBLE__
projections (RecCon Arg Type
_ [(Term -> Term, RecordTree)]
args) =
  forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Term -> Term
p, RecordTree
t) -> forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
p)) 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  = 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 = forall (t :: * -> *) a. Foldable t => t a -> Nat
length forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
== Kind
k) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Term -> Term, Kind)]
ps

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case RecordTree
tree of
    Leaf Pattern
p     -> (Pattern
p,   [Term]
s, [forall a b. a -> Either a b
Left Pattern
p])
    RecCon Arg Type
t [(Term -> Term, RecordTree)]
_ -> (Pattern
pat, [Term]
s, [forall a b. b -> Either a b
Right (Kind -> Nat
count, PatVarName
"r", 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
      forall (m :: * -> *) a. Monad m => a -> m a
return (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
      forall (m :: * -> *) a. Monad m => a -> m a
return (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{} = forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
p, [], [])
translatePattern p :: Pattern
p@ProjP{}= forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
p, [], [])
translatePattern p :: Pattern
p@IApplyP{}= 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) <- forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg Pattern]
ps
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Pattern
p -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern
p forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$)) [Pattern]
ps' [NamedArg Pattern]
ps, forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Term]]
ss, 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
ci
  [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
rs <- 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg Pattern]
ps
  case forall a b. [Either a b] -> Maybe [b]
allRight [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
rs of
    Maybe [RecordTree]
Nothing ->
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ do
        ([Pattern]
ps', [[Term]]
ss, [Changes]
cs) <- forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id RecordTree -> RecPatM (Pattern, [Term], Changes)
removeTree) [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
rs
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci ([Pattern]
ps' forall a b. [a] -> [NamedArg b] -> [NamedArg a]
`withNamedArgsFrom` [NamedArg Pattern]
ps),
                forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Term]]
ss, forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Changes]
cs)
    Just [RecordTree]
ts -> forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      Arg Type
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Arg Type
t
      forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.rec" Nat
45 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"recordTree: "
        , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"constructor pattern " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Pattern
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" has type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (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 = (forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' t QName
p])
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ Arg Type -> [(Term -> Term, RecordTree)] -> RecordTree
RecCon Arg Type
t forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map 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]
_) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern Pattern
p
recordTree p :: Pattern
p@DefP{} = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern Pattern
p
recordTree p :: Pattern
p@VarP{} = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Pattern -> RecordTree
Leaf Pattern
p))
recordTree p :: Pattern
p@DotP{} = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Pattern -> RecordTree
Leaf Pattern
p))
recordTree p :: Pattern
p@LitP{} = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern Pattern
p
recordTree p :: Pattern
p@ProjP{}= forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern Pattern
p
recordTree p :: Pattern
p@IApplyP{}= forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left 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 = forall a. Maybe a
Nothing 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 = forall a. a -> Maybe a
Just (PatVarName
x, Dom Type
t) forall a. a -> [a] -> [a]
:
                                              Changes
-> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
translateTel Changes
rest
                                                (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)    = forall a. a -> Maybe a
Just (PatVarName, Dom Type)
t 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
_)    []           = forall a. HasCallStack => a
__IMPOSSIBLE__
translateTel []              ((PatVarName, Dom Type)
_ : [(PatVarName, Dom Type)]
_)      = forall a. HasCallStack => a
__IMPOSSIBLE__