module Agda.TypeChecking.Conversion where
import Control.Applicative
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Error
import Data.Traversable hiding (mapM, sequence)
import Data.List hiding (sort)
import qualified Data.List as List
import Agda.Syntax.Abstract.Views (isSet)
import Agda.Syntax.Literal
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Translation.InternalToAbstract (reify)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.MetaVars.Occurs (killArgs,PruneResult(..))
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Primitive (constructorForm)
import Agda.TypeChecking.Free
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Level
import Agda.TypeChecking.Implicit (implicitArgs)
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Eliminators
import Agda.Utils.Size
import Agda.Utils.Monad
import Agda.Utils.Maybe
import Agda.TypeChecking.Monad.Debug
#include "../undefined.h"
import Agda.Utils.Impossible
mlevel :: TCM (Maybe Term)
mlevel = liftTCM $ (Just <$> primLevel) `catchError` \_ -> return Nothing
sameVars :: Args -> Args -> Bool
sameVars xs ys = and $ zipWith same xs ys
where
same (Arg _ _ (Var n [])) (Arg _ _ (Var m [])) = n == m
same _ _ = False
intersectVars :: Args -> Args -> Maybe [Bool]
intersectVars = zipWithM areVars where
areVars u v | argRelevance u == Irrelevant = Just False
areVars (Arg _ _ (Var n [])) (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
(u, v) <- instantiateFull (u, v)
if u == v then unifyPointers cmp u v $ verboseS "profile.sharing" 20 $ tick "equal terms" else do
verboseS "profile.sharing" 20 $ tick "unequal terms"
let checkPointerEquality def | not $ null $ List.intersect (pointerChain u) (pointerChain v) = do
verboseS "profile.sharing" 10 $ tick "pointer equality"
return ()
checkPointerEquality def = def
checkPointerEquality $ do
reportSDoc "tc.conv.term" 10 $ sep [ text "compareTerm"
, 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
isSize <- isJust <$> do isSizeTypeTest <*> reduce a
if isSize then fallback else cont
case (ignoreSharing u, ignoreSharing 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 x us v, assign y vs u)
| otherwise = (assign y vs u, assign x us v)
(MetaV x us, _) -> unlessSubtyping $ assign x us v `orelse` fallback
(_, MetaV y vs) -> unlessSubtyping $ assign y vs u `orelse` fallback
_ -> fallback
where
assign x us v = do
reportSDoc "tc.conv.term.shortcut" 20 $ sep
[ text "attempting shortcut"
, nest 2 $ prettyTCM (MetaV x us) <+> text ":=" <+> prettyTCM v
]
ifM (isInstantiatedMeta x) patternViolation (assignV x us v)
instantiate u
reportSLn "tc.conv.term.shortcut" 50 $
"shortcut successful\n result: " ++ show u
m `orelse` h = m `catchError` \err -> case err of
PatternErr s -> put s >> h
_ -> h
unifyPointers _ _ _ action = action
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 <- mlevel
case s of
Prop | proofIrr -> return ()
_ | isSize -> compareSizes cmp m n
_ -> case ignoreSharing $ 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 ps -> do
isrec <- isEtaRecord r
if isrec
then do
m <- reduceB m
n <- reduceB n
case (m, n) of
_ | isMeta m || isMeta n ->
compareAtom cmp a' (ignoreBlocking m) (ignoreBlocking n)
_ | isNeutral m && isNeutral n -> 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 [] (telePi_ tel $ sort Prop) (Con c []) m' n'
else compareAtom cmp a' m n
_ -> compareAtom cmp a' m n
where
isNeutral = isNeutral' . fmap ignoreSharing
isMeta = isMeta' . fmap ignoreSharing
isNeutral' (NotBlocked Con{}) = False
isNeutral' _ = True
isMeta' (NotBlocked MetaV{}) = True
isMeta' _ = False
equalFun :: Term -> Term -> Term -> TCM ()
equalFun (Shared p) m n = equalFun (derefPtr p) m n
equalFun (Pi dom@(Dom h r _) b) m n = do
name <- freshName_ $ properName $ absName b
addCtx name dom $ compareTerm cmp (absBody b) m' n'
where
(m',n') = raise 1 (m,n) `apply` [Arg h r $ var 0]
properName "_" = "x"
properName x = x
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 arg1@(Dom h1 r1 a1) tel1, ExtendTel arg2@(Dom h2 r2 a2) tel2)
| h1 /= h2 -> bad
| otherwise -> do
name <- freshName_ (suggest (absName tel1) (absName tel2))
let checkArg = escapeContext 1 $ compareType cmp a1 a2
c = TelCmp t1 t2 cmp (absBody tel1) (absBody tel2)
r = max r1 r2
dependent = (r /= Irrelevant) && isBinderUsed tel2
addCtx name arg1 $
if dependent
then guardConstraint c checkArg
else checkArg >> solveConstraint_ c
where
suggest "_" y = y
suggest x _ = x
where
bad = typeError $ UnequalTypes cmp t2 t1
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' <- etaExpandBlocked =<< reduceB m
nb' <- etaExpandBlocked =<< reduceB n
(mb'', nb'') <- case (ignoreSharing $ ignoreBlocking mb', ignoreSharing $ 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
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 (ignoreSharing <$> mb, ignoreSharing <$> 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) = (l,r)
| otherwise = (r,l)
where l = assignV x xArgs n
r = assignV y yArgs m
try m h = m `catchError_` \err -> case err of
PatternErr s -> put s >> h
_ -> throwError err
try solve1 solve2
(NotBlocked (MetaV x xArgs), _) -> assignV x xArgs n
(_, NotBlocked (MetaV x xArgs)) -> assignV x xArgs m
(Blocked{}, Blocked{}) -> checkSyntacticEquality
(Blocked{}, _) -> useInjectivity cmp t m n
(_,Blocked{}) -> useInjectivity cmp t m n
_ -> case (ignoreSharing m, ignoreSharing n) of
(Pi{}, Pi{}) -> equalFun m n
(Sort s1, Sort s2) -> compareSort CmpEq s1 s2
(Lit l1, Lit l2) | l1 == l2 -> return ()
(Var i iArgs, Var j jArgs) | i == j -> do
a <- typeOfBV i
compareArgs [] a (Var i []) iArgs jArgs
(Def{}, Def{}) -> do
ev1 <- elimView m
ev2 <- elimView n
reportSDoc "tc.conv.atom" 50 $
sep [ text $ "ev1 = " ++ show ev1
, text $ "ev2 = " ++ show ev2 ]
case (ev1, ev2) of
(VarElim x els1, VarElim y els2) | x == y -> cmpElim (typeOfBV x) (Var x []) els1 els2
(ConElim x els1, ConElim y els2) | x == y ->
cmpElim (conType x t) (Con x []) els1 els2
(DefElim x els1, DefElim y els2) | x == y ->
cmpElim (defType <$> getConstInfo x) (Def x []) els1 els2
(DefElim x els1, DefElim y els2) ->
trySizeUniv cmp t m n x els1 y els2
(MetaElim{}, _) -> __IMPOSSIBLE__
(_, MetaElim{}) -> __IMPOSSIBLE__
_ -> typeError $ UnequalTerms cmp m n t
where
polarities (Def x _) = getPolarity' cmp x
polarities _ = return []
cmpElim t v els1 els2 = do
a <- t
pol <- polarities v
reportSDoc "tc.conv.elim" 10 $
text "compareElim" <+> vcat
[ text "a =" <+> prettyTCM a
, text "v =" <+> prettyTCM v
, text "els1 =" <+> prettyTCM els1
, text "els2 =" <+> prettyTCM els2
]
compareElims pol a v els1 els2
(Con x xArgs, Con y yArgs)
| x == y -> do
a' <- conType x t
compareArgs [] a' (Con x []) xArgs yArgs
_ -> typeError $ UnequalTerms cmp m n t
where
conType c (El _ v) = case ignoreSharing v of
Def d args -> do
npars <- do
def <- theDef <$> getConstInfo d
return $ case def of Datatype{dataPars = n} -> n
Record{recPars = n} -> n
_ -> __IMPOSSIBLE__
a <- defType <$> getConstInfo c
return $ piApply a (genericTake npars args)
_ -> __IMPOSSIBLE__
equalFun t1 t2 = case (ignoreSharing t1, ignoreSharing t2) of
(Pi dom1@(Dom h1 r1 a1) b1, Pi (Dom h2 r2 a2) b2)
| h1 /= h2 -> typeError $ UnequalHiding t1 t2
| not (compareRelevance cmp (ignoreForced r2) (ignoreForced r1)) -> typeError $ UnequalRelevance cmp t1 t2
| otherwise -> 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 ]
let checkDom = escapeContext 1 $ compareType cmp a2 a1
conCoDom = TypeCmp cmp (absBody b1) (absBody b2)
name <- freshName_ (suggest b1 b2)
addCtx name dom1 $
if isBinderUsed b2
then guardConstraint conCoDom checkDom
else checkDom >> solveConstraint_ conCoDom
where
suggest b1 b2 = head $
[ x | x <- map absName [b1,b2], x /= "_"] ++ ["_"]
_ -> __IMPOSSIBLE__
compareRelevance :: Comparison -> Relevance -> Relevance -> Bool
compareRelevance CmpEq = (==)
compareRelevance CmpLeq = (<=)
compareElims :: [Polarity] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
compareElims _ _ _ [] [] = return ()
compareElims _ _ _ [] (_:_) = __IMPOSSIBLE__
compareElims _ _ _ (_:_) [] = __IMPOSSIBLE__
compareElims _ _ _ (Apply{} : _) (Proj{} : _) = __IMPOSSIBLE__
compareElims _ _ _ (Proj{} : _) (Apply{} : _) = __IMPOSSIBLE__
compareElims pols0 a v els01@(Apply arg1 : els1) els02@(Apply arg2 : els2) =
verboseBracket "tc.conv.elim" 20 "compare Apply" $ do
reportSDoc "tc.conv.elim" 25 $ 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 =" <+> text (show v)
, text "arg1 =" <+> text (show arg1)
, text "arg2 =" <+> text (show arg2)
]
let (pol, pols) = nextPolarity pols0
ab <- reduceB a
let a = ignoreBlocking ab
catchConstraint (ElimCmp pols0 a v els01 els02) $ do
case ignoreSharing . unEl <$> ab of
Blocked{} -> patternViolation
NotBlocked MetaV{} -> patternViolation
NotBlocked (Pi (Dom _ r b) _) -> do
mlvl <- mlevel
let checkArg = applyRelevanceToContext r $ case r of
Forced -> return ()
r | irrelevantOrUnused r ->
compareIrrelevant b (unArg arg1) (unArg arg2)
_ -> compareWithPol pol (flip compareTerm b)
(unArg arg1) (unArg arg2)
dependent = case ignoreSharing $ unEl a of
Pi (Dom _ _ (El _ lvl')) c -> 0 `freeInIgnoringSorts` absBody c
&& Just lvl' /= mlvl
_ -> False
theRest = ElimCmp pols (piApply a [arg1]) (apply v [arg1]) els1 els2
if dependent
then guardConstraint theRest checkArg
else checkArg >> solveConstraint_ theRest
_ -> __IMPOSSIBLE__
compareElims pols a v els01@(Proj f : els1) els02@(Proj f' : els2)
| f /= f' = typeError . GenericError . show =<< prettyTCM f <+> text "/=" <+> prettyTCM f'
| otherwise = do
a <- reduce a
case ignoreSharing $ unEl a of
Def r us -> do
let (pol, _) = nextPolarity pols
ft <- defType <$> getConstInfo f
let arg = Arg NotHidden Relevant v
let c = piApply ft (us ++ [arg])
(cmp, els1, els2) <- return $ case pol of
Invariant -> (CmpEq, els1, els2)
Covariant -> (CmpLeq, els1, els2)
Contravariant -> (CmpLeq, els2, els1)
Nonvariant -> __IMPOSSIBLE__
pols' <- getPolarity' cmp f
compareElims pols' c (Def f [arg]) els1 els2
_ -> __IMPOSSIBLE__
compareIrrelevant :: Type -> Term -> Term -> TCM ()
compareIrrelevant a 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 = " ++ show v
, nest 2 $ text $ "w = " ++ show w
]
try v w $ try w v $ return ()
where
try (Shared p) w fallback = try (derefPtr p) w fallback
try (MetaV x vs) w fallback = do
mv <- lookupMeta x
let rel = getMetaRelevance mv
inst = case mvInstantiation mv of
InstV{} -> True
InstS{} -> True
_ -> False
reportSDoc "tc.conv.irr" 20 $ vcat
[ nest 2 $ text $ "rel = " ++ show rel
, nest 2 $ text $ "inst = " ++ show inst
]
if not (irrelevantOrUnused rel) || inst then fallback else assignV x vs w
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 ()
compareArgs :: [Polarity] -> Type -> Term -> Args -> Args -> TCM ()
compareArgs pol a v args1 args2 =
compareElims pol 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
throwError err
_ -> 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
]
TelV tel1 b1 <- telViewUpTo' (1) ((NotHidden /=) . domHiding) t1
TelV tel2 b2 <- telViewUpTo' (1) ((NotHidden /=) . domHiding) t2
let n = size tel1 size tel2
if n <= 0 then fallback else do
ifBlockedType b2 (\ _ _ -> fallback) $ \ _ -> do
(args, t1') <- implicitArgs n (NotHidden /=) t1
v `apply` args <$ do workOnTypes $ leqType t1' t2
where
fallback = v <$ do workOnTypes $ leqType t1 t2
compareSort :: Comparison -> Sort -> Sort -> TCM ()
compareSort CmpEq = equalSort
compareSort CmpLeq = equalSort
leqSort :: Sort -> Sort -> TCM ()
leqSort s1 s2 =
ifM typeInType (return ()) $
catchConstraint (SortCmp CmpLeq s1 s2) $
do (s1,s2) <- reduce (s1,s2)
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 , Prop ) -> return ()
(Type _ , Prop ) -> notLeq s1 s2
(Prop , Type _ ) -> return ()
(_ , Inf ) -> return ()
(Inf , _ ) -> equalSort s1 s2
(DLub{} , _ ) -> equalSort s1 s2
(_ , DLub{} ) -> equalSort s1 s2
where
notLeq s1 s2 = typeError $ NotLeqSort s1 s2
leqLevel :: Level -> Level -> TCM ()
leqLevel a b = liftTCM $ do
reportSDoc "tc.conv.nat" 30 $
text "compareLevel" <+>
sep [ prettyTCM a <+> text "=<"
, prettyTCM b ]
a <- reduce a
b <- reduce b
catchConstraint (LevelCmp CmpLeq a b) $ leqView a b
where
leqView a@(Max as) b@(Max bs) = do
reportSDoc "tc.conv.nat" 30 $
text "compareLevelView" <+>
sep [ text (show a) <+> text "=<"
, text (show b) ]
wrap $ case (as, bs) of
_ | as == bs -> ok
([], _) -> ok
(as, []) -> 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 dups -> leqView (Max $ as \\ dups) (Max bs)
where
dups = [ a | a@(Plus m l) <- as, Just n <- [findN l], m <= n ]
findN a = case [ n | Plus n b <- bs, b == a ] of
[n] -> Just n
_ -> Nothing
([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__
([a@(Plus n _)], [b@(Plus m NeutralLevel{})])
| m == n -> equalLevel (Max [a]) (Max [b])
_ -> postpone
where
ok = return ()
notok = 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 <- reduce a
b <- reduce b
reportSLn "tc.conv.level" 50 $ "equalLevel (" ++ show a ++ ") (" ++ show b ++ ")"
liftTCM $ catchConstraint (LevelCmp CmpEq a b) $
check a b
where
check a@(Max as) b@(Max bs) = do
reportSDoc "tc.conv.level" 40 $
sep [ text "equalLevel"
, vcat [ nest 2 $ sep [ prettyTCM a <+> text "=="
, prettyTCM b
]
, nest 2 $ sep [ text (show (Max as)) <+> text "=="
, text (show (Max bs))
]
]
]
let a === b = do
lvl <- getLvl
equalAtom lvl a b
as =!= bs = levelTm (Max as) === levelTm (Max bs)
as <- return $ closed0 as
bs <- return $ closed0 bs
case (as, bs) of
_ | List.sort as == List.sort bs -> ok
| any isBlocked (as ++ bs) -> do
lvl <- getLvl
liftTCM $ useInjectivity 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 _)], [Plus m (MetaLevel y _)])
| n == m && x == y -> ok
([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 n (MetaLevel x bs)]) -> meta n x bs as
_ | any isMeta (as ++ bs) -> postpone
_ | all isNeutralOrClosed (as ++ bs) ->
if length as == length bs
then zipWithM_ (\a b -> [a] =!= [b]) as bs
else notok
_ -> postpone
where
ok = return ()
notok = typeError $ UnequalSorts (Type a) (Type b)
postpone = do
reportSLn "tc.conv.level" 30 $ "postponing: " ++ show a ++ " == " ++ show b
patternViolation
closed0 [] = [ClosedLevel 0]
closed0 as = as
getLvl = El (mkType 0) <$> primLevel
meta n x as bs = do
reportSLn "tc.meta.level" 50 $ "meta " ++ show as ++ " " ++ show bs
bs' <- mapM (subtr n) bs
assignV 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 = 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
isMeta (Plus _ MetaLevel{}) = True
isMeta _ = False
isThisMeta x (Plus _ (MetaLevel y _)) = x == y
isThisMeta _ _ = False
equalSort :: Sort -> Sort -> TCM ()
equalSort s1 s2 =
ifM typeInType (return ()) $
catchConstraint (SortCmp CmpEq s1 s2) $ do
(s1,s2) <- reduce (s1,s2)
reportSDoc "tc.conv.sort" 30 $
sep [ text "equalSort"
, vcat [ nest 2 $ fsep [ prettyTCM s1 <+> text "=="
, prettyTCM s2 ]
, nest 2 $ fsep [ text (show s1) <+> text "=="
, text (show s2) ]
]
]
case (s1, s2) of
(Type a , Type b ) -> equalLevel a b
(Prop , Prop ) -> return ()
(Type _ , Prop ) -> notEq s1 s2
(Prop , Type _ ) -> notEq s1 s2
(Inf , Inf ) -> return ()
(Inf , Type (Max as@(_:_))) -> mapM_ (isInf $ notEq s1 s2) as
(Type (Max as@(_:_)), Inf) -> mapM_ (isInf $ notEq s1 s2) as
(Inf , _ ) -> notEq s1 s2
(_ , Inf ) -> notEq s1 s2
(DLub s1 s2, s0@(Type (Max []))) -> do
equalSort s1 s0
underAbstraction_ s2 $ \s2 -> equalSort s2 s0
(s0@(Type (Max [])), DLub s1 s2) -> do
equalSort s0 s1
underAbstraction_ s2 $ \s2 -> equalSort s0 s2
(DLub{} , _ ) -> addConstraint (SortCmp CmpEq s1 s2)
(_ , DLub{} ) -> addConstraint (SortCmp CmpEq s1 s2)
where
notEq s1 s2 = typeError $ UnequalSorts s1 s2
isInf notok ClosedLevel{} = notok
isInf notok (Plus _ l) = case l of
MetaLevel x vs -> assignV x vs (Sort Inf)
NeutralLevel (Shared p) -> isInf notok (Plus 0 $ NeutralLevel $ derefPtr p)
NeutralLevel (Sort Inf) -> return ()
_ -> notok