{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.SizedTypes where

import Prelude hiding (null)

import Control.Monad.Writer

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

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.Constraints

import Agda.Utils.Except ( MonadError(catchError, throwError) )
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)
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
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size" VerboseLevel
10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    Telescope
tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
    [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
      [ TCM Doc
"checking that " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
" is not an empty type of sizes"
      , if Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel then TCM Doc
forall a. Null a => a
empty else do
        TCM Doc
"in context " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel)
      ]
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size" VerboseLevel
60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"- raw type = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show Term
t
  let postpone :: Term -> TCM ()
      postpone :: Term -> TCM ()
postpone Term
t = do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size.lt" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ TCM Doc
"- postponing `not empty type of sizes' check for " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t ]
        Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Constraint
CheckSizeLtSat Term
t
  let ok :: TCM ()
      ok :: TCM ()
ok = VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size.lt" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"- succeeded: not an empty type of sizes"
  Term
-> (MetaId -> Term -> TCM ())
-> (NotBlocked -> Term -> TCM ())
-> TCM ()
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
t ((Term -> TCM ()) -> MetaId -> Term -> TCM ()
forall a b. a -> b -> a
const Term -> TCM ()
postpone) ((NotBlocked -> Term -> TCM ()) -> TCM ())
-> (NotBlocked -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
t -> do
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size.lt" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"- 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
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size.lt" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
" - type is a size type"
      case BoundedSize
b of
        BoundedSize
BoundedNo -> TCM ()
ok
        BoundedLt Term
b -> do
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size.lt" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
" - type is SIZELT" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
b
          Term
-> (MetaId -> Term -> TCM ())
-> (NotBlocked -> Term -> TCM ())
-> TCM ()
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
b (\ MetaId
_ Term
_ -> Term -> TCM ()
postpone Term
t) ((NotBlocked -> Term -> TCM ()) -> TCM ())
-> (NotBlocked -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
b -> do
            VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size.lt" VerboseLevel
20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
" - 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 ()) -> TCM Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
                  TCM Doc
"Possibly empty type of sizes " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM 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, MonadError TCErr 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 VerboseLevel
i [] -> VerboseLevel -> TCMT IO Bool
checkSizeVarNeverZero VerboseLevel
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 :: VerboseLevel -> TCMT IO Bool
checkSizeVarNeverZero VerboseLevel
i = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checkSizeVarNeverZero" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
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)
-> [Dom' Term (Name, Type)] -> [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) ([Dom' Term (Name, Type)] -> [Type])
-> ([Dom' Term (Name, Type)] -> [Dom' Term (Name, Type)])
-> [Dom' Term (Name, Type)]
-> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel
-> [Dom' Term (Name, Type)] -> [Dom' Term (Name, Type)]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
i ([Dom' Term (Name, Type)] -> [Type])
-> TCMT IO [Dom' Term (Name, Type)] -> TCMT IO [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Dom' Term (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
getContext
  -- If we encountered a blocking meta in the context, we cannot
  -- say ``no'' for sure.
  (VerboseLevel
n, Any Bool
meta) <- WriterT Any TCM VerboseLevel -> TCM (VerboseLevel, Any)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT Any TCM VerboseLevel -> TCM (VerboseLevel, Any))
-> WriterT Any TCM VerboseLevel -> TCM (VerboseLevel, Any)
forall a b. (a -> b) -> a -> b
$ [Type] -> [VerboseLevel] -> WriterT Any TCM VerboseLevel
minSizeValAux [Type]
ts ([VerboseLevel] -> WriterT Any TCM VerboseLevel)
-> [VerboseLevel] -> WriterT Any TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. a -> [a]
repeat VerboseLevel
0
  if VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else
    if Bool
meta then TCMT IO Bool
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation else Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  where
  -- Compute the least valuation for size context ts above the
  -- given valuation and return its last value.
  minSizeValAux :: [Type] -> [Int] -> WriterT Any TCM Int
  minSizeValAux :: [Type] -> [VerboseLevel] -> WriterT Any TCM VerboseLevel
minSizeValAux [Type]
_        []      = WriterT Any TCM VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__
  minSizeValAux []       (VerboseLevel
n : [VerboseLevel]
_) = VerboseLevel -> WriterT Any TCM VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseLevel
n
  minSizeValAux (Type
t : [Type]
ts) (VerboseLevel
n : [VerboseLevel]
ns) = do
    VerboseKey -> VerboseLevel -> TCM Doc -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size" VerboseLevel
60 (TCM Doc -> WriterT Any TCM ()) -> TCM Doc -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$
       VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey
"minSizeVal (n:ns) = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [VerboseLevel] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. VerboseLevel -> [a] -> [a]
take ([Type] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Type]
ts VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
2) ([VerboseLevel] -> [VerboseLevel])
-> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ VerboseLevel
nVerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. a -> [a] -> [a]
:[VerboseLevel]
ns) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
             VerboseKey
" t =") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> (Type -> VerboseKey) -> Type -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> VerboseKey
forall a. Show a => a -> VerboseKey
show) Type
t  -- prettyTCM t  -- Wrong context!
    -- n is the min. value for variable 0 which has type t.
    let cont :: WriterT Any TCM VerboseLevel
