{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Conversion where
import Control.Arrow (first, second)
import Control.Monad
import Control.Monad.Fail (MonadFail)
import Data.Function
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.IntSet as IntSet
import Agda.Syntax.Abstract.Views (isSet)
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.Monad.Builtin
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)
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (infer)
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.Warnings (MonadWarning)
import Agda.Interaction.Options
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Functor
import Agda.Utils.Monad
import Agda.Utils.Maybe
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.WithDefault
import Agda.Utils.Impossible
type MonadConversion m =
( MonadReduce m
, MonadAddContext m
, MonadConstraint m
, MonadMetaSolver m
, MonadError TCErr m
, MonadWarning m
, MonadDebug m
, MonadStatistics m
, MonadFresh ProblemId m
, MonadFresh Int m
, HasBuiltins m
, HasConstInfo m
, HasOptions m
, MonadFail m
)
tryConversion
:: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
=> m () -> m Bool
tryConversion = isJust <.> tryConversion'
tryConversion'
:: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m)
=> m a -> m (Maybe a)
tryConversion' m = tryMaybe $ noConstraints m
sameVars :: Elims -> Elims -> Bool
sameVars xs ys = and $ zipWith same xs ys
where
same (Apply (Arg _ (Var n []))) (Apply (Arg _ (Var m []))) = n == m
same _ _ = False
intersectVars :: Elims -> Elims -> Maybe [Bool]
intersectVars = zipWithM areVars where
areVars (Apply u) v | isIrrelevant u = Just False
areVars (Apply (Arg _ (Var n []))) (Apply (Arg _ (Var m []))) = Just $ n /= m
areVars _ _ = Nothing
equalTerm :: MonadConversion m => Type -> Term -> Term -> m ()
equalTerm = compareTerm CmpEq
equalAtom :: MonadConversion m => CompareAs -> Term -> Term -> m ()
equalAtom = compareAtom CmpEq
equalType :: MonadConversion m => Type -> Type -> m ()
equalType = compareType CmpEq
convError :: TypeError -> TCM ()
convError err = ifM ((==) Irrelevant <$> asksTC getRelevance) (return ()) $ typeError err
compareTerm :: forall m. MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
compareTerm cmp a u v = compareAs cmp (AsTermsOf a) u v
compareAs :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m ()
compareAs cmp a u v = do
reportSDoc "tc.conv.term" 10 $ sep $
[ "compareTerm"
, nest 2 $ prettyTCM u <+> prettyTCM cmp <+> prettyTCM v
, nest 2 $ prettyTCM a
]
((u, v), equal) <- SynEq.checkSyntacticEquality u v
if equal then verboseS "profile.sharing" 20 $ tick "equal terms" else do
verboseS "profile.sharing" 20 $ tick "unequal terms"
reportSDoc "tc.conv.term" 15 $ sep $
[ "compareTerm (not syntactically equal)"
, nest 2 $ prettyTCM u <+> prettyTCM cmp <+> prettyTCM v
, nest 2 $ prettyTCM a
]
let fallback = compareAs' cmp a u v
unlessSubtyping :: m () -> m ()
unlessSubtyping cont =
if cmp == CmpEq then cont else do
ifBlocked a (\ _ _ -> fallback) $ \ _ a -> do
caseMaybeM (isSizeType a) cont (\ _ -> fallback)
dir = fromCmp cmp
rid = flipCmp dir
case (u, v) of
(MetaV x us, MetaV y vs)
| x /= y -> unlessSubtyping $ solve1 `orelse` solve2 `orelse` fallback
| otherwise -> fallback
where
(solve1, solve2) | x > y = (assign dir x us v, assign rid y vs u)
| otherwise = (assign rid y vs u, assign dir x us v)
(MetaV x us, _) -> unlessSubtyping $ assign dir x us v `orelse` fallback
(_, MetaV y vs) -> unlessSubtyping $ assign rid y vs u `orelse` fallback
_ -> fallback
where
assign :: CompareDirection -> MetaId -> Elims -> Term -> m ()
assign dir x es v = do
reportSDoc "tc.conv.term.shortcut" 20 $ sep
[ "attempting shortcut"
, nest 2 $ prettyTCM (MetaV x es) <+> ":=" <+> prettyTCM v
]
whenM (isInstantiatedMeta x) patternViolation
assignE dir x es v a $ compareAsDir dir a
reportSDoc "tc.conv.term.shortcut" 50 $
"shortcut successful" $$ nest 2 ("result:" <+> (pretty =<< instantiate (MetaV x es)))
orelse :: m () -> m () -> m ()
orelse m h = catchError m (\_ -> h)
assignE :: (MonadConversion m)
=> CompareDirection -> MetaId -> Elims -> Term -> CompareAs -> (Term -> Term -> m ()) -> m ()
assignE dir x es v a comp = assignWrapper dir x es v $ do
case allApplyElims es of
Just vs -> assignV dir x vs v a
Nothing -> do
reportSDoc "tc.conv.assign" 30 $ sep
[ "assigning to projected meta "
, prettyTCM x <+> sep (map prettyTCM es) <+> text (":" ++ show dir) <+> prettyTCM v
]
etaExpandMeta [Records] x
res <- isInstantiatedMeta' x
case res of
Just u -> do
reportSDoc "tc.conv.assign" 30 $ sep
[ "seems like eta expansion instantiated meta "
, prettyTCM x <+> text (":" ++ show dir) <+> prettyTCM u
]
let w = u `applyE` es
comp w v
Nothing -> do
reportSLn "tc.conv.assign" 30 "eta expansion did not instantiate meta"
patternViolation
compareAsDir :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m ()
compareAsDir dir a = dirToCmp (`compareAs'` a) dir
compareAs' :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m ()
compareAs' cmp tt m n = case tt of
AsTermsOf a -> compareTerm' cmp a m n
AsSizes -> compareSizes cmp m n
AsTypes -> compareAtom cmp AsTypes m n
compareTerm' :: forall m. MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
compareTerm' cmp a m n =
verboseBracket "tc.conv.term" 20 "compareTerm" $ do
a' <- reduce a
(catchConstraint (ValueCmp cmp (AsTermsOf a') m n) :: m () -> m ()) $ do
reportSDoc "tc.conv.term" 30 $ fsep
[ "compareTerm", prettyTCM m, prettyTCM cmp, prettyTCM n, ":", prettyTCM a' ]
propIrr <- isPropEnabled
isSize <- isJust <$> isSizeType a'
s <- reduce $ getSort a'
mlvl <- getBuiltin' builtinLevel
reportSDoc "tc.conv.level" 60 $ nest 2 $ sep
[ "a' =" <+> pretty a'
, "mlvl =" <+> pretty mlvl
, text $ "(Just (unEl a') == mlvl) = " ++ show (Just (unEl a') == mlvl)
]
case s of
Prop{} | propIrr -> compareIrrelevant a' m n
_ | isSize -> compareSizes cmp m n
_ -> case unEl a' of
a | Just a == mlvl -> do
a <- levelView m
b <- levelView n
equalLevel a b
a@Pi{} -> equalFun s a m n
Lam _ _ -> __IMPOSSIBLE__
Def r es -> do
isrec <- isEtaRecord r
if isrec
then do
sig <- getSignature
let ps = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
isNeutral (NotBlocked _ Con{}) = return False
isNeutral (NotBlocked r (Def q _)) = do
not <$> usesCopatterns q
isNeutral _ = return True
isMeta (NotBlocked _ MetaV{}) = True
isMeta _ = False
reportSDoc "tc.conv.term" 30 $ prettyTCM a <+> "is eta record type"
m <- reduceB m
mNeutral <- isNeutral m
n <- reduceB n
nNeutral <- isNeutral n
case (m, n) of
_ | isMeta m || isMeta n ->
compareAtom cmp (AsTermsOf a') (ignoreBlocking m) (ignoreBlocking n)
_ | mNeutral && nNeutral -> do
isSing <- isSingletonRecordModuloRelevance r ps
case isSing of
Right True -> return ()
_ -> compareAtom cmp (AsTermsOf a') (ignoreBlocking m) (ignoreBlocking n)
_ -> do
(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)
_ -> compareAtom cmp (AsTermsOf a') m n
where
equalFun :: (MonadConversion m) => Sort -> Term -> Term -> Term -> m ()
equalFun s a@(Pi dom b) m n | domFinite dom = do
mp <- fmap getPrimName <$> getBuiltin' builtinIsOne
case unEl $ unDom dom of
Def q [Apply phi]
| Just q == mp -> compareTermOnFace cmp (unArg phi) (El s (Pi (dom {domFinite = False}) b)) m n
_ -> equalFun s (Pi (dom{domFinite = False}) b) m n
equalFun _ (Pi dom@Dom{domInfo = info} b) m n | not $ domFinite dom = do
let name = suggests [ Suggestion b , Suggestion m , Suggestion n ]
addContext (name, dom) $ compareTerm cmp (absBody b) m' n'
where
(m',n') = raise 1 (m,n) `apply` [Arg info $ var 0]
equalFun _ _ _ _ = __IMPOSSIBLE__
equalPath :: (MonadConversion m) => PathView -> Type -> Term -> Term -> m ()
equalPath (PathType s _ l a x y) _ m n = do
let name = "i" :: String
interval <- el 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{} a' m n = cmpDef a' m n
cmpDef a'@(El s ty) m n = do
mI <- getBuiltinName' builtinInterval
mIsOne <- getBuiltinName' builtinIsOne
mGlue <- getPrimitiveName' builtinGlue
mHComp <- getPrimitiveName' builtinHComp
mSub <- getBuiltinName' builtinSub
case ty of
Def q es | Just q == mIsOne -> return ()
Def q es | Just q == mGlue, Just args@(l:_:a:phi:_) <- allApplyElims es -> do
ty <- el' (pure $ unArg l) (pure $ unArg a)
unglue <- prim_unglue
let mkUnglue m = apply unglue $ map (setHiding Hidden) args ++ [argN m]
reportSDoc "conv.glue" 20 $ prettyTCM (ty,mkUnglue m,mkUnglue n)
compareTermOnFace cmp (unArg phi) ty m n
compareTerm cmp ty (mkUnglue m) (mkUnglue n)
Def q es | Just q == mHComp, Just (sl:s:args@[phi,u,u0]) <- allApplyElims es
, Sort (Type lvl) <- unArg s -> do
let l = Level lvl
ty <- el' (pure $ l) (pure $ unArg u0)
unglueU <- prim_unglueU
subIn <- primSubIn
let bA = subIn `apply` [sl,s,phi,u0]
let mkUnglue m = apply unglueU $ [argH l] ++ map (setHiding Hidden) [phi,u] ++ [argH bA,argN m]
reportSDoc "conv.hcompU" 20 $ prettyTCM (ty,mkUnglue m,mkUnglue n)
compareTermOnFace cmp (unArg phi) ty m n
compareTerm cmp ty (mkUnglue m) (mkUnglue n)
Def q es | Just q == mSub, Just args@(l:a:_) <- allApplyElims es -> do
ty <- el' (pure $ unArg l) (pure $ unArg a)
out <- primSubOut
let mkOut m = apply out $ map (setHiding Hidden) args ++ [argN m]
compareTerm cmp ty (mkOut m) (mkOut n)
Def q [] | Just q == mI -> compareInterval cmp a' m n
_ -> compareAtom cmp (AsTermsOf a') m n
compareTel :: MonadConversion m => Type -> Type ->
Comparison -> Telescope -> Telescope -> m ()
compareTel t1 t2 cmp tel1 tel2 =
verboseBracket "tc.conv.tel" 20 "compareTel" $
catchConstraint (TelCmp t1 t2 cmp tel1 tel2) $ case (tel1, tel2) of
(EmptyTel, EmptyTel) -> return ()
(EmptyTel, _) -> bad
(_, EmptyTel) -> bad
(ExtendTel dom1 tel1, ExtendTel dom2 tel2) -> do
compareDom cmp dom1 dom2 tel1 tel2 bad bad bad bad $
compareTel t1 t2 cmp (absBody tel1) (absBody tel2)
where
bad = typeError $ UnequalTypes cmp t2 t1
compareAtomDir :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m ()
compareAtomDir dir a = dirToCmp (`compareAtom` a) dir
computeElimHeadType :: MonadConversion m => QName -> Elims -> Elims -> m Type
computeElimHeadType f es es' = do
def <- getConstInfo f
if projectionArgs (theDef def) <= 0 then return $ defType def else do
let arg = case (es, es') of
(Apply arg : _, _) -> arg
(_, Apply arg : _) -> arg
_ -> __IMPOSSIBLE__
reportSDoc "tc.conv.infer" 30 $
"inferring type of internal arg: " <+> prettyTCM arg
targ <- infer $ unArg arg
reportSDoc "tc.conv.infer" 30 $
"inferred type: " <+> prettyTCM targ
fromMaybeM patternViolation $ getDefType f =<< reduce targ
compareAtom :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom cmp t m n =
verboseBracket "tc.conv.atom" 20 "compareAtom" $
(catchConstraint (ValueCmp cmp t m n) :: m () -> m ()) $ do
reportSDoc "tc.conv.atom" 50 $
"compareAtom" <+> fsep [ prettyTCM m <+> prettyTCM cmp
, prettyTCM n
, prettyTCM t
]
(mb',nb') <- ifM (asksTC envCompareBlocked) ((notBlocked -*- notBlocked) <$> reduce (m,n)) $ do
mb' <- etaExpandBlocked =<< reduceB m
nb' <- etaExpandBlocked =<< reduceB n
return (mb', nb')
(mb'', nb'') <- case (ignoreBlocking mb', ignoreBlocking nb') of
(Lit _, Lit _) -> return (mb', nb')
_ -> (,) <$> traverse constructorForm mb'
<*> traverse constructorForm nb'
mb <- traverse unLevel mb''
nb <- traverse unLevel nb''
cmpBlocked <- viewTC eCompareBlocked
let m = ignoreBlocking mb
n = ignoreBlocking nb
postpone = addConstraint $ ValueCmp cmp t m n
postponeIfBlockedAs :: CompareAs -> (Blocked CompareAs -> m ()) -> m ()
postponeIfBlockedAs AsTypes f = f $ NotBlocked ReallyNotBlocked AsTypes
postponeIfBlockedAs AsSizes f = f $ NotBlocked ReallyNotBlocked AsSizes
postponeIfBlockedAs (AsTermsOf t) f = ifBlocked t
(\m t -> (f $ Blocked m $ AsTermsOf t) `catchError` \case
TypeError{} -> postpone
err -> throwError err)
(\nb t -> f $ NotBlocked nb $ AsTermsOf t)
checkDefinitionalEquality = unlessM (pureCompareAs CmpEq t m n) postpone
dir = fromCmp cmp
rid = flipCmp dir
assign dir x es v = assignE dir x es v t $ compareAtomDir dir t
reportSDoc "tc.conv.atom" 30 $
"compareAtom" <+> fsep [ prettyTCM mb <+> prettyTCM cmp
, prettyTCM nb
, prettyTCM t
]
reportSDoc "tc.conv.atom" 80 $
"compareAtom" <+> fsep [ (text . show) mb <+> prettyTCM cmp
, (text . show) nb
, ":" <+> (text . show) t ]
case (mb, nb) of
(NotBlocked _ (MetaV x xArgs), NotBlocked _ (MetaV y yArgs))
| x == y , cmpBlocked -> do
a <- metaType x
compareElims [] [] a (MetaV x []) xArgs yArgs
| x == y ->
case intersectVars xArgs yArgs of
Just kills -> do
killResult <- killArgs kills x
case killResult of
NothingToPrune -> return ()
PrunedEverything -> return ()
PrunedNothing -> postpone
PrunedSomething -> postpone
Nothing -> checkDefinitionalEquality
| otherwise -> do
[p1, p2] <- mapM getMetaPriority [x,y]
let (solve1, solve2)
| (p1, x) > (p2, y) = (l1, r2)
| otherwise = (r1, l2)
where l1 = assign dir x xArgs n
r1 = assign rid y yArgs m
l2 = ifM (isInstantiatedMeta x) (compareAsDir dir t m n) l1
r2 = ifM (isInstantiatedMeta y) (compareAsDir rid t n m) r1
catchPatternErr solve2 solve1
(NotBlocked _ (MetaV x es), _) -> assign dir x es n
(_, NotBlocked _ (MetaV x es)) -> assign rid x es m
(Blocked{}, Blocked{}) -> checkDefinitionalEquality
(Blocked{}, _) -> useInjectivity (fromCmp cmp) t m n
(_, Blocked{}) -> useInjectivity (flipCmp $ fromCmp cmp) t n m
_ -> postponeIfBlockedAs t $ \bt -> do
case (m, n) of
(Pi{}, Pi{}) -> equalFun m n
(Sort s1, Sort s2) ->
ifM (optCumulativity <$> pragmaOptions)
(compareSort cmp s1 s2)
(equalSort s1 s2)
(Lit l1, Lit l2) | l1 == l2 -> return ()
(Var i es, Var i' es') | i == i' -> do
a <- typeOfBV i
compareElims [] [] a (var i) es es'
(Def f es, Def f' es') -> do
unlessM (bothAbsurd f f') $ do
if f /= f' then trySizeUniv cmp t m n f es f' es' else do
unless (null es && null es') $ do
unlessM (compareEtaPrims f es es') $ do
a <- computeElimHeadType f es es'
pol <- getPolarity' cmp f
compareElims pol [] a (Def f []) es es'
(Con x ci xArgs, Con y _ yArgs)
| x == y -> do
a' <- case t of
AsTermsOf a -> conType x a
AsSizes -> __IMPOSSIBLE__
AsTypes -> __IMPOSSIBLE__
forcedArgs <- getForcedArgs $ conName x
compareElims (repeat $ polFromCmp cmp) forcedArgs a' (Con x ci []) xArgs yArgs
_ -> typeError $ UnequalTerms cmp m n $ ignoreBlocking bt
where
compareEtaPrims :: MonadConversion m => QName -> Elims -> Elims -> m Bool
compareEtaPrims q es es' = do
munglue <- getPrimitiveName' builtin_unglue
munglueU <- getPrimitiveName' builtin_unglueU
msubout <- getPrimitiveName' builtinSubOut
case () of
_ | Just q == munglue -> compareUnglueApp q es es'
_ | Just q == munglueU -> compareUnglueUApp q es es'
_ | Just q == msubout -> compareSubApp q es es'
_ -> return False
compareSubApp q es es' = do
let (as,bs) = splitAt 5 es; (as',bs') = splitAt 5 es'
case (allApplyElims as, allApplyElims as') of
(Just [a,bA,phi,u,x], Just [a',bA',phi',u',x']) -> do
tSub <- primSub
equalType (El Inf $ apply tSub $ [a] ++ map (setHiding NotHidden) [bA,phi,u])
(El Inf $ apply tSub $ [a] ++ map (setHiding NotHidden) [bA',phi',u'])
compareAtom cmp (AsTermsOf $ El Inf $ 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
_ -> return False
compareUnglueApp q es es' = do
let (as,bs) = splitAt 7 es; (as',bs') = splitAt 7 es'
case (allApplyElims as, allApplyElims as') of
(Just [la,lb,bA,phi,bT,e,b], Just [la',lb',bA',phi',bT',e',b']) -> do
tGlue <- getPrimitiveTerm 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
_ -> return False
compareUnglueUApp :: MonadConversion m => QName -> Elims -> Elims -> m Bool
compareUnglueUApp q es es' = do
let (as,bs) = splitAt 5 es; (as',bs') = splitAt 5 es'
case (allApplyElims as, allApplyElims as') of
(Just [la,phi,bT,bAS,b], Just [la',phi',bT',bA',b']) -> do
tHComp <- primHComp
tLSuc <- primLevelSuc
tSubOut <- primSubOut
iz <- primIZero
let lsuc t = tLSuc `apply` [argN t]
s = tmSort $ unArg la
sucla = lsuc <$> 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
_ -> return False
conType c t = ifBlocked t (\ _ _ -> patternViolation) $ \ _ t -> do
let impossible = do
reportSDoc "impossible" 10 $
"expected data/record type, found " <+> prettyTCM t
reportSDoc "impossible" 70 $ nest 2 $ "raw =" <+> pretty t
patternViolation
maybe impossible (return . snd) =<< getFullyAppliedConType c t
equalFun t1 t2 = case (t1, t2) of
(Pi dom1 b1, Pi dom2 b2) -> do
verboseBracket "tc.conv.fun" 15 "compare function types" $ do
reportSDoc "tc.conv.fun" 20 $ nest 2 $ vcat
[ "t1 =" <+> prettyTCM t1
, "t2 =" <+> prettyTCM t2
]
compareDom cmp dom2 dom1 b1 b2 errH errR errQ errC $
compareType cmp (absBody b1) (absBody b2)
where
errH = typeError $ UnequalHiding t1 t2
errR = typeError $ UnequalRelevance cmp t1 t2
errQ = typeError $ UnequalQuantity cmp t1 t2
errC = typeError $ UnequalCohesion cmp t1 t2
_ -> __IMPOSSIBLE__
compareDom :: (MonadConversion m , Free c)
=> Comparison
-> Dom Type
-> Dom Type
-> Abs b
-> Abs c
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
-> m ()
compareDom cmp0
dom1@(Dom{domInfo = i1, unDom = a1})
dom2@(Dom{domInfo = i2, unDom = a2})
b1 b2 errH errR errQ errC cont = do
hasSubtyping <- collapseDefault . optSubtyping <$> pragmaOptions
let cmp = if hasSubtyping then cmp0 else CmpEq
if | not $ sameHiding dom1 dom2 -> errH
| not $ compareRelevance cmp (getRelevance dom1) (getRelevance dom2) -> errR
| not $ compareQuantity cmp (getQuantity dom1) (getQuantity dom2) -> errQ
| not $ compareCohesion cmp (getCohesion dom1) (getCohesion dom2) -> errC
| otherwise -> do
let r = max (getRelevance dom1) (getRelevance dom2)
dependent = (r /= Irrelevant) && isBinderUsed b2
pid <- newProblem_ $ compareType cmp0 a1 a2
dom <- if dependent
then (\ a -> dom1 {unDom = a}) <$> blockTypeOnProblem a1 pid
else return dom1
let name = suggests [ Suggestion b1 , Suggestion b2 ]
addContext (name, dom) $ cont
stealConstraints pid
compareRelevance :: Comparison -> Relevance -> Relevance -> Bool
compareRelevance CmpEq = (==)
compareRelevance CmpLeq = (<=)
compareQuantity :: Comparison -> Quantity -> Quantity -> Bool
compareQuantity CmpEq = sameQuantity
compareQuantity CmpLeq = moreQuantity
compareCohesion :: Comparison -> Cohesion -> Cohesion -> Bool
compareCohesion CmpEq = sameCohesion
compareCohesion CmpLeq = moreCohesion
antiUnify :: MonadConversion m => ProblemId -> Type -> Term -> Term -> m Term
antiUnify pid a u v = do
((u, v), eq) <- SynEq.checkSyntacticEquality u v
if eq then return u else do
(u, v) <- reduce (u, v)
reportSDoc "tc.conv.antiUnify" 30 $ vcat
[ "antiUnify"
, "a =" <+> prettyTCM a
, "u =" <+> prettyTCM u
, "v =" <+> prettyTCM v
]
case (u, v) of
(Pi ua ub, Pi va vb) -> do
wa0 <- antiUnifyType pid (unDom ua) (unDom va)
let wa = wa0 <$ ua
wb <- addContext wa $ antiUnifyType pid (absBody ub) (absBody vb)
return $ Pi wa (mkAbs (absName ub) wb)
(Lam i u, Lam _ v) ->
reduce (unEl a) >>= \case
Pi a b -> Lam i . (mkAbs (absName u)) <$> addContext a (antiUnify pid (absBody b) (absBody u) (absBody v))
_ -> fallback
(Var i us, Var j vs) | i == j -> maybeGiveUp $ do
a <- typeOfBV i
antiUnifyElims pid a (var i) us vs
(Con x ci us, Con y _ vs) | x == y -> maybeGiveUp $ do
a <- maybe patternViolation (return . snd) =<< getConType x a
antiUnifyElims pid a (Con x ci []) us vs
(Def f us, Def g vs) | f == g, length us == length vs -> maybeGiveUp $ do
a <- computeElimHeadType f us vs
antiUnifyElims pid a (Def f []) us vs
_ -> fallback
where
maybeGiveUp = catchPatternErr fallback
fallback = blockTermOnProblem a u pid
antiUnifyArgs :: MonadConversion m => ProblemId -> Dom Type -> Arg Term -> Arg Term -> m (Arg Term)
antiUnifyArgs pid dom u v
| getModality u /= getModality v = patternViolation
| otherwise = applyModalityToContext u $
ifM (isIrrelevantOrPropM dom)
(return u)
((<$ u) <$> antiUnify pid (unDom dom) (unArg u) (unArg v))
antiUnifyType :: MonadConversion m => ProblemId -> Type -> Type -> m Type
antiUnifyType pid (El s a) (El _ b) = workOnTypes $ El s <$> antiUnify pid (sort s) a b
antiUnifyElims :: MonadConversion m => ProblemId -> Type -> Term -> Elims -> Elims -> m Term
antiUnifyElims pid a self [] [] = return self
antiUnifyElims pid a self (Proj o f : es1) (Proj _ g : es2) | f == g = do
res <- projectTyped self a o f
case res of
Just (_, self, a) -> antiUnifyElims pid a self es1 es2
Nothing -> patternViolation
antiUnifyElims pid a self (Apply u : es1) (Apply v : es2) = do
reduce (unEl a) >>= \case
Pi a b -> do
w <- antiUnifyArgs pid a u v
antiUnifyElims pid (b `lazyAbsApp` unArg w) (apply self [w]) es1 es2
_ -> patternViolation
antiUnifyElims _ _ _ _ _ = patternViolation
compareElims :: forall m. MonadConversion m => [Polarity] -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> m ()
compareElims pols0 fors0 a v els01 els02 = (catchConstraint (ElimCmp pols0 fors0 a v els01 els02) :: m () -> m ()) $ do
let v1 = applyE v els01
v2 = applyE v els02
failure = typeError $ UnequalTerms CmpEq v1 v2 (AsTermsOf a)
unless (null els01) $ do
reportSDoc "tc.conv.elim" 25 $ "compareElims" $$ do
nest 2 $ vcat
[ "a =" <+> prettyTCM a
, "pols0 (truncated to 10) =" <+> hsep (map prettyTCM $ take 10 pols0)
, "fors0 (truncated to 10) =" <+> hsep (map prettyTCM $ take 10 fors0)
, "v =" <+> prettyTCM v
, "els01 =" <+> prettyTCM els01
, "els02 =" <+> prettyTCM els02
]
case (els01, els02) of
([] , [] ) -> return ()
([] , Proj{}:_ ) -> failure
(Proj{} : _, [] ) -> failure
([] , Apply{} : _) -> failure
(Apply{} : _, [] ) -> failure
([] , IApply{} : _) -> failure
(IApply{} : _, [] ) -> failure
(Apply{} : _, Proj{} : _) -> __IMPOSSIBLE__ <$ solveAwakeConstraints' True
(Proj{} : _, Apply{} : _) -> __IMPOSSIBLE__ <$ solveAwakeConstraints' True
(IApply{} : _, Proj{} : _) -> __IMPOSSIBLE__ <$ solveAwakeConstraints' True
(Proj{} : _, IApply{} : _) -> __IMPOSSIBLE__ <$ solveAwakeConstraints' True
(IApply{} : _, Apply{} : _) -> __IMPOSSIBLE__ <$ solveAwakeConstraints' True
(Apply{} : _, IApply{} : _) -> __IMPOSSIBLE__ <$ solveAwakeConstraints' True
(e@(IApply x1 y1 r1) : els1, IApply x2 y2 r2 : els2) -> do
reportSDoc "tc.conv.elim" 25 $ "compareElims IApply"
let (pol, pols) = nextPolarity pols0
ifBlocked a (\ m t -> patternViolation) $ \ _ a -> do
va <- pathView a
reportSDoc "tc.conv.elim.iapply" 60 $ "compareElims IApply" $$ do
nest 2 $ "va =" <+> text (show (isPathType va))
case va of
PathType s path l bA x y -> do
b <- elInf primInterval
compareWithPol pol (flip compareTerm b)
r1 r2
let r = r1
codom <- el' (pure . unArg $ l) ((pure . unArg $ bA) <@> pure r)
compareElims pols [] codom
(applyE v [e]) els1 els2
OType t@(El _ Pi{}) -> compareElims pols0 fors0 t v (Apply (defaultArg r1) : els1) (Apply (defaultArg r2) : els2)
OType{} -> patternViolation
(Apply arg1 : els1, Apply arg2 : els2) ->
(verboseBracket "tc.conv.elim" 20 "compare Apply" :: m () -> m ()) $ do
reportSDoc "tc.conv.elim" 10 $ nest 2 $ vcat
[ "a =" <+> prettyTCM a
, "v =" <+> prettyTCM v
, "arg1 =" <+> prettyTCM arg1
, "arg2 =" <+> prettyTCM arg2
]
reportSDoc "tc.conv.elim" 50 $ nest 2 $ vcat
[ "raw:"
, "a =" <+> pretty a
, "v =" <+> pretty v
, "arg1 =" <+> pretty arg1
, "arg2 =" <+> pretty arg2
]
let (pol, pols) = nextPolarity pols0
(for, fors) = nextIsForced fors0
ifBlocked a (\ m t -> patternViolation) $ \ _ a -> do
reportSLn "tc.conv.elim" 90 $ "type is not blocked"
case unEl a of
(Pi (Dom{domInfo = info, unDom = b}) codom) -> do
reportSLn "tc.conv.elim" 90 $ "type is a function type"
mlvl <- tryMaybe primLevel
let freeInCoDom (Abs _ c) = 0 `freeInIgnoringSorts` c
freeInCoDom _ = False
dependent = (Just (unEl b) /= mlvl) && freeInCoDom codom
pid <- newProblem_ $ applyModalityToContext info $
if isForced for then
reportSLn "tc.conv.elim" 90 $ "argument is forced"
else if isIrrelevant info then do
reportSLn "tc.conv.elim" 90 $ "argument is irrelevant"
compareIrrelevant b (unArg arg1) (unArg arg2)
else do
reportSLn "tc.conv.elim" 90 $ "argument has polarity " ++ show pol
compareWithPol pol (flip compareTerm b)
(unArg arg1) (unArg arg2)
solved <- isProblemSolved pid
reportSLn "tc.conv.elim" 90 $ "solved = " ++ show solved
arg <- if dependent && not solved
then applyModalityToContext info $ do
reportSDoc "tc.conv.elims" 30 $ 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" 30 $ 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" 90 $ "stealing constraints from problem " ++ show pid
stealConstraints pid
a -> do
reportSDoc "impossible" 10 $
"unexpected type when comparing apply eliminations " <+> prettyTCM a
reportSDoc "impossible" 50 $ "raw type:" <+> pretty a
patternViolation
(Proj o f : els1, Proj _ f' : els2)
| f /= f' -> typeError . GenericError . show =<< prettyTCM f <+> "/=" <+> prettyTCM f'
| otherwise -> ifBlocked a (\ m t -> patternViolation) $ \ _ a -> do
res <- projectTyped v a o f
case res of
Just (_, u, t) -> do
compareElims [] [] t u els1 els2
Nothing -> do
reportSDoc "tc.conv.elims" 30 $ sep
[ text $ "projection " ++ show f
, text "applied to value " <+> prettyTCM v
, text "of unexpected type " <+> prettyTCM a
]
patternViolation
compareIrrelevant :: MonadConversion m => Type -> Term -> Term -> m ()
compareIrrelevant t v0 w0 = do
let v = stripDontCare v0
w = stripDontCare w0
reportSDoc "tc.conv.irr" 20 $ vcat
[ "compareIrrelevant"
, nest 2 $ "v =" <+> prettyTCM v
, nest 2 $ "w =" <+> prettyTCM w
]
reportSDoc "tc.conv.irr" 50 $ vcat
[ nest 2 $ "v =" <+> pretty v
, nest 2 $ "w =" <+> pretty w
]
try v w $ try w v $ return ()
where
try (MetaV x es) w fallback = do
mv <- lookupMeta x
let rel = getMetaRelevance mv
inst = case mvInstantiation mv of
InstV{} -> True
_ -> 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` \ _ -> fallback
try v w fallback = fallback
compareWithPol :: MonadConversion m => Polarity -> (Comparison -> a -> a -> m ()) -> a -> a -> m ()
compareWithPol Invariant cmp x y = cmp CmpEq x y
compareWithPol Covariant cmp x y = cmp CmpLeq x y
compareWithPol Contravariant cmp x y = cmp CmpLeq y x
compareWithPol Nonvariant cmp x y = return ()
polFromCmp :: Comparison -> Polarity
polFromCmp CmpLeq = Covariant
polFromCmp CmpEq = Invariant
compareArgs :: MonadConversion m => [Polarity] -> [IsForced] -> Type -> Term -> Args -> Args -> m ()
compareArgs pol for a v args1 args2 =
compareElims pol for a v (map Apply args1) (map Apply args2)
compareType :: MonadConversion m => Comparison -> Type -> Type -> m ()
compareType cmp ty1@(El s1 a1) ty2@(El s2 a2) =
workOnTypes $
verboseBracket "tc.conv.type" 20 "compareType" $ do
reportSDoc "tc.conv.type" 50 $ vcat
[ "compareType" <+> sep [ prettyTCM ty1 <+> prettyTCM cmp
, prettyTCM ty2 ]
, hsep [ " sorts:", prettyTCM s1, " and ", prettyTCM s2 ]
]
compareAs cmp AsTypes a1 a2
unlessM ((optCumulativity <$> pragmaOptions) `or2M`
(not . optCompareSorts <$> pragmaOptions)) $
compareSort CmpEq s1 s2
return ()
leqType :: MonadConversion m => Type -> Type -> m ()
leqType = compareType CmpLeq
coerce :: (MonadConversion m, MonadTCM m) => Comparison -> Term -> Type -> Type -> m Term
coerce cmp v t1 t2 = blockTerm t2 $ do
verboseS "tc.conv.coerce" 10 $ do
(a1,a2) <- reify (t1,t2)
let dbglvl = if isSet a1 && isSet a2 then 50 else 10
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 <- telViewUpTo' (-1) notVisible t1
TelV tel2 b2 <- telViewUpTo' (-1) notVisible t2
let n = size tel1 - size tel2
if n <= 0 then fallback else do
ifBlocked b2 (\ _ _ -> fallback) $ \ _ _ -> do
(args, t1') <- implicitArgs n notVisible t1
let v' = v `apply` args
v' <$ coerceSize (compareType cmp) v' t1' t2
where
fallback = v <$ coerceSize (compareType cmp) v t1 t2
coerceSize :: MonadConversion m => (Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
coerceSize leqType v t1 t2 = verboseBracket "tc.conv.size.coerce" 45 "coerceSize" $
workOnTypes $ do
reportSDoc "tc.conv.size.coerce" 70 $
"coerceSize" <+> vcat
[ "term v =" <+> pretty v
, "from type t1 =" <+> pretty t1
, "to type t2 =" <+> pretty t2
]
let fallback = leqType t1 t2
done = caseMaybeM (isSizeType =<< reduce t1) fallback $ \ _ -> return ()
caseMaybeM (isSizeType =<< reduce t2) fallback $ \ b2 -> do
mv <- sizeMaxView v
if any (\case{ DOtherSize{} -> True; _ -> 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
BoundedNo -> done
BoundedLt v2 -> do
sv2 <- sizeView v2
case sv2 of
SizeInf -> done
OtherSize{} -> do
vinc <- sizeSuc 1 v
compareSizes CmpLeq vinc v2
done
SizeSuc a2 -> do
compareSizes CmpLeq v a2
done
compareLevel :: MonadConversion m => Comparison -> Level -> Level -> m ()
compareLevel CmpLeq u v = leqLevel u v
compareLevel CmpEq u v = equalLevel u v
compareSort :: MonadConversion m => Comparison -> Sort -> Sort -> m ()
compareSort CmpEq = equalSort
compareSort CmpLeq = leqSort
leqSort :: forall m. MonadConversion m => Sort -> Sort -> m ()
leqSort s1 s2 = (catchConstraint (SortCmp CmpLeq s1 s2) :: m () -> m ()) $ do
(s1,s2) <- reduce (s1,s2)
let postpone = addConstraint (SortCmp CmpLeq s1 s2)
no = typeError $ NotLeqSort s1 s2
yes = return ()
synEq = ifNotM (optSyntacticEquality <$> pragmaOptions) postpone $ do
((s1,s2) , equal) <- SynEq.checkSyntacticEquality s1 s2
if | equal -> yes
| otherwise -> postpone
reportSDoc "tc.conv.sort" 30 $
sep [ "leqSort"
, nest 2 $ fsep [ prettyTCM s1 <+> "=<"
, prettyTCM s2 ]
]
propEnabled <- isPropEnabled
let fvsRHS = (`IntSet.member` allFreeVars s2)
badRigid <- s1 `rigidVarsNotContainedIn` fvsRHS
case (s1, s2) of
(DummyS s, _) -> impossibleSort s
(_, DummyS s) -> impossibleSort s
(Type a , Type b ) -> leqLevel a b
(Prop a , Prop b ) -> leqLevel a b
(Prop a , Type b ) -> leqLevel a b
(Type a , Prop b ) -> no
(_ , Inf ) -> yes
(Inf , _ ) -> equalSort s1 s2
(_ , SizeUniv) -> equalSort s1 s2
(_ , Prop (Max 0 [])) -> equalSort s1 s2
(_ , Type (Max 0 []))
| not propEnabled -> equalSort s1 s2
(SizeUniv, Type{} ) -> no
(SizeUniv, Prop{} ) -> no
(_ , _ ) | badRigid -> equalSort s2 Inf
(UnivSort Inf , UnivSort Inf) -> yes
(PiSort{}, _ ) -> synEq
(_ , PiSort{}) -> synEq
(FunSort{}, _ ) -> synEq
(_ , FunSort{}) -> synEq
(UnivSort{}, _ ) -> synEq
(_ , UnivSort{}) -> synEq
(MetaS{} , _ ) -> synEq
(_ , MetaS{} ) -> synEq
(DefS{} , _ ) -> synEq
(_ , DefS{}) -> synEq
where
impossibleSort s = do
reportS "impossible" 10
[ "leqSort: found dummy sort with description:"
, s
]
__IMPOSSIBLE__
leqLevel :: MonadConversion m => Level -> Level -> m ()
leqLevel a b = do
reportSDoc "tc.conv.nat" 30 $
"compareLevel" <+>
sep [ prettyTCM a <+> "=<"
, prettyTCM b ]
a <- normalise a
b <- normalise b
leqView a b
where
leqView :: MonadConversion m => Level -> Level -> m ()
leqView a b = catchConstraint (LevelCmp CmpLeq a b) $ do
reportSDoc "tc.conv.level" 30 $
"compareLevelView" <+>
sep [ pretty a <+> "=<"
, pretty b ]
cumulativity <- optCumulativity <$> pragmaOptions
reportSDoc "tc.conv.level" 40 $
"compareLevelView" <+>
sep [ prettyList_ (map (pretty . unSingleLevel) $ NonEmpty.toList $ levelMaxView a)
, "=<"
, prettyList_ (map (pretty . unSingleLevel) $ NonEmpty.toList $ levelMaxView b)
]
wrap $ case (levelMaxView a, levelMaxView b) of
_ | a == b -> ok
(SingleClosed 0 :| [] , _) -> ok
(as , SingleClosed 0 :| []) ->
sequence_ [ equalLevel (unSingleLevel a') (ClosedLevel 0) | a' <- NonEmpty.toList as ]
(SingleClosed m :| [], SingleClosed n :| []) -> if m <= n then ok else notok
(SingleClosed m :| [] , _)
| m <= levelLowerBound b -> ok
(as, bs)
| all neutralOrClosed bs , levelLowerBound a > levelLowerBound b -> notok
(as@(_:|_:_), b :| []) ->
sequence_ [ leqView (unSingleLevel a') (unSingleLevel b) | a' <- NonEmpty.toList as ]
(as, bs)
| let minN = min (fst $ levelPlusView a) (fst $ levelPlusView b)
a' = fromMaybe __IMPOSSIBLE__ $ subLevel minN a
b' = fromMaybe __IMPOSSIBLE__ $ subLevel minN b
, minN > 0 -> leqView a' b'
(as, bs)
| (subsumed@(_:_) , as') <- List.partition isSubsumed (NonEmpty.toList as)
-> leqView (unSingleLevels as') b
where
isSubsumed a = any (`subsumes` a) (NonEmpty.toList bs)
subsumes :: SingleLevel -> SingleLevel -> Bool
subsumes (SingleClosed m) (SingleClosed n) = m >= n
subsumes (SinglePlus (Plus m _)) (SingleClosed n) = m >= n
subsumes (SinglePlus (Plus m a)) (SinglePlus (Plus n b)) = a == b && m >= n
subsumes _ _ = False
(as , bs)
| cumulativity
, Just (mb@(MetaLevel x es) , bs') <- singleMetaView (NonEmpty.toList bs)
, null bs' || noMetas (Level a , unSingleLevels bs') -> do
mv <- lookupMeta x
abort <- (isJust <$> isInteractionMeta x) `or2M`
((== YesGeneralize) <$> isGeneralizableMeta x)
if | abort -> postpone
| otherwise -> do
x' <- case mvJudgement mv of
IsSort{} -> __IMPOSSIBLE__
HasType _ cmp t -> do
TelV tel t' <- telView 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 $ MetaLevel x' es)
_ | noMetas (Level a , Level b) -> notok
| otherwise -> postpone
where
ok = return ()
notok = unlessM typeInType $ typeError $ NotLeqSort (Type a) (Type b)
postpone = patternViolation
wrap m = m `catchError` \case
TypeError{} -> notok
err -> throwError err
neutralOrClosed (SingleClosed _) = True
neutralOrClosed (SinglePlus (Plus _ NeutralLevel{})) = True
neutralOrClosed _ = False
singleMetaView :: [SingleLevel] -> Maybe (LevelAtom, [SingleLevel])
singleMetaView (SinglePlus (Plus 0 l@(MetaLevel m es)) : ls)
| all (not . isMetaLevel) ls = Just (l,ls)
singleMetaView (l : ls)
| not $ isMetaLevel l = second (l:) <$> singleMetaView ls
singleMetaView _ = Nothing
isMetaLevel :: SingleLevel -> Bool
isMetaLevel (SinglePlus (Plus _ MetaLevel{})) = True
isMetaLevel (SinglePlus (Plus _ UnreducedLevel{})) = __IMPOSSIBLE__
isMetaLevel _ = False
equalLevel :: MonadConversion m => Level -> Level -> m ()
equalLevel a b = do
(a, b) <- normalise (a, b)
equalLevel' a b
equalLevel' :: forall m. MonadConversion m => Level -> Level -> m ()
equalLevel' a b = do
reportSDoc "tc.conv.level" 50 $ sep [ "equalLevel", nest 2 $ parens $ pretty a, nest 2 $ parens $ pretty b ]
reportSDoc "tc.conv.level" 40 $
sep [ "equalLevel"
, vcat [ nest 2 $ sep [ prettyTCM a <+> "=="
, prettyTCM b
]
]
]
let (a',b') = removeSubsumed a b
reportSDoc "tc.conv.level" 50 $
sep [ "equalLevel (w/o subsumed)"
, vcat [ nest 2 $ sep [ prettyTCM a' <+> "=="
, prettyTCM b'
]
]
]
let as = levelMaxView a'
bs = levelMaxView b'
reportSDoc "tc.conv.level" 50 $
sep [ text "equalLevel"
, vcat [ nest 2 $ sep [ prettyList_ (map (pretty . unSingleLevel) $ NonEmpty.toList $ as)
, "=="
, prettyList_ (map (pretty . unSingleLevel) $ NonEmpty.toList $ bs)
]
]
]
reportSDoc "tc.conv.level" 80 $
sep [ text "equalLevel"
, vcat [ nest 2 $ sep [ prettyList_ (map (text . show . unSingleLevel) $ NonEmpty.toList $ as)
, "=="
, prettyList_ (map (text . show . unSingleLevel) $ NonEmpty.toList $ bs)
]
]
]
catchConstraint (LevelCmp CmpEq a b) $ case (as, bs) of
_ | a == b -> ok
(SingleClosed m :| [], SingleClosed n :| [])
| m == n -> ok
| otherwise -> notok
(SingleClosed m :| [] , bs) | any isNeutral bs -> notok
(as , SingleClosed n :| []) | any isNeutral as -> notok
(SingleClosed m :| [] , _) | m < levelLowerBound b -> notok
(_ , SingleClosed n :| []) | n < levelLowerBound a -> notok
(SingleClosed 0 :| [] , bs@(_:|_:_)) ->
sequence_ [ equalLevel' (ClosedLevel 0) (unSingleLevel b') | b' <- NonEmpty.toList bs ]
(as@(_:|_:_) , SingleClosed 0 :| []) ->
sequence_ [ equalLevel' (unSingleLevel a') (ClosedLevel 0) | a' <- NonEmpty.toList as ]
(SinglePlus (Plus k (MetaLevel x as)) :| [] , bs)
| any (isThisMeta x) bs -> postpone
(as , SinglePlus (Plus k (MetaLevel x bs)) :| [])
| any (isThisMeta x) as -> postpone
(SinglePlus (Plus k (MetaLevel x as')) :| [] , SinglePlus (Plus l (MetaLevel y bs')) :| [])
| k == l -> if
| y < x -> meta x as' $ atomicLevel $ MetaLevel y bs'
| otherwise -> meta y bs' $ atomicLevel $ MetaLevel x as'
(SinglePlus (Plus k (MetaLevel x as')) :| [] , _)
| Just b' <- subLevel k b -> meta x as' b'
(_ , SinglePlus (Plus l (MetaLevel y bs')) :| [])
| Just a' <- subLevel l a -> meta y bs' a'
_ | Just a' <- levelMaxDiff a b
, b /= ClosedLevel 0 -> leqLevel a' b
_ | Just b' <- levelMaxDiff b a
, a /= ClosedLevel 0 -> leqLevel b' a
(as , bs)
| all isNeutralOrClosed (NonEmpty.toList as ++ NonEmpty.toList bs)
, not (any hasMeta (NonEmpty.toList as ++ NonEmpty.toList bs))
, length as == length bs -> do
reportSLn "tc.conv.level" 60 $ "equalLevel: all are neutral or closed"
zipWithM_ ((===) `on` levelTm . unSingleLevel) (NonEmpty.toList as) (NonEmpty.toList bs)
_ | noMetas (Level a , Level b) -> notok
| otherwise -> postpone
where
a === b = unlessM typeInType $ do
lvl <- levelType
equalAtom (AsTermsOf lvl) a b
ok = return ()
notok = unlessM typeInType notOk
notOk = typeError $ UnequalLevel CmpEq a b
postpone = do
reportSDoc "tc.conv.level" 30 $ hang "postponing:" 2 $ hang (pretty a <+> "==") 0 (pretty b)
patternViolation
meta x as b = do
reportSLn "tc.meta.level" 30 $ "Assigning meta level"
reportSDoc "tc.meta.level" 50 $ "meta" <+> sep [prettyList $ map pretty as, pretty b]
lvl <- levelType
assignE DirEq x as (levelTm b) (AsTermsOf lvl) (===)
wrap m = m `catchError` \case
TypeError{} -> notok
err -> throwError err
isNeutral (SinglePlus (Plus _ NeutralLevel{})) = True
isNeutral _ = False
isNeutralOrClosed (SingleClosed _) = True
isNeutralOrClosed (SinglePlus (Plus _ NeutralLevel{})) = True
isNeutralOrClosed _ = False
hasMeta (SinglePlus a) = case a of
Plus _ MetaLevel{} -> True
Plus _ (BlockedLevel _ v) -> isJust $ firstMeta v
Plus _ (NeutralLevel _ v) -> isJust $ firstMeta v
Plus _ (UnreducedLevel v) -> isJust $ firstMeta v
hasMeta (SingleClosed _) = False
isThisMeta x (SinglePlus (Plus _ (MetaLevel y _))) = x == y
isThisMeta _ _ = False
removeSubsumed a b =
let as = NonEmpty.toList $ levelMaxView a
bs = NonEmpty.toList $ levelMaxView b
a' = unSingleLevels $ filter (not . (`isStrictlySubsumedBy` bs)) as
b' = unSingleLevels $ filter (not . (`isStrictlySubsumedBy` as)) bs
in (a',b')
x `isStrictlySubsumedBy` ys = any (`strictlySubsumes` x) ys
SingleClosed m `strictlySubsumes` SingleClosed n = m > n
SinglePlus (Plus m a) `strictlySubsumes` SingleClosed n = m > n
SinglePlus (Plus m a) `strictlySubsumes` SinglePlus (Plus n b) = a == b && m > n
_ `strictlySubsumes` _ = False
equalSort :: forall m. MonadConversion m => Sort -> Sort -> m ()
equalSort s1 s2 = do
catchConstraint (SortCmp CmpEq s1 s2) $ do
(s1,s2) <- reduce (s1,s2)
let yes = return ()
no = typeError $ UnequalSorts s1 s2
reportSDoc "tc.conv.sort" 30 $ sep
[ "equalSort"
, vcat [ nest 2 $ fsep [ prettyTCM s1 <+> "=="
, prettyTCM s2 ]
, nest 2 $ fsep [ pretty s1 <+> "=="
, pretty s2 ]
]
]
propEnabled <- isPropEnabled
typeInTypeEnabled <- typeInType
case (s1, s2) of
(DummyS s, _) -> impossibleSort s
(_, DummyS s) -> impossibleSort s
(MetaS x es , MetaS y es')
| x == y -> synEq s1 s2
| x < y -> meta y es' s1
| otherwise -> meta x es s2
(MetaS x es , _ ) -> meta x es s2
(_ , MetaS x es ) -> meta x es s1
(Type a , Type b ) -> equalLevel a b `catchInequalLevel` no
(SizeUniv , SizeUniv ) -> yes
(Prop a , Prop b ) -> equalLevel a b `catchInequalLevel` no
(Inf , Inf ) -> yes
(Type{} , Inf )
| typeInTypeEnabled -> yes
(Inf , Type{} )
| typeInTypeEnabled -> yes
(s1 , PiSort a b) -> piSortEquals s1 a b
(PiSort a b , s2) -> piSortEquals s2 a b
(s1 , FunSort a b) -> funSortEquals s1 a b
(FunSort a b , s2) -> funSortEquals s2 a b
(s1 , UnivSort s2) -> univSortEquals s1 s2
(UnivSort s1 , s2 ) -> univSortEquals s2 s1
(DefS d es , DefS d' es')
| d == d' -> synEq s1 s2
| otherwise -> no
(_ , _ ) -> no
where
meta :: MetaId -> [Elim' Term] -> Sort -> m ()
meta x es s = do
reportSLn "tc.meta.sort" 30 $ "Assigning meta sort"
reportSDoc "tc.meta.sort" 50 $ "meta" <+> sep [pretty x, prettyList $ map pretty es, pretty s]
assignE DirEq x es (Sort s) AsTypes __IMPOSSIBLE__
synEq :: Sort -> Sort -> m ()
synEq s1 s2 = do
let postpone = addConstraint $ SortCmp CmpEq s1 s2
doSynEq <- optSyntacticEquality <$> pragmaOptions
if | doSynEq -> do
((s1,s2) , equal) <- SynEq.checkSyntacticEquality s1 s2
if | equal -> return ()
| otherwise -> postpone
| otherwise -> postpone
set0 = mkType 0
prop0 = mkProp 0
univSortEquals :: Sort -> Sort -> m ()
univSortEquals s1 s2 = do
reportSDoc "tc.conv.sort" 35 $ vcat
[ "univSortEquals"
, " s1 =" <+> prettyTCM s1
, " s2 =" <+> prettyTCM s2
]
let no = typeError $ UnequalSorts s1 (UnivSort s2)
case s1 of
Type l1 -> do
propEnabled <- isPropEnabled
if | Inf <- s2 -> no
| SizeUniv <- s2 -> no
| not propEnabled -> do
l2 <- case subLevel 1 l1 of
Just l2 -> return l2
Nothing -> do
l2 <- newLevelMeta
equalLevel l1 (levelSuc l2)
return l2
equalSort (Type l2) s2
| otherwise -> synEq (Type l1) (UnivSort s2)
Inf -> do
infInInf <- (optOmegaInOmega <$> pragmaOptions) `or2M` typeInType
if | infInInf -> equalSort Inf s2
| otherwise -> no
Prop{} -> no
SizeUniv{} -> no
_ -> synEq s1 (UnivSort s2)
piSortEquals :: Sort -> Dom Type -> Abs Sort -> m ()
piSortEquals s a NoAbs{} = __IMPOSSIBLE__
piSortEquals s a bAbs@(Abs x b) = do
reportSDoc "tc.conv.sort" 35 $ vcat
[ "piSortEquals"
, " s =" <+> prettyTCM s
, " a =" <+> prettyTCM a
, " b =" <+> addContext (x,a) (prettyTCM b)
]
propEnabled <- isPropEnabled
if | definitelyNotInf s -> do
b' <- newSortMeta
addContext (x,a) $ equalSort b (raise 1 b')
funSortEquals s (getSort a) b'
| otherwise -> synEq (PiSort a bAbs) s
funSortEquals :: Sort -> Sort -> Sort -> m ()
funSortEquals s0 s1 s2 = do
reportSDoc "tc.conv.sort" 35 $ vcat
[ "funSortEquals"
, " s0 =" <+> prettyTCM s0
, " s1 =" <+> prettyTCM s1
, " s2 =" <+> prettyTCM s2
]
propEnabled <- isPropEnabled
sizedTypesEnabled <- sizedTypesOption
case s0 of
Inf | definitelyNotInf s1 && definitelyNotInf s2 -> do
typeError $ UnequalSorts s0 (FunSort s1 s2)
| definitelyNotInf s1 -> equalSort Inf s2
| definitelyNotInf s2 -> equalSort Inf s1
| otherwise -> synEq s0 (FunSort s1 s2)
Type l -> do
l2 <- forceType s2
leqLevel l2 l
if | propEnabled -> case funSort' s1 (Type l2) of
Just s -> equalSort (Type l) s
Nothing -> synEq (Type l) (FunSort s1 $ Type l2)
| otherwise -> do
l1 <- forceType s1
equalLevel l (levelLub l1 l2)
Prop l -> do
l2 <- forceProp s2
leqLevel l2 l
case funSort' s1 (Prop l2) of
Just s -> equalSort (Prop l) s
Nothing -> synEq (Prop l) (FunSort s1 $ Prop l2)
SizeUniv -> equalSort SizeUniv s2
_ -> synEq s0 (FunSort s1 s2)
isBottomSort :: Bool -> Sort -> Bool
isBottomSort propEnabled (Prop (ClosedLevel 0)) = True
isBottomSort propEnabled (Type (ClosedLevel 0)) = not propEnabled
isBottomSort propEnabled _ = False
definitelyNotInf :: Sort -> Bool
definitelyNotInf = \case
Inf -> False
Type{} -> True
Prop{} -> True
SizeUniv -> True
PiSort{} -> False
FunSort{} -> False
UnivSort{} -> False
MetaS{} -> False
DefS{} -> False
DummyS{} -> False
forceType :: Sort -> m Level
forceType (Type l) = return l
forceType s = do
l <- newLevelMeta
equalSort s (Type l)
return l
forceProp :: Sort -> m Level
forceProp (Prop l) = return l
forceProp s = do
l <- newLevelMeta
equalSort s (Prop l)
return l
impossibleSort s = do
reportS "impossible" 10
[ "equalSort: found dummy sort with description:"
, s
]
__IMPOSSIBLE__
catchInequalLevel m fail = m `catchError` \case
TypeError{} -> fail
err -> throwError err
forallFaceMaps :: MonadConversion m => Term -> (Map.Map Int Bool -> MetaId -> Term -> m a) -> (Substitution -> m a) -> m [a]
forallFaceMaps t kb k = do
reportSDoc "conv.forall" 20 $
fsep ["forallFaceMaps"
, prettyTCM t
]
as <- decomposeInterval t
boolToI <- do
io <- primIOne
iz <- primIZero
return (\b -> if b then io else iz)
forM as $ \ (ms,ts) -> do
ifBlockeds ts (kb ms) $ \ _ _ -> do
let xs = map (id -*- boolToI) $ Map.toAscList ms
cxt <- getContext
reportSDoc "conv.forall" 20 $
fsep ["substContextN"
, prettyTCM cxt
, prettyTCM xs
]
(cxt',sigma) <- substContextN cxt xs
resolved <- forM xs (\ (i,t) -> (,) <$> lookupBV i <*> return (applySubst sigma t))
updateContext sigma (const cxt') $
addBindings resolved $ do
cl <- buildClosure ()
tel <- getContextTelescope
m <- currentModule
sub <- getModuleParameterSub m
reportS "conv.forall" 10
[ replicate 10 '-'
, show (envCurrentModule $ clEnv cl)
, show (envLetBindings $ clEnv cl)
, show tel
, show sigma
, show m
, show sub
]
k sigma
where
ifBlockeds ts blocked unblocked = do
and <- getPrimitiveTerm "primIMin"
io <- primIOne
let t = foldr (\ x r -> and `apply` [argN x,argN r]) io ts
ifBlocked t blocked unblocked
addBindings [] m = m
addBindings ((Dom{domInfo = info,unDom = (nm,ty)},t):bs) m = addLetBinding info nm t ty (addBindings bs m)
substContextN :: MonadConversion m => Context -> [(Int,Term)] -> m (Context , Substitution)
substContextN c [] = return (c, idS)
substContextN c ((i,t):xs) = do
(c', sigma) <- substContext i t 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 i t [] = __IMPOSSIBLE__
substContext i t (x:xs) | i == 0 = return $ (xs , singletonS 0 t)
substContext i t (x:xs) | i > 0 = do
reportSDoc "conv.forall" 20 $
fsep ["substContext"
, text (show (i-1))
, prettyTCM t
, prettyTCM xs
]
(c,sigma) <- substContext (i-1) t xs
let e = applySubst sigma x
return (e:c, liftS 1 sigma)
substContext i t (x:xs) = __IMPOSSIBLE__
compareInterval :: MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
compareInterval cmp i t u = do
reportSDoc "tc.conv.interval" 15 $
sep [ "{ compareInterval" <+> prettyTCM t <+> "=" <+> prettyTCM u ]
tb <- reduceB t
ub <- reduceB u
let t = ignoreBlocking tb
u = ignoreBlocking ub
it <- decomposeInterval' t
iu <- decomposeInterval' u
case () of
_ | blockedOrMeta tb || blockedOrMeta ub -> do
interval <- elInf $ primInterval
compareAtom CmpEq (AsTermsOf interval) t u
_ | otherwise -> do
x <- leqInterval it iu
y <- leqInterval iu it
let final = isCanonical it && isCanonical 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
where
blockedOrMeta Blocked{} = True
blockedOrMeta (NotBlocked _ (MetaV{})) = True
blockedOrMeta _ = False
type Conj = (Map.Map Int (Set.Set Bool),[Term])
isCanonical :: [Conj] -> Bool
isCanonical = all (null . snd)
leqInterval :: MonadConversion m => [Conj] -> [Conj] -> m Bool
leqInterval r q =
and <$> forM r (\ r_i ->
or <$> forM q (\ q_j -> leqConj r_i q_j))
leqConj :: MonadConversion m => Conj -> Conj -> m Bool
leqConj (rs,rst) (qs,qst) = do
case toSet qs `Set.isSubsetOf` toSet rs of
False -> return False
True -> do
interval <- elInf $ fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinInterval
let eqT t u = tryConversion (compareAtom CmpEq (AsTermsOf interval) t u)
let listSubset ts us = and <$> forM ts (\ t ->
or <$> forM us (\ u -> eqT t u))
listSubset qst rst
where
toSet m = Set.fromList [ (i,b) | (i,bs) <- Map.toList m, b <- Set.toList bs]
equalTermOnFace :: MonadConversion m => Term -> Type -> Term -> Term -> m ()
equalTermOnFace = compareTermOnFace CmpEq
compareTermOnFace :: MonadConversion m => Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace = compareTermOnFace' compareTerm
compareTermOnFace' :: MonadConversion m => (Comparison -> Type -> Term -> Term -> m ()) -> Comparison -> Term -> Type -> Term -> Term -> m ()
compareTermOnFace' k cmp phi ty u v = do
phi <- reduce phi
_ <- forallFaceMaps phi postponed
$ \ alpha -> k cmp (applySubst alpha ty) (applySubst alpha u) (applySubst alpha v)
return ()
where
postponed ms i psi = do
phi <- runNamesT [] $ do
imin <- cl $ getPrimitiveTerm "primIMin"
ineg <- cl $ getPrimitiveTerm "primINeg"
psi <- open psi
let phi = foldr (\ (i,b) r -> do i <- open (var i); pure imin <@> (if b then i else pure ineg <@> i) <@> r)
psi (Map.toList ms)
phi
addConstraint (ValueCmpOnFace cmp phi ty u v)
bothAbsurd :: MonadConversion m => QName -> QName -> m Bool
bothAbsurd f f'
| isAbsurdLambdaName f, isAbsurdLambdaName f' = do
def <- getConstInfo f
def' <- getConstInfo f'
case (theDef def, theDef def') of
(Function{ funClauses = [Clause{ clauseBody = Nothing }] },
Function{ funClauses = [Clause{ clauseBody = Nothing }] }) -> return True
_ -> return False
| otherwise = return False