{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.LHS.Unify
( UnificationResult
, UnificationResult'(..)
, unifyIndices ) where
import Prelude hiding (null)
import Control.Monad
import Control.Monad.State
import Control.Monad.Writer (WriterT(..), MonadWriter(..))
import Control.Monad.Except
import Data.Semigroup hiding (Arg)
import qualified Data.List as List
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Data.IntMap (IntMap)
import qualified Agda.Benchmarking as Bench
import Agda.Interaction.Options (optInjectiveTypeConstructors)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Conversion.Pure
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Reduce
import qualified Agda.TypeChecking.Patterns.Match as Match
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Free
import Agda.TypeChecking.Free.Precompute
import Agda.TypeChecking.Free.Reduce
import Agda.TypeChecking.Records
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.Utils.Benchmark
import Agda.Utils.Either
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.PartialOrd
import Agda.Utils.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
type UnificationResult = UnificationResult'
( Telescope
, PatternSubstitution
, [NamedArg DeBruijnPattern]
)
data UnificationResult' a
= Unifies a
| NoUnify NegativeUnification
| UnifyBlocked Blocker
| UnifyStuck [UnificationFailure]
deriving (Int -> UnificationResult' a -> ShowS
forall a. Show a => Int -> UnificationResult' a -> ShowS
forall a. Show a => [UnificationResult' a] -> ShowS
forall a. Show a => UnificationResult' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnificationResult' a] -> ShowS
$cshowList :: forall a. Show a => [UnificationResult' a] -> ShowS
show :: UnificationResult' a -> String
$cshow :: forall a. Show a => UnificationResult' a -> String
showsPrec :: Int -> UnificationResult' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> UnificationResult' a -> ShowS
Show, forall a b. a -> UnificationResult' b -> UnificationResult' a
forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' 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 -> UnificationResult' b -> UnificationResult' a
$c<$ :: forall a b. a -> UnificationResult' b -> UnificationResult' a
fmap :: forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
$cfmap :: forall a b.
(a -> b) -> UnificationResult' a -> UnificationResult' b
Functor, forall a. Eq a => a -> UnificationResult' a -> Bool
forall a. Num a => UnificationResult' a -> a
forall a. Ord a => UnificationResult' a -> a
forall m. Monoid m => UnificationResult' m -> m
forall a. UnificationResult' a -> Bool
forall a. UnificationResult' a -> Int
forall a. UnificationResult' a -> [a]
forall a. (a -> a -> a) -> UnificationResult' a -> a
forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => UnificationResult' a -> a
$cproduct :: forall a. Num a => UnificationResult' a -> a
sum :: forall a. Num a => UnificationResult' a -> a
$csum :: forall a. Num a => UnificationResult' a -> a
minimum :: forall a. Ord a => UnificationResult' a -> a
$cminimum :: forall a. Ord a => UnificationResult' a -> a
maximum :: forall a. Ord a => UnificationResult' a -> a
$cmaximum :: forall a. Ord a => UnificationResult' a -> a
elem :: forall a. Eq a => a -> UnificationResult' a -> Bool
$celem :: forall a. Eq a => a -> UnificationResult' a -> Bool
length :: forall a. UnificationResult' a -> Int
$clength :: forall a. UnificationResult' a -> Int
null :: forall a. UnificationResult' a -> Bool
$cnull :: forall a. UnificationResult' a -> Bool
toList :: forall a. UnificationResult' a -> [a]
$ctoList :: forall a. UnificationResult' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
foldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> UnificationResult' a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> UnificationResult' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> UnificationResult' a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> UnificationResult' a -> m
fold :: forall m. Monoid m => UnificationResult' m -> m
$cfold :: forall m. Monoid m => UnificationResult' m -> m
Foldable, Functor UnificationResult'
Foldable UnificationResult'
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
sequence :: forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
UnificationResult' (m a) -> m (UnificationResult' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnificationResult' a -> m (UnificationResult' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnificationResult' (f a) -> f (UnificationResult' a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnificationResult' a -> f (UnificationResult' b)
Traversable)
unifyIndices
:: (PureTCM m, MonadBench m, BenchPhase m ~ Bench.Phase)
=> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m UnificationResult
unifyIndices :: forall (m :: * -> *).
(PureTCM m, MonadBench m, BenchPhase m ~ Phase) =>
Telescope
-> FlexibleVars
-> Type
-> [Arg Term]
-> [Arg Term]
-> m UnificationResult
unifyIndices Telescope
tel FlexibleVars
flex Type
a [Arg Term]
us [Arg Term]
vs =
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [Phase
Bench.Typing, Phase
Bench.CheckLHS, Phase
Bench.UnifyIndices] forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
PureTCM m =>
Telescope
-> FlexibleVars
-> Type
-> [Arg Term]
-> [Arg Term]
-> m UnificationResult
unifyIndices' Telescope
tel FlexibleVars
flex Type
a [Arg Term]
us [Arg Term]
vs
unifyIndices'
:: (PureTCM m)
=> Telescope
-> FlexibleVars
-> Type
-> Args
-> Args
-> m UnificationResult
unifyIndices' :: forall (m :: * -> *).
PureTCM m =>
Telescope
-> FlexibleVars
-> Type
-> [Arg Term]
-> [Arg Term]
-> m UnificationResult
unifyIndices' Telescope
tel FlexibleVars
flex Type
a [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies (Telescope
tel, forall a. Substitution' a
idS, [])
unifyIndices' Telescope
tel FlexibleVars
flex Type
a [Arg Term]
us [Arg Term]
vs = do
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
10 forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"unifyIndices"
, (TCMT IO Doc
"tel =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
, (TCMT IO Doc
"flex =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. FlexibleVar a -> a
flexVar FlexibleVars
flex
, (TCMT IO Doc
"a =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a)
, (TCMT IO Doc
"us =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
us
, (TCMT IO Doc
"vs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs
]
UnifyState
initialState <- forall (m :: * -> *).
PureTCM m =>
Telescope
-> FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> m UnifyState
initUnifyState Telescope
tel FlexibleVars
flex Type
a [Arg Term]
us [Arg Term]
vs
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"initial unifyState:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyState
initialState
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
70 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"initial unifyState:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show UnifyState
initialState)
(UnificationResult' UnifyState
result,UnifyOutput
output) <- forall (m :: * -> *) a. UnifyLogT m a -> m (a, UnifyOutput)
runUnifyLogT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify UnifyState
initialState UnifyStrategy
rightToLeftStrategy
let ps :: [NamedArg (Pattern' DBPatVar)]
ps = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
output) forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs (UnifyState -> Telescope
eqTel UnifyState
initialState)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\UnifyState
s -> (UnifyState -> Telescope
varTel UnifyState
s , UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
output , [NamedArg (Pattern' DBPatVar)]
ps)) UnificationResult' UnifyState
result
data Equality = Equal
{ Equality -> Dom' Term Type
_eqType :: Dom Type
, Equality -> Term
_eqLeft :: Term
, Equality -> Term
_eqRight :: Term
}
instance Reduce Equality where
reduce' :: Equality -> ReduceM Equality
reduce' (Equal Dom' Term Type
a Term
u Term
v) = Dom' Term Type -> Term -> Term -> Equality
Equal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Reduce t => t -> ReduceM t
reduce' Dom' Term Type
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall t. Reduce t => t -> ReduceM t
reduce' Term
v
eqConstructorForm :: HasBuiltins m => Equality -> m Equality
eqConstructorForm :: forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqConstructorForm (Equal Dom' Term Type
a Term
u Term
v) = Dom' Term Type -> Term -> Term -> Equality
Equal Dom' Term Type
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v
eqUnLevel :: HasBuiltins m => Equality -> m Equality
eqUnLevel :: forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel (Equal Dom' Term Type
a Term
u Term
v) = Dom' Term Type -> Term -> Term -> Equality
Equal Dom' Term Type
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
v
where
unLevel :: Term -> m Term
unLevel (Level Level
l) = forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l
unLevel Term
u = forall (m :: * -> *) a. Monad m => a -> m a
return Term
u
data UnifyState = UState
{ UnifyState -> Telescope
varTel :: Telescope
, UnifyState -> FlexibleVars
flexVars :: FlexibleVars
, UnifyState -> Telescope
eqTel :: Telescope
, UnifyState -> [Arg Term]
eqLHS :: [Arg Term]
, UnifyState -> [Arg Term]
eqRHS :: [Arg Term]
} deriving (Int -> UnifyState -> ShowS
[UnifyState] -> ShowS
UnifyState -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnifyState] -> ShowS
$cshowList :: [UnifyState] -> ShowS
show :: UnifyState -> String
$cshow :: UnifyState -> String
showsPrec :: Int -> UnifyState -> ShowS
$cshowsPrec :: Int -> UnifyState -> ShowS
Show)
lensVarTel :: Lens' Telescope UnifyState
lensVarTel :: Lens' Telescope UnifyState
lensVarTel Telescope -> f Telescope
f UnifyState
s = Telescope -> f Telescope
f (UnifyState -> Telescope
varTel UnifyState
s) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Telescope
tel -> UnifyState
s { varTel :: Telescope
varTel = Telescope
tel }
lensEqTel :: Lens' Telescope UnifyState
lensEqTel :: Lens' Telescope UnifyState
lensEqTel Telescope -> f Telescope
f UnifyState
s = Telescope -> f Telescope
f (UnifyState -> Telescope
eqTel UnifyState
s) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Telescope
x -> UnifyState
s { eqTel :: Telescope
eqTel = Telescope
x }
instance Reduce UnifyState where
reduce' :: UnifyState -> ReduceM UnifyState
reduce' = forall a. HasCallStack => a
__IMPOSSIBLE__
instance PrettyTCM UnifyState where
prettyTCM :: forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
prettyTCM UnifyState
state = m Doc
"UnifyState" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"variable tel: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
gamma
, m Doc
"flexible vars: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
pshow (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. FlexibleVar a -> (a, IsForced)
flexVarF forall a b. (a -> b) -> a -> b
$ UnifyState -> FlexibleVars
flexVars UnifyState
state)
, m Doc
"equation tel: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta)
, m Doc
"equations: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
gamma (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {m :: * -> *} {a} {a}.
(PureTCM m, MonadInteractionPoints m, MonadFresh NameId m,
MonadStConcreteNames m, IsString (m Doc), Null (m Doc),
Semigroup (m Doc), PrettyTCM a, PrettyTCM a) =>
a -> a -> m Doc
prettyEquality (UnifyState -> [Arg Term]
eqLHS UnifyState
state) (UnifyState -> [Arg Term]
eqRHS UnifyState
state)))
])
where
flexVarF :: FlexibleVar a -> (a, IsForced)
flexVarF FlexibleVar a
fi = (forall a. FlexibleVar a -> a
flexVar FlexibleVar a
fi, forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar a
fi)
gamma :: Telescope
gamma = UnifyState -> Telescope
varTel UnifyState
state
delta :: Telescope
delta = UnifyState -> Telescope
eqTel UnifyState
state
prettyEquality :: a -> a -> m Doc
prettyEquality a
x a
y = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=?=" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
y
initUnifyState
:: PureTCM m
=> Telescope -> FlexibleVars -> Type -> Args -> Args -> m UnifyState
initUnifyState :: forall (m :: * -> *).
PureTCM m =>
Telescope
-> FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> m UnifyState
initUnifyState Telescope
tel FlexibleVars
flex Type
a [Arg Term]
lhs [Arg Term]
rhs = do
(Telescope
tel, Type
a, [Arg Term]
lhs, [Arg Term]
rhs) <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Telescope
tel, Type
a, [Arg Term]
lhs, [Arg Term]
rhs)
let n :: Int
n = forall a. Sized a => a -> Int
size [Arg Term]
lhs
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size [Arg Term]
rhs) forall a. HasCallStack => a
__IMPOSSIBLE__
TelV Telescope
eqTel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size Telescope
eqTel) forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Telescope
-> FlexibleVars
-> Telescope
-> [Arg Term]
-> [Arg Term]
-> UnifyState
UState Telescope
tel FlexibleVars
flex Telescope
eqTel [Arg Term]
lhs [Arg Term]
rhs
isUnifyStateSolved :: UnifyState -> Bool
isUnifyStateSolved :: UnifyState -> Bool
isUnifyStateSolved = forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Telescope
eqTel
varCount :: UnifyState -> Int
varCount :: UnifyState -> Int
varCount = forall a. Sized a => a -> Int
size forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Telescope
varTel
getVarType :: Int -> UnifyState -> Dom Type
getVarType :: Int -> UnifyState -> Dom' Term Type
getVarType Int
i UnifyState
s = forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
varTel UnifyState
s) Int
i
getVarTypeUnraised :: Int -> UnifyState -> Dom Type
getVarTypeUnraised :: Int -> UnifyState -> Dom' Term Type
getVarTypeUnraised Int
i UnifyState
s = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
varTel UnifyState
s) Int
i
eqCount :: UnifyState -> Int
eqCount :: UnifyState -> Int
eqCount = forall a. Sized a => a -> Int
size forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Telescope
eqTel
getEquality :: Int -> UnifyState -> Equality
getEquality :: Int -> UnifyState -> Equality
getEquality Int
k UState { eqTel :: UnifyState -> Telescope
eqTel = Telescope
eqs, eqLHS :: UnifyState -> [Arg Term]
eqLHS = [Arg Term]
lhs, eqRHS :: UnifyState -> [Arg Term]
eqRHS = [Arg Term]
rhs } =
Dom' Term Type -> Term -> Term -> Equality
Equal (forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
eqs) Int
k)
(forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Int
k)
(forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
rhs Int
k)
getEqualityUnraised :: Int -> UnifyState -> Equality
getEqualityUnraised :: Int -> UnifyState -> Equality
getEqualityUnraised Int
k UState { eqTel :: UnifyState -> Telescope
eqTel = Telescope
eqs, eqLHS :: UnifyState -> [Arg Term]
eqLHS = [Arg Term]
lhs, eqRHS :: UnifyState -> [Arg Term]
eqRHS = [Arg Term]
rhs } =
Dom' Term Type -> Term -> Term -> Equality
Equal (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
eqs) Int
k)
(forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Int
k)
(forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
rhs Int
k)
solveVar :: Int
-> DeBruijnPattern
-> UnifyState -> Maybe (UnifyState, PatternSubstitution)
solveVar :: Int
-> Pattern' DBPatVar
-> UnifyState
-> Maybe (UnifyState, PatternSubstitution)
solveVar Int
k Pattern' DBPatVar
u UnifyState
s = case Telescope
-> Int
-> Pattern' DBPatVar
-> Maybe (Telescope, PatternSubstitution, Permutation)
instantiateTelescope (UnifyState -> Telescope
varTel UnifyState
s) Int
k Pattern' DBPatVar
u of
Maybe (Telescope, PatternSubstitution, Permutation)
Nothing -> forall a. Maybe a
Nothing
Just (Telescope
tel' , PatternSubstitution
sigma , Permutation
rho) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (,PatternSubstitution
sigma) forall a b. (a -> b) -> a -> b
$ UState
{ varTel :: Telescope
varTel = Telescope
tel'
, flexVars :: FlexibleVars
flexVars = Permutation -> FlexibleVars -> FlexibleVars
permuteFlex (Permutation -> Permutation
reverseP Permutation
rho) forall a b. (a -> b) -> a -> b
$ UnifyState -> FlexibleVars
flexVars UnifyState
s
, eqTel :: Telescope
eqTel = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
, eqLHS :: [Arg Term]
eqLHS = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
, eqRHS :: [Arg Term]
eqRHS = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
}
where
permuteFlex :: Permutation -> FlexibleVars -> FlexibleVars
permuteFlex :: Permutation -> FlexibleVars -> FlexibleVars
permuteFlex Permutation
perm =
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a b. (a -> b) -> a -> b
$ \(FlexibleVar ArgInfo
ai IsForced
fc FlexibleVarKind
k Maybe Int
p Int
x) ->
forall a.
ArgInfo
-> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
FlexibleVar ArgInfo
ai IsForced
fc FlexibleVarKind
k Maybe Int
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
x (Permutation -> [Int]
permPicks Permutation
perm)
applyUnder :: Int -> Telescope -> Term -> Telescope
applyUnder :: Int -> Telescope -> Term -> Telescope
applyUnder Int
k Telescope
tel Term
u
| Int
k forall a. Ord a => a -> a -> Bool
< Int
0 = forall a. HasCallStack => a
__IMPOSSIBLE__
| Int
k forall a. Eq a => a -> a -> Bool
== Int
0 = Telescope
tel forall t. Apply t => t -> Term -> t
`apply1` Term
u
| Bool
otherwise = case Telescope
tel of
Telescope
EmptyTel -> forall a. HasCallStack => a
__IMPOSSIBLE__
ExtendTel Dom' Term Type
a Abs Telescope
tel' -> forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
a forall a b. (a -> b) -> a -> b
$
forall a. String -> a -> Abs a
Abs (forall a. Abs a -> String
absName Abs Telescope
tel') forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> Term -> Telescope
applyUnder (Int
kforall a. Num a => a -> a -> a
-Int
1) (forall a. Subst a => Abs a -> a
absBody Abs Telescope
tel') Term
u
dropAt :: Int -> [a] -> [a]
dropAt :: forall a. Int -> [a] -> [a]
dropAt Int
_ [] = forall a. HasCallStack => a
__IMPOSSIBLE__
dropAt Int
k (a
x:[a]
xs)
| Int
k forall a. Ord a => a -> a -> Bool
< Int
0 = forall a. HasCallStack => a
__IMPOSSIBLE__
| Int
k forall a. Eq a => a -> a -> Bool
== Int
0 = [a]
xs
| Bool
otherwise = a
x forall a. a -> [a] -> [a]
: forall a. Int -> [a] -> [a]
dropAt (Int
kforall a. Num a => a -> a -> a
-Int
1) [a]
xs
solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq :: Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Int
k Term
u UnifyState
s = (,PatternSubstitution
sigma) forall a b. (a -> b) -> a -> b
$ UnifyState
s
{ eqTel :: Telescope
eqTel = Int -> Telescope -> Term -> Telescope
applyUnder Int
k (UnifyState -> Telescope
eqTel UnifyState
s) Term
u'
, eqLHS :: [Arg Term]
eqLHS = forall a. Int -> [a] -> [a]
dropAt Int
k forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
, eqRHS :: [Arg Term]
eqRHS = forall a. Int -> [a] -> [a]
dropAt Int
k forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
}
where
u' :: Term
u' = forall a. Subst a => Int -> a -> a
raise Int
k Term
u
n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
sigma :: PatternSubstitution
sigma = forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
nforall a. Num a => a -> a -> a
-Int
kforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (forall a. Term -> Pattern' a
dotP Term
u') forall a. Substitution' a
idS
data UnifyStep
= Deletion
{ UnifyStep -> Int
deleteAt :: Int
, UnifyStep -> Type
deleteType :: Type
, UnifyStep -> Term
deleteLeft :: Term
, UnifyStep -> Term
deleteRight :: Term
}
| Solution
{ UnifyStep -> Int
solutionAt :: Int
, UnifyStep -> Dom' Term Type
solutionType :: Dom Type
, UnifyStep -> FlexibleVar Int
solutionVar :: FlexibleVar Int
, UnifyStep -> Term
solutionTerm :: Term
}
| Injectivity
{ UnifyStep -> Int
injectAt :: Int
, UnifyStep -> Type
injectType :: Type
, UnifyStep -> QName
injectDatatype :: QName
, UnifyStep -> [Arg Term]
injectParameters :: Args
, UnifyStep -> [Arg Term]
injectIndices :: Args
, UnifyStep -> ConHead
injectConstructor :: ConHead
}
| Conflict
{ UnifyStep -> Int
conflictAt :: Int
, UnifyStep -> Type
conflictType :: Type
, UnifyStep -> QName
conflictDatatype :: QName
, UnifyStep -> [Arg Term]
conflictParameters :: Args
, UnifyStep -> Term
conflictLeft :: Term
, UnifyStep -> Term
conflictRight :: Term
}
| Cycle
{ UnifyStep -> Int
cycleAt :: Int
, UnifyStep -> Type
cycleType :: Type
, UnifyStep -> QName
cycleDatatype :: QName
, UnifyStep -> [Arg Term]
cycleParameters :: Args
, UnifyStep -> Int
cycleVar :: Int
, UnifyStep -> Term
cycleOccursIn :: Term
}
| EtaExpandVar
{ UnifyStep -> FlexibleVar Int
expandVar :: FlexibleVar Int
, UnifyStep -> QName
expandVarRecordType :: QName
, UnifyStep -> [Arg Term]
expandVarParameters :: Args
}
| EtaExpandEquation
{ UnifyStep -> Int
expandAt :: Int
, UnifyStep -> QName
expandRecordType :: QName
, UnifyStep -> [Arg Term]
expandParameters :: Args
}
| LitConflict
{ UnifyStep -> Int
litConflictAt :: Int
, UnifyStep -> Type
litType :: Type
, UnifyStep -> Literal
litConflictLeft :: Literal
, UnifyStep -> Literal
litConflictRight :: Literal
}
| StripSizeSuc
{ UnifyStep -> Int
stripAt :: Int
, UnifyStep -> Term
stripArgLeft :: Term
, UnifyStep -> Term
stripArgRight :: Term
}
| SkipIrrelevantEquation
{ UnifyStep -> Int
skipIrrelevantAt :: Int
}
| TypeConInjectivity
{ UnifyStep -> Int
typeConInjectAt :: Int
, UnifyStep -> QName
typeConstructor :: QName
, UnifyStep -> [Arg Term]
typeConArgsLeft :: Args
, UnifyStep -> [Arg Term]
typeConArgsRight :: Args
} deriving (Int -> UnifyStep -> ShowS
[UnifyStep] -> ShowS
UnifyStep -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnifyStep] -> ShowS
$cshowList :: [UnifyStep] -> ShowS
show :: UnifyStep -> String
$cshow :: UnifyStep -> String
showsPrec :: Int -> UnifyStep -> ShowS
$cshowsPrec :: Int -> UnifyStep -> ShowS
Show)
instance PrettyTCM UnifyStep where
prettyTCM :: forall (m :: * -> *). MonadPretty m => UnifyStep -> m Doc
prettyTCM UnifyStep
step = case UnifyStep
step of
Deletion Int
k Type
a Term
u Term
v -> m Doc
"Deletion" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
, m Doc
"lhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
, m Doc
"rhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
])
Solution Int
k Dom' Term Type
a FlexibleVar Int
i Term
u -> m Doc
"Solution" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Dom' Term Type
a
, m Doc
"variable: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show (forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
i, forall a. FlexibleVar a -> Maybe Int
flexPos FlexibleVar Int
i, forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Int
i, forall a. FlexibleVar a -> FlexibleVarKind
flexKind FlexibleVar Int
i))
, m Doc
"term: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
])
Injectivity Int
k Type
a QName
d [Arg Term]
pars [Arg Term]
ixs ConHead
c -> m Doc
"Injectivity" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
, m Doc
"datatype: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
, m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars)
, m Doc
"indices: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
ixs)
, m Doc
"constructor:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ConHead
c
])
Conflict Int
k Type
a QName
d [Arg Term]
pars Term
u Term
v -> m Doc
"Conflict" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
, m Doc
"datatype: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
, m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars)
, m Doc
"lhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
, m Doc
"rhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
])
Cycle Int
k Type
a QName
d [Arg Term]
pars Int
i Term
u -> m Doc
"Cycle" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
, m Doc
"datatype: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
, m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars)
, m Doc
"variable: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
i)
, m Doc
"term: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
])
EtaExpandVar FlexibleVar Int
fi QName
r [Arg Term]
pars -> m Doc
"EtaExpandVar" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"variable: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show FlexibleVar Int
fi)
, m Doc
"record type:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
, m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars
])
EtaExpandEquation Int
k QName
r [Arg Term]
pars -> m Doc
"EtaExpandEquation" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
, m Doc
"record type:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
r
, m Doc
"parameters: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
pars
])
LitConflict Int
k Type
a Literal
u Literal
v -> m Doc
"LitConflict" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
, m Doc
"lhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Literal
u
, m Doc
"rhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Literal
v
])
StripSizeSuc Int
k Term
u Term
v -> m Doc
"StripSizeSuc" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
, m Doc
"lhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
, m Doc
"rhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
])
SkipIrrelevantEquation Int
k -> m Doc
"SkipIrrelevantEquation" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
])
TypeConInjectivity Int
k QName
d [Arg Term]
us [Arg Term]
vs -> m Doc
"TypeConInjectivity" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
k)
, m Doc
"datatype: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
, m Doc
"lhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
us)
, m Doc
"rhs: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs)
])
type UnifyStrategy = forall m. (PureTCM m, MonadPlus m) => UnifyState -> m UnifyStep
rightToLeftStrategy :: UnifyStrategy
rightToLeftStrategy :: UnifyStrategy
rightToLeftStrategy UnifyState
s =
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for (forall a. Integral a => a -> [a]
downFrom Int
n) forall a b. (a -> b) -> a -> b
$ \Int
k -> Int -> UnifyStrategy
completeStrategyAt Int
k UnifyState
s)
where n :: Int
n = forall a. Sized a => a -> Int
size forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
completeStrategyAt :: Int -> UnifyStrategy
completeStrategyAt :: Int -> UnifyStrategy
completeStrategyAt Int
k UnifyState
s = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Int -> UnifyState -> m UnifyStep
strat -> Int -> UnifyState -> m UnifyStep
strat Int
k UnifyState
s) forall a b. (a -> b) -> a -> b
$
[ (\Int
n -> Int -> UnifyStrategy
skipIrrelevantStrategy Int
n)
, (\Int
n -> Int -> UnifyStrategy
basicUnifyStrategy Int
n)
, (\Int
n -> Int -> UnifyStrategy
literalStrategy Int
n)
, (\Int
n -> Int -> UnifyStrategy
dataStrategy Int
n)
, (\Int
n -> Int -> UnifyStrategy
etaExpandVarStrategy Int
n)
, (\Int
n -> Int -> UnifyStrategy
etaExpandEquationStrategy Int
n)
, (\Int
n -> Int -> UnifyStrategy
injectiveTypeConStrategy Int
n)
, (\Int
n -> Int -> UnifyStrategy
injectivePragmaStrategy Int
n)
, (\Int
n -> Int -> UnifyStrategy
simplifySizesStrategy Int
n)
, (\Int
n -> Int -> UnifyStrategy
checkEqualityStrategy Int
n)
]
isHom :: (Free a, Subst a) => Int -> a -> Maybe a
isHom :: forall a. (Free a, Subst a) => Int -> a -> Maybe a
isHom Int
n a
x = do
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ All -> Bool
getAll forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Bool -> All
All forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Ord a => a -> a -> Bool
>= Int
n)) IgnoreSorts
IgnoreNot a
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Int -> a -> a
raise (-Int
n) a
x
findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Nat)
findFlexible :: Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i FlexibleVars
flex = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Int
i forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FlexibleVar a -> a
flexVar) FlexibleVars
flex
basicUnifyStrategy :: Int -> UnifyStrategy
basicUnifyStrategy :: Int -> UnifyStrategy
basicUnifyStrategy Int
k UnifyState
s = do
Equal dom :: Dom' Term Type
dom@Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel (Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s)
Type
ha <- forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP forall a b. (a -> b) -> a -> b
$ forall a. (Free a, Subst a) => Int -> a -> Maybe a
isHom Int
n Type
a
(Maybe Int
mi, Maybe Int
mj) <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar Term
u Type
ha forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). PureTCM m => Term -> Type -> m (Maybe Int)
isEtaVar Term
v Type
ha
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"isEtaVar results: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show [Maybe Int
mi,Maybe Int
mj])
case (Maybe Int
mi, Maybe Int
mj) of
(Just Int
i, Just Int
j)
| Int
i forall a. Eq a => a -> a -> Bool
== Int
j -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
(Just Int
i, Just Int
j)
| Just FlexibleVar Int
fi <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i FlexibleVars
flex
, Just FlexibleVar Int
fj <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
j FlexibleVars
flex -> do
let choice :: FlexChoice
choice = forall a. ChooseFlex a => a -> a -> FlexChoice
chooseFlex FlexibleVar Int
fi FlexibleVar Int
fj
firstTryLeft :: m UnifyStep
firstTryLeft = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom' Term Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fi Term
v)
, forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom' Term Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fj Term
u)]
firstTryRight :: m UnifyStep
firstTryRight = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom' Term Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fj Term
u)
, forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom' Term Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fi Term
v)]
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"fi = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show FlexibleVar Int
fi)
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"fj = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show FlexibleVar Int
fj)
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"chooseFlex: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show FlexChoice
choice)
case FlexChoice
choice of
FlexChoice
ChooseLeft -> m UnifyStep
firstTryLeft
FlexChoice
ChooseRight -> m UnifyStep
firstTryRight
FlexChoice
ExpandBoth -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
FlexChoice
ChooseEither -> m UnifyStep
firstTryRight
(Just Int
i, Maybe Int
_)
| Just FlexibleVar Int
fi <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i FlexibleVars
flex -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom' Term Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fi Term
v
(Maybe Int
_, Just Int
j)
| Just FlexibleVar Int
fj <- Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
j FlexibleVars
flex -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Dom' Term Type -> FlexibleVar Int -> Term -> UnifyStep
Solution Int
k Dom' Term Type
dom{unDom :: Type
unDom = Type
ha} FlexibleVar Int
fj Term
u
(Maybe Int, Maybe Int)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
where
flex :: FlexibleVars
flex = UnifyState -> FlexibleVars
flexVars UnifyState
s
n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
dataStrategy :: Int -> UnifyStrategy
dataStrategy :: Int -> UnifyStrategy
dataStrategy Int
k UnifyState
s = do
Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqConstructorForm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Int -> UnifyState -> Equality
getEqualityUnraised Int
k UnifyState
s)
Sort
sa <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. LensSort a => a -> Sort
getSort Type
a
case forall t a. Type'' t a -> a
unEl Type
a of
Def QName
d Elims
es | Type{} <- Sort
sa -> do
Int
npars <- forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Int)
getNumberOfParameters QName
d
let ([Arg Term]
pars,[Arg Term]
ixs) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
npars 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
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Found equation at datatype " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" with parameters " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size (UnifyState -> Telescope
eqTel UnifyState
s) forall a. Num a => a -> a -> a
- Int
k) [Arg Term]
pars)
case (Term
u, Term
v) of
(Con ConHead
c ConInfo
_ Elims
_ , Con ConHead
c' ConInfo
_ Elims
_ ) | ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead
c' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int
-> Type
-> QName
-> [Arg Term]
-> [Arg Term]
-> ConHead
-> UnifyStep
Injectivity Int
k Type
a QName
d [Arg Term]
pars [Arg Term]
ixs ConHead
c
(Con ConHead
c ConInfo
_ Elims
_ , Con ConHead
c' ConInfo
_ Elims
_ ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> [Arg Term] -> Term -> Term -> UnifyStep
Conflict Int
k Type
a QName
d [Arg Term]
pars Term
u Term
v
(Var Int
i [] , Term
v ) -> forall {m :: * -> *} {a} {b}.
(ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
Int -> a -> m b -> m b
ifOccursStronglyRigid Int
i Term
v forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> [Arg Term] -> Int -> Term -> UnifyStep
Cycle Int
k Type
a QName
d [Arg Term]
pars Int
i Term
v
(Term
u , Var Int
j [] ) -> forall {m :: * -> *} {a} {b}.
(ForceNotFree a, Reduce a, MonadReduce m, Free a, MonadPlus m) =>
Int -> a -> m b -> m b
ifOccursStronglyRigid Int
j Term
u forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> QName -> [Arg Term] -> Int -> Term -> UnifyStep
Cycle Int
k Type
a QName
d [Arg Term]
pars Int
j Term
u
(Term, Term)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
Term
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
where
ifOccursStronglyRigid :: Int -> a -> m b -> m b
ifOccursStronglyRigid Int
i a
u m b
ret = do
(IntMap IsFree
_ , a
u) <- forall a (m :: * -> *).
(ForceNotFree a, Reduce a, MonadReduce m) =>
IntSet -> a -> m (IntMap IsFree, a)
forceNotFree (forall el coll. Singleton el coll => el -> coll
singleton Int
i) a
u
case forall a. Free a => Int -> a -> Maybe (FlexRig' ())
flexRigOccurrenceIn Int
i a
u of
Just FlexRig' ()
StronglyRigid -> m b
ret
Maybe (FlexRig' ())
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
checkEqualityStrategy :: Int -> UnifyStrategy
checkEqualityStrategy :: Int -> UnifyStrategy
checkEqualityStrategy Int
k UnifyState
s = do
let Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
Type
ha <- forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP forall a b. (a -> b) -> a -> b
$ forall a. (Free a, Subst a) => Int -> a -> Maybe a
isHom Int
n Type
a
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> Term -> Term -> UnifyStep
Deletion Int
k Type
ha Term
u Term
v
literalStrategy :: Int -> UnifyStrategy
literalStrategy :: Int -> UnifyStrategy
literalStrategy Int
k UnifyState
s = do
let n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
Type
ha <- forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP forall a b. (a -> b) -> a -> b
$ forall a. (Free a, Subst a) => Int -> a -> Maybe a
isHom Int
n Type
a
(Term
u, Term
v) <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
u, Term
v)
case (Term
u , Term
v) of
(Lit Literal
l1 , Lit Literal
l2)
| Literal
l1 forall a. Eq a => a -> a -> Bool
== Literal
l2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> Term -> Term -> UnifyStep
Deletion Int
k Type
ha Term
u Term
v
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Type -> Literal -> Literal -> UnifyStep
LitConflict Int
k Type
ha Literal
l1 Literal
l2
(Term, Term)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
etaExpandVarStrategy :: Int -> UnifyStrategy
etaExpandVarStrategy :: Int -> UnifyStrategy
etaExpandVarStrategy Int
k UnifyState
s = do
Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand Term
u Term
v Type
a UnifyState
s forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand Term
v Term
u Type
a UnifyState
s
where
shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand :: Term -> Term -> Type -> UnifyStrategy
shouldEtaExpand (Var Int
i Elims
es) Term
v Type
a UnifyState
s = do
FlexibleVar Int
fi <- forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP forall a b. (a -> b) -> a -> b
$ Int -> FlexibleVars -> Maybe (FlexibleVar Int)
findFlexible Int
i (UnifyState -> FlexibleVars
flexVars UnifyState
s)
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
50 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Found flexible variable " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => String -> m Doc
text (forall a. Show a => a -> String
show Int
i)
Type
b <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Dom' Term Type
getVarTypeUnraised (UnifyState -> Int
varCount UnifyState
s forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- Int
i) UnifyState
s
(QName
d, [Arg Term]
pars) <- forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, [Arg Term]))
isEtaRecordType Type
b
[(ProjOrigin, QName)]
ps <- forall (m :: * -> *) a. MonadPlus m => Maybe a -> m a
fromMaybeMP forall a b. (a -> b) -> a -> b
$ forall t. [Elim' t] -> Maybe [(ProjOrigin, QName)]
allProjElims Elims
es
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM
[ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null [(ProjOrigin, QName)]
ps
, forall {f :: * -> *}. HasConstInfo f => Term -> f Bool
isRecCon Term
v
, (forall a b. b -> Either a b
Right Bool
True forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> [Arg Term] -> m Bool
isSingletonRecord QName
d [Arg Term]
pars)
]
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
50 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"with projections " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(ProjOrigin, QName)]
ps)
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
50 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"at record type " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
d
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FlexibleVar Int -> QName -> [Arg Term] -> UnifyStep
EtaExpandVar FlexibleVar Int
fi QName
d [Arg Term]
pars
shouldEtaExpand Term
_ Term
_ Type
_ UnifyState
_ = forall (m :: * -> *) a. MonadPlus m => m a
mzero
isRecCon :: Term -> f Bool
isRecCon (Con ConHead
c ConInfo
_ Elims
_) = forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor (ConHead -> QName
conName ConHead
c)
isRecCon Term
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
etaExpandEquationStrategy :: Int -> UnifyStrategy
etaExpandEquationStrategy :: Int -> UnifyStrategy
etaExpandEquationStrategy Int
k UnifyState
s = do
Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEqualityUnraised Int
k UnifyState
s
(QName
d, [Arg Term]
pars) <- forall (m :: * -> *) a. MonadPlus m => m (Maybe a) -> m a
catMaybesMP forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
HasConstInfo m =>
Type -> m (Maybe (QName, [Arg Term]))
isEtaRecordType Type
a
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
orM
[ (forall a b. b -> Either a b
Right Bool
True forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> [Arg Term] -> m Bool
isSingletonRecord QName
d [Arg Term]
pars)
, forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject Term
u
, forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject Term
v
]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> QName -> [Arg Term] -> UnifyStep
EtaExpandEquation Int
k QName
d [Arg Term]
pars
where
shouldProject :: PureTCM m => Term -> m Bool
shouldProject :: forall (m :: * -> *). PureTCM m => Term -> m Bool
shouldProject = \case
Def QName
f Elims
es -> forall (m :: * -> *). HasConstInfo m => QName -> m Bool
usesCopatterns QName
f
Con ConHead
c ConInfo
_ Elims
_ -> forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe (QName, Defn))
isRecordConstructor (ConHead -> QName
conName ConHead
c)
Var Int
_ Elims
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Lam ArgInfo
_ Abs Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
Lit Literal
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
Pi Dom' Term Type
_ Abs Type
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
Sort Sort
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
Level Level
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
MetaV MetaId
_ Elims
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
DontCare Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Dummy String
s Elims
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s
tel :: Telescope
tel = UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` [Dom (String, Type)] -> Telescope
telFromList (forall a. Int -> [a] -> [a]
take Int
k forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s)
simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy :: Int -> UnifyStrategy
simplifySizesStrategy Int
k UnifyState
s = do
QName -> Bool
isSizeName <- forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (QName -> Bool)
isSizeNameTest
Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
case forall t a. Type'' t a -> a
unEl Type
a of
Def QName
d Elims
_ -> do
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ QName -> Bool
isSizeName QName
d
SizeView
su <- forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
SizeView
sv <- forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
v
case (SizeView
su, SizeView
sv) of
(SizeSuc Term
u, SizeSuc Term
v) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
(SizeSuc Term
u, SizeView
SizeInf ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
(SizeView
SizeInf , SizeSuc Term
v) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term -> UnifyStep
StripSizeSuc Int
k Term
u Term
v
(SizeView, SizeView)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
Term
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy :: Int -> UnifyStrategy
injectiveTypeConStrategy Int
k UnifyState
s = do
Bool
injTyCon <- PragmaOptions -> Bool
optInjectiveTypeConstructors forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
injTyCon
Equality
eq <- forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
case Equality
eq of
Equal Dom' Term Type
a u :: Term
u@(Def QName
d Elims
es) v :: Term
v@(Def QName
d' Elims
es') | QName
d forall a. Eq a => a -> a -> Bool
== QName
d' -> do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ case Definition -> Defn
theDef Definition
def of
Datatype{} -> Bool
True
Record{} -> Bool
True
Axiom{} -> Bool
True
DataOrRecSig{} -> Bool
True
AbstractDefn{} -> Bool
False
Function{} -> Bool
False
Primitive{} -> Bool
False
PrimitiveSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
GeneralizableVar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Constructor{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
let us :: [Arg Term]
us = 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
vs :: [Arg Term]
vs = 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'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> QName -> [Arg Term] -> [Arg Term] -> UnifyStep
TypeConInjectivity Int
k QName
d [Arg Term]
us [Arg Term]
vs
Equality
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
injectivePragmaStrategy :: Int -> UnifyStrategy
injectivePragmaStrategy :: Int -> UnifyStrategy
injectivePragmaStrategy Int
k UnifyState
s = do
Equality
eq <- forall (m :: * -> *). HasBuiltins m => Equality -> m Equality
eqUnLevel forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
case Equality
eq of
Equal Dom' Term Type
a u :: Term
u@(Def QName
d Elims
es) v :: Term
v@(Def QName
d' Elims
es') | QName
d forall a. Eq a => a -> a -> Bool
== QName
d' -> do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Definition -> Bool
defInjective Definition
def
let us :: [Arg Term]
us = 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
vs :: [Arg Term]
vs = 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'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> QName -> [Arg Term] -> [Arg Term] -> UnifyStep
TypeConInjectivity Int
k QName
d [Arg Term]
us [Arg Term]
vs
Equality
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
skipIrrelevantStrategy :: Int -> UnifyStrategy
skipIrrelevantStrategy :: Int -> UnifyStrategy
skipIrrelevantStrategy Int
k UnifyState
s = do
let Equal Dom' Term Type
a Term
_ Term
_ = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Eq a => a -> a -> Bool
== forall a b. b -> Either a b
Right Bool
True) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM Dom' Term Type
a)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> UnifyStep
SkipIrrelevantEquation Int
k
data UnifyLogEntry
= UnificationStep UnifyState UnifyStep
type UnifyLog = [UnifyLogEntry]
data UnifyOutput = UnifyOutput
{ UnifyOutput -> PatternSubstitution
unifySubst :: PatternSubstitution
, UnifyOutput -> PatternSubstitution
unifyProof :: PatternSubstitution
, UnifyOutput -> UnifyLog
unifyLog :: UnifyLog
}
instance Semigroup UnifyOutput where
UnifyOutput
x <> :: UnifyOutput -> UnifyOutput -> UnifyOutput
<> UnifyOutput
y = UnifyOutput
{ unifySubst :: PatternSubstitution
unifySubst = UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
y forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
x
, unifyProof :: PatternSubstitution
unifyProof = UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
y forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
x
, unifyLog :: UnifyLog
unifyLog = UnifyOutput -> UnifyLog
unifyLog UnifyOutput
x forall a. [a] -> [a] -> [a]
++ UnifyOutput -> UnifyLog
unifyLog UnifyOutput
y
}
instance Monoid UnifyOutput where
mempty :: UnifyOutput
mempty = PatternSubstitution
-> PatternSubstitution -> UnifyLog -> UnifyOutput
UnifyOutput forall a. Substitution' a
IdS forall a. Substitution' a
IdS []
mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput
mappend = forall a. Semigroup a => a -> a -> a
(<>)
type UnifyLogT m a = WriterT UnifyOutput m a
tellUnifySubst :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()
tellUnifySubst :: forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifySubst PatternSubstitution
sub = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall a b. (a -> b) -> a -> b
$ PatternSubstitution
-> PatternSubstitution -> UnifyLog -> UnifyOutput
UnifyOutput PatternSubstitution
sub forall a. Substitution' a
IdS []
tellUnifyProof :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()
tellUnifyProof :: forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sub = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall a b. (a -> b) -> a -> b
$ PatternSubstitution
-> PatternSubstitution -> UnifyLog -> UnifyOutput
UnifyOutput forall a. Substitution' a
IdS PatternSubstitution
sub []
writeUnifyLog :: MonadWriter UnifyOutput m => UnifyLogEntry -> m ()
writeUnifyLog :: forall (m :: * -> *).
MonadWriter UnifyOutput m =>
UnifyLogEntry -> m ()
writeUnifyLog UnifyLogEntry
x = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall a b. (a -> b) -> a -> b
$ PatternSubstitution
-> PatternSubstitution -> UnifyLog -> UnifyOutput
UnifyOutput forall a. Substitution' a
IdS forall a. Substitution' a
IdS [UnifyLogEntry
x]
runUnifyLogT :: UnifyLogT m a -> m (a,UnifyOutput)
runUnifyLogT :: forall (m :: * -> *) a. UnifyLogT m a -> m (a, UnifyOutput)
runUnifyLogT = forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
unifyStep
:: (PureTCM m, MonadWriter UnifyOutput m)
=> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
unifyStep :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
unifyStep UnifyState
s Deletion{ deleteAt :: UnifyStep -> Int
deleteAt = Int
k , deleteType :: UnifyStep -> Type
deleteType = Type
a , deleteLeft :: UnifyStep -> Term
deleteLeft = Term
u , deleteRight :: UnifyStep -> Term
deleteRight = Term
v } = do
Either Blocker Bool
isReflexive <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Term -> Term -> m Bool
pureEqualTerm Type
a Term
u Term
v
Bool
withoutK <- forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
Bool
splitOnStrict <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envSplitOnStrict
case Either Blocker Bool
isReflexive of
Left Blocker
block -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block
Right Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
Right Bool
True | Bool
withoutK Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
splitOnStrict
-> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Term -> UnificationFailure
UnifyReflexiveEq (UnifyState -> Telescope
varTel UnifyState
s) Type
a Term
u]
Right Bool
True -> do
let (UnifyState
s', PatternSubstitution
sigma) = Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Int
k Term
u UnifyState
s
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
forall a. a -> UnificationResult' a
Unifies forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' Telescope UnifyState
lensEqTel forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce UnifyState
s'
unifyStep UnifyState
s step :: UnifyStep
step@Solution{} = forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
RetryNormalised
-> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
solutionStep RetryNormalised
RetryNormalised UnifyState
s UnifyStep
step
unifyStep UnifyState
s (Injectivity Int
k Type
a QName
d [Arg Term]
pars [Arg Term]
ixs ConHead
c) = do
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) forall a b. (a -> b) -> a -> b
$ do
Bool
withoutK <- forall (m :: * -> *). HasOptions m => m Bool
withoutKOption
let ([Dom (String, Type)]
eqListTel1, Dom (String, Type)
_ : [Dom (String, Type)]
eqListTel2) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
k forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (String, t)]
telToList forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
(Telescope
eqTel1, Telescope
eqTel2) = ([Dom (String, Type)] -> Telescope
telFromList [Dom (String, Type)]
eqListTel1, [Dom (String, Type)] -> Telescope
telFromList [Dom (String, Type)]
eqListTel2)
Definition
cdef <- forall (m :: * -> *). HasConstInfo m => ConHead -> m Definition
getConInfo ConHead
c
let ctype :: Type
ctype = Definition -> Type
defType Definition
cdef Type -> [Arg Term] -> Type
`piApply` [Arg Term]
pars
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel1) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Constructor type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
ctype
TelV Telescope
ctel Type
ctarget <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
ctype
let cixs :: [Arg Term]
cixs = case forall t a. Type'' t a -> a
unEl Type
ctarget of
Def QName
d' Elims
es | QName
d forall a. Eq a => a -> a -> Bool
== QName
d' ->
let args :: [Arg Term]
args = 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
in forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
pars) [Arg Term]
args
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
Type
dtype <- (Type -> [Arg Term] -> Type
`piApply` [Arg Term]
pars) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel1) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
40 forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Datatype type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
dtype
let hduTel :: Telescope
hduTel = Telescope
eqTel1 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
notforced :: [IsForced]
notforced = forall a. Int -> a -> [a]
replicate (forall a. Sized a => a -> Int
size Telescope
hduTel) IsForced
NotForced
UnificationResult
res <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Telescope
-> FlexibleVars
-> Type
-> [Arg Term]
-> [Arg Term]
-> m UnificationResult
unifyIndices'
Telescope
hduTel
([IsForced] -> Telescope -> FlexibleVars
allFlexVars [IsForced]
notforced Telescope
hduTel)
(forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
ctel) Type
dtype)
(forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
ctel) [Arg Term]
ixs)
[Arg Term]
cixs
case UnificationResult
res of
NoUnify NegativeUnification
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
UnifyBlocked Blocker
block -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block
UnifyStuck [UnificationFailure]
_ | Bool -> Bool
not Bool
withoutK -> do
let eqTel1' :: Telescope
eqTel1' = Telescope
eqTel1 forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
ctel
rho1 :: PatternSubstitution
rho1 = forall a. Int -> Substitution' a
raiseS (forall a. Sized a => a -> Int
size Telescope
ctel)
ceq :: Pattern' DBPatVar
ceq = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
ctel
rho3 :: PatternSubstitution
rho3 = forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Pattern' DBPatVar
ceq PatternSubstitution
rho1
eqTel2' :: Telescope
eqTel2' = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho3 Telescope
eqTel2
eqTel' :: Telescope
eqTel' = Telescope
eqTel1' forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
rho :: PatternSubstitution
rho = forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size Telescope
eqTel2) PatternSubstitution
rho3
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
rho
Telescope
eqTel' <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Telescope
eqTel'
([Arg Term]
lhs', [Arg Term]
rhs') <- do
let ps :: [NamedArg (Pattern' DBPatVar)]
ps = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
(Match Term
lhsMatch, [Arg Term]
_) <- forall (m :: * -> *).
MonadMatch m =>
[NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> m (Match Term, [Arg Term])
Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
ps forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
(Match Term
rhsMatch, [Arg Term]
_) <- forall (m :: * -> *).
MonadMatch m =>
[NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> m (Match Term, [Arg Term])
Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
ps forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
case (Match Term
lhsMatch, Match Term
rhsMatch) of
(Match.Yes Simplification
_ IntMap (Arg Term)
lhs', Match.Yes Simplification
_ IntMap (Arg Term)
rhs') -> forall (m :: * -> *) a. Monad m => a -> m a
return
(forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
lhs',
forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
rhs')
(Match Term, Match Term)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies forall a b. (a -> b) -> a -> b
$ UnifyState
s { eqTel :: Telescope
eqTel = Telescope
eqTel' , eqLHS :: [Arg Term]
eqLHS = [Arg Term]
lhs' , eqRHS :: [Arg Term]
eqRHS = [Arg Term]
rhs' }
UnifyStuck [UnificationFailure]
_ -> let n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
Equal Dom{unDom :: forall t e. Dom' t e -> e
unDom = Type
a} Term
u Term
v = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
in forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope
-> Type -> Term -> Term -> [Arg Term] -> UnificationFailure
UnifyIndicesNotVars
(UnifyState -> Telescope
varTel UnifyState
s forall t. Abstract t => Telescope -> t -> t
`abstract` UnifyState -> Telescope
eqTel UnifyState
s) Type
a
(forall a. Subst a => Int -> a -> a
raise Int
n Term
u) (forall a. Subst a => Int -> a -> a
raise Int
n Term
v) (forall a. Subst a => Int -> a -> a
raise (Int
nforall a. Num a => a -> a -> a
-Int
k) [Arg Term]
ixs)]
Unifies (Telescope
eqTel1', PatternSubstitution
rho0, [NamedArg (Pattern' DBPatVar)]
_) -> do
let (PatternSubstitution
rho1, PatternSubstitution
rho2) = forall a.
Int -> Substitution' a -> (Substitution' a, Substitution' a)
splitS (forall a. Sized a => a -> Int
size Telescope
ctel) PatternSubstitution
rho0
let ceq :: Pattern' DBPatVar
ceq = forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
noConPatternInfo forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
rho2 forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs Telescope
ctel
rho3 :: PatternSubstitution
rho3 = forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Pattern' DBPatVar
ceq PatternSubstitution
rho1
eqTel2' :: Telescope
eqTel2' = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho3 Telescope
eqTel2
eqTel' :: Telescope
eqTel' = Telescope
eqTel1' forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
eqTel2'
rho :: PatternSubstitution
rho = forall a. Int -> Substitution' a -> Substitution' a
liftS (forall a. Sized a => a -> Int
size Telescope
eqTel2) PatternSubstitution
rho3
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
rho
Telescope
eqTel' <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Telescope
eqTel'
([Arg Term]
lhs', [Arg Term]
rhs') <- do
let ps :: [NamedArg (Pattern' DBPatVar)]
ps = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => Telescope -> [NamedArg a]
teleNamedArgs forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
(Match Term
lhsMatch, [Arg Term]
_) <- forall (m :: * -> *).
MonadMatch m =>
[NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> m (Match Term, [Arg Term])
Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
ps forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
(Match Term
rhsMatch, [Arg Term]
_) <- forall (m :: * -> *).
MonadMatch m =>
[NamedArg (Pattern' DBPatVar)]
-> [Arg Term] -> m (Match Term, [Arg Term])
Match.matchPatterns [NamedArg (Pattern' DBPatVar)]
ps forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
case (Match Term
lhsMatch, Match Term
rhsMatch) of
(Match.Yes Simplification
_ IntMap (Arg Term)
lhs', Match.Yes Simplification
_ IntMap (Arg Term)
rhs') -> forall (m :: * -> *) a. Monad m => a -> m a
return
(forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
lhs',
forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
Match.matchedArgs forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. Sized a => a -> Int
size Telescope
eqTel') IntMap (Arg Term)
rhs')
(Match Term, Match Term)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies forall a b. (a -> b) -> a -> b
$ UnifyState
s { eqTel :: Telescope
eqTel = Telescope
eqTel' , eqLHS :: [Arg Term]
eqLHS = [Arg Term]
lhs' , eqRHS :: [Arg Term]
eqRHS = [Arg Term]
rhs' }
unifyStep UnifyState
s Conflict
{ conflictLeft :: UnifyStep -> Term
conflictLeft = Term
u
, conflictRight :: UnifyStep -> Term
conflictRight = Term
v
} =
case Term
u of
Con ConHead
h ConInfo
_ Elims
_ -> do
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
h) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. NegativeUnification -> UnificationResult' a
NoUnify forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term -> NegativeUnification
UnifyConflict (UnifyState -> Telescope
varTel UnifyState
s) Term
u Term
v
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
unifyStep UnifyState
s Cycle
{ cycleVar :: UnifyStep -> Int
cycleVar = Int
i
, cycleOccursIn :: UnifyStep -> Term
cycleOccursIn = Term
u
} =
case Term
u of
Con ConHead
h ConInfo
_ Elims
_ -> do
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). HasConstInfo m => QName -> m Bool
consOfHIT forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
h) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []) forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. NegativeUnification -> UnificationResult' a
NoUnify forall a b. (a -> b) -> a -> b
$ Telescope -> Int -> Term -> NegativeUnification
UnifyCycle (UnifyState -> Telescope
varTel UnifyState
s) Int
i Term
u
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
unifyStep UnifyState
s EtaExpandVar{ expandVar :: UnifyStep -> FlexibleVar Int
expandVar = FlexibleVar Int
fi, expandVarRecordType :: UnifyStep -> QName
expandVarRecordType = QName
d , expandVarParameters :: UnifyStep -> [Arg Term]
expandVarParameters = [Arg Term]
pars } = do
Defn
recd <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
d
let delta :: Telescope
delta = Defn -> Telescope
recTel Defn
recd forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
pars
c :: ConHead
c = Defn -> ConHead
recConHead Defn
recd
let nfields :: Int
nfields = forall a. Sized a => a -> Int
size Telescope
delta
(Telescope
varTel', PatternSubstitution
rho) = Telescope
-> Int -> Telescope -> ConHead -> (Telescope, PatternSubstitution)
expandTelescopeVar (UnifyState -> Telescope
varTel UnifyState
s) (Int
mforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
i) Telescope
delta ConHead
c
projectFlexible :: FlexibleVars
projectFlexible = [ forall a.
ArgInfo
-> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
FlexibleVar (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo FlexibleVar Int
fi) (forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Int
fi) (Int -> FlexibleVarKind
projFlexKind Int
j) (forall a. FlexibleVar a -> Maybe Int
flexPos FlexibleVar Int
fi) (Int
iforall a. Num a => a -> a -> a
+Int
j) | Int
j <- [Int
0..Int
nfieldsforall a. Num a => a -> a -> a
-Int
1] ]
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifySubst forall a b. (a -> b) -> a -> b
$ PatternSubstitution
rho
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies forall a b. (a -> b) -> a -> b
$ UState
{ varTel :: Telescope
varTel = Telescope
varTel'
, flexVars :: FlexibleVars
flexVars = FlexibleVars
projectFlexible forall a. [a] -> [a] -> [a]
++ Int -> FlexibleVars -> FlexibleVars
liftFlexibles Int
nfields (UnifyState -> FlexibleVars
flexVars UnifyState
s)
, eqTel :: Telescope
eqTel = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
, eqLHS :: [Arg Term]
eqLHS = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
, eqRHS :: [Arg Term]
eqRHS = forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
}
where
i :: Int
i = forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fi
m :: Int
m = UnifyState -> Int
varCount UnifyState
s
projFlexKind :: Int -> FlexibleVarKind
projFlexKind :: Int -> FlexibleVarKind
projFlexKind Int
j = case forall a. FlexibleVar a -> FlexibleVarKind
flexKind FlexibleVar Int
fi of
RecordFlex [FlexibleVarKind]
ks -> forall a. a -> [a] -> Int -> a
indexWithDefault FlexibleVarKind
ImplicitFlex [FlexibleVarKind]
ks Int
j
FlexibleVarKind
ImplicitFlex -> FlexibleVarKind
ImplicitFlex
FlexibleVarKind
DotFlex -> FlexibleVarKind
DotFlex
FlexibleVarKind
OtherFlex -> FlexibleVarKind
OtherFlex
liftFlexible :: Int -> Int -> Maybe Int
liftFlexible :: Int -> Int -> Maybe Int
liftFlexible Int
n Int
j = if Int
j forall a. Eq a => a -> a -> Bool
== Int
i then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just (if Int
j forall a. Ord a => a -> a -> Bool
> Int
i then Int
j forall a. Num a => a -> a -> a
+ (Int
nforall a. Num a => a -> a -> a
-Int
1) else Int
j)
liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
liftFlexibles :: Int -> FlexibleVars -> FlexibleVars
liftFlexibles Int
n FlexibleVars
fs = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a b. (a -> b) -> a -> b
$ Int -> Int -> Maybe Int
liftFlexible Int
n) FlexibleVars
fs
unifyStep UnifyState
s EtaExpandEquation{ expandAt :: UnifyStep -> Int
expandAt = Int
k, expandRecordType :: UnifyStep -> QName
expandRecordType = QName
d, expandParameters :: UnifyStep -> [Arg Term]
expandParameters = [Arg Term]
pars } = do
Defn
recd <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m (Maybe Defn)
isRecord QName
d
let delta :: Telescope
delta = Defn -> Telescope
recTel Defn
recd forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
pars
c :: ConHead
c = Defn -> ConHead
recConHead Defn
recd
[Arg Term]
lhs <- [Arg Term] -> m [Arg Term]
expandKth forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
[Arg Term]
rhs <- [Arg Term] -> m [Arg Term]
expandKth forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
let (Telescope
tel, PatternSubstitution
sigma) = Telescope
-> Int -> Telescope -> ConHead -> (Telescope, PatternSubstitution)
expandTelescopeVar (UnifyState -> Telescope
eqTel UnifyState
s) Int
k Telescope
delta ConHead
c
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
forall a. a -> UnificationResult' a
Unifies forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Lens' Telescope UnifyState
lensEqTel forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ UnifyState
s
{ eqTel :: Telescope
eqTel = Telescope
tel
, eqLHS :: [Arg Term]
eqLHS = [Arg Term]
lhs
, eqRHS :: [Arg Term]
eqRHS = [Arg Term]
rhs
}
where
expandKth :: [Arg Term] -> m [Arg Term]
expandKth [Arg Term]
us = do
let ([Arg Term]
us1,Arg Term
v:[Arg Term]
us2) = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall n a. Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt Int
k [Arg Term]
us
[Arg Term]
vs <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasConstInfo m, MonadDebug m, ReadTCState m) =>
QName -> [Arg Term] -> Term -> m (Telescope, [Arg Term])
etaExpandRecord QName
d [Arg Term]
pars (forall e. Arg e -> e
unArg Arg Term
v)
[Arg Term]
vs <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce [Arg Term]
vs
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Arg Term]
us1 forall a. [a] -> [a] -> [a]
++ [Arg Term]
vs forall a. [a] -> [a] -> [a]
++ [Arg Term]
us2
unifyStep UnifyState
s LitConflict
{ litType :: UnifyStep -> Type
litType = Type
a
, litConflictLeft :: UnifyStep -> Literal
litConflictLeft = Literal
l
, litConflictRight :: UnifyStep -> Literal
litConflictRight = Literal
l'
} = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. NegativeUnification -> UnificationResult' a
NoUnify forall a b. (a -> b) -> a -> b
$ Telescope -> Term -> Term -> NegativeUnification
UnifyConflict (UnifyState -> Telescope
varTel UnifyState
s) (Literal -> Term
Lit Literal
l) (Literal -> Term
Lit Literal
l')
unifyStep UnifyState
s (StripSizeSuc Int
k Term
u Term
v) = do
Type
sizeTy <- forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
Term
sizeSu <- forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 (Int -> Term
var Int
0)
let n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
sub :: Substitution' Term
sub = forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
nforall a. Num a => a -> a -> a
-Int
kforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS Term
sizeSu forall a b. (a -> b) -> a -> b
$ forall a. Int -> Substitution' a
raiseS Int
1
eqFlatTel :: [Dom' Term Type]
eqFlatTel = forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
eqFlatTel' :: [Dom' Term Type]
eqFlatTel' = forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
sub forall a b. (a -> b) -> a -> b
$ forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
k (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Type
sizeTy) forall a b. (a -> b) -> a -> b
$ [Dom' Term Type]
eqFlatTel
eqTel' :: Telescope
eqTel' = [String] -> [Dom' Term Type] -> Telescope
unflattenTel (Telescope -> [String]
teleNames forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s) [Dom' Term Type]
eqFlatTel'
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies forall a b. (a -> b) -> a -> b
$ UnifyState
s
{ eqTel :: Telescope
eqTel = Telescope
eqTel'
, eqLHS :: [Arg Term]
eqLHS = forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
k (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Term
u) forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
, eqRHS :: [Arg Term]
eqRHS = forall a. Int -> (a -> a) -> [a] -> [a]
updateAt Int
k (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Term
v) forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqRHS UnifyState
s
}
unifyStep UnifyState
s (SkipIrrelevantEquation Int
k) = do
let lhs :: [Arg Term]
lhs = UnifyState -> [Arg Term]
eqLHS UnifyState
s
(UnifyState
s', PatternSubstitution
sigma) = Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Int
k (Term -> Term
DontCare forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> Int -> a
indexWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Int
k) UnifyState
s
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies UnifyState
s'
unifyStep UnifyState
s (TypeConInjectivity Int
k QName
d [Arg Term]
us [Arg Term]
vs) = do
Type
dtype <- Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
TelV Telescope
dtel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
dtype
let deq :: Term
deq = QName -> Elims -> Term
Def QName
d forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
dtel
forall a. a -> UnificationResult' a
Unifies forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
Lens' Telescope UnifyState
lensEqTel forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ UnifyState
s
{ eqTel :: Telescope
eqTel = Telescope
dtel forall t. Abstract t => Telescope -> t -> t
`abstract` Int -> Telescope -> Term -> Telescope
applyUnder Int
k (UnifyState -> Telescope
eqTel UnifyState
s) (forall a. Subst a => Int -> a -> a
raise Int
k Term
deq)
, eqLHS :: [Arg Term]
eqLHS = [Arg Term]
us forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
dropAt Int
k (UnifyState -> [Arg Term]
eqLHS UnifyState
s)
, eqRHS :: [Arg Term]
eqRHS = [Arg Term]
vs forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
dropAt Int
k (UnifyState -> [Arg Term]
eqRHS UnifyState
s)
}
data RetryNormalised = RetryNormalised | DontRetryNormalised
deriving (RetryNormalised -> RetryNormalised -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RetryNormalised -> RetryNormalised -> Bool
$c/= :: RetryNormalised -> RetryNormalised -> Bool
== :: RetryNormalised -> RetryNormalised -> Bool
$c== :: RetryNormalised -> RetryNormalised -> Bool
Eq, Int -> RetryNormalised -> ShowS
[RetryNormalised] -> ShowS
RetryNormalised -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RetryNormalised] -> ShowS
$cshowList :: [RetryNormalised] -> ShowS
show :: RetryNormalised -> String
$cshow :: RetryNormalised -> String
showsPrec :: Int -> RetryNormalised -> ShowS
$cshowsPrec :: Int -> RetryNormalised -> ShowS
Show)
solutionStep
:: (PureTCM m, MonadWriter UnifyOutput m)
=> RetryNormalised
-> UnifyState
-> UnifyStep
-> m (UnificationResult' UnifyState)
solutionStep :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
RetryNormalised
-> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
solutionStep RetryNormalised
retry UnifyState
s
step :: UnifyStep
step@Solution{ solutionAt :: UnifyStep -> Int
solutionAt = Int
k
, solutionType :: UnifyStep -> Dom' Term Type
solutionType = dom :: Dom' Term Type
dom@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = Type
a }
, solutionVar :: UnifyStep -> FlexibleVar Int
solutionVar = fi :: FlexibleVar Int
fi@FlexibleVar{ flexVar :: forall a. FlexibleVar a -> a
flexVar = Int
i }
, solutionTerm :: UnifyStep -> Term
solutionTerm = Term
u } = do
let m :: Int
m = UnifyState -> Int
varCount UnifyState
s
Bool
inMakeCase <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Bool TCEnv
eMakeCase
let forcedVars :: IntMap Modality
forcedVars | Bool
inMakeCase = forall a. IntMap a
IntMap.empty
| Bool
otherwise = forall a. [(Int, a)] -> IntMap a
IntMap.fromList [ (forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
fi, forall a. LensModality a => a -> Modality
getModality FlexibleVar Int
fi) | FlexibleVar Int
fi <- UnifyState -> FlexibleVars
flexVars UnifyState
s,
forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Int
fi forall a. Eq a => a -> a -> Bool
== IsForced
Forced ]
(Pattern' DBPatVar
p, IntMap Modality
bound) <- forall (m :: * -> *).
PureTCM m =>
IntMap Modality -> Term -> m (Pattern' DBPatVar, IntMap Modality)
patternBindingForcedVars IntMap Modality
forcedVars Term
u
let dotSub :: PatternSubstitution
dotSub = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS forall a. Substitution' a
idS [ forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
i (forall a. Term -> Pattern' a
dotP (Int -> Elims -> Term
Var Int
i [])) | Int
i <- forall a. IntMap a -> [Int]
IntMap.keys IntMap Modality
bound ]
let updModality :: Modality -> IntMap Modality -> Telescope -> Telescope
updModality Modality
md IntMap Modality
vars Telescope
tel
| forall a. IntMap a -> Bool
IntMap.null IntMap Modality
vars = Telescope
tel
| Bool
otherwise = [Dom (String, Type)] -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Dom (String, Type) -> Dom (String, Type)
upd (forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Telescope
tel) (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel)
where
upd :: Int -> Dom (String, Type) -> Dom (String, Type)
upd Int
i Dom (String, Type)
a | Just Modality
md' <- forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Modality
vars = forall a. LensModality a => Modality -> a -> a
setModality (Modality -> Modality -> Modality
composeModality Modality
md Modality
md') Dom (String, Type)
a
| Bool
otherwise = Dom (String, Type)
a
UnifyState
s <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UnifyState
s { varTel :: Telescope
varTel = Modality -> IntMap Modality -> Telescope -> Telescope
updModality (forall a. LensModality a => a -> Modality
getModality FlexibleVar Int
fi) IntMap Modality
bound (UnifyState -> Telescope
varTel UnifyState
s) }
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify.force" Int
45 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"forcedVars =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. IntMap a -> [Int]
IntMap.keys IntMap Modality
forcedVars)
, TCMT IO Doc
"u =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
, TCMT IO Doc
"p =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Pattern' DBPatVar
p
, TCMT IO Doc
"bound =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (forall a. IntMap a -> [Int]
IntMap.keys IntMap Modality
bound)
, TCMT IO Doc
"dotSub =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty PatternSubstitution
dotSub ]
let dom' :: Dom' Term Type
dom'@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = Type
a' } = Int -> UnifyState -> Dom' Term Type
getVarType (Int
mforall a. Num a => a -> a -> a
-Int
1forall a. Num a => a -> a -> a
-Int
i) UnifyState
s
Either Blocker Bool
equalTypes <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked forall a b. (a -> b) -> a -> b
$ do
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Equation type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Variable type: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a'
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type -> Type -> m Bool
pureEqualType Type
a Type
a'
Modality
envmod <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Modality TCEnv
eModality
let eqrel :: Relevance
eqrel = forall a. LensRelevance a => a -> Relevance
getRelevance Dom' Term Type
dom
eqmod :: Modality
eqmod = forall a. LensModality a => a -> Modality
getModality Dom' Term Type
dom
varmod :: Modality
varmod = forall a. LensModality a => a -> Modality
getModality Dom' Term Type
dom'
mod :: Modality
mod = forall a. Bool -> (a -> a) -> a -> a
applyUnless (Relevance
NonStrict Relevance -> Relevance -> Bool
`moreRelevant` Relevance
eqrel) (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
eqrel)
forall a b. (a -> b) -> a -> b
$ forall a. Bool -> (a -> a) -> a -> a
applyUnless (forall a. LensQuantity a => a -> Bool
usableQuantity Modality
envmod) (forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
zeroQuantity)
forall a b. (a -> b) -> a -> b
$ Modality
varmod
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"Equation modality: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. LensModality a => a -> Modality
getModality Dom' Term Type
dom)
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"Variable modality: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Modality
varmod
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
65 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => String -> m Doc
text forall a b. (a -> b) -> a -> b
$ String
"Solution must be usable in a " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Modality
mod forall a. [a] -> [a] -> [a]
++ String
" position."
Either Blocker Bool
eusable <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(UsableModality a, ReadTCState m, HasConstInfo m, MonadTCEnv m,
MonadAddContext m, MonadDebug m, MonadReduce m,
MonadError Blocker m) =>
Modality -> a -> m Bool
usableMod Modality
mod Term
u
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (forall (m :: * -> *) a. Monad m => a -> m a
return Either Blocker Bool
eusable) (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Blocker -> UnificationResult' a
UnifyBlocked) forall a b. (a -> b) -> a -> b
$ \ Bool
usable -> do
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
45 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Modality ok: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Bool
usable
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
usable forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.lhs.unify" Int
65 forall a b. (a -> b) -> a -> b
$ String
"Rejected solution: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
u
if Bool -> Bool
not (forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
eqmod Cohesion -> Cohesion -> Bool
`moreCohesion` forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
varmod) then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [] else do
case Either Blocker Bool
equalTypes of
Left Blocker
block -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
block
Right Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
Right Bool
True | Bool
usable ->
case Int
-> Pattern' DBPatVar
-> UnifyState
-> Maybe (UnifyState, PatternSubstitution)
solveVar (Int
m forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- Int
i) Pattern' DBPatVar
p UnifyState
s of
Maybe (UnifyState, PatternSubstitution)
Nothing | RetryNormalised
retry forall a. Eq a => a -> a -> Bool
== RetryNormalised
RetryNormalised -> do
Term
u <- forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
u
UnifyState
s <- Lens' Telescope UnifyState
lensVarTel forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise UnifyState
s
forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
RetryNormalised
-> UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
solutionStep RetryNormalised
DontRetryNormalised UnifyState
s UnifyStep
step{ solutionTerm :: Term
solutionTerm = Term
u }
Maybe (UnifyState, PatternSubstitution)
Nothing ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Int -> Term -> UnificationFailure
UnifyRecursiveEq (UnifyState -> Telescope
varTel UnifyState
s) Type
a Int
i Term
u]
Just (UnifyState
s', PatternSubstitution
sub) -> do
let rho :: PatternSubstitution
rho = PatternSubstitution
sub forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` PatternSubstitution
dotSub
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifySubst PatternSubstitution
rho
let (UnifyState
s'', PatternSubstitution
sigma) = Int -> Term -> UnifyState -> (UnifyState, PatternSubstitution)
solveEq Int
k (forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
rho Term
u) UnifyState
s'
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sigma
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies UnifyState
s''
Right Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [Telescope -> Type -> Int -> Term -> Modality -> UnificationFailure
UnifyUnusableModality (UnifyState -> Telescope
varTel UnifyState
s) Type
a Int
i Term
u Modality
mod]
solutionStep RetryNormalised
_ UnifyState
_ UnifyStep
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
unify
:: (PureTCM m, MonadWriter UnifyOutput m)
=> UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify UnifyState
s UnifyStrategy
strategy = if UnifyState -> Bool
isUnifyStateSolved UnifyState
s
then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> UnificationResult' a
Unifies UnifyState
s
else forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
ListT m UnifyStep -> m (UnificationResult' UnifyState)
tryUnifyStepsAndContinue (UnifyStrategy
strategy UnifyState
s)
where
tryUnifyStepsAndContinue
:: (PureTCM m, MonadWriter UnifyOutput m)
=> ListT m UnifyStep -> m (UnificationResult' UnifyState)
tryUnifyStepsAndContinue :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
ListT m UnifyStep -> m (UnificationResult' UnifyState)
tryUnifyStepsAndContinue ListT m UnifyStep
steps = do
UnificationResult' UnifyState
x <- forall (m :: * -> *) a b.
Monad m =>
(a -> m b -> m b) -> m b -> ListT m a -> m b
foldListT forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
UnifyStep
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
tryUnifyStep forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
failure ListT m UnifyStep
steps
case UnificationResult' UnifyState
x of
Unifies UnifyState
s' -> forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
UnifyState -> UnifyStrategy -> m (UnificationResult' UnifyState)
unify UnifyState
s' UnifyStrategy
strategy
NoUnify NegativeUnification
err -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. NegativeUnification -> UnificationResult' a
NoUnify NegativeUnification
err
UnifyBlocked Blocker
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
b
UnifyStuck [UnificationFailure]
err -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck [UnificationFailure]
err
tryUnifyStep :: (PureTCM m, MonadWriter UnifyOutput m)
=> UnifyStep
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
tryUnifyStep :: forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
UnifyStep
-> m (UnificationResult' UnifyState)
-> m (UnificationResult' UnifyState)
tryUnifyStep UnifyStep
step m (UnificationResult' UnifyState)
fallback = do
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying unifyStep" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyStep
step
UnificationResult' UnifyState
x <- forall (m :: * -> *).
(PureTCM m, MonadWriter UnifyOutput m) =>
UnifyState -> UnifyStep -> m (UnificationResult' UnifyState)
unifyStep UnifyState
s UnifyStep
step
case UnificationResult' UnifyState
x of
Unifies UnifyState
s' -> do
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"unifyStep successful."
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.lhs.unify" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"new unifyState:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM UnifyState
s'
forall (m :: * -> *).
MonadWriter UnifyOutput m =>
UnifyLogEntry -> m ()
writeUnifyLog forall a b. (a -> b) -> a -> b
$ UnifyState -> UnifyStep -> UnifyLogEntry
UnificationStep UnifyState
s UnifyStep
step
forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
NoUnify{} -> forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
x
UnifyBlocked Blocker
b1 -> do
UnificationResult' UnifyState
y <- m (UnificationResult' UnifyState)
fallback
case UnificationResult' UnifyState
y of
UnifyStuck [UnificationFailure]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked Blocker
b1
UnifyBlocked Blocker
b2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Blocker -> UnificationResult' a
UnifyBlocked forall a b. (a -> b) -> a -> b
$ Blocker -> Blocker -> Blocker
unblockOnEither Blocker
b1 Blocker
b2
UnificationResult' UnifyState
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
y
UnifyStuck [UnificationFailure]
err1 -> do
UnificationResult' UnifyState
y <- m (UnificationResult' UnifyState)
fallback
case UnificationResult' UnifyState
y of
UnifyStuck [UnificationFailure]
err2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck forall a b. (a -> b) -> a -> b
$ [UnificationFailure]
err1 forall a. [a] -> [a] -> [a]
++ [UnificationFailure]
err2
UnificationResult' UnifyState
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return UnificationResult' UnifyState
y
failure :: Monad m => m (UnificationResult' a)
failure :: forall (m :: * -> *) a. Monad m => m (UnificationResult' a)
failure = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [UnificationFailure] -> UnificationResult' a
UnifyStuck []
patternBindingForcedVars :: PureTCM m => IntMap Modality -> Term -> m (DeBruijnPattern, IntMap Modality)
patternBindingForcedVars :: forall (m :: * -> *).
PureTCM m =>
IntMap Modality -> Term -> m (Pattern' DBPatVar, IntMap Modality)
patternBindingForcedVars IntMap Modality
forced Term
v = do
let v' :: Term
v' = forall a. PrecomputeFreeVars a => a -> a
precomputeFreeVars_ Term
v
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
{m :: * -> *} {a}.
(MonadWriter (IntMap Modality) (t (t m)), HasConstInfo (t (t m)),
DeBruijn a, MonadTrans t, MonadTrans t, Monad (t m), MonadReduce m,
MonadState (IntMap Modality) (t (t m))) =>
Modality -> Term -> t (t m) (Pattern' a)
go Modality
defaultModality Term
v') IntMap Modality
forced)
where
noForced :: a -> m Bool
noForced a
v = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ IntSet -> IntSet -> Bool
IntSet.disjoint (forall a. PrecomputeFreeVars a => a -> IntSet
precomputedFreeVars a
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IntMap a -> IntSet
IntMap.keysSet
bind :: a -> Int -> m (Pattern' a)
bind a
md Int
i = do
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just a
md' | forall a. PartialOrd a => a -> PartialOrdering -> a -> Bool
related a
md PartialOrdering
POLE a
md' -> do
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> IntMap a
IntMap.singleton Int
i a
md
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. Int -> IntMap a -> IntMap a
IntMap.delete Int
i
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Pattern' a
varP (forall a. DeBruijn a => Int -> a
deBruijnVar Int
i)
Maybe a
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP (Int -> Elims -> Term
Var Int
i [])
go :: Modality -> Term -> t (t m) (Pattern' a)
go Modality
md Term
v = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall {a} {m :: * -> *} {a}.
(MonadState (IntMap a) m, PrecomputeFreeVars a) =>
a -> m Bool
noForced Term
v) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v) forall a b. (a -> b) -> a -> b
$ do
Term
v' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
case Term
v' of
Var Int
i [] -> forall {a} {m :: * -> *} {a}.
(MonadState (IntMap a) m, PartialOrd a, MonadWriter (IntMap a) m,
DeBruijn a) =>
a -> Int -> m (Pattern' a)
bind Modality
md Int
i
Con ConHead
c ConInfo
ci Elims
es
| Just [Arg Term]
vs <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
[IsForced]
fs <- Definition -> [IsForced]
defForced forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)
let goArg :: IsForced -> Arg Term -> t (t m) (NamedArg (Pattern' a))
goArg IsForced
Forced Arg Term
v = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a name. a -> Named name a
unnamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Term -> Pattern' a
dotP) Arg Term
v
goArg IsForced
NotForced Arg Term
v = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a name. a -> Named name a
unnamed 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 (Modality -> Term -> t (t m) (Pattern' a)
go forall a b. (a -> b) -> a -> b
$ Modality -> Modality -> Modality
composeModality Modality
md forall a b. (a -> b) -> a -> b
$ forall a. LensModality a => a -> Modality
getModality Arg Term
v) Arg Term
v
([NamedArg (Pattern' a)]
ps, IntMap Modality
bound) <- forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM IsForced -> Arg Term -> t (t m) (NamedArg (Pattern' a))
goArg ([IsForced]
fs forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat IsForced
NotForced) [Arg Term]
vs
if forall a. IntMap a -> Bool
IntMap.null IntMap Modality
bound
then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
else do
let cpi :: ConPatternInfo
cpi = (ConInfo -> ConPatternInfo
toConPatternInfo ConInfo
ci) { conPLazy :: Bool
conPLazy = Bool
True }
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
ConP ConHead
c ConPatternInfo
cpi forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted) [NamedArg (Pattern' a)]
ps
| Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
Var Int
_ (Elim
_:Elims
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
Lam{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
Pi{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
Def{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
MetaV{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
Sort{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
Level{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
DontCare{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
Dummy{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Term -> Pattern' a
dotP Term
v
Lit{} -> forall a. HasCallStack => a
__IMPOSSIBLE__