module Agda.TypeChecking.Conversion where
import Control.Applicative
import Control.Monad
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.Literal
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
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.SizedTypes
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Level
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.UniversePolymorphism
import Agda.Utils.Monad
import Agda.TypeChecking.Monad.Debug
#include "../undefined.h"
import Agda.Utils.Impossible
nextPolarity [] = (Invariant, [])
nextPolarity (p : ps) = (p, ps)
sameVars :: Args -> Args -> Bool
sameVars xs ys = and $ zipWith same xs ys
where
same (Arg _ _ (Var n [])) (Arg _ _ (Var m [])) = n == m
same _ _ = False
equalTerm :: MonadTCM tcm => Type -> Term -> Term -> tcm Constraints
equalTerm = compareTerm CmpEq
equalAtom :: MonadTCM tcm => Type -> Term -> Term -> tcm Constraints
equalAtom = compareAtom CmpEq
equalArgs :: MonadTCM tcm => Type -> Args -> Args -> tcm Constraints
equalArgs = compareArgs []
equalType :: MonadTCM tcm => Type -> Type -> tcm Constraints
equalType = compareType CmpEq
compareTerm :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints
compareTerm cmp a m n =
verboseBracket "tc.conv.term" 5 "compareTerm" $
catchConstraint (ValueCmp cmp a m n) $ do
a' <- reduce a
reportSDoc "tc.conv.term" 10 $ fsep
[ text "compareTerm", prettyTCM m, prettyTCM cmp, prettyTCM n, text ":", prettyTCM a' ]
proofIrr <- proofIrrelevance
isSize <- isSizeType a'
s <- reduce $ getSort a'
mlvl <- mlevel
case s of
Prop | proofIrr -> return []
_ | isSize -> compareSizes cmp m n
_ -> case unEl a' of
a | Just a == mlvl -> equalLevel m n
Pi a _ -> equalFun (a,a') m n
Fun a _ -> equalFun (a,a') m n
MetaV x _ -> do
(m,n) <- normalise (m,n)
if m == n
then return []
else buildConstraint (ValueCmp cmp 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 || (isNeutral m && isNeutral n) ->
compareAtom cmp a' (ignoreBlocking m) (ignoreBlocking n)
_ -> do
(tel, m') <- etaExpandRecord r ps $ ignoreBlocking m
(_ , n') <- etaExpandRecord r ps $ ignoreBlocking n
compareArgs [] (telePi_ tel $ sort Prop) m' n'
else compareAtom cmp a' m n
_ -> compareAtom cmp a' m n
where
isNeutral (NotBlocked Con{}) = False
isNeutral _ = True
isMeta (NotBlocked MetaV{}) = True
isMeta _ = False
equalFun (a,t) m n = do
name <- freshName_ (suggest $ unEl t)
addCtx name a $ compareTerm cmp t' m' n'
where
p = fmap (const $ Var 0 []) a
(m',n') = raise 1 (m,n) `apply` [p]
t' = raise 1 t `piApply` [p]
suggest (Fun _ _) = "x"
suggest (Pi _ (Abs x _)) = x
suggest _ = __IMPOSSIBLE__
compareTel :: MonadTCM tcm => Comparison -> Telescope -> Telescope -> tcm Constraints
compareTel cmp tel1 tel2 =
verboseBracket "tc.conv.tel" 5 "compareTel" $
catchConstraint (TelCmp cmp tel1 tel2) $ case (tel1, tel2) of
(EmptyTel, EmptyTel) -> return []
(EmptyTel, _) -> bad
(_, EmptyTel) -> bad
(ExtendTel arg1@(Arg h1 r1 a1) tel1, ExtendTel arg2@(Arg h2 r2 a2) tel2)
| h1 /= h2 -> bad
| otherwise -> do
let (tel1', tel2') = raise 1 (tel1, tel2)
arg = Var 0 []
name <- freshName_ (suggest (absName tel1) (absName tel2))
cs <- compareType cmp a1 a2
let c = TelCmp cmp (absApp tel1' arg) (absApp tel2' arg)
let dependent = 0 `freeIn` absBody tel2
if dependent
then addCtx name arg1 $ guardConstraint (return cs) c
else do cs' <- addCtx name arg1 $ solveConstraint c
return $ cs ++ cs'
where
suggest "_" y = y
suggest x _ = x
where
bad = typeError $ UnequalTelescopes cmp tel1 tel2
compareAtom :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints
compareAtom cmp t m n =
verboseBracket "tc.conv.atom" 5 "compareAtom" $
catchConstraint (ValueCmp cmp t m n) $ do
mb <- traverse constructorForm =<< etaExpandBlocked =<< reduceB m
nb <- traverse constructorForm =<< etaExpandBlocked =<< reduceB n
let m = ignoreBlocking mb
n = ignoreBlocking nb
reportSDoc "tc.conv.atom" 10 $ fsep
[ text "compareAtom", prettyTCM mb, prettyTCM cmp, prettyTCM nb, text ":", prettyTCM t ]
case (mb, nb) of
(NotBlocked (MetaV x xArgs), NotBlocked (MetaV y yArgs))
| x == y -> if sameVars xArgs yArgs
then return []
else do
m <- normalise m
n <- normalise n
if m == n
then return []
else buildConstraint (ValueCmp cmp t m n)
| otherwise -> do
[p1, p2] <- mapM getMetaPriority [x,y]
let (solve1, solve2)
| (p1,x) > (p2,y) = (l,r)
| otherwise = (r,l)
where l = assignV t x xArgs n
r = assignV t y yArgs m
try m fallback = do
cs <- m
case cs of
[] -> return []
_ -> fallback cs
rollback <- return . put =<< get
try solve1 $ \cs -> do
undoRollback <- return . put =<< get
rollback
try solve2 $ \_ -> do
undoRollback
return cs
(NotBlocked (MetaV x xArgs), _) -> assignV t x xArgs n
(_, NotBlocked (MetaV x xArgs)) -> assignV t x xArgs m
(Blocked{}, Blocked{}) -> do
n <- normalise n
m <- normalise m
if m == n
then return []
else buildConstraint $ ValueCmp cmp t m n
(Blocked{}, _) -> useInjectivity cmp t m n
(_,Blocked{}) -> useInjectivity cmp t m n
_ -> case (m, n) of
_ | f1@(FunV _ _) <- funView m
, f2@(FunV _ _) <- funView n -> equalFun f1 f2
(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 iArgs jArgs
(Def x xArgs, Def y yArgs) | x == y -> do
pol <- getPolarity' cmp x
reportSDoc "tc.conv.atom" 20 $
text "compareArgs" <+> sep
[ sep [ prettyTCM xArgs
, prettyTCM yArgs
]
, nest 2 $ text (show pol)
]
a <- defType <$> getConstInfo x
compareArgs pol a xArgs yArgs
(Con x xArgs, Con y yArgs)
| x == y -> do
Def d args <- reduce $ unEl t
npars <- do
def <- theDef <$> getConstInfo d
case def of
Datatype{dataPars = npars} -> return npars
Record{recPars = npars} -> return npars
_ -> __IMPOSSIBLE__
a <- defType <$> getConstInfo x
let a' = piApply a (genericTake npars args)
compareArgs [] a' xArgs yArgs
_ -> typeError $ UnequalTerms cmp m n t
where
equalFun (FunV arg1@(Arg h1 r1 a1) t1) (FunV (Arg h2 r2 a2) t2)
| h1 /= h2 = typeError $ UnequalHiding ty1 ty2
| ignoreForced r1 /= ignoreForced r2 = typeError $ UnequalRelevance ty1 ty2
| otherwise = do
let (ty1',ty2') = raise 1 (ty1,ty2)
arg = Arg h1 r1 (Var 0 [])
name <- freshName_ (suggest t1 t2)
cs <- compareType cmp a2 a1
let c = TypeCmp cmp (piApply ty1' [arg]) (piApply ty2' [arg])
let dependent = case t2 of
Pi _ _ -> True
Fun _ _ -> False
_ -> __IMPOSSIBLE__
if dependent
then addCtx name arg1 $ guardConstraint (return cs) c
else do
cs' <- addCtx name arg1 $ solveConstraint c
return $ cs ++ cs'
where
ty1 = El (getSort a1) t1
ty2 = El (getSort a2) t2
suggest t1 t2 = case concatMap name [t1,t2] of
[] -> "_"
x:_ -> x
where
name (Pi _ (Abs x _)) = [x]
name (Fun _ _) = []
name _ = __IMPOSSIBLE__
equalFun _ _ = __IMPOSSIBLE__
compareArgs :: MonadTCM tcm => [Polarity] -> Type -> Args -> Args -> tcm Constraints
compareArgs _ _ [] [] = return []
compareArgs _ _ [] (_:_) = __IMPOSSIBLE__
compareArgs _ _ (_:_) [] = __IMPOSSIBLE__
compareArgs pols0 a (arg1 : args1) (arg2 : args2) =
verboseBracket "tc.conv.args" 5 "compareArgs" $ do
let (pol, pols) = nextPolarity pols0
a <- reduce a
catchConstraint (ArgsCmp pols0 a (arg1 : args1) (arg2 : args2)) $ do
reportSDoc "tc.conv.args" 30 $
sep [ text "compareArgs"
, nest 2 $ sep [ prettyTCM (arg1 : args1)
, prettyTCM (arg2 : args2)
]
, nest 2 $ text ":" <+> prettyTCM a
]
case funView (unEl a) of
FunV (Arg _ r b) _ -> do
reportSDoc "tc.conv.args" 10 $
sep [ text "compareArgs" <+> parens (text $ show pol ++ " " ++ show r)
, nest 2 $ sep [ prettyTCM arg1
, text "~~" <+> prettyTCM arg2
, text ":" <+> prettyTCM b
]
]
let cmp x y = case pol of
Invariant -> compareTerm CmpEq b x y
Covariant -> compareTerm CmpLeq b x y
Contravariant -> compareTerm CmpLeq b y x
cs1 <- case r of
Forced -> return []
Irrelevant -> return []
Relevant -> cmp (unArg arg1) (unArg arg2)
case (cs1, unEl a) of
(_:_, Pi (Arg _ _ (El _ lvl')) c) | 0 `freeInIgnoringSorts` absBody c
-> do
reportSDoc "tc.conv.args" 15 $ sep
[ text "aborting compareArgs" <+> parens (text $ show pol)
, nest 2 $ fsep
[ prettyTCM arg1
, text "~~" <+> prettyTCM arg2
, text ":" <+> prettyTCM b
, text "--->" <+> prettyTCM cs1
]
]
patternViolation
_ -> do
reportSDoc "tc.conv.args" 15 $ sep
[ text "compareArgs" <+> parens (text $ show pol)
, nest 2 $ sep
[ prettyTCM args1
, text "~~" <+> prettyTCM args2
, text ":" <+> prettyTCM (piApply a [arg1])
]
]
cs2 <- compareArgs pols (piApply a [arg1]) args1 args2
return $ cs1 ++ cs2
_ -> patternViolation
compareType :: MonadTCM tcm => Comparison -> Type -> Type -> tcm Constraints
compareType cmp ty1@(El s1 a1) ty2@(El s2 a2) =
verboseBracket "tc.conv.type" 5 "compareType" $
catchConstraint (TypeCmp cmp ty1 ty2) $ do
reportSDoc "tc.conv.type" 9 $ vcat
[ hsep [ text "compareType", prettyTCM ty1, prettyTCM cmp, prettyTCM ty2 ]
, hsep [ text " sorts:", prettyTCM s1, text " and ", prettyTCM s2 ]
]
cs1 <- compareSort CmpEq s1 s2 `catchError` \err -> case errError err of
TypeError _ _ -> do
reportSDoc "tc.conv.type" 10 $ vcat
[ text "sort comparison failed"
, nest 2 $ vcat
[ text "s1 =" <+> prettyTCM s1
, text "s2 =" <+> prettyTCM s2
]
]
compareTerm cmp (sort s1) a1 a2
throwError err
_ -> throwError err
cs2 <- compareTerm cmp (sort s1) a1 a2
cs <- solveConstraints $ cs1 ++ cs2
unless (null cs) $
reportSDoc "tc.conv.type" 9 $
text " --> " <+> prettyTCM cs
return cs
leqType :: MonadTCM tcm => Type -> Type -> tcm Constraints
leqType = compareType CmpLeq
compareSort :: MonadTCM tcm => Comparison -> Sort -> Sort -> tcm Constraints
compareSort CmpEq = equalSort
compareSort CmpLeq = leqSort
leqSort :: MonadTCM tcm => Sort -> Sort -> tcm Constraints
leqSort s1 s2 =
ifM typeInType (return []) $
catchConstraint (SortCmp CmpLeq s1 s2) $
do (s1,s2) <- reduce (s1,s2)
reportSDoc "tc.conv.sort" 10 $
sep [ text "leqSort"
, nest 2 $ fsep [ prettyTCM s1 <+> text "=<"
, prettyTCM s2 ]
]
case (s1,s2) of
(Type (Lit (LitLevel _ n)), Type (Lit (LitLevel _ m)))
| n <= m -> return []
| otherwise -> notLeq s1 s2
(Type a, Type b) -> leqLevel a b
(Prop , Prop ) -> return []
(Type _ , Prop ) -> notLeq s1 s2
(Suc _ , Prop ) -> notLeq s1 s2
(Prop , Type _ ) -> return []
(Suc s , Type (Lit (LitLevel _ n)))
| 1 <= n -> leqSort s (mkType $ n 1)
(Suc s , Type b ) -> notLeq s1 s2
(Suc s1 , Suc s2 ) -> leqSort s1 s2
(_ , Suc _ ) -> equalSort s1 s2
(Lub a b , _ ) -> liftM2 (++) (leqSort a s2) (leqSort b s2)
(_ , Lub _ _ ) -> equalSort s1 s2
(MetaS{} , _ ) -> equalSort s1 s2
(_ , MetaS{} ) -> equalSort s1 s2
(Inf , Inf ) -> return []
(Inf , _ ) -> notLeq s1 s2
(_ , Inf ) -> return []
(DLub{} , _ ) -> equalSort s1 s2
(_ , DLub{} ) -> equalSort s1 s2
where
notLeq s1 s2 = typeError $ NotLeqSort s1 s2
leqLevel :: MonadTCM tcm => Term -> Term -> tcm Constraints
leqLevel a b = liftTCM $ do
reportSDoc "tc.conv.nat" 10 $
text "compareLevel" <+>
sep [ prettyTCM a <+> text "=<"
, prettyTCM b ]
n <- levelView a
m <- levelView b
leqView n m
where
leqView n@(Max as) m@(Max bs) = do
reportSDoc "tc.conv.nat" 10 $
text "compareLevelView" <+>
sep [ text (show n) <+> text "=<"
, text (show m) ]
case (as, bs) of
(_, []) -> concat <$> sequence [ leqPlusView a (ClosedLevel 0) | a <- as ]
(_, [b]) -> concat <$> sequence [ leqPlusView a b | a <- as ]
_ -> do
sequence [ choice [ leqPlusView a b | b <- bs ] | a <- as ]
return []
leqPlusView n m = do
reportSDoc "tc.conv.nat" 10 $
text "comparePlusView" <+>
sep [ text (show n) <+> text "=<"
, text (show m) ]
case (n, m) of
(ClosedLevel n, ClosedLevel m)
| n <= m -> ok
(Plus n (NeutralLevel a), Plus m (NeutralLevel b))
| n <= m -> do
lvl <- primLevel
equalTerm (El (mkType 0) lvl) a b
(ClosedLevel n, Plus m _)
| n <= m -> ok
(Plus _ BlockedLevel{}, _) -> postpone
(_, Plus _ BlockedLevel{}) -> postpone
(Plus _ MetaLevel{}, _) -> postpone
(_, Plus _ MetaLevel{}) -> postpone
_ -> notok
ok = return []
notok = typeError $ NotLeqSort (Type a) (Type b)
postpone = patternViolation
choice [] = patternViolation
choice (m:ms) = noConstraints m `catchError` \_ -> choice ms
equalLevel :: MonadTCM tcm => Term -> Term -> tcm Constraints
equalLevel a b = do
lvl <- primLevel
Max as <- levelView a
Max bs <- levelView b
a <- unLevelView (Max as)
b <- unLevelView (Max bs)
liftTCM $ catchConstraint (ValueCmp CmpEq (El (mkType 0) lvl) a b)
$ check a b as bs
where
check a b as bs = do
reportSDoc "tc.conv.nat" 20 $
sep [ text "equalLevel"
, 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 = do a <- unLevelView (Max as)
b <- unLevelView (Max bs)
a === b
case (as, bs) of
_ | List.sort as == List.sort bs -> ok
| any isBlocked (as ++ bs) -> do
lvl <- getLvl
liftTCM $ useInjectivity CmpEq lvl a b
([], _) -> wrap $ concat <$> sequence [ as =!= [b] | b <- bs ]
(_, []) -> wrap $ concat <$> sequence [ [a] =!= bs | a <- as ]
([ClosedLevel n], [ClosedLevel m])
| n == m -> ok
| otherwise -> notok
([ClosedLevel{}], _) | any isNeutral bs -> notok
(_, [ClosedLevel{}]) | any isNeutral as -> notok
([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) -> as =!= bs
_ -> postpone
where
ok = return []
notok = typeError $ UnequalSorts (Type a) (Type b)
postpone = patternViolation
getLvl = El (mkType 0) <$> primLevel
meta n x as bs = do
bs' <- mapM (subtr n) bs
lvl <- getLvl
assignV lvl x as =<< unLevelView (Max bs')
wrap m = m `catchError` \err ->
case errError 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
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 :: MonadTCM tcm => Sort -> Sort -> tcm Constraints
equalSort s1 s2 =
ifM typeInType (return []) $
catchConstraint (SortCmp CmpEq s1 s2) $ do
(s1,s2) <- reduce (s1,s2)
reportSDoc "tc.conv.sort" 10 $
sep [ text "equalSort"
, nest 2 $ fsep [ prettyTCM s1 <+> text "=="
, prettyTCM s2 ]
]
case (s1,s2) of
(Type (Lit n), Type (Lit m))
| n == m -> return []
| otherwise -> notEq s1 s2
(Type a , Type b ) -> equalLevel a b
(MetaS x us , MetaS y vs) -> do
s1 <- normalise s1
s2 <- normalise s2
if s1 == s2 then return []
else do
[p1, p2] <- mapM getMetaPriority [x, y]
if p1 >= p2 then assignS x us s2
else assignS y vs s1
(MetaS x vs, _ ) -> assignS x vs s2
(_ , MetaS{} ) -> equalSort s2 s1
(Prop , Prop ) -> return []
(Type _ , Prop ) -> notEq s1 s2
(Prop , Type _ ) -> notEq s1 s2
(Suc s , Prop ) -> notEq s1 s2
(Suc s , Type (Lit (LitLevel _ 0))) -> notEq s1 s2
(Suc s , Type (Lit (LitLevel _ 1))) -> buildConstraint (SortCmp CmpEq s1 s2)
(Suc s , Type (Lit (LitLevel _ n))) -> equalSort s (mkType $ n 1)
(Prop , Suc s ) -> notEq s1 s2
(Type (Lit (LitLevel _ 0)) , Suc s ) -> notEq s1 s2
(Type (Lit (LitLevel _ 1)) , Suc s ) -> buildConstraint (SortCmp CmpEq s1 s2)
(Type (Lit (LitLevel _ n)) , Suc s ) -> equalSort (mkType $ n 1) s
(Suc s1 , Suc s2 ) -> equalSort s1 s2
(_ , Suc _ ) -> buildConstraint (SortCmp CmpEq s1 s2)
(Suc _ , _ ) -> buildConstraint (SortCmp CmpEq s1 s2)
(Inf , Inf ) -> return []
(Inf , _ ) -> notEq s1 s2
(_ , Inf ) -> notEq s1 s2
(s0@(Type (Lit (LitLevel _ 0))), Lub s1 s2) -> do
cs1 <- equalSort s0 s1
cs2 <- equalSort s0 s2
return $ cs1 ++ cs2
(Lub s1 s2, s0@(Type (Lit (LitLevel _ 0)))) -> do
cs1 <- equalSort s1 s0
cs2 <- equalSort s2 s0
return $ cs1 ++ cs2
(Lub{} , Lub{} ) -> do
(s1, s2) <- normalise (s1, s2)
if s1 == s2
then return []
else buildConstraint (SortCmp CmpEq s1 s2)
(Lub _ _ , _ ) -> buildConstraint (SortCmp CmpEq s1 s2)
(_ , Lub _ _ ) -> buildConstraint (SortCmp CmpEq s1 s2)
(DLub s1 s2, s0@(Type (Lit (LitLevel _ 0)))) -> do
cs1 <- equalSort s1 s0
cs2 <- underAbstraction_ s2 $ \s2 -> equalSort s2 s0
return $ cs1 ++ cs2
(s0@(Type (Lit (LitLevel _ 0))), DLub s1 s2) -> do
cs1 <- equalSort s0 s1
cs2 <- underAbstraction_ s2 $ \s2 -> equalSort s0 s2
return $ cs1 ++ cs2
(DLub{} , _ ) -> buildConstraint (SortCmp CmpEq s1 s2)
(_ , DLub{} ) -> buildConstraint (SortCmp CmpEq s1 s2)
where
notEq s1 s2 = typeError $ UnequalSorts s1 s2