{-# LANGUAGE CPP, PatternGuards #-} module Agda.TypeChecking.Conversion where import Control.Applicative import Control.Monad import Control.Monad.State import Control.Monad.Error import Data.Generics import Data.Traversable hiding (mapM) import Data.List hiding (sort) 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.Utils.Monad import Agda.TypeChecking.Monad.Debug #include "../undefined.h" import Agda.Utils.Impossible nextPolarity [] = (Invariant, []) nextPolarity (p : ps) = (p, ps) -- | Check if to lists of arguments are the same (and all variables). -- Precondition: the lists have the same length. 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 -- | Type directed equality on values. -- compareTerm :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints compareTerm cmp a m n = 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' case s of Prop | proofIrr -> return [] _ | isSize -> compareSizes cmp m n _ -> case unEl a' of 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 <- isRecord r if isrec then do m <- reduceB m n <- reduceB n case (m, n) of _ | 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 -- No subtyping on record terms compareArgs [] (telePi_ tel $ sort Prop) m' n' else compareAtom cmp a' m n _ -> compareAtom cmp a' m n where isNeutral Blocked{} = False isNeutral (NotBlocked Con{}) = False isNeutral _ = True 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 = catchConstraint (TelCmp cmp tel1 tel2) $ case (tel1, tel2) of (EmptyTel, EmptyTel) -> return [] (EmptyTel, _) -> bad (_, EmptyTel) -> bad (ExtendTel arg1@(Arg h1 a1) tel1, ExtendTel arg2@(Arg h2 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 -- | Syntax directed equality on atomic values -- compareAtom :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints compareAtom cmp t m n = catchConstraint (ValueCmp cmp t m n) $ do mb <- traverse constructorForm =<< reduceB m nb <- traverse constructorForm =<< 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 -- Check syntactic equality on meta-variables -- (same as for blocked terms) 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] -- instantiate later meta variables first 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 -- First try the one with the highest priority. If that doesn't -- work, try the low priority one. If that doesn't work either, -- go with the first version. 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 -- is this what we want? m <- normalise m if m == n then return [] -- Check syntactic equality for blocked terms 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 cmp s1 s2 (Lit l1, Lit l2) | l1 == l2 -> return [] (Var i iArgs, Var j jArgs) | i == j -> do a <- typeOfBV i -- Variables are invariant in their arguments 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 -- The type is a datatype. Def d args <- reduce $ unEl t -- Get the number of parameters to the datatype Datatype{dataPars = npars} <- theDef <$> getConstInfo d -- The type to compare the arguments at is obtained by -- instantiating the parameters. a <- defType <$> getConstInfo x let a' = piApply a (genericTake npars args) -- Constructors are invariant in their arguments -- (could be covariant). compareArgs [] a' xArgs yArgs _ -> typeError $ UnequalTerms cmp m n t where equalFun (FunV arg1@(Arg h1 a1) t1) (FunV (Arg h2 a2) t2) | h1 /= h2 = typeError $ UnequalHiding ty1 ty2 | otherwise = do let (ty1',ty2') = raise 1 (ty1,ty2) arg = Arg h1 (Var 0 []) name <- freshName_ (suggest t1 t2) cs <- compareType cmp a2 a1 let c = TypeCmp cmp (piApply ty1' [arg]) (piApply ty2' [arg]) -- We only need to require a1 == a2 if t2 is a dependent function type. -- If it's non-dependent it doesn't matter what we add to the context. 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 -- TODO: wrong (but it doesn't matter) 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__ -- | Type-directed equality on argument lists -- compareArgs :: MonadTCM tcm => [Polarity] -> Type -> Args -> Args -> tcm Constraints compareArgs _ _ [] [] = return [] compareArgs _ _ [] (_:_) = __IMPOSSIBLE__ compareArgs _ _ (_:_) [] = __IMPOSSIBLE__ compareArgs pols0 a (arg1 : args1) (arg2 : args2) = do let (pol, pols) = nextPolarity pols0 a <- reduce a case funView (unEl a) of FunV (Arg _ b) _ -> do reportSDoc "tc.conv.args" 10 $ sep [ text "compareArgs" <+> parens (text $ show pol) , 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 <- cmp (unArg arg1) (unArg arg2) case (cs1, unEl a) of (_:_, Pi _ c) | 0 `freeIn` absBody c -> do reportSDoc "tc.conv.args" 15 $ sep [ text "aborting compareArgs" <+> parens (text $ show pol) , nest 2 $ sep [ parens $ text (show pol) , prettyTCM arg1 , text "~~" <+> prettyTCM arg2 , text ":" <+> prettyTCM b , text "-->" <+> prettyTCM cs1 ] ] patternViolation -- TODO: will duplicate work (all arguments checked so far) _ -> do reportSDoc "tc.conv.args" 15 $ sep [ text "compareArgs" <+> parens (text $ show pol) , nest 2 $ sep [ prettyTCM arg1 , text "~~" <+> prettyTCM arg2 , text ":" <+> prettyTCM (piApply a [arg1]) ] ] cs2 <- compareArgs pols (piApply a [arg1]) args1 args2 return $ cs1 ++ cs2 _ -> patternViolation -- | Equality on Types compareType :: MonadTCM tcm => Comparison -> Type -> Type -> tcm Constraints compareType cmp ty1@(El s1 a1) ty2@(El s2 a2) = 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 cmp s1 s2 `catchError` \err -> case err of TypeError _ _ -> typeError $ UnequalTypes cmp ty1 ty2 _ -> throwError err cs2 <- compareTerm cmp (sort s1) a1 a2 unless (null $ cs1 ++ cs2) $ reportSDoc "tc.conv.type" 9 $ text " --> " <+> prettyTCM (cs1 ++ cs2) return $ cs1 ++ cs2 leqType :: MonadTCM tcm => Type -> Type -> tcm Constraints leqType = compareType CmpLeq --------------------------------------------------------------------------- -- * Sorts --------------------------------------------------------------------------- compareSort :: MonadTCM tcm => Comparison -> Sort -> Sort -> tcm Constraints compareSort CmpEq = equalSort compareSort CmpLeq = equalSort -- TODO: change to leqSort when we have better constraint solving -- | Check that the first sort is less or equal to the second. leqSort :: MonadTCM tcm => Sort -> Sort -> tcm Constraints leqSort s1 s2 = ifM typeInType (return []) $ catchConstraint (SortCmp CmpLeq s1 s2) $ do (s1,s2) <- reduce (s1,s2) -- do d1 <- prettyTCM s1 -- d2 <- prettyTCM s2 -- debug $ "leqSort " ++ show d1 ++ " <= " ++ show d2 case (s1,s2) of (Prop , Prop ) -> return [] (Type _ , Prop ) -> notLeq s1 s2 (Suc _ , Prop ) -> notLeq s1 s2 (Prop , Type _ ) -> return [] (Type n , Type m ) | n <= m -> return [] | otherwise -> notLeq s1 s2 (Suc s , Type n ) | 1 <= n -> leqSort s (Type $ n - 1) | otherwise -> notLeq s1 s2 (_ , Suc _ ) -> equalSort s1 s2 (Lub a b , _ ) -> liftM2 (++) (leqSort a s2) (leqSort b s2) (_ , Lub _ _ ) -> equalSort s1 s2 (MetaS x , MetaS y ) | x == y -> return [] (MetaS x , _ ) -> equalSort s1 s2 (_ , MetaS x ) -> equalSort s1 s2 where notLeq s1 s2 = typeError $ NotLeqSort s1 s2 -- | Check that the first sort equal to the second. equalSort :: MonadTCM tcm => Sort -> Sort -> tcm Constraints equalSort s1 s2 = ifM typeInType (return []) $ catchConstraint (SortCmp CmpEq s1 s2) $ do (s1,s2) <- reduce (s1,s2) -- do d1 <- prettyTCM s1 -- d2 <- prettyTCM s2 -- debug $ "equalSort " ++ show d1 ++ " == " ++ show d2 case (s1,s2) of (MetaS x , MetaS y ) | x == y -> return [] | otherwise -> do [p1, p2] <- mapM getMetaPriority [x, y] if p1 >= p2 then assignS x s2 else assignS y s1 (MetaS x , _ ) -> assignS x s2 (_ , MetaS x ) -> equalSort s2 s1 (Prop , Prop ) -> return [] (Type _ , Prop ) -> notEq s1 s2 (Prop , Type _ ) -> notEq s1 s2 (Type n , Type m ) | n == m -> return [] | otherwise -> notEq s1 s2 (Suc s , Prop ) -> notEq s1 s2 (Suc s , Type 0 ) -> notEq s1 s2 (Suc s , Type 1 ) -> buildConstraint (SortCmp CmpEq s1 s2) (Suc s , Type n ) -> equalSort s (Type $ n - 1) (Prop , Suc s ) -> notEq s1 s2 (Type 0 , Suc s ) -> notEq s1 s2 (Type 1 , Suc s ) -> buildConstraint (SortCmp CmpEq s1 s2) (Type n , Suc s ) -> equalSort (Type $ n - 1) s (_ , Suc _ ) -> buildConstraint (SortCmp CmpEq s1 s2) (Suc _ , _ ) -> buildConstraint (SortCmp CmpEq s1 s2) (Lub _ _ , _ ) -> buildConstraint (SortCmp CmpEq s1 s2) (_ , Lub _ _ ) -> buildConstraint (SortCmp CmpEq s1 s2) where notEq s1 s2 = typeError $ UnequalSorts s1 s2