{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.SizedTypes where

import Prelude hiding (null)

import Control.Monad.Trans.Maybe ( MaybeT(..), runMaybeT )
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.Set as Set
import Data.Set (Set)

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Common.Pretty (Pretty)
import qualified Agda.Syntax.Common.Pretty as P

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Constraint () -- instance PrettyTCM Constraint
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (infer)
import {-# SOURCE #-} Agda.TypeChecking.Constraints () -- instance MonadConstraint TCM
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import Agda.TypeChecking.Conversion.Errors

import Agda.Utils.List as List
import Agda.Utils.List1 (pattern (:|))
import Agda.Utils.ListInf (ListInf, pattern (:<))
import Agda.Utils.ListInf qualified as ListInf
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Interaction.Options.ProfileOptions as Profile
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple

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 = TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCMT IO Bool
haveSizeLt (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    tel <- TCMT IO (Tele (Dom (Type'' Term Term)))
forall (m :: * -> *).
MonadTCEnv m =>
m (Tele (Dom (Type'' Term Term)))
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)
      ]
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size" Int
60 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"- raw type = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall a. Show a => a -> [Char]
show Term
t
  let postpone :: Blocker -> Term -> TCM ()
      postpone :: Blocker -> Term -> TCM ()
postpone Blocker
b Term
t = do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.lt" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"- postponing `not empty type of sizes' check for " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t ]
        Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
b (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Constraint
CheckSizeLtSat Term
t
  let ok :: TCM ()
      ok :: TCM ()
ok = [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.lt" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"- succeeded: not an empty type of sizes"
  Term
-> (Blocker -> Term -> TCM ())
-> (NotBlocked -> Term -> TCM ())
-> TCM ()
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 ((NotBlocked -> Term -> TCM ()) -> TCM ())
-> (NotBlocked -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
t -> do
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.lt" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"- type is not blocked"
    TCMT IO (Maybe BoundedSize)
-> TCM () -> (BoundedSize -> TCM ()) -> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Term -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Term -> m (Maybe BoundedSize)
isSizeType Term
t) TCM ()
ok ((BoundedSize -> TCM ()) -> TCM ())
-> (BoundedSize -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ BoundedSize
b -> do
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.lt" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
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
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.lt" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" - type is SIZELT" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
b
          Term
-> (Blocker -> Term -> TCM ())
-> (NotBlocked -> Term -> TCM ())
-> TCM ()
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) ((NotBlocked -> Term -> TCM ()) -> TCM ())
-> (NotBlocked -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
b -> do
            [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.lt" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
" - size bound is not blocked"
            Constraint -> TCM () -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Term -> Constraint
CheckSizeLtSat Term
t) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
              TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Term -> TCMT IO Bool
checkSizeNeverZero Term
b) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
                TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> TypeError
EmptyTypeOfSizes Term
t

-- | Precondition: Term is reduced and not blocked.
--   Throws a 'patternViolation' if undecided
checkSizeNeverZero :: Term -> TCM Bool
checkSizeNeverZero :: Term -> TCMT IO Bool
checkSizeNeverZero Term
u = do
  v <- Term -> TCMT IO SizeView
forall (m :: * -> *). HasBuiltins m => Term -> m SizeView
sizeView Term
u
  case v of
    SizeView
SizeInf     -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- OK, infty is never 0.
    SizeSuc{}   -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
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 -> TCMT IO Bool
checkSizeVarNeverZero Int
i
        -- neutral sizes cannot be guaranteed > 0
        Term
_ -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
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 -> TCMT IO Bool
checkSizeVarNeverZero Int
i = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checkSizeVarNeverZero" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> 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.
  ts <- (ContextEntry -> Type'' Term Term)
-> [ContextEntry] -> [Type'' Term Term]
forall a b. (a -> b) -> [a] -> [b]
map ContextEntry -> Type'' Term Term
ctxEntryType ([ContextEntry] -> [Type'' Term Term])
-> (Context' ContextEntry -> [ContextEntry])
-> Context' ContextEntry
-> [Type'' Term Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Context' ContextEntry -> [ContextEntry]
cxTake Int
i (Context' ContextEntry -> [Type'' Term Term])
-> TCMT IO (Context' ContextEntry) -> TCMT IO [Type'' Term Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Context' ContextEntry)
forall (m :: * -> *). MonadTCEnv m => m (Context' ContextEntry)
getContext
  -- If we encountered a blocking meta in the context, we cannot
  -- say ``no'' for sure.
  (n, blockers) <- runWriterT $ minSizeValAux ts $ ListInf.repeat 0
  let blocker = Set Blocker -> Blocker
unblockOnAll Set Blocker
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] -> ListInf Int -> WriterT (Set Blocker) TCM Int
  minSizeValAux :: [Type'' Term Term]
-> ListInf Int -> WriterT (Set Blocker) (TCMT IO) Int
minSizeValAux []       (Int
n :< ListInf Int
_) = Int -> WriterT (Set Blocker) (TCMT IO) Int
forall a. a -> WriterT (Set Blocker) (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
  minSizeValAux (Type'' Term Term
t : [Type'' Term Term]
ts) (Int
n :< ListInf Int
ns) = do
    [Char] -> Int -> TCMT IO Doc -> WriterT (Set Blocker) (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size" Int
60 (TCMT IO Doc -> WriterT (Set Blocker) (TCMT IO) ())
-> TCMT IO Doc -> WriterT (Set Blocker) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$
       [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"minSizeVal (n:ns) = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Int] -> [Char]
forall a. Show a => a -> [Char]
show (Int -> ListInf Int -> [Int]
forall n a. Integral n => n -> ListInf a -> [a]
ListInf.take ([Type'' Term Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type'' Term Term]
ts Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2) (ListInf Int -> [Int]) -> ListInf Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Int
n Int -> ListInf Int -> ListInf Int
forall a. a -> Infinite a -> Infinite a
:< ListInf Int
ns) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
             [Char]
" t =") TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Type'' Term Term -> [Char]) -> Type'' Term Term -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term -> [Char]
forall a. Show a => a -> [Char]
show) Type'' Term Term
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'' Term Term]
-> ListInf Int -> WriterT (Set Blocker) (TCMT IO) Int
minSizeValAux [Type'' Term Term]
ts ListInf Int
ns
        perhaps :: Blocker -> WriterT (Set Blocker) (TCMT IO) Int
perhaps Blocker
x = Set Blocker -> WriterT (Set Blocker) (TCMT IO) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Blocker -> Set Blocker
forall a. a -> Set a
Set.singleton Blocker
x) WriterT (Set Blocker) (TCMT IO) ()
-> WriterT (Set Blocker) (TCMT IO) Int
-> WriterT (Set Blocker) (TCMT IO) Int
forall a b.
WriterT (Set Blocker) (TCMT IO) a
-> WriterT (Set Blocker) (TCMT IO) b
-> WriterT (Set Blocker) (TCMT IO) b
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.
    Type'' Term Term
-> (Blocker
    -> Type'' Term Term -> WriterT (Set Blocker) (TCMT IO) Int)
-> (NotBlocked
    -> Type'' Term Term -> WriterT (Set Blocker) (TCMT IO) Int)
-> WriterT (Set Blocker) (TCMT IO) Int
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type'' Term Term
t (\ Blocker
x Type'' Term Term
_ -> Blocker -> WriterT (Set Blocker) (TCMT IO) Int
perhaps Blocker
x) ((NotBlocked
  -> Type'' Term Term -> WriterT (Set Blocker) (TCMT IO) Int)
 -> WriterT (Set Blocker) (TCMT IO) Int)
-> (NotBlocked
    -> Type'' Term Term -> WriterT (Set Blocker) (TCMT IO) Int)
-> WriterT (Set Blocker) (TCMT IO) Int
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type'' Term Term
t -> do
      WriterT (Set Blocker) (TCMT IO) (Maybe BoundedSize)
-> WriterT (Set Blocker) (TCMT IO) Int
-> (BoundedSize -> WriterT (Set Blocker) (TCMT IO) Int)
-> WriterT (Set Blocker) (TCMT IO) Int
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCMT IO (Maybe BoundedSize)
-> WriterT (Set Blocker) (TCMT IO) (Maybe BoundedSize)
forall a. TCM a -> WriterT (Set Blocker) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (Maybe BoundedSize)
 -> WriterT (Set Blocker) (TCMT IO) (Maybe BoundedSize))
-> TCMT IO (Maybe BoundedSize)
-> WriterT (Set Blocker) (TCMT IO) (Maybe BoundedSize)
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type'' Term Term -> m (Maybe BoundedSize)
isSizeType Type'' Term Term
t) WriterT (Set Blocker) (TCMT IO) Int
cont ((BoundedSize -> WriterT (Set Blocker) (TCMT IO) Int)
 -> WriterT (Set Blocker) (TCMT IO) Int)
-> (BoundedSize -> WriterT (Set Blocker) (TCMT IO) Int)
-> WriterT (Set Blocker) (TCMT IO) Int
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 -> Term
-> (Blocker -> Term -> WriterT (Set Blocker) (TCMT IO) Int)
-> (NotBlocked -> Term -> WriterT (Set Blocker) (TCMT IO) Int)
-> WriterT (Set Blocker) (TCMT IO) Int
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) ((NotBlocked -> Term -> WriterT (Set Blocker) (TCMT IO) Int)
 -> WriterT (Set Blocker) (TCMT IO) Int)
-> (NotBlocked -> Term -> WriterT (Set Blocker) (TCMT IO) Int)
-> WriterT (Set Blocker) (TCMT IO) Int
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
u -> do
            [Char] -> Int -> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size" Int
60 ([Char] -> WriterT (Set Blocker) (TCMT IO) ())
-> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"minSizeVal upper bound u = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall a. Show a => a -> [Char]
show Term
u
            v <- TCM DeepSizeView -> WriterT (Set Blocker) (TCMT IO) DeepSizeView
forall a. TCM a -> WriterT (Set Blocker) (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM DeepSizeView -> WriterT (Set Blocker) (TCMT IO) DeepSizeView)
-> TCM DeepSizeView -> WriterT (Set Blocker) (TCMT IO) DeepSizeView
forall a b. (a -> b) -> a -> b
$ Term -> TCM DeepSizeView
forall (m :: * -> *).
(PureTCM m, MonadTCError m) =>
Term -> m DeepSizeView
deepSizeView Term
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 Int
j []) Int
m -> do
                [Char] -> Int -> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size" Int
60 ([Char] -> WriterT (Set Blocker) (TCMT IO) ())
-> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"minSizeVal upper bound v = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DeepSizeView -> [Char]
forall a. Show a => a -> [Char]
show DeepSizeView
v
                let ns' :: ListInf Int
ns' = Int -> (Int -> Int) -> ListInf Int -> ListInf Int
forall n a. Integral n => n -> (a -> a) -> ListInf a -> ListInf a
ListInf.updateAt Int
j (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Int -> Int -> Int) -> Int -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m) ListInf Int
ns
                [Char] -> Int -> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size" Int
60 ([Char] -> WriterT (Set Blocker) (TCMT IO) ())
-> [Char] -> WriterT (Set Blocker) (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"minSizeVal ns' = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Int] -> [Char]
forall a. Show a => a -> [Char]
show (Int -> ListInf Int -> [Int]
forall n a. Integral n => n -> ListInf a -> [a]
ListInf.take ([Type'' Term Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type'' Term Term]
ts Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ListInf Int
ns')
                [Type'' Term Term]
-> ListInf Int -> WriterT (Set Blocker) (TCMT IO) Int
minSizeValAux [Type'' Term Term]
ts ListInf 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 = Type'' Term Term -> m BoundedSize
forall (m :: * -> *).
PureTCM m =>
Type'' Term Term -> m BoundedSize
isBoundedSizeType (Type'' Term Term -> m BoundedSize)
-> m (Type'' Term Term) -> m BoundedSize
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> m (Type'' Term Term)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Type'' Term Term)
typeOfBV Int
i

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

isBoundedSizeType :: PureTCM m => Type -> m BoundedSize
isBoundedSizeType :: forall (m :: * -> *).
PureTCM m =>
Type'' Term Term -> m BoundedSize
isBoundedSizeType Type'' Term Term
t =
  Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
t) m Term -> (Term -> m BoundedSize) -> m BoundedSize
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Def QName
x [Apply Arg Term
u] -> do
      sizelt <- BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSizeLt
      return $ if (Just (Def x []) == sizelt) then BoundedLt $ unArg u else BoundedNo
    Term
_ -> BoundedSize -> m BoundedSize
forall a. a -> m a
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
     , MonadAddContext m
     , HasBuiltins m
     )
  => Term -> Telescope -> Type -> m ()
boundedSizeMetaHook :: forall (m :: * -> *).
(MonadConstraint m, MonadAddContext m, HasBuiltins m) =>
Term -> Tele (Dom (Type'' Term Term)) -> Type'' Term Term -> m ()
boundedSizeMetaHook v :: Term
v@(MetaV MetaId
x [Elim]
_) Tele (Dom (Type'' Term Term))
tel0 Type'' Term Term
a = do
  res <- Type'' Term Term -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type'' Term Term -> m (Maybe BoundedSize)
isSizeType Type'' Term Term
a
  case res of
    Just (BoundedLt Term
u) -> do
      n <- m Int
forall (m :: * -> *). MonadTCEnv m => m Int
getContextSize
      let tel | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0     = ListTel -> Tele (Dom (Type'' Term Term))
telFromList (ListTel -> Tele (Dom (Type'' Term Term)))
-> ListTel -> Tele (Dom (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$ Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
drop Int
n (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom (Type'' Term Term))
tel0
              | Bool
otherwise = Tele (Dom (Type'' Term Term))
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
    Maybe BoundedSize
_ -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
boundedSizeMetaHook Term
_ Tele (Dom (Type'' Term Term))
_ Type'' Term Term
_ = m ()
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 ::
     Comparison -> CompareAs -> Term -> Term
  -> QName -> Elims -> QName -> Elims -> TCM ()
trySizeUniv :: Comparison
-> CompareAs
-> Term
-> Term
-> QName
-> [Elim]
-> QName
-> [Elim]
-> TCM ()
trySizeUniv Comparison
cmp CompareAs
t Term
m Term
n QName
x [Elim]
els1 QName
y [Elim]
els2 = do
  let failure :: forall a. TCM a
      failure :: forall a. TCM a
failure = Comparison -> Term -> Term -> CompareAs -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCError m, HasBuiltins m) =>
Comparison -> Term -> Term -> CompareAs -> m a
failConversion Comparison
cmp Term
m Term
n CompareAs
t
      forceInfty :: Arg Term -> TCM ()
forceInfty Arg Term
u = Comparison -> Term -> Term -> TCM ()
compareSizes Comparison
CmpEq (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u) (Term -> TCM ()) -> TCMT IO Term -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  -- Get the SIZE built-ins.
  (size, sizelt) <- TCMT IO (QName, QName)
-> ((QName, QName) -> TCMT IO (QName, QName))
-> Maybe (QName, QName)
-> TCMT IO (QName, QName)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO (QName, QName)
forall a. TCM a
failure (QName, QName) -> TCMT IO (QName, QName)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (QName, QName) -> TCMT IO (QName, QName))
-> TCMT IO (Maybe (QName, QName)) -> TCMT IO (QName, QName)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MaybeT (TCMT IO) (QName, QName) -> TCMT IO (Maybe (QName, QName))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do
    size   <- TCMT IO (Maybe QName) -> MaybeT (TCMT IO) QName
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe QName) -> MaybeT (TCMT IO) QName)
-> TCMT IO (Maybe QName) -> MaybeT (TCMT IO) QName
forall a b. (a -> b) -> a -> b
$ BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinSize
    sizelt <- MaybeT $ getBuiltinName' builtinSizeLt
    pure (size, sizelt)
  case (cmp, els1, els2) of
     -- Case @Size< _ <= Size@: true.
     (Comparison
CmpLeq, [Elim
_], [])  | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
size -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     -- Case @Size< u = Size@: forces @u = ∞@.
     (Comparison
_, [Apply Arg Term
u], []) | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
size -> Arg Term -> TCM ()
forceInfty Arg Term
u
     (Comparison
_, [], [Apply Arg Term
u]) | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
size Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt -> Arg Term -> TCM ()
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])
_                                             -> TCM ()
forall a. TCM 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
  inf <- BuiltinId -> m QName
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m QName
getBuiltinName_ BuiltinId
builtinSizeInf
  suc <- getBuiltinName_ builtinSizeSuc
  let loop Term
v =
        Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v m Term -> (Term -> m DeepSizeView) -> m DeepSizeView
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Def QName
x []        | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
inf -> DeepSizeView -> m DeepSizeView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
forall a b. (a -> b) -> a -> b
$ DeepSizeView
DSizeInf
          Def QName
x [Apply Arg Term
u] | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
suc -> QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ QName
suc (DeepSizeView -> DeepSizeView) -> m DeepSizeView -> m DeepSizeView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m DeepSizeView
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u)

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

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

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

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

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

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

compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> TCM ()
compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> TCM ()
compareSizeViews Comparison
cmp DeepSizeView
s1' DeepSizeView
s2' = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
    [ TCMT IO Doc
"compareSizeViews"
    , DeepSizeView -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeepSizeView
s1'
    , Comparison -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Comparison
cmp
    , DeepSizeView -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeepSizeView
s2'
    ]
  size <- TCMT IO (Type'' Term Term)
forall (m :: * -> *). HasBuiltins m => m (Type'' Term Term)
sizeType
  let (s1, s2) = removeSucs (s1', s2')
      withUnView Term -> Term -> TCM ()
cont = do
        u <- DeepSizeView -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s1
        v <- unDeepSizeView s2
        cont u v
      failure = (Term -> Term -> TCM ()) -> TCM ()
withUnView ((Term -> Term -> TCM ()) -> TCM ())
-> (Term -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Term
u Term
v -> Comparison -> Term -> Term -> CompareAs -> TCM ()
forall (m :: * -> *) a.
(MonadTCError m, HasBuiltins m) =>
Comparison -> Term -> Term -> CompareAs -> m a
failConversion Comparison
cmp Term
u Term
v CompareAs
AsSizes
      continue Comparison
cmp = (Term -> Term -> TCM ()) -> TCM ()
withUnView ((Term -> Term -> TCM ()) -> TCM ())
-> (Term -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> TCM ()
compareAtom Comparison
cmp CompareAs
AsSizes
  case (cmp, s1, s2) of
    (Comparison
CmpLeq, DeepSizeView
_,            DeepSizeView
DSizeInf)   -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Comparison
CmpEq,  DeepSizeView
DSizeInf,     DeepSizeView
DSizeInf)   -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Comparison
CmpEq,  DSizeVar{},   DeepSizeView
DSizeInf)   -> TCM ()
failure
    (Comparison
_    ,  DeepSizeView
DSizeInf,     DSizeVar{}) -> TCM ()
failure
    (Comparison
_    ,  DeepSizeView
DSizeInf,     DeepSizeView
_         ) -> Comparison -> TCM ()
continue Comparison
CmpEq
    (Comparison
CmpLeq, DSizeVar ProjectedVar
i Int
n, DSizeVar ProjectedVar
j Int
m) | ProjectedVar
i ProjectedVar -> ProjectedVar -> Bool
forall a. Eq a => a -> a -> Bool
== ProjectedVar
j -> Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
m) TCM ()
failure
    (Comparison
CmpLeq, DSizeVar ProjectedVar
i Int
n, DSizeVar ProjectedVar
j Int
m) | ProjectedVar
i ProjectedVar -> ProjectedVar -> Bool
forall a. Eq a => a -> a -> Bool
/= ProjectedVar
j -> do
       res <- ProjectedVar -> TCM BoundedSize
isBoundedProjVar ProjectedVar
i
       case res of
         BoundedSize
BoundedNo -> TCM ()
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
            v <- DeepSizeView -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s2
            if n > 0 then do
              u'' <- sizeSuc (n - 1) u'
              compareSizes cmp u'' v
             else compareSizes cmp u' =<< sizeSuc 1 v
    (Comparison
CmpLeq, DeepSizeView
s1,        DeepSizeView
s2)         -> (Term -> Term -> TCM ()) -> TCM ()
withUnView ((Term -> Term -> TCM ()) -> TCM ())
-> (Term -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Term
u Term
v -> do
      TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Term -> Term -> TCMT IO Bool
trivial Term
u Term
v) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Type'' Term Term -> Term -> Term -> TCM ()
giveUp Comparison
CmpLeq Type'' Term Term
size Term
u Term
v
    (Comparison
CmpEq, DeepSizeView
s1, DeepSizeView
s2) -> Comparison -> TCM ()
continue Comparison
cmp

-- | If 'envAssignMetas' then postpone as constraint, otherwise, fail hard.
--   Failing is required if we speculatively test several alternatives.
giveUp :: Comparison -> Type -> Term -> Term -> TCM ()
giveUp :: Comparison -> Type'' Term Term -> Term -> Term -> TCM ()
giveUp Comparison
cmp Type'' Term Term
size Term
u Term
v =
  TCMT IO Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eAssignMetas)
    {-then-} (do
      -- TODO: compute proper blocker
      unblock <- [Term] -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn ([Term] -> Blocker) -> TCMT IO [Term] -> TCMT IO Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term] -> TCMT IO [Term]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull [Term
u, Term
v]
      addConstraint unblock $ ValueCmp CmpLeq AsSizes u v)
    {-else-} (Comparison -> Term -> Term -> CompareAs -> TCM ()
forall (m :: * -> *) a.
(MonadTCError m, HasBuiltins m) =>
Comparison -> Term -> Term -> CompareAs -> m a
failConversion Comparison
cmp Term
u Term
v CompareAs
AsSizes)

-- | Checked whether a size constraint is trivial (like @X <= X+1@).
trivial :: Term -> Term -> TCM Bool
trivial :: Term -> Term -> TCMT IO Bool
trivial Term
u Term
v = do
    a@(e , n ) <- Term -> TCM (OldSizeExpr, Int)
oldSizeExpr Term
u
    b@(e', n') <- oldSizeExpr v
    let triv = OldSizeExpr
e OldSizeExpr -> OldSizeExpr -> Bool
forall a. Eq a => a -> a -> Bool
== OldSizeExpr
e' Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
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
  TCMT IO Bool -> (TCErr -> TCMT IO Bool) -> TCMT IO Bool
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
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
  test <- m (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
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 :: forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
(Comparison -> Bool) -> Closure Constraint -> m Bool
isSizeConstraint Comparison -> Bool
p Closure Constraint
c = m (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest m (Term -> Maybe BoundedSize)
-> ((Term -> Maybe BoundedSize) -> Bool) -> m Bool
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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'' Term Term -> Bool)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
isSizeConstraint_ ((Type'' Term Term -> Bool)
 -> (Comparison -> Bool) -> Closure Constraint -> Bool)
-> (Type'' Term Term -> Bool)
-> (Comparison -> Bool)
-> Closure Constraint
-> Bool
forall a b. (a -> b) -> a -> b
$ Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool)
-> (Type'' Term Term -> Maybe BoundedSize)
-> Type'' Term Term
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe BoundedSize
test (Term -> Maybe BoundedSize)
-> (Type'' Term Term -> Term)
-> Type'' Term Term
-> Maybe BoundedSize
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term -> Term
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'' Term Term -> Bool)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
isSizeConstraint_ Type'' Term Term -> 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'' Term Term -> Bool
isSizeType Comparison -> Bool
p Closure{ clValue :: forall a. Closure a -> a
clValue = ValueCmp Comparison
cmp (AsTermsOf Type'' Term Term
s) Term
_ Term
_ } = Comparison -> Bool
p Comparison
cmp Bool -> Bool -> Bool
&& Type'' Term Term -> Bool
isSizeType Type'' Term Term
s
isSizeConstraint_ Type'' Term Term -> 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 [ProblemConstraint]
takeSizeConstraints Comparison -> Bool
p = do
  test <- TCMT IO (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  takeConstraints (mkIsSizeConstraint test p . theConstraint)

-- | Find the size constraints of the matching direction.
getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
getSizeConstraints :: (Comparison -> Bool) -> TCM [ProblemConstraint]
getSizeConstraints Comparison -> Bool
p = do
  test <- TCMT IO (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  filter (mkIsSizeConstraint test p . theConstraint) <$> getAllConstraints

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

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

instance Pretty OldSizeConstraint where
  pretty :: OldSizeConstraint -> Doc
pretty (Leq OldSizeExpr
a Int
n OldSizeExpr
b)
    | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc
"=<" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0     = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc
"=<" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc
"+" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> [Char] -> Doc
forall a. [Char] -> Doc a
P.text (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
    | Bool
otherwise = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc
"+" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> [Char] -> Doc
forall a. [Char] -> Doc a
P.text (Int -> [Char]
forall a. Show a => a -> [Char]
show (-Int
n)) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Doc
"=<" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> OldSizeExpr -> Doc
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 :: [ProblemConstraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [] = [OldSizeConstraint] -> TCM [OldSizeConstraint]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- special case to avoid maximum []
oldComputeSizeConstraints [ProblemConstraint]
cs = [Maybe OldSizeConstraint] -> [OldSizeConstraint]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe OldSizeConstraint] -> [OldSizeConstraint])
-> TCMT IO [Maybe OldSizeConstraint] -> TCM [OldSizeConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint -> TCMT IO (Maybe OldSizeConstraint))
-> [Constraint] -> TCMT IO [Maybe OldSizeConstraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Constraint -> TCMT IO (Maybe OldSizeConstraint)
oldComputeSizeConstraint [Constraint]
leqs
  where
    -- get the constraints plus contexts they are defined in
    gammas :: [Context' ContextEntry]
gammas       = (ProblemConstraint -> Context' ContextEntry)
-> [ProblemConstraint] -> [Context' ContextEntry]
forall a b. (a -> b) -> [a] -> [b]
map' (Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
-> TCEnv -> Context' ContextEntry
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext (TCEnv -> Context' ContextEntry)
-> (ProblemConstraint -> TCEnv)
-> ProblemConstraint
-> Context' ContextEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv (Closure Constraint -> TCEnv)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) [ProblemConstraint]
cs
    ls :: [Constraint]
ls           = (ProblemConstraint -> Constraint)
-> [ProblemConstraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map' (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) [ProblemConstraint]
cs
    -- compute the longest context (common water level)
    ns :: [Int]
ns           = (Context' ContextEntry -> Int) -> [Context' ContextEntry] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' Context' ContextEntry -> Int
forall a. Sized a => a -> Int
size [Context' ContextEntry]
gammas
    waterLevel :: Int
waterLevel   = [Int] -> Int
forall a. Ord a => [a] -> a
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 = (Int -> Constraint -> Constraint)
-> [Int] -> [Constraint] -> [Constraint]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Constraint -> Constraint
forall a. Subst a => Int -> a -> a
raise ((Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int
waterLevel Int -> Int -> Int
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 -> TCMT IO (Maybe OldSizeConstraint)
oldComputeSizeConstraint Constraint
c =
  case Constraint
c of
    ValueCmp Comparison
CmpLeq CompareAs
_ Term
u Term
v -> do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"converting size constraint"
          , Constraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Constraint -> m Doc
prettyTCM Constraint
c
          ]
        (a, n) <- Term -> TCM (OldSizeExpr, Int)
oldSizeExpr Term
u
        (b, m) <- oldSizeExpr v
        return $ Just $ Leq a (m - n) b
      TCMT IO (Maybe OldSizeConstraint)
-> (TCErr -> TCMT IO (Maybe OldSizeConstraint))
-> TCMT IO (Maybe OldSizeConstraint)
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> case TCErr
err of
        PatternErr{} -> Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe OldSizeConstraint
forall a. Maybe a
Nothing
        TCErr
_            -> TCErr -> TCMT IO (Maybe OldSizeConstraint)
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
    Constraint
_ -> TCMT IO (Maybe OldSizeConstraint)
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 :: Term -> TCM (OldSizeExpr, Int)
oldSizeExpr :: Term -> TCM (OldSizeExpr, Int)
oldSizeExpr Term
u = do
  u <- Term -> TCMT IO Term
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.
  reportSDoc "tc.conv.size" 60 $ "oldSizeExpr:" <+> prettyTCM u
  s <- sizeView u
  case s of
    SizeView
SizeInf     -> Blocker -> TCM (OldSizeExpr, Int)
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
    SizeSuc Term
u   -> (Int -> Int) -> (OldSizeExpr, Int) -> (OldSizeExpr, Int)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ((OldSizeExpr, Int) -> (OldSizeExpr, Int))
-> TCM (OldSizeExpr, Int) -> TCM (OldSizeExpr, Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (OldSizeExpr, Int)
oldSizeExpr Term
u
    OtherSize Term
u -> case Term
u of
      Var Int
i []  -> (OldSizeExpr, Int) -> TCM (OldSizeExpr, Int)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> OldSizeExpr
Rigid Int
i, Int
0)
      MetaV MetaId
m [Elim]
es | Just [Int]
xs <- (Elim -> Maybe Int) -> [Elim] -> Maybe [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim -> Maybe Int
isVar [Elim]
es, [Int] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [Int]
xs
                -> (OldSizeExpr, Int) -> TCM (OldSizeExpr, Int)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
m [Int]
xs, Int
0)
      Term
_ -> Blocker -> TCM (OldSizeExpr, Int)
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
  where
    isVar :: Elim -> Maybe Int
isVar (Proj{})  = Maybe Int
forall a. Maybe a
Nothing
    isVar (IApply Term
_ Term
_ Term
v) = Elim -> Maybe Int
isVar (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v))
    isVar (Apply Arg Term
v) = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v of
      Var Int
i [] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
      Term
_        -> Maybe Int
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 [(MetaId, [Int])] -> [(MetaId, [Int])] -> [(MetaId, [Int])]
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{})       -> OldSizeConstraint -> Maybe OldSizeConstraint
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return OldSizeConstraint
c
    (SizeMeta MetaId
m [Int]
xs, Rigid Int
i) -> do
      j <- Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
i [Int]
xs
      return $ Leq (SizeMeta m [0..size xs-1]) n (Rigid j)
    (Rigid Int
i, SizeMeta MetaId
m [Int]
xs) -> do
      j <- Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
i [Int]
xs
      return $ Leq (Rigid j) n (SizeMeta m [0..size xs-1])
    (SizeMeta MetaId
m [Int]
xs, SizeMeta MetaId
l [Int]
ys)
         -- try to invert xs on ys
       | Just [Int]
ys' <- (Int -> Maybe Int) -> [Int] -> Maybe [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ Int
y -> Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
y [Int]
xs) [Int]
ys ->
           OldSizeConstraint -> Maybe OldSizeConstraint
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
m [Int
0..[Int] -> Int
forall a. Sized a => a -> Int
size [Int]
xsInt -> Int -> Int
forall 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' <- (Int -> Maybe Int) -> [Int] -> Maybe [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ Int
x -> Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
x [Int]
ys) [Int]
xs ->
           OldSizeConstraint -> Maybe OldSizeConstraint
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
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..[Int] -> Int
forall a. Sized a => a -> Int
size [Int]
ysInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1])
         -- give up
       | Bool
otherwise -> Maybe OldSizeConstraint
forall a. Maybe a
Nothing