{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-- | 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.Fix
import Control.Monad.Reader
import Control.Monad.State

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.Maybe
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
x -> Term
x ]
    LitP{}       -> TypeError -> TCM [Term -> Term]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM [Term -> Term])
-> TypeError -> TCM [Term -> Term]
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
    ConP ConHead
c ConPatternInfo
ci [NamedArg DeBruijnPattern]
ps -> do
      Bool -> TCMT IO () -> TCMT IO ()
forall (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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
      VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec" VerboseLevel
45 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"recordPatternToProjections: "
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"constructor pattern " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DeBruijnPattern
p TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" has type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
        ]
      VerboseKey -> VerboseLevel -> VerboseKey -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.rec" VerboseLevel
70 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"  type raw: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Type -> VerboseKey
forall a. Show a => a -> VerboseKey
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) ((NamedArg DeBruijnPattern -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg [NamedArg DeBruijnPattern]
ps)
    ProjP{}      -> TCM [Term -> Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ -- copattern cannot appear here
    IApplyP{}    -> TypeError -> TCM [Term -> Term]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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, VerboseLevel)
getEtaAndArity (SplitCon QName
c) =
  TCMT IO ConstructorInfo
-> (ConstructorInfo -> (Bool, VerboseLevel))
-> TCM (Bool, VerboseLevel)
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, VerboseLevel))
 -> TCM (Bool, VerboseLevel))
-> (ConstructorInfo -> (Bool, VerboseLevel))
-> TCM (Bool, VerboseLevel)
forall a b. (a -> b) -> a -> b
$ \case
    DataCon VerboseLevel
n        -> (Bool
False, VerboseLevel
n)
    RecordCon HasEta
eta [Dom QName]
fs -> (HasEta
eta HasEta -> HasEta -> Bool
forall a. Eq a => a -> a -> Bool
== HasEta
YesEta, [Dom QName] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [Dom QName]
fs)
getEtaAndArity (SplitLit Literal
l) = (Bool, VerboseLevel) -> TCM (Bool, VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, VerboseLevel
0)
getEtaAndArity SplitTag
SplitCatchall = (Bool, VerboseLevel) -> TCM (Bool, VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, VerboseLevel
1)

translateCompiledClauses
  :: forall m. (HasConstInfo m, MonadChange m)
  => CompiledClauses -> m CompiledClauses
translateCompiledClauses :: 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
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc.record" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"translate record patterns in compiled clauses"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM 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
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc.record" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"translated compiled clauses (no eta record patterns):"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM 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
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.cc.record" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"translated compiled clauses (record expressions to copatterns):"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM 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
      CompiledClauses
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 VerboseLevel
i Case CompiledClauses
cs -> Arg VerboseLevel -> Case CompiledClauses -> m CompiledClauses
loops Arg VerboseLevel
i Case CompiledClauses
cs

    loops :: Arg Int              -- ^ split variable
          -> Case CompiledClauses -- ^ original split tree
          -> m CompiledClauses
    loops :: Arg VerboseLevel -> Case CompiledClauses -> m CompiledClauses
loops Arg VerboseLevel
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 a)
noEtaCase = (, Maybe a
forall a. Maybe a
Nothing) (Map QName (WithArity CompiledClauses)
 -> (Map QName (WithArity CompiledClauses), Maybe a))
-> m (Map QName (WithArity CompiledClauses))
-> m (Map QName (WithArity CompiledClauses), Maybe a)
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 :: t -> t CompiledClauses -> m (Map k a, Maybe (t, t CompiledClauses))
yesEtaCase t
ch t CompiledClauses
b = (Map k a
forall k a. Map k a
Map.empty,) (Maybe (t, t CompiledClauses)
 -> (Map k a, Maybe (t, t CompiledClauses)))
