{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.SizedTypes where

import Prelude hiding (null)

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 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.List1 (pattern (:|))
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (Pretty, prettyShow)
import qualified Agda.Utils.ProfileOptions as Profile
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 :: Term -> TCM ()
checkSizeLtSat Term
t = forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCM Bool
haveSizeLt forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size" Int
10 forall a b. (a -> b) -> a -> b
$ do
    Telescope
tel <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
    forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"checking that " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is not an empty type of sizes"
      , if forall a. Null a => a -> Bool
null Telescope
tel then forall a. Null a => a
empty else do
        TCMT IO Doc
"in context " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel)
      ]
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size" Int
60 forall a b. (a -> b) -> a -> b
$ [Char]
"- raw type = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term
t
  let postpone :: Blocker -> Term -> TCM ()
      postpone :: Blocker -> Term -> TCM ()
postpone Blocker
b Term
t = do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.lt" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"- postponing `not empty type of sizes' check for " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t ]
        forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
b forall a b. (a -> b) -> a -> b
$ Term -> Constraint
CheckSizeLtSat Term
t
  let ok :: TCM ()
      ok :: TCM ()
ok = forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.lt" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"- succeeded: not an empty type of sizes"
  forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
t Blocker -> Term -> TCM ()
postpone forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
t -> do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.lt" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"- type is not blocked"
    forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Term
t) TCM ()
ok forall a b. (a -> b) -> a -> b
$ \ BoundedSize
b -> do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.lt" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
" - type is a size type"
      case BoundedSize
b of
        BoundedSize
BoundedNo -> TCM ()
ok
        BoundedLt Term
b -> do
          forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.lt" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" - type is SIZELT" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
b
          forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
b (\ Blocker
x Term
_ -> Blocker -> Term -> TCM ()
postpone Blocker
x Term
t) forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
b -> do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.lt" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
" - size bound is not blocked"
            forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Term -> Constraint
CheckSizeLtSat Term
t) forall a b. (a -> b) -> a -> b
$ do
              forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Term -> TCM Bool
checkSizeNeverZero Term
b) forall a b. (a -> b) -> a -> b
$ do
                forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
                  TCMT IO Doc
"Possibly empty type of sizes " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t

-- | Precondition: Term is reduced and not blocked.
--   Throws a 'patternViolation' if undecided
checkSizeNeverZero :: Term -> TCM Bool
checkSizeNeverZero :: Term -> TCM Bool
checkSizeNeverZero Term
u = do
  SizeView
v <- forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
  case SizeView
v of
    SizeView
SizeInf     -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- OK, infty is never 0.
    SizeSuc{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- OK, a + 1 is never 0.
    OtherSize Term
u ->
      case Term
u of
        Var Int
i [] -> Int -> TCM Bool
checkSizeVarNeverZero Int
i
        -- neutral sizes cannot be guaranteed > 0
        Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
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 :: Int -> TCM Bool
checkSizeVarNeverZero Int
i = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checkSizeVarNeverZero" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
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.
  [Type]
ts <- forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m Context
getContext
  -- If we encountered a blocking meta in the context, we cannot
  -- say ``no'' for sure.
  (Int
n, Set Blocker
blockers) <- forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall a b. (a -> b) -> a -> b
$ [Type] -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
minSizeValAux [Type]
ts forall a b. (a -> b) -> a -> b
$ forall a. a -> [a]
repeat Int
0
  let blocker :: Blocker
blocker = Set Blocker -> Blocker
unblockOnAll Set Blocker
blockers
  if Int
n forall a. Ord a => a -> a -> Bool
> Int
0 then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else
    if Blocker
blocker forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock
      then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      else forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
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 :: [Type] -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
minSizeValAux [Type]
_        []      = forall a. HasCallStack => a
__IMPOSSIBLE__
  minSizeValAux []       (Int
n : [Int]
_) = forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
  minSizeValAux (Type
t : [Type]
ts) (Int
n : [Int]
ns) = do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size" Int
60 forall a b. (a -> b) -> a -> b
$
       forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"minSizeVal (n:ns) = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts forall a. Num a => a -> a -> a
+ Int
2) forall a b. (a -> b) -> a -> b
$ Int
nforall a. a -> [a] -> [a]
:[Int]
ns) forall a. [a] -> [a] -> [a]
++
             [Char]
" t =") forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show) Type
t  -- prettyTCM t  -- Wrong context!
    -- n is the min. value for variable 0 which has type t.
    let cont :: WriterT (Set Blocker) (TCMT IO) Int
cont = [Type] -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
minSizeValAux [Type]
ts [Int]
ns
        perhaps :: Blocker -> WriterT (Set Blocker) (TCMT IO) Int
perhaps Blocker
x = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (forall a. a -> Set a
Set.singleton Blocker
x) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriterT (Set Blocker) (TCMT IO) Int
cont
    -- If we encounter a blocked type in the context, we cannot
    -- give a definite answer.
    forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
x Type
_ -> Blocker -> WriterT (Set Blocker) (TCMT IO) Int
perhaps Blocker
x) forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
      forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
t) WriterT (Set Blocker) (TCMT IO) Int
cont forall a b. (a -> b) -> a -> b
$ \ BoundedSize
b -> do
        case BoundedSize
b of
          BoundedSize
BoundedNo -> WriterT (Set Blocker) (TCMT IO) Int
cont
          BoundedLt Term
u -> forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
u (\ Blocker
x Term
_ -> Blocker -> WriterT (Set Blocker) (TCMT IO) Int
perhaps Blocker
x) forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
u -> do
            forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size" Int
60 forall a b. (a -> b) -> a -> b
$ [Char]
"minSizeVal upper bound u = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Term
u
            DeepSizeView
v <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(PureTCM m, MonadTCError m) =>
Term -> m DeepSizeView
deepSizeView Term
u
            case DeepSizeView
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 Int
j []) Int
m -> do
                forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size" Int
60 forall a b. (a -> b) -> a -> b
$ [Char]
"minSizeVal upper bound v = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show DeepSizeView
v
                let ns' :: [Int]
ns' = forall a. Int -> (a -> a) -> [a] -> [a]
List.updateAt Int
j (forall a. Ord a => a -> a -> a
max forall a b. (a -> b) -> a -> b
$ Int
nforall a. Num a => a -> a -> a
+Int
1forall a. Num a => a -> a -> a
-Int
m) [Int]
ns
                forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size" Int
60 forall a b. (a -> b) -> a -> b
$ [Char]
"minSizeVal ns' = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts forall a. Num a => a -> a -> a
+ Int
1) [Int]
ns')
                [Type] -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
minSizeValAux [Type]
ts [Int]
ns'
              DSizeMeta MetaId
x [Elim]
_ Int
_ -> Blocker -> WriterT (Set Blocker) (TCMT IO) Int
perhaps (MetaId -> Blocker
unblockOnMeta MetaId
x)
              DeepSizeView
_ -> WriterT (Set Blocker) (TCMT IO) Int
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 :: forall (m :: * -> *). PureTCM m => Int -> m BoundedSize
isBounded Int
i = forall (m :: * -> *). PureTCM m => Type -> m BoundedSize
isBoundedSizeType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Type
typeOfBV Int
i

isBoundedProjVar
  :: (MonadCheckInternal m, PureTCM m)
  => ProjectedVar -> m BoundedSize
isBoundedProjVar :: forall (m :: * -> *).
(MonadCheckInternal m, PureTCM m) =>
ProjectedVar -> m BoundedSize
isBoundedProjVar ProjectedVar
pv = forall (m :: * -> *). PureTCM m => Type -> m BoundedSize
isBoundedSizeType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadCheckInternal m => Term -> m Type
infer (ProjectedVar -> Term
unviewProjectedVar ProjectedVar
pv)

isBoundedSizeType :: PureTCM m => Type -> m BoundedSize
isBoundedSizeType :: forall (m :: * -> *). PureTCM m => Type -> m BoundedSize
isBoundedSizeType Type
t =
  forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Def QName
x [Apply Arg Term
u] -> do
      Maybe Term
sizelt <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getBuiltin' [Char]
builtinSizeLt
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if (forall a. a -> Maybe a
Just (QName -> [Elim] -> Term
Def QName
x []) forall a. Eq a => a -> a -> Bool
== Maybe Term
sizelt) then Term -> BoundedSize
BoundedLt forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
u else BoundedSize
BoundedNo
    Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return BoundedSize
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 :: forall (m :: * -> *).
(MonadConstraint m, MonadTCEnv m, ReadTCState m, MonadAddContext m,
 HasOptions m, HasBuiltins m) =>
Term -> Telescope -> Type -> m ()
boundedSizeMetaHook v :: Term
v@(MetaV MetaId
x [Elim]
_) Telescope
tel0 Type
a = do
  Maybe BoundedSize
res <- forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
a
  case Maybe BoundedSize
res of
    Just (BoundedLt Term
u) -> do
      Int
n <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
      let tel :: Telescope
tel | Int
n forall a. Ord a => a -> a -> Bool
> Int
0     = ListTel -> Telescope
telFromList forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
n forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel0
              | Bool
otherwise = Telescope
tel0
      forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ do
        Term
v <- forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Int -> a -> a
raise (forall a. Sized a => a -> Int
size Telescope
tel) Term
v forall t. Apply t => t -> Args -> t
`apply` forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel
        -- compareSizes CmpLeq v u
        forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (MetaId -> Blocker
unblockOnMeta MetaId
x) forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpLeq CompareAs
AsSizes Term
v Term
u
    Maybe BoundedSize
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
boundedSizeMetaHook Term
_ Telescope
_ Type
_ = forall a. HasCallStack => a
__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 :: forall (m :: * -> *).
MonadConversion m =>
Comparison
-> CompareAs
-> Term
-> Term
-> QName
-> [Elim]
-> QName
-> [Elim]
-> m ()
trySizeUniv Comparison
cmp CompareAs
t Term
m Term
n QName
x [Elim]
els1 QName
y [Elim]
els2 = do
  let failure :: forall m a. MonadTCError m => m a
      failure :: forall (m :: * -> *) a. MonadTCError m => m a
failure = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
m Term
n CompareAs
t
      forceInfty :: Arg Term -> m ()
forceInfty Arg Term
u = forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
CmpEq (forall e. Arg e -> e
unArg Arg Term
u) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  -- Get the SIZE built-ins.
  (QName
size, QName
sizelt) <- forall a b c. (a -> b -> c) -> b -> a -> c
flip forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (forall a b. a -> b -> a
const forall (m :: * -> *) a. MonadTCError m => m a
failure) forall a b. (a -> b) -> a -> b
$ do
     Def QName
size   [Elim]
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
     Def QName
sizelt [Elim]
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeLt
     forall (m :: * -> *) a. Monad m => a -> m a
return (QName
size, QName
sizelt)
  case (Comparison
cmp, [Elim]
els1, [Elim]
els2) of
     -- Case @Size< _ <= Size@: true.
     (Comparison
CmpLeq, [Elim
_], [])  | QName
x forall a. Eq a => a -> a -> Bool
== QName
sizelt Bool -> Bool -> Bool
&& QName
y forall a. Eq a => a -> a -> Bool
== QName
size -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
     -- Case @Size< u = Size@: forces @u = ∞@.
     (Comparison
_, [Apply Arg Term
u], []) | QName
x forall a. Eq a => a -> a -> Bool
== QName
sizelt Bool -> Bool -> Bool
&& QName
y forall a. Eq a => a -> a -> Bool
== QName
size -> forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh Int m) =>
Arg Term -> m ()
forceInfty Arg Term
u
     (Comparison
_, [], [Apply Arg Term
u]) | QName
x forall a. Eq a => a -> a -> Bool
== QName
size Bool -> Bool -> Bool
&& QName
y forall a. Eq a => a -> a -> Bool
== QName
sizelt -> forall {m :: * -> *}.
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh Int m) =>
Arg Term -> m ()
forceInfty Arg Term
u
     -- This covers all cases for SIZE and SIZELT.
     -- The remaining case is for @x@ and @y@ which are not size built-ins.
     (Comparison, [Elim], [Elim])
_                                             -> forall (m :: * -> *) a. MonadTCError m => m a
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 :: forall (m :: * -> *).
(PureTCM m, MonadTCError m) =>
Term -> m DeepSizeView
deepSizeView Term
v = do
  Def QName
inf [] <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  Def QName
suc [] <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
  let loop :: Term -> m DeepSizeView
loop Term
v =
        forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Def QName
x []        | QName
x forall a. Eq a => a -> a -> Bool
== QName
inf -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ DeepSizeView
DSizeInf
          Def QName
x [Apply Arg Term
u] | QName
x forall a. Eq a => a -> a -> Bool
== QName
suc -> QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ QName
suc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m DeepSizeView
loop (forall e. Arg e -> e
unArg Arg Term
u)

          Var Int
i [Elim]
es | Just ProjectedVar
pv <- Int -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim [Elim]
es
                                     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ProjectedVar -> Int -> DeepSizeView
DSizeVar ProjectedVar
pv Int
0
          MetaV MetaId
x [Elim]
us                 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ MetaId -> [Elim] -> Int -> DeepSizeView
DSizeMeta MetaId
x [Elim]
us Int
0
          Term
v                          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term -> DeepSizeView
DOtherSize Term
v
  Term -> m DeepSizeView
loop Term
v

sizeMaxView :: PureTCM m => Term -> m SizeMaxView
sizeMaxView :: forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
sizeMaxView Term
v = do
  Maybe QName
inf <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinDefName [Char]
builtinSizeInf
  Maybe QName
suc <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinDefName [Char]
builtinSizeSuc
  Maybe QName
max <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinDefName [Char]
builtinSizeMax
  let loop :: Term -> m SizeMaxView
loop Term
v = do
        Term
v <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
        case Term
v of
          Def QName
x []                   | forall a. a -> Maybe a
Just QName
x forall a. Eq a => a -> a -> Bool
== Maybe QName
inf -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ DeepSizeView
DSizeInf
          Def QName
x [Apply Arg Term
u]            | forall a. a -> Maybe a
Just QName
x forall a. Eq a => a -> a -> Bool
== Maybe QName
suc -> QName -> SizeMaxView -> SizeMaxView
maxViewSuc_ (forall a. HasCallStack => Maybe a -> a
fromJust Maybe QName
suc) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m SizeMaxView
loop (forall e. Arg e -> e
unArg Arg Term
u)
          Def QName
x [Apply Arg Term
u1, Apply Arg Term
u2] | forall a. a -> Maybe a
Just QName
x forall a. Eq a => a -> a -> Bool
== Maybe QName
max -> SizeMaxView -> SizeMaxView -> SizeMaxView
maxViewMax forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m SizeMaxView
loop (forall e. Arg e -> e
unArg Arg Term
u1) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m SizeMaxView
loop (forall e. Arg e -> e
unArg Arg Term
u2)
          Var Int
i [Elim]
es | Just ProjectedVar
pv <- Int -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim [Elim]
es
                                        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ ProjectedVar -> Int -> DeepSizeView
DSizeVar ProjectedVar
pv Int
0
          MetaV MetaId
x [Elim]
us                    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ MetaId -> [Elim] -> Int -> DeepSizeView
DSizeMeta MetaId
x [Elim]
us Int
0
          Term
_                             -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ Term -> DeepSizeView
DOtherSize Term
v
  Term -> m SizeMaxView
loop Term
v

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

-- | Compare two sizes.
compareSizes :: (MonadConversion m) => Comparison -> Term -> Term -> m ()
compareSizes :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u Term
v = forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.conv.size" Int
10 [Char]
"compareSizes" forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"Comparing sizes"
    , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp
                   , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
                   ]
    ]
  forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.conv.size" Int
60 forall a b. (a -> b) -> a -> b
$ do
    Term
u <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
    Term
v <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
60 forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
u forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp
                   , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
                   ]
  forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Conversion forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadStatistics m => [Char] -> m ()
tick [Char]
"compare sizes"
  SizeMaxView
us <- forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
sizeMaxView Term
u
  SizeMaxView
vs <- forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
sizeMaxView Term
v
  forall (m :: * -> *).
MonadConversion m =>
Comparison -> SizeMaxView -> SizeMaxView -> m ()
compareMaxViews Comparison
cmp SizeMaxView
us SizeMaxView
vs

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

-- | @compareBelowMax u vs@ checks @u <= max vs@.  Precondition: @size vs >= 2@
compareBelowMax :: (MonadConversion m) => DeepSizeView -> SizeMaxView -> m ()
compareBelowMax :: forall (m :: * -> *).
MonadConversion m =>
DeepSizeView -> SizeMaxView -> m ()
compareBelowMax DeepSizeView
u SizeMaxView
vs = forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.conv.size" Int
45 [Char]
"compareBelowMax" forall a b. (a -> b) -> a -> b
$ do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
45 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeepSizeView
u
    , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Comparison
CmpLeq
    , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty SizeMaxView
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.
  forall {e} {m :: * -> *} {a}. MonadError e m => m a -> m a -> m a
alt (forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
Fold.foldr1 forall {e} {m :: * -> *} {a}. MonadError e m => m a -> m a -> m a
alt forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
CmpLeq DeepSizeView
u) SizeMaxView
vs) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
45 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"compareBelowMax: giving up"
      ]
    Term
u <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
u
    Term
v <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
SizeMaxView -> m Term
unMaxView SizeMaxView
vs
    Type
size <- forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
    forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
giveUp Comparison
CmpLeq Type
size Term
u Term
v
  where
  alt :: m a -> m a -> m a
alt m a
c1 m a
c2 = m a
c1 forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` forall a b. a -> b -> a
const m a
c2

