{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Conversion where
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.List as List
import Data.Traversable hiding (mapM, sequence)
import Agda.Syntax.Abstract.Views (isSet)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Translation.InternalToAbstract (reify)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.CompiledClause (CompiledClauses'(Fail))
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.MetaVars.Occurs (killArgs,PruneResult(..))
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import qualified Agda.TypeChecking.SyntacticEquality as SynEq
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (infer)
import Agda.TypeChecking.Errors
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.ProjectionLike (elimView)
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.Size
import Agda.Utils.Tuple
import Agda.Utils.Lens
#include "undefined.h"
import Agda.Utils.Impossible
tryConversion :: TCM () -> TCM Bool
tryConversion = isJust <.> tryConversion'
tryConversion' :: TCM a -> TCM (Maybe a)
tryConversion' m = tryMaybe $ disableDestructiveUpdate $ 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 :: Type -> Term -> Term -> TCM ()
equalTerm = compareTerm CmpEq
equalAtom :: Type -> Term -> Term -> TCM ()
equalAtom = compareAtom CmpEq
equalType :: Type -> Type -> TCM ()
equalType = compareType CmpEq
convError :: TypeError -> TCM ()
convError err = ifM ((==) Irrelevant <$> asks envRelevance) (return ()) $ typeError err
compareTerm :: Comparison -> Type -> Term -> Term -> TCM ()
compareTerm cmp a u v = do
reportSDoc "tc.conv.term" 10 $ sep
[ text "compareTerm"
, nest 2 $ prettyTCM u <+> prettyTCM cmp <+> prettyTCM v
, nest 2 $ text ":" <+> prettyTCM a
]
((u, v), equal) <- runReduceM $ SynEq.checkSyntacticEquality u v
unifyPointers cmp 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
[ text "compareTerm (not syntactically equal)"
, nest 2 $ prettyTCM u <+> prettyTCM cmp <+> prettyTCM v
, nest 2 $ text ":" <+> prettyTCM a
]
let fallback = compareTerm' cmp a u v
unlessSubtyping cont =
if cmp == CmpEq then cont else do
ifBlockedType 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` compareTerm' cmp a u v
| 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 dir x es v = do
reportSDoc "tc.conv.term.shortcut" 20 $ sep
[ text "attempting shortcut"
, nest 2 $ prettyTCM (MetaV x es) <+> text ":=" <+> prettyTCM v
]
ifM (isInstantiatedMeta x) patternViolation $ do
assignE dir x es v $ compareTermDir dir a
reportSDoc "tc.conv.term.shortcut" 50 $
text "shortcut successful" $$ nest 2 (text "result:" <+> (pretty =<< instantiate (MetaV x es)))
orelse m h = catchError m (\_ -> h)
unifyPointers :: Comparison -> Term -> Term -> TCM () -> TCM ()
unifyPointers _ _ _ action = action
assignE :: CompareDirection -> MetaId -> Elims -> Term -> (Term -> Term -> TCM ()) -> TCM ()
assignE dir x es v comp = assignWrapper dir x es v $ do
case allApplyElims es of
Just vs -> assignV dir x vs v
Nothing -> do
reportSDoc "tc.conv.assign" 30 $ sep
[ text "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
[ text "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
compareTermDir :: CompareDirection -> Type -> Term -> Term -> TCM ()
compareTermDir dir a = dirToCmp (`compareTerm'` a) dir
compareTerm' :: Comparison -> Type -> Term -> Term -> TCM ()
compareTerm' cmp a m n =
verboseBracket "tc.conv.term" 20 "compareTerm" $ do
a' <- reduce a
catchConstraint (ValueCmp cmp a' m n) $ do
reportSDoc "tc.conv.term" 30 $ fsep
[ text "compareTerm", prettyTCM m, prettyTCM cmp, prettyTCM n, text ":", prettyTCM a' ]
proofIrr <- proofIrrelevance
isSize <- isJust <$> isSizeType a'
s <- reduce $ getSort a'
mlvl <- tryMaybe primLevel
reportSDoc "tc.conv.level" 60 $ nest 2 $ sep
[ text "a' =" <+> pretty a'
, text "mlvl =" <+> pretty mlvl
, text $ "(Just (unEl a') == mlvl) = " ++ show (Just (unEl a') == mlvl)
]
case s of
Prop | proofIrr -> return ()
_ | 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 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 <+> text "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 a' (ignoreBlocking m) (ignoreBlocking n)
_ | mNeutral && nNeutral -> do
isSing <- isSingletonRecordModuloRelevance r ps
case isSing of
Right True -> return ()
_ -> compareAtom cmp 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 $ sort Prop) (Con c ConOSystem []) m' n'
else compareAtom cmp a' m n
_ -> compareAtom cmp a' m n
where
equalFun :: Term -> Term -> Term -> TCM ()
equalFun (Pi dom@(Dom info _) b) m n = do
name <- freshName_ $ suggest (absName b) "x"
addContext (name, dom) $ compareTerm cmp (absBody b) m' n'
where
(m',n') = raise 1 (m,n) `apply` [Arg info $ var 0]
equalFun _ _ _ = __IMPOSSIBLE__
compareTel :: Type -> Type ->
Comparison -> Telescope -> Telescope -> TCM ()
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@(Dom i1 a1) tel1, ExtendTel dom2@(Dom i2 a2) tel2) -> do
compareDom cmp dom1 dom2 tel1 tel2 bad bad $
compareTel t1 t2 cmp (absBody tel1) (absBody tel2)
where
bad = typeError $ UnequalTypes cmp t2 t1
etaInequal :: Comparison -> Type -> Term -> Term -> TCM ()
etaInequal cmp t m n = do
let inequal = typeError $ UnequalTerms cmp m n t
dontKnow = do
reportSDoc "tc.conv.inequal" 20 $ hsep
[ text "etaInequal: postponing "
, prettyTCM m
, text " != "
, prettyTCM n
]
patternViolation
flip (ifBlockedType t) (\ _ _ -> inequal) $ \ _ _ -> do
case (m, n) of
(Con{}, _) -> dontKnow
(_, Con{}) -> dontKnow
(Lam{}, _) -> dontKnow
(_, Lam{}) -> dontKnow
_ -> inequal
compareAtomDir :: CompareDirection -> Type -> Term -> Term -> TCM ()
compareAtomDir dir a = dirToCmp (`compareAtom` a) dir
computeElimHeadType :: QName -> Elims -> Elims -> TCM 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 $
text "inferring type of internal arg: " <+> prettyTCM arg
targ <- infer $ unArg arg
reportSDoc "tc.conv.infer" 30 $
text "inferred type: " <+> prettyTCM targ
fromMaybeM patternViolation $ getDefType f =<< reduce targ
compareAtom :: Comparison -> Type -> Term -> Term -> TCM ()
compareAtom cmp t m n =
verboseBracket "tc.conv.atom" 20 "compareAtom" $
catchConstraint (ValueCmp cmp t m n) $ do
reportSDoc "tc.conv.atom" 50 $
text "compareAtom" <+> fsep [ prettyTCM m <+> prettyTCM cmp
, prettyTCM n
, text ":" <+> prettyTCM t ]
(mb',nb') <- ifM (asks 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''
let m = ignoreBlocking mb
n = ignoreBlocking nb
postpone = addConstraint $ ValueCmp cmp t m n
checkSyntacticEquality = do
n <- normalise n
m <- normalise m
if m == n
then return ()
else postpone
dir = fromCmp cmp
rid = flipCmp dir
assign dir x es v = assignE dir x es v $ compareAtomDir dir t
unifyPointers cmp (ignoreBlocking mb') (ignoreBlocking nb') $ do
reportSDoc "tc.conv.atom" 30 $
text "compareAtom" <+> fsep [ prettyTCM mb <+> prettyTCM cmp
, prettyTCM nb
, text ":" <+> prettyTCM t ]
case (mb, nb) of
(NotBlocked _ (MetaV x xArgs), NotBlocked _ (MetaV y 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 -> checkSyntacticEquality
| 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) (compareTermDir dir t m n) l1
r2 = ifM (isInstantiatedMeta y) (compareTermDir rid t n m) r1
try m h = m `catchError_` \err -> case err of
PatternErr{} -> h
_ -> throwError err
try solve1 solve2
(NotBlocked _ (MetaV x es), _) -> assign dir x es n
(_, NotBlocked _ (MetaV x es)) -> assign rid x es m
(Blocked{}, Blocked{}) -> checkSyntacticEquality
(Blocked{}, _) -> useInjectivity (fromCmp cmp) t m n
(_, Blocked{}) -> useInjectivity (flipCmp $ fromCmp cmp) t n m
_ -> do
case (m, n) of
(Pi{}, Pi{}) -> equalFun m n
(Sort s1, Sort Inf) -> return ()
(Sort s1, Sort s2) -> compareSort CmpEq 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 [], Def f' []) | f == f' -> return ()
(Def f es, Def f' es') | f == f' -> do
a <- computeElimHeadType f es es'
pol <- getPolarity' cmp f
compareElims pol [] a (Def f []) es es'
(Def f es, Def f' es') ->
unlessM (bothAbsurd f f') $ do
trySizeUniv cmp t m n f es f' es'
(Con x ci xArgs, Con y _ yArgs)
| x == y -> do
a' <- conType x t
forcedArgs <- getForcedArgs $ conName x
compareElims (repeat $ polFromCmp cmp) forcedArgs a' (Con x ci []) xArgs yArgs
_ -> etaInequal cmp t m n
where
conType c t = ifBlockedType t (\ _ _ -> patternViolation) $ \ _ t -> do
let impossible = do
reportSDoc "impossible" 10 $
text "expected data/record type, found " <+> prettyTCM t
reportSDoc "impossible" 70 $ nest 2 $ text "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
[ text "t1 =" <+> prettyTCM t1
, text "t2 =" <+> prettyTCM t2 ]
compareDom cmp dom2 dom1 b1 b2 errH errR $
compareType cmp (absBody b1) (absBody b2)
where
errH = typeError $ UnequalHiding t1 t2
errR = typeError $ UnequalRelevance cmp t1 t2
_ -> __IMPOSSIBLE__
compareDom :: Free c
=> Comparison
-> Dom Type
-> Dom Type
-> Abs b
-> Abs c
-> TCM ()
-> TCM ()
-> TCM ()
-> TCM ()
compareDom cmp dom1@(Dom i1 a1) dom2@(Dom i2 a2) b1 b2 errH errR cont
| not (sameHiding dom1 dom2) = errH
| not $ compareRelevance cmp (getRelevance dom1) (getRelevance dom2) = errR
| otherwise = do
let r = max (getRelevance dom1) (getRelevance dom2)
dependent = (r /= Irrelevant) && isBinderUsed b2
pid <- newProblem_ $ compareType cmp a1 a2
dom <- if dependent
then Dom i1 <$> blockTypeOnProblem a1 pid
else return dom1
name <- freshName_ $ suggest b1 b2
addContext (name, dom) $ cont
stealConstraints pid
compareRelevance :: Comparison -> Relevance -> Relevance -> Bool
compareRelevance CmpEq = (==)
compareRelevance CmpLeq = (<=)
antiUnify :: ProblemId -> Type -> Term -> Term -> TCM Term
antiUnify pid a u v = do
((u, v), eq) <- runReduceM (SynEq.checkSyntacticEquality u v)
if eq then return u else do
(u, v) <- reduce (u, 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 (unAbs ub) (unAbs vb)
return $ Pi wa (wb <$ ub)
(Lam i u, Lam _ v) ->
case unEl a of
Pi a b -> Lam i . (<$ u) <$> addContext a (antiUnify pid (unAbs b) (unAbs u) (unAbs 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
fallback = blockTermOnProblem a u pid
maybeGiveUp m = m `catchError_` \ err ->
case err of
PatternErr{} -> fallback
_ -> throwError err
antiUnifyType :: ProblemId -> Type -> Type -> TCM Type
antiUnifyType pid (El s a) (El _ b) = El s <$> antiUnify pid (sort s) a b
antiUnifyElims :: ProblemId -> Type -> Term -> Elims -> Elims -> TCM 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
case unEl a of
Pi a b -> do
w <- antiUnify pid (unDom a) (unArg u) (unArg v)
antiUnifyElims pid (b `lazyAbsApp` w) (apply self [w <$ u]) es1 es2
_ -> patternViolation
antiUnifyElims _ _ _ _ _ = patternViolation
compareElims :: [Polarity] -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
compareElims pols0 fors0 a v els01 els02 = catchConstraint (ElimCmp pols0 fors0 a v els01 els02) $ do
let v1 = applyE v els01
v2 = applyE v els02
failure = typeError $ UnequalTerms CmpEq v1 v2 a
unless (null els01) $ do
reportSDoc "tc.conv.elim" 25 $ text "compareElims" $$ do
nest 2 $ vcat
[ text "a =" <+> prettyTCM a
, text "pols0 (truncated to 10) =" <+> sep (map prettyTCM $ take 10 pols0)
, text "fors0 (truncated to 10) =" <+> sep (map prettyTCM $ take 10 fors0)
, text "v =" <+> prettyTCM v
, text "els01 =" <+> prettyTCM els01
, text "els02 =" <+> prettyTCM els02
]
case (els01, els02) of
([] , [] ) -> return ()
([] , Proj{}:_ ) -> failure
(Proj{} : _, [] ) -> failure
([] , Apply{} : _) -> failure
(Apply{} : _, [] ) -> failure
(Apply{} : _, Proj{} : _) -> __IMPOSSIBLE__ <$ solveAwakeConstraints' True
(Proj{} : _, Apply{} : _) -> __IMPOSSIBLE__ <$ solveAwakeConstraints' True
(Apply arg1 : els1, Apply arg2 : els2) ->
verboseBracket "tc.conv.elim" 20 "compare Apply" $ do
reportSDoc "tc.conv.elim" 10 $ nest 2 $ vcat
[ text "a =" <+> prettyTCM a
, text "v =" <+> prettyTCM v
, text "arg1 =" <+> prettyTCM arg1
, text "arg2 =" <+> prettyTCM arg2
]
reportSDoc "tc.conv.elim" 50 $ nest 2 $ vcat
[ text "v =" <+> pretty v
, text "arg1 =" <+> pretty arg1
, text "arg2 =" <+> pretty arg2
, text ""
]
let (pol, pols) = nextPolarity pols0
(for, fors) = nextIsForced fors0
ifBlockedType a (\ m t -> patternViolation) $ \ _ a -> do
case unEl a of
(Pi (Dom info b) codom) -> do
mlvl <- tryMaybe primLevel
let freeInCoDom (Abs _ c) = 0 `freeInIgnoringSorts` c
freeInCoDom _ = False
dependent = (Just (unEl b) /= mlvl) && freeInCoDom codom
r = getRelevance info
pid <- newProblem_ $ applyRelevanceToContext r $
if isForced for then
return ()
else if isIrrelevant r then
compareIrrelevant b (unArg arg1) (unArg arg2)
else
compareWithPol pol (flip compareTerm b)
(unArg arg1) (unArg arg2)
solved <- isProblemSolved pid
arg <- if dependent && not solved
then do
arg <- (arg1 $>) <$> antiUnify pid b (unArg arg1) (unArg arg2)
reportSDoc "tc.conv.elims" 30 $ hang (text "Anti-unification:") 2 (prettyTCM arg)
reportSDoc "tc.conv.elims" 70 $ nest 2 $ text "raw:" <+> pretty arg
return arg
else return arg1
compareElims pols fors (codom `lazyAbsApp` unArg arg) (apply v [arg]) els1 els2
stealConstraints pid
a -> do
reportSDoc "impossible" 10 $
text "unexpected type when comparing apply eliminations " <+> prettyTCM a
reportSDoc "impossible" 50 $ text "raw type:" <+> pretty a
patternViolation
(Proj o f : els1, Proj _ f' : els2)
| f /= f' -> typeError . GenericError . show =<< prettyTCM f <+> text "/=" <+> prettyTCM f'
| otherwise -> ifBlockedType 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 :: Type -> Term -> Term -> TCM ()
compareIrrelevant t v w = do
reportSDoc "tc.conv.irr" 20 $ vcat
[ text "compareIrrelevant"
, nest 2 $ text "v =" <+> prettyTCM v
, nest 2 $ text "w =" <+> prettyTCM w
]
reportSDoc "tc.conv.irr" 50 $ vcat
[ nest 2 $ text "v =" <+> pretty v
, nest 2 $ text "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 $ text "inst =" <+> pretty inst
]
if not (isIrrelevant rel) || inst
then fallback
else (assignE DirEq x es w $ compareIrrelevant t) `catchError` \ _ -> fallback
try v w fallback = fallback
compareWithPol :: Polarity -> (Comparison -> a -> a -> TCM ()) -> a -> a -> TCM ()
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 :: [Polarity] -> [IsForced] -> Type -> Term -> Args -> Args -> TCM ()
compareArgs pol for a v args1 args2 =
compareElims pol for a v (map Apply args1) (map Apply args2)
compareType :: Comparison -> Type -> Type -> TCM ()
compareType cmp ty1@(El s1 a1) ty2@(El s2 a2) =
verboseBracket "tc.conv.type" 20 "compareType" $
catchConstraint (TypeCmp cmp ty1 ty2) $ do
reportSDoc "tc.conv.type" 50 $ vcat
[ text "compareType" <+> sep [ prettyTCM ty1 <+> prettyTCM cmp
, prettyTCM ty2 ]
, hsep [ text " sorts:", prettyTCM s1, text " and ", prettyTCM s2 ]
]
compareSort CmpEq s1 s2 `catchError` \err -> case err of
TypeError _ e -> do
reportSDoc "tc.conv.type" 30 $ vcat
[ text "sort comparison failed"
, nest 2 $ vcat
[ text "s1 =" <+> prettyTCM s1
, text "s2 =" <+> prettyTCM s2
]
]
case clValue e of
SetOmegaNotValidType -> typeError $ UnequalBecauseOfUniverseConflict cmp a1 a2
_ -> do
compareTerm cmp (sort s1) a1 a2
compareSort CmpEq s1 s2
_ -> throwError err
compareTerm cmp (sort s1) a1 a2
return ()
leqType :: Type -> Type -> TCM ()
leqType = compareType CmpLeq
coerce :: Term -> Type -> Type -> TCM Term
coerce 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 $
text "coerce" <+> vcat
[ text "term v =" <+> prettyTCM v
, text "from type t1 =" <+> prettyTCM a1
, text "to type t2 =" <+> prettyTCM a2
]
reportSDoc "tc.conv.coerce" 70 $
text "coerce" <+> vcat
[ text "term v =" <+> pretty v
, text "from type t1 =" <+> pretty t1
, text "to type t2 =" <+> pretty t2
]
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
ifBlockedType b2 (\ _ _ -> fallback) $ \ _ _ -> do
(args, t1') <- implicitArgs n notVisible t1
let v' = v `apply` args
v' <$ coerceSize leqType v' t1' t2
where
fallback = v <$ coerceSize leqType v t1 t2
coerceSize :: (Type -> Type -> TCM ()) -> Term -> Type -> Type -> TCM ()
coerceSize leqType v t1 t2 = workOnTypes $ do
reportSDoc "tc.conv.coerce" 70 $
text "coerceSize" <+> vcat
[ text "term v =" <+> pretty v
, text "from type t1 =" <+> pretty t1
, text "to type t2 =" <+> pretty t2
]
let fallback = leqType t1 t2
done = caseMaybeM (isSizeType t1) fallback $ \ _ -> return ()
caseMaybeM (isSizeType 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.coerce" 20 $ text "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 :: Comparison -> Level -> Level -> TCM ()
compareLevel CmpLeq u v = leqLevel u v
compareLevel CmpEq u v = equalLevel u v
compareSort :: Comparison -> Sort -> Sort -> TCM ()
compareSort CmpEq = equalSort
compareSort CmpLeq = leqSort
leqSort :: Sort -> Sort -> TCM ()
leqSort s1 s2 = catchConstraint (SortCmp CmpLeq s1 s2) $ do
(s1,s2) <- reduce (s1,s2)
let postpone = addConstraint (SortCmp CmpLeq s1 s2)
no = typeError $ NotLeqSort s1 s2
yes = return ()
reportSDoc "tc.conv.sort" 30 $
sep [ text "leqSort"
, nest 2 $ fsep [ prettyTCM s1 <+> text "=<"
, prettyTCM s2 ]
]
case (s1, s2) of
(Type a , Type b ) -> leqLevel a b
(Prop , _ ) -> __IMPOSSIBLE__
(_ , Prop ) -> __IMPOSSIBLE__
(_ , Inf ) -> yes
(Inf , _ ) -> equalSort s1 s2
(_ , Type (Max [])) -> equalSort s1 s2
(_ , SizeUniv) -> equalSort s1 s2
(UnivSort s, Type b )
| Just b' <- levelSucView b -> leqSort s (Type b')
(Type a , UnivSort s)
| Just a' <- levelSucView a -> leqSort (Type a') s
(SizeUniv, Type{} ) -> no
(PiSort{}, _ ) -> postpone
(_ , PiSort{}) -> postpone
(UnivSort{}, _ ) -> postpone
(_ , UnivSort{}) -> postpone
(MetaS{} , _ ) -> postpone
(_ , MetaS{} ) -> postpone
leqLevel :: Level -> Level -> TCM ()
leqLevel a b = liftTCM $ do
reportSDoc "tc.conv.nat" 30 $
text "compareLevel" <+>
sep [ prettyTCM a <+> text "=<"
, prettyTCM b ]
a <- normalise a
b <- normalise b
leqView a b
where
leqView a@(Max as) b@(Max bs) = catchConstraint (LevelCmp CmpLeq a b) $ do
reportSDoc "tc.conv.nat" 30 $
text "compareLevelView" <+>
sep [ pretty a <+> text "=<"
, pretty b ]
wrap $ case (as, bs) of
_ | as == bs -> ok
([], _) -> ok
(as, []) -> sequence_ [ equalLevel' (Max [a]) (Max []) | a <- as ]
(as, [ClosedLevel 0]) -> sequence_ [ equalLevel' (Max [a]) (Max []) | a <- as ]
(as@(_:_:_), [b]) -> sequence_ [ leqView (Max [a]) (Max [b]) | a <- as ]
(as, bs) | minN > 0 -> leqView (Max $ map (subtr minN) as) (Max $ map (subtr minN) bs)
where
ns = map constant as
ms = map constant bs
minN = minimum (ns ++ ms)
(as, bs)
| not $ null subsumed -> leqView (Max $ as List.\\ subsumed) (Max bs)
where
subsumed = [ a | a@(Plus m l) <- as, n <- findN l, m <= n ]
findN a = case [ n | Plus n b <- bs, b == a ] of
[n] -> [n]
_ -> []
([ClosedLevel n], [ClosedLevel m]) -> if n <= m then ok else notok
([ClosedLevel n], bs)
| n <= maximum (map constant bs) -> ok
(as, bs)
| neutralB && maxA > maxB -> notok
| neutralB && any (\a -> neutral a && not (isInB a)) as -> notok
| neutralB && neutralA -> maybeok $ all (\a -> constant a <= findN a) as
where
maxA = maximum $ map constant as
maxB = maximum $ map constant bs
neutralA = all neutral as
neutralB = all neutral bs
isInB a = elem (unneutral a) $ map unneutral bs
findN a = case [ n | b@(Plus n _) <- bs, unneutral b == unneutral a ] of
[n] -> n
_ -> __IMPOSSIBLE__
_ -> postpone
where
ok = return ()
notok = unlessM typeInType $ typeError $ NotLeqSort (Type a) (Type b)
postpone = patternViolation
wrap m = catchError m $ \e ->
case e of
TypeError{} -> notok
_ -> throwError e
maybeok True = ok
maybeok False = notok
neutral (Plus _ NeutralLevel{}) = True
neutral _ = False
meta (Plus _ MetaLevel{}) = True
meta _ = False
unneutral (Plus _ (NeutralLevel _ v)) = v
unneutral _ = __IMPOSSIBLE__
constant (ClosedLevel n) = n
constant (Plus n _) = n
subtr m (ClosedLevel n) = ClosedLevel (n - m)
subtr m (Plus n l) = Plus (n - m) l
equalLevel :: Level -> Level -> TCM ()
equalLevel a b = do
(a, b) <- normalise (a, b)
equalLevel' a b
equalLevel' :: Level -> Level -> TCM ()
equalLevel' a b = do
reportSDoc "tc.conv.level" 50 $ sep [ text "equalLevel", nest 2 $ parens $ pretty a, nest 2 $ parens $ pretty b ]
liftTCM $ catchConstraint (LevelCmp CmpEq a b) $
check a b
where
check a@(Max as) b@(Max bs) = do
as <- return $ [ a | a <- as, not $ a `isStrictlySubsumedBy` bs ]
bs <- return $ [ b | b <- bs, not $ b `isStrictlySubsumedBy` as ]
as <- return $ List.sort $ closed0 as
bs <- return $ List.sort $ closed0 bs
reportSDoc "tc.conv.level" 40 $
sep [ text "equalLevel"
, vcat [ nest 2 $ sep [ prettyTCM a <+> text "=="
, prettyTCM b
]
, text "reduced"
, nest 2 $ sep [ prettyTCM (Max as) <+> text "=="
, prettyTCM (Max bs)
]
]
]
reportSDoc "tc.conv.level" 50 $
sep [ text "equalLevel"
, vcat [ nest 2 $ sep [ pretty (Max as) <+> text "=="
, pretty (Max bs)
]
]
]
case (as, bs) of
_ | as == bs -> ok
| any isBlocked (as ++ bs) -> do
lvl <- levelType
liftTCM $ addConstraint $ ValueCmp CmpEq lvl (Level a) (Level b)
([ClosedLevel n], [ClosedLevel m])
| n == m -> ok
| otherwise -> notok
([ClosedLevel{}], _) | any isNeutral bs -> notok
(_, [ClosedLevel{}]) | any isNeutral as -> notok
([ClosedLevel 0], bs@(_:_:_)) -> sequence_ [ equalLevel' (Max []) (Max [b]) | b <- bs ]
(as@(_:_:_), [ClosedLevel 0]) -> sequence_ [ equalLevel' (Max [a]) (Max []) | a <- as ]
([Plus n (MetaLevel x as)], _)
| any (isThisMeta x) bs -> postpone
(_, [Plus n (MetaLevel x bs)])
| any (isThisMeta x) as -> postpone
([Plus n (MetaLevel x as')], [Plus m (MetaLevel y bs')])
| (n, y) < (m, x) -> meta n x as' bs
| otherwise -> meta m y bs' as
([Plus n (MetaLevel x as')],_) -> meta n x as' bs
(_,[Plus m (MetaLevel y bs')]) -> meta m y bs' as
_ | any hasMeta (as ++ bs) -> postpone
_ | all isNeutralOrClosed (as ++ bs) -> do
reportSLn "tc.conv.level" 60 $ "equalLevel: all are neutral or closed"
if length as == length bs
then zipWithM_ (\a b -> [a] =!= [b]) as bs
else notok
_ -> postpone
where
a === b = unlessM typeInType $ do
lvl <- levelType
equalAtom lvl a b
as =!= bs = levelTm (Max as) === levelTm (Max bs)
ok = return ()
notok = unlessM typeInType notOk
notOk = typeError $ UnequalSorts (Type a) (Type b)
postpone = do
reportSDoc "tc.conv.level" 30 $ hang (text "postponing:") 2 $ hang (pretty a <+> text "==") 0 (pretty b)
patternViolation
closed0 [] = [ClosedLevel 0]
closed0 as = as
meta n x as bs = do
reportSLn "tc.meta.level" 30 $ "Assigning meta level"
reportSDoc "tc.meta.level" 50 $ text "meta" <+> sep [prettyList $ map pretty as, prettyList $ map pretty bs]
bs' <- mapM (subtr n) bs
assignE DirEq x as (levelTm (Max bs')) (===)
wrap m = m `catchError` \err ->
case err of
TypeError{} -> notok
_ -> throwError err
subtr n (ClosedLevel m)
| m >= n = return $ ClosedLevel (m - n)
| otherwise = ifM typeInType (return $ ClosedLevel 0) $ notOk
subtr n (Plus m a)
| m >= n = return $ Plus (m - n) a
subtr _ (Plus _ BlockedLevel{}) = postpone
subtr _ (Plus _ MetaLevel{}) = postpone
subtr _ (Plus _ NeutralLevel{}) = postpone
subtr _ (Plus _ UnreducedLevel{}) = __IMPOSSIBLE__
isNeutral (Plus _ NeutralLevel{}) = True
isNeutral _ = False
isClosed ClosedLevel{} = True
isClosed _ = False
isNeutralOrClosed l = isClosed l || isNeutral l
isBlocked (Plus _ BlockedLevel{}) = True
isBlocked _ = False
hasMeta ClosedLevel{} = False
hasMeta (Plus _ MetaLevel{}) = True
hasMeta (Plus _ (BlockedLevel _ v)) = not $ null $ allMetas v
hasMeta (Plus _ (NeutralLevel _ v)) = not $ null $ allMetas v
hasMeta (Plus _ (UnreducedLevel v)) = not $ null $ allMetas v
isThisMeta x (Plus _ (MetaLevel y _)) = x == y
isThisMeta _ _ = False
constant (ClosedLevel n) = n
constant (Plus n _) = n
(ClosedLevel m) `isStrictlySubsumedBy` [] = m == 0
(ClosedLevel m) `isStrictlySubsumedBy` ys = m < maximum (map constant ys)
(Plus m x) `isStrictlySubsumedBy` ys = not $ null $
[ n | Plus n y <- ys, x == y, m < n ]
equalSort :: Sort -> Sort -> TCM ()
equalSort s1 s2 = do
catchConstraint (SortCmp CmpEq s1 s2) $ do
(s1,s2) <- reduce (s1,s2)
let postpone = addConstraint (SortCmp CmpEq s1 s2)
yes = return ()
no = unlessM typeInType $ typeError $ UnequalSorts s1 s2
reportSDoc "tc.conv.sort" 30 $ sep
[ text "equalSort"
, vcat [ nest 2 $ fsep [ prettyTCM s1 <+> text "=="
, prettyTCM s2 ]
, nest 2 $ fsep [ pretty s1 <+> text "=="
, pretty s2 ]
]
]
case (s1, s2) of
_ | s1 == s2 -> return ()
(MetaS x es , MetaS y es')
| 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
(SizeUniv , SizeUniv ) -> yes
(Prop , Prop ) -> yes
(Inf , Inf ) -> yes
(Type a , UnivSort s )
| Just a' <- levelSucView a -> equalSort (Type a') s
(UnivSort s , Type b )
| Just b' <- levelSucView b -> equalSort s (Type b')
(Type (Max []) , PiSort a b ) -> piSortEqualToSet0 a b
(PiSort a b , Type (Max [])) -> piSortEqualToSet0 a b
(SizeUniv , PiSort a b ) ->
underAbstraction_ b $ equalSort SizeUniv
(PiSort a b , SizeUniv ) ->
underAbstraction_ b $ equalSort SizeUniv
(Prop , UnivSort s ) -> no
(UnivSort s , Prop ) -> no
(SizeUniv , UnivSort s ) -> no
(UnivSort s , SizeUniv ) -> no
(PiSort{} , _ ) -> postpone
(_ , PiSort{} ) -> postpone
(UnivSort{} , _ ) -> postpone
(_ , UnivSort{} ) -> postpone
(_ , _ ) -> no
where
meta x es s = do
reportSLn "tc.meta.sort" 30 $ "Assigning meta sort"
reportSDoc "tc.meta.sort" 50 $ text "meta" <+> sep [pretty x, prettyList $ map pretty es, pretty s]
assignE DirEq x es (Sort s) __IMPOSSIBLE__
piSortEqualToSet0 a b = do
let set0 = Type $ Max []
underAbstraction_ b $ equalSort set0
a <- reduce a
case funSort' a set0 of
Just s -> equalSort s set0
Nothing -> addConstraint $ SortCmp CmpEq (funSort a set0) set0
bothAbsurd :: QName -> QName -> TCM Bool
bothAbsurd f f'
| isAbsurdLambdaName f, isAbsurdLambdaName f' = do
def <- getConstInfo f
def' <- getConstInfo f'
case (theDef def, theDef def') of
(Function{ funCompiled = Just Fail},
Function{ funCompiled = Just Fail}) -> return True
_ -> return False
| otherwise = return False