-> (t CompiledClauses -> Maybe (t, t CompiledClauses))
-> t CompiledClauses
-> (Map k a, Maybe (t, t CompiledClauses))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t, t CompiledClauses) -> Maybe (t, t CompiledClauses)
forall a. a -> Maybe a
Just ((t, t CompiledClauses) -> Maybe (t, t CompiledClauses))
-> (t CompiledClauses -> (t, t CompiledClauses))
-> t CompiledClauses
-> Maybe (t, t CompiledClauses)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t
ch,) (t CompiledClauses -> (Map k a, Maybe (t, t CompiledClauses)))
-> m (t CompiledClauses)
-> m (Map k a, Maybe (t, t CompiledClauses))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CompiledClauses -> m CompiledClauses)
-> t CompiledClauses -> m (t CompiledClauses)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompiledClauses -> m CompiledClauses
loop t 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 -> ConHead
-> WithArity CompiledClauses
-> m (Map QName (WithArity CompiledClauses),
      Maybe (ConHead, WithArity CompiledClauses))
forall (t :: * -> *) t k a.
Traversable t =>
t -> t CompiledClauses -> m (Map k a, Maybe (t, t CompiledClauses))
yesEtaCase ConHead
ch WithArity CompiledClauses
b
          [(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 HasEta
YesEta [Dom QName]
fs ->
                let ch :: ConHead
ch = QName -> Induction -> [Arg QName] -> ConHead
ConHead QName
c 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) in
                ConHead
-> WithArity CompiledClauses
-> m (Map QName (WithArity CompiledClauses),
      Maybe (ConHead, WithArity CompiledClauses))
forall (t :: * -> *) t k a.
Traversable t =>
t -> t CompiledClauses -> m (Map k a, Maybe (t, t CompiledClauses))
yesEtaCase ConHead
ch WithArity CompiledClauses
b
              ConstructorInfo
_ -> m (Map QName (WithArity CompiledClauses),
   Maybe (ConHead, WithArity CompiledClauses))
forall a. m (Map QName (WithArity CompiledClauses), Maybe a)
noEtaCase
          [(QName, WithArity CompiledClauses)]
_ -> m (Map QName (WithArity CompiledClauses),
   Maybe (ConHead, WithArity CompiledClauses))
forall a. m (Map QName (WithArity CompiledClauses), Maybe a)
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 VerboseLevel -> Case CompiledClauses -> CompiledClauses
forall a.
Arg VerboseLevel -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg VerboseLevel
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 :: CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns = \case
    Case Arg VerboseLevel
i Case CompiledClauses
bs -> Arg VerboseLevel -> Case CompiledClauses -> CompiledClauses
forall a.
Arg VerboseLevel -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg VerboseLevel
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@CompiledClauses
Fail   -> CompiledClauses -> m CompiledClauses
forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
    cc :: CompiledClauses
cc@(Done [Arg VerboseKey]
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 -> VerboseLevel
conArity = VerboseLevel
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 HasEta
YesEta [Dom QName]
fs
          | VerboseLevel
ar <- [Dom QName] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Dom QName]
fs, VerboseLevel
ar VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0,                   -- only for eta-records with at least one field
            [Term] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Term]