compareSizeViews :: (MonadConversion m) => Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
cmp DeepSizeView
s1' DeepSizeView
s2' = do
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
45 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
    [ TCMT IO Doc
"compareSizeViews"
    , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeepSizeView
s1'
    , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Comparison
cmp
    , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeepSizeView
s2'
    ]
  Type
size <- forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
  let (DeepSizeView
s1, DeepSizeView
s2) = (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
removeSucs (DeepSizeView
s1', DeepSizeView
s2')
      withUnView :: (Term -> Term -> m ()) -> m ()
withUnView Term -> Term -> m ()
cont = do
        Term
u <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s1
        Term
v <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s2
        Term -> Term -> m ()
cont Term
u Term
v
      failure :: m ()
failure = (Term -> Term -> m ()) -> m ()
withUnView forall a b. (a -> b) -> a -> b
$ \ Term
u Term
v -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
u Term
v CompareAs
AsSizes
      continue :: Comparison -> m ()
continue Comparison
cmp = (Term -> Term -> m ()) -> m ()
withUnView forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom Comparison
cmp CompareAs
AsSizes
  case (Comparison
cmp, DeepSizeView
s1, DeepSizeView
s2) of
    (Comparison
CmpLeq, DeepSizeView
_,            DeepSizeView
DSizeInf)   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Comparison
CmpEq,  DeepSizeView
DSizeInf,     DeepSizeView
DSizeInf)   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Comparison
CmpEq,  DSizeVar{},   DeepSizeView
DSizeInf)   -> m ()
failure
    (Comparison
_    ,  DeepSizeView
DSizeInf,     DSizeVar{}) -> m ()
failure
    (Comparison
_    ,  DeepSizeView
DSizeInf,     DeepSizeView
_         ) -> Comparison -> m ()
continue Comparison
CmpEq
    (Comparison
CmpLeq, DSizeVar ProjectedVar
i Int
n, DSizeVar ProjectedVar
j Int
m) | ProjectedVar
i forall a. Eq a => a -> a -> Bool
== ProjectedVar
j -> forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n forall a. Ord a => a -> a -> Bool
<= Int
m) m ()
failure
    (Comparison
CmpLeq, DSizeVar ProjectedVar
i Int
n, DSizeVar ProjectedVar
j Int
m) | ProjectedVar
i forall a. Eq a => a -> a -> Bool
/= ProjectedVar
j -> do
       BoundedSize