cont = [Type] -> [VerboseLevel] -> WriterT Any TCM VerboseLevel
minSizeValAux [Type]
ts [VerboseLevel]
ns
        perhaps :: WriterT Any TCM VerboseLevel
perhaps = Any -> WriterT Any TCM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True) WriterT Any TCM ()
-> WriterT Any TCM VerboseLevel -> WriterT Any TCM VerboseLevel
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriterT Any TCM VerboseLevel
cont
    -- If we encounter a blocked type in the context, we cannot
    -- give a definite answer.
    Type
-> (MetaId -> Type -> WriterT Any TCM VerboseLevel)
-> (NotBlocked -> Type -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ MetaId
_ Type
_ -> WriterT Any TCM VerboseLevel
perhaps) ((NotBlocked -> Type -> WriterT Any TCM VerboseLevel)
 -> WriterT Any TCM VerboseLevel)
-> (NotBlocked -> Type -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
      WriterT Any TCM (Maybe BoundedSize)
-> WriterT Any TCM VerboseLevel
-> (BoundedSize -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCMT IO (Maybe BoundedSize) -> WriterT Any TCM (Maybe BoundedSize)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (Maybe BoundedSize)
 -> WriterT Any TCM (Maybe BoundedSize))
-> TCMT IO (Maybe BoundedSize)
-> WriterT Any TCM (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 Any TCM VerboseLevel
cont ((BoundedSize -> WriterT Any TCM VerboseLevel)
 -> WriterT Any TCM VerboseLevel)
-> (BoundedSize -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ \ BoundedSize
b -> do
        case BoundedSize
b of
          BoundedSize
BoundedNo -> WriterT Any TCM VerboseLevel
cont
          BoundedLt Term
u -> Term
-> (MetaId -> Term -> WriterT Any TCM VerboseLevel)
-> (NotBlocked -> Term -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
u (\ MetaId
_ Term
_ -> WriterT Any TCM VerboseLevel
perhaps) ((NotBlocked -> Term -> WriterT Any TCM VerboseLevel)
 -> WriterT Any TCM VerboseLevel)
-> (NotBlocked -> Term -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
u -> do
            VerboseKey -> VerboseLevel -> VerboseKey -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size" VerboseLevel
60 (VerboseKey -> WriterT Any TCM ())
-> VerboseKey -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"minSizeVal upper bound u = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show Term
u
            DeepSizeView
v <- TCM DeepSizeView -> WriterT Any TCM DeepSizeView
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM DeepSizeView -> WriterT Any TCM DeepSizeView)
-> TCM DeepSizeView -> WriterT Any TCM DeepSizeView
forall a b. (a -> b) -> a -> b
$ Term -> TCM 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 VerboseLevel
j VerboseLevel
m -> do
                VerboseKey -> VerboseLevel -> VerboseKey -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size" VerboseLevel
60 (VerboseKey -> WriterT Any TCM ())
-> VerboseKey -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"minSizeVal upper bound v = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ DeepSizeView -> VerboseKey
forall a. Show a => a -> VerboseKey
show DeepSizeView
v
                let ns' :: [VerboseLevel]
ns' = VerboseLevel
-> (VerboseLevel -> VerboseLevel)
-> [VerboseLevel]
-> [VerboseLevel]
forall a. VerboseLevel -> (a -> a) -> [a] -> [a]
List.updateAt VerboseLevel
j (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Ord a => a -> a -> a
max (VerboseLevel -> VerboseLevel -> VerboseLevel)
-> VerboseLevel -> VerboseLevel -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ VerboseLevel
nVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
1VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
m) [VerboseLevel]
ns
                VerboseKey -> VerboseLevel -> VerboseKey -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size" VerboseLevel
60 (VerboseKey -> WriterT Any TCM ())
-> VerboseKey -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"minSizeVal ns' = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [VerboseLevel] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. VerboseLevel -> [a] -> [a]
take ([Type] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Type]
ts VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1) [VerboseLevel]
ns')
                [Type] -> [VerboseLevel] -> WriterT Any TCM VerboseLevel
minSizeValAux [Type]
ts [VerboseLevel]
ns'
              DSizeMeta{} -> WriterT Any TCM VerboseLevel
perhaps
              DeepSizeView
_ -> WriterT Any TCM VerboseLevel
cont

-- | Check whether a variable in the context is bounded by a size expression.
--   If @x : Size< a@, then @a@ is returned.
isBounded :: (MonadReduce m, MonadTCEnv m, HasBuiltins m)
          => Nat -> m BoundedSize
isBounded :: VerboseLevel -> m BoundedSize
isBounded VerboseLevel
i = do
  Type
t <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> m Type) -> m Type -> m Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseLevel -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i
  case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
    Def QName
x [Apply Arg Term
u] -> do
      Maybe Term
sizelt <- VerboseKey -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getBuiltin' VerboseKey
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.
--   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 :: Term -> Telescope -> Type -> m ()
boundedSizeMetaHook Term
v 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
      VerboseLevel
n <- m VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
      let tel :: Telescope
tel | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0     = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> ListTel -> ListTel
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
n (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (VerboseKey, 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 <- VerboseLevel -> Term -> m Term
forall (m :: * -> *).
HasBuiltins m =>
VerboseLevel -> Term -> m Term
sizeSuc VerboseLevel
1 (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term -> Term
forall t a. Subst t a => VerboseLevel -> a -> a
raise (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
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
        Constraint -> m ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (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 ()

-- | @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 :: 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 :: m a
failure = TypeError -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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 a. 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 VerboseLevel 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 VerboseLevel 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 a. m a
failure

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

-- | Compute the deep size view of a term.
--   Precondition: sized types are enabled.
deepSizeView :: Term -> TCM DeepSizeView
deepSizeView :: Term -> TCM DeepSizeView
deepSizeView Term
v = do
  Def QName
inf [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  Def QName
suc [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
  let loop :: Term -> m DeepSizeView
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
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 VerboseLevel
i []                   -> 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
$ VerboseLevel -> VerboseLevel -> DeepSizeView
DSizeVar VerboseLevel
i VerboseLevel
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] -> VerboseLevel -> DeepSizeView
DSizeMeta MetaId
x [Elim]
us VerboseLevel
0
          Term
_                          -> 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 -> TCM DeepSizeView
forall (m :: * -> *). MonadReduce m => Term -> m DeepSizeView
loop Term
v

sizeMaxView :: (MonadReduce m, HasBuiltins m) => Term -> m SizeMaxView
sizeMaxView :: Term -> m SizeMaxView
sizeMaxView Term
v = do
  Maybe QName
inf <- VerboseKey -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinDefName VerboseKey
builtinSizeInf
  Maybe QName
suc <- VerboseKey -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinDefName VerboseKey
builtinSizeSuc
  Maybe QName
max <- VerboseKey -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinDefName VerboseKey
builtinSizeMax
  let loop :: Term -> f SizeMaxView
loop Term
v = do
        Term
v <- Term -> f 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 -> f SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> f SizeMaxView) -> SizeMaxView -> f 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) -> f SizeMaxView -> f SizeMaxView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f 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)
-> f SizeMaxView -> f (SizeMaxView -> SizeMaxView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f SizeMaxView
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u1) f (SizeMaxView -> SizeMaxView) -> f SizeMaxView -> f SizeMaxView
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> f SizeMaxView
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u2)
          Var VerboseLevel
i []                      -> SizeMaxView -> f SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> f SizeMaxView) -> SizeMaxView -> f 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
$ VerboseLevel -> VerboseLevel -> DeepSizeView
DSizeVar VerboseLevel
i VerboseLevel
0
          MetaV MetaId
x [Elim]
us                    -> SizeMaxView -> f SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> f SizeMaxView) -> SizeMaxView -> f 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] -> VerboseLevel -> DeepSizeView
DSizeMeta MetaId
x [Elim]
us VerboseLevel
0
          Term
_                             -> SizeMaxView -> f SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> f SizeMaxView) -> SizeMaxView -> f 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
forall (f :: * -> *). MonadReduce f => Term -> f SizeMaxView
loop Term
v

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

