{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.SizedTypes where

import Prelude hiding (null)

import Control.Monad
import Control.Monad.Except ( MonadError(..) )
import Control.Monad.Writer ( MonadWriter(..), WriterT(..), runWriterT )

import qualified Data.Foldable as Fold
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Set (Set)

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Constraint
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (MonadCheckInternal, infer)
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.Constraints

import Agda.Utils.Functor
import Agda.Utils.List as List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (Pretty, prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple

import qualified Agda.Utils.Pretty as P
import qualified Agda.Utils.Warshall as W

import Agda.Utils.Impossible

------------------------------------------------------------------------
-- * SIZELT stuff
------------------------------------------------------------------------

-- | Check whether a type is either not a SIZELT or a SIZELT that is non-empty.
checkSizeLtSat :: Term -> TCM ()
checkSizeLtSat t = whenM haveSizeLt $ do
  reportSDoc "tc.size" 10 $ do
    tel <- getContextTelescope
    sep
      [ "checking that " <+> prettyTCM t <+> " is not an empty type of sizes"
      , if null tel then empty else do
        "in context " <+> inTopContext (prettyTCM tel)
      ]
  reportSLn "tc.size" 60 $ "- raw type = " ++ show t
  let postpone :: Blocker -> Term -> TCM ()
      postpone b t = do
        reportSDoc "tc.size.lt" 20 $ sep
          [ "- postponing `not empty type of sizes' check for " <+> prettyTCM t ]
        addConstraint b $ CheckSizeLtSat t
  let ok :: TCM ()
      ok = reportSLn "tc.size.lt" 20 $ "- succeeded: not an empty type of sizes"
  ifBlocked t postpone $ \ _ t -> do
    reportSLn "tc.size.lt" 20 $ "- type is not blocked"
    caseMaybeM (isSizeType t) ok $ \ b -> do
      reportSLn "tc.size.lt" 20 $ " - type is a size type"
      case b of
        BoundedNo -> ok
        BoundedLt b -> do
          reportSDoc "tc.size.lt" 20 $ " - type is SIZELT" <+> prettyTCM b
          ifBlocked b (\ x _ -> postpone x t) $ \ _ b -> do
            reportSLn "tc.size.lt" 20 $ " - size bound is not blocked"
            catchConstraint (CheckSizeLtSat t) $ do
              unlessM (checkSizeNeverZero b) $ do
                typeError . GenericDocError =<< do
                  "Possibly empty type of sizes " <+> prettyTCM t

-- | Precondition: Term is reduced and not blocked.
--   Throws a 'patternViolation' if undecided
checkSizeNeverZero :: Term -> TCM Bool
checkSizeNeverZero u = do
  v <- sizeView u
  case v of
    SizeInf     -> return True  -- OK, infty is never 0.
    SizeSuc{}   -> return True  -- OK, a + 1 is never 0.
    OtherSize u ->
      case u of
        Var i [] -> checkSizeVarNeverZero i
        -- neutral sizes cannot be guaranteed > 0
        _ -> return False

-- -- | A size variable is never zero if it is the strict upper bound of
-- --   some other size variable in context.
-- --   Eg. @i : Size, j : Size< i@ |- i is never zero.
-- --   Throws a 'patternViolation' if undecided.
-- checkSizeVarNeverZero :: Int -> TCM Bool
-- checkSizeVarNeverZero i = do
--   -- Looking for a variable j : Size< i, we can restrict to the last i
--   -- entries, as this variable necessarily has been defined later than i.
--   doms <- take i <$> getContext
--   -- We raise each type to make sense in the current context.
--   let ts = zipWith raise [1..] $ map (snd . unDom) doms
--   reportSDoc "tc.size" 15 $ sep
--     [ "checking that size " <+> prettyTCM (var i) <+> " is never 0"
--     , "in context " <+> do sep $ map prettyTCM ts
--     ]
--   foldr f (return False) ts
--   where
--   f t cont = do
--     -- If we encounter a blocked type in the context, we cannot
--     -- definitely say no.
--     let yes     = return True
--         no      = cont
--         perhaps = cont >>= \ res -> if res then return res else patternViolation
--     ifBlocked t (\ _ _ -> perhaps) $ \ t -> do
--       caseMaybeM (isSizeType t) no $ \ b -> do
--         case b of
--           BoundedNo -> no
--           BoundedLt u -> ifBlocked u (\ _ _ -> perhaps) $ \ u -> do
--             case u of
--                Var i' [] | i == i' -> yes
--                _ -> no


-- | Checks that a size variable is ensured to be @> 0@.
--   E.g. variable @i@ cannot be zero in context
--   @(i : Size) (j : Size< ↑ ↑ i) (k : Size< j) (k' : Size< k)@.
--   Throws a 'patternViolation' if undecided.
checkSizeVarNeverZero :: Int -> TCM Bool
checkSizeVarNeverZero i = do
  reportSDoc "tc.size" 20 $ "checkSizeVarNeverZero" <+> prettyTCM (var i)
  -- Looking for the minimal value for size variable i,
  -- we can restrict to the last i
  -- entries, as only these can contain i in an upper bound.
  ts <- map (snd . unDom) . take i <$> getContext
  -- If we encountered a blocking meta in the context, we cannot
  -- say ``no'' for sure.
  (n, blockers) <- runWriterT $ minSizeValAux ts $ repeat 0
  let blocker = unblockOnAll blockers
  if n > 0 then return True else
    if blocker == alwaysUnblock
      then return False
      else patternViolation blocker
  where
  -- Compute the least valuation for size context ts above the
  -- given valuation and return its last value.
  minSizeValAux :: [Type] -> [Int] -> WriterT (Set Blocker) TCM Int
  minSizeValAux _        []      = __IMPOSSIBLE__
  minSizeValAux []       (n : _) = return n
  minSizeValAux (t : ts) (n : ns) = do
    reportSDoc "tc.size" 60 $
       text ("minSizeVal (n:ns) = " ++ show (take (length ts + 2) $ n:ns) ++
             " t =") <+> (text . show) t  -- prettyTCM t  -- Wrong context!
    -- n is the min. value for variable 0 which has type t.
    let cont = minSizeValAux ts ns
        perhaps x = tell (Set.singleton x) >> cont
    -- If we encounter a blocked type in the context, we cannot
    -- give a definite answer.
    ifBlocked t (\ x _ -> perhaps x) $ \ _ t -> do
      caseMaybeM (liftTCM $ isSizeType t) cont $ \ b -> do
        case b of
          BoundedNo -> cont
          BoundedLt u -> ifBlocked u (\ x _ -> perhaps x) $ \ _ u -> do
            reportSLn "tc.size" 60 $ "minSizeVal upper bound u = " ++ show u
            v <- liftTCM $ deepSizeView u
            case v of
              -- Variable 0 has bound @(< j + m)@
              -- meaning that @minval(j) > n - m@, i.e., @minval(j) >= n+1-m@.
              -- Thus, we update the min value for @j@ with function @(max (n+1-m))@.
              DSizeVar (ProjectedVar j []) m -> do
                reportSLn "tc.size" 60 $ "minSizeVal upper bound v = " ++ show v
                let ns' = List.updateAt j (max $ n+1-m) ns
                reportSLn "tc.size" 60 $ "minSizeVal ns' = " ++ show (take (length ts + 1) ns')
                minSizeValAux ts ns'
              DSizeMeta x _ _ -> perhaps (unblockOnMeta x)
              _ -> cont

-- | Check whether a variable in the context is bounded by a size expression.
--   If @x : Size< a@, then @a@ is returned.
isBounded :: PureTCM m => Nat -> m BoundedSize
isBounded i = isBoundedSizeType =<< typeOfBV i

isBoundedProjVar
  :: (MonadCheckInternal m, PureTCM m)
  => ProjectedVar -> m BoundedSize
isBoundedProjVar pv = isBoundedSizeType =<< infer (unviewProjectedVar pv)

isBoundedSizeType :: PureTCM m => Type -> m BoundedSize
isBoundedSizeType t =
  reduce (unEl t) >>= \case
    Def x [Apply u] -> do
      sizelt <- getBuiltin' builtinSizeLt
      return $ if (Just (Def x []) == sizelt) then BoundedLt $ unArg u else BoundedNo
    _ -> return BoundedNo

-- | Whenever we create a bounded size meta, add a constraint
--   expressing the bound. First argument is the new meta and must be a @MetaV{}@.
--   In @boundedSizeMetaHook v tel a@, @tel@ includes the current context.
boundedSizeMetaHook
  :: ( MonadConstraint m
     , MonadTCEnv m
     , ReadTCState m
     , MonadAddContext m
     , HasOptions m
     , HasBuiltins m
     )
  => Term -> Telescope -> Type -> m ()
boundedSizeMetaHook v@(MetaV x _) tel0 a = do
  res <- isSizeType a
  case res of
    Just (BoundedLt u) -> do
      n <- getContextSize
      let tel | n > 0     = telFromList $ drop n $ telToList tel0
              | otherwise = tel0
      addContext tel $ do
        v <- sizeSuc 1 $ raise (size tel) v `apply` teleArgs tel
        -- compareSizes CmpLeq v u
        addConstraint (unblockOnMeta x) $ ValueCmp CmpLeq AsSizes v u
    _ -> return ()
boundedSizeMetaHook _ _ _ = __IMPOSSIBLE__

-- | @trySizeUniv cmp t m n x els1 y els2@
--   is called as a last resort when conversion checking @m `cmp` n : t@
--   failed for definitions @m = x els1@ and @n = y els2@,
--   where the heads @x@ and @y@ are not equal.
--
--   @trySizeUniv@ accounts for subtyping between SIZELT and SIZE,
--   like @Size< i =< Size@.
--
--   If it does not succeed it reports failure of conversion check.
trySizeUniv
  :: MonadConversion m
  => Comparison -> CompareAs -> Term -> Term
  -> QName -> Elims -> QName -> Elims -> m ()
trySizeUniv cmp t m n x els1 y els2 = do
  let failure :: forall m a. MonadTCError m => m a
      failure = typeError $ UnequalTerms cmp m n t
      forceInfty u = compareSizes CmpEq (unArg u) =<< primSizeInf
  -- Get the SIZE built-ins.
  (size, sizelt) <- flip catchError (const failure) $ do
     Def size   _ <- primSize
     Def sizelt _ <- primSizeLt
     return (size, sizelt)
  case (cmp, els1, els2) of
     -- Case @Size< _ <= Size@: true.
     (CmpLeq, [_], [])  | x == sizelt && y == size -> return ()
     -- Case @Size< u = Size@: forces @u = ∞@.
     (_, [Apply u], []) | x == sizelt && y == size -> forceInfty u
     (_, [], [Apply u]) | x == size && y == sizelt -> forceInfty u
     -- This covers all cases for SIZE and SIZELT.
     -- The remaining case is for @x@ and @y@ which are not size built-ins.
     _                                             -> failure

------------------------------------------------------------------------
-- * Size views that 'reduce'.
------------------------------------------------------------------------

-- | Compute the deep size view of a term.
--   Precondition: sized types are enabled.
deepSizeView :: (PureTCM m, MonadTCError m) => Term -> m DeepSizeView
deepSizeView v = do
  Def inf [] <- primSizeInf
  Def suc [] <- primSizeSuc
  let loop v =
        reduce v >>= \case
          Def x []        | x == inf -> return $ DSizeInf
          Def x [Apply u] | x == suc -> sizeViewSuc_ suc <$> loop (unArg u)

          Var i es | Just pv <- ProjectedVar i <$> mapM isProjElim es
                                     -> return $ DSizeVar pv 0
          MetaV x us                 -> return $ DSizeMeta x us 0
          v                          -> return $ DOtherSize v
  loop v

sizeMaxView :: PureTCM m => Term -> m SizeMaxView
sizeMaxView v = do
  inf <- getBuiltinDefName builtinSizeInf
  suc <- getBuiltinDefName builtinSizeSuc
  max <- getBuiltinDefName builtinSizeMax
  let loop v = do
        v <- reduce v
        case v of
          Def x []                   | Just x == inf -> return $ singleton $ DSizeInf
          Def x [Apply u]            | Just x == suc -> maxViewSuc_ (fromJust suc) <$> loop (unArg u)
          Def x [Apply u1, Apply u2] | Just x == max -> maxViewMax <$> loop (unArg u1) <*> loop (unArg u2)
          Var i es | Just pv <- ProjectedVar i <$> mapM isProjElim es
                                        -> return $ singleton $ DSizeVar pv 0
          MetaV x us                    -> return $ singleton $ DSizeMeta x us 0
          _                             -> return $ singleton $ DOtherSize v
  loop v

------------------------------------------------------------------------
-- * Size comparison that might add constraints.
------------------------------------------------------------------------

-- | Compare two sizes.
compareSizes :: (MonadConversion m) => Comparison -> Term -> Term -> m ()
compareSizes cmp u v = verboseBracket "tc.conv.size" 10 "compareSizes" $ do
  reportSDoc "tc.conv.size" 10 $ vcat
    [ "Comparing sizes"
    , nest 2 $ sep [ prettyTCM u <+> prettyTCM cmp
                   , prettyTCM v
                   ]
    ]
  verboseS "tc.conv.size" 60 $ do
    u <- reduce u
    v <- reduce v
    reportSDoc "tc.conv.size" 60 $
      nest 2 $ sep [ pretty u <+> prettyTCM cmp
                   , pretty v
                   ]
  us <- sizeMaxView u
  vs <- sizeMaxView v
  compareMaxViews cmp us vs

-- | Compare two sizes in max view.
compareMaxViews :: (MonadConversion m) => Comparison -> SizeMaxView -> SizeMaxView -> m ()
compareMaxViews cmp us vs = case (cmp, us, vs) of
  (CmpLeq, _, (DSizeInf :| _)) -> return ()
  (cmp, u:|[], v:|[]) -> compareSizeViews cmp u v
  (CmpLeq, us, v:|[]) -> Fold.forM_ us $ \ u -> compareSizeViews cmp u v
  (CmpLeq, us, vs)    -> Fold.forM_ us $ \ u -> compareBelowMax u vs
  (CmpEq,  us, vs)    -> do
    compareMaxViews CmpLeq us vs
    compareMaxViews CmpLeq vs us

-- | @compareBelowMax u vs@ checks @u <= max vs@.  Precondition: @size vs >= 2@
compareBelowMax :: (MonadConversion m) => DeepSizeView -> SizeMaxView -> m ()
compareBelowMax u vs = verboseBracket "tc.conv.size" 45 "compareBelowMax" $ do
  reportSDoc "tc.conv.size" 45 $ sep
    [ pretty u
    , pretty CmpLeq
    , pretty vs
    ]
  -- When trying several alternatives, we do not assign metas
  -- and also do not produce constraints (see 'giveUp' below).
  -- Andreas, 2019-03-28, issue #3600.
  alt (dontAssignMetas $ Fold.foldr1 alt $ fmap (compareSizeViews CmpLeq u) vs) $ do
    reportSDoc "tc.conv.size" 45 $ vcat
      [ "compareBelowMax: giving up"
      ]
    u <- unDeepSizeView u
    v <- unMaxView vs
    size <- sizeType
    giveUp CmpLeq size u v
  where
  alt c1 c2 = c1 `catchError` const c2

compareSizeViews :: (MonadConversion m) => Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews cmp s1' s2' = do
  reportSDoc "tc.conv.size" 45 $ hsep
    [ "compareSizeViews"
    , pretty s1'
    , pretty cmp
    , pretty s2'
    ]
  size <- sizeType
  let (s1, s2) = removeSucs (s1', s2')
      withUnView cont = do
        u <- unDeepSizeView s1
        v <- unDeepSizeView s2
        cont u v
      failure = withUnView $ \ u v -> typeError $ UnequalTerms cmp u v AsSizes
      continue cmp = withUnView $ compareAtom cmp AsSizes
  case (cmp, s1, s2) of
    (CmpLeq, _,            DSizeInf)   -> return ()
    (CmpEq,  DSizeInf,     DSizeInf)   -> return ()
    (CmpEq,  DSizeVar{},   DSizeInf)   -> failure
    (_    ,  DSizeInf,     DSizeVar{}) -> failure
    (_    ,  DSizeInf,     _         ) -> continue CmpEq
    (CmpLeq, DSizeVar i n, DSizeVar j m) | i == j -> unless (n <= m) failure
    (CmpLeq, DSizeVar i n, DSizeVar j m) | i /= j -> do
       res <- isBoundedProjVar i
       case res of
         BoundedNo -> failure
         BoundedLt u' -> do
            -- now we have i < u', in the worst case i+1 = u'
            -- and we want to check i+n <= v
            v <- unDeepSizeView s2
            if n > 0 then do
              u'' <- sizeSuc (n - 1) u'
              compareSizes cmp u'' v
             else compareSizes cmp u' =<< sizeSuc 1 v
    (CmpLeq, s1,        s2)         -> withUnView $ \ u v -> do
      unlessM (trivial u v) $ giveUp CmpLeq size u v
    (CmpEq, s1, s2) -> continue cmp

-- | If 'envAssignMetas' then postpone as constraint, otherwise, fail hard.
--   Failing is required if we speculatively test several alternatives.
giveUp :: (MonadConversion m) => Comparison -> Type -> Term -> Term -> m ()
giveUp cmp size u v =
  ifM (asksTC envAssignMetas)
    {-then-} (addConstraint unblock $ ValueCmp CmpLeq AsSizes u v)
    {-else-} (typeError $ UnequalTerms cmp u v AsSizes)
  where
    unblock = unblockOnAnyMetaIn [u, v]

-- | Checked whether a size constraint is trivial (like @X <= X+1@).
trivial :: (MonadConversion m) => Term -> Term -> m Bool
trivial u v = do
    a@(e , n ) <- oldSizeExpr u
    b@(e', n') <- oldSizeExpr v
    let triv = e == e' && n <= n'
          -- Andreas, 2012-02-24  filtering out more trivial constraints fixes
          -- test/lib-succeed/SizeInconsistentMeta4.agda
    reportSDoc "tc.conv.size" 60 $
      nest 2 $ sep [ if triv then "trivial constraint" else empty
                   , pretty a <+> "<="
                   , pretty b
                   ]
    return triv
  `catchError` \_ -> return False

------------------------------------------------------------------------
-- * Size constraints.
------------------------------------------------------------------------

-- | Test whether a problem consists only of size constraints.
isSizeProblem :: (ReadTCState m, HasOptions m, HasBuiltins m) => ProblemId -> m Bool
isSizeProblem pid = do
  test <- isSizeTypeTest
  all (mkIsSizeConstraint test (const True) . theConstraint) <$> getConstraintsForProblem pid

-- | Test whether a constraint speaks about sizes.
isSizeConstraint :: (HasOptions m, HasBuiltins m) => (Comparison -> Bool) -> Closure Constraint -> m Bool
isSizeConstraint p c = isSizeTypeTest <&> \ test -> mkIsSizeConstraint test p c

mkIsSizeConstraint :: (Term -> Maybe BoundedSize) -> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint test = isSizeConstraint_ $ isJust . test . unEl

isSizeConstraint_
  :: (Type -> Bool)       -- ^ Test for being a sized type
  -> (Comparison -> Bool) -- ^ Restriction to these directions.
  -> Closure Constraint
  -> Bool
isSizeConstraint_ _isSizeType p Closure{ clValue = ValueCmp cmp AsSizes       _ _ } = p cmp
isSizeConstraint_  isSizeType p Closure{ clValue = ValueCmp cmp (AsTermsOf s) _ _ } = p cmp && isSizeType s
isSizeConstraint_ _isSizeType _ _ = False

-- | Take out all size constraints of the given direction (DANGER!).
takeSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
takeSizeConstraints p = do
  test <- isSizeTypeTest
  takeConstraints (mkIsSizeConstraint test p . theConstraint)

-- | Find the size constraints of the matching direction.
getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
getSizeConstraints p = do
  test <- isSizeTypeTest
  filter (mkIsSizeConstraint test p . theConstraint) <$> getAllConstraints

-- | Return a list of size metas and their context.
getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
getSizeMetas interactionMetas = do
  test <- isSizeTypeTest
  catMaybes <$> do
    getOpenMetas >>= do
      mapM $ \ m -> do
        let no = return Nothing
        mi <- lookupMeta m
        case mvJudgement mi of
          _ | BlockedConst{} <- mvInstantiation mi -> no  -- Blocked terms should not be touched (#2637, #2881)
          HasType _ cmp a -> do
            TelV tel b <- telView a
            -- b is reduced
            caseMaybe (test $ unEl b) no $ \ _ -> do
              let yes = return $ Just (m, a, tel)
              if interactionMetas then yes else do
                ifM (isJust <$> isInteractionMeta m) no yes
          _ -> no

{- ROLLED BACK
getSizeMetas :: TCM ([(MetaId, Int)], [SizeConstraint])
getSizeMetas = do
  ms <- getOpenMetas
  test <- isSizeTypeTest
  let sizeCon m = do
        let nothing  = return ([], [])
        mi <- lookupMeta m
        case mvJudgement mi of
          HasType _ a -> do
            TelV tel b <- telView =<< instantiateFull a
            let noConstr = return ([(m, size tel)], [])
            case test b of
              Nothing            -> nothing
              Just BoundedNo     -> noConstr
              Just (BoundedLt u) -> noConstr
{- WORKS NOT
              Just (BoundedLt u) -> flip catchError (const $ noConstr) $ do
                -- we assume the metavariable is used in an
                -- extension of its creation context
                ctxIds <- getContextId
                let a = SizeMeta m $ take (size tel) $ reverse ctxIds
                (b, n) <- oldSizeExpr u
                return ([(m, size tel)], [Leq a (n-1) b])
-}
          _ -> nothing
  (mss, css) <- unzip <$> mapM sizeCon ms
  return (concat mss, concat css)
-}

------------------------------------------------------------------------
-- * Size constraint solving.
------------------------------------------------------------------------

-- | Atomic size expressions.
data OldSizeExpr
  = SizeMeta MetaId [Int] -- ^ A size meta applied to de Bruijn indices.
  | Rigid Int             -- ^ A de Bruijn index.
  deriving (Eq, Show)

instance Pretty OldSizeExpr where
  pretty (SizeMeta m _) = P.text $ "X" ++ show (fromIntegral m :: Int)
  pretty (Rigid i)      = P.text $ "c" ++ show i

-- | Size constraints we can solve.
data OldSizeConstraint
  = Leq OldSizeExpr Int OldSizeExpr
    -- ^ @Leq a +n b@ represents @a =< b + n@.
    --   @Leq a -n b@ represents @a + n =< b@.
  deriving (Show)

instance Pretty OldSizeConstraint where
  pretty (Leq a n b)
    | n == 0    = P.pretty a P.<+> "=<" P.<+> P.pretty b
    | n > 0     = P.pretty a P.<+> "=<" P.<+> P.pretty b P.<+> "+" P.<+> P.text (show n)
    | otherwise = P.pretty a P.<+> "+" P.<+> P.text (show (-n)) P.<+> "=<" P.<+> P.pretty b

-- | Compute a set of size constraints that all live in the same context
--   from constraints over terms of type size that may live in different
--   contexts.
--
--   cf. 'Agda.TypeChecking.LevelConstraints.simplifyLevelConstraint'
oldComputeSizeConstraints :: [ProblemConstraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [] = return [] -- special case to avoid maximum []
oldComputeSizeConstraints cs = catMaybes <$> mapM oldComputeSizeConstraint leqs
  where
    -- get the constraints plus contexts they are defined in
    gammas       = map (envContext . clEnv . theConstraint) cs
    ls           = map (clValue . theConstraint) cs
    -- compute the longest context (common water level)
    ns           = map size gammas
    waterLevel   = maximum ns
    -- lift all constraints to live in the longest context
    -- (assuming this context is an extension of the shorter ones)
    -- by raising the de Bruijn indices
    leqs = zipWith raise (map (waterLevel -) ns) ls

-- | Turn a constraint over de Bruijn indices into a size constraint.
oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint)
oldComputeSizeConstraint c =
  case c of
    ValueCmp CmpLeq _ u v -> do
        reportSDoc "tc.size.solve" 50 $ sep
          [ "converting size constraint"
          , prettyTCM c
          ]
        (a, n) <- oldSizeExpr u
        (b, m) <- oldSizeExpr v
        return $ Just $ Leq a (m - n) b
      `catchError` \ err -> case err of
        PatternErr{} -> return Nothing
        _            -> throwError err
    _ -> __IMPOSSIBLE__

-- | Turn a term with de Bruijn indices into a size expression with offset.
--
--   Throws a 'patternViolation' if the term isn't a proper size expression.
oldSizeExpr :: (PureTCM m, MonadBlock m) => Term -> m (OldSizeExpr, Int)
oldSizeExpr u = do
  u <- reduce u -- Andreas, 2009-02-09.
                -- This is necessary to surface the solutions of metavariables.
  reportSDoc "tc.conv.size" 60 $ "oldSizeExpr:" <+> prettyTCM u
  s <- sizeView u
  case s of
    SizeInf     -> patternViolation neverUnblock
    SizeSuc u   -> mapSnd (+1) <$> oldSizeExpr u
    OtherSize u -> case u of
      Var i []  -> return (Rigid i, 0)
      MetaV m es | Just xs <- mapM isVar es, fastDistinct xs
                -> return (SizeMeta m xs, 0)
      _ -> patternViolation neverUnblock
  where
    isVar (Proj{})  = Nothing
    isVar (IApply _ _ v) = isVar (Apply (defaultArg v))
    isVar (Apply v) = case unArg v of
      Var i [] -> Just i
      _        -> Nothing

-- | Compute list of size metavariables with their arguments
--   appearing in a constraint.
flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
flexibleVariables (Leq a _ b) = flex a ++ flex b
  where
    flex (Rigid _)       = []
    flex (SizeMeta m xs) = [(m, xs)]

-- | Convert size constraint into form where each meta is applied
--   to indices @0,1,..,n-1@ where @n@ is the arity of that meta.
--
--   @X[σ] <= t@ becomes @X[id] <= t[σ^-1]@
--
--   @X[σ] ≤ Y[τ]@ becomes @X[id] ≤ Y[τ[σ^-1]]@ or @X[σ[τ^1]] ≤ Y[id]@
--   whichever is defined.  If none is defined, we give up.
--
oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint
oldCanonicalizeSizeConstraint c@(Leq a n b) =
  case (a,b) of
    (Rigid{}, Rigid{})       -> return c
    (SizeMeta m xs, Rigid i) -> do
      j <- List.elemIndex i xs
      return $ Leq (SizeMeta m [0..size xs-1]) n (Rigid j)
    (Rigid i, SizeMeta m xs) -> do
      j <- List.elemIndex i xs
      return $ Leq (Rigid j) n (SizeMeta m [0..size xs-1])
    (SizeMeta m xs, SizeMeta l ys)
         -- try to invert xs on ys
       | Just ys' <- mapM (\ y -> List.elemIndex y xs) ys ->
           return $ Leq (SizeMeta m [0..size xs-1]) n (SizeMeta l ys')
         -- try to invert ys on xs
       | Just xs' <- mapM (\ x -> List.elemIndex x ys) xs ->
           return $ Leq (SizeMeta m xs') n (SizeMeta l [0..size ys-1])
         -- give up
       | otherwise -> Nothing

-- | Main function.
--   Uses the old solver for size constraints using "Agda.Utils.Warshall".
--   This solver does not smartly use size hypotheses @j : Size< i@.
--   It only checks that its computed solution is compatible
oldSolveSizeConstraints :: TCM ()
oldSolveSizeConstraints = whenM haveSizedTypes $ do
  reportSLn "tc.size.solve" 70 $ "Considering to solve size constraints"
  cs0 <- getSizeConstraints (== CmpLeq)
  cs <- oldComputeSizeConstraints cs0
  ms <- getSizeMetas True -- get all size metas, also interaction metas

  when (not (null cs) || not (null ms)) $ do
    reportSLn "tc.size.solve" 10 $ "Solving size constraints " ++ show cs

    cs <- return $ mapMaybe oldCanonicalizeSizeConstraint cs
    reportSLn "tc.size.solve" 10 $ "Canonicalized constraints: " ++ show cs

    let -- Error for giving up
        cannotSolve = typeError . GenericDocError =<<
          vcat ("Cannot solve size constraints" : map prettyTCM cs0)

        -- Size metas in constraints.
        metas0 :: [(MetaId, Int)]  -- meta id + arity
        metas0 = List.nubOn id $ map (mapSnd length) $ concatMap flexibleVariables cs

        -- Unconstrained size metas that do not occur in constraints.
        metas1 :: [(MetaId, Int)]
        metas1 = forMaybe ms $ \ (m, _, tel) ->
          maybe (Just (m, size tel)) (const Nothing) $
            lookup m metas0

        -- All size metas
        metas = metas0 ++ metas1

    reportSLn "tc.size.solve" 15 $ "Metas: " ++ show metas0 ++ ", " ++ show metas1

    verboseS "tc.size.solve" 20 $
        -- debug print the type of all size metas
        forM_ metas $ \ (m, _) ->
            reportSDoc "tc.size.solve" 20 $ prettyTCM =<< mvJudgement <$> lookupMeta m

    -- Run the solver.
    unlessM (oldSolver metas cs) cannotSolve

    -- Double-checking the solution.

    -- Andreas, 2012-09-19
    -- The returned solution might not be consistent with
    -- the hypotheses on rigid vars (j : Size< i).
    -- Thus, we double check that all size constraints
    -- have been solved correctly.
    flip catchError (const cannotSolve) $
      noConstraints $
        forM_ cs0 $ withConstraint solveConstraint


-- | Old solver for size constraints using "Agda.Utils.Warshall".
--   This solver does not smartly use size hypotheses @j : Size< i@.
oldSolver
  :: [(MetaId, Int)]      -- ^ Size metas and their arity.
  -> [OldSizeConstraint]  -- ^ Size constraints (in preprocessed form).
  -> TCM Bool             -- ^ Returns @False@ if solver fails.
oldSolver metas cs = do
  let cannotSolve    = return False
      mkFlex (m, ar) = W.NewFlex (fromIntegral m) $ \ i -> fromIntegral i < ar
      mkConstr (Leq a n b)  = W.Arc (mkNode a) n (mkNode b)
      mkNode (Rigid i)      = W.Rigid $ W.RVar i
      mkNode (SizeMeta m _) = W.Flex $ fromIntegral m

  -- run the Warshall solver
  case W.solve $ map mkFlex metas ++ map mkConstr cs of
    Nothing  -> cannotSolve
    Just sol -> do
      reportSLn "tc.size.solve" 10 $ "Solved constraints: " ++ prettyShow sol
      suc   <- primSizeSuc
      infty <- primSizeInf
      let plus v 0 = v
          plus v n = suc `apply1` plus v (n - 1)

          inst (i, e) = do

            let m  = fromIntegral i  -- meta variable identifier
                ar = fromMaybe __IMPOSSIBLE__ $ lookup m metas  -- meta var arity

                term (W.SizeConst W.Infinite) = infty
                term (W.SizeVar j n) | j < ar = plus (var $ ar - j - 1) n
                term _                        = __IMPOSSIBLE__

                tel = replicate ar $ defaultArg "s"
                -- convert size expression to term
                v = term e

            reportSDoc "tc.size.solve" 20 $ sep
              [ pretty m <+> ":="
              , nest 2 $ prettyTCM v
              ]

            -- Andreas, 2012-09-25: do not assign interaction metas to \infty
            let isInf (W.SizeConst W.Infinite) = True
                isInf _                        = False
            unlessM (((isInf e &&) . isJust <$> isInteractionMeta m) `or2M` isFrozen m) $
              assignTerm m tel v

      mapM_ inst $ Map.toList sol
      return True