res <- forall (m :: * -> *).
(MonadCheckInternal m, PureTCM m) =>
ProjectedVar -> m BoundedSize
isBoundedProjVar ProjectedVar
i
       case BoundedSize
res of
         BoundedSize
BoundedNo -> m ()
failure
         BoundedLt Term
u' -> do
            -- now we have i < u', in the worst case i+1 = u'
            -- and we want to check i+n <= v
            Term
v <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s2
            if Int
n forall a. Ord a => a -> a -> Bool
> Int
0 then do
              Term
u'' <- forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc (Int
n forall a. Num a => a -> a -> a
- Int
1) Term
u'
              forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u'' Term
v
             else forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 Term
v
    (Comparison
CmpLeq, DeepSizeView
s1,        DeepSizeView
s2)         -> (Term -> Term -> m ()) -> m ()
withUnView forall a b. (a -> b) -> a -> b
$ \ Term
u Term
v -> do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (m :: * -> *). MonadConversion m => Term -> Term -> m Bool
trivial Term
u Term
v) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
giveUp Comparison
CmpLeq Type
size Term
u Term
v
    (Comparison
CmpEq, DeepSizeView
s1, DeepSizeView
s2) -> Comparison -> m ()
continue Comparison
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 :: forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
giveUp Comparison
cmp Type
size Term
u Term
v =
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas)
    {-then-} (do
      -- TODO: compute proper blocker
      Blocker
unblock <- forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull [Term
u, Term
v]
      forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
unblock forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpLeq CompareAs
AsSizes Term
u Term
v)
    {-else-} (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
u Term
v CompareAs
AsSizes)

