{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.TypeChecking.Rules.LHS.Unify.Types where
import Prelude hiding (null)
import Control.Monad
import Control.Monad.Writer (WriterT(..), MonadWriter(..))
import Data.Foldable (toList)
import Data.DList (DList)
import qualified Data.List as List
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
data Equality = Equal
{ Equality -> Dom' Term Type
_eqType :: Dom Type
, Equality -> Term
_eqLeft :: Term
, Equality -> Term
_eqRight :: Term
}
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 (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
u m (Term -> Equality) -> m Term -> m Equality
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v
eqUnLevel :: (HasBuiltins m, HasOptions m) => Equality -> m Equality
eqUnLevel :: forall (m :: * -> *).
(HasBuiltins m, HasOptions 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 (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
u m (Term -> Equality) -> m Term -> m Equality
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel Term
v
where
unLevel :: Term -> m Term
unLevel (Level Level
l) = Level -> m Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l
unLevel Term
u = Term -> m Term
forall a. a -> m a
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
(Int -> UnifyState -> ShowS)
-> (UnifyState -> String)
-> ([UnifyState] -> ShowS)
-> Show UnifyState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnifyState -> ShowS
showsPrec :: Int -> UnifyState -> ShowS
$cshow :: UnifyState -> String
show :: UnifyState -> String
$cshowList :: [UnifyState] -> ShowS
showList :: [UnifyState] -> ShowS
Show)
lensVarTel :: Lens' UnifyState Telescope
lensVarTel :: Lens' UnifyState Telescope
lensVarTel Telescope -> f Telescope
f UnifyState
s = Telescope -> f Telescope
f (UnifyState -> Telescope
varTel UnifyState
s) f Telescope -> (Telescope -> UnifyState) -> f UnifyState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Telescope
tel -> UnifyState
s { varTel = tel }
{-# INLINE lensVarTel #-}
lensEqTel :: Lens' UnifyState Telescope
lensEqTel :: Lens' UnifyState Telescope
lensEqTel Telescope -> f Telescope
f UnifyState
s = Telescope -> f Telescope
f (UnifyState -> Telescope
eqTel UnifyState
s) f Telescope -> (Telescope -> UnifyState) -> f UnifyState
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Telescope
x -> UnifyState
s { eqTel = x }
{-# INLINE lensEqTel #-}
instance Reduce UnifyState where
reduce' :: UnifyState -> ReduceM UnifyState
reduce' = UnifyState -> ReduceM UnifyState
forall a. HasCallStack => a
__IMPOSSIBLE__
instance PrettyTCM UnifyState where
prettyTCM :: forall (m :: * -> *). MonadPretty m => UnifyState -> m Doc
prettyTCM UnifyState
state = m Doc
"UnifyState" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"variable tel: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
gamma
, m Doc
"flexible vars: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [(Int, IsForced)] -> m Doc
forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
pshow ((FlexibleVar Int -> (Int, IsForced))
-> FlexibleVars -> [(Int, IsForced)]
forall a b. (a -> b) -> [a] -> [b]
map FlexibleVar Int -> (Int, IsForced)
forall {a}. FlexibleVar a -> (a, IsForced)
flexVarF (FlexibleVars -> [(Int, IsForced)])
-> FlexibleVars -> [(Int, IsForced)]
forall a b. (a -> b) -> a -> b
$ UnifyState -> FlexibleVars
flexVars UnifyState
state)
, m Doc
"equation tel: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma (Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
delta)
, m Doc
"equations: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
gamma ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> Arg Term -> m Doc)
-> [Arg Term] -> [Arg Term] -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Arg Term -> m Doc
forall {m :: * -> *} {a} {a}.
(MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM 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 = (FlexibleVar a -> a
forall a. FlexibleVar a -> a
flexVar FlexibleVar a
fi, FlexibleVar a -> IsForced
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 = a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
x m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"=?=" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). 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
(tel, a, lhs, rhs) <- (Telescope, Type, [Arg Term], [Arg Term])
-> m (Telescope, Type, [Arg Term], [Arg Term])
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Telescope
tel, Type
a, [Arg Term]
lhs, [Arg Term]
rhs)
let n = [Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
lhs
unless (n == size rhs) __IMPOSSIBLE__
TelV eqTel _ <- telView a
unless (n == size eqTel) __IMPOSSIBLE__
return $ UState tel flex eqTel lhs rhs
isUnifyStateSolved :: UnifyState -> Bool
isUnifyStateSolved :: UnifyState -> Bool
isUnifyStateSolved = Telescope -> Bool
forall a. Null a => a -> Bool
null (Telescope -> Bool)
-> (UnifyState -> Telescope) -> UnifyState -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnifyState -> Telescope
eqTel
varCount :: UnifyState -> Int
varCount :: UnifyState -> Int
varCount = Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int)
-> (UnifyState -> Telescope) -> UnifyState -> Int
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 = Dom' Term Type -> [Dom' Term Type] -> Int -> Dom' Term Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom' Term Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom' Term Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel (Telescope -> [Dom' Term Type]) -> Telescope -> [Dom' Term Type]
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 = (String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type)
-> Dom' Term (String, Type) -> Dom' Term Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (String, Type)
-> [Dom' Term (String, Type)] -> Int -> Dom' Term (String, Type)
forall a. a -> [a] -> Int -> a
indexWithDefault Dom' Term (String, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Telescope -> [Dom' Term (String, Type)])
-> Telescope -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
varTel UnifyState
s) Int
i
eqCount :: UnifyState -> Int
eqCount :: UnifyState -> Int
eqCount = Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int)
-> (UnifyState -> Telescope) -> UnifyState -> Int
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 (Dom' Term Type -> [Dom' Term Type] -> Int -> Dom' Term Type
forall a. a -> [a] -> Int -> a
indexWithDefault Dom' Term Type
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom' Term Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
eqs) Int
k)
(Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Arg Term] -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Int
k)
(Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Arg Term] -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
rhs Int
k)
getReducedEquality
:: (MonadReduce m, MonadAddContext m)
=> Int -> UnifyState -> m Equality
getReducedEquality :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEquality Int
k UnifyState
s = do
let Equal Dom' Term Type
a Term
u Term
v = Int -> UnifyState -> Equality
getEquality Int
k UnifyState
s
Telescope -> m Equality -> m Equality
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (m Equality -> m Equality) -> m Equality -> m Equality
forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> Term -> Term -> Equality
Equal
(Dom' Term Type -> Term -> Term -> Equality)
-> m (Dom' Term Type) -> m (Term -> Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m (Dom' Term Type) -> m (Dom' Term Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
eqTel UnifyState
s) (Dom' Term Type -> m (Dom' Term Type)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Dom' Term Type
a)
m (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
m (Term -> Equality) -> m Term -> m Equality
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
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 ((String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type)
-> Dom' Term (String, Type) -> Dom' Term Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term (String, Type)
-> [Dom' Term (String, Type)] -> Int -> Dom' Term (String, Type)
forall a. a -> [a] -> Int -> a
indexWithDefault Dom' Term (String, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
eqs) Int
k)
(Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Arg Term] -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
lhs Int
k)
(Arg Term -> Term
forall e. Arg e -> e
unArg (Arg Term -> Term) -> Arg Term -> Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> [Arg Term] -> Int -> Arg Term
forall a. a -> [a] -> Int -> a
indexWithDefault Arg Term
forall a. HasCallStack => a
__IMPOSSIBLE__ [Arg Term]
rhs Int
k)
getReducedEqualityUnraised
:: (MonadReduce m, MonadAddContext m)
=> Int -> UnifyState -> m Equality
getReducedEqualityUnraised :: forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> UnifyState -> m Equality
getReducedEqualityUnraised Int
k UnifyState
s = do
let Equal Dom' Term Type
a Term
u Term
v = Int -> UnifyState -> Equality
getEqualityUnraised Int
k UnifyState
s
Telescope -> m Equality -> m Equality
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext (UnifyState -> Telescope
varTel UnifyState
s) (m Equality -> m Equality) -> m Equality -> m Equality
forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> Term -> Term -> Equality
Equal
(Dom' Term Type -> Term -> Term -> Equality)
-> m (Dom' Term Type) -> m (Term -> Term -> Equality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m (Dom' Term Type) -> m (Dom' Term Type)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext ([Dom' Term (String, Type)] -> Telescope
telFromList ([Dom' Term (String, Type)] -> Telescope)
-> [Dom' Term (String, Type)] -> Telescope
forall a b. (a -> b) -> a -> b
$ Int -> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
forall a. Int -> [a] -> [a]
take Int
k ([Dom' Term (String, Type)] -> [Dom' Term (String, Type)])
-> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList (Telescope -> [Dom' Term (String, Type)])
-> Telescope -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s) (Dom' Term Type -> m (Dom' Term Type)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Dom' Term Type
a)
m (Term -> Term -> Equality) -> m Term -> m (Term -> Equality)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
m (Term -> Equality) -> m Term -> m Equality
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
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 -> Maybe (UnifyState, PatternSubstitution)
forall a. Maybe a
Nothing
Just (Telescope
tel' , PatternSubstitution
sigma , Permutation
rho) -> (UnifyState, PatternSubstitution)
-> Maybe (UnifyState, PatternSubstitution)
forall a. a -> Maybe a
Just ((UnifyState, PatternSubstitution)
-> Maybe (UnifyState, PatternSubstitution))
-> (UnifyState, PatternSubstitution)
-> Maybe (UnifyState, PatternSubstitution)
forall a b. (a -> b) -> a -> b
$ (,PatternSubstitution
sigma) (UnifyState -> (UnifyState, PatternSubstitution))
-> UnifyState -> (UnifyState, PatternSubstitution)
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) (FlexibleVars -> FlexibleVars) -> FlexibleVars -> FlexibleVars
forall a b. (a -> b) -> a -> b
$ UnifyState -> FlexibleVars
flexVars UnifyState
s
, eqTel :: Telescope
eqTel = PatternSubstitution -> Telescope -> Telescope
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ UnifyState -> Telescope
eqTel UnifyState
s
, eqLHS :: [Arg Term]
eqLHS = PatternSubstitution -> [Arg Term] -> [Arg Term]
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ UnifyState -> [Arg Term]
eqLHS UnifyState
s
, eqRHS :: [Arg Term]
eqRHS = PatternSubstitution -> [Arg Term] -> [Arg Term]
forall a. TermSubst a => PatternSubstitution -> a -> a
applyPatSubst PatternSubstitution
sigma ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
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 =
(FlexibleVar Int -> Maybe (FlexibleVar Int))
-> FlexibleVars -> FlexibleVars
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((FlexibleVar Int -> Maybe (FlexibleVar Int))
-> FlexibleVars -> FlexibleVars)
-> (FlexibleVar Int -> Maybe (FlexibleVar Int))
-> FlexibleVars
-> FlexibleVars
forall a b. (a -> b) -> a -> b
$ \(FlexibleVar ArgInfo
ai IsForced
fc FlexibleVarKind
k Maybe Int
p Int
x) ->
ArgInfo
-> IsForced
-> FlexibleVarKind
-> Maybe Int
-> Int
-> FlexibleVar Int
forall a.
ArgInfo
-> IsForced -> FlexibleVarKind -> Maybe Int -> a -> FlexibleVar a
FlexibleVar ArgInfo
ai IsForced
fc FlexibleVarKind
k Maybe Int
p (Int -> FlexibleVar Int) -> Maybe Int -> Maybe (FlexibleVar Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Int] -> Maybe Int
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
| Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Telescope
tel Telescope -> Term -> Telescope
forall t. Apply t => t -> Term -> t
`apply1` Term
u
| Bool
otherwise = case Telescope
tel of
Telescope
EmptyTel -> Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
ExtendTel Dom' Term Type
a Abs Telescope
tel' -> Dom' Term Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
a (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$
String -> Telescope -> Abs Telescope
forall a. String -> a -> Abs a
Abs (Abs Telescope -> String
forall a. Abs a -> String
absName Abs Telescope
tel') (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> Term -> Telescope
applyUnder (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Abs Telescope -> Telescope
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
_ [] = [a]
forall a. HasCallStack => a
__IMPOSSIBLE__
dropAt Int
k (a
x:[a]
xs)
| Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = [a]
forall a. HasCallStack => a
__IMPOSSIBLE__
| Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = [a]
xs
| Bool
otherwise = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
dropAt (Int
kInt -> Int -> Int
forall 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) (UnifyState -> (UnifyState, PatternSubstitution))
-> UnifyState -> (UnifyState, PatternSubstitution)
forall a b. (a -> b) -> a -> b
$ UnifyState
s
{ eqTel = applyUnder k (eqTel s) u'
, eqLHS = dropAt k $ eqLHS s
, eqRHS = dropAt k $ eqRHS s
}
where
u' :: Term
u' = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
k Term
u
n :: Int
n = UnifyState -> Int
eqCount UnifyState
s
sigma :: PatternSubstitution
sigma = Int -> PatternSubstitution -> PatternSubstitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (PatternSubstitution -> PatternSubstitution)
-> PatternSubstitution -> PatternSubstitution
forall a b. (a -> b) -> a -> b
$ Pattern' DBPatVar -> PatternSubstitution -> PatternSubstitution
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (Term -> Pattern' DBPatVar
forall a. Term -> Pattern' a
dotP Term
u') PatternSubstitution
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
, UnifyStep -> Either () ()
solutionSide :: Either () ()
}
| 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
(Int -> UnifyStep -> ShowS)
-> (UnifyStep -> String)
-> ([UnifyStep] -> ShowS)
-> Show UnifyStep
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnifyStep -> ShowS
showsPrec :: Int -> UnifyStep -> ShowS
$cshow :: UnifyStep -> String
show :: UnifyStep -> String
$cshowList :: [UnifyStep] -> ShowS
showList :: [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" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, m Doc
"lhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
, m Doc
"rhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
])
Solution Int
k Dom' Term Type
a FlexibleVar Int
i Term
u Either () ()
s -> m Doc
"Solution" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom' Term Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom' Term Type -> m Doc
prettyTCM Dom' Term Type
a
, m Doc
"variable: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ((Int, Maybe Int, IsForced, FlexibleVarKind) -> String
forall a. Show a => a -> String
show (FlexibleVar Int -> Int
forall a. FlexibleVar a -> a
flexVar FlexibleVar Int
i, FlexibleVar Int -> Maybe Int
forall a. FlexibleVar a -> Maybe Int
flexPos FlexibleVar Int
i, FlexibleVar Int -> IsForced
forall a. FlexibleVar a -> IsForced
flexForced FlexibleVar Int
i, FlexibleVar Int -> FlexibleVarKind
forall a. FlexibleVar a -> FlexibleVarKind
flexKind FlexibleVar Int
i))
, m Doc
"term: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
, m Doc
"side: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Either () () -> String
forall a. Show a => a -> String
show Either () ()
s)
])
Injectivity Int
k Type
a QName
d [Arg Term]
pars [Arg Term]
ixs ConHead
c -> m Doc
"Injectivity" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, m Doc
"datatype: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
, m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
pars)
, m Doc
"indices: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
ixs)
, m Doc
"constructor:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
])
Conflict Int
k Type
a QName
d [Arg Term]
pars Term
u Term
v -> m Doc
"Conflict" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, m Doc
"datatype: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
, m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
pars)
, m Doc
"lhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
, m Doc
"rhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
])
Cycle Int
k Type
a QName
d [Arg Term]
pars Int
i Term
u -> m Doc
"Cycle" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, m Doc
"datatype: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
, m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
pars)
, m Doc
"variable: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
i)
, m Doc
"term: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
])
EtaExpandVar FlexibleVar Int
fi QName
r [Arg Term]
pars -> m Doc
"EtaExpandVar" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"variable: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (FlexibleVar Int -> String
forall a. Show a => a -> String
show FlexibleVar Int
fi)
, m Doc
"record type:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r
, m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
pars
])
EtaExpandEquation Int
k QName
r [Arg Term]
pars -> m Doc
"EtaExpandEquation" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
, m Doc
"record type:" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
r
, m Doc
"parameters: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
pars
])
LitConflict Int
k Type
a Literal
u Literal
v -> m Doc
"LitConflict" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
, m Doc
"type: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, m Doc
"lhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Literal -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Literal -> m Doc
prettyTCM Literal
u
, m Doc
"rhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Literal -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Literal -> m Doc
prettyTCM Literal
v
])
StripSizeSuc Int
k Term
u Term
v -> m Doc
"StripSizeSuc" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
, m Doc
"lhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
, m Doc
"rhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
])
SkipIrrelevantEquation Int
k -> m Doc
"SkipIrrelevantEquation" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
])
TypeConInjectivity Int
k QName
d [Arg Term]
us [Arg Term]
vs -> m Doc
"TypeConInjectivity" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"position: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show Int
k)
, m Doc
"datatype: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d
, m Doc
"lhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
us)
, m Doc
"rhs: " m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg Term -> m Doc) -> [Arg Term] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
vs)
])
data UnifyLogEntry
= UnificationStep UnifyState UnifyStep UnifyOutput
type UnifyLog = [(UnifyLogEntry,UnifyState)]
type UnifyLog' = DList (UnifyLogEntry, UnifyState)
data UnifyOutput = UnifyOutput
{ UnifyOutput -> PatternSubstitution
unifySubst :: PatternSubstitution
, UnifyOutput -> PatternSubstitution
unifyProof :: PatternSubstitution
}
instance Semigroup UnifyOutput where
UnifyOutput
x <> :: UnifyOutput -> UnifyOutput -> UnifyOutput
<> UnifyOutput
y = UnifyOutput
{ unifySubst :: PatternSubstitution
unifySubst = UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
y PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` UnifyOutput -> PatternSubstitution
unifySubst UnifyOutput
x
, unifyProof :: PatternSubstitution
unifyProof = UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
y PatternSubstitution -> PatternSubstitution -> PatternSubstitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` UnifyOutput -> PatternSubstitution
unifyProof UnifyOutput
x
}
instance Monoid UnifyOutput where
mempty :: UnifyOutput
mempty = PatternSubstitution -> PatternSubstitution -> UnifyOutput
UnifyOutput PatternSubstitution
forall a. Substitution' a
IdS PatternSubstitution
forall a. Substitution' a
IdS
mappend :: UnifyOutput -> UnifyOutput -> UnifyOutput
mappend = UnifyOutput -> UnifyOutput -> UnifyOutput
forall a. Semigroup a => a -> a -> a
(<>)
type UnifyLogT m a = WriterT UnifyLog' m a
type UnifyStepT m a = WriterT UnifyOutput m a
tellUnifySubst :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()
tellUnifySubst :: forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifySubst PatternSubstitution
sub = UnifyOutput -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (UnifyOutput -> m ()) -> UnifyOutput -> m ()
forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> PatternSubstitution -> UnifyOutput
UnifyOutput PatternSubstitution
sub PatternSubstitution
forall a. Substitution' a
IdS
tellUnifyProof :: MonadWriter UnifyOutput m => PatternSubstitution -> m ()
tellUnifyProof :: forall (m :: * -> *).
MonadWriter UnifyOutput m =>
PatternSubstitution -> m ()
tellUnifyProof PatternSubstitution
sub = UnifyOutput -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (UnifyOutput -> m ()) -> UnifyOutput -> m ()
forall a b. (a -> b) -> a -> b
$ PatternSubstitution -> PatternSubstitution -> UnifyOutput
UnifyOutput PatternSubstitution
forall a. Substitution' a
IdS PatternSubstitution
sub
writeUnifyLog ::
MonadWriter UnifyLog' m => (UnifyLogEntry, UnifyState) -> m ()
writeUnifyLog :: forall (m :: * -> *).
MonadWriter UnifyLog' m =>
(UnifyLogEntry, UnifyState) -> m ()
writeUnifyLog (UnifyLogEntry, UnifyState)
x = UnifyLog' -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ((UnifyLogEntry, UnifyState) -> UnifyLog'
forall el coll. Singleton el coll => el -> coll
singleton (UnifyLogEntry, UnifyState)
x)
runUnifyLogT :: Functor m => UnifyLogT m a -> m (a, UnifyLog)
runUnifyLogT :: forall (m :: * -> *) a.
Functor m =>
UnifyLogT m a -> m (a, UnifyLog)
runUnifyLogT UnifyLogT m a
m = (UnifyLog' -> UnifyLog) -> (a, UnifyLog') -> (a, UnifyLog)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd UnifyLog' -> UnifyLog
forall a. DList a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ((a, UnifyLog') -> (a, UnifyLog))
-> m (a, UnifyLog') -> m (a, UnifyLog)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UnifyLogT m a -> m (a, UnifyLog')
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT UnifyLogT m a
m