-- | Compare two sizes.
compareSizes :: (MonadConversion m) => Comparison -> Term -> Term -> m ()
compareSizes :: Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u Term
v = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.conv.size" VerboseLevel
10 VerboseKey
"compareSizes" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
10 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ TCM Doc
"Comparing sizes"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Comparison -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp
                   , Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
                   ]
    ]
  VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"tc.conv.size" VerboseLevel
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
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Term
u TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Comparison -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp
                   , Term -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Term
v
                   ]
  SizeMaxView
us <- Term -> m SizeMaxView
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Term -> m SizeMaxView
sizeMaxView Term
u
  SizeMaxView
vs <- Term -> m SizeMaxView
forall (m :: * -> *).
(MonadReduce m, HasBuiltins 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 :: 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 :: DeepSizeView -> SizeMaxView -> m ()
compareBelowMax DeepSizeView
u SizeMaxView
vs = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.conv.size" VerboseLevel
45 VerboseKey
"compareBelowMax" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
45 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
    [ DeepSizeView -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty DeepSizeView
u
    , Comparison -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Comparison
CmpLeq
    , SizeMaxView -> TCM Doc
forall (m :: * -> *) a. (Monad 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 b (m :: * -> *) a. MonadError b 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 b (m :: * -> *) a. MonadError b 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
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
45 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
      [ TCM 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 -> (b -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` m a -> b -> m a
forall a b. a -> b -> a
const m a
c2

compareSizeViews :: (MonadConversion m) => Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
cmp DeepSizeView
s1' DeepSizeView
s2' = do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
45 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
hsep
    [ TCM Doc
"compareSizeViews"
    , DeepSizeView -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty DeepSizeView
s1'
    , Comparison -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Comparison
cmp
    , DeepSizeView -> TCM Doc
forall (m :: * -> *) a. (Monad 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 b) -> m b
withUnView Term -> Term -> m b
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 b
cont Term
u Term
v
      failure :: m b
failure = (Term -> Term -> m b) -> m b
forall (m :: * -> *) b.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
(Term -> Term -> m b) -> m b
withUnView ((Term -> Term -> m b) -> m b) -> (Term -> Term -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \ Term
u Term
v -> TypeError -> m b
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m b) -> TypeError -> m b
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 ()
forall (m :: * -> *) b.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
(Term -> Term -> m b) -> m b
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 ()
forall b. m b
failure
    (Comparison
_    ,  DeepSizeView
DSizeInf,     DSizeVar{}) -> m ()
forall b. m b
failure
    (Comparison
_    ,  DeepSizeView
DSizeInf,     DeepSizeView
_         ) -> Comparison -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh VerboseLevel m) =>
Comparison -> m ()
continue Comparison
CmpEq
    (Comparison
CmpLeq, DSizeVar VerboseLevel
i VerboseLevel
n, DSizeVar VerboseLevel
j VerboseLevel
m) | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
j -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
m) m ()
forall b. m b
failure
    (Comparison
CmpLeq, DSizeVar VerboseLevel
i VerboseLevel
n, DSizeVar VerboseLevel
j VerboseLevel
m) | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
/= VerboseLevel
j -> do
       BoundedSize
res <- VerboseLevel -> m BoundedSize
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, HasBuiltins m) =>
VerboseLevel -> m BoundedSize
isBounded VerboseLevel
i
       case BoundedSize
res of
         BoundedSize
BoundedNo -> m ()
forall b. m b
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 VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 then do
              Term
u'' <- VerboseLevel -> Term -> m Term
forall (m :: * -> *).
HasBuiltins m =>
VerboseLevel -> Term -> m Term
sizeSuc (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
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
=<< VerboseLevel -> Term -> m Term
forall (m :: * -> *).
HasBuiltins m =>
VerboseLevel -> Term -> m Term
sizeSuc VerboseLevel
1 Term
v
    (Comparison
CmpLeq, DeepSizeView
s1,        DeepSizeView
s2)         -> (Term -> Term -> m ()) -> m ()
forall (m :: * -> *) b.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
(Term -> Term -> m b) -> m b
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 ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh VerboseLevel m) =>
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 :: 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-} (Constraint -> m ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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)

-- | Checked whether a size constraint is trivial (like @X <= X+1@).
trivial :: (MonadConversion m) => Term -> Term -> m Bool
trivial :: Term -> Term -> m Bool
trivial Term
u Term
v = do
    a :: (OldSizeExpr, VerboseLevel)
a@(OldSizeExpr
e , VerboseLevel
n ) <- Term -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
u
    b :: (OldSizeExpr, VerboseLevel)
b@(OldSizeExpr
e', VerboseLevel
n') <- Term -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
v
    let triv :: Bool
triv = OldSizeExpr
e OldSizeExpr -> OldSizeExpr -> Bool
forall a. Eq a => a -> a -> Bool
== OldSizeExpr
e' Bool -> Bool -> Bool
&& VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
n'
          -- Andreas, 2012-02-24  filtering out more trivial constraints fixes
          -- test/lib-succeed/SizeInconsistentMeta4.agda
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ if Bool
triv then TCM Doc
"trivial constraint" else TCM Doc
forall a. Null a => a
empty
                   , (OldSizeExpr, VerboseLevel) -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (OldSizeExpr, VerboseLevel)
a TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"<="
                   , (OldSizeExpr, VerboseLevel) -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (OldSizeExpr, VerboseLevel)
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 :: 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 :: (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 [Closure Constraint]
takeSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]
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 -> Closure Constraint)
-> [ProblemConstraint] -> [Closure Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint ([ProblemConstraint] -> [Closure Constraint])
-> TCMT IO [ProblemConstraint] -> TCM [Closure Constraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ProblemConstraint -> Bool) -> TCMT IO [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 [Closure Constraint]
getSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]
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
  (Closure Constraint -> Bool)
-> [Closure Constraint] -> [Closure Constraint]
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] -> [Closure Constraint])
-> ([ProblemConstraint] -> [Closure Constraint])
-> [ProblemConstraint]
-> [Closure Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Closure Constraint)
-> [ProblemConstraint] -> [Closure Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint ([ProblemConstraint] -> [Closure Constraint])
-> TCMT IO [ProblemConstraint] -> TCM [Closure Constraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [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, VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey
[OldSizeExpr] -> VerboseKey -> VerboseKey
OldSizeExpr -> VerboseKey
(VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey)
-> (OldSizeExpr -> VerboseKey)
-> ([OldSizeExpr] -> VerboseKey -> VerboseKey)
-> Show OldSizeExpr
forall a.
(VerboseLevel -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [OldSizeExpr] -> VerboseKey -> VerboseKey
$cshowList :: [OldSizeExpr] -> VerboseKey -> VerboseKey
show :: OldSizeExpr -> VerboseKey
$cshow :: OldSizeExpr -> VerboseKey
showsPrec :: VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey
$cshowsPrec :: VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey
Show)

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

instance Pretty OldSizeConstraint where
  pretty :: OldSizeConstraint -> Doc
pretty (Leq OldSizeExpr
a VerboseLevel
n OldSizeExpr
b)
    | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
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
    | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
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.<+> VerboseKey -> Doc
P.text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
n)
    | Bool
otherwise = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> Doc
"+" Doc -> Doc -> Doc
P.<+> VerboseKey -> Doc
P.text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (-VerboseLevel
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 :: [Closure Constraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints :: [Closure Constraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [] = [OldSizeConstraint] -> TCM [OldSizeConstraint]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- special case to avoid maximum []
oldComputeSizeConstraints [Closure Constraint]
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 :: [[Dom' Term (Name, Type)]]
gammas       = (Closure Constraint -> [Dom' Term (Name, Type)])
-> [Closure Constraint] -> [[Dom' Term (Name, Type)]]
forall a b. (a -> b) -> [a] -> [b]
map (TCEnv -> [Dom' Term (Name, Type)]
envContext (TCEnv -> [Dom' Term (Name, Type)])
-> (Closure Constraint -> TCEnv)
-> Closure Constraint
-> [Dom' Term (Name, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv) [Closure Constraint]
cs
    ls :: [Constraint]
ls           = (Closure Constraint -> Constraint)
-> [Closure Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map Closure Constraint -> Constraint
forall a. Closure a -> a
clValue [Closure Constraint]
cs
    -- compute the longest context (common water level)
    ns :: [VerboseLevel]
ns           = ([Dom' Term (Name, Type)] -> VerboseLevel)
-> [[Dom' Term (Name, Type)]] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map [Dom' Term (Name, Type)] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [[Dom' Term (Name, Type)]]
gammas
    waterLevel :: VerboseLevel
waterLevel   = [VerboseLevel] -> VerboseLevel
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [VerboseLevel]
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 = (VerboseLevel -> Constraint -> Constraint)
-> [VerboseLevel] -> [Constraint] -> [Constraint]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VerboseLevel -> Constraint -> Constraint
forall t a. Subst t a => VerboseLevel -> a -> a
raise ((VerboseLevel -> VerboseLevel) -> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel
waterLevel VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-) [VerboseLevel]
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
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size.solve" VerboseLevel
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ TCM Doc
"converting size constraint"
          , Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c
          ]
        (OldSizeExpr
a, VerboseLevel
n) <- Term -> TCMT IO (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
u
        (OldSizeExpr
b, VerboseLevel
m) <- Term -> TCMT IO (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
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 -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq OldSizeExpr
a (VerboseLevel
m VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
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 :: (MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m)
            => Term -> m (OldSizeExpr, Int)
oldSizeExpr :: Term -> m (OldSizeExpr, VerboseLevel)
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.
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"oldSizeExpr:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
  SizeView
s <- Term -> m SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
  case SizeView
s of
    SizeView
SizeInf     -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
    SizeSuc Term
u   -> (VerboseLevel -> VerboseLevel)
-> (OldSizeExpr, VerboseLevel) -> (OldSizeExpr, VerboseLevel)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
1) ((OldSizeExpr, VerboseLevel) -> (OldSizeExpr, VerboseLevel))
-> m (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
u
    OtherSize Term
u -> case Term
u of
      Var VerboseLevel
i []  -> (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
i, VerboseLevel
0)
      MetaV MetaId
m [Elim]
es | Just [VerboseLevel]
xs <- (Elim -> Maybe VerboseLevel) -> [Elim] -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Elim -> Maybe VerboseLevel
isVar [Elim]
es, [VerboseLevel] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [VerboseLevel]
xs
                -> (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel]
xs, VerboseLevel
0)
      Term
_ -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  where
    isVar :: Elim -> Maybe VerboseLevel
isVar (Proj{})  = Maybe VerboseLevel
forall a. Maybe a
Nothing
    isVar (IApply Term
_ Term
_ Term
v) = Elim -> Maybe VerboseLevel
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 VerboseLevel
i [] -> VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
i
      Term
_        -> Maybe VerboseLevel
forall a. Maybe a
Nothing

-- | Compute list of size metavariables with their arguments
--   appearing in a constraint.
flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
flexibleVariables :: OldSizeConstraint -> [(MetaId, [VerboseLevel])]
flexibleVariables (Leq OldSizeExpr
a VerboseLevel
_ OldSizeExpr
b) = OldSizeExpr -> [(MetaId, [VerboseLevel])]
flex OldSizeExpr
a [(MetaId, [VerboseLevel])]
-> [(MetaId, [VerboseLevel])] -> [(MetaId, [VerboseLevel])]
forall a. [a] -> [a] -> [a]
++ OldSizeExpr -> [(MetaId, [VerboseLevel])]
flex OldSizeExpr
b
  where
    flex :: OldSizeExpr -> [(MetaId, [VerboseLevel])]
flex (Rigid VerboseLevel
_)       = []
    flex (SizeMeta MetaId
m [VerboseLevel]
xs) = [(MetaId
m, [VerboseLevel]
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 VerboseLevel
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 [VerboseLevel]
xs, Rigid VerboseLevel
i) -> do
      VerboseLevel
j <- (VerboseLevel -> Bool) -> [VerboseLevel] -> Maybe VerboseLevel
forall a. (a -> Bool) -> [a] -> Maybe VerboseLevel
List.findIndex (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==VerboseLevel
i) [VerboseLevel]
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 -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel
0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1]) VerboseLevel
n (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
j)
    (Rigid VerboseLevel
i, SizeMeta MetaId
m [VerboseLevel]
xs) -> do
      VerboseLevel
j <- (VerboseLevel -> Bool) -> [VerboseLevel] -> Maybe VerboseLevel
forall a. (a -> Bool) -> [a] -> Maybe VerboseLevel
List.findIndex (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==VerboseLevel
i) [VerboseLevel]
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 -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
j) VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel
0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1])
    (SizeMeta MetaId
m [VerboseLevel]
xs, SizeMeta MetaId
l [VerboseLevel]
ys)
         -- try to invert xs on ys
       | Just [VerboseLevel]
ys' <- (VerboseLevel -> Maybe VerboseLevel)
-> [VerboseLevel] -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ VerboseLevel
y -> (VerboseLevel -> Bool) -> [VerboseLevel] -> Maybe VerboseLevel
forall a. (a -> Bool) -> [a] -> Maybe VerboseLevel
List.findIndex (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==VerboseLevel
y) [VerboseLevel]
xs) [VerboseLevel]
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 -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel
0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1]) VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
l [VerboseLevel]
ys')
         -- try to invert ys on xs
       | Just [VerboseLevel]
xs' <- (VerboseLevel -> Maybe VerboseLevel)
-> [VerboseLevel] -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ VerboseLevel
x -> (VerboseLevel -> Bool) -> [VerboseLevel] -> Maybe VerboseLevel
forall a. (a -> Bool) -> [a] -> Maybe VerboseLevel
List.findIndex (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==VerboseLevel
x) [VerboseLevel]
ys) [VerboseLevel]
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 -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel]
xs') VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
l [VerboseLevel
0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
ysVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
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
  VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size.solve" VerboseLevel
70 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Considering to solve size constraints"
  [Closure Constraint]
cs0 <- (Comparison -> Bool) -> TCM [Closure Constraint]
getSizeConstraints (Comparison -> Comparison -> Bool
forall a. Eq a => a -> a -> Bool
== Comparison
CmpLeq)
  [OldSizeConstraint]
cs <- [Closure Constraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [Closure Constraint]
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
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size.solve" VerboseLevel
10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Solving size constraints " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [OldSizeConstraint] -> VerboseKey
forall a. Show a => a -> VerboseKey
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
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size.solve" VerboseLevel
10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Canonicalized constraints: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [OldSizeConstraint] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [OldSizeConstraint]
cs

    let -- Error for giving up
        cannotSolve :: TCMT IO b
cannotSolve = TypeError -> TCMT IO b
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO b) -> (Doc -> TypeError) -> Doc -> TCMT IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO b) -> TCM Doc -> TCMT IO b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat (TCM Doc
"Cannot solve size constraints" TCM Doc -> [TCM Doc] -> [TCM Doc]
forall a. a -> [a] -> [a]
: (Closure Constraint -> TCM Doc)
-> [Closure Constraint] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Closure Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Closure Constraint]
cs0)

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

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

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

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

    VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"tc.size.solve" VerboseLevel
20 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        -- debug print the type of all size metas
        [(MetaId, VerboseLevel)]
-> ((MetaId, VerboseLevel) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(MetaId, VerboseLevel)]
metas (((MetaId, VerboseLevel) -> TCM ()) -> TCM ())
-> ((MetaId, VerboseLevel) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (MetaId
m, VerboseLevel
_) ->
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size.solve" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Judgement MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Judgement MetaId -> TCM Doc)
-> TCMT IO (Judgement MetaId) -> TCM 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, VerboseLevel)] -> [OldSizeConstraint] -> TCMT IO Bool
oldSolver [(MetaId, VerboseLevel)]
metas [OldSizeConstraint]
cs) TCM ()
forall b. TCMT IO b
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 ()
forall b. TCMT IO b
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
$
        [Closure Constraint] -> (Closure Constraint -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Closure Constraint]
cs0 ((Closure Constraint -> TCM ()) -> TCM ())
-> (Closure Constraint -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Closure Constraint
cl -> Closure Constraint -> (Constraint -> TCM ()) -> TCM ()
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
cl 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, VerboseLevel)] -> [OldSizeConstraint] -> TCMT IO Bool
oldSolver [(MetaId, VerboseLevel)]
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) = VerboseLevel -> (VerboseLevel -> Bool) -> Constraint
W.NewFlex (a -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
m) ((VerboseLevel -> Bool) -> Constraint)
-> (VerboseLevel -> Bool) -> Constraint
forall a b. (a -> b) -> a -> b
$ \ VerboseLevel
i -> VerboseLevel -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral VerboseLevel
i a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
ar
      mkConstr :: OldSizeConstraint -> Constraint
mkConstr (Leq OldSizeExpr
a VerboseLevel
n OldSizeExpr
b)  = Node -> VerboseLevel -> Node -> Constraint
W.Arc (OldSizeExpr -> Node
mkNode OldSizeExpr
a) VerboseLevel
n (OldSizeExpr -> Node
mkNode OldSizeExpr
b)
      mkNode :: OldSizeExpr -> Node
mkNode (Rigid VerboseLevel
i)      = Rigid -> Node
W.Rigid (Rigid -> Node) -> Rigid -> Node
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Rigid
W.RVar VerboseLevel
i
      mkNode (SizeMeta MetaId
m [VerboseLevel]
_) = VerboseLevel -> Node
W.Flex (VerboseLevel -> Node) -> VerboseLevel -> Node
forall a b. (a -> b) -> a -> b
$ MetaId -> VerboseLevel
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, VerboseLevel) -> Constraint)
-> [(MetaId, VerboseLevel)] -> Constraints
forall a b. (a -> b) -> [a] -> [b]
map (MetaId, VerboseLevel) -> Constraint
forall a a. (Integral a, Num a, Ord a) => (a, a) -> Constraint
mkFlex [(MetaId, VerboseLevel)]
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
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size.solve" VerboseLevel
10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"Solved constraints: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Solution -> VerboseKey
forall a. Show a => a -> VerboseKey
show 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 -> t -> Term
plus Term
v t
0 = Term
v
          plus Term
v t
n = Term
suc Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term -> t -> Term
plus Term
v (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1)

          inst :: (a, SizeExpr) -> m ()
inst (a
i, SizeExpr
e) = do

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

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

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

            VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size.solve" VerboseLevel
20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
              [ MetaId -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":="
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM 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
            m Bool -> m () -> m ()
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) -> m (Maybe InteractionId) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
m) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` MetaId -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
              MetaId -> [Arg VerboseKey] -> Term -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg VerboseKey] -> Term -> m ()
assignTerm MetaId
m [Arg VerboseKey]
tel Term
v

      ((VerboseLevel, SizeExpr) -> TCM ())
-> [(VerboseLevel, SizeExpr)] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (VerboseLevel, SizeExpr) -> TCM ()
forall (m :: * -> *) a.
(MonadMetaSolver m, Integral a) =>
(a, SizeExpr) -> m ()
inst ([(VerboseLevel, SizeExpr)] -> TCM ())
-> [(VerboseLevel, SizeExpr)] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Solution -> [(VerboseLevel, 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