{-# 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