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