{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.SizedTypes where

import Prelude hiding (null)

import Control.Monad.Except
import Control.Monad.Writer

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

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

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

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

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

import Agda.Utils.Impossible

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

-- | Check whether a type is either not a SIZELT or a SIZELT that is non-empty.
checkSizeLtSat :: Term -> TCM ()
checkSizeLtSat :: 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
    Telescope
tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
    [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
      [ TCMT IO Doc
"checking that " 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
prettyTCM Term
t TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is not an empty type of sizes"
      , if Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel then TCMT IO Doc
forall a. Null a => a
empty else do
        TCMT IO Doc
"in context " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
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
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)
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
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 ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
                  TCMT IO Doc
"Possibly empty type of sizes " 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
prettyTCM 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
  SizeView
v <- Term -> TCMT IO SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
  case SizeView
v of
    SizeView
SizeInf     -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- OK, infty is never 0.
    SizeSuc{}   -> Bool -> TCMT IO Bool
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 (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
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 <- (Dom' Term (Name, Type) -> Type) -> Context -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) (Context -> [Type]) -> (Context -> Context) -> Context -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Context -> Context
forall a. Int -> [a] -> [a]
take Int
i (Context -> [Type]) -> TCMT IO Context -> TCMT IO [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Context
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) <- WriterT (Set Blocker) (TCMT IO) Int -> TCMT IO (Int, Set Blocker)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT (Set Blocker) (TCMT IO) Int -> TCMT IO (Int, Set Blocker))
-> WriterT (Set Blocker) (TCMT IO) Int
-> TCMT IO (Int, Set Blocker)
forall a b. (a -> b) -> a -> b
$ [Type] -> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
minSizeValAux [Type]
ts ([Int] -> WriterT (Set Blocker) (TCMT IO) Int)
-> [Int] -> WriterT (Set Blocker) (TCMT IO) Int
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. a -> [a]
repeat Int
0
  let blocker :: Blocker
blocker = Set Blocker -> Blocker
unblockOnAll Set Blocker
blockers
  if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else
    if Blocker
blocker Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock
      then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      else Blocker -> TCMT IO Bool
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]
_        []      = WriterT (Set Blocker) (TCMT IO) Int
forall a. HasCallStack => a
__IMPOSSIBLE__
  minSizeValAux []       (Int
n : [Int]
_) = Int -> WriterT (Set Blocker) (TCMT IO) Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
  minSizeValAux (Type
t : [Type]
ts) (Int
n : [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 -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Int
nInt -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[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 -> [Char]) -> Type -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Char]
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 = 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 (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
-> (Blocker -> Type -> WriterT (Set Blocker) (TCMT IO) Int)
-> (NotBlocked -> Type -> 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
t (\ Blocker
x Type
_ -> Blocker -> WriterT (Set Blocker) (TCMT IO) Int
perhaps Blocker
x) ((NotBlocked -> Type -> WriterT (Set Blocker) (TCMT IO) Int)
 -> WriterT (Set Blocker) (TCMT IO) Int)
-> (NotBlocked -> Type -> WriterT (Set Blocker) (TCMT IO) Int)
-> WriterT (Set Blocker) (TCMT IO) Int
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
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 (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 -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
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
            DeepSizeView
v <- TCM DeepSizeView -> WriterT (Set Blocker) (TCMT IO) DeepSizeView
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 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
                [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' :: [Int]
ns' = Int -> (Int -> Int) -> [Int] -> [Int]
forall a. Int -> (a -> a) -> [a] -> [a]
List.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
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
m) [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 -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts Int -> Int -> Int
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 = Type -> m BoundedSize
forall (m :: * -> *). PureTCM m => Type -> m BoundedSize
isBoundedSizeType (Type -> m BoundedSize) -> m Type -> m BoundedSize
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> m Type
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 = Type -> m BoundedSize
forall (m :: * -> *). PureTCM m => Type -> m BoundedSize
isBoundedSizeType (Type -> m BoundedSize) -> m Type -> m BoundedSize
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> m Type
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 =
  Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) m Term -> (Term -> m BoundedSize) -> m BoundedSize
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 <- [Char] -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getBuiltin' [Char]
builtinSizeLt
      BoundedSize -> m BoundedSize
forall (m :: * -> *) a. Monad m => a -> m a
return (BoundedSize -> m BoundedSize) -> BoundedSize -> m BoundedSize
forall a b. (a -> b) -> a -> b
$ if (Term -> Maybe Term
forall a. a -> Maybe a
Just (QName -> [Elim] -> Term
Def QName
x []) Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Term
sizelt) then Term -> BoundedSize
BoundedLt (Term -> BoundedSize) -> Term -> BoundedSize
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u else BoundedSize
BoundedNo
    Term
_ -> BoundedSize -> m BoundedSize
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 <- Type -> m (Maybe BoundedSize)
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 <- m Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
      let tel :: Telescope
tel | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0     = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
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
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel0
              | Bool
otherwise = Telescope
tel0
      Telescope -> m () -> m ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        Term
v <- Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel
        -- compareSizes CmpLeq v u
        Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (MetaId -> Blocker
unblockOnMeta MetaId
x) (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpLeq CompareAs
AsSizes Term
v Term
u
    Maybe BoundedSize
_ -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
boundedSizeMetaHook Term
_ Telescope
_ Type
_ = 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
  :: 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 = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
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 = Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
CmpEq (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u) (Term -> m ()) -> m Term -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  -- Get the SIZE built-ins.
  (QName
size, QName
sizelt) <- (m (QName, QName)
 -> (TCErr -> m (QName, QName)) -> m (QName, QName))
-> (TCErr -> m (QName, QName))
-> m (QName, QName)
-> m (QName, QName)
forall a b c. (a -> b -> c) -> b -> a -> c
flip m (QName, QName) -> (TCErr -> m (QName, QName)) -> m (QName, QName)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (m (QName, QName) -> TCErr -> m (QName, QName)
forall a b. a -> b -> a
const m (QName, QName)
forall (m :: * -> *) a. MonadTCError m => m a
failure) (m (QName, QName) -> m (QName, QName))
-> m (QName, QName) -> m (QName, QName)
forall a b. (a -> b) -> a -> b
$ do
     Def QName
size   [Elim]
_ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
     Def QName
sizelt [Elim]
_ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeLt
     (QName, QName) -> m (QName, QName)
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 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 -> () -> m ()
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 -> m ()
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 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 -> m ()
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])
_                                             -> m ()
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 [] <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  Def QName
suc [] <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
  let loop :: Term -> m DeepSizeView
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 (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 (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)
mapM Elim -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim [Elim]
es
                                     -> DeepSizeView -> m DeepSizeView
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 (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 (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
  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 <- [Char] -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinDefName [Char]
builtinSizeInf
  Maybe QName
suc <- [Char] -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinDefName [Char]
builtinSizeSuc
  Maybe QName
max <- [Char] -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe QName)
getBuiltinDefName [Char]
builtinSizeMax
  let loop :: Term -> m SizeMaxView
loop Term
v = do
        Term
v <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
        case Term
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 -> SizeMaxView -> m SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> m SizeMaxView) -> SizeMaxView -> m SizeMaxView
forall a b. (a -> b) -> a -> b
$ DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
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 -> SizeMaxView -> SizeMaxView
maxViewSuc_ (Maybe QName -> QName
forall a. HasCallStack => Maybe a -> a
fromJust Maybe QName
suc) (SizeMaxView -> SizeMaxView) -> m SizeMaxView -> m SizeMaxView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m SizeMaxView
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 -> SizeMaxView -> SizeMaxView -> SizeMaxView
maxViewMax (SizeMaxView -> SizeMaxView -> SizeMaxView)
-> m SizeMaxView -> m (SizeMaxView -> SizeMaxView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m SizeMaxView
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u1) m (SizeMaxView -> SizeMaxView) -> m SizeMaxView -> m SizeMaxView
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m SizeMaxView
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)
mapM Elim -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim [Elim]
es
                                        -> SizeMaxView -> m SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> m SizeMaxView) -> SizeMaxView -> m SizeMaxView
forall a b. (a -> b) -> a -> b
$ DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
forall a b. (a -> b) -> a -> b
$ ProjectedVar -> Int -> DeepSizeView
DSizeVar ProjectedVar
pv Int
0
          MetaV MetaId
x [Elim]
us                    -> SizeMaxView -> m SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> m SizeMaxView) -> SizeMaxView -> m SizeMaxView
forall a b. (a -> b) -> a -> b
$ DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
forall a b. (a -> b) -> a -> b
$ MetaId -> [Elim] -> Int -> DeepSizeView
DSizeMeta MetaId
x [Elim]
us Int
0
          Term
_                             -> SizeMaxView -> m SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> m SizeMaxView) -> SizeMaxView -> m SizeMaxView
forall a b. (a -> b) -> a -> b
$ DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
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 = [Char] -> Int -> [Char] -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.conv.size" Int
10 [Char]
"compareSizes" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
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
prettyTCM Comparison
cmp
                   , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
                   ]
    ]
  [Char] -> Int -> m () -> m ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.conv.size" Int