vs VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
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 VerboseLevel -> Case CompiledClauses -> CompiledClauses
forall a.
Arg VerboseLevel -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (VerboseLevel -> Arg VerboseLevel
forall a. a -> Arg a
defaultArg (VerboseLevel -> Arg VerboseLevel)
-> VerboseLevel -> Arg VerboseLevel
forall a b. (a -> b) -> a -> b
$ [Arg VerboseKey] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Arg VerboseKey]
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    = [(QName, WithArity CompiledClauses)]
-> Map QName (WithArity CompiledClauses)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(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, VerboseLevel -> CompiledClauses -> WithArity CompiledClauses
forall c. VerboseLevel -> c -> WithArity c
WithArity VerboseLevel
0 (CompiledClauses -> WithArity CompiledClauses)
-> CompiledClauses -> WithArity CompiledClauses
forall a b. (a -> b) -> a -> b
$ [Arg VerboseKey] -> Term -> CompiledClauses
forall a. [Arg VerboseKey] -> a -> CompiledClauses' a
Done [Arg VerboseKey]
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 t = snd <$> loop t
--  where
--
--    loop :: SplitTree -> TCM ([Bool], RecordSplitTree)
--    loop t = case t of
--      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 SplitTree
t = ([Bool], SplitTree) -> SplitTree
forall a b. (a, b) -> b
snd (([Bool], SplitTree) -> SplitTree)
-> TCMT IO ([Bool], SplitTree) -> TCM SplitTree
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SplitTree -> TCMT IO ([Bool], SplitTree)
loop SplitTree
t
  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 SplitTree
t = case SplitTree
t of
      SplittingDone VerboseLevel
n ->
        -- start with n virgin variables
        ([Bool], SplitTree) -> TCMT IO ([Bool], SplitTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel -> Bool -> [Bool]
forall a. VerboseLevel -> a -> [a]
replicate VerboseLevel
n Bool
True, VerboseLevel -> SplitTree
forall a. VerboseLevel -> SplitTree' a
SplittingDone VerboseLevel
n)
      SplitAt Arg VerboseLevel
i LazySplit
lz SplitTrees' SplitTag
ts    -> do
        (Bool
x, [Bool]
xs, SplitTrees' SplitTag
ts) <- VerboseLevel
-> SplitTrees' SplitTag -> TCM (Bool, [Bool], SplitTrees' SplitTag)
loops (Arg VerboseLevel -> VerboseLevel
forall e. Arg e -> e
unArg Arg VerboseLevel
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 VerboseLevel -> LazySplit -> SplitTrees' SplitTag -> SplitTree
forall a.
Arg VerboseLevel -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg VerboseLevel
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 :: VerboseLevel
-> SplitTrees' SplitTag -> TCM (Bool, [Bool], SplitTrees' SplitTag)
loops VerboseLevel
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, VerboseLevel
n) <- SplitTag -> TCM (Bool, VerboseLevel)
getEtaAndArity SplitTag
c
          -- now drop variables from i to i+n-1
          let ([Bool]
xs0, [Bool]
rest) = VerboseLevel -> [Bool] -> ([Bool], [Bool])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
i [Bool]
xs
              ([Bool]
xs1, [Bool]
xs2)  = VerboseLevel -> [Bool] -> ([Bool], [Bool])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
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 VerboseLevel -> VerboseLevel -> SplitTree -> SplitTree
forall a. DropFrom a => VerboseLevel -> VerboseLevel -> a -> a
dropFrom VerboseLevel
i (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
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 ()
unless ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
rs Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False) 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 :: VerboseLevel -> VerboseLevel -> SplitTree' c -> SplitTree' c
dropFrom VerboseLevel
i VerboseLevel
n SplitTree' c
t = case SplitTree' c
t of
    SplittingDone VerboseLevel
m -> VerboseLevel -> SplitTree' c
forall a. VerboseLevel -> SplitTree' a
SplittingDone (VerboseLevel
m VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
n)
    SplitAt x :: Arg VerboseLevel
x@(Arg ArgInfo
ai VerboseLevel
j) LazySplit
lz SplitTrees' c
ts
      | VerboseLevel
j VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
>= VerboseLevel
i VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
n -> Arg VerboseLevel -> LazySplit -> SplitTrees' c -> SplitTree' c
forall a.
Arg VerboseLevel -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt (ArgInfo -> VerboseLevel -> Arg VerboseLevel
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (VerboseLevel -> Arg VerboseLevel)
-> VerboseLevel -> Arg VerboseLevel
forall a b. (a -> b) -> a -> b
$ VerboseLevel
j VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
n) LazySplit
lz (SplitTrees' c -> SplitTree' c) -> SplitTrees' c -> SplitTree' c
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> VerboseLevel -> SplitTrees' c -> SplitTrees' c
forall a. DropFrom a => VerboseLevel -> VerboseLevel -> a -> a
dropFrom VerboseLevel
i VerboseLevel
n SplitTrees' c
ts
      | VerboseLevel
j VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
i      -> Arg VerboseLevel -> LazySplit -> SplitTrees' c -> SplitTree' c
forall a.
Arg VerboseLevel -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg VerboseLevel
x LazySplit
lz (SplitTrees' c -> SplitTree' c) -> SplitTrees' c -> SplitTree' c
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> VerboseLevel -> SplitTrees' c -> SplitTrees' c
forall a. DropFrom a => VerboseLevel -> VerboseLevel -> a -> a
dropFrom VerboseLevel
i VerboseLevel
n SplitTrees' c
ts
      | Bool
otherwise  -> SplitTree' c
forall a. HasCallStack => a
__IMPOSSIBLE__

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

instance DropFrom a => DropFrom [a] where
  dropFrom :: VerboseLevel -> VerboseLevel -> [a] -> [a]