-- | Checked whether a size constraint is trivial (like @X <= X+1@).
trivial :: (MonadConversion m) => Term -> Term -> m Bool
trivial :: forall (m :: * -> *). MonadConversion m => Term -> Term -> m Bool
trivial Term
u Term
v = do
    a :: (OldSizeExpr, Int)
a@(OldSizeExpr
e , Int
n ) <- forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
u
    b :: (OldSizeExpr, Int)
b@(OldSizeExpr
e', Int
n') <- forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
v
    let triv :: Bool
triv = OldSizeExpr
e forall a. Eq a => a -> a -> Bool
== OldSizeExpr
e' Bool -> Bool -> Bool
&& Int
n forall a. Ord a => a -> a -> Bool
<= Int
n'
          -- Andreas, 2012-02-24  filtering out more trivial constraints fixes
          -- test/lib-succeed/SizeInconsistentMeta4.agda
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
60 forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ if Bool
triv then TCMT IO Doc
"trivial constraint" else forall a. Null a => a
empty
                   , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (OldSizeExpr, Int)
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"<="
                   , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (OldSizeExpr, Int)
b
                   ]
    forall (m :: * -> *) a. Monad m => a -> m a
return Bool
triv
  forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

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

-- | Test whether a problem consists only of size constraints.
isSizeProblem :: (ReadTCState m, HasOptions m, HasBuiltins m) => ProblemId -> m Bool
isSizeProblem :: forall (m :: * -> *).
(ReadTCState m, HasOptions m, HasBuiltins m) =>
ProblemId -> m Bool
isSizeProblem ProblemId
pid = do
  Term -> Maybe BoundedSize