60 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    Term
u <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
    Term
v <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
    [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      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 (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty 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
prettyTCM Comparison
cmp
                   , Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
                   ]
  SizeMaxView
us <- Term -> m SizeMaxView
forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
sizeMaxView Term
u
  SizeMaxView
vs <- Term -> m SizeMaxView
forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
sizeMaxView Term
v
  Comparison -> SizeMaxView -> SizeMaxView -> m ()
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]
_)) -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  (Comparison
cmp, DeepSizeView
u:|[], DeepSizeView
v:|[]) -> Comparison -> DeepSizeView -> DeepSizeView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
cmp DeepSizeView
u DeepSizeView
v
  (Comparison
CmpLeq, SizeMaxView
us, DeepSizeView
v:|[]) -> SizeMaxView -> (DeepSizeView -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Fold.forM_ SizeMaxView
us ((DeepSizeView -> m ()) -> m ()) -> (DeepSizeView -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ DeepSizeView
u -> Comparison -> DeepSizeView -> DeepSizeView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
cmp DeepSizeView
u DeepSizeView
v
  (Comparison
CmpLeq, SizeMaxView
us, SizeMaxView
vs)    -> SizeMaxView -> (DeepSizeView -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Fold.forM_ SizeMaxView
us ((DeepSizeView -> m ()) -> m ()) -> (DeepSizeView -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ DeepSizeView
u -> DeepSizeView -> SizeMaxView -> m ()
forall (m :: * -> *).
MonadConversion m =>
DeepSizeView -> SizeMaxView -> m ()
compareBelowMax DeepSizeView
u SizeMaxView
vs
  (Comparison
CmpEq,  SizeMaxView
us, SizeMaxView
vs)    -> do
    Comparison -> SizeMaxView -> SizeMaxView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> SizeMaxView -> SizeMaxView -> m ()
compareMaxViews Comparison
CmpLeq SizeMaxView
us SizeMaxView
vs
    Comparison -> SizeMaxView -> SizeMaxView -> m ()
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 = [Char] -> Int -> [Char] -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.conv.size" Int
45 [Char]
"compareBelowMax" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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
    , SizeMaxView -> TCMT IO Doc
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.
  m () -> m () -> m ()
forall {e} {m :: * -> *} {a}. MonadError e m => m a -> m a -> m a
alt (m () -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ (m () -> m () -> m ()) -> NonEmpty (m ()) -> m ()
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
Fold.foldr1 m () -> m () -> m ()
forall {e} {m :: * -> *} {a}. MonadError e m => m a -> m a -> m a
alt (NonEmpty (m ()) -> m ()) -> NonEmpty (m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ (DeepSizeView -> m ()) -> SizeMaxView -> NonEmpty (m ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Comparison -> DeepSizeView -> DeepSizeView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
CmpLeq DeepSizeView
u) SizeMaxView
vs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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"
      ]
    Term
u <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
u
    Term
v <- SizeMaxView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
SizeMaxView -> m Term
unMaxView SizeMaxView
vs
    Type
size <- m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
    Comparison -> Type -> Term -> Term -> m ()
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 m a -> (e -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` m a -> e -> m a
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
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
45 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
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'
    ]
  Type
size <- m Type
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 <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s1
        Term
v <- DeepSizeView -> m Term
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 ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Term
u Term
v -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
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 ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> m ()
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)   -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Comparison
CmpEq,  DeepSizeView
DSizeInf,     DeepSizeView
DSizeInf)   -> () -> m ()
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 ProjectedVar -> ProjectedVar -> Bool
forall a. Eq a => a -> a -> Bool
== ProjectedVar
j -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
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 ProjectedVar -> ProjectedVar -> Bool
forall a. Eq a => a -> a -> Bool
/= ProjectedVar
j -> do
       BoundedSize
res <- ProjectedVar -> m BoundedSize
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 <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s2
            if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then do
              Term
u'' <- Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Term
u'
              Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u'' Term
v
             else Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u' (Term -> m ()) -> m Term -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 Term
v
    (Comparison
CmpLeq, DeepSizeView
s1,        DeepSizeView
s2)         -> (Term -> Term -> m ()) -> m ()
withUnView ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Term
u Term
v -> do
      m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Term -> Term -> m Bool
forall (m :: * -> *). MonadConversion m => Term -> Term -> m Bool
trivial Term
u Term
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Type -> Term -> Term -> m ()
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 =
  m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas)
    {-then-} (Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
unblock (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpLeq CompareAs
AsSizes Term
u Term
v)
    {-else-} (TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
u Term
v CompareAs
AsSizes)
  where
    unblock :: Blocker
unblock = [Term] -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn [Term
u, Term
v]

-- | 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 ) <- Term -> m (OldSizeExpr, Int)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
u
    b :: (OldSizeExpr, Int)
b@(OldSizeExpr
e', Int
n') <- Term -> m (OldSizeExpr, Int)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
v
    let triv :: Bool
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
    [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      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 [ if Bool
triv then TCMT IO Doc
"trivial constraint" else TCMT IO Doc
forall a. Null a => a
empty
                   , (OldSizeExpr, Int) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (OldSizeExpr, Int)
a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"<="
                   , (OldSizeExpr, Int) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (OldSizeExpr, Int)
b
                   ]
    Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
triv
  m Bool -> (TCErr -> m Bool) -> m Bool
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> Bool -> m Bool
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 <- m (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  (ProblemConstraint -> Bool) -> [ProblemConstraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test (Bool -> Comparison -> Bool
forall a b. a -> b -> a
const Bool
True) (Closure Constraint -> Bool)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) ([ProblemConstraint] -> Bool) -> m [ProblemConstraint] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProblemId -> m [ProblemConstraint]
forall (m :: * -> *).
ReadTCState m =>
ProblemId -> m [ProblemConstraint]
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 = 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 (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_ ((Type -> Bool)
 -> (Comparison -> Bool) -> Closure Constraint -> Bool)
-> (Type -> 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 -> Maybe BoundedSize) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe BoundedSize
test (Term -> Maybe BoundedSize)
-> (Type -> Term) -> Type -> Maybe BoundedSize
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> 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 -> 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 [ProblemConstraint]
takeSizeConstraints Comparison -> Bool
p = do
  Term -> Maybe BoundedSize
test <- TCMT IO (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  (ProblemConstraint -> Bool) -> TCM [ProblemConstraint]
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m [ProblemConstraint]
takeConstraints ((Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test Comparison -> Bool
p (Closure Constraint -> Bool)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Bool
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 [ProblemConstraint]
getSizeConstraints Comparison -> Bool
p = do
  Term -> Maybe BoundedSize
test <- TCMT IO (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  (ProblemConstraint -> Bool)
-> [ProblemConstraint] -> [ProblemConstraint]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test Comparison -> Bool
p (Closure Constraint -> Bool)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) ([ProblemConstraint] -> [ProblemConstraint])
-> TCM [ProblemConstraint] -> TCM [ProblemConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
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 <- TCMT IO (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
  [Maybe (MetaId, Type, Telescope)] -> [(MetaId, Type, Telescope)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (MetaId, Type, Telescope)] -> [(MetaId, Type, Telescope)])
-> TCMT IO [Maybe (MetaId, Type, Telescope)]
-> TCM [(MetaId, Type, Telescope)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas TCMT IO [MetaId]
-> ([MetaId] -> TCMT IO [Maybe (MetaId, Type, Telescope)])
-> TCMT IO [Maybe (MetaId, Type, Telescope)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= do
      (MetaId -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> [MetaId] -> TCMT IO [Maybe (MetaId, Type, Telescope)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((MetaId -> TCMT IO (Maybe (MetaId, Type, Telescope)))
 -> [MetaId] -> TCMT IO [Maybe (MetaId, Type, Telescope)])
-> (MetaId -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> [MetaId]
-> TCMT IO [Maybe (MetaId, Type, Telescope)]
forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> do
        let no :: TCMT IO (Maybe a)
no = Maybe a -> TCMT IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
        MetaVariable
mi <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
        case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mi of
          Judgement MetaId
_ | BlockedConst{} <- MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mi -> TCMT IO (Maybe (MetaId, Type, Telescope))
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 <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
            -- b is reduced
            Maybe BoundedSize
-> TCMT IO (Maybe (MetaId, Type, Telescope))
-> (BoundedSize -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> TCMT IO (Maybe (MetaId, Type, Telescope))
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Term -> Maybe BoundedSize
test (Term -> Maybe BoundedSize) -> Term -> Maybe BoundedSize
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
b) TCMT IO (Maybe (MetaId, Type, Telescope))
forall {a}. TCMT IO (Maybe a)
no ((BoundedSize -> TCMT IO (Maybe (MetaId, Type, Telescope)))
 -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> (BoundedSize -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> TCMT IO (Maybe (MetaId, Type, Telescope))
forall a b. (a -> b) -> a -> b
$ \ BoundedSize
_ -> do
              let yes :: TCMT IO (Maybe (MetaId, Type, Telescope))
yes = Maybe (MetaId, Type, Telescope)
-> TCMT IO (Maybe (MetaId, Type, Telescope))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (MetaId, Type, Telescope)
 -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> Maybe (MetaId, Type, Telescope)
-> TCMT IO (Maybe (MetaId, Type, Telescope))
forall a b. (a -> b) -> a -> b
$ (MetaId, Type, Telescope) -> Maybe (MetaId, Type, Telescope)
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
                TCMT IO Bool
-> TCMT IO (Maybe (MetaId, Type, Telescope))
-> TCMT IO (Maybe (MetaId, Type, Telescope))
-> TCMT IO (Maybe (MetaId, Type, Telescope))
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, Telescope))
forall {a}. TCMT IO (Maybe a)
no TCMT IO (Maybe (MetaId, Type, Telescope))
yes
          Judgement MetaId
_ -> TCMT IO (Maybe (MetaId, Type, Telescope))
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
/= :: OldSizeExpr -> OldSizeExpr -> Bool
$c/= :: OldSizeExpr -> OldSizeExpr -> Bool
== :: OldSizeExpr -> OldSizeExpr -> Bool
$c== :: 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
showList :: [OldSizeExpr] -> [Char] -> [Char]
$cshowList :: [OldSizeExpr] -> [Char] -> [Char]
show :: OldSizeExpr -> [Char]
$cshow :: OldSizeExpr -> [Char]
showsPrec :: Int -> OldSizeExpr -> [Char] -> [Char]
$cshowsPrec :: Int -> OldSizeExpr -> [Char] -> [Char]
Show)

instance Pretty OldSizeExpr where
  pretty :: OldSizeExpr -> Doc
pretty (SizeMeta MetaId
m [Int]
_) = [Char] -> Doc
P.text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"X" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (MetaId -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral MetaId
m :: Int)
  pretty (Rigid Int
i)      = [Char] -> Doc
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
showList :: [OldSizeConstraint] -> [Char] -> [Char]
$cshowList :: [OldSizeConstraint] -> [Char] -> [Char]
show :: OldSizeConstraint -> [Char]
$cshow :: OldSizeConstraint -> [Char]
showsPrec :: Int -> OldSizeConstraint -> [Char] -> [Char]
$cshowsPrec :: Int -> 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
P.<+> Doc
"=<" Doc -> Doc -> Doc
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
P.<+> Doc
"=<" Doc -> Doc -> Doc
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b Doc -> Doc -> Doc
P.<+> Doc
"+" Doc -> Doc -> Doc
P.<+> [Char] -> Doc
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
P.<+> Doc
"+" Doc -> Doc -> Doc
P.<+> [Char] -> Doc
P.text (Int -> [Char]
forall a. Show a => a -> [Char]
show (-Int
n)) Doc -> Doc -> Doc
P.<+> Doc
"=<" Doc -> Doc -> Doc
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 (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)
mapM Constraint -> TCMT IO (Maybe OldSizeConstraint)
oldComputeSizeConstraint [Constraint]
leqs
  where
    -- get the constraints plus contexts they are defined in
    gammas :: [Context]
gammas       = (ProblemConstraint -> Context) -> [ProblemConstraint] -> [Context]
forall a b. (a -> b) -> [a] -> [b]
map (TCEnv -> Context
envContext (TCEnv -> Context)
-> (ProblemConstraint -> TCEnv) -> ProblemConstraint -> Context
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 -> Int) -> [Context] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Context -> Int
forall a. Sized a => a -> Int
size [Context]
gammas
    waterLevel :: Int
waterLevel   = [Int] -> Int
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
prettyTCM Constraint
c
          ]
        (OldSizeExpr
a, Int
n) <- Term -> TCMT IO (OldSizeExpr, Int)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
u
        (OldSizeExpr
b, Int
m) <- Term -> TCMT IO (OldSizeExpr, Int)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
v
        Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint))
-> Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
forall a b. (a -> b) -> a -> b
$ OldSizeConstraint -> Maybe OldSizeConstraint
forall a. a -> Maybe a
Just (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> Int -> OldSizeExpr -> OldSizeConstraint
Leq OldSizeExpr
a (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) OldSizeExpr
b
      TCMT IO (Maybe OldSizeConstraint)
-> (TCErr -> TCMT IO (Maybe OldSizeConstraint))
-> TCMT IO (Maybe OldSizeConstraint)
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 (m :: * -> *) a. Monad m => a -> m a
return Maybe OldSizeConstraint
forall a. Maybe a
Nothing
        TCErr
_            -> TCErr -> TCMT IO (Maybe OldSizeConstraint)
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 :: (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 <- Term -> m 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.
  [Char] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.conv.size" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"oldSizeExpr:" 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
prettyTCM Term
u
  SizeView
s <- Term -> m SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
  case SizeView
s of
    SizeView
SizeInf     -> Blocker -> m (OldSizeExpr, Int)
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
    SizeSuc Term
u   -> (Int -> Int) -> (OldSizeExpr, Int) -> (OldSizeExpr, Int)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ((OldSizeExpr, Int) -> (OldSizeExpr, Int))
-> m (OldSizeExpr, Int) -> m (OldSizeExpr, Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (OldSizeExpr, Int)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, Int)
oldSizeExpr Term
u
    OtherSize Term
u -> case Term
u of
      Var Int
i []  -> (OldSizeExpr, Int) -> m (OldSizeExpr, Int)
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)
mapM Elim -> Maybe Int
isVar [Elim]
es, [Int] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [Int]
xs
                -> (OldSizeExpr, Int) -> m (OldSizeExpr, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId -> [Int] -> OldSizeExpr
SizeMeta MetaId
m [Int]
xs, Int
0)
      Term
_ -> Blocker -> m (OldSizeExpr, Int)
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 (m :: * -> *) a. Monad m => a -> m a
return OldSizeConstraint
c
    (SizeMeta MetaId
m [Int]
xs, Rigid Int
i) -> do
      Int
j <- Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
i [Int]
xs
      OldSizeConstraint -> Maybe OldSizeConstraint
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 (Int -> OldSizeExpr
Rigid Int
j)
    (Rigid Int
i, SizeMeta MetaId
m [Int]
xs) -> do
      Int
j <- Int -> [Int] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex Int
i [Int]
xs
      OldSizeConstraint -> Maybe OldSizeConstraint
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 (Int -> OldSizeExpr
Rigid Int
j) Int
n (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])
    (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)
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 (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)
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 (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

-- | Main function.
--   Uses the old solver for size constraints using "Agda.Utils.Warshall".
--   This solver does not smartly use size hypotheses @j : Size< i@.
--   It only checks that its computed solution is compatible
oldSolveSizeConstraints :: TCM ()
oldSolveSizeConstraints :: TCM ()
oldSolveSizeConstraints = TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCMT IO Bool
haveSizedTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.solve" Int
70 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Considering to solve size constraints"
  [ProblemConstraint]
cs0 <- (Comparison -> Bool) -> TCM [ProblemConstraint]
getSizeConstraints (Comparison -> Comparison -> Bool
forall a. Eq a => a -> a -> Bool
== Comparison
CmpLeq)
  [OldSizeConstraint]
cs <- [ProblemConstraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [ProblemConstraint]
cs0
  [(MetaId, Type, Telescope)]
ms <- Bool -> TCM [(MetaId, Type, Telescope)]
getSizeMetas Bool
True -- get all size metas, also interaction metas

  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([OldSizeConstraint] -> Bool
forall a. Null a => a -> Bool
null [OldSizeConstraint]
cs) Bool -> Bool -> Bool
|| Bool -> Bool
not ([(MetaId, Type, Telescope)] -> Bool
forall a. Null a => a -> Bool
null [(MetaId, Type, Telescope)]
ms)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.solve" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Solving size constraints " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [OldSizeConstraint] -> [Char]
forall a. Show a => a -> [Char]
show [OldSizeConstraint]
cs

    [OldSizeConstraint]
cs <- [OldSizeConstraint] -> TCM [OldSizeConstraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([OldSizeConstraint] -> TCM [OldSizeConstraint])
-> [OldSizeConstraint] -> TCM [OldSizeConstraint]
forall a b. (a -> b) -> a -> b
$ (OldSizeConstraint -> Maybe OldSizeConstraint)
-> [OldSizeConstraint] -> [OldSizeConstraint]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe OldSizeConstraint -> Maybe OldSizeConstraint
oldCanonicalizeSizeConstraint [OldSizeConstraint]
cs
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.solve" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Canonicalized constraints: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [OldSizeConstraint] -> [Char]
forall a. Show a => a -> [Char]
show [OldSizeConstraint]
cs

    let -- Error for giving up
        cannotSolve :: TCM ()
cannotSolve = TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (TCMT IO Doc
"Cannot solve size constraints" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (ProblemConstraint -> TCMT IO Doc)
-> [ProblemConstraint] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ProblemConstraint]
cs0)

        -- Size metas in constraints.
        metas0 :: [(MetaId, Int)]  -- meta id + arity
        metas0 :: [(MetaId, Int)]
metas0 = ((MetaId, Int) -> (MetaId, Int))
-> [(MetaId, Int)] -> [(MetaId, Int)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
List.nubOn (MetaId, Int) -> (MetaId, Int)
forall a. a -> a
id ([(MetaId, Int)] -> [(MetaId, Int)])
-> [(MetaId, Int)] -> [(MetaId, Int)]
forall a b. (a -> b) -> a -> b
$ ((MetaId, [Int]) -> (MetaId, Int))
-> [(MetaId, [Int])] -> [(MetaId, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (([Int] -> Int) -> (MetaId, [Int]) -> (MetaId, Int)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) ([(MetaId, [Int])] -> [(MetaId, Int)])
-> [(MetaId, [Int])] -> [(MetaId, Int)]
forall a b. (a -> b) -> a -> b
$ (OldSizeConstraint -> [(MetaId, [Int])])
-> [OldSizeConstraint] -> [(MetaId, [Int])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap OldSizeConstraint -> [(MetaId, [Int])]
flexibleVariables [OldSizeConstraint]
cs

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

        -- All size metas
        metas :: [(MetaId, Int)]
metas = [(MetaId, Int)]
metas0 [(MetaId, Int)] -> [(MetaId, Int)] -> [(MetaId, Int)]
forall a. [a] -> [a] -> [a]
++ [(MetaId, Int)]
metas1

    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.solve" Int
15 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Metas: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(MetaId, Int)] -> [Char]
forall a. Show a => a -> [Char]
show [(MetaId, Int)]
metas0 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
", " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(MetaId, Int)] -> [Char]
forall a. Show a => a -> [Char]
show [(MetaId, Int)]
metas1

    [Char] -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => [Char] -> Int -> m () -> m ()
verboseS [Char]
"tc.size.solve" Int
20 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        -- debug print the type of all size metas
        [(MetaId, Int)] -> ((MetaId, Int) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(MetaId, Int)]
metas (((MetaId, Int) -> TCM ()) -> TCM ())
-> ((MetaId, Int) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (MetaId
m, Int
_) ->
            [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Judgement MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Judgement MetaId -> TCMT IO Doc)
-> TCMT IO (Judgement MetaId) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaVariable -> Judgement MetaId
mvJudgement (MetaVariable -> Judgement MetaId)
-> TCMT IO MetaVariable -> TCMT IO (Judgement MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m

    -- Run the solver.
    TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ([(MetaId, Int)] -> [OldSizeConstraint] -> TCMT IO Bool
oldSolver [(MetaId, Int)]
metas [OldSizeConstraint]
cs) TCM ()
cannotSolve

    -- Double-checking the solution.

    -- Andreas, 2012-09-19
    -- The returned solution might not be consistent with
    -- the hypotheses on rigid vars (j : Size< i).
    -- Thus, we double check that all size constraints
    -- have been solved correctly.
    (TCM () -> (TCErr -> TCM ()) -> TCM ())
-> (TCErr -> TCM ()) -> TCM () -> TCM ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCM () -> (TCErr -> TCM ()) -> TCM ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (TCM () -> TCErr -> TCM ()
forall a b. a -> b -> a
const TCM ()
cannotSolve) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        [ProblemConstraint] -> (ProblemConstraint -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ProblemConstraint]
cs0 ((ProblemConstraint -> TCM ()) -> TCM ())
-> (ProblemConstraint -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Constraint -> TCM ()) -> ProblemConstraint -> TCM ()
forall (m :: * -> *) a.
MonadConstraint m =>
(Constraint -> m a) -> ProblemConstraint -> m a
withConstraint Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint


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

  -- run the Warshall solver
  case Constraints -> Maybe Solution
W.solve (Constraints -> Maybe Solution) -> Constraints -> Maybe Solution
forall a b. (a -> b) -> a -> b
$ ((MetaId, Int) -> Constraint) -> [(MetaId, Int)] -> Constraints
forall a b. (a -> b) -> [a] -> [b]
map (MetaId, Int) -> Constraint
forall {a} {a}. (Integral a, Num a, Ord a) => (a, a) -> Constraint
mkFlex [(MetaId, Int)]
metas Constraints -> Constraints -> Constraints
forall a. [a] -> [a] -> [a]
++ (OldSizeConstraint -> Constraint)
-> [OldSizeConstraint] -> Constraints
forall a b. (a -> b) -> [a] -> [b]
map OldSizeConstraint -> Constraint
mkConstr [OldSizeConstraint]
cs of
    Maybe Solution
Nothing  -> TCMT IO Bool
cannotSolve
    Just Solution
sol -> do
      [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.size.solve" Int
10 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Solved constraints: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Solution -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Solution
sol
      Term
suc   <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
      Term
infty <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
      let plus :: Term -> Int -> Term
plus Term
v Int
0 = Term
v
          plus Term
v Int
n = Term
suc Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term -> Int -> Term
plus Term
v (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

          inst :: (Int, SizeExpr) -> TCM ()
inst (Int
i, SizeExpr
e) = do

            let m :: MetaId
m  = Int -> MetaId
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i  -- meta variable identifier
                ar :: Int
ar = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ MetaId -> [(MetaId, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
m [(MetaId, Int)]
metas  -- meta var arity

                term :: SizeExpr -> Term
term (W.SizeConst Weight
W.Infinite) = Term
infty
                term (W.SizeVar Int
j Int
n) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
ar = Term -> Int -> Term
plus (Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
n
                term SizeExpr
_                        = Term
forall a. HasCallStack => a
__IMPOSSIBLE__

                tel :: [Arg [Char]]
tel = Int -> Arg [Char] -> [Arg [Char]]
forall a. Int -> a -> [a]
replicate Int
ar (Arg [Char] -> [Arg [Char]]) -> Arg [Char] -> [Arg [Char]]
forall a b. (a -> b) -> a -> b
$ [Char] -> Arg [Char]
forall a. a -> Arg a
defaultArg [Char]
"s"
                -- convert size expression to term
                v :: Term
v = SizeExpr -> Term
term SizeExpr
e

            [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" 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
              [ MetaId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":="
              , 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
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
              ]

            -- Andreas, 2012-09-25: do not assign interaction metas to \infty
            let isInf :: SizeExpr -> Bool
isInf (W.SizeConst Weight
W.Infinite) = Bool
True
                isInf SizeExpr
_                        = Bool
False
            TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (((SizeExpr -> Bool
isInf SizeExpr
e Bool -> Bool -> Bool
&&) (Bool -> Bool)
-> (Maybe InteractionId -> Bool) -> Maybe InteractionId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` MetaId -> TCMT IO Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
              MetaId -> [Arg [Char]] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm MetaId
m [Arg [Char]]
tel Term
v

      ((Int, SizeExpr) -> TCM ()) -> [(Int, SizeExpr)] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Int, SizeExpr) -> TCM ()
inst ([(Int, SizeExpr)] -> TCM ()) -> [(Int, SizeExpr)] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Solution -> [(Int, SizeExpr)]
forall k a. Map k a -> [(k, a)]
Map.toList Solution
sol
      Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True