dropFrom VerboseLevel
i VerboseLevel
n [a]
ts = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel -> VerboseLevel -> a -> a
forall a. DropFrom a => VerboseLevel -> VerboseLevel -> a -> a
dropFrom VerboseLevel
i VerboseLevel
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
$ [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b i. LabelPatVars a b i => b -> a
unnumberPatVars ([NamedArg DeBruijnPattern] -> [NamedArg Pattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
clause

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

      s' :: [Term]
s'   = [Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
s
      mkSub :: [a] -> Substitution' a
mkSub [a]
s = [a]
s [a] -> Substitution' a -> Substitution' a
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# VerboseLevel -> Substitution' a
forall a. VerboseLevel -> Substitution' a
raiseS VerboseLevel
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
forall a. DeBruijn a => [a] -> Substitution' a
mkSub [Term]
s'

      -- 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
forall a. DeBruijn a => [a] -> Substitution' a
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 :: [(VerboseKey, Dom Type)]
flattenedOldTel =
        Permutation -> [(VerboseKey, Dom Type)] -> [(VerboseKey, Dom Type)]
forall a. Permutation -> [a] -> [a]
permute (VerboseLevel -> Permutation -> Permutation
invertP VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__ (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
compactP Permutation
perm) ([(VerboseKey, Dom Type)] -> [(VerboseKey, Dom Type)])
-> [(VerboseKey, Dom Type)] -> [(VerboseKey, Dom Type)]
forall a b. (a -> b) -> a -> b
$
        [VerboseKey] -> [Dom Type] -> [(VerboseKey, Dom Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Telescope -> [VerboseKey]
teleNames (Telescope -> [VerboseKey]) -> Telescope -> [VerboseKey]
forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
clause) ([Dom Type] -> [(VerboseKey, Dom Type)])
-> [Dom Type] -> [(VerboseKey, Dom Type)]
forall a b. (a -> b) -> a -> b
$
        Telescope -> [Dom Type]
forall a. Subst Term 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' Term
-> [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' Term
    -> Maybe (d, Dom Type) -> Maybe (d, Dom Type))
-> Substitution' Term
-> [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' Term -> (d, Dom Type) -> (d, Dom Type))
-> Substitution' Term
-> 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' Term -> Dom Type -> Dom Type)
-> Substitution' Term
-> (d, Dom Type)
-> (d, Dom Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution' Term -> Dom Type -> Dom Type
forall t a. Subst t a => Substitution' t -> a -> a
applySubst
      newTel' :: [Maybe (VerboseKey, Dom Type)]
newTel' =
        Substitution' Term
-> [Maybe (VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
forall d.
Substitution' Term
-> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
substTel Substitution' Term
rhsSubst' ([Maybe (VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)])
-> [Maybe (VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
forall a b. (a -> b) -> a -> b
$
        Changes
-> [(VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
translateTel Changes
cs ([(VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)])
-> [(VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
forall a b. (a -> b) -> a -> b
$
        [(VerboseKey, 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 (VerboseKey, Dom Type) -> Dom Type)
-> [Maybe (VerboseKey, Dom Type)] -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map (Dom Type
-> ((VerboseKey, Dom Type) -> Dom Type)
-> Maybe (VerboseKey, Dom Type)
-> Dom Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Dom Type
HasCallStack => Dom Type
__DUMMY_DOM__ (VerboseKey, Dom Type) -> Dom Type
forall a b. (a, b) -> b
snd) [Maybe (VerboseKey, Dom Type)]
newTel'
        -- It is important that __DUMMY_DOM__ does not mention any variable
        -- (see the definition of reorderTel).
        where
        isDotP :: i -> Bool
isDotP i
n = case Changes -> i -> Change
forall i a. Integral i => [a] -> i -> a
List.genericIndex Changes
cs i
n of
                     Left DotP{} -> Bool
True
                     Change
_           -> Bool
False

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

      -- Substitution used to convert terms in the new RHS's context
      -- to terms in the new telescope's context.
      lhsSubst' :: Substitution' Term
lhsSubst' = {-'-} Empty -> Permutation -> Substitution' Term
forall a. DeBruijn a => Empty -> Permutation -> Substitution' a
renaming Empty
forall a. HasCallStack => a
__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' Term -> Substitution' Term -> Substitution' Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
lhsSubst' Substitution' Term
rhsSubst'

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

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

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

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

  VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.lhs.recpat" VerboseLevel
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    Empty -> VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *) a.
MonadAddContext m =>
Empty -> VerboseLevel -> m a -> m a
escapeContext Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size (Telescope -> VerboseLevel) -> Telescope -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
clause) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
      [ TCM Doc
"Translated clause:"
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"delta =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Clause -> Telescope
clauseTel Clause
c)
        , TCM Doc
"ps    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text ([Arg DeBruijnPattern] -> VerboseKey
forall a. Show a => a -> VerboseKey
show ([Arg DeBruijnPattern] -> VerboseKey)
-> [Arg DeBruijnPattern] -> VerboseKey
forall a b. (a -> b) -> a -> b
$ Clause -> [Arg DeBruijnPattern]
clausePats Clause
c)
        , TCM Doc
"body  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (Maybe Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show (Maybe Term -> VerboseKey) -> Maybe Term -> VerboseKey
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
c)
        , TCM Doc
"body  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
c) (TCM Doc -> (Term -> TCM Doc) -> Maybe Term -> TCM Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCM Doc
"_|_" Term -> TCM 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 (a -> RecPatM b -> RecPatM a
(a -> b) -> RecPatM a -> RecPatM b
(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
<$ :: a -> RecPatM b -> RecPatM a
$c<$ :: forall a b. a -> RecPatM b -> RecPatM a
fmap :: (a -> b) -> RecPatM a -> RecPatM b
$cfmap :: forall a b. (a -> b) -> RecPatM a -> RecPatM b
Functor, Functor RecPatM
a -> RecPatM a
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
RecPatM a -> RecPatM b -> RecPatM b
RecPatM a -> RecPatM b -> RecPatM a
RecPatM (a -> b) -> RecPatM a -> RecPatM b
(a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c
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
<* :: RecPatM a -> RecPatM b -> RecPatM a
$c<* :: forall a b. RecPatM a -> RecPatM b -> RecPatM a
*> :: RecPatM a -> RecPatM b -> RecPatM b
$c*> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
liftA2 :: (a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c
$cliftA2 :: forall a b c. (a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c
<*> :: RecPatM (a -> b) -> RecPatM a -> RecPatM b
$c<*> :: forall a b. RecPatM (a -> b) -> RecPatM a -> RecPatM b
pure :: a -> RecPatM a
$cpure :: forall a. a -> RecPatM a
$cp1Applicative :: Functor RecPatM
Applicative, Applicative RecPatM
a -> RecPatM a
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
RecPatM a -> (a -> RecPatM b) -> RecPatM b
RecPatM a -> RecPatM b -> RecPatM b
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 :: a -> RecPatM a
$creturn :: forall a. a -> RecPatM a
>> :: RecPatM a -> RecPatM b -> RecPatM b
$c>> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
>>= :: RecPatM a -> (a -> RecPatM b) -> RecPatM b
$c>>= :: forall a b. RecPatM a -> (a -> RecPatM b) -> RecPatM b
$cp1Monad :: Applicative RecPatM
Monad,
            Monad RecPatM
Monad RecPatM -> (forall a. IO a -> RecPatM a) -> MonadIO RecPatM
IO a -> RecPatM a
forall a. IO a -> RecPatM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> RecPatM a
$cliftIO :: forall a. IO a -> RecPatM a
$cp1MonadIO :: Monad RecPatM
MonadIO, Applicative RecPatM
MonadIO RecPatM
MonadTCState RecPatM
MonadTCEnv RecPatM
HasOptions RecPatM
Applicative RecPatM
-> MonadIO RecPatM
-> MonadTCEnv RecPatM
-> MonadTCState RecPatM
-> HasOptions RecPatM
-> (forall a. TCM a -> RecPatM a)
-> MonadTCM RecPatM
TCM a -> RecPatM a
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 :: TCM a -> RecPatM a
$cliftTCM :: forall a. TCM a -> RecPatM a
$cp5MonadTCM :: HasOptions RecPatM
$cp4MonadTCM :: MonadTCState RecPatM
$cp3MonadTCM :: MonadTCEnv RecPatM
$cp2MonadTCM :: MonadIO RecPatM
$cp1MonadTCM :: Applicative RecPatM
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
$cp3HasOptions :: Monad RecPatM
$cp2HasOptions :: Applicative RecPatM
$cp1HasOptions :: Functor RecPatM
HasOptions,
            Monad RecPatM
RecPatM TCEnv
Monad RecPatM
-> RecPatM TCEnv
-> (forall a. (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a)
-> MonadTCEnv RecPatM
(TCEnv -> TCEnv) -> RecPatM a -> RecPatM a
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 :: (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a
$clocalTC :: forall a. (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a
askTC :: RecPatM TCEnv
$caskTC :: RecPatM TCEnv
$cp1MonadTCEnv :: Monad RecPatM
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
$cp1MonadTCState :: Monad RecPatM
MonadTCState)

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

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

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

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

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

instance PrettyTCM Change where
  prettyTCM :: Change -> 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 -> VerboseLevel
f, VerboseKey
x, Dom Type
t)) = m Doc
"Change" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Kind -> VerboseLevel) -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Kind -> VerboseLevel
f m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> VerboseKey -> m Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text VerboseKey
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 -> VerboseLevel
count Kind
k = [(Term -> Term, Kind)] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([(Term -> Term, Kind)] -> VerboseLevel)
-> [(Term -> Term, Kind)] -> VerboseLevel
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 -> Change
forall a b. a -> Either a b
Left Pattern
p])
    RecCon Arg Type
t [(Term -> Term, RecordTree)]
_ -> (Pattern
pat, [Term]
s, [(Kind -> VerboseLevel, VerboseKey, Dom Type) -> Change
forall a b. b -> Either a b
Right (Kind -> VerboseLevel
count, VerboseKey
"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
      VerboseKey -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.rec" VerboseLevel
45 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
        [ TCM Doc
"recordTree: "
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"constructor pattern " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Pattern
p TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" has type " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Type -> TCM 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
-> [(VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
translateTel (Left (DotP{}) : Changes
rest)   [(VerboseKey, Dom Type)]
tel = Maybe (VerboseKey, Dom Type)
forall a. Maybe a
Nothing Maybe (VerboseKey, Dom Type)
-> [Maybe (VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
forall a. a -> [a] -> [a]
: Changes
-> [(VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
translateTel Changes
rest [(VerboseKey, Dom Type)]
tel
translateTel (Right (Kind -> VerboseLevel
n, VerboseKey
x, Dom Type
t) : Changes
rest) [(VerboseKey, Dom Type)]
tel = (VerboseKey, Dom Type) -> Maybe (VerboseKey, Dom Type)
forall a. a -> Maybe a
Just (VerboseKey
x, Dom Type
t) Maybe (VerboseKey, Dom Type)
-> [Maybe (VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
forall a. a -> [a] -> [a]
:
                                              Changes
-> [(VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
translateTel Changes
rest
                                                (VerboseLevel
-> [(VerboseKey, Dom Type)] -> [(VerboseKey, Dom Type)]
forall a. VerboseLevel -> [a] -> [a]
drop (Kind -> VerboseLevel
n Kind
VarPat) [(VerboseKey, Dom Type)]
tel)
translateTel (Left Pattern
_ : Changes
rest) ((VerboseKey, Dom Type)
t : [(VerboseKey, Dom Type)]
tel)    = (VerboseKey, Dom Type) -> Maybe (VerboseKey, Dom Type)
forall a. a -> Maybe a
Just (VerboseKey, Dom Type)
t Maybe (VerboseKey, Dom Type)
-> [Maybe (VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
forall a. a -> [a] -> [a]
: Changes
-> [(VerboseKey, Dom Type)] -> [Maybe (VerboseKey, Dom Type)]
translateTel Changes
rest [(VerboseKey, Dom Type)]
tel
translateTel []              []           = []
translateTel (Left Pattern
_ : Changes
_)    []           = [Maybe (VerboseKey, Dom Type)]
forall a. HasCallStack => a
__IMPOSSIBLE__
translateTel []              ((VerboseKey, Dom Type)
_ : [(VerboseKey, Dom Type)]
_)      = [Maybe (VerboseKey, Dom Type)]
forall a. HasCallStack => a
__IMPOSSIBLE__