module Agda.TypeChecking.RecordPatterns
( translateRecordPatterns
, translateCompiledClauses
, translateSplitTree
, recordPatternToProjections
, recordRHSToCopatterns
) where
import Control.Arrow ( first, second )
import Control.Monad ( forM, join, unless, when, zipWithM )
import Control.Monad.Fix ( mfix )
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Reader ( MonadReader(..), ReaderT(..), runReaderT )
import Control.Monad.State ( MonadState(..), StateT(..), runStateT )
import Control.Monad.Trans ( lift )
import qualified Data.List as List
import Data.Maybe
import qualified Data.Map as Map
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Common.Pretty (Pretty(..), prettyShow)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty hiding (pretty)
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Interaction.Options
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Monad
import Agda.Utils.Permutation hiding (dropFrom)
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Update (MonadChange, tellDirty)
import Agda.Utils.Impossible
recordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections :: DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections DeBruijnPattern
p =
case DeBruijnPattern
p of
VarP{} -> forall (m :: * -> *) a. Monad m => a -> m a
return [ forall a. a -> a
id ]
LitP{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
DotP{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
ConP ConHead
c ConPatternInfo
ci NAPs
ps -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ConPatternInfo -> Bool
conPRecord ConPatternInfo
ci) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
let t :: Type
t = forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
ci
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.rec" Nat
45 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"recordPatternToProjections: "
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"constructor pattern " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM DeBruijnPattern
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" has type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
]
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> PatVarName -> m ()
reportSLn PatVarName
"tc.rec" Nat
70 forall a b. (a -> b) -> a -> b
$ PatVarName
" type raw: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> PatVarName
show Type
t
[Dom QName]
fields <- Type -> TCM [Dom QName]
getRecordTypeFields Type
t
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Term -> Term) -> DeBruijnPattern -> TCM [Term -> Term]
comb (forall a b. (a -> b) -> [a] -> [b]
map forall {t} {t}. Apply t => Dom' t QName -> t -> t
proj [Dom QName]
fields) (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg NAPs
ps)
ProjP{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
IApplyP{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
DefP{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> TypeError
ShouldBeRecordPattern DeBruijnPattern
p
where
proj :: Dom' t QName -> t -> t
proj Dom' t QName
p = (forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' t QName
p])
comb :: (Term -> Term) -> DeBruijnPattern -> TCM [Term -> Term]
comb :: (Term -> Term) -> DeBruijnPattern -> TCM [Term -> Term]
comb Term -> Term
prj DeBruijnPattern
p = forall a b. (a -> b) -> [a] -> [b]
map (\ Term -> Term
f -> Term -> Term
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
prj) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections DeBruijnPattern
p
conjColumns :: [[Bool]] -> [Bool]
conjColumns :: [[Bool]] -> [Bool]
conjColumns = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Bool -> Bool -> Bool
(&&))
getEtaAndArity :: SplitTag -> TCM (Bool, Nat)
getEtaAndArity :: SplitTag -> TCM (Bool, Nat)
getEtaAndArity (SplitCon QName
c) =
forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo QName
c forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
DataCon Nat
n -> (Bool
False, Nat
n)
RecordCon PatternOrCopattern
_ HasEta
eta Nat
n [Dom QName]
_ -> (HasEta
eta forall a. Eq a => a -> a -> Bool
== forall a. HasEta' a
YesEta, Nat
n)
getEtaAndArity (SplitLit Literal
l) = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Nat
0)
getEtaAndArity SplitTag
SplitCatchall = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Nat
1)
translateCompiledClauses
:: forall m. (HasConstInfo m, MonadChange m)
=> CompiledClauses -> m CompiledClauses
translateCompiledClauses :: forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
translateCompiledClauses CompiledClauses
cc = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc.record" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"translate record patterns in compiled clauses"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty CompiledClauses
cc
]
CompiledClauses
cc <- CompiledClauses -> m CompiledClauses
loop CompiledClauses
cc
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc.record" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"translated compiled clauses (no eta record patterns):"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty CompiledClauses
cc
]
CompiledClauses
cc <- forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns CompiledClauses
cc
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.cc.record" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"translated compiled clauses (record expressions to copatterns):"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> Doc
pretty CompiledClauses
cc
]
forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
where
loop :: CompiledClauses -> m (CompiledClauses)
loop :: CompiledClauses -> m CompiledClauses
loop CompiledClauses
cc = case CompiledClauses
cc of
Fail{} -> forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
Done{} -> forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
Case Arg Nat
i Case CompiledClauses
cs -> Arg Nat -> Case CompiledClauses -> m CompiledClauses
loops Arg Nat
i Case CompiledClauses
cs
loops :: Arg Int
-> Case CompiledClauses
-> m CompiledClauses
loops :: Arg Nat -> Case CompiledClauses -> m CompiledClauses
loops Arg Nat
i cs :: Case CompiledClauses
cs@Branches{ projPatterns :: forall c. Case c -> Bool
projPatterns = Bool
comatch
, conBranches :: forall c. Case c -> Map QName (WithArity c)
conBranches = Map QName (WithArity CompiledClauses)
conMap
, etaBranch :: forall c. Case c -> Maybe (ConHead, WithArity c)
etaBranch = Maybe (ConHead, WithArity CompiledClauses)
eta
, litBranches :: forall c. Case c -> Map Literal c
litBranches = Map Literal CompiledClauses
litMap
, fallThrough :: forall c. Case c -> Maybe Bool
fallThrough = Maybe Bool
fT
, catchAllBranch :: forall c. Case c -> Maybe c
catchAllBranch = Maybe CompiledClauses
catchAll
, lazyMatch :: forall c. Case c -> Bool
lazyMatch = Bool
lazy } = do
Maybe CompiledClauses
catchAll <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompiledClauses -> m CompiledClauses
loop Maybe CompiledClauses
catchAll
Map Literal CompiledClauses
litMap <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompiledClauses -> m CompiledClauses
loop Map Literal CompiledClauses
litMap
(Map QName (WithArity CompiledClauses)
conMap, Maybe (ConHead, WithArity CompiledClauses)
eta) <- do
let noEtaCase :: m (Map QName (WithArity CompiledClauses),
Maybe (ConHead, WithArity CompiledClauses))
noEtaCase = (, forall a. Maybe a
Nothing) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) CompiledClauses -> m CompiledClauses
loop Map QName (WithArity CompiledClauses)
conMap
yesEtaCase :: WithArity CompiledClauses
-> ConHead
-> m (Map QName (WithArity CompiledClauses),
Maybe (ConHead, WithArity CompiledClauses))
yesEtaCase WithArity CompiledClauses
b ConHead
ch = (forall k a. Map k a
Map.empty,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ConHead
ch,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompiledClauses -> m CompiledClauses
loop WithArity CompiledClauses
b
case forall k a. Map k a -> [(k, a)]
Map.toList Map QName (WithArity CompiledClauses)
conMap of
[(QName, WithArity CompiledClauses)]
_ | Just (ConHead
ch, WithArity CompiledClauses
b) <- Maybe (ConHead, WithArity CompiledClauses)
eta -> WithArity CompiledClauses
-> ConHead
-> m (Map QName (WithArity CompiledClauses),
Maybe (ConHead, WithArity CompiledClauses))
yesEtaCase WithArity CompiledClauses
b ConHead
ch
[(QName
c, WithArity CompiledClauses
b)] | Bool -> Bool
not Bool
comatch ->
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe ConstructorInfo)
getConstructorInfo' QName
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
Just (RecordCon PatternOrCopattern
pm HasEta
YesEta Nat
_ar [Dom QName]
fs) -> WithArity CompiledClauses
-> ConHead
-> m (Map QName (WithArity CompiledClauses),
Maybe (ConHead, WithArity CompiledClauses))
yesEtaCase WithArity CompiledClauses
b forall a b. (a -> b) -> a -> b
$
QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c (forall p. p -> DataOrRecord' p
IsRecord PatternOrCopattern
pm) Induction
Inductive (forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom QName]
fs)
Maybe ConstructorInfo
_ -> m (Map QName (WithArity CompiledClauses),
Maybe (ConHead, WithArity CompiledClauses))
noEtaCase
[(QName, WithArity CompiledClauses)]
_ -> m (Map QName (WithArity CompiledClauses),
Maybe (ConHead, WithArity CompiledClauses))
noEtaCase
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a.
Arg Nat -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Nat
i Case CompiledClauses
cs{ conBranches :: Map QName (WithArity CompiledClauses)
conBranches = Map QName (WithArity CompiledClauses)
conMap
, etaBranch :: Maybe (ConHead, WithArity CompiledClauses)
etaBranch = Maybe (ConHead, WithArity CompiledClauses)
eta
, litBranches :: Map Literal CompiledClauses
litBranches = Map Literal CompiledClauses
litMap
, fallThrough :: Maybe Bool
fallThrough = Maybe Bool
fT
, catchAllBranch :: Maybe CompiledClauses
catchAllBranch = Maybe CompiledClauses
catchAll
}
recordRHSsToCopatterns ::
forall m. (MonadChange m, PureTCM m)
=> [Clause]
-> m [Clause]
recordRHSsToCopatterns :: forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
[Clause] -> m [Clause]
recordRHSsToCopatterns [Clause]
cls = do
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> PatVarName -> m ()
reportSLn PatVarName
"tc.inline.con" Nat
40 forall a b. (a -> b) -> a -> b
$ PatVarName
"enter recordRHSsToCopatterns with " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> PatVarName
show (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Clause]
cls) forall a. [a] -> [a] -> [a]
++ PatVarName
" clauses"
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
Clause -> m [Clause]
recordRHSToCopatterns [Clause]
cls
recordRHSToCopatterns ::
forall m. (MonadChange m, PureTCM m)
=> Clause
-> m [Clause]
recordRHSToCopatterns :: forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
Clause -> m [Clause]
recordRHSToCopatterns Clause
cl = do
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> PatVarName -> m ()
reportSLn PatVarName
"tc.inline.con" Nat
40 forall a b. (a -> b) -> a -> b
$ PatVarName
"enter recordRHSToCopatterns"
case Clause
cl of
cl :: Clause
cl@Clause{ namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps
, clauseBody :: Clause -> Maybe Term
clauseBody = Just v0 :: Term
v0@(Con con :: ConHead
con@(ConHead QName
c DataOrRecord
_ Induction
_ind [Arg QName]
fs) ConInfo
_ci Elims
es)
, clauseType :: Clause -> Maybe (Arg Type)
clauseType = Maybe (Arg Type)
mt
}
| Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Arg QName]
fs)
, forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg QName]
fs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es
, Just [Arg Term]
vs <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
-> QName -> m (Maybe Bool)
inlineConstructor QName
c forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe Bool
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return [Clause
cl]
Just Bool
eta -> do
Maybe (Arg Type)
mt <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Maybe (Arg Type)
mt
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
eta forall (m :: * -> *). MonadChange m => m ()
tellDirty
forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
[Clause] -> m [Clause]
recordRHSsToCopatterns forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip [Arg QName]
fs [Arg Term]
vs) forall a b. (a -> b) -> a -> b
$ \ (Arg QName
f, Arg Term
v) -> do
let inst :: Type -> m (Maybe Type)
inst :: Type -> m (Maybe Type)
inst Type
t = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b c. (a, b, c) -> c
thd3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
v0 Type
t ProjOrigin
ProjSystem (forall e. Arg e -> e
unArg Arg QName
f)
let fuse :: Maybe (Arg (Maybe a)) -> Maybe (Arg a)
fuse :: forall a. Maybe (Arg (Maybe a)) -> Maybe (Arg a)
fuse = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) (m :: * -> *) a.
(Decoration t, Functor m) =>
t (m a) -> m (t a)
distributeF
Maybe (Arg Type)
mt' :: Maybe (Arg Type) <- forall a. Maybe (Arg (Maybe a)) -> Maybe (Arg a)
fuse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type -> m (Maybe Type)
inst) Maybe (Arg Type)
mt
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
cl
{ namedClausePats :: NAPs
namedClausePats = NAPs
ps forall a. [a] -> [a] -> [a]
++ [ forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. ProjOrigin -> QName -> Pattern' x
ProjP ProjOrigin
ProjSystem forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg QName
f ]
, clauseBody :: Maybe Term
clauseBody = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
v
, clauseType :: Maybe (Arg Type)
clauseType = Maybe (Arg Type)
mt'
}
Clause
cl -> forall (m :: * -> *) a. Monad m => a -> m a
return [Clause
cl]
where
inlineConstructor :: QName -> m (Maybe Bool)
inlineConstructor :: QName -> m (Maybe Bool)
inlineConstructor QName
c = forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Definition -> Defn
theDef forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Constructor { QName
conData :: Defn -> QName
conData :: QName
conData, Bool
conInline :: Defn -> Bool
conInline :: Bool
conInline } -> do
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> PatVarName -> m ()
reportSLn PatVarName
"tc.inline.con" Nat
80 forall a b. (a -> b) -> a -> b
$
(PatVarName
"can" forall a. [a] -> [a] -> [a]
++) forall a b. (a -> b) -> a -> b
$ forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless Bool
conInline (PatVarName
"not" forall a. [a] -> [a] -> [a]
++) forall a b. (a -> b) -> a -> b
$ PatVarName
" inline constructor " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> PatVarName
prettyShow QName
c
if Bool -> Bool
not Bool
conInline then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
conData
Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
recordExpressionsToCopatterns
:: (HasConstInfo m, MonadChange m)
=> CompiledClauses
-> m CompiledClauses
recordExpressionsToCopatterns :: forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns = \case
Case Arg Nat
i Case CompiledClauses
bs -> forall a.
Arg Nat -> Case (CompiledClauses' a) -> CompiledClauses' a
Case Arg Nat
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns Case CompiledClauses
bs
cc :: CompiledClauses
cc@Fail{} -> forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
cc :: CompiledClauses
cc@(Done [Arg PatVarName]
xs (Con ConHead
c ConInfo
ConORec Elims
es)) -> do
let vs :: [Term]
vs = forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
Bool
irrProj <- PragmaOptions -> Bool
optIrrelevantProjections forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
forall (m :: * -> *). HasConstInfo m => QName -> m ConstructorInfo
getConstructorInfo (ConHead -> QName
conName ConHead
c) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
RecordCon PatternOrCopattern
CopatternMatching HasEta
YesEta Nat
ar [Dom QName]
fs
| Nat
ar forall a. Ord a => a -> a -> Bool
> Nat
0
, forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Term]
vs forall a. Eq a => a -> a -> Bool
== Nat
ar
, Bool
irrProj Bool -> Bool -> Bool
|| Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. LensRelevance a => a -> Bool
isIrrelevant [Dom QName]
fs) -> do
forall (m :: * -> *). MonadChange m => m ()
tellDirty
forall a.
Arg Nat -> Case (CompiledClauses' a) -> CompiledClauses' a
Case (forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Arg PatVarName]
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
(HasConstInfo m, MonadChange m) =>
CompiledClauses -> m CompiledClauses
recordExpressionsToCopatterns forall a b. (a -> b) -> a -> b
$ Branches
{ projPatterns :: Bool
projPatterns = Bool
True
, conBranches :: Map QName (WithArity CompiledClauses)
conBranches = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ Dom QName
f Term
v -> (forall t e. Dom' t e -> e
unDom Dom QName
f, forall c. Nat -> c -> WithArity c
WithArity Nat
0 forall a b. (a -> b) -> a -> b
$ forall a. [Arg PatVarName] -> a -> CompiledClauses' a
Done [Arg PatVarName]
xs Term
v)) [Dom QName]
fs [Term]
vs
, etaBranch :: Maybe (ConHead, WithArity CompiledClauses)
etaBranch = forall a. Maybe a
Nothing
, litBranches :: Map Literal CompiledClauses
litBranches = forall k a. Map k a
Map.empty
, catchAllBranch :: Maybe CompiledClauses
catchAllBranch = forall a. Maybe a
Nothing
, fallThrough :: Maybe Bool
fallThrough = forall a. Maybe a
Nothing
, lazyMatch :: Bool
lazyMatch = Bool
False
}
ConstructorInfo
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
cc :: CompiledClauses
cc@Done{} -> forall (m :: * -> *) a. Monad m => a -> m a
return CompiledClauses
cc
translateSplitTree :: SplitTree -> TCM SplitTree
translateSplitTree :: SplitTree -> TCM SplitTree
translateSplitTree = forall a b. (a, b) -> b
snd forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> SplitTree -> TCM ([Bool], SplitTree)
loop
where
loop :: SplitTree -> TCM ([Bool], SplitTree)
loop :: SplitTree -> TCM ([Bool], SplitTree)
loop = \case
SplittingDone Nat
n ->
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Nat -> a -> [a]
replicate Nat
n Bool
True, forall a. Nat -> SplitTree' a
SplittingDone Nat
n)
SplitAt Arg Nat
i LazySplit
lz SplitTrees' SplitTag
ts -> do
(Bool
x, [Bool]
xs, SplitTrees' SplitTag
ts) <- Nat
-> SplitTrees' SplitTag -> TCM (Bool, [Bool], SplitTrees' SplitTag)
loops (forall e. Arg e -> e
unArg Arg Nat
i) SplitTrees' SplitTag
ts
let t' :: SplitTree
t' = if Bool
x then
case SplitTrees' SplitTag
ts of
[(SplitTag
c,SplitTree
t)] -> SplitTree
t
SplitTrees' SplitTag
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
else forall a. Arg Nat -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Nat
i LazySplit
lz SplitTrees' SplitTag
ts
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool]
xs, SplitTree
t')
loops :: Int -> SplitTrees -> TCM (Bool, [Bool], SplitTrees)
loops :: Nat
-> SplitTrees' SplitTag -> TCM (Bool, [Bool], SplitTrees' SplitTag)
loops Nat
i SplitTrees' SplitTag
ts = do
([Bool]
rs, [[Bool]]
xss, SplitTrees' SplitTag
ts) <- forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM SplitTrees' SplitTag
ts forall a b. (a -> b) -> a -> b
$ \ (SplitTag
c, SplitTree
t) -> do
([Bool]
xs, SplitTree
t) <- SplitTree -> TCM ([Bool], SplitTree)
loop SplitTree
t
(Bool
isRC, Nat
n) <- SplitTag -> TCM (Bool, Nat)
getEtaAndArity SplitTag
c
let ([Bool]
xs0, [Bool]
rest) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
i [Bool]
xs
([Bool]
xs1, [Bool]
xs2) = forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
n [Bool]
rest
x :: Bool
x = Bool
isRC Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
xs1
xs' :: [Bool]
xs' = [Bool]
xs0 forall a. [a] -> [a] -> [a]
++ Bool
x forall a. a -> [a] -> [a]
: [Bool]
xs2
t' :: SplitTree
t' = if Bool
x then forall a. DropFrom a => Nat -> Nat -> a -> a
dropFrom Nat
i (Nat
n forall a. Num a => a -> a -> a
- Nat
1) SplitTree
t else SplitTree
t
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
x, [Bool]
xs', (SplitTag
c, SplitTree
t'))
let x :: Bool
x = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
rs
if Bool
x then forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Bool]
rs forall a. Eq a => a -> a -> Bool
== [Bool
True]) forall a. HasCallStack => a
__IMPOSSIBLE__
else forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
rs) forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
x, [[Bool]] -> [Bool]
conjColumns [[Bool]]
xss, SplitTrees' SplitTag
ts)
class DropFrom a where
dropFrom :: Int -> Int -> a -> a
instance DropFrom (SplitTree' c) where
dropFrom :: Nat -> Nat -> SplitTree' c -> SplitTree' c
dropFrom Nat
i Nat
n = \case
SplittingDone Nat
m -> forall a. Nat -> SplitTree' a
SplittingDone (Nat
m forall a. Num a => a -> a -> a
- Nat
n)
SplitAt x :: Arg Nat
x@(Arg ArgInfo
ai Nat
j) LazySplit
lz SplitTrees' c
ts
| Nat
j forall a. Ord a => a -> a -> Bool
>= Nat
i forall a. Num a => a -> a -> a
+ Nat
n -> forall a. Arg Nat -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Nat
j forall a. Num a => a -> a -> a
- Nat
n) LazySplit
lz forall a b. (a -> b) -> a -> b
$ forall a. DropFrom a => Nat -> Nat -> a -> a
dropFrom Nat
i Nat
n SplitTrees' c
ts
| Nat
j forall a. Ord a => a -> a -> Bool
< Nat
i -> forall a. Arg Nat -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Nat
x LazySplit
lz forall a b. (a -> b) -> a -> b
$ forall a. DropFrom a => Nat -> Nat -> a -> a
dropFrom Nat
i Nat
n SplitTrees' c
ts
| Bool
otherwise -> forall a. HasCallStack => a
__IMPOSSIBLE__
instance DropFrom (c, SplitTree' c) where
dropFrom :: Nat -> Nat -> (c, SplitTree' c) -> (c, SplitTree' c)
dropFrom Nat
i Nat
n (c
c, SplitTree' c
t) = (c
c, forall a. DropFrom a => Nat -> Nat -> a -> a
dropFrom Nat
i Nat
n SplitTree' c
t)
instance DropFrom a => DropFrom [a] where
dropFrom :: Nat -> Nat -> [a] -> [a]
dropFrom Nat
i Nat
n [a]
ts = forall a b. (a -> b) -> [a] -> [b]
map (forall a. DropFrom a => Nat -> Nat -> a -> a
dropFrom Nat
i Nat
n) [a]
ts
translateRecordPatterns :: Clause -> TCM Clause
translateRecordPatterns :: Clause -> TCM Clause
translateRecordPatterns Clause
clause = do
([NamedArg Pattern]
ps, [Term]
s, Changes
cs) <- forall a. RecPatM a -> TCM a
runRecPatM forall a b. (a -> b) -> a -> b
$ [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
translatePatterns forall a b. (a -> b) -> a -> b
$ forall a b. LabelPatVars a b => b -> a
unnumberPatVars forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
clause
let
noNewPatternVars :: Nat
noNewPatternVars = forall a. Sized a => a -> Nat
size Changes
cs
s' :: [Term]
s' = forall a. [a] -> [a]
reverse [Term]
s
mkSub :: [Term] -> Substitution' Term
mkSub [Term]
s = [Term]
s forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Nat -> Substitution' a
raiseS Nat
noNewPatternVars
rhsSubst :: Substitution' Term
rhsSubst = [Term] -> Substitution' Term
mkSub [Term]
s'
perm :: Permutation
perm = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Permutation
clausePerm Clause
clause
rhsSubst' :: Substitution' Term
rhsSubst' = [Term] -> Substitution' Term
mkSub forall a b. (a -> b) -> a -> b
$ forall a. Permutation -> [a] -> [a]
permute (Permutation -> Permutation
reverseP Permutation
perm) [Term]
s'
flattenedOldTel :: [(PatVarName, Dom Type)]
flattenedOldTel =
forall a. Permutation -> [a] -> [a]
permute (Nat -> Permutation -> Permutation
invertP forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
compactP Permutation
perm) forall a b. (a -> b) -> a -> b
$
forall a b. [a] -> [b] -> [(a, b)]
zip (Telescope -> [PatVarName]
teleNames forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
clause) forall a b. (a -> b) -> a -> b
$
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel forall a b. (a -> b) -> a -> b
$
Clause -> Telescope
clauseTel Clause
clause
substTel :: Substitution' (SubstArg (Dom Type))
-> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
substTel = forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst
newTel' :: [Maybe (PatVarName, Dom Type)]
newTel' =
forall {d}.
Substitution' (SubstArg (Dom Type))
-> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
substTel Substitution' Term
rhsSubst' forall a b. (a -> b) -> a -> b
$
Changes
-> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
translateTel Changes
cs forall a b. (a -> b) -> a -> b
$
[(PatVarName, Dom Type)]
flattenedOldTel
newPerm :: Permutation
newPerm = Permutation -> Permutation
adjustForDotPatterns forall a b. (a -> b) -> a -> b
$
[Dom Type] -> Permutation
reorderTel_ forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall b a. b -> (a -> b) -> Maybe a -> b
maybe HasCallStack => Dom Type
__DUMMY_DOM__ forall a b. (a, b) -> b
snd) [Maybe (PatVarName, Dom Type)]
newTel'
where
isDotP :: Nat -> Bool
isDotP Nat
n = case forall i a. Integral i => [a] -> i -> a
List.genericIndex Changes
cs Nat
n of
Left DotP{} -> Bool
True
Either Pattern (Kind -> Nat, PatVarName, Dom Type)
_ -> Bool
False
adjustForDotPatterns :: Permutation -> Permutation
adjustForDotPatterns (Perm Nat
n [Nat]
is) =
Nat -> [Nat] -> Permutation
Perm Nat
n (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Bool
isDotP) [Nat]
is)
lhsSubst' :: Substitution' Term
lhsSubst' = forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
newPerm)
lhsSubst :: Substitution' Term
lhsSubst = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
lhsSubst' Substitution' Term
rhsSubst'
newTel :: Telescope
newTel =
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [PatVarName] -> [Dom Type] -> Telescope
unflattenTel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__) forall a b. (a -> b) -> a -> b
$
forall a. Permutation -> [a] -> [a]
permute Permutation
newPerm forall a b. (a -> b) -> a -> b
$
forall {d}.
Substitution' (SubstArg (Dom Type))
-> [Maybe (d, Dom Type)] -> [Maybe (d, Dom Type)]
substTel Substitution' Term
lhsSubst' forall a b. (a -> b) -> a -> b
$
[Maybe (PatVarName, Dom Type)]
newTel'
c :: Clause
c = Clause
clause
{ clauseTel :: Telescope
clauseTel = Telescope
newTel
, namedClausePats :: NAPs
namedClausePats = forall a b.
(LabelPatVars a b, PatVarLabel b ~ Nat) =>
Nat -> Permutation -> a -> b
numberPatVars forall a. HasCallStack => a
__IMPOSSIBLE__ Permutation
newPerm forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
lhsSubst [NamedArg Pattern]
ps
, clauseBody :: Maybe Term
clauseBody = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
lhsSubst forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
clause
}
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.lhs.recpat" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"Original clause:"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"delta =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Clause -> Telescope
clauseTel Clause
clause)
, TCMT IO Doc
"pats =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text (forall a. Show a => a -> PatVarName
show forall a b. (a -> b) -> a -> b
$ Clause -> [Arg DeBruijnPattern]
clausePats Clause
clause)
]
, TCMT IO Doc
"Intermediate results:"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"ps =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text (forall a. Show a => a -> PatVarName
show [NamedArg Pattern]
ps)
, TCMT IO Doc
"s =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
s
, TCMT IO Doc
"cs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Changes
cs
, TCMT IO Doc
"flattenedOldTel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> PatVarName
show) [(PatVarName, Dom Type)]
flattenedOldTel
, TCMT IO Doc
"newTel' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> PatVarName
show) [Maybe (PatVarName, Dom Type)]
newTel'
, TCMT IO Doc
"newPerm =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Permutation
newPerm
]
]
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.lhs.recpat" Nat
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"lhsSubst' =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> PatVarName
show) Substitution' Term
lhsSubst'
, TCMT IO Doc
"lhsSubst =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> PatVarName
show) Substitution' Term
lhsSubst
, TCMT IO Doc
"newTel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
newTel
]
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.lhs.recpat" Nat
10 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Nat -> m a -> m a
escapeContext HasCallStack => Impossible
impossible (forall a. Sized a => a -> Nat
size forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
clause) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"Translated clause:"
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"delta =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Clause -> Telescope
clauseTel Clause
c)
, TCMT IO Doc
"ps =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text (forall a. Show a => a -> PatVarName
show forall a b. (a -> b) -> a -> b
$ Clause -> [Arg DeBruijnPattern]
clausePats Clause
c)
, TCMT IO Doc
"body =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text (forall a. Show a => a -> PatVarName
show forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
c)
, TCMT IO Doc
"body =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
c) (forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Doc
"_|_" forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Clause -> Maybe Term
clauseBody Clause
c))
]
]
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c
newtype RecPatM a = RecPatM (TCMT (ReaderT Nat (StateT Nat IO)) a)
deriving (forall a b. a -> RecPatM b -> RecPatM a
forall a b. (a -> b) -> RecPatM a -> RecPatM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> RecPatM b -> RecPatM a
$c<$ :: forall a b. a -> RecPatM b -> RecPatM a
fmap :: forall a b. (a -> b) -> RecPatM a -> RecPatM b
$cfmap :: forall a b. (a -> b) -> RecPatM a -> RecPatM b
Functor, Functor RecPatM
forall a. a -> RecPatM a
forall a b. RecPatM a -> RecPatM b -> RecPatM a
forall a b. RecPatM a -> RecPatM b -> RecPatM b
forall a b. RecPatM (a -> b) -> RecPatM a -> RecPatM b
forall a b c. (a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. RecPatM a -> RecPatM b -> RecPatM a
$c<* :: forall a b. RecPatM a -> RecPatM b -> RecPatM a
*> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
$c*> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
liftA2 :: forall a b c. (a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c
$cliftA2 :: forall a b c. (a -> b -> c) -> RecPatM a -> RecPatM b -> RecPatM c
<*> :: forall a b. RecPatM (a -> b) -> RecPatM a -> RecPatM b
$c<*> :: forall a b. RecPatM (a -> b) -> RecPatM a -> RecPatM b
pure :: forall a. a -> RecPatM a
$cpure :: forall a. a -> RecPatM a
Applicative, Applicative RecPatM
forall a. a -> RecPatM a
forall a b. RecPatM a -> RecPatM b -> RecPatM b
forall a b. RecPatM a -> (a -> RecPatM b) -> RecPatM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> RecPatM a
$creturn :: forall a. a -> RecPatM a
>> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
$c>> :: forall a b. RecPatM a -> RecPatM b -> RecPatM b
>>= :: forall a b. RecPatM a -> (a -> RecPatM b) -> RecPatM b
$c>>= :: forall a b. RecPatM a -> (a -> RecPatM b) -> RecPatM b
Monad,
Monad RecPatM
forall a. IO a -> RecPatM a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> RecPatM a
$cliftIO :: forall a. IO a -> RecPatM a
MonadIO, Applicative RecPatM
MonadIO RecPatM
HasOptions RecPatM
MonadTCState RecPatM
MonadTCEnv RecPatM
forall a. TCM a -> RecPatM a
forall (tcm :: * -> *).
Applicative tcm
-> MonadIO tcm
-> MonadTCEnv tcm
-> MonadTCState tcm
-> HasOptions tcm
-> (forall a. TCM a -> tcm a)
-> MonadTCM tcm
liftTCM :: forall a. TCM a -> RecPatM a
$cliftTCM :: forall a. TCM a -> RecPatM a
MonadTCM, Monad RecPatM
Functor RecPatM
Applicative RecPatM
RecPatM PragmaOptions
RecPatM CommandLineOptions
forall (m :: * -> *).
Functor m
-> Applicative m
-> Monad m
-> m PragmaOptions
-> m CommandLineOptions
-> HasOptions m
commandLineOptions :: RecPatM CommandLineOptions
$ccommandLineOptions :: RecPatM CommandLineOptions
pragmaOptions :: RecPatM PragmaOptions
$cpragmaOptions :: RecPatM PragmaOptions
HasOptions,
Monad RecPatM
RecPatM TCEnv
forall a. (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a
forall (m :: * -> *).
Monad m
-> m TCEnv
-> (forall a. (TCEnv -> TCEnv) -> m a -> m a)
-> MonadTCEnv m
localTC :: forall a. (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a
$clocalTC :: forall a. (TCEnv -> TCEnv) -> RecPatM a -> RecPatM a
askTC :: RecPatM TCEnv
$caskTC :: RecPatM TCEnv
MonadTCEnv, Monad RecPatM
RecPatM TCState
TCState -> RecPatM ()
(TCState -> TCState) -> RecPatM ()
forall (m :: * -> *).
Monad m
-> m TCState
-> (TCState -> m ())
-> ((TCState -> TCState) -> m ())
-> MonadTCState m
modifyTC :: (TCState -> TCState) -> RecPatM ()
$cmodifyTC :: (TCState -> TCState) -> RecPatM ()
putTC :: TCState -> RecPatM ()
$cputTC :: TCState -> RecPatM ()
getTC :: RecPatM TCState
$cgetTC :: RecPatM TCState
MonadTCState)
runRecPatM :: RecPatM a -> TCM a
runRecPatM :: forall a. RecPatM a -> TCM a
runRecPatM (RecPatM TCMT (ReaderT Nat (StateT Nat IO)) a
m) =
forall (m :: * -> *) (n :: * -> *) a.
(forall a1. m a1 -> n a1) -> TCMT m a -> TCMT n a
mapTCMT (\ReaderT Nat (StateT Nat IO) a1
m -> do
(a1
x, Nat
noVars) <- forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix forall a b. (a -> b) -> a -> b
$ \ ~(a1
_, Nat
noVars) ->
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Nat (StateT Nat IO) a1
m Nat
noVars) Nat
0
forall (m :: * -> *) a. Monad m => a -> m a
return a1
x)
TCMT (ReaderT Nat (StateT Nat IO)) a
m
nextVar :: RecPatM (Pattern, Term)
nextVar :: RecPatM (Pattern, Term)
nextVar = forall a. TCMT (ReaderT Nat (StateT Nat IO)) a -> RecPatM a
RecPatM forall a b. (a -> b) -> a -> b
$ do
Nat
n <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall s (m :: * -> *). MonadState s m => m s
get
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
succ Nat
n
Nat
noVars <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall r (m :: * -> *). MonadReader r m => m r
ask
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Pattern' a
varP PatVarName
"r", Nat -> Term
var forall a b. (a -> b) -> a -> b
$ Nat
noVars forall a. Num a => a -> a -> a
- Nat
n forall a. Num a => a -> a -> a
- Nat
1)
data Kind = VarPat | DotPat
deriving Kind -> Kind -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Kind -> Kind -> Bool
$c/= :: Kind -> Kind -> Bool
== :: Kind -> Kind -> Bool
$c== :: Kind -> Kind -> Bool
Eq
type Change = Either Pattern (Kind -> Nat, ArgName, Dom Type)
type Changes = [Change]
instance Pretty (Kind -> Nat) where
pretty :: (Kind -> Nat) -> Doc
pretty Kind -> Nat
f =
(Doc
"(VarPat:" forall a. Doc a -> Doc a -> Doc a
P.<+> forall a. PatVarName -> Doc a
P.text (forall a. Show a => a -> PatVarName
show forall a b. (a -> b) -> a -> b
$ Kind -> Nat
f Kind
VarPat) forall a. Doc a -> Doc a -> Doc a
P.<+>
Doc
"DotPat:" forall a. Doc a -> Doc a -> Doc a
P.<+> forall a. PatVarName -> Doc a
P.text (forall a. Show a => a -> PatVarName
show forall a b. (a -> b) -> a -> b
$ Kind -> Nat
f Kind
DotPat)) forall a. Semigroup a => a -> a -> a
<> Doc
")"
instance PrettyTCM (Kind -> Nat) where
prettyTCM :: forall (m :: * -> *). MonadPretty m => (Kind -> Nat) -> m Doc
prettyTCM = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty
instance PrettyTCM Change where
prettyTCM :: forall (m :: * -> *).
MonadPretty m =>
Either Pattern (Kind -> Nat, PatVarName, Dom Type) -> m Doc
prettyTCM (Left Pattern
p) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Pattern
p
prettyTCM (Right (Kind -> Nat
f, PatVarName
x, Dom Type
t)) = m Doc
"Change" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Kind -> Nat
f forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => PatVarName -> m Doc
text PatVarName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom Type
t
data RecordTree
= Leaf Pattern
| RecCon (Arg Type) [(Term -> Term, RecordTree)]
projections :: RecordTree -> [(Term -> Term, Kind)]
projections :: RecordTree -> [(Term -> Term, Kind)]
projections (Leaf (DotP{})) = [(forall a. a -> a
id, Kind
DotPat)]
projections (Leaf (VarP{})) = [(forall a. a -> a
id, Kind
VarPat)]
projections (Leaf Pattern
_) = forall a. HasCallStack => a
__IMPOSSIBLE__
projections (RecCon Arg Type
_ [(Term -> Term, RecordTree)]
args) =
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Term -> Term
p, RecordTree
t) -> forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
p)) forall a b. (a -> b) -> a -> b
$ RecordTree -> [(Term -> Term, Kind)]
projections RecordTree
t)
[(Term -> Term, RecordTree)]
args
removeTree :: RecordTree -> RecPatM (Pattern, [Term], Changes)
removeTree :: RecordTree -> RecPatM (Pattern, [Term], Changes)
removeTree RecordTree
tree = do
(Pattern
pat, Term
x) <- RecPatM (Pattern, Term)
nextVar
let ps :: [(Term -> Term, Kind)]
ps = RecordTree -> [(Term -> Term, Kind)]
projections RecordTree
tree
s :: [Term]
s = forall a b. (a -> b) -> [a] -> [b]
map (\(Term -> Term
p, Kind
_) -> Term -> Term
p Term
x) [(Term -> Term, Kind)]
ps
count :: Kind -> Nat
count Kind
k = forall (t :: * -> *) a. Foldable t => t a -> Nat
length forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
== Kind
k) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Term -> Term, Kind)]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case RecordTree
tree of
Leaf Pattern
p -> (Pattern
p, [Term]
s, [forall a b. a -> Either a b
Left Pattern
p])
RecCon Arg Type
t [(Term -> Term, RecordTree)]
_ -> (Pattern
pat, [Term]
s, [forall a b. b -> Either a b
Right (Kind -> Nat
count, PatVarName
"r", forall a. Arg a -> Dom a
domFromArg Arg Type
t)])
translatePattern :: Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern :: Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern 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
Either (RecPatM (Pattern, [Term], Changes)) RecordTree
r <- Pattern
-> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
recordTree Pattern
p
case Either (RecPatM (Pattern, [Term], Changes)) RecordTree
r of
Left RecPatM (Pattern, [Term], Changes)
r -> RecPatM (Pattern, [Term], Changes)
r
Right RecordTree
t -> RecordTree -> RecPatM (Pattern, [Term], Changes)
removeTree RecordTree
t
| Bool
otherwise = do
([NamedArg Pattern]
ps, [Term]
s, Changes
cs) <- [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
translatePatterns [NamedArg Pattern]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return (forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci [NamedArg Pattern]
ps, [Term]
s, Changes
cs)
translatePattern p :: Pattern
p@(DefP PatternInfo
o QName
q [NamedArg Pattern]
ps) = do
([NamedArg Pattern]
ps, [Term]
s, Changes
cs) <- [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
translatePatterns [NamedArg Pattern]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return (forall x.
PatternInfo -> QName -> [NamedArg (Pattern' x)] -> Pattern' x
DefP PatternInfo
o QName
q [NamedArg Pattern]
ps, [Term]
s, Changes
cs)
translatePattern p :: Pattern
p@VarP{} = RecordTree -> RecPatM (Pattern, [Term], Changes)
removeTree (Pattern -> RecordTree
Leaf Pattern
p)
translatePattern p :: Pattern
p@DotP{} = RecordTree -> RecPatM (Pattern, [Term], Changes)
removeTree (Pattern -> RecordTree
Leaf Pattern
p)
translatePattern p :: Pattern
p@LitP{} = forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
p, [], [])
translatePattern p :: Pattern
p@ProjP{}= forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
p, [], [])
translatePattern p :: Pattern
p@IApplyP{}= forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
p, [], [])
translatePatterns :: [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
translatePatterns :: [NamedArg Pattern] -> RecPatM ([NamedArg Pattern], [Term], Changes)
translatePatterns [NamedArg Pattern]
ps = do
([Pattern]
ps', [[Term]]
ss, [Changes]
cs) <- forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg Pattern]
ps
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Pattern
p -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Pattern
p forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$)) [Pattern]
ps' [NamedArg Pattern]
ps, forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Term]]
ss, forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Changes]
cs)
recordTree ::
Pattern ->
RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
recordTree :: Pattern
-> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
recordTree p :: Pattern
p@(ConP ConHead
c ConPatternInfo
ci [NamedArg Pattern]
ps) | ConPatternInfo -> Bool
conPRecord ConPatternInfo
ci , PatOrigin
PatOSystem <- PatternInfo -> PatOrigin
patOrigin (ConPatternInfo -> PatternInfo
conPInfo ConPatternInfo
ci) = do
let t :: Arg Type
t = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ ConPatternInfo -> Maybe (Arg Type)
conPType ConPatternInfo
ci
[Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
rs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Pattern
-> RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
recordTree forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg Pattern]
ps
case forall a b. [Either a b] -> Maybe [b]
allRight [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
rs of
Maybe [RecordTree]
Nothing ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ do
([Pattern]
ps', [[Term]]
ss, [Changes]
cs) <- forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id RecordTree -> RecPatM (Pattern, [Term], Changes)
removeTree) [Either (RecPatM (Pattern, [Term], Changes)) RecordTree]
rs
forall (m :: * -> *) a. Monad m => a -> m a
return (forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
ci ([Pattern]
ps' forall a b. [a] -> [NamedArg b] -> [NamedArg a]
`withNamedArgsFrom` [NamedArg Pattern]
ps),
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Term]]
ss, forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Changes]
cs)
Just [RecordTree]
ts -> forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
Arg Type
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Arg Type
t
forall (m :: * -> *).
MonadDebug m =>
PatVarName -> Nat -> TCMT IO Doc -> m ()
reportSDoc PatVarName
"tc.rec" Nat
45 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"recordTree: "
, forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"constructor pattern " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Pattern
p forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" has type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Arg Type
t
]
[Dom QName]
fields <- Type -> TCM [Dom QName]
getRecordTypeFields forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall e. Arg e -> e
unArg Arg Type
t)
let proj :: Dom' t QName -> t -> t
proj Dom' t QName
p = (forall t. Apply t => t -> Elims -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom Dom' t QName
p])
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ Arg Type -> [(Term -> Term, RecordTree)] -> RecordTree
RecCon Arg Type
t forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall {t} {t}. Apply t => Dom' t QName -> t -> t
proj [Dom QName]
fields) [RecordTree]
ts
recordTree p :: Pattern
p@(ConP ConHead
_ ConPatternInfo
ci [NamedArg Pattern]
_) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern Pattern
p
recordTree p :: Pattern
p@DefP{} = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern Pattern
p
recordTree p :: Pattern
p@VarP{} = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Pattern -> RecordTree
Leaf Pattern
p))
recordTree p :: Pattern
p@DotP{} = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Pattern -> RecordTree
Leaf Pattern
p))
recordTree p :: Pattern
p@LitP{} = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern Pattern
p
recordTree p :: Pattern
p@ProjP{}= forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern Pattern
p
recordTree p :: Pattern
p@IApplyP{}= forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Pattern -> RecPatM (Pattern, [Term], Changes)
translatePattern Pattern
p
translateTel
:: Changes
-> [(ArgName, Dom Type)]
-> [Maybe (ArgName, Dom Type)]
translateTel :: Changes
-> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
translateTel (Left (DotP{}) : Changes
rest) [(PatVarName, Dom Type)]
tel = forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: Changes
-> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
translateTel Changes
rest [(PatVarName, Dom Type)]
tel
translateTel (Right (Kind -> Nat
n, PatVarName
x, Dom Type
t) : Changes
rest) [(PatVarName, Dom Type)]
tel = forall a. a -> Maybe a
Just (PatVarName
x, Dom Type
t) forall a. a -> [a] -> [a]
:
Changes
-> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
translateTel Changes
rest
(forall a. Nat -> [a] -> [a]
drop (Kind -> Nat
n Kind
VarPat) [(PatVarName, Dom Type)]
tel)
translateTel (Left Pattern
_ : Changes
rest) ((PatVarName, Dom Type)
t : [(PatVarName, Dom Type)]
tel) = forall a. a -> Maybe a
Just (PatVarName, Dom Type)
t forall a. a -> [a] -> [a]
: Changes
-> [(PatVarName, Dom Type)] -> [Maybe (PatVarName, Dom Type)]
translateTel Changes
rest [(PatVarName, Dom Type)]
tel
translateTel [] [] = []
translateTel (Left Pattern
_ : Changes
_) [] = forall a. HasCallStack => a
__IMPOSSIBLE__
translateTel [] ((PatVarName, Dom Type)
_ : [(PatVarName, Dom Type)]
_) = forall a. HasCallStack => a
__IMPOSSIBLE__