test <- forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test (forall a b. a -> b -> a
const Bool
True) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => ProblemId -> m Constraints
getConstraintsForProblem ProblemId
pid

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

mkIsSizeConstraint :: (Term -> Maybe BoundedSize) -> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint :: (Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test = (Type -> Bool)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
isSizeConstraint_ forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe BoundedSize
test forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Type'' t a -> a
unEl

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

-- | Take out all size constraints of the given direction (DANGER!).
takeSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
takeSizeConstraints :: (Comparison -> Bool) -> TCM Constraints
takeSizeConstraints Comparison -> Bool
p = do
  Term -> Maybe BoundedSize
test <- forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m Constraints
takeConstraints ((Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test Comparison -> Bool
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint)

-- | Find the size constraints of the matching direction.
getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
getSizeConstraints :: (Comparison -> Bool) -> TCM Constraints
getSizeConstraints Comparison -> Bool
p = do
  Term -> Maybe BoundedSize
test <- forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  forall a. (a -> Bool) -> [a] -> [a]
filter ((Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test Comparison -> Bool
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints

-- | Return a list of size metas and their context.
getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
getSizeMetas Bool
interactionMetas = do
  Term -> Maybe BoundedSize
test <- forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= do
      forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> do
        let no :: TCMT IO (Maybe a)
no = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        MetaVariable
mi <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
        case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mi of
          Judgement MetaId
_ | BlockedConst{} <- MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mi -> forall {a}. TCMT IO (Maybe a)
no  -- Blocked terms should not be touched (#2637, #2881)
          HasType MetaId
_ Comparison
cmp Type
a -> do
            TelV Telescope
tel Type
b <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
            -- b is reduced
            forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Term -> Maybe BoundedSize
test forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
b) forall {a}. TCMT IO (Maybe a)
no forall a b. (a -> b) -> a -> b
$ \ BoundedSize
_ -> do
              let yes :: TCMT IO (Maybe (MetaId, Type, Telescope))
yes = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (MetaId
m, Type
a, Telescope
tel)
              if Bool
interactionMetas then TCMT IO (Maybe (MetaId, Type, Telescope))
yes else do
                forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
m) forall {a}. TCMT IO (Maybe a)
no TCMT IO (Maybe (MetaId, Type, Telescope))
yes
          Judgement MetaId
_ -> forall {a}. TCMT IO (Maybe a)
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 (OldSizeExpr -> OldSizeExpr -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OldSizeExpr -> OldSizeExpr -> Bool
$c/= :: OldSizeExpr -> OldSizeExpr -> Bool
== :: OldSizeExpr -> OldSizeExpr -> Bool
$c== :: OldSizeExpr -> OldSizeExpr -> Bool
Eq, Int -> OldSizeExpr -> ShowS
[OldSizeExpr] -> ShowS
OldSizeExpr -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [OldSizeExpr] -> ShowS
$cshowList :: [OldSizeExpr] -> ShowS
show :: OldSizeExpr -> [Char]
$cshow :: OldSizeExpr -> [Char]
showsPrec :: Int -> OldSizeExpr -> ShowS
$cshowsPrec :: Int -> OldSizeExpr -> ShowS
Show)

instance Pretty OldSizeExpr where
  pretty :: OldSizeExpr -> Doc
pretty (SizeMeta MetaId
m [Int]
_) = [Char] -> Doc
P.text [Char]
"X" forall a. Semigroup a => a -> a -> a
<> forall a. Pretty a => a -> Doc
P.pretty MetaId
m
  pretty (Rigid Int
i)      = [Char] -> Doc
P.text forall a b. (a -> b) -> a -> b
$ [Char]
"c" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
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 (Int -> OldSizeConstraint -> ShowS
[OldSizeConstraint] -> ShowS
OldSizeConstraint -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [OldSizeConstraint] -> ShowS
$cshowList :: [OldSizeConstraint] -> ShowS
show :: OldSizeConstraint -> [Char]
$cshow :: OldSizeConstraint -> [Char]
showsPrec :: Int -> OldSizeConstraint -> ShowS
$cshowsPrec :: Int -> OldSizeConstraint -> ShowS
Show)

instance Pretty OldSizeConstraint where
  pretty :: OldSizeConstraint -> Doc
pretty (Leq OldSizeExpr
a Int
n OldSizeExpr
b)
    | Int
n forall a. Eq a => a -> a -> Bool
== Int
0    = forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> Doc
"=<" Doc -> Doc -> Doc
P.<+> forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b
    | Int
n forall a. Ord a => a -> a -> Bool
> Int
0     = forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> Doc
"=<" Doc -> Doc -> Doc
P.<+> forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b Doc -> Doc -> Doc
P.<+> Doc
"+" Doc -> Doc -> Doc
P.<+> [Char] -> Doc
P.text (forall a. Show a => a -> [Char]
show Int
n)
    | Bool
otherwise = forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> Doc
"+" Doc -> Doc -> Doc
P.<+> [Char] -> Doc
P.text (forall a. Show a => a -> [Char]
show (-Int
n)) Doc -> Doc -> Doc
P.<+> Doc
"=<" Doc -> Doc -> Doc
P.<+> forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
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 :: Constraints -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [] = forall (m :: * -> *) a. Monad m => a -> m a
return [] -- special case to avoid maximum []
oldComputeSizeConstraints Constraints
cs = forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Constraint -> TCM (Maybe OldSizeConstraint)
oldComputeSizeConstraint [Constraint]
leqs
  where
    -- get the constraints plus contexts they are defined in
    gammas :: [Context]
gammas       = forall a b. (a -> b) -> [a] -> [b]
map (TCEnv -> Context
envContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Closure a -> TCEnv
clEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) Constraints
cs
    ls :: [Constraint]
ls           = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Closure a -> a
clValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) Constraints
cs
    -- compute the longest context (common water level)
    ns :: [Int]
ns           = forall a b. (a -> b) -> [a] -> [b]
map forall a. Sized a => a -> Int
size [Context]
gammas
    waterLevel :: Int
waterLevel   = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int]
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 :: [Constraint]
leqs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Subst a => Int -> a -> a
raise (forall a b. (a -> b) -> [a] -> [b]
map (Int
waterLevel forall a. Num a => a -> a -> a
-) [Int]
ns) [Constraint]
ls

-- | Turn a constraint over de Bruijn indices into a size constraint.
oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint)
oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint)
oldComputeSizeConstraint Constraint
c =
  case Constraint
