{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
#if __GLASGOW_HASKELL__ >= 810
{-# OPTIONS_GHC -fmax-pmcheck-models=390 #-}
#endif
module Agda.TypeChecking.Conversion where
import Control.Arrow (second)
import Control.Monad
import Control.Monad.Except
import Control.Monad.Fail (MonadFail)
import Data.Function (on)
import Data.Semigroup ((<>))
import Data.IntMap (IntMap)
import qualified Data.List as List
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import qualified Data.Set as Set
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Translation.InternalToAbstract (reify)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.MetaVars.Occurs (killArgs,PruneResult(..),rigidVarsNotContainedIn)
import Agda.TypeChecking.Names
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import qualified Agda.TypeChecking.SyntacticEquality as SynEq
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion.Pure (pureCompareAs, runPureConversion)
import Agda.TypeChecking.Forcing (isForced, nextIsForced)
import Agda.TypeChecking.Free
import Agda.TypeChecking.Datatypes (getConType, getFullyAppliedConType)
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.Level
import Agda.TypeChecking.Implicit (implicitArgs)
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.ProjectionLike
import Agda.TypeChecking.Warnings (MonadWarning)
import Agda.Interaction.Options
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Monad
import Agda.Utils.Maybe
import Agda.Utils.Permutation
import Agda.Syntax.Common.Pretty (prettyShow)
import qualified Agda.Utils.ProfileOptions as Profile
import Agda.Utils.BoolSet (BoolSet)
import qualified Agda.Utils.BoolSet as BoolSet
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Unsafe ( unsafeComparePointers )
import Agda.Utils.Impossible
type MonadConversion m =
( PureTCM m
, MonadConstraint m
, MonadMetaSolver m
, MonadError TCErr m
, MonadWarning m
, MonadStatistics m
, MonadFresh ProblemId m
, MonadFresh Int m
, MonadFail m
)
tryConversion
:: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
=> m () -> m Bool
tryConversion :: forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> (m () -> m (Maybe ())) -> m () -> m Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> m () -> m (Maybe ())
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m (Maybe a)
tryConversion'
tryConversion'
:: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
=> m a -> m (Maybe a)
tryConversion' :: forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m (Maybe a)
tryConversion' m a
m = m a -> m (Maybe a)
forall e (m :: * -> *) a.
(MonadError e m, Functor m) =>
m a -> m (Maybe a)
tryMaybe (m a -> m (Maybe a)) -> m a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ m a -> m a
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints m a
m
sameVars :: Elims -> Elims -> Bool
sameVars :: Elims -> Elims -> Bool
sameVars Elims
xs Elims
ys = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> Elim' Term -> Bool) -> Elims -> Elims -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Elim' Term -> Elim' Term -> Bool
same Elims
xs Elims
ys
where
same :: Elim' Term -> Elim' Term -> Bool
same (Apply (Arg ArgInfo
_ (Var Int
n []))) (Apply (Arg ArgInfo
_ (Var Int
m []))) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m
same Elim' Term
_ Elim' Term
_ = Bool
False
intersectVars :: Elims -> Elims -> Maybe [Bool]
intersectVars :: Elims -> Elims -> Maybe [Bool]
intersectVars = (Elim' Term -> Elim' Term -> Maybe Bool)
-> Elims -> Elims -> Maybe [Bool]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Elim' Term -> Elim' Term -> Maybe Bool
areVars where
areVars :: Elim' Term -> Elim' Term -> Maybe Bool
areVars (Apply Arg Term
u) Elim' Term
v | Arg Term -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant Arg Term
u = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
areVars (Apply (Arg ArgInfo
_ (Var Int
n []))) (Apply (Arg ArgInfo
_ (Var Int
m []))) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
m
areVars Elim' Term
_ Elim' Term
_ = Maybe Bool
forall a. Maybe a
Nothing
guardPointerEquality :: MonadConversion m => a -> a -> String -> m () -> m ()
guardPointerEquality :: forall (m :: * -> *) a.
MonadConversion m =>
a -> a -> String -> m () -> m ()
guardPointerEquality a
u a
v String
profileSection m ()
action =
if a -> a -> Bool
forall a. a -> a -> Bool
unsafeComparePointers a
u a
v
then ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
profileSection
else m ()
action
{-# SPECIALIZE equalTerm :: Type -> Term -> Term -> TCM () #-}
equalTerm :: MonadConversion m => Type -> Term -> Term -> m ()
equalTerm :: forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm = Comparison -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareTerm Comparison
CmpEq
{-# SPECIALIZE equalAtom :: CompareAs -> Term -> Term -> TCM () #-}
equalAtom :: MonadConversion m => CompareAs -> Term -> Term -> m ()
equalAtom :: forall (m :: * -> *).
MonadConversion m =>
CompareAs -> Term -> Term -> m ()
equalAtom = Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom Comparison
CmpEq
{-# SPECIALIZE equalType :: Type -> Type -> TCM () #-}
equalType :: MonadConversion m => Type -> Type -> m ()
equalType :: forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
equalType = Comparison -> Type -> Type -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
CmpEq
convError :: TypeError -> TCM ()
convError :: TypeError -> TCM ()
convError TypeError
err =
TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
(==) Relevance
Irrelevant (Relevance -> Bool) -> TCMT IO Relevance -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv Relevance -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
Lens' TCEnv Relevance
eRelevance)
(() -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
(TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
err)
compareTerm :: forall m. MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
compareTerm :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareTerm Comparison
cmp Type
a Term
u Term
v = Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAs Comparison
cmp (Type -> CompareAs
AsTermsOf Type
a) Term
u Term
v
{-# SPECIALIZE compareAs :: Comparison -> CompareAs -> Term -> Term -> TCM () #-}
compareAs :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m ()
compareAs :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAs Comparison
cmp CompareAs
a Term
u Term
v = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.term" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"compareTerm"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Comparison -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ CompareAs -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CompareAs -> m Doc
prettyTCM CompareAs
a
]
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare"
Term -> Term -> String -> m () -> m ()
forall (m :: * -> *) a.
MonadConversion m =>
a -> a -> String -> m () -> m ()
guardPointerEquality Term
u Term
v String
"pointer equality: terms" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Term
-> Term -> (Term -> Term -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
SynEq.checkSyntacticEquality Term
u Term
v
(\Term
_ Term
_ -> ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare equal") ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$
\Term
u Term
v -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.term" Int
15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"compareTerm (not syntactically equal)"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Comparison -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ CompareAs -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CompareAs -> m Doc
prettyTCM CompareAs
a
]
let fallback :: m ()
fallback = Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAs' Comparison
cmp CompareAs
a Term
u Term
v
unlessSubtyping :: m () -> m ()
unlessSubtyping :: m () -> m ()
unlessSubtyping m ()
cont =
if Comparison
cmp Comparison -> Comparison -> Bool
forall a. Eq a => a -> a -> Bool
== Comparison
CmpEq then m ()
cont else do
CompareAs
-> (Blocker -> CompareAs -> m ())
-> (NotBlocked -> CompareAs -> m ())
-> m ()
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked CompareAs
a (\ Blocker
_ CompareAs
_ -> m ()
fallback) ((NotBlocked -> CompareAs -> m ()) -> m ())
-> (NotBlocked -> CompareAs -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ CompareAs
a -> do
m (Maybe BoundedSize) -> m () -> (BoundedSize -> m ()) -> m ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (CompareAs -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
CompareAs -> m (Maybe BoundedSize)
isSizeType CompareAs
a) m ()
cont (\ BoundedSize
_ -> m ()
fallback)
dir :: CompareDirection
dir = Comparison -> CompareDirection
fromCmp Comparison
cmp
rid :: CompareDirection
rid = CompareDirection -> CompareDirection
flipCmp CompareDirection
dir
case (Term
u, Term
v) of
(MetaV MetaId
x Elims
us, MetaV MetaId
y Elims
vs)
| MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
/= MetaId
y -> m () -> m ()
unlessSubtyping (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m ()
solve1 m () -> m () -> m ()
`orelse` m ()
solve2 m () -> m () -> m ()
`orelse` m ()
fallback
| Bool
otherwise -> m ()
fallback
where
(m ()
solve1, m ()
solve2) | MetaId
x MetaId -> MetaId -> Bool
forall a. Ord a => a -> a -> Bool
> MetaId
y = (CompareDirection -> MetaId -> Elims -> Term -> m ()
assign CompareDirection
dir MetaId
x Elims
us Term
v, CompareDirection -> MetaId -> Elims -> Term -> m ()
assign CompareDirection
rid MetaId
y Elims
vs Term
u)
| Bool
otherwise = (CompareDirection -> MetaId -> Elims -> Term -> m ()
assign CompareDirection
rid MetaId
y Elims
vs Term
u, CompareDirection -> MetaId -> Elims -> Term -> m ()
assign CompareDirection
dir MetaId
x Elims
us Term
v)
(MetaV MetaId
x Elims
us, Term
_) -> m () -> m ()
unlessSubtyping (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> MetaId -> Elims -> Term -> m ()
assign CompareDirection
dir MetaId
x Elims
us Term
v m () -> m () -> m ()
`orelse` m ()
fallback
(Term
_, MetaV MetaId
y Elims
vs) -> m () -> m ()
unlessSubtyping (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> MetaId -> Elims -> Term -> m ()
assign CompareDirection
rid MetaId
y Elims
vs Term
u m () -> m () -> m ()
`orelse` m ()
fallback
(Def QName
f Elims
es, Def QName
f' Elims
es') | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> do
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
opts <- pragmaOptions
let shortcut = case Definition -> Defn
theDef Definition
def of
Defn
_ | PragmaOptions -> Bool
optFirstOrder PragmaOptions
opts -> Bool
True
d :: Defn
d@Function{}
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
optRequireUniqueMetaSolutions PragmaOptions
opts -> Defn
d Defn -> Lens' Defn Bool -> Bool
forall o i. o -> Lens' o i -> i
^. (Bool -> f Bool) -> Defn -> f Defn
Lens' Defn Bool
funFirstOrder
Defn
_ -> Bool
False
if not shortcut then fallback else unlessSubtyping $ do
cubicalProjs <- traverse getName' [builtin_unglue, builtin_unglueU]
let
notFirstOrder = Maybe Projection -> Bool
forall a. Maybe a -> Bool
isJust (Definition -> Maybe Projection
isRelevantProjection_ Definition
def)
Bool -> Bool -> Bool
|| (QName -> Maybe QName
forall a. a -> Maybe a
Just QName
f) Maybe QName -> [Maybe QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName]
cubicalProjs
if notFirstOrder then fallback else do
pol <- getPolarity' cmp f
whenProfile Profile.Conversion $ tick "compare first-order shortcut"
compareElims pol [] (defType def) (Def f []) es es' `orelse` fallback
(Term, Term)
_ -> m ()
fallback
where
assign :: CompareDirection -> MetaId -> Elims -> Term -> m ()
assign :: CompareDirection -> MetaId -> Elims -> Term -> m ()
assign CompareDirection
dir MetaId
x Elims
es Term
v = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.term.shortcut" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"attempting shortcut"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
]
m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isInstantiatedMeta MetaId
x) (Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock)
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare meta shortcut"
CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
forall (m :: * -> *).
MonadConversion m =>
CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
assignE CompareDirection
dir MetaId
x Elims
es Term
v CompareAs
a ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
CompareDirection -> CompareAs -> Term -> Term -> m ()
compareAsDir CompareDirection
dir CompareAs
a
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.term.shortcut" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"shortcut successful" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc
"result:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es)))
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare meta shortcut successful"
orelse :: m () -> m () -> m ()
orelse :: m () -> m () -> m ()
orelse m ()
m m ()
h = m () -> (TCErr -> m ()) -> m ()
forall a. m a -> (TCErr -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError m ()
m (\TCErr
_ -> m ()
h)
assignE :: (MonadConversion m)
=> CompareDirection -> MetaId -> Elims -> Term -> CompareAs -> (Term -> Term -> m ()) -> m ()
assignE :: forall (m :: * -> *).
MonadConversion m =>
CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
assignE CompareDirection
dir MetaId
x Elims
es Term
v CompareAs
a Term -> Term -> m ()
comp = do
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare meta"
case Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es of
Just [Arg Term]
vs -> CompareDirection
-> MetaId -> [Arg Term] -> Term -> CompareAs -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
CompareDirection
-> MetaId -> [Arg Term] -> Term -> CompareAs -> m ()
assignV CompareDirection
dir MetaId
x [Arg Term]
vs Term
v CompareAs
a
Maybe [Arg Term]
Nothing -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.assign" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"assigning to projected meta "
, MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ((Elim' Term -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim' Term -> m Doc
prettyTCM Elims
es) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String
":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CompareDirection -> String
forall a. Show a => a -> String
show CompareDirection
dir) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
]
[MetaClass] -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[MetaClass] -> MetaId -> m ()
etaExpandMeta [MetaClass
Records] MetaId
x
res <- MetaId -> m (Maybe Term)
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m (Maybe Term)
isInstantiatedMeta' MetaId
x
case res of
Just Term
u -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.assign" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"seems like eta expansion instantiated meta "
, MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String
":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CompareDirection -> String
forall a. Show a => a -> String
show CompareDirection
dir) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
]
let w :: Term
w = Term
u Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` Elims
es
Term -> Term -> m ()
comp Term
w Term
v
Maybe Term
Nothing -> do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.conv.assign" Int
30 String
"eta expansion did not instantiate meta"
Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> m ()) -> Blocker -> m ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
x
compareAsDir :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m ()
compareAsDir :: forall (m :: * -> *).
MonadConversion m =>
CompareDirection -> CompareAs -> Term -> Term -> m ()
compareAsDir CompareDirection
dir CompareAs
a = (Comparison -> Term -> Term -> m ())
-> CompareDirection -> Term -> Term -> m ()
forall a c.
(Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp (Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
`compareAs'` CompareAs
a) CompareDirection
dir
compareAs' :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m ()
compareAs' :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAs' Comparison
cmp CompareAs
tt Term
m Term
n = case CompareAs
tt of
AsTermsOf Type
a -> Comparison -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareTerm' Comparison
cmp Type
a Term
m Term
n
CompareAs
AsSizes -> Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
m Term
n
CompareAs
AsTypes -> Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom Comparison
cmp CompareAs
AsTypes Term
m Term
n
compareTerm' :: forall m. MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
compareTerm' :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareTerm' Comparison
cmp Type
a Term
m Term
n =
String -> Int -> String -> m () -> m ()
forall a. String -> Int -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.conv.term" Int
20 String
"compareTerm" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
(ba, a') <- Type -> m (Blocker, Type)
forall a (m :: * -> *).
(Reduce a, IsMeta a, MonadReduce m) =>
a -> m (Blocker, a)
reduceWithBlocker Type
a
(catchConstraint (ValueCmp cmp (AsTermsOf a') m n) :: m () -> m ()) $ blockOnError ba $ do
reportSDoc "tc.conv.term" 30 $ fsep
[ "compareTerm", prettyTCM m, prettyTCM cmp, prettyTCM n, ":", prettyTCM a' ]
propIrr <- isPropEnabled
isSize <- isJust <$> isSizeType a'
(bs, s) <- reduceWithBlocker $ getSort a'
mlvl <- getBuiltin' builtinLevel
reportSDoc "tc.conv.term" 40 $ fsep
[ "compareTerm", prettyTCM m, prettyTCM cmp, prettyTCM n, ":", prettyTCM a'
, "at sort", prettyTCM s]
reportSDoc "tc.conv.level" 60 $ nest 2 $ sep
[ "a' =" <+> pretty a'
, "mlvl =" <+> pretty mlvl
, text $ "(Just (unEl a') == mlvl) = " ++ show (Just (unEl a') == mlvl)
]
blockOnError bs $ case s of
Prop{} | Bool
propIrr -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
compareIrrelevant Type
a' Term
m Term
n
Sort
_ | Bool
isSize -> Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
m Term
n
Sort
_ -> case Type -> Term
forall t a. Type'' t a -> a
unEl Type
a' of
Term
a | Term -> Maybe Term
forall a. a -> Maybe a
Just Term
a Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Term
mlvl -> do
a <- Term -> m Level
forall (m :: * -> *). PureTCM m => Term -> m Level
levelView Term
m
b <- levelView n
equalLevel a b
a :: Term
a@Pi{} -> MonadConversion m => Sort -> Term -> Term -> Term -> m ()
Sort -> Term -> Term -> Term -> m ()
equalFun Sort
s Term
a Term
m Term
n
Lam ArgInfo
_ Abs Term
_ -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.term.sort" Int
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ TCMT IO Doc
"compareTerm", Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
m, Comparison -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
n, TCMT IO Doc
":", Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a'
, TCMT IO Doc
"at sort", Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s
]
m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Def QName
r Elims
es -> do
isrec <- QName -> m Bool
forall (m :: * -> *). HasConstInfo m => QName -> m Bool
isEtaRecord QName
r
if isrec
then do
whenProfile Profile.Conversion $ tick "compare at eta record"
sig <- getSignature
transp <- getPrimitiveName' builtinTrans
hcomp <- getPrimitiveName' builtinHComp
let
ps = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
isNeutral (NotBlocked NotBlocked' t
_ Con{}) = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isNeutral (NotBlocked NotBlocked' t
r (Def QName
q Elims
_)) = do
Bool -> Bool
not (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Bool
forall (m :: * -> *).
(HasConstInfo m, HasBuiltins m) =>
QName -> m Bool
usesCopatterns QName
q
isNeutral Blocked' t Term
_ = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
isCubicalPrimHead (NotBlocked NotBlocked
r (Def QName
q Elims
_))
| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
transp Bool -> Bool -> Bool
|| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
hcomp
= QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q
isCubicalPrimHead Blocked Term
_ = Maybe QName
forall a. Maybe a
Nothing
isMeta Blocked' t Term
b = case Blocked' t Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' t Term
b of
MetaV{} -> Bool
True
Term
_ -> Bool
False
reportSDoc "tc.conv.term" 30 $ prettyTCM a <+> "is eta record type"
m <- reduceB m
mNeutral <- isNeutral m
n <- reduceB n
nNeutral <- isNeutral n
let
h1 = Blocked Term -> Maybe QName
isCubicalPrimHead Blocked Term
m
h2 = Blocked Term -> Maybe QName
isCubicalPrimHead Blocked Term
n
mCub = Maybe QName -> Bool
forall a. Maybe a -> Bool
isJust (Blocked Term -> Maybe QName
isCubicalPrimHead Blocked Term
m)
nCub = Maybe QName -> Bool
forall a. Maybe a -> Bool
isJust (Blocked Term -> Maybe QName
isCubicalPrimHead Blocked Term
n)
when (mCub || nCub) $
reportSDoc "tc.conv.term.cubical" 30 $ vcat
[ ("m (" <> prettyTCM mNeutral <> ", " <> prettyTCM mCub <> ", " <> prettyTCM h1 <> "):")
, nest 2 (prettyTCM m)
, ("n (" <> prettyTCM nNeutral <> ", " <> prettyTCM nCub <> ", " <> prettyTCM h2 <> "):")
, nest 2 (prettyTCM n)
, "at type"
, nest 2 (prettyTCM a')
, "same head:" <+> prettyTCM (h1 == h2)
]
if | isMeta m || isMeta n -> do
whenProfile Profile.Conversion $ tick "compare at eta-record: meta"
compareAtom cmp (AsTermsOf a') (ignoreBlocking m) (ignoreBlocking n)
| mNeutral && nNeutral && (not (mCub && nCub) || h1 == h2) -> do
whenProfile Profile.Conversion $ tick "compare at eta-record: both neutral"
let profUnitEta = ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare at eta-record: both neutral at unit"
ifM (isSingletonRecordModuloRelevance r ps) profUnitEta $ do
compareAtom cmp (AsTermsOf a') (ignoreBlocking m) (ignoreBlocking n)
| otherwise -> do
whenProfile Profile.Conversion $ tick "compare at eta-record: eta-expanding"
(tel, m') <- etaExpandRecord r ps $ ignoreBlocking m
(_ , n') <- etaExpandRecord r ps $ ignoreBlocking n
c <- getRecordConstructor r
compareArgs (repeat $ polFromCmp cmp) [] (telePi_ tel __DUMMY_TYPE__) (Con c ConOSystem []) m' n'
else (do pathview <- pathView a'
equalPath pathview a' m n)
Term
_ -> Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom Comparison
cmp (Type -> CompareAs
AsTermsOf Type
a') Term
m Term
n
where
equalFun :: (MonadConversion m) => Sort -> Term -> Term -> Term -> m ()
equalFun :: MonadConversion m => Sort -> Term -> Term -> Term -> m ()
equalFun Sort
s a :: Term
a@(Pi Dom Type
dom Abs Type
b) Term
m Term
n | Dom Type -> Bool
forall t e. Dom' t e -> Bool
domIsFinite Dom Type
dom = do
mp <- (Term -> QName) -> Maybe Term -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> QName
getPrimName (Maybe Term -> Maybe QName) -> m (Maybe Term) -> m (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinIsOne
let asFn = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Dom Type -> Abs Type -> Term
Pi (Dom Type
dom { domIsFinite = False }) Abs Type
b)
case unEl $ unDom dom of
Def QName
q [Apply Arg Term
phi]
| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mp -> Comparison -> Term -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace Comparison
cmp (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
phi) Type
asFn Term
m Term
n
Term
_ -> MonadConversion m => Sort -> Term -> Term -> Term -> m ()
Sort -> Term -> Term -> Term -> m ()
equalFun Sort
s (Type -> Term
forall t a. Type'' t a -> a
unEl Type
asFn) Term
m Term
n
equalFun Sort
_ (Pi dom :: Dom Type
dom@Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info} Abs Type
b) Term
m Term
n = do
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare at function type"
let name :: String
name = [Suggestion] -> String
suggests [ Abs Type -> Suggestion
forall a. Suggest a => a -> Suggestion
Suggestion Abs Type
b , Term -> Suggestion
forall a. Suggest a => a -> Suggestion
Suggestion Term
m , Term -> Suggestion
forall a. Suggest a => a -> Suggestion
Suggestion Term
n ]
(String, Dom Type) -> m () -> m ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
name, Dom Type
dom) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareTerm Comparison
cmp (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) Term
m' Term
n'
where
(Term
m',Term
n') = Int -> (Term, Term) -> (Term, Term)
forall a. Subst a => Int -> a -> a
raise Int
1 (Term
m,Term
n) (Term, Term) -> [Arg Term] -> (Term, Term)
forall t. Apply t => t -> [Arg Term] -> t
`apply` [ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0]
equalFun Sort
_ Term
_ Term
_ Term
_ = m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
equalPath :: (MonadConversion m) => PathView -> Type -> Term -> Term -> m ()
equalPath :: MonadConversion m => PathView -> Type -> Term -> Term -> m ()
equalPath (PathType Sort
s QName
_ Arg Term
l Arg Term
a Arg Term
x Arg Term
y) Type
_ Term
m Term
n = do
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare at path type"
let name :: String
name = String
"i" :: String
interval <- m Term -> m Type
forall (m :: * -> *). Functor m => m Term -> m Type
el m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInterval
let (m',n') = raise 1 (m, n) `applyE` [IApply (raise 1 $ unArg x) (raise 1 $ unArg y) (var 0)]
addContext (name, defaultDom interval) $ compareTerm cmp (El (raise 1 s) $ raise 1 (unArg a) `apply` [argN $ var 0]) m' n'
equalPath OType{} Type
a' Term
m Term
n = Type -> Term -> Term -> m ()
cmpDef Type
a' Term
m Term
n
cmpDef :: Type -> Term -> Term -> m ()
cmpDef a' :: Type
a'@(El Sort
s Term
ty) Term
m Term
n = do
mI <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinInterval
mIsOne <- getBuiltinName' builtinIsOne
mGlue <- getPrimitiveName' builtinGlue
mHComp <- getPrimitiveName' builtinHComp
mSub <- getBuiltinName' builtinSub
mUnglueU <- getPrimitiveTerm' builtin_unglueU
mSubIn <- getBuiltin' builtinSubIn
case ty of
Def QName
q Elims
es | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mIsOne -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Def QName
q Elims
es | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mGlue, Just args :: [Arg Term]
args@(Arg Term
l:Arg Term
_:Arg Term
a:Arg Term
phi:[Arg Term]
_) <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
aty <- m Term -> m Term -> m Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (Term -> m Term
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
l) (Term -> m Term
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
unglue <- prim_unglue
let mkUnglue Term
m = Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
apply Term
unglue ([Arg Term] -> Term) -> [Arg Term] -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden) [Arg Term]
args [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++ [Term -> Arg Term
forall e. e -> Arg e
argN Term
m]
reportSDoc "conv.glue" 20 $ prettyTCM (aty,mkUnglue m,mkUnglue n)
compareTerm cmp aty (mkUnglue m) (mkUnglue n)
Def QName
q Elims
es | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mHComp, Just (Arg Term
sl:Arg Term
s:args :: [Arg Term]
args@[Arg Term
phi,Arg Term
u,Arg Term
u0]) <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
, Sort (Type Level
lvl) <- Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
s
, Just Term
unglueU <- Maybe Term
mUnglueU, Just Term
subIn <- Maybe Term
mSubIn
-> do
let l :: Term
l = Level -> Term
Level Level
lvl
ty <- m Term -> m Term -> m Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (Term -> m Term
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Term
l) (Term -> m Term
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u0)
let bA = Term
subIn Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
sl,Arg Term
s,Arg Term
phi,Arg Term
u0]
let mkUnglue Term
m = Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
apply Term
unglueU ([Arg Term] -> Term) -> [Arg Term] -> Term
forall a b. (a -> b) -> a -> b
$ [Term -> Arg Term
forall e. e -> Arg e
argH Term
l] [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++ (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden) [Arg Term
phi,Arg Term
u] [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++ [Term -> Arg Term
forall e. e -> Arg e
argH Term
bA,Term -> Arg Term
forall e. e -> Arg e
argN Term
m]
reportSDoc "conv.hcompU" 20 $ prettyTCM (ty,mkUnglue m,mkUnglue n)
compareTerm cmp ty (mkUnglue m) (mkUnglue n)
Def QName
q Elims
es | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mSub, Just args :: [Arg Term]
args@(Arg Term
l:Arg Term
a:[Arg Term]
_) <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
ty <- m Term -> m Term -> m Type
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (Term -> m Term
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
l) (Term -> m Term
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a)
out <- primSubOut
let mkOut Term
m = Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
apply Term
out ([Arg Term] -> Term) -> [Arg Term] -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map (Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden) [Arg Term]
args [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++ [Term -> Arg Term
forall e. e -> Arg e
argN Term
m]
compareTerm cmp ty (mkOut m) (mkOut n)
Def QName
q [] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mI -> Comparison -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareInterval Comparison
cmp Type
a' Term
m Term
n
Term
_ -> Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom Comparison
cmp (Type -> CompareAs
AsTermsOf Type
a') Term
m Term
n
compareAtomDir :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m ()
compareAtomDir :: forall (m :: * -> *).
MonadConversion m =>
CompareDirection -> CompareAs -> Term -> Term -> m ()
compareAtomDir CompareDirection
dir CompareAs
a = (Comparison -> Term -> Term -> m ())
-> CompareDirection -> Term -> Term -> m ()
forall a c.
(Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp (Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
`compareAtom` CompareAs
a) CompareDirection
dir
computeElimHeadType :: MonadConversion m => QName -> Elims -> Elims -> m Type
computeElimHeadType :: forall (m :: * -> *).
MonadConversion m =>
QName -> Elims -> Elims -> m Type
computeElimHeadType QName
f [] Elims
es' = QName -> Elims -> m Type
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> Elims -> m Type
computeDefType QName
f Elims
es'
computeElimHeadType QName
f Elims
es Elims
_ = QName -> Elims -> m Type
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> Elims -> m Type
computeDefType QName
f Elims
es
compareAtom :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom Comparison
cmp CompareAs
t Term
m Term
n =
String -> Int -> String -> m () -> m ()
forall a. String -> Int -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.conv.atom" Int
20 String
"compareAtom" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
(Constraint -> m () -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
cmp CompareAs
t Term
m Term
n) :: m () -> m ()) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.conv.atom.size" Int
50 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"compareAtom term size: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Term -> Int
forall a. TermSize a => a -> Int
termSize Term
m, Term -> Int
forall a. TermSize a => a -> Int
termSize Term
n)
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.atom" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"compareAtom" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Comparison -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp
, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
n
, CompareAs -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => CompareAs -> m Doc
prettyTCM CompareAs
t
]
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare by reduction"
currentMutuals <- m (Set QName)
-> (MutualId -> m (Set QName)) -> Maybe MutualId -> m (Set QName)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Set QName -> m (Set QName)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Set QName
forall a. Set a
Set.empty) (MutualBlock -> Set QName
mutualNames (MutualBlock -> Set QName)
-> (MutualId -> m MutualBlock) -> MutualId -> m (Set QName)
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MutualId -> m MutualBlock
forall (tcm :: * -> *).
ReadTCState tcm =>
MutualId -> tcm MutualBlock
lookupMutualBlock) (Maybe MutualId -> m (Set QName))
-> m (Maybe MutualId) -> m (Set QName)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Maybe MutualId) -> m (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock
(mb',nb') <- do
mb' <- etaExpandBlocked =<< reduceB m
nb' <- etaExpandBlocked =<< reduceB n
return (mb', nb')
let blocker = Blocker -> Blocker -> Blocker
unblockOnEither (Blocked Term -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Term
mb') (Blocked Term -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Term
nb')
reportSLn "tc.conv.atom.size" 50 $ "term size after reduce: " ++ show (termSize $ ignoreBlocking mb', termSize $ ignoreBlocking nb')
(mb'', nb'') <- case (ignoreBlocking mb', ignoreBlocking nb') of
(Lit Literal
_, Lit Literal
_) -> (Blocked Term, Blocked Term) -> m (Blocked Term, Blocked Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocked Term
mb', Blocked Term
nb')
(Term, Term)
_ -> (,) (Blocked Term -> Blocked Term -> (Blocked Term, Blocked Term))
-> m (Blocked Term)
-> m (Blocked Term -> (Blocked Term, Blocked Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> m Term) -> Blocked Term -> m (Blocked Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Blocked' Term a -> f (Blocked' Term b)
traverse Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Blocked Term
mb'
m (Blocked Term -> (Blocked Term, Blocked Term))
-> m (Blocked Term) -> m (Blocked Term, Blocked Term)
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) -> Blocked Term -> m (Blocked Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Blocked' Term a -> f (Blocked' Term b)
traverse Term -> m Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Blocked Term
nb'
mb <- traverse unLevel mb''
nb <- traverse unLevel nb''
cmpBlocked <- viewTC eCompareBlocked
let m = Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
mb
n = Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
nb
checkDefinitionalEquality = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Comparison -> CompareAs -> Term -> Term -> m Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Comparison -> CompareAs -> Term -> Term -> m Bool
pureCompareAs Comparison
CmpEq CompareAs
t Term
m Term
n) m ()
notEqual
notEqual = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
m Term
n CompareAs
t
dir = Comparison -> CompareDirection
fromCmp Comparison
cmp
rid = CompareDirection -> CompareDirection
flipCmp CompareDirection
dir
assign CompareDirection
dir MetaId
x Elims
es Term
v = CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
forall (m :: * -> *).
MonadConversion m =>
CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
assignE CompareDirection
dir MetaId
x Elims
es Term
v CompareAs
t ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
CompareDirection -> CompareAs -> Term -> Term -> m ()
compareAsDir CompareDirection
dir CompareAs
t
reportSDoc "tc.conv.atom" 30 $
"compareAtom" <+> fsep [ prettyTCM mb <+> prettyTCM cmp
, prettyTCM nb
, prettyTCM t
, prettyTCM blocker
]
reportSDoc "tc.conv.atom" 80 $
"compareAtom" <+> fsep [ pretty mb <+> prettyTCM cmp
, pretty nb
, ":" <+> pretty t ]
case (mb, nb) of
(Blocked Term, Blocked Term)
_ | MetaV MetaId
x Elims
xArgs <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
mb,
MetaV MetaId
y Elims
yArgs <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
nb ->
Comparison
-> CompareAs -> MetaId -> Elims -> MetaId -> Elims -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison
-> CompareAs -> MetaId -> Elims -> MetaId -> Elims -> m ()
compareMetas Comparison
cmp CompareAs
t MetaId
x Elims
xArgs MetaId
y Elims
yArgs
(Blocked Term, Blocked Term)
_ | MetaV MetaId
x Elims
es <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
mb -> CompareDirection -> MetaId -> Elims -> Term -> m ()
assign CompareDirection
dir MetaId
x Elims
es Term
n
(Blocked Term, Blocked Term)
_ | MetaV MetaId
x Elims
es <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
nb -> CompareDirection -> MetaId -> Elims -> Term -> m ()
assign CompareDirection
rid MetaId
x Elims
es Term
m
(Blocked{}, Blocked{}) | Bool -> Bool
not Bool
cmpBlocked -> m ()
checkDefinitionalEquality
(Blocked Blocker
b Term
_, Blocked Term
_) | Bool -> Bool
not Bool
cmpBlocked -> CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
useInjectivity (Comparison -> CompareDirection
fromCmp Comparison
cmp) Blocker
b CompareAs
t Term
m Term
n
(Blocked Term
_, Blocked Blocker
b Term
_) | Bool -> Bool
not Bool
cmpBlocked -> CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
CompareDirection -> Blocker -> CompareAs -> Term -> Term -> m ()
useInjectivity (CompareDirection -> CompareDirection
flipCmp (CompareDirection -> CompareDirection)
-> CompareDirection -> CompareDirection
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareDirection
fromCmp Comparison
cmp) Blocker
b CompareAs
t Term
n Term
m
(Blocked Term, Blocked Term)
bs -> do
Blocker -> m () -> m ()
forall (m :: * -> *) a. MonadError TCErr m => Blocker -> m a -> m a
blockOnError Blocker
blocker (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
case (Term
m, Term
n) of
(Pi{}, Pi{}) -> Term -> Term -> m ()
equalFun Term
m Term
n
(Sort Sort
s1, Sort Sort
s2) ->
m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions)
(Comparison -> Sort -> Sort -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
cmp Sort
s1 Sort
s2)
(Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s1 Sort
s2)
(Lit Literal
l1, Lit Literal
l2) | Literal
l1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l2 -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(Var Int
i Elims
es, Var Int
i' Elims
es') | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i' -> do
a <- Int -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
compareElims [] [] a (var i) es es'
(Def QName
f Elims
es, Def QName
f' Elims
es') -> do
m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (QName -> QName -> m Bool
forall (m :: * -> *). MonadConversion m => QName -> QName -> m Bool
bothAbsurd QName
f QName
f') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
if QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
f' then Comparison
-> CompareAs
-> Term
-> Term
-> QName
-> Elims
-> QName
-> Elims
-> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison
-> CompareAs
-> Term
-> Term
-> QName
-> Elims
-> QName
-> Elims
-> m ()
trySizeUniv Comparison
cmp CompareAs
t Term
m Term
n QName
f Elims
es QName
f' Elims
es' else do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Elims -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Elims
es Bool -> Bool -> Bool
&& Elims -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Elims
es') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (MonadConversion m => QName -> Elims -> Elims -> m Bool
QName -> Elims -> Elims -> m Bool
compareEtaPrims QName
f Elims
es Elims
es') (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
a <- QName -> Elims -> Elims -> m Type
forall (m :: * -> *).
MonadConversion m =>
QName -> Elims -> Elims -> m Type
computeElimHeadType QName
f Elims
es Elims
es'
pol <- getPolarity' cmp f
compareElims pol [] a (Def f []) es es'
(Con ConHead
x ConInfo
ci Elims
xArgs, Con ConHead
y ConInfo
_ Elims
yArgs)
| ConHead
x ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
y -> do
a' <- case CompareAs
t of
AsTermsOf Type
a -> ConHead -> Type -> m Type
forall {m :: * -> *}.
(MonadBlock m, PureTCM m) =>
ConHead -> Type -> m Type
conType ConHead
x Type
a
CompareAs
AsSizes -> m Type
forall a. HasCallStack => a
__IMPOSSIBLE__
CompareAs
AsTypes -> m Type
forall a. HasCallStack => a
__IMPOSSIBLE__
forcedArgs <- getForcedArgs $ conName x
compareElims (repeat $ polFromCmp cmp) forcedArgs a' (Con x ci []) xArgs yArgs
(Term, Term)
_ -> m ()
notEqual
where
compareEtaPrims :: MonadConversion m => QName -> Elims -> Elims -> m Bool
compareEtaPrims :: MonadConversion m => QName -> Elims -> Elims -> m Bool
compareEtaPrims QName
q Elims
es Elims
es' = do
munglue <- PrimitiveId -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtin_unglue
munglueU <- getPrimitiveName' builtin_unglueU
msubout <- getPrimitiveName' builtinSubOut
case () of
()
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
munglue -> QName -> Elims -> Elims -> m Bool
compareUnglueApp QName
q Elims
es Elims
es'
()
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
munglueU -> MonadConversion m => QName -> Elims -> Elims -> m Bool
QName -> Elims -> Elims -> m Bool
compareUnglueUApp QName
q Elims
es Elims
es'
()
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
msubout -> QName -> Elims -> Elims -> m Bool
compareSubApp QName
q Elims
es Elims
es'
()
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
compareSubApp :: QName -> Elims -> Elims -> m Bool
compareSubApp QName
q Elims
es Elims
es' = do
let (Elims
as,Elims
bs) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
5 Elims
es; (Elims
as',Elims
bs') = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
5 Elims
es'
case (Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
as, Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
as') of
(Just [Arg Term
a,Arg Term
bA,Arg Term
phi,Arg Term
u,Arg Term
x], Just [Arg Term
a',Arg Term
bA',Arg Term
phi',Arg Term
u',Arg Term
x']) -> do
tSub <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub
equalType (El (tmSSort $ unArg a) $ apply tSub $ a : map (setHiding NotHidden) [bA,phi,u])
(El (tmSSort $ unArg a) $ apply tSub $ a : map (setHiding NotHidden) [bA',phi',u'])
compareAtom cmp (AsTermsOf $ El (tmSSort $ unArg a) $ apply tSub $ a : map (setHiding NotHidden) [bA,phi,u])
(unArg x) (unArg x')
compareElims [] [] (El (tmSort (unArg a)) (unArg bA)) (Def q as) bs bs'
return True
(Maybe [Arg Term], Maybe [Arg Term])
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
compareUnglueApp :: QName -> Elims -> Elims -> m Bool
compareUnglueApp QName
q Elims
es Elims
es' = do
let (Elims
as,Elims
bs) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
7 Elims
es; (Elims
as',Elims
bs') = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
7 Elims
es'
case (Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
as, Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
as') of
(Just [Arg Term
la,Arg Term
lb,Arg Term
bA,Arg Term
phi,Arg Term
bT,Arg Term
e,Arg Term
b], Just [Arg Term
la',Arg Term
lb',Arg Term
bA',Arg Term
phi',Arg Term
bT',Arg Term
e',Arg Term
b']) -> do
tGlue <- PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinGlue
compareAtom cmp (AsTermsOf $ El (tmSort (unArg lb)) $ apply tGlue $ [la,lb] ++ map (setHiding NotHidden) [bA,phi,bT,e])
(unArg b) (unArg b')
compareElims [] [] (El (tmSort (unArg la)) (unArg bA)) (Def q as) bs bs'
return True
(Maybe [Arg Term], Maybe [Arg Term])
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
compareUnglueUApp :: MonadConversion m => QName -> Elims -> Elims -> m Bool
compareUnglueUApp :: MonadConversion m => QName -> Elims -> Elims -> m Bool
compareUnglueUApp QName
q Elims
es Elims
es' = do
let (Elims
as,Elims
bs) = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
5 Elims
es; (Elims
as',Elims
bs') = Int -> Elims -> (Elims, Elims)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
5 Elims
es'
case (Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
as, Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
as') of
(Just [Arg Term
la,Arg Term
phi,Arg Term
bT,Arg Term
bAS,Arg Term
b], Just [Arg Term
la',Arg Term
phi',Arg Term
bT',Arg Term
bA',Arg Term
b']) -> do
tHComp <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp
tLSuc <- primLevelSuc
tSubOut <- primSubOut
iz <- primIZero
let lsuc Term
t = Term
tLSuc Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
t]
s = Term -> Sort
tmSort (Term -> Sort) -> Term -> Sort
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
la
sucla = Term -> Term
lsuc (Term -> Term) -> Arg Term -> Arg Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
la
bA <- runNamesT [] $ do
[la,phi,bT,bAS] <- mapM (open . unArg) [la,phi,bT,bAS]
(pure tSubOut <#> (pure tLSuc <@> la) <#> (Sort . tmSort <$> la) <#> phi <#> (bT <@> primIZero) <@> bAS)
compareAtom cmp (AsTermsOf $ El (tmSort . unArg $ sucla) $ apply tHComp $ [sucla, argH (Sort s), phi] ++ [argH (unArg bT), argH bA])
(unArg b) (unArg b')
compareElims [] [] (El s bA) (Def q as) bs bs'
return True
(Maybe [Arg Term], Maybe [Arg Term])
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
conType :: ConHead -> Type -> m Type
conType ConHead
c Type
t = do
t <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
t
let impossible = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"impossible" Int
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"expected data/record type, found " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"impossible" Int
70 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"raw =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t
Blocker -> m Type
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
maybe impossible (return . snd) =<< getFullyAppliedConType c t
equalFun :: Term -> Term -> m ()
equalFun Term
t1 Term
t2 = case (Term
t1, Term
t2) of
(Pi Dom Type
dom1 Abs Type
b1, Pi Dom Type
dom2 Abs Type
b2) -> do
String -> Int -> String -> m () -> m ()
forall a. String -> Int -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.conv.fun" Int
15 String
"compare function types" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.fun" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"t1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t1
, TCMT IO Doc
"t2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t2
]
Comparison
-> Dom Type
-> Dom Type
-> Abs Type
-> Abs Type
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
forall (m :: * -> *) c b.
(MonadConversion m, Free c) =>
Comparison
-> Dom Type
-> Dom Type
-> Abs b
-> Abs c
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
compareDom Comparison
cmp Dom Type
dom2 Dom Type
dom1 Abs Type
b1 Abs Type
b2 m ()
errH m ()
errR m ()
errQ m ()
errC m ()
errF (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Comparison -> Type -> Type -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b1) (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b2)
where
errH :: m ()
errH = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> TypeError
UnequalHiding Term
t1 Term
t2
errR :: m ()
errR = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> TypeError
UnequalRelevance Comparison
cmp Term
t1 Term
t2
errQ :: m ()
errQ = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> TypeError
UnequalQuantity Comparison
cmp Term
t1 Term
t2
errC :: m ()
errC = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> TypeError
UnequalCohesion Comparison
cmp Term
t1 Term
t2
errF :: m ()
errF = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> TypeError
UnequalFiniteness Comparison
cmp Term
t1 Term
t2
(Term, Term)
_ -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
compareMetas :: MonadConversion m => Comparison -> CompareAs -> MetaId -> Elims -> MetaId -> Elims -> m ()
compareMetas :: forall (m :: * -> *).
MonadConversion m =>
Comparison
-> CompareAs -> MetaId -> Elims -> MetaId -> Elims -> m ()
compareMetas Comparison
cmp CompareAs
t MetaId
x Elims
xArgs MetaId
y Elims
yArgs | MetaId
x MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
y = Blocker -> m () -> m ()
forall (m :: * -> *) a. MonadError TCErr m => Blocker -> m a -> m a
blockOnError (MetaId -> Blocker
unblockOnMeta MetaId
x) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
cmpBlocked <- Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eCompareBlocked
let ok = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
notOk = Blocker -> m a
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
fallback = do
a <- MetaId -> m Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
runPureConversion (compareElims [] [] a (MetaV x []) xArgs yArgs) >>= \case
Just{} -> m ()
ok
Maybe ()
Nothing -> m ()
forall {a}. m a
notOk
if | cmpBlocked -> do
a <- metaType x
compareElims [] [] a (MetaV x []) xArgs yArgs
| otherwise -> case intersectVars xArgs yArgs of
Just [Bool]
kills -> do
killResult <- [Bool] -> MetaId -> m PruneResult
forall (m :: * -> *).
MonadMetaSolver m =>
[Bool] -> MetaId -> m PruneResult
killArgs [Bool]
kills MetaId
x
case killResult of
PruneResult
NothingToPrune -> m ()
ok
PruneResult
PrunedEverything -> m ()
ok
PruneResult
PrunedNothing -> m ()
fallback
PruneResult
PrunedSomething -> m ()
fallback
Maybe [Bool]
Nothing -> m ()
fallback
compareMetas Comparison
cmp CompareAs
t MetaId
x Elims
xArgs MetaId
y Elims
yArgs = do
[p1, p2] <- (MetaId -> m MetaPriority) -> [MetaId] -> m [MetaPriority]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM MetaId -> m MetaPriority
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaPriority
getMetaPriority [MetaId
x,MetaId
y]
let dir = Comparison -> CompareDirection
fromCmp Comparison
cmp
rid = CompareDirection -> CompareDirection
flipCmp CompareDirection
dir
retry = Blocker -> m a
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock
let (solve1, solve2)
| (p1, x) > (p2, y) = (l1, r2)
| otherwise = (r1, l2)
where l1 = CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
forall (m :: * -> *).
MonadConversion m =>
CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
assignE CompareDirection
dir MetaId
x Elims
xArgs (MetaId -> Elims -> Term
MetaV MetaId
y Elims
yArgs) CompareAs
t ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Term
_ Term
_ -> m ()
forall {a}. m a
retry
r1 = CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
forall (m :: * -> *).
MonadConversion m =>
CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
assignE CompareDirection
rid MetaId
y Elims
yArgs (MetaId -> Elims -> Term
MetaV MetaId
x Elims
xArgs) CompareAs
t ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Term
_ Term
_ -> m ()
forall {a}. m a
retry
l2 = m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isInstantiatedMeta MetaId
x) m ()
forall {a}. m a
retry m ()
l1
r2 = m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> m Bool
forall a (m :: * -> *).
(IsInstantiatedMeta a, MonadFail m, ReadTCState m) =>
a -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isInstantiatedMeta MetaId
y) m ()
forall {a}. m a
retry m ()
r1
catchPatternErr (`addOrUnblocker` solve2) solve1
compareDom :: (MonadConversion m , Free c)
=> Comparison
-> Dom Type
-> Dom Type
-> Abs b
-> Abs c
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
compareDom :: forall (m :: * -> *) c b.
(MonadConversion m, Free c) =>
Comparison
-> Dom Type
-> Dom Type
-> Abs b
-> Abs c
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
compareDom Comparison
cmp0
dom1 :: Dom Type
dom1@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
i1, unDom :: forall t e. Dom' t e -> e
unDom = Type
a1})
dom2 :: Dom Type
dom2@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
i2, unDom :: forall t e. Dom' t e -> e
unDom = Type
a2})
Abs b
b1 Abs c
b2 m ()
errH m ()
errR m ()
errQ m ()
errC m ()
errF m ()
cont = do
if | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Dom Type -> Dom Type -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Dom Type
dom1 Dom Type
dom2 -> m ()
errH
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
dom1) (Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
dom2) -> m ()
errR
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Quantity -> Quantity -> Bool
sameQuantity (Dom Type -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
dom1) (Dom Type -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Dom Type
dom2) -> m ()
errQ
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Cohesion -> Cohesion -> Bool
sameCohesion (Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
dom1) (Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
dom2) -> m ()
errC
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Dom Type -> Bool
forall t e. Dom' t e -> Bool
domIsFinite Dom Type
dom1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Dom Type -> Bool
forall t e. Dom' t e -> Bool
domIsFinite Dom Type
dom2 -> m ()
errF
| Bool
otherwise -> do
let r :: Relevance
r = Relevance -> Relevance -> Relevance
forall a. Ord a => a -> a -> a
max (Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
dom1) (Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
dom2)
dependent :: Bool
dependent = (Relevance
r Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Relevance
Irrelevant) Bool -> Bool -> Bool
&& Abs c -> Bool
forall a. Free a => Abs a -> Bool
isBinderUsed Abs c
b2
pid <- m () -> m ProblemId
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblem_ (m () -> m ProblemId) -> m () -> m ProblemId
forall a b. (a -> b) -> a -> b
$ Comparison -> Type -> Type -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp0 Type
a1 Type
a2
dom <- if dependent
then (\ Type
a -> Dom Type
dom1 {unDom = a}) <$> blockTypeOnProblem a1 pid
else return dom1
let name = [Suggestion] -> String
suggests [ Abs b -> Suggestion
forall a. Suggest a => a -> Suggestion
Suggestion Abs b
b1 , Abs c -> Suggestion
forall a. Suggest a => a -> Suggestion
Suggestion Abs c
b2 ]
addContext (name, dom) $ cont
stealConstraints pid
antiUnify :: MonadConversion m => ProblemId -> Type -> Term -> Term -> m Term
antiUnify :: forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Type -> Term -> Term -> m Term
antiUnify ProblemId
pid Type
a Term
u Term
v = do
Term
-> Term
-> (Term -> Term -> m Term)
-> (Term -> Term -> m Term)
-> m Term
forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
SynEq.checkSyntacticEquality Term
u Term
v (\Term
u Term
_ -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u) ((Term -> Term -> m Term) -> m Term)
-> (Term -> Term -> m Term) -> m Term
forall a b. (a -> b) -> a -> b
$ \Term
u Term
v -> do
(u, v) <- (Term, Term) -> m (Term, Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
u, Term
v)
reportSDoc "tc.conv.antiUnify" 30 $ vcat
[ "antiUnify"
, "a =" <+> prettyTCM a
, "u =" <+> prettyTCM u
, "v =" <+> prettyTCM v
]
case (u, v) of
(Pi Dom Type
ua Abs Type
ub, Pi Dom Type
va Abs Type
vb) -> do
wa0 <- ProblemId -> Type -> Type -> m Type
forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Type -> Type -> m Type
antiUnifyType ProblemId
pid (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
ua) (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
va)
let wa = Type
wa0 Type -> Dom Type -> Dom Type
forall a b. a -> Dom' Term b -> Dom' Term a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Dom Type
ua
wb <- addContext wa $ antiUnifyType pid (absBody ub) (absBody vb)
return $ Pi wa (mkAbs (absName ub) wb)
(Lam ArgInfo
i Abs Term
u, Lam ArgInfo
_ Abs Term
v) ->
Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) m Term -> (Term -> m Term) -> m Term
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Pi Dom Type
a Abs Type
b -> ArgInfo -> Abs Term -> Term
Lam ArgInfo
i (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Term -> Abs Term
forall a. (Subst a, Free a) => String -> a -> Abs a
mkAbs (Abs Term -> String
forall a. Abs a -> String
absName Abs Term
u)) (Term -> Term) -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> m Term -> m Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => Dom Type -> m a -> m a
addContext Dom Type
a (ProblemId -> Type -> Term -> Term -> m Term
forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Type -> Term -> Term -> m Term
antiUnify ProblemId
pid (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) (Abs Term -> Term
forall a. Subst a => Abs a -> a
absBody Abs Term
u) (Abs Term -> Term
forall a. Subst a => Abs a -> a
absBody Abs Term
v))
Term
_ -> m Term
fallback
(Var Int
i Elims
us, Var Int
j Elims
vs) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j -> m Term -> m Term
maybeGiveUp (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
a <- Int -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i
antiUnifyElims pid a (var i) us vs
(Con ConHead
x ConInfo
ci Elims
us, Con ConHead
y ConInfo
_ Elims
vs) | ConHead
x ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
y -> m Term -> m Term
maybeGiveUp (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
a <- m Type
-> (((QName, Type, [Arg Term]), Type) -> m Type)
-> Maybe ((QName, Type, [Arg Term]), Type)
-> m Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m Type
forall {a}. m a
abort (Type -> m Type
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type)
-> (((QName, Type, [Arg Term]), Type) -> Type)
-> ((QName, Type, [Arg Term]), Type)
-> m Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QName, Type, [Arg Term]), Type) -> Type
forall a b. (a, b) -> b
snd) (Maybe ((QName, Type, [Arg Term]), Type) -> m Type)
-> m (Maybe ((QName, Type, [Arg Term]), Type)) -> m Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConHead -> Type -> m (Maybe ((QName, Type, [Arg Term]), Type))
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
ConHead -> Type -> m (Maybe ((QName, Type, [Arg Term]), Type))
getConType ConHead
x Type
a
antiUnifyElims pid a (Con x ci []) us vs
(Def QName
f [], Def QName
g []) | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> Elims -> Term
Def QName
f [])
(Def QName
f Elims
us, Def QName
g Elims
vs) | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g, Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
us Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
vs -> m Term -> m Term
maybeGiveUp (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
a <- QName -> Elims -> Elims -> m Type
forall (m :: * -> *).
MonadConversion m =>
QName -> Elims -> Elims -> m Type
computeElimHeadType QName
f Elims
us Elims
vs
antiUnifyElims pid a (Def f []) us vs
(Term, Term)
_ -> m Term
fallback
where
maybeGiveUp :: m Term -> m Term
maybeGiveUp = (Blocker -> m Term) -> m Term -> m Term
forall a. (Blocker -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr ((Blocker -> m Term) -> m Term -> m Term)
-> (Blocker -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ \ Blocker
_ -> m Term
fallback
abort :: m a
abort = Blocker -> m a
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
fallback :: m Term
fallback = Type -> Term -> ProblemId -> m Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Int m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
a Term
u ProblemId
pid
antiUnifyArgs :: MonadConversion m => ProblemId -> Dom Type -> Arg Term -> Arg Term -> m (Arg Term)
antiUnifyArgs :: forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Dom Type -> Arg Term -> Arg Term -> m (Arg Term)
antiUnifyArgs ProblemId
pid Dom Type
dom Arg Term
u Arg Term
v
| Bool -> Bool
not (Modality -> Modality -> Bool
forall a b. (LensModality a, LensModality b) => a -> b -> Bool
sameModality (Arg Term -> Modality
forall a. LensModality a => a -> Modality
getModality Arg Term
u) (Arg Term -> Modality
forall a. LensModality a => a -> Modality
getModality Arg Term
v))
= Blocker -> m (Arg Term)
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
| Bool
otherwise = Arg Term -> m (Arg Term) -> m (Arg Term)
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Arg Term
u (m (Arg Term) -> m (Arg Term)) -> m (Arg Term) -> m (Arg Term)
forall a b. (a -> b) -> a -> b
$
m Bool -> m (Arg Term) -> m (Arg Term) -> m (Arg Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Dom Type -> m Bool
forall a (m :: * -> *).
(LensRelevance a, LensSort a, PrettyTCM a, PureTCM m,
MonadBlock m) =>
a -> m Bool
isIrrelevantOrPropM Dom Type
dom)
(Arg Term -> m (Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Arg Term
u)
((Term -> Arg Term -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Term
u) (Term -> Arg Term) -> m Term -> m (Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProblemId -> Type -> Term -> Term -> m Term
forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Type -> Term -> Term -> m Term
antiUnify ProblemId
pid (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom) (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u) (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v))
antiUnifyType :: MonadConversion m => ProblemId -> Type -> Type -> m Type
antiUnifyType :: forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Type -> Type -> m Type
antiUnifyType ProblemId
pid (El Sort
s Term
a) (El Sort
_ Term
b) = m Type -> m Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (m Type -> m Type) -> m Type -> m Type
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProblemId -> Type -> Term -> Term -> m Term
forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Type -> Term -> Term -> m Term
antiUnify ProblemId
pid (Sort -> Type
sort Sort
s) Term
a Term
b
antiUnifyElims :: MonadConversion m => ProblemId -> Type -> Term -> Elims -> Elims -> m Term
antiUnifyElims :: forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Type -> Term -> Elims -> Elims -> m Term
antiUnifyElims ProblemId
pid Type
a Term
self [] [] = Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
self
antiUnifyElims ProblemId
pid Type
a Term
self (Proj ProjOrigin
o QName
f : Elims
es1) (Proj ProjOrigin
_ QName
g : Elims
es2) | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g = do
res <- Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
forall (m :: * -> *).
PureTCM m =>
Term
-> Type -> ProjOrigin -> QName -> m (Maybe (Dom Type, Term, Type))
projectTyped Term
self Type
a ProjOrigin
o QName
f
case res of
Just (Dom Type
_, Term
self, Type
a) -> ProblemId -> Type -> Term -> Elims -> Elims -> m Term
forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Type -> Term -> Elims -> Elims -> m Term
antiUnifyElims ProblemId
pid Type
a Term
self Elims
es1 Elims
es2
Maybe (Dom Type, Term, Type)
Nothing -> Blocker -> m Term
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
antiUnifyElims ProblemId
pid Type
a Term
self (Apply Arg Term
u : Elims
es1) (Apply Arg Term
v : Elims
es2) = do
Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) m Term -> (Term -> m Term) -> m Term
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Pi Dom Type
a Abs Type
b -> do
w <- ProblemId -> Dom Type -> Arg Term -> Arg Term -> m (Arg Term)
forall (m :: * -> *).
MonadConversion m =>
ProblemId -> Dom Type -> Arg Term -> Arg Term -> m (Arg Term)
antiUnifyArgs ProblemId
pid Dom Type
a Arg Term
u Arg Term
v
antiUnifyElims pid (b `lazyAbsApp` unArg w) (apply self [w]) es1 es2
Term
_ -> Blocker -> m Term
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
antiUnifyElims ProblemId
_ Type
_ Term
_ Elims
_ Elims
_ = Blocker -> m Term
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
compareElims :: forall m. MonadConversion m => [Polarity] -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> m ()
compareElims :: forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
compareElims [Polarity]
pols0 [IsForced]
fors0 Type
a Term
v Elims
els01 Elims
els02 =
String -> Int -> String -> m () -> m ()
forall a. String -> Int -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.conv.elim" Int
20 String
"compareElims" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
(Constraint -> m () -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint ([Polarity]
-> [IsForced] -> Type -> Term -> Elims -> Elims -> Constraint
ElimCmp [Polarity]
pols0 [IsForced]
fors0 Type
a Term
v Elims
els01 Elims
els02) :: m () -> m ()) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
let v1 :: Term
v1 = Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v Elims
els01
v2 :: Term
v2 = Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE Term
v Elims
els02
failure :: m ()
failure = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
CmpEq Term
v1 Term
v2 (Type -> CompareAs
AsTermsOf Type
a)
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Elims -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Elims
els01) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.elim" Int
25 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"compareElims" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"a =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, TCMT IO Doc
"pols0 (truncated to 10) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ((Polarity -> TCMT IO Doc) -> [Polarity] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Polarity -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Polarity -> m Doc
prettyTCM ([Polarity] -> [TCMT IO Doc]) -> [Polarity] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ Int -> [Polarity] -> [Polarity]
forall a. Int -> [a] -> [a]
take Int
10 [Polarity]
pols0)
, TCMT IO Doc
"fors0 (truncated to 10) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ((IsForced -> TCMT IO Doc) -> [IsForced] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map IsForced -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => IsForced -> m Doc
prettyTCM ([IsForced] -> [TCMT IO Doc]) -> [IsForced] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ Int -> [IsForced] -> [IsForced]
forall a. Int -> [a] -> [a]
take Int
10 [IsForced]
fors0)
, TCMT IO Doc
"v =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, TCMT IO Doc
"els01 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elims -> m Doc
prettyTCM Elims
els01
, TCMT IO Doc
"els02 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Elims -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elims -> m Doc
prettyTCM Elims
els02
]
case (Elims
els01, Elims
els02) of
([] , [] ) -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
([] , Proj{}:Elims
_ ) -> m ()
failure
(Proj{} : Elims
_, [] ) -> m ()
failure
([] , Apply{} : Elims
_) -> m ()
failure
(Apply{} : Elims
_, [] ) -> m ()
failure
([] , IApply{} : Elims
_) -> m ()
failure
(IApply{} : Elims
_, [] ) -> m ()
failure
(Apply{} : Elims
_, Proj{} : Elims
_) -> ()
forall a. HasCallStack => a
__IMPOSSIBLE__ () -> m () -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> m ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
True
(Proj{} : Elims
_, Apply{} : Elims
_) -> ()
forall a. HasCallStack => a
__IMPOSSIBLE__ () -> m () -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> m ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
True
(IApply{} : Elims
_, Proj{} : Elims
_) -> ()
forall a. HasCallStack => a
__IMPOSSIBLE__ () -> m () -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> m ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
True
(Proj{} : Elims
_, IApply{} : Elims
_) -> ()
forall a. HasCallStack => a
__IMPOSSIBLE__ () -> m () -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> m ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
True
(IApply{} : Elims
_, Apply{} : Elims
_) -> ()
forall a. HasCallStack => a
__IMPOSSIBLE__ () -> m () -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> m ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
True
(Apply{} : Elims
_, IApply{} : Elims
_) -> ()
forall a. HasCallStack => a
__IMPOSSIBLE__ () -> m () -> m ()
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> m ()
forall (m :: * -> *). MonadConstraint m => Bool -> m ()
solveAwakeConstraints' Bool
True
(e :: Elim' Term
e@(IApply Term
x1 Term
y1 Term
r1) : Elims
els1, IApply Term
x2 Term
y2 Term
r2 : Elims
els2) -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.elim" Int
25 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"compareElims IApply"
let (Polarity
pol, [Polarity]
pols) = [Polarity] -> (Polarity, [Polarity])
nextPolarity [Polarity]
pols0
a <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
a
va <- pathView a
reportSDoc "tc.conv.elim.iapply" 60 $ "compareElims IApply" $$ do
nest 2 $ "va =" <+> text (show (isPathType va))
case va of
PathType Sort
s QName
path Arg Term
l Arg Term
bA Arg Term
x Arg Term
y -> do
b <- m Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
compareWithPol pol (flip compareTerm b)
r1 r2
let r = Term
r1
codom <- el' (pure . unArg $ l) ((pure . unArg $ bA) <@> pure r)
compareElims pols [] codom
(applyE v [e]) els1 els2
OType t :: Type
t@(El Sort
_ Pi{}) -> [Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
compareElims [Polarity]
pols0 [IsForced]
fors0 Type
t Term
v (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall e. e -> Arg e
defaultArg Term
r1) Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
els1) (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall e. e -> Arg e
defaultArg Term
r2) Elim' Term -> Elims -> Elims
forall a. a -> [a] -> [a]
: Elims
els2)
OType Type
t -> Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Type -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type
t)
(Apply Arg Term
arg1 : Elims
els1, Apply Arg Term
arg2 : Elims
els2) ->
(String -> Int -> String -> m () -> m ()
forall a. String -> Int -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.conv.elim" Int
20 String
"compare Apply" :: m () -> m ()) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.elim" Int
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"a =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
, TCMT IO Doc
"v =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, TCMT IO Doc
"arg1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Arg Term
arg1
, TCMT IO Doc
"arg2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Arg Term
arg2
]
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.elim" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"raw:"
, TCMT IO Doc
"a =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
a
, TCMT IO Doc
"v =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
, TCMT IO Doc
"arg1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Term
arg1
, TCMT IO Doc
"arg2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Arg Term
arg2
]
let (Polarity
pol, [Polarity]
pols) = [Polarity] -> (Polarity, [Polarity])
nextPolarity [Polarity]
pols0
(IsForced
for, [IsForced]
fors) = [IsForced] -> (IsForced, [IsForced])
nextIsForced [IsForced]
fors0
a <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
a
reportSLn "tc.conv.elim" 40 $ "type is not blocked"
case unEl a of
(Pi (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
b}) Abs Type
codom) -> do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.conv.elim" Int
40 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"type is a function type"
mlvl <- m Term -> m (Maybe Term)
forall e (m :: * -> *) a.
(MonadError e m, Functor m) =>
m a -> m (Maybe a)
tryMaybe m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel
let freeInCoDom (Abs String
_ a
c) = Int
0 Int -> a -> Bool
forall a. Free a => Int -> a -> Bool
`freeInIgnoringSorts` a
c
freeInCoDom Abs a
_ = Bool
False
dependent = (Term -> Maybe Term
forall a. a -> Maybe a
Just (Type -> Term
forall t a. Type'' t a -> a
unEl Type
b) Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Term
mlvl) Bool -> Bool -> Bool
&& Abs Type -> Bool
forall a. Free a => Abs a -> Bool
freeInCoDom Abs Type
codom
pid <- newProblem_ $ applyModalityToContext info $
if isForced for then
reportSLn "tc.conv.elim" 40 $ "argument is forced"
else if isIrrelevant info then do
reportSLn "tc.conv.elim" 40 $ "argument is irrelevant"
compareIrrelevant b (unArg arg1) (unArg arg2)
else do
reportSLn "tc.conv.elim" 40 $ "argument has polarity " ++ show pol
compareWithPol pol (flip compareTerm b)
(unArg arg1) (unArg arg2)
solved <- isProblemSolved pid
reportSLn "tc.conv.elim" 40 $ "solved = " ++ show solved
arg <- if dependent && not solved
then applyModalityToContext info $ do
reportSDoc "tc.conv.elims" 50 $ vcat $
[ "Trying antiUnify:"
, nest 2 $ "b =" <+> prettyTCM b
, nest 2 $ "arg1 =" <+> prettyTCM arg1
, nest 2 $ "arg2 =" <+> prettyTCM arg2
]
arg <- (arg1 $>) <$> antiUnify pid b (unArg arg1) (unArg arg2)
reportSDoc "tc.conv.elims" 50 $ hang "Anti-unification:" 2 (prettyTCM arg)
reportSDoc "tc.conv.elims" 70 $ nest 2 $ "raw:" <+> pretty arg
return arg
else return arg1
compareElims pols fors (codom `lazyAbsApp` unArg arg) (apply v [arg]) els1 els2
reportSLn "tc.conv.elim" 40 $ "stealing constraints from problem " ++ show pid
stealConstraints pid
Term
a -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"impossible" Int
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"unexpected type when comparing apply eliminations " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
a
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"impossible" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"raw type:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
a
Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
a)
(Proj ProjOrigin
o QName
f : Elims
els1, Proj ProjOrigin
_ QName
f' : Elims
els2)
| QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
/= QName
f' -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ QName -> QName -> TypeError
MismatchedProjectionsError QName
f QName
f'
| Bool
otherwise -> do
a <- Type -> m Type
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked Type
a
res <- projectTyped v a o f
case res of
Just (Dom Type
_, Term
u, Type
t) -> do
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
compareElims [] [] Type
t Term
u Elims
els1 Elims
els2
Maybe (Dom Type, Term, Type)
Nothing -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.elims" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"projection " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
f
, String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"applied to value " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"of unexpected type " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a
]
Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Type -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type
a)
compareIrrelevant :: MonadConversion m => Type -> Term -> Term -> m ()
compareIrrelevant :: forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
compareIrrelevant Type
t Term
v0 Term
w0 = do
let v :: Term
v = Term -> Term
stripDontCare Term
v0
w :: Term
w = Term -> Term
stripDontCare Term
w0
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.irr" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"compareIrrelevant"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"w =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
w
]
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.irr" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"w =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
w
]
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare irrelevant"
Term -> Term -> m () -> m ()
try Term
v Term
w (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> m () -> m ()
try Term
w Term
v (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
try :: Term -> Term -> m () -> m ()
try (MetaV MetaId
x Elims
es) Term
w m ()
fallback = do
mi <- MetaId -> m MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
mm <- lookupMetaModality x
let rel = Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mm
inst = case MetaInstantiation
mi of
InstV{} -> Bool
True
MetaInstantiation
_ -> Bool
False
reportSDoc "tc.conv.irr" 20 $ vcat
[ nest 2 $ text $ "rel = " ++ show rel
, nest 2 $ "inst =" <+> pretty inst
]
if not (isIrrelevant rel) || inst
then fallback
else assignE DirEq x es w (AsTermsOf t) (compareIrrelevant t) `catchError` \ TCErr
_ -> m ()
fallback
try Term
v Term
w m ()
fallback = m ()
fallback
compareWithPol :: MonadConversion m => Polarity -> (Comparison -> a -> a -> m ()) -> a -> a -> m ()
compareWithPol :: forall (m :: * -> *) a.
MonadConversion m =>
Polarity -> (Comparison -> a -> a -> m ()) -> a -> a -> m ()
compareWithPol Polarity
Invariant Comparison -> a -> a -> m ()
cmp a
x a
y = Comparison -> a -> a -> m ()
cmp Comparison
CmpEq a
x a
y
compareWithPol Polarity
Covariant Comparison -> a -> a -> m ()
cmp a
x a
y = Comparison -> a -> a -> m ()
cmp Comparison
CmpLeq a
x a
y
compareWithPol Polarity
Contravariant Comparison -> a -> a -> m ()
cmp a
x a
y = Comparison -> a -> a -> m ()
cmp Comparison
CmpLeq a
y a
x
compareWithPol Polarity
Nonvariant Comparison -> a -> a -> m ()
cmp a
x a
y = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
polFromCmp :: Comparison -> Polarity
polFromCmp :: Comparison -> Polarity
polFromCmp Comparison
CmpLeq = Polarity
Covariant
polFromCmp Comparison
CmpEq = Polarity
Invariant
compareArgs :: MonadConversion m => [Polarity] -> [IsForced] -> Type -> Term -> Args -> Args -> m ()
compareArgs :: forall (m :: * -> *).
MonadConversion m =>
[Polarity]
-> [IsForced] -> Type -> Term -> [Arg Term] -> [Arg Term] -> m ()
compareArgs [Polarity]
pol [IsForced]
for Type
a Term
v [Arg Term]
args1 [Arg Term]
args2 =
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
forall (m :: * -> *).
MonadConversion m =>
[Polarity] -> [IsForced] -> Type -> Term -> Elims -> Elims -> m ()
compareElims [Polarity]
pol [IsForced]
for Type
a Term
v ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
args1) ((Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term]
args2)
{-# SPECIALIZE compareType :: Comparison -> Type -> Type -> TCM () #-}
compareType :: MonadConversion m => Comparison -> Type -> Type -> m ()
compareType :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp ty1 :: Type
ty1@(El Sort
s1 Term
a1) ty2 :: Type
ty2@(El Sort
s2 Term
a2) =
m () -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
String -> Int -> String -> m () -> m ()
forall a. String -> Int -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.conv.type" Int
20 String
"compareType" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.type" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"compareType" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Comparison -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp
, Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
ty2 ]
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ TCMT IO Doc
" sorts:", Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1, TCMT IO Doc
" and ", Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2 ]
]
Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAs Comparison
cmp CompareAs
AsTypes Term
a1 Term
a2
leqType :: MonadConversion m => Type -> Type -> m ()
leqType :: forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType = Comparison -> Type -> Type -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
CmpLeq
{-# SPECIALIZE coerce :: Comparison -> Term -> Type -> Type -> TCM Term #-}
coerce :: (MonadConversion m, MonadTCM m) => Comparison -> Term -> Type -> Type -> m Term
coerce :: forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
t1 Type
t2 = Type -> m Term -> m Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Int m,
MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t2 (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> m () -> m ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS String
"tc.conv.coerce" Int
10 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
(a1,a2) <- (Type, Type) -> m (ReifiesTo (Type, Type))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
(Type, Type) -> m (ReifiesTo (Type, Type))
reify (Type
t1,Type
t2)
let dbglvl = Int
30
reportSDoc "tc.conv.coerce" dbglvl $
"coerce" <+> vcat
[ "term v =" <+> prettyTCM v
, "from type t1 =" <+> prettyTCM a1
, "to type t2 =" <+> prettyTCM a2
, "comparison =" <+> prettyTCM cmp
]
reportSDoc "tc.conv.coerce" 70 $
"coerce" <+> vcat
[ "term v =" <+> pretty v
, "from type t1 =" <+> pretty t1
, "to type t2 =" <+> pretty t2
, "comparison =" <+> pretty cmp
]
TelV tel1 b1 <- Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t1
TelV tel2 b2 <- telViewUpTo' (-1) notVisible t2
let n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel2
if n <= 0 then fallback else do
ifBlocked b2 (\ Blocker
_ Type
_ -> m Term
fallback) $ \ NotBlocked
_ Type
_ -> do
(args, t1') <- Int -> (Hiding -> Bool) -> Type -> m ([Arg Term], Type)
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int -> (Hiding -> Bool) -> Type -> m ([Arg Term], Type)
implicitArgs Int
n Hiding -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t1
let v' = Term
v Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args
v' <$ coerceSize (compareType cmp) v' t1' t2
where
fallback :: m Term
fallback = Term
v Term -> m () -> m Term
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
forall (m :: * -> *).
MonadConversion m =>
(Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
coerceSize (Comparison -> Type -> Type -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Type -> m ()
compareType Comparison
cmp) Term
v Type
t1 Type
t2
{-# SPECIALIZE coerceSize :: (Type -> Type -> TCM ()) -> Term -> Type -> Type -> TCM () #-}
coerceSize :: MonadConversion m => (Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
coerceSize :: forall (m :: * -> *).
MonadConversion m =>
(Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
coerceSize Type -> Type -> m ()
leqType Term
v Type
t1 Type
t2 = String -> Int -> String -> m () -> m ()
forall a. String -> Int -> String -> m a -> m a
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> String -> m a -> m a
verboseBracket String
"tc.conv.size.coerce" Int
45 String
"coerceSize" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
m () -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.size.coerce" Int
70 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"coerceSize" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"term v =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
, TCMT IO Doc
"from type t1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t1
, TCMT IO Doc
"to type t2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
t2
]
let fallback :: m ()
fallback = Type -> Type -> m ()
leqType Type
t1 Type
t2
done :: m ()
done = m (Maybe BoundedSize) -> m () -> (BoundedSize -> m ()) -> m ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> m (Maybe BoundedSize)
isSizeType (Type -> m (Maybe BoundedSize)) -> m Type -> m (Maybe BoundedSize)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t1) m ()
fallback ((BoundedSize -> m ()) -> m ()) -> (BoundedSize -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ BoundedSize
_ -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
m (Maybe BoundedSize) -> m () -> (BoundedSize -> m ()) -> m ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> m (Maybe BoundedSize)
isSizeType (Type -> m (Maybe BoundedSize)) -> m Type -> m (Maybe BoundedSize)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t2) m ()
fallback ((BoundedSize -> m ()) -> m ()) -> (BoundedSize -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ BoundedSize
b2 -> do
mv <- Term -> m SizeMaxView
forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
sizeMaxView Term
v
if any (\case{ DOtherSize{} -> Bool
True; DeepSizeView
_ -> Bool
False }) mv then fallback else do
unlessM (tryConversion $ dontAssignMetas $ leqType t1 t2) $ do
reportSDoc "tc.conv.size.coerce" 20 $ "coercing to a size type"
case b2 of
BoundedSize
BoundedNo -> m ()
done
BoundedLt Term
v2 -> do
sv2 <- Term -> m SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
v2
case sv2 of
SizeView
SizeInf -> m ()
done
OtherSize{} -> do
vinc <- Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 Term
v
compareSizes CmpLeq vinc v2
done
SizeSuc Term
a2 -> do
Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
CmpLeq Term
v Term
a2
m ()
done
compareLevel :: MonadConversion m => Comparison -> Level -> Level -> m ()
compareLevel :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> Level -> Level -> m ()
compareLevel Comparison
CmpLeq Level
u Level
v = Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
leqLevel Level
u Level
v
compareLevel Comparison
CmpEq Level
u Level
v = Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
equalLevel Level
u Level
v
compareSort :: MonadConversion m => Comparison -> Sort -> Sort -> m ()
compareSort :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> Sort -> Sort -> m ()
compareSort Comparison
CmpEq = Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort
compareSort Comparison
CmpLeq = Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
leqSort
leqSort :: forall m. MonadConversion m => Sort -> Sort -> m ()
leqSort :: forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
leqSort Sort
s1 Sort
s2 = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"leqSort"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=<"
, Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2 ]
]
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"leqSort"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ Sort -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Sort
s1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=<"
, Sort -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Sort
s2 ]
]
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare sorts"
Sort
-> Sort -> (Sort -> Sort -> m ()) -> (Sort -> Sort -> m ()) -> m ()
forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
SynEq.checkSyntacticEquality Sort
s1 Sort
s2 (\Sort
_ Sort
_ -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((Sort -> Sort -> m ()) -> m ()) -> (Sort -> Sort -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Sort
s1 Sort
s2 -> do
s1b <- Sort -> m (Blocked Sort)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Sort
s1
s2b <- reduceB s2
let (s1,s2) = (ignoreBlocking s1b , ignoreBlocking s2b)
blocker = Blocker -> Blocker -> Blocker
unblockOnEither (Blocked Sort -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Sort
s1b) (Blocked Sort -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Sort
s2b)
postpone = Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
let postponeIfBlocked = (Blocker -> m ()) -> m () -> m ()
forall a. (Blocker -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr ((Blocker -> m ()) -> m () -> m ())
-> (Blocker -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ \Blocker
blocker -> do
if | Blocker
blocker Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> TypeError
NotLeqSort Sort
s1 Sort
s2
| Bool
otherwise -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"Postponing constraint"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=<"
, Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2 ]
]
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"Postponing constraint"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ Sort -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Sort
s1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=<"
, Sort -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Sort
s2 ]
]
blocker <- Blocker -> m Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker Blocker
blocker
addConstraint blocker $ SortCmp CmpLeq s1 s2
propEnabled <- isPropEnabled
typeInTypeEnabled <- typeInType
omegaInOmegaEnabled <- optOmegaInOmega <$> pragmaOptions
let infInInf = Bool
typeInTypeEnabled Bool -> Bool -> Bool
|| Bool
omegaInOmegaEnabled
let fvsRHS = (Int -> IntSet -> Bool
`IntSet.member` Sort -> IntSet
forall t. Free t => t -> IntSet
allFreeVars Sort
s2)
badRigid <- s1 `rigidVarsNotContainedIn` fvsRHS
postponeIfBlocked $ case (s1, s2) of
(DummyS String
s, Sort
_) -> String -> m ()
forall {m :: * -> *} {a} {b}.
(ReportS [a], MonadDebug m, IsString a) =>
a -> m b
impossibleSort String
s
(Sort
_, DummyS String
s) -> String -> m ()
forall {m :: * -> *} {a} {b}.
(ReportS [a], MonadDebug m, IsString a) =>
a -> m b
impossibleSort String
s
(Univ Univ
u Level
a, Univ Univ
u' Level
b) -> if Univ
u Univ -> Univ -> Bool
forall a. Ord a => a -> a -> Bool
<= Univ
u' then Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
leqLevel Level
a Level
b else m ()
forall {a}. m a
no
(Inf Univ
u Integer
m , Inf Univ
u' Integer
n) -> Bool -> m ()
answer (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ Univ
u Univ -> Univ -> Bool
forall a. Ord a => a -> a -> Bool
<= Univ
u' Bool -> Bool -> Bool
&& (Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n Bool -> Bool -> Bool
|| Bool
infInInf)
(Univ Univ
u Level
_, Inf Univ
u' Integer
_) -> Bool -> m ()
answer (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ Univ
u Univ -> Univ -> Bool
forall a. Ord a => a -> a -> Bool
<= Univ
u'
(Inf Univ
u Integer
_, Univ Univ
u' Level
_) -> Bool -> m ()
answer (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u' Bool -> Bool -> Bool
&& Bool
typeInTypeEnabled
(Sort
_ , Sort
LockUniv) -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s1 Sort
s2
(Sort
_ , Sort
LevelUniv) -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s1 Sort
s2
(Sort
_ , Sort
IntervalUniv) -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s1 Sort
s2
(Sort
_ , Sort
SizeUniv) -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s1 Sort
s2
(Sort
_ , Prop (Max Integer
0 [])) -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s1 Sort
s2
(Sort
_ , Type (Max Integer
0 []))
| Bool -> Bool
not Bool
propEnabled -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s1 Sort
s2
(Sort
SizeUniv, Univ{} ) -> m ()
forall {a}. m a
no
(Sort
SizeUniv , Inf{} ) -> m ()
forall {a}. m a
no
(Sort
LockUniv, Univ{} ) -> m ()
forall {a}. m a
no
(Sort
LockUniv , Inf{} ) -> m ()
forall {a}. m a
no
(Sort
LevelUniv, Univ{} ) -> m ()
forall {a}. m a
no
(Sort
LevelUniv , Inf{} ) -> m ()
forall {a}. m a
no
(Sort
IntervalUniv, Type{}) -> m ()
forall {a}. m a
no
(Sort
IntervalUniv, Prop{}) -> m ()
forall {a}. m a
no
(Sort
IntervalUniv , Inf Univ
u Integer
_) -> Bool -> m ()
answer (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ Univ -> IsFibrant
univFibrancy Univ
u IsFibrant -> IsFibrant -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant
IsStrict
(Sort
IntervalUniv , SSet Level
b) -> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
leqLevel (Integer -> Level
ClosedLevel Integer
0) Level
b
(Sort
_ , Sort
_ ) | Right (SmallSort Univ
f) <- Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s1 , Bool
badRigid -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
leqSort (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
f Integer
0) Sort
s2
(PiSort{}, Sort
_ ) -> m ()
postpone
(Sort
_ , PiSort{}) -> m ()
postpone
(FunSort{}, Sort
_ ) -> m ()
postpone
(Sort
_ , FunSort{}) -> m ()
postpone
(UnivSort{}, Sort
_ ) -> m ()
postpone
(Sort
_ , UnivSort{}) -> m ()
postpone
(MetaS{} , Sort
_ ) -> m ()
postpone
(Sort
_ , MetaS{} ) -> m ()
postpone
(DefS{} , Sort
_ ) -> m ()
forall {a}. m a
no
(Sort
_ , DefS{}) -> m ()
forall {a}. m a
no
where
no :: m a
no = Blocker -> m a
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
yes :: m ()
yes = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
answer :: Bool -> m ()
answer = \case
Bool
True -> m ()
yes
Bool
False -> m ()
forall {a}. m a
no
impossibleSort :: a -> m b
impossibleSort a
s = do
String -> Int -> [a] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
forall (m :: * -> *). MonadDebug m => String -> Int -> [a] -> m ()
reportS String
"impossible" Int
10
[ a
"leqSort: found dummy sort with description:"
, a
s
]
m b
forall a. HasCallStack => a
__IMPOSSIBLE__
leqLevel :: MonadConversion m => Level -> Level -> m ()
leqLevel :: forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
leqLevel Level
a Level
b = Constraint -> m () -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
CmpLeq Level
a Level
b) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"compareLevel" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Level -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM Level
a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=<"
, Level -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM Level
b ]
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare levels"
(a, b) <- (Level, Level) -> m (Level, Level)
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (Level
a, Level
b)
SynEq.checkSyntacticEquality' a b
(\Level
_ Level
_ ->
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
60
TCMT IO Doc
"checkSyntacticEquality returns True") $ \Level
a Level
b -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
60
TCMT IO Doc
"checkSyntacticEquality returns False"
let notok :: m ()
notok = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM m Bool
forall (m :: * -> *). HasOptions m => m Bool
typeInType (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> TypeError
NotLeqSort (Level -> Sort
forall t. Level' t -> Sort' t
Type Level
a) (Level -> Sort
forall t. Level' t -> Sort' t
Type Level
b)
postpone :: m ()
postpone = Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation ((Level, Level) -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn (Level
a, Level
b))
wrap :: m () -> m ()
wrap m ()
m = m ()
m m () -> (TCErr -> m ()) -> m ()
forall a. m a -> (TCErr -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
TypeError{} -> m ()
notok
TCErr
err -> TCErr -> m ()
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
cumulativity <- PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
areWeComputingOverlap <- viewTC eConflComputingOverlap
reportSDoc "tc.conv.level" 40 $
"compareLevelView" <+>
sep [ prettyList_ $ fmap (pretty . unSingleLevel) $ levelMaxView a
, "=<"
, prettyList_ $ fmap (pretty . unSingleLevel) $ levelMaxView b
]
aB <- mapM reduceB a
bB <- mapM reduceB b
wrap $ case (levelMaxView aB, levelMaxView bB) of
(SingleClosed Integer
0 :| [] , List1 (SingleLevel' (Blocked Term))
_) -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(List1 (SingleLevel' (Blocked Term))
as , SingleClosed Integer
0 :| []) ->
List1 (SingleLevel' (Blocked Term))
-> (SingleLevel' (Blocked Term) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ List1 (SingleLevel' (Blocked Term))
as ((SingleLevel' (Blocked Term) -> m ()) -> m ())
-> (SingleLevel' (Blocked Term) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ SingleLevel' (Blocked Term)
a' -> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
equalLevel (SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel (SingleLevel' Term -> Level) -> SingleLevel' Term -> Level
forall a b. (a -> b) -> a -> b
$ (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking SingleLevel' (Blocked Term)
a') (Integer -> Level
ClosedLevel Integer
0)
(SingleClosed Integer
m :| [], SingleClosed Integer
n :| []) -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n) m ()
notok
(SingleClosed Integer
m :| [] , List1 (SingleLevel' (Blocked Term))
_)
| Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Level -> Integer
levelLowerBound Level
b -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(List1 (SingleLevel' (Blocked Term))
as, List1 (SingleLevel' (Blocked Term))
bs)
| (SingleLevel' (Blocked Term) -> Bool)
-> List1 (SingleLevel' (Blocked Term)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SingleLevel' (Blocked Term) -> Bool
forall {t} {a}. SingleLevel' (Blocked' t a) -> Bool
neutralOrClosed List1 (SingleLevel' (Blocked Term))
bs , Level -> Integer
levelLowerBound Level
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Level -> Integer
levelLowerBound Level
b -> m ()
notok
(as :: List1 (SingleLevel' (Blocked Term))
as@(SingleLevel' (Blocked Term)
_ :| SingleLevel' (Blocked Term)
_ : [SingleLevel' (Blocked Term)]
_), SingleLevel' (Blocked Term)
b :| []) ->
List1 (SingleLevel' (Blocked Term))
-> (SingleLevel' (Blocked Term) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ List1 (SingleLevel' (Blocked Term))
as ((SingleLevel' (Blocked Term) -> m ()) -> m ())
-> (SingleLevel' (Blocked Term) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ SingleLevel' (Blocked Term)
a' -> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
leqLevel (SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel (SingleLevel' Term -> Level) -> SingleLevel' Term -> Level
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SingleLevel' (Blocked Term)
a')
(SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel (SingleLevel' Term -> Level) -> SingleLevel' Term -> Level
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SingleLevel' (Blocked Term)
b)
(List1 (SingleLevel' (Blocked Term))
as, List1 (SingleLevel' (Blocked Term))
bs)
| let minN :: Integer
minN = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min ((Integer, Level) -> Integer
forall a b. (a, b) -> a
fst ((Integer, Level) -> Integer) -> (Integer, Level) -> Integer
forall a b. (a -> b) -> a -> b
$ Level -> (Integer, Level)
levelPlusView Level
a) ((Integer, Level) -> Integer
forall a b. (a, b) -> a
fst ((Integer, Level) -> Integer) -> (Integer, Level) -> Integer
forall a b. (a -> b) -> a -> b
$ Level -> (Integer, Level)
levelPlusView Level
b)
a' :: Level
a' = Level -> Maybe Level -> Level
forall a. a -> Maybe a -> a
fromMaybe Level
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Level -> Level) -> Maybe Level -> Level
forall a b. (a -> b) -> a -> b
$ Integer -> Level -> Maybe Level
subLevel Integer
minN Level
a
b' :: Level
b' = Level -> Maybe Level -> Level
forall a. a -> Maybe a -> a
fromMaybe Level
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Level -> Level) -> Maybe Level -> Level
forall a b. (a -> b) -> a -> b
$ Integer -> Level -> Maybe Level
subLevel Integer
minN Level
b
, Integer
minN Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
leqLevel Level
a' Level
b'
(List1 (SingleLevel' (Blocked Term))
as, List1 (SingleLevel' (Blocked Term))
bs)
| (subsumed :: [SingleLevel' (Blocked Term)]
subsumed@(SingleLevel' (Blocked Term)
_:[SingleLevel' (Blocked Term)]
_) , [SingleLevel' (Blocked Term)]
as') <- (SingleLevel' (Blocked Term) -> Bool)
-> List1 (SingleLevel' (Blocked Term))
-> ([SingleLevel' (Blocked Term)], [SingleLevel' (Blocked Term)])
forall a. (a -> Bool) -> NonEmpty a -> ([a], [a])
List1.partition (SingleLevel' Term -> Bool
isSubsumed (SingleLevel' Term -> Bool)
-> (SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> SingleLevel' (Blocked Term)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking) List1 (SingleLevel' (Blocked Term))
as
-> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
leqLevel ([SingleLevel' Term] -> Level
unSingleLevels ([SingleLevel' Term] -> Level) -> [SingleLevel' Term] -> Level
forall a b. (a -> b) -> a -> b
$ ((SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> [SingleLevel' (Blocked Term)] -> [SingleLevel' Term]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> [SingleLevel' (Blocked Term)] -> [SingleLevel' Term])
-> ((Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> (Blocked Term -> Term)
-> [SingleLevel' (Blocked Term)]
-> [SingleLevel' Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking [SingleLevel' (Blocked Term)]
as') Level
b
where
isSubsumed :: SingleLevel' Term -> Bool
isSubsumed SingleLevel' Term
a = (SingleLevel' Term -> Bool) -> NonEmpty (SingleLevel' Term) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SingleLevel' Term -> SingleLevel' Term -> Bool
`subsumes` SingleLevel' Term
a) (NonEmpty (SingleLevel' Term) -> Bool)
-> NonEmpty (SingleLevel' Term) -> Bool
forall a b. (a -> b) -> a -> b
$ ((SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> List1 (SingleLevel' (Blocked Term))
-> NonEmpty (SingleLevel' Term)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> List1 (SingleLevel' (Blocked Term))
-> NonEmpty (SingleLevel' Term))
-> ((Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> (Blocked Term -> Term)
-> List1 (SingleLevel' (Blocked Term))
-> NonEmpty (SingleLevel' Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking List1 (SingleLevel' (Blocked Term))
bs
subsumes :: SingleLevel -> SingleLevel -> Bool
subsumes :: SingleLevel' Term -> SingleLevel' Term -> Bool
subsumes (SingleClosed Integer
m) (SingleClosed Integer
n) = Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n
subsumes (SinglePlus (Plus Integer
m Term
_)) (SingleClosed Integer
n) = Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n
subsumes (SinglePlus (Plus Integer
m Term
a)) (SinglePlus (Plus Integer
n Term
b)) = Term
a Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
b Bool -> Bool -> Bool
&& Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n
subsumes SingleLevel' Term
_ SingleLevel' Term
_ = Bool
False
(List1 (SingleLevel' (Blocked Term))
as , List1 (SingleLevel' (Blocked Term))
bs)
| Bool
cumulativity
, Bool -> Bool
not Bool
areWeComputingOverlap
, Just (mb :: Term
mb@(MetaV MetaId
x Elims
es) , [SingleLevel' Term]
bs') <- [SingleLevel' Term] -> Maybe (Term, [SingleLevel' Term])
singleMetaView ([SingleLevel' Term] -> Maybe (Term, [SingleLevel' Term]))
-> [SingleLevel' Term] -> Maybe (Term, [SingleLevel' Term])
forall a b. (a -> b) -> a -> b
$ ((SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> [SingleLevel' (Blocked Term)] -> [SingleLevel' Term]
forall a b. (a -> b) -> [a] -> [b]
map ((SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> [SingleLevel' (Blocked Term)] -> [SingleLevel' Term])
-> ((Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> (Blocked Term -> Term)
-> [SingleLevel' (Blocked Term)]
-> [SingleLevel' Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking (List1 (SingleLevel' (Blocked Term))
-> [Item (List1 (SingleLevel' (Blocked Term)))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (SingleLevel' (Blocked Term))
bs)
, [SingleLevel' Term] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SingleLevel' Term]
bs' Bool -> Bool -> Bool
|| (Term, Level) -> Bool
forall a. AllMetas a => a -> Bool
noMetas (Level -> Term
Level Level
a , [SingleLevel' Term] -> Level
unSingleLevels [SingleLevel' Term]
bs') -> do
mv <- MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
abort <- (isJust <$> isInteractionMeta x) `or2M`
((== YesGeneralizeVar) <$> isGeneralizableMeta x)
if | abort -> postpone
| otherwise -> do
x' <- case mvJudgement mv of
IsSort{} -> m MetaId
forall a. HasCallStack => a
__IMPOSSIBLE__
HasType MetaId
_ Comparison
cmp Type
t -> do
TelV tel t' <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
newMeta Instantiable (mvInfo mv) normalMetaPriority (idP $ size tel) $ HasType () cmp t
reportSDoc "tc.conv.level" 20 $ fsep
[ "attempting to solve" , prettyTCM (MetaV x es) , "to the maximum of"
, prettyTCM (Level a) , "and the fresh meta" , prettyTCM (MetaV x' es)
]
equalLevel (atomicLevel mb) $ levelLub a (atomicLevel $ MetaV x' es)
(List1 (SingleLevel' (Blocked Term)),
List1 (SingleLevel' (Blocked Term)))
_ | (Level, Level) -> Bool
forall a. AllMetas a => a -> Bool
noMetas (Level
a, Level
b) -> m ()
notok
| Bool
otherwise -> m ()
postpone
where
neutralOrClosed :: SingleLevel' (Blocked' t a) -> Bool
neutralOrClosed (SingleClosed Integer
_) = Bool
True
neutralOrClosed (SinglePlus (Plus Integer
_ NotBlocked{})) = Bool
True
neutralOrClosed SingleLevel' (Blocked' t a)
_ = Bool
False
singleMetaView :: [SingleLevel] -> Maybe (Term, [SingleLevel])
singleMetaView :: [SingleLevel' Term] -> Maybe (Term, [SingleLevel' Term])
singleMetaView (SinglePlus (Plus Integer
0 l :: Term
l@(MetaV MetaId
m Elims
es)) : [SingleLevel' Term]
ls)
| (SingleLevel' Term -> Bool) -> [SingleLevel' Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool)
-> (SingleLevel' Term -> Bool) -> SingleLevel' Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleLevel' Term -> Bool
isMetaLevel) [SingleLevel' Term]
ls = (Term, [SingleLevel' Term]) -> Maybe (Term, [SingleLevel' Term])
forall a. a -> Maybe a
Just (Term
l,[SingleLevel' Term]
ls)
singleMetaView (SingleLevel' Term
l : [SingleLevel' Term]
ls)
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SingleLevel' Term -> Bool
isMetaLevel SingleLevel' Term
l = ([SingleLevel' Term] -> [SingleLevel' Term])
-> (Term, [SingleLevel' Term]) -> (Term, [SingleLevel' Term])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (SingleLevel' Term
lSingleLevel' Term -> [SingleLevel' Term] -> [SingleLevel' Term]
forall a. a -> [a] -> [a]
:) ((Term, [SingleLevel' Term]) -> (Term, [SingleLevel' Term]))
-> Maybe (Term, [SingleLevel' Term])
-> Maybe (Term, [SingleLevel' Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SingleLevel' Term] -> Maybe (Term, [SingleLevel' Term])
singleMetaView [SingleLevel' Term]
ls
singleMetaView [SingleLevel' Term]
_ = Maybe (Term, [SingleLevel' Term])
forall a. Maybe a
Nothing
isMetaLevel :: SingleLevel -> Bool
isMetaLevel :: SingleLevel' Term -> Bool
isMetaLevel (SinglePlus (Plus Integer
_ MetaV{})) = Bool
True
isMetaLevel SingleLevel' Term
_ = Bool
False
{-# SPECIALIZE equalLevel :: Level -> Level -> TCM () #-}
equalLevel :: forall m. MonadConversion m => Level -> Level -> m ()
equalLevel :: forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
equalLevel Level
a Level
b = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"equalLevel", Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Level -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Level
a, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Level -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Level
b ]
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare levels"
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"equalLevel"
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Level -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM Level
a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=="
, Level -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM Level
b
]
]
]
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
80 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"equalLevel", Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Level -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Level
a, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Level -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Level
b ]
(a, b) <- (Level, Level) -> m (Level, Level)
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (Level
a, Level
b)
let (a', b') = removeSubsumed a b
SynEq.checkSyntacticEquality' a' b'
(\Level
_ Level
_ ->
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
60
TCMT IO Doc
"checkSyntacticEquality returns True") $ \Level
a Level
b -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
60 TCMT IO Doc
"checkSyntacticEquality returns False"
let notok :: m ()
notok = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM m Bool
forall (m :: * -> *). HasOptions m => m Bool
typeInType m ()
notOk
notOk :: m ()
notOk = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Level -> Level -> TypeError
UnequalLevel Comparison
CmpEq Level
a' Level
b'
postpone :: m ()
postpone = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang TCMT IO Doc
"postponing:" Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (Level -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Level
a' TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"==") Int
0 (Level -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Level
b')
blocker <- (Level, Level) -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn ((Level, Level) -> Blocker) -> m (Level, Level) -> m Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Level, Level) -> m (Level, Level)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Level
a', Level
b')
patternViolation blocker
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"equalLevel (w/o subsumed)"
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Level -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM Level
a' TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=="
, Level -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM Level
b'
]
]
]
let as :: NonEmpty (SingleLevel' Term)
as = Level -> NonEmpty (SingleLevel' Term)
forall t. Level' t -> List1 (SingleLevel' t)
levelMaxView Level
a'
bs :: NonEmpty (SingleLevel' Term)
bs = Level -> NonEmpty (SingleLevel' Term)
forall t. Level' t -> List1 (SingleLevel' t)
levelMaxView Level
b'
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"equalLevel"
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (SingleLevel' Term -> TCMT IO Doc)
-> NonEmpty (SingleLevel' Term) -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Level -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM (Level -> TCMT IO Doc)
-> (SingleLevel' Term -> Level) -> SingleLevel' Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel) NonEmpty (SingleLevel' Term)
as
, TCMT IO Doc
"=="
, NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (SingleLevel' Term -> TCMT IO Doc)
-> NonEmpty (SingleLevel' Term) -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Level -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM (Level -> TCMT IO Doc)
-> (SingleLevel' Term -> Level) -> SingleLevel' Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel) NonEmpty (SingleLevel' Term)
bs
]
]
]
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.level" Int
80 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"equalLevel"
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (SingleLevel' Term -> TCMT IO Doc)
-> NonEmpty (SingleLevel' Term) -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Level -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Level -> TCMT IO Doc)
-> (SingleLevel' Term -> Level) -> SingleLevel' Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel) NonEmpty (SingleLevel' Term)
as
, TCMT IO Doc
"=="
, NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (SingleLevel' Term -> TCMT IO Doc)
-> NonEmpty (SingleLevel' Term) -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Level -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Level -> TCMT IO Doc)
-> (SingleLevel' Term -> Level) -> SingleLevel' Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel) NonEmpty (SingleLevel' Term)
bs
]
]
]
as <- ((SingleLevel' Term -> m (SingleLevel' (Blocked Term)))
-> NonEmpty (SingleLevel' Term)
-> m (List1 (SingleLevel' (Blocked Term)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM ((SingleLevel' Term -> m (SingleLevel' (Blocked Term)))
-> NonEmpty (SingleLevel' Term)
-> m (List1 (SingleLevel' (Blocked Term))))
-> ((Term -> m (Blocked Term))
-> SingleLevel' Term -> m (SingleLevel' (Blocked Term)))
-> (Term -> m (Blocked Term))
-> NonEmpty (SingleLevel' Term)
-> m (List1 (SingleLevel' (Blocked Term)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> m (Blocked Term))
-> SingleLevel' Term -> m (SingleLevel' (Blocked Term))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
mapM) Term -> m (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB NonEmpty (SingleLevel' Term)
as
bs <- (mapM . mapM) reduceB bs
catchConstraint (LevelCmp CmpEq a b) $ case (as, bs) of
(SingleClosed Integer
m :| [], SingleClosed Integer
n :| [])
| Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise -> m ()
notok
(SingleClosed Integer
m :| [] , List1 (SingleLevel' (Blocked Term))
bs) | (SingleLevel' (Blocked Term) -> Bool)
-> List1 (SingleLevel' (Blocked Term)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SingleLevel' (Blocked Term) -> Bool
forall {t} {a}. SingleLevel' (Blocked' t a) -> Bool
isNeutral List1 (SingleLevel' (Blocked Term))
bs -> m ()
notok
(List1 (SingleLevel' (Blocked Term))
as , SingleClosed Integer
n :| []) | (SingleLevel' (Blocked Term) -> Bool)
-> List1 (SingleLevel' (Blocked Term)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SingleLevel' (Blocked Term) -> Bool
forall {t} {a}. SingleLevel' (Blocked' t a) -> Bool
isNeutral List1 (SingleLevel' (Blocked Term))
as -> m ()
notok
(SingleClosed Integer
m :| [] , List1 (SingleLevel' (Blocked Term))
_) | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Level -> Integer
levelLowerBound Level
b -> m ()
notok
(List1 (SingleLevel' (Blocked Term))
_ , SingleClosed Integer
n :| []) | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Level -> Integer
levelLowerBound Level
a -> m ()
notok
(SingleClosed Integer
0 :| [] , bs :: List1 (SingleLevel' (Blocked Term))
bs@(SingleLevel' (Blocked Term)
_ :| SingleLevel' (Blocked Term)
_ : [SingleLevel' (Blocked Term)]
_)) ->
List1 (SingleLevel' (Blocked Term))
-> (SingleLevel' (Blocked Term) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ List1 (SingleLevel' (Blocked Term))
bs ((SingleLevel' (Blocked Term) -> m ()) -> m ())
-> (SingleLevel' (Blocked Term) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ SingleLevel' (Blocked Term)
b' -> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
equalLevel (Integer -> Level
ClosedLevel Integer
0) (SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel (SingleLevel' Term -> Level) -> SingleLevel' Term -> Level
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SingleLevel' (Blocked Term)
b')
(as :: List1 (SingleLevel' (Blocked Term))
as@(SingleLevel' (Blocked Term)
_ :| SingleLevel' (Blocked Term)
_ : [SingleLevel' (Blocked Term)]
_) , SingleClosed Integer
0 :| []) ->
List1 (SingleLevel' (Blocked Term))
-> (SingleLevel' (Blocked Term) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ List1 (SingleLevel' (Blocked Term))
as ((SingleLevel' (Blocked Term) -> m ()) -> m ())
-> (SingleLevel' (Blocked Term) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ SingleLevel' (Blocked Term)
a' -> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
equalLevel (SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel (SingleLevel' Term -> Level) -> SingleLevel' Term -> Level
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SingleLevel' (Blocked Term)
a') (Integer -> Level
ClosedLevel Integer
0)
(SinglePlus (Plus Integer
k Blocked Term
a) :| [] , SinglePlus (Plus Integer
l Blocked Term
b) :| [])
| MetaV MetaId
x Elims
as' <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
a
, MetaV MetaId
y Elims
bs' <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
b
, Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
l -> do
lvl <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType'
compareMetas CmpEq (AsTermsOf lvl) x as' y bs'
(SinglePlus (Plus Integer
k Blocked Term
a) :| [] , List1 (SingleLevel' (Blocked Term))
_)
| MetaV MetaId
x Elims
as' <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
a
, Just Level
b' <- Integer -> Level -> Maybe Level
subLevel Integer
k Level
b -> MetaId -> Elims -> Level -> m ()
forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh Int m) =>
MetaId -> Elims -> Level -> m ()
meta MetaId
x Elims
as' Level
b'
(List1 (SingleLevel' (Blocked Term))
_ , SinglePlus (Plus Integer
l Blocked Term
b) :| [])
| MetaV MetaId
y Elims
bs' <- Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
b
, Just Level
a' <- Integer -> Level -> Maybe Level
subLevel Integer
l Level
a -> MetaId -> Elims -> Level -> m ()
forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh Int m) =>
MetaId -> Elims -> Level -> m ()
meta MetaId
y Elims
bs' Level
a'
(List1 (SingleLevel' (Blocked Term)),
List1 (SingleLevel' (Blocked Term)))
_ | Just Level
a' <- Level -> Level -> Maybe Level
levelMaxDiff Level
a Level
b
, Level
b Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer -> Level
ClosedLevel Integer
0 -> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
leqLevel Level
a' Level
b
(List1 (SingleLevel' (Blocked Term)),
List1 (SingleLevel' (Blocked Term)))
_ | Just Level
b' <- Level -> Level -> Maybe Level
levelMaxDiff Level
b Level
a
, Level
a Level -> Level -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer -> Level
ClosedLevel Integer
0 -> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
leqLevel Level
b' Level
a
(List1 (SingleLevel' (Blocked Term))
as , List1 (SingleLevel' (Blocked Term))
bs)
| (SingleLevel' (Blocked Term) -> Bool)
-> List1 (SingleLevel' (Blocked Term)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SingleLevel' (Blocked Term) -> Bool
forall {t} {a}. SingleLevel' (Blocked' t a) -> Bool
isNeutralOrClosed (List1 (SingleLevel' (Blocked Term))
as List1 (SingleLevel' (Blocked Term))
-> List1 (SingleLevel' (Blocked Term))
-> List1 (SingleLevel' (Blocked Term))
forall a. Semigroup a => a -> a -> a
<> List1 (SingleLevel' (Blocked Term))
bs)
, Bool -> Bool
not ((SingleLevel' (Blocked Term) -> Bool)
-> List1 (SingleLevel' (Blocked Term)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SingleLevel' (Blocked Term) -> Bool
forall {a} {t}. AllMetas a => SingleLevel' (Blocked' t a) -> Bool
hasMeta (List1 (SingleLevel' (Blocked Term))
as List1 (SingleLevel' (Blocked Term))
-> List1 (SingleLevel' (Blocked Term))
-> List1 (SingleLevel' (Blocked Term))
forall a. Semigroup a => a -> a -> a
<> List1 (SingleLevel' (Blocked Term))
bs))
, List1 (SingleLevel' (Blocked Term)) -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 (SingleLevel' (Blocked Term))
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== List1 (SingleLevel' (Blocked Term)) -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 (SingleLevel' (Blocked Term))
bs -> do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.conv.level" Int
60 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"equalLevel: all are neutral or closed"
(SingleLevel' (Blocked Term)
-> SingleLevel' (Blocked Term) -> m ())
-> List1 (SingleLevel' (Blocked Term))
-> List1 (SingleLevel' (Blocked Term))
-> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> List1 a -> List1 b -> m ()
List1.zipWithM_ (Term -> Term -> m ()
forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh Int m) =>
Term -> Term -> m ()
(===) (Term -> Term -> m ())
-> (SingleLevel' (Blocked Term) -> Term)
-> SingleLevel' (Blocked Term)
-> SingleLevel' (Blocked Term)
-> m ()
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Level -> Term
levelTm (Level -> Term)
-> (SingleLevel' (Blocked Term) -> Level)
-> SingleLevel' (Blocked Term)
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel (SingleLevel' Term -> Level)
-> (SingleLevel' (Blocked Term) -> SingleLevel' Term)
-> SingleLevel' (Blocked Term)
-> Level
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Blocked Term -> Term)
-> SingleLevel' (Blocked Term) -> SingleLevel' Term
forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking) List1 (SingleLevel' (Blocked Term))
as List1 (SingleLevel' (Blocked Term))
bs
(List1 (SingleLevel' (Blocked Term)),
List1 (SingleLevel' (Blocked Term)))
_ | (Level, Level) -> Bool
forall a. AllMetas a => a -> Bool
noMetas (Level
a , Level
b) -> m ()
notok
| Bool
otherwise -> m ()
postpone
where
Term
a === :: Term -> Term -> m ()
=== Term
b = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM m Bool
forall (m :: * -> *). HasOptions m => m Bool
typeInType (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
lvl <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType'
equalAtom (AsTermsOf lvl) a b
meta :: MetaId -> Elims -> Level -> m ()
meta MetaId
x Elims
as Level
b = do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.meta.level" Int
30 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Assigning meta level"
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.meta.level" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"meta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim' Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Elims
as, Level -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Level
b]
lvl <- m Type
forall (m :: * -> *). HasBuiltins m => m Type
levelType'
assignE DirEq x as (levelTm b) (AsTermsOf lvl) (===)
isNeutral :: SingleLevel' (Blocked' t a) -> Bool
isNeutral (SinglePlus (Plus Integer
_ NotBlocked{})) = Bool
True
isNeutral SingleLevel' (Blocked' t a)
_ = Bool
False
isNeutralOrClosed :: SingleLevel' (Blocked' t a) -> Bool
isNeutralOrClosed (SingleClosed Integer
_) = Bool
True
isNeutralOrClosed (SinglePlus (Plus Integer
_ NotBlocked{})) = Bool
True
isNeutralOrClosed SingleLevel' (Blocked' t a)
_ = Bool
False
hasMeta :: SingleLevel' (Blocked' t a) -> Bool
hasMeta (SinglePlus (Plus Integer
_ Blocked{})) = Bool
True
hasMeta (SinglePlus (Plus Integer
_ Blocked' t a
a)) = Maybe MetaId -> Bool
forall a. Maybe a -> Bool
isJust (Maybe MetaId -> Bool) -> Maybe MetaId -> Bool
forall a b. (a -> b) -> a -> b
$ a -> Maybe MetaId
forall a. AllMetas a => a -> Maybe MetaId
firstMeta (a -> Maybe MetaId) -> a -> Maybe MetaId
forall a b. (a -> b) -> a -> b
$ Blocked' t a -> a
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' t a
a
hasMeta (SingleClosed Integer
_) = Bool
False
removeSubsumed :: Level -> Level -> (Level, Level)
removeSubsumed Level
a Level
b =
let as :: [Item (NonEmpty (SingleLevel' Term))]
as = NonEmpty (SingleLevel' Term)
-> [Item (NonEmpty (SingleLevel' Term))]
forall l. IsList l => l -> [Item l]
List1.toList (NonEmpty (SingleLevel' Term)
-> [Item (NonEmpty (SingleLevel' Term))])
-> NonEmpty (SingleLevel' Term)
-> [Item (NonEmpty (SingleLevel' Term))]
forall a b. (a -> b) -> a -> b
$ Level -> NonEmpty (SingleLevel' Term)
forall t. Level' t -> List1 (SingleLevel' t)
levelMaxView Level
a
bs :: [Item (NonEmpty (SingleLevel' Term))]
bs = NonEmpty (SingleLevel' Term)
-> [Item (NonEmpty (SingleLevel' Term))]
forall l. IsList l => l -> [Item l]
List1.toList (NonEmpty (SingleLevel' Term)
-> [Item (NonEmpty (SingleLevel' Term))])
-> NonEmpty (SingleLevel' Term)
-> [Item (NonEmpty (SingleLevel' Term))]
forall a b. (a -> b) -> a -> b
$ Level -> NonEmpty (SingleLevel' Term)
forall t. Level' t -> List1 (SingleLevel' t)
levelMaxView Level
b
a' :: Level
a' = [SingleLevel' Term] -> Level
unSingleLevels ([SingleLevel' Term] -> Level) -> [SingleLevel' Term] -> Level
forall a b. (a -> b) -> a -> b
$ (SingleLevel' Term -> Bool)
-> [SingleLevel' Term] -> [SingleLevel' Term]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (SingleLevel' Term -> Bool) -> SingleLevel' Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SingleLevel' Term -> [SingleLevel' Term] -> Bool
forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
SingleLevel' a -> t (SingleLevel' a) -> Bool
`isStrictlySubsumedBy` [Item (NonEmpty (SingleLevel' Term))]
[SingleLevel' Term]
bs)) [Item (NonEmpty (SingleLevel' Term))]
[SingleLevel' Term]
as
b' :: Level
b' = [SingleLevel' Term] -> Level
unSingleLevels ([SingleLevel' Term] -> Level) -> [SingleLevel' Term] -> Level
forall a b. (a -> b) -> a -> b
$ (SingleLevel' Term -> Bool)
-> [SingleLevel' Term] -> [SingleLevel' Term]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (SingleLevel' Term -> Bool) -> SingleLevel' Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SingleLevel' Term -> [SingleLevel' Term] -> Bool
forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
SingleLevel' a -> t (SingleLevel' a) -> Bool
`isStrictlySubsumedBy` [Item (NonEmpty (SingleLevel' Term))]
[SingleLevel' Term]
as)) [Item (NonEmpty (SingleLevel' Term))]
[SingleLevel' Term]
bs
in (Level
a',Level
b')
SingleLevel' a
x isStrictlySubsumedBy :: SingleLevel' a -> t (SingleLevel' a) -> Bool
`isStrictlySubsumedBy` t (SingleLevel' a)
ys = (SingleLevel' a -> Bool) -> t (SingleLevel' a) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SingleLevel' a -> SingleLevel' a -> Bool
forall {a}. Eq a => SingleLevel' a -> SingleLevel' a -> Bool
`strictlySubsumes` SingleLevel' a
x) t (SingleLevel' a)
ys
SingleClosed Integer
m strictlySubsumes :: SingleLevel' a -> SingleLevel' a -> Bool
`strictlySubsumes` SingleClosed Integer
n = Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n
SinglePlus (Plus Integer
m a
a) `strictlySubsumes` SingleClosed Integer
n = Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n
SinglePlus (Plus Integer
m a
a) `strictlySubsumes` SinglePlus (Plus Integer
n a
b) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b Bool -> Bool -> Bool
&& Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n
SingleLevel' a
_ `strictlySubsumes` SingleLevel' a
_ = Bool
False
{-# SPECIALIZE equalSort :: Sort -> Sort -> TCM () #-}
equalSort :: forall m. MonadConversion m => Sort -> Sort -> m ()
equalSort :: forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s1 Sort
s2 = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"equalSort"
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=="
, Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2 ]
]
]
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ TCMT IO Doc
"equalSort"
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ Sort -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Sort
s1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=="
, Sort -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Sort
s2 ]
]
]
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare sorts"
Sort -> Sort -> String -> m () -> m ()
forall (m :: * -> *) a.
MonadConversion m =>
a -> a -> String -> m () -> m ()
guardPointerEquality Sort
s1 Sort
s2 String
"pointer equality: sorts" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Sort
-> Sort -> (Sort -> Sort -> m ()) -> (Sort -> Sort -> m ()) -> m ()
forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
SynEq.checkSyntacticEquality Sort
s1 Sort
s2 (\Sort
_ Sort
_ -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((Sort -> Sort -> m ()) -> m ()) -> (Sort -> Sort -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Sort
s1 Sort
s2 -> do
s1b <- Sort -> m (Blocked Sort)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Sort
s1
s2b <- reduceB s2
let (s1,s2) = (ignoreBlocking s1b, ignoreBlocking s2b)
blocker = Blocker -> Blocker -> Blocker
unblockOnEither (Blocked Sort -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Sort
s1b) (Blocked Sort -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Sort
s2b)
let postponeIfBlocked = (Blocker -> m ()) -> m () -> m ()
forall a. (Blocker -> m a) -> m a -> m a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr ((Blocker -> m ()) -> m () -> m ())
-> (Blocker -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ \Blocker
blocker -> do
if | Blocker
blocker Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
neverUnblock -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> TypeError
UnequalSorts Sort
s1 Sort
s2
| Bool
otherwise -> do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"Postponing constraint"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=="
, Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2 ]
]
blocker <- Blocker -> m Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker Blocker
blocker
addConstraint blocker $ SortCmp CmpEq s1 s2
propEnabled <- isPropEnabled
typeInTypeEnabled <- typeInType
omegaInOmegaEnabled <- optOmegaInOmega <$> pragmaOptions
let infInInf = Bool
typeInTypeEnabled Bool -> Bool -> Bool
|| Bool
omegaInOmegaEnabled
postponeIfBlocked $ case (s1, s2) of
(DummyS String
s, Sort
_) -> String -> m ()
forall {m :: * -> *} {a} {b}.
(ReportS [a], MonadDebug m, IsString a) =>
a -> m b
impossibleSort String
s
(Sort
_, DummyS String
s) -> String -> m ()
forall {m :: * -> *} {a} {b}.
(ReportS [a], MonadDebug m, IsString a) =>
a -> m b
impossibleSort String
s
(MetaS MetaId
x Elims
es , MetaS MetaId
y Elims
es') -> Comparison
-> CompareAs -> MetaId -> Elims -> MetaId -> Elims -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison
-> CompareAs -> MetaId -> Elims -> MetaId -> Elims -> m ()
compareMetas Comparison
CmpEq CompareAs
AsTypes MetaId
x Elims
es MetaId
y Elims
es'
(MetaS MetaId
x Elims
es , Sort
_ ) -> MetaId -> Elims -> Sort -> m ()
meta MetaId
x Elims
es Sort
s2
(Sort
_ , MetaS MetaId
x Elims
es ) -> MetaId -> Elims -> Sort -> m ()
meta MetaId
x Elims
es Sort
s1
(Univ Univ
u Level
a , Univ Univ
u' Level
b ) | Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u' -> Level -> Level -> m ()
forall (m :: * -> *). MonadConversion m => Level -> Level -> m ()
equalLevel Level
a Level
b m () -> m () -> m ()
forall {m :: * -> *} {a}. MonadError TCErr m => m a -> m a -> m a
`catchInequalLevel` m ()
forall {a}. m a
no
(Sort
SizeUniv , Sort
SizeUniv ) -> m ()
yes
(Sort
LockUniv , Sort
LockUniv ) -> m ()
yes
(Sort
LevelUniv , Sort
LevelUniv ) -> m ()
yes
(Sort
IntervalUniv , Sort
IntervalUniv) -> m ()
yes
(Inf Univ
u Integer
m , Inf Univ
u' Integer
n ) ->
if Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u' Bool -> Bool -> Bool
&& (Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n Bool -> Bool -> Bool
|| Bool
infInInf) then m ()
yes else m ()
forall {a}. m a
no
(Univ Univ
u Level
_ , Inf Univ
u' Integer
_ ) -> Bool -> m ()
answer (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u' Bool -> Bool -> Bool
&& Bool
typeInTypeEnabled
(Inf Univ
u Integer
_ , Univ Univ
u' Level
_ ) -> Bool -> m ()
answer (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u' Bool -> Bool -> Bool
&& Bool
typeInTypeEnabled
(Sort
s1 , PiSort Dom' Term Term
a Sort
b Abs Sort
c) -> Bool
-> Sort -> Dom' Term Term -> Sort -> Abs Sort -> Blocker -> m ()
piSortEquals Bool
propEnabled Sort
s1 Dom' Term Term
a Sort
b Abs Sort
c Blocker
blocker
(PiSort Dom' Term Term
a Sort
b Abs Sort
c , Sort
s2) -> Bool
-> Sort -> Dom' Term Term -> Sort -> Abs Sort -> Blocker -> m ()
piSortEquals Bool
propEnabled Sort
s2 Dom' Term Term
a Sort
b Abs Sort
c Blocker
blocker
(Sort
s1 , FunSort Sort
a Sort
b) -> Bool -> Sort -> Sort -> Sort -> Blocker -> m ()
funSortEquals Bool
propEnabled Sort
s1 Sort
a Sort
b Blocker
blocker
(FunSort Sort
a Sort
b , Sort
s2) -> Bool -> Sort -> Sort -> Sort -> Blocker -> m ()
funSortEquals Bool
propEnabled Sort
s2 Sort
a Sort
b Blocker
blocker
(Sort
s1 , UnivSort Sort
s2) -> Bool -> Bool -> Sort -> Sort -> Blocker -> m ()
univSortEquals Bool
propEnabled Bool
infInInf Sort
s1 Sort
s2 Blocker
blocker
(UnivSort Sort
s1 , Sort
s2 ) -> Bool -> Bool -> Sort -> Sort -> Blocker -> m ()
univSortEquals Bool
propEnabled Bool
infInInf Sort
s2 Sort
s1 Blocker
blocker
(DefS QName
d Elims
es , DefS QName
d' Elims
es')
| QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
d' -> do
pol <- Comparison -> QName -> m [Polarity]
forall (m :: * -> *).
HasConstInfo m =>
Comparison -> QName -> m [Polarity]
getPolarity' Comparison
CmpEq QName
d
a <- computeElimHeadType d es es'
compareElims pol [] a (Def d []) es es'
| Bool
otherwise -> m ()
forall {a}. m a
no
(Sort
_ , Sort
_ ) -> m ()
forall {a}. m a
no
where
yes :: m ()
yes = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
no :: m a
no = Blocker -> m a
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
answer :: Bool -> m ()
answer = \case
Bool
True -> m ()
yes
Bool
False -> m ()
forall {a}. m a
no
meta :: MetaId -> [Elim' Term] -> Sort -> m ()
meta :: MetaId -> Elims -> Sort -> m ()
meta MetaId
x Elims
es Sort
s = do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"tc.meta.sort" Int
30 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Assigning meta sort"
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.meta.sort" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"meta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [MetaId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
x, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Elim' Term -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim' Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Elims
es, Sort -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Sort
s]
CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
forall (m :: * -> *).
MonadConversion m =>
CompareDirection
-> MetaId
-> Elims
-> Term
-> CompareAs
-> (Term -> Term -> m ())
-> m ()
assignE CompareDirection
DirEq MetaId
x Elims
es (Sort -> Term
Sort Sort
s) CompareAs
AsTypes Term -> Term -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
invertibleSort :: Bool -> Univ -> Bool
invertibleSort :: Bool -> Univ -> Bool
invertibleSort Bool
propEnabled = \case
Univ
USSet -> Bool
True
Univ
UType -> Bool -> Bool
not Bool
propEnabled
Univ
UProp -> Bool
False
univSortEquals :: Bool -> Bool -> Sort -> Sort -> Blocker -> m ()
univSortEquals :: Bool -> Bool -> Sort -> Sort -> Blocker -> m ()
univSortEquals Bool
propEnabled Bool
infInInf Sort
s1 Sort
s2 Blocker
blocker = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
35 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"univSortEquals"
, TCMT IO Doc
" s1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1
, TCMT IO Doc
" s2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2
]
let postpone :: m ()
postpone = Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
case Sort
s1 of
Prop{} -> m ()
forall {a}. m a
no
Inf Univ
UProp Integer
_ -> m ()
forall {a}. m a
no
SizeUniv{} -> m ()
forall {a}. m a
no
LevelUniv{} -> m ()
forall {a}. m a
no
LockUniv{} -> m ()
forall {a}. m a
no
IntervalUniv{} -> m ()
forall {a}. m a
no
Type Level
l1 -> do
levelUnivEnabled <- PragmaOptions -> Bool
optLevelUniverse (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
guardedEnabled <- optGuarded <$> pragmaOptions
if | Inf _ _n <- s2 -> __IMPOSSIBLE__
| SizeUniv <- s2 -> __IMPOSSIBLE__
| Univ USSet _ <- s2 -> __IMPOSSIBLE__
| IntervalUniv <- s2 -> __IMPOSSIBLE__
| not (propEnabled || guardedEnabled || levelUnivEnabled) -> do
l2 <- case subLevel 1 l1 of
Just Level
l2 -> Level -> m Level
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Level
l2
Maybe Level
Nothing -> do
l2 <- m Level
forall (m :: * -> *). MonadMetaSolver m => m Level
newLevelMeta
equalLevel l1 (levelSuc l2)
return l2
equalSort (Type l2) s2
| otherwise -> postpone
Inf Univ
u Integer
0 -> do
sizedTypesEnabled <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption
case concat
[ [ s1 | u /= UProp, infInInf ]
, [ dummy | u == UType, infInInf, propEnabled, let dummy = Univ -> Integer -> Sort' t
forall t. Univ -> Integer -> Sort' t
Inf Univ
UProp Integer
0 ]
, [ SizeUniv | u == UType, sizedTypesEnabled ]
]
of
[ Sort
s ] -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s Sort
s2
[] -> m ()
forall {a}. m a
no
[Sort]
_ -> m ()
postpone
Inf Univ
u Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0, Bool -> Univ -> Bool
invertibleSort Bool
propEnabled Univ
u ->
Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
u (Integer -> Sort) -> Integer -> Sort
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Sort
s2
Sort
_ -> m ()
postpone
piSortEquals :: Bool -> Sort -> Dom Term -> Sort -> Abs Sort -> Blocker -> m ()
piSortEquals :: Bool
-> Sort -> Dom' Term Term -> Sort -> Abs Sort -> Blocker -> m ()
piSortEquals Bool
propEnabled Sort
s Dom' Term Term
a Sort
s1 NoAbs{} Blocker
blocker = m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
piSortEquals Bool
propEnabled Sort
s Dom' Term Term
a Sort
s1 s2Abs :: Abs Sort
s2Abs@(Abs String
x Sort
s2) Blocker
blocker = do
let adom :: Dom Type
adom = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s1 (Term -> Type) -> Dom' Term Term -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom' Term Term
a
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
35 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"piSortEquals"
, TCMT IO Doc
" s =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s
, TCMT IO Doc
" a =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Dom Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Dom Type -> m Doc
prettyTCM Dom Type
adom
, TCMT IO Doc
" s1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1
, TCMT IO Doc
" s2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (String, Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(String, Dom Type) -> m a -> m a
addContext (String
x,Dom Type
adom) (Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2)
]
let postpone :: m ()
postpone = Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
if | Sort -> Bool
isSmallSort Sort
s -> do
s2' <- m Sort
forall (m :: * -> *). MonadMetaSolver m => m Sort
newSortMeta
addContext (x , adom) $ equalSort s2 (raise 1 s2')
funSortEquals propEnabled s s1 s2' blocker
| Bool
otherwise -> m ()
postpone
funSortEquals :: Bool -> Sort -> Sort -> Sort -> Blocker -> m ()
funSortEquals :: Bool -> Sort -> Sort -> Sort -> Blocker -> m ()
funSortEquals Bool
propEnabled Sort
s0 Sort
s1 Sort
s2 Blocker
blocker = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.sort" Int
35 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"funSortEquals"
, TCMT IO Doc
" s0 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s0
, TCMT IO Doc
" s1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1
, TCMT IO Doc
" s2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Sort -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2
]
sizedTypesEnabled <- m Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption
cubicalEnabled <- isJust <$> cubicalOption
levelUnivEnabled <- optLevelUniverse <$> pragmaOptions
let postpone = Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
err :: m ()
err = TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> TypeError
UnequalSorts Sort
s0 (Sort -> Sort -> Sort
forall t. Sort' t -> Sort' t -> Sort' t
FunSort Sort
s1 Sort
s2)
case s0 of
Inf Univ
u Integer
n ->
case (Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s1, Sort -> Either Blocker SizeOfSort
sizeOfSort Sort
s2) of
(Right (SizeOfSort Univ
u' Integer
n'), Either Blocker SizeOfSort
_)
| Integer
n' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n -> m ()
err
| Univ -> IsFibrant
univFibrancy Univ
u' IsFibrant -> IsFibrant -> Bool
forall a. Ord a => a -> a -> Bool
> Univ -> IsFibrant
univFibrancy Univ
u -> m ()
err
(Either Blocker SizeOfSort
_, Right (SizeOfSort Univ
u' Integer
n'))
| Integer
n' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n -> m ()
err
| Univ -> IsFibrant
univFibrancy Univ
u' IsFibrant -> IsFibrant -> Bool
forall a. Ord a => a -> a -> Bool
> Univ -> IsFibrant
univFibrancy Univ
u -> m ()
err
| Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
/= Univ
USSet, Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
/= Univ
u' -> m ()
err
(Right (SizeOfSort Univ
u1 Integer
n1), Right (SizeOfSort Univ
u2 Integer
n2))
| Integer
n1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n, Integer
n2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n -> m ()
err
| Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
/= Univ -> Univ -> Univ
funUniv Univ
u1 Univ
u2 -> m ()
err
(Right (SizeOfSort Univ
u' Integer
n'), Either Blocker SizeOfSort
_)
| Univ
u' Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
/= Univ
USSet, Integer
n' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s0 Sort
s2
| Bool
otherwise -> m ()
postpone
(Either Blocker SizeOfSort
_, Right (SizeOfSort Univ
USSet Integer
n')) -> m ()
postpone
(Either Blocker SizeOfSort
_, Right (SizeOfSort Univ
_ Integer
n'))
| Integer
n' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n, Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
USSet -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
s1 Sort
s2
| Integer
n' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
n, Bool -> Bool
not Bool
propEnabled,
Bool -> Bool
not Bool
levelUnivEnabled Bool -> Bool -> Bool
|| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort (Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
UType Integer
n) Sort
s1
| Bool
otherwise -> m ()
postpone
(Either Blocker SizeOfSort, Either Blocker SizeOfSort)
_ -> m ()
postpone
Type Level
l -> do
l2 <- Univ -> Sort -> m Level
forceUniv Univ
UType Sort
s2
leqLevel l2 l
s1b <- reduceB s1
let s1 = Blocked Sort -> Sort
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
s1b
blocker = Blocked Sort -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Sort
s1b
if | propEnabled || cubicalEnabled ->
case funSort' s1 (Type l2) of
Right Sort
s -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort (Level -> Sort
forall t. Level' t -> Sort' t
Type Level
l) Sort
s
Left{} -> Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
| otherwise -> do
l1 <- forceUniv UType s1
equalLevel l (levelLub l1 l2)
Prop Level
l -> do
l2 <- Univ -> Sort -> m Level
forceUniv Univ
UProp Sort
s2
leqLevel l2 l
s1b <- reduceB s1
let s1 = Blocked Sort -> Sort
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Sort
s1b
blocker = Blocked Sort -> Blocker
forall t a. Blocked' t a -> Blocker
getBlocker Blocked Sort
s1b
case funSort' s1 (Prop l2) of
Right Sort
s -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort (Level -> Sort
forall t. Level' t -> Sort' t
Prop Level
l) Sort
s
Left Blocker
_ -> Blocker -> m ()
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
Sort
SizeUniv -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
forall {t}. Sort' t
SizeUniv Sort
s2
Sort
LevelUniv -> Sort -> Sort -> m ()
forall (m :: * -> *). MonadConversion m => Sort -> Sort -> m ()
equalSort Sort
forall {t}. Sort' t
LevelUniv Sort
s2
Sort
_ -> m ()
postpone
forceUniv :: Univ -> Sort -> m Level
forceUniv :: Univ -> Sort -> m Level
forceUniv Univ
u = \case
Univ Univ
u' Level
l | Univ
u Univ -> Univ -> Bool
forall a. Eq a => a -> a -> Bool
== Univ
u' -> Level -> m Level
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Level
l
Sort
s -> do
l <- m Level
forall (m :: * -> *). MonadMetaSolver m => m Level
newLevelMeta
equalSort s (Univ u l)
return l
impossibleSort :: a -> m b
impossibleSort a
s = do
String -> Int -> [a] -> m ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
forall (m :: * -> *). MonadDebug m => String -> Int -> [a] -> m ()
reportS String
"impossible" Int
10
[ a
"equalSort: found dummy sort with description:"
, a
s
]
m b
forall a. HasCallStack => a
__IMPOSSIBLE__
catchInequalLevel :: m a -> m a -> m a
catchInequalLevel m a
m m a
fail = m a
m m a -> (TCErr -> m a) -> m a
forall a. m a -> (TCErr -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \case
TypeError{} -> m a
fail
TCErr
err -> TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
forallFaceMaps
:: MonadConversion m
=> Term
-> (IntMap Bool -> Blocker -> Term -> m a)
-> (IntMap Bool -> Substitution -> m a)
-> m [a]
forallFaceMaps :: forall (m :: * -> *) a.
MonadConversion m =>
Term
-> (IntMap Bool -> Blocker -> Term -> m a)
-> (IntMap Bool -> Substitution -> m a)
-> m [a]
forallFaceMaps Term
t IntMap Bool -> Blocker -> Term -> m a
kb IntMap Bool -> Substitution -> m a
k = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"conv.forall" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [TCMT IO Doc
"forallFaceMaps"
, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t
]
as <- Term -> m [(IntMap Bool, [Term])]
forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap Bool, [Term])]
decomposeInterval Term
t
boolToI <- do
io <- primIOne
iz <- primIZero
return (\Bool
b -> if Bool
b then Term
io else Term
iz)
forM as $ \ (IntMap Bool
ms,[Term]
ts) -> do
[Term]
-> (Blocker -> Term -> m a) -> (NotBlocked -> Term -> m a) -> m a
forall {m :: * -> *} {t :: * -> *} {b}.
(HasBuiltins m, MonadError TCErr m, Foldable t, MonadReduce m) =>
t Term
-> (Blocker -> Term -> m b) -> (NotBlocked -> Term -> m b) -> m b
ifBlockeds [Term]
ts (IntMap Bool -> Blocker -> Term -> m a
kb IntMap Bool
ms) ((NotBlocked -> Term -> m a) -> m a)
-> (NotBlocked -> Term -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
_ -> do
let xs :: [(Int, Term)]
xs = ((Int, Bool) -> (Int, Term)) -> [(Int, Bool)] -> [(Int, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ((Bool -> Term) -> (Int, Bool) -> (Int, Term)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Bool -> Term
boolToI) ([(Int, Bool)] -> [(Int, Term)]) -> [(Int, Bool)] -> [(Int, Term)]
forall a b. (a -> b) -> a -> b
$ IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
IntMap.toAscList IntMap Bool
ms
cxt <- m Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
reportSDoc "conv.forall" 20 $
fsep ["substContextN"
, prettyTCM cxt
, prettyTCM xs
]
(cxt',sigma) <- substContextN cxt xs
resolved <- forM xs (\ (Int
i,Term
t) -> (,) (Dom' Term (Name, Type) -> Term -> (Dom' Term (Name, Type), Term))
-> m (Dom' Term (Name, Type))
-> m (Term -> (Dom' Term (Name, Type), Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Dom' Term (Name, Type))
forall (m :: * -> *).
(MonadFail m, MonadTCEnv m) =>
Int -> m (Dom' Term (Name, Type))
lookupBV Int
i m (Term -> (Dom' Term (Name, Type), Term))
-> m Term -> m (Dom' Term (Name, Type), Term)
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. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
sigma Term
t))
updateContext sigma (const cxt') $
addBindings resolved $ do
cl <- buildClosure ()
tel <- getContextTelescope
m <- currentModule
sub <- getModuleParameterSub m
reportSDoc "conv.forall" 30 $ vcat
[ text (replicate 10 '-')
, prettyTCM (envCurrentModule $ clEnv cl)
, prettyTCM tel
, prettyTCM sigma
, prettyTCM m
, prettyTCM sub
]
k ms sigma
where
ifBlockeds :: t Term
-> (Blocker -> Term -> m b) -> (NotBlocked -> Term -> m b) -> m b
ifBlockeds t Term
ts Blocker -> Term -> m b
blocked NotBlocked -> Term -> m b
unblocked = do
and <- PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
PrimIMin
io <- primIOne
let t = (Term -> Term -> Term) -> Term -> t Term -> Term
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Term
x Term
r -> Term
and Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
x,Term -> Arg Term
forall e. e -> Arg e
argN Term
r]) Term
io t Term
ts
ifBlocked t blocked unblocked
addBindings :: [(Dom' t (Name, Type), Term)] -> m a -> m a
addBindings [] m a
m = m a
m
addBindings ((Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info,unDom :: forall t e. Dom' t e -> e
unDom = (Name
nm,Type
ty)},Term
t):[(Dom' t (Name, Type), Term)]
bs) m a
m = ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Origin -> Name -> Term -> Type -> m a -> m a
addLetBinding ArgInfo
info Origin
Inserted Name
nm Term
t Type
ty ([(Dom' t (Name, Type), Term)] -> m a -> m a
addBindings [(Dom' t (Name, Type), Term)]
bs m a
m)
substContextN :: MonadConversion m => Context -> [(Int,Term)] -> m (Context , Substitution)
substContextN :: forall (m :: * -> *).
MonadConversion m =>
Context -> [(Int, Term)] -> m (Context, Substitution)
substContextN Context
c [] = (Context, Substitution) -> m (Context, Substitution)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Context
c, Substitution
forall a. Substitution' a
idS)
substContextN Context
c ((Int
i,Term
t):[(Int, Term)]
xs) = do
(c', sigma) <- Int -> Term -> Context -> m (Context, Substitution)
forall (m :: * -> *).
MonadConversion m =>
Int -> Term -> Context -> m (Context, Substitution)
substContext Int
i Term
t Context
c
(c'', sigma') <- substContextN c' (map (subtract 1 -*- applySubst sigma) xs)
return (c'', applySubst sigma' sigma)
substContext :: MonadConversion m => Int -> Term -> Context -> m (Context , Substitution)
substContext :: forall (m :: * -> *).
MonadConversion m =>
Int -> Term -> Context -> m (Context, Substitution)
substContext Int
i Term
t [] = m (Context, Substitution)
forall a. HasCallStack => a
__IMPOSSIBLE__
substContext Int
i Term
t (Dom' Term (Name, Type)
x:Context
xs) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = (Context, Substitution) -> m (Context, Substitution)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Context, Substitution) -> m (Context, Substitution))
-> (Context, Substitution) -> m (Context, Substitution)
forall a b. (a -> b) -> a -> b
$ (Context
xs , Int -> Term -> Substitution
forall a. DeBruijn a => Int -> a -> Substitution' a
singletonS Int
0 Term
t)
substContext Int
i Term
t (Dom' Term (Name, Type)
x:Context
xs) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"conv.forall" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [TCMT IO Doc
"substContext"
, String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Int -> String
forall a. Show a => a -> String
show (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
, Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t
, Context -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Context -> m Doc
prettyTCM Context
xs
]
(c,sigma) <- Int -> Term -> Context -> m (Context, Substitution)
forall (m :: * -> *).
MonadConversion m =>
Int -> Term -> Context -> m (Context, Substitution)
substContext (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Term
t Context
xs
let e = Substitution' (SubstArg (Dom' Term (Name, Type)))
-> Dom' Term (Name, Type) -> Dom' Term (Name, Type)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg (Dom' Term (Name, Type)))
sigma Dom' Term (Name, Type)
x
return (e:c, liftS 1 sigma)
substContext Int
i Term
t (Dom' Term (Name, Type)
x:Context
xs) = m (Context, Substitution)
forall a. HasCallStack => a
__IMPOSSIBLE__
compareInterval :: MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
compareInterval :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareInterval Comparison
cmp Type
i Term
t Term
u = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.interval" Int
15 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"{ compareInterval" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u ]
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare at interval type"
tb <- Term -> m (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
t
ub <- reduceB u
let t = Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
tb
u = Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
ub
it <- decomposeInterval' t
iu <- decomposeInterval' u
case () of
()
_ | Blocked Term -> Bool
forall {t} {a}. Blocked' t a -> Bool
isBlocked Blocked Term
tb Bool -> Bool -> Bool
|| Blocked Term -> Bool
forall {t} {a}. Blocked' t a -> Bool
isBlocked Blocked Term
ub -> do
interval <- m Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
compareAtom CmpEq (AsTermsOf interval) t u
()
_ | Bool
otherwise -> do
x <- [(IntMap BoolSet, [Term])] -> [(IntMap BoolSet, [Term])] -> m Bool
forall (m :: * -> *).
MonadConversion m =>
[(IntMap BoolSet, [Term])] -> [(IntMap BoolSet, [Term])] -> m Bool
leqInterval [(IntMap BoolSet, [Term])]
it [(IntMap BoolSet, [Term])]
iu
y <- leqInterval iu it
let final = [(IntMap BoolSet, [Term])] -> Bool
isCanonical [(IntMap BoolSet, [Term])]
it Bool -> Bool -> Bool
&& [(IntMap BoolSet, [Term])] -> Bool
isCanonical [(IntMap BoolSet, [Term])]
iu
if x && y then reportSDoc "tc.conv.interval" 15 $ "Ok! }" else
if final then typeError $ UnequalTerms cmp t u (AsTermsOf i)
else do
reportSDoc "tc.conv.interval" 15 $ "Giving up! }"
patternViolation (unblockOnAnyMetaIn (t, u))
where
isBlocked :: Blocked' t a -> Bool
isBlocked Blocked{} = Bool
True
isBlocked NotBlocked{} = Bool
False
type Conj = (IntMap BoolSet, [Term])
isCanonical :: [Conj] -> Bool
isCanonical :: [(IntMap BoolSet, [Term])] -> Bool
isCanonical = ((IntMap BoolSet, [Term]) -> Bool)
-> [(IntMap BoolSet, [Term])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Term] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Term] -> Bool)
-> ((IntMap BoolSet, [Term]) -> [Term])
-> (IntMap BoolSet, [Term])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IntMap BoolSet, [Term]) -> [Term]
forall a b. (a, b) -> b
snd)
leqInterval :: MonadConversion m => [Conj] -> [Conj] -> m Bool
leqInterval :: forall (m :: * -> *).
MonadConversion m =>
[(IntMap BoolSet, [Term])] -> [(IntMap BoolSet, [Term])] -> m Bool
leqInterval [(IntMap BoolSet, [Term])]
r [(IntMap BoolSet, [Term])]
q =
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(IntMap BoolSet, [Term])]
-> ((IntMap BoolSet, [Term]) -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(IntMap BoolSet, [Term])]
r (\ (IntMap BoolSet, [Term])
r_i ->
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(IntMap BoolSet, [Term])]
-> ((IntMap BoolSet, [Term]) -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(IntMap BoolSet, [Term])]
q (\ (IntMap BoolSet, [Term])
q_j -> (IntMap BoolSet, [Term]) -> (IntMap BoolSet, [Term]) -> m Bool
forall (m :: * -> *).
MonadConversion m =>
(IntMap BoolSet, [Term]) -> (IntMap BoolSet, [Term]) -> m Bool
leqConj (IntMap BoolSet, [Term])
r_i (IntMap BoolSet, [Term])
q_j))
leqConj :: MonadConversion m => Conj -> Conj -> m Bool
leqConj :: forall (m :: * -> *).
MonadConversion m =>
(IntMap BoolSet, [Term]) -> (IntMap BoolSet, [Term]) -> m Bool
leqConj (IntMap BoolSet
rs, [Term]
rst) (IntMap BoolSet
qs, [Term]
qst) = do
if (BoolSet -> BoolSet -> Bool)
-> IntMap BoolSet -> IntMap BoolSet -> Bool
forall a b. (a -> b -> Bool) -> IntMap a -> IntMap b -> Bool
IntMap.isSubmapOfBy BoolSet -> BoolSet -> Bool
BoolSet.isSubsetOf IntMap BoolSet
qs IntMap BoolSet
rs
then do
interval <-
Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
forall {t}. Sort' t
IntervalUniv (Term -> Type) -> (Maybe Term -> Term) -> Maybe Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Type) -> m (Maybe Term) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinInterval
let eqT Term
t Term
u = m () -> m Bool
forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion (Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom Comparison
CmpEq (Type -> CompareAs
AsTermsOf Type
interval) Term
t Term
u)
let listSubset [Term]
ts [Term]
us =
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term] -> (Term -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Term]
ts (\Term
t -> [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term] -> (Term -> m Bool) -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Term]
us (\Term
u -> Term -> Term -> m Bool
eqT Term
t Term
u))
listSubset qst rst
else
Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
equalTermOnFace :: MonadConversion m => Term -> Type -> Term -> Term -> m ()
equalTermOnFace :: forall (m :: * -> *).
MonadConversion m =>
Term -> Type -> Term -> Term -> m ()
equalTermOnFace = Comparison -> Term -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace Comparison
CmpEq
compareTermOnFace :: MonadConversion m => Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace = (Substitution -> Comparison -> Type -> Term -> Term -> m ())
-> Comparison -> Term -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
(Substitution -> Comparison -> Type -> Term -> Term -> m ())
-> Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace' ((Comparison -> Type -> Term -> Term -> m ())
-> Substitution -> Comparison -> Type -> Term -> Term -> m ()
forall a b. a -> b -> a
const Comparison -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
compareTerm)
compareTermOnFace'
:: MonadConversion m
=> (Substitution -> Comparison -> Type -> Term -> Term -> m ())
-> Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace' :: forall (m :: * -> *).
MonadConversion m =>
(Substitution -> Comparison -> Type -> Term -> Term -> m ())
-> Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace' Substitution -> Comparison -> Type -> Term -> Term -> m ()
k Comparison
cmp Term
phi Type
ty Term
u Term
v = do
String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.face" Int
40 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"compareTermOnFace:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
phi TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"|-" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
u TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"==" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
ty
ProfileOption -> m () -> m ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadStatistics m => String -> m ()
tick String
"compare at face type"
phi <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
phi
_ <- forallFaceMaps phi postponed $ \ IntMap Bool
faces Substitution
alpha ->
Substitution -> Comparison -> Type -> Term -> Term -> m ()
k Substitution
alpha Comparison
cmp (Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
alpha Type
ty) (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
alpha Term
u) (Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
alpha Term
v)
return ()
where
postponed :: IntMap Bool -> Blocker -> Term -> m ()
postponed IntMap Bool
ms Blocker
blocker Term
psi = do
phi <- Names -> NamesT m Term -> m Term
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT m Term -> m Term) -> NamesT m Term -> m Term
forall a b. (a -> b) -> a -> b
$ do
imin <- m Term -> NamesT m Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl (m Term -> NamesT m Term) -> m Term -> NamesT m Term
forall a b. (a -> b) -> a -> b
$ PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
PrimIMin
ineg <- cl $ getPrimitiveTerm PrimINeg
psi <- open psi
let phi = ((Int, Bool) -> NamesT m Term -> NamesT m Term)
-> NamesT m Term -> [(Int, Bool)] -> NamesT m Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (Int
i,Bool
b) NamesT m Term
r -> do i <- Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (Int -> Term
var Int
i); pure imin <@> (if b then i else pure ineg <@> i) <@> r)
NamesT m Term
psi (IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Bool
ms)
phi
addConstraint blocker (ValueCmpOnFace cmp phi ty u v)
bothAbsurd :: MonadConversion m => QName -> QName -> m Bool
bothAbsurd :: forall (m :: * -> *). MonadConversion m => QName -> QName -> m Bool
bothAbsurd QName
f QName
f'
| QName -> Bool
isAbsurdLambdaName QName
f, QName -> Bool
isAbsurdLambdaName QName
f' = do
def <- QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
f
def' <- getConstInfo f'
case (theDef def, theDef def') of
(Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause{ clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
Nothing }] },
Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause{ clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
Nothing }] }) -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
(Defn, Defn)
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
| Bool
otherwise = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False