c of
    ValueCmp Comparison
CmpLeq CompareAs
_ Term
u Term
v -> do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"converting size constraint"
          , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c
          ]
        (OldSizeExpr
a, Int
n) <- forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
u
        (OldSizeExpr
b, Int
m) <- forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
v
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
Leq OldSizeExpr
a (Int
m forall a. Num a => a -> a -> a
- Int
n) OldSizeExpr
b
      forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> case TCErr
err of
        PatternErr{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        TCErr
_            -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
    Constraint
_ -> forall a. HasCallStack => a
__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 :: forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
u = do
  Term
u <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u -- Andreas, 2009-02-09.
                -- This is necessary to surface the solutions of metavariables.
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
60 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"oldSizeExpr:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
  SizeView
s <- forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
  case SizeView
s of
    SizeView
SizeInf     -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
    SizeSuc Term
u   -> forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (forall a. Num a => a -> a -> a
+Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
u
    OtherSize Term
u -> case Term
u of
      Var Int
i []  -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> OldSizeExpr
Rigid Int
i, Int
0)
      MetaV MetaId
m [Elim]
es | Just [Int]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Elim -> Maybe Int
isVar [Elim]
es, forall a. Ord a => [a] -> Bool
fastDistinct [Int]
xs
                -> forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
m [Int]
xs, Int
0)
      Term
_ -> forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
  where
    isVar :: Elim -> Maybe Int
isVar (Proj{})  = forall a. Maybe a
Nothing
    isVar (IApply Term
_ Term
_ Term
v) = Elim -> Maybe Int
isVar (forall a. Arg a -> Elim' a
Apply (forall a. a -> Arg a
defaultArg Term
v))
    isVar (Apply Arg Term
v) = case forall e. Arg e -> e
unArg Arg Term
v of
      Var Int
i [] -> forall a. a -> Maybe a
Just Int
i
      Term
_        -> forall a. Maybe a
Nothing

-- | Compute list of size metavariables with their arguments
--   appearing in a constraint.
flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
flexibleVariables (Leq OldSizeExpr
a Int
_ OldSizeExpr
b) = OldSizeExpr -> [(MetaId, [Int])]
flex OldSizeExpr
a forall a. [a] -> [a] -> [a]
++ OldSizeExpr -> [(MetaId, [Int])]
flex OldSizeExpr
b
  where
    flex :: OldSizeExpr -> [(MetaId, [Int])]
flex (Rigid Int
_)       = []
    flex (SizeMeta MetaId
m [Int]
xs) = [(MetaId
m, [Int]
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 :: OldSizeConstraint -> Maybe OldSizeConstraint
oldCanonicalizeSizeConstraint c :: OldSizeConstraint
c@(Leq OldSizeExpr
a Int
n OldSizeExpr
b) =
  case (OldSizeExpr
a,OldSizeExpr
b) of
    (Rigid{}, Rigid{})       -> forall (m :: * -> *) a. Monad m => a -> m a
return OldSizeConstraint
c
    (SizeMeta MetaId
m [Int]
xs, Rigid Int
i) -> do
      Int
j <- forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
i [Int]
xs
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
m [Int
0..forall a. Sized a => a -> Int
size [Int]
xsforall a. Num a => a -> a -> a
-Int
1]) Int
n (Int -> OldSizeExpr
Rigid Int
j)
    (Rigid Int
i, SizeMeta MetaId
m [Int]
xs) -> do
      Int
j <- forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
i [Int]
xs
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
Leq (Int -> OldSizeExpr
Rigid Int
j) Int
n (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
m [Int
0..forall a. Sized a => a -> Int
size [Int]
xsforall a. Num a => a -> a -> a
-Int
1])
    (SizeMeta MetaId
m [Int]
xs, SizeMeta MetaId
l [Int]
ys)
         -- try to invert xs on ys
       | Just [Int]
ys' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Int
y -> forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
y [Int]
xs) [Int]
ys ->
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
m [Int
0..forall a. Sized a => a -> Int
size [Int]
xsforall a. Num a => a -> a -> a
-Int
1]) Int
n (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
l [Int]
ys')
         -- try to invert ys on xs
       | Just [Int]
xs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Int
x -> forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
x [Int]
ys) [Int]
xs ->
           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
m [Int]
xs') Int
n (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
l [Int
0..forall a. Sized a => a -> Int
size [Int]
ysforall a. Num a => a -> a -> a
-Int
1])
         -- give up
       | Bool
otherwise -> forall a. Maybe a
Nothing