{-# 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 t :: 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 "tc.size" 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
      [ "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
<+> " 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
        "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 "tc.size" 60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "- 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 t :: Term
t = do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size.lt" 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
          [ "- 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 "tc.size.lt" 20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "- 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
$ \ _ t :: Term
t -> do
    VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.lt" 20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "- 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
$ \ b :: BoundedSize
b -> do
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.lt" 20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " - type is a size type"
      case BoundedSize
b of
        BoundedNo -> TCM ()
ok
        BoundedLt b :: Term
b -> do
          VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size.lt" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ " - 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 (\ _ _ -> Term -> TCM ()
postpone Term
t) ((NotBlocked -> Term -> TCM ()) -> TCM ())
-> (NotBlocked -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ _ b :: Term
b -> do
            VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.lt" 20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " - 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
                  "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 u :: 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
    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 u :: Term
u ->
      case Term
u of
        Var i :: VerboseLevel
i [] -> VerboseLevel -> TCMT IO Bool
checkSizeVarNeverZero VerboseLevel
i
        -- neutral sizes cannot be guaranteed > 0
        _ -> 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 i :: VerboseLevel
i = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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.
  (n :: VerboseLevel
n, Any meta :: 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 0
  if VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> 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 _        []      = WriterT Any TCM VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__
  minSizeValAux []       (n :: VerboseLevel
n : _) = VerboseLevel -> WriterT Any TCM VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseLevel
n
  minSizeValAux (t :: Type
t : ts :: [Type]
ts) (n :: VerboseLevel
n : ns :: [VerboseLevel]
ns) = do
    VerboseKey -> VerboseLevel -> TCM Doc -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size" 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 ("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
+ 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]
++
             " 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 (\ _ _ -> 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
$ \ _ t :: 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
$ \ b :: BoundedSize
b -> do
        case BoundedSize
b of
          BoundedNo -> WriterT Any TCM VerboseLevel
cont
          BoundedLt u :: 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 (\ _ _ -> 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
$ \ _ u :: Term
u -> do
            VerboseKey -> VerboseLevel -> VerboseKey -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size" 60 (VerboseKey -> WriterT Any TCM ())
-> VerboseKey -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$ "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 j :: VerboseLevel
j m :: VerboseLevel
m -> do
                VerboseKey -> VerboseLevel -> VerboseKey -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size" 60 (VerboseKey -> WriterT Any TCM ())
-> VerboseKey -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$ "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
+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 "tc.size" 60 (VerboseKey -> WriterT Any TCM ())
-> VerboseKey -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$ "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
+ 1) [VerboseLevel]
ns')
                [Type] -> [VerboseLevel] -> WriterT Any TCM VerboseLevel
minSizeValAux [Type]
ts [VerboseLevel]
ns'
              DSizeMeta{} -> WriterT Any TCM VerboseLevel
perhaps
              _ -> 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 i :: 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 x :: QName
x [Apply u :: 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 -> Elims -> 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
    _ -> 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 v :: Term
v tel0 :: Telescope
tel0 a :: 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 u :: 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
> 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 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
    _ -> () -> 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
-> Elims
-> QName
-> Elims
-> m ()
trySizeUniv cmp :: Comparison
cmp t :: CompareAs
t m :: Term
m n :: Term
n x :: QName
x els1 :: Elims
els1 y :: QName
y els2 :: Elims
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 u :: 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.
  (size :: QName
size, sizelt :: 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 size :: QName
size   _ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
     Def sizelt :: QName
sizelt _ <- 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, Elims
els1, Elims
els2) of
     -- Case @Size< _ <= Size@: true.
     (CmpLeq, [_], [])  | 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 = ∞@.
     (_, [Apply u :: 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
     (_, [], [Apply u :: 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.
     _                                             -> 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 v :: Term
v = do
  Def inf :: QName
inf [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  Def suc :: 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 v :: 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 x :: 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 x :: QName
x [Apply u :: 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 i :: 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 0
          MetaV x :: MetaId
x us :: Elims
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 -> Elims -> VerboseLevel -> DeepSizeView
DSizeMeta MetaId
x Elims
us 0
          _                          -> 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 v :: 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 v :: 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 x :: 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 x :: QName
x [Apply u :: 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 x :: QName
x [Apply u1 :: Arg Term
u1, Apply u2 :: 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 i :: 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 0
          MetaV x :: MetaId
x us :: Elims
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 -> Elims -> VerboseLevel -> DeepSizeView
DSizeMeta MetaId
x Elims
us 0
          _                             -> 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 cmp :: Comparison
cmp u :: Term
u v :: Term
v = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket "tc.conv.size" 10 "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 "tc.conv.size" 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
    [ "Comparing sizes"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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 "tc.conv.size" 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 "tc.conv.size" 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 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 cmp :: Comparison
cmp us :: SizeMaxView
us vs :: SizeMaxView
vs = case (Comparison
cmp, SizeMaxView
us, SizeMaxView
vs) of
  (CmpLeq, _, (DSizeInf :| _)) -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  (cmp :: Comparison
cmp, u :: DeepSizeView
u:|[], v :: DeepSizeView
v:|[]) -> Comparison -> DeepSizeView -> DeepSizeView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
cmp DeepSizeView
u DeepSizeView
v
  (CmpLeq, us :: SizeMaxView
us, v :: 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
$ \ u :: DeepSizeView
u -> Comparison -> DeepSizeView -> DeepSizeView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
cmp DeepSizeView
u DeepSizeView
v
  (CmpLeq, us :: SizeMaxView
us, vs :: 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
$ \ u :: DeepSizeView
u -> DeepSizeView -> SizeMaxView -> m ()
forall (m :: * -> *).
MonadConversion m =>
DeepSizeView -> SizeMaxView -> m ()
compareBelowMax DeepSizeView
u SizeMaxView
vs
  (CmpEq,  us :: SizeMaxView
us, vs :: 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 u :: DeepSizeView
u vs :: SizeMaxView
vs = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket "tc.conv.size" 45 "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 "tc.conv.size" 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 "tc.conv.size" 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
      [ "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 c1 :: m a
c1 c2 :: 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 cmp :: Comparison
cmp s1' :: DeepSizeView
s1' s2' :: DeepSizeView
s2' = do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.conv.size" 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
    [ "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 (s1 :: DeepSizeView
s1, s2 :: DeepSizeView
s2) = (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
removeSucs (DeepSizeView
s1', DeepSizeView
s2')
      withUnView :: (Term -> Term -> m b) -> m b
withUnView cont :: 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
$ \ u :: Term
u v :: 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 cmp :: 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
    (CmpLeq, _,            DSizeInf)   -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (CmpEq,  DSizeInf,     DSizeInf)   -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (CmpEq,  DSizeVar{},   DSizeInf)   -> m ()
forall b. m b
failure
    (_    ,  DSizeInf,     DSizeVar{}) -> m ()
forall b. m b
failure
    (_    ,  DSizeInf,     _         ) -> Comparison -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh VerboseLevel m) =>
Comparison -> m ()
continue Comparison
CmpEq
    (CmpLeq, DSizeVar i :: VerboseLevel
i n :: VerboseLevel
n, DSizeVar j :: VerboseLevel
j m :: 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
    (CmpLeq, DSizeVar i :: VerboseLevel
i n :: VerboseLevel
n, DSizeVar j :: VerboseLevel
j m :: 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
         BoundedNo -> m ()
forall b. m b
failure
         BoundedLt u' :: 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
> 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
- 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 1 Term
v
    (CmpLeq, s1 :: DeepSizeView
s1,        s2 :: 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
$ \ u :: Term
u v :: 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
    (CmpEq, s1 :: DeepSizeView
s1, s2 :: 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 cmp :: Comparison
cmp size :: Type
size u :: Term
u v :: 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 u :: Term
u v :: Term
v = do
    a :: (OldSizeExpr, VerboseLevel)
a@(e :: OldSizeExpr
e , n :: 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@(e' :: OldSizeExpr
e', n' :: 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 "tc.conv.size" 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 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 "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
<+> "<="
                   , (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` \_ -> 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 pid :: 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 p :: Comparison -> Bool
p c :: 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
<&> \ test :: 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 test :: 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_ _isSizeType :: Type -> Bool
_isSizeType p :: Comparison -> Bool
p Closure{ clValue :: forall a. Closure a -> a
clValue = ValueCmp cmp :: Comparison
cmp AsSizes       _ _ } = Comparison -> Bool
p Comparison
cmp
isSizeConstraint_  isSizeType :: Type -> Bool
isSizeType p :: Comparison -> Bool
p Closure{ clValue :: forall a. Closure a -> a
clValue = ValueCmp cmp :: Comparison
cmp (AsTermsOf s :: Type
s) _ _ } = Comparison -> Bool
p Comparison
cmp Bool -> Bool -> Bool
&& Type -> Bool
isSizeType Type
s
isSizeConstraint_ _isSizeType :: Type -> Bool
_isSizeType _ _ = 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 p :: 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 p :: 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 interactionMetas :: 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
$ \ m :: 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
          _ | 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 _ cmp :: Comparison
cmp a :: Type
a -> do
            TelV tel :: Telescope
tel b :: 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
$ \ _ -> 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
          _ -> 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 m :: MetaId
m _) = VerboseKey -> Doc
P.text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ "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 i :: VerboseLevel
i)      = VerboseKey -> Doc
P.text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ "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 a :: OldSizeExpr
a n :: VerboseLevel
n b :: OldSizeExpr
b)
    | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== 0    = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> "=<" 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
> 0     = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> "=<" Doc -> Doc -> Doc
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b Doc -> Doc -> Doc
P.<+> "+" 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
P.<+> VerboseKey -> Doc
P.text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (-VerboseLevel
n)) Doc -> Doc -> Doc
P.<+> "=<" 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 cs :: [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 c :: Constraint
c =
  case Constraint
c of
    ValueCmp CmpLeq _ u :: Term
u v :: Term
v -> do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size.solve" 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
          [ "converting size constraint"
          , Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c
          ]
        (a :: OldSizeExpr
a, n :: 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
        (b :: OldSizeExpr
b, m :: 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` \ err :: 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 -> TCMT IO (Maybe OldSizeConstraint)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
    _ -> 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 u :: 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 "tc.conv.size" 60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ "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
    SizeInf     -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
    SizeSuc u :: 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
+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 u :: Term
u -> case Term
u of
      Var i :: VerboseLevel
i []  -> (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
i, 0)
      MetaV m :: MetaId
m es :: Elims
es | Just xs :: [VerboseLevel]
xs <- (Elim' Term -> Maybe VerboseLevel) -> Elims -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Elim' Term -> Maybe VerboseLevel
isVar Elims
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, 0)
      _ -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
  where
    isVar :: Elim' Term -> Maybe VerboseLevel
isVar (Proj{})  = Maybe VerboseLevel
forall a. Maybe a
Nothing
    isVar (IApply _ _ v :: Term
v) = Elim' Term -> Maybe VerboseLevel
isVar (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v))
    isVar (Apply v :: Arg Term
v) = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v of
      Var i :: VerboseLevel
i [] -> VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
i
      _        -> 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 a :: OldSizeExpr
a _ b :: 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 _)       = []
    flex (SizeMeta m :: MetaId
m xs :: [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 a :: OldSizeExpr
a n :: VerboseLevel
n b :: 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 m :: MetaId
m xs :: [VerboseLevel]
xs, Rigid i :: 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 [0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-1]) VerboseLevel
n (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
j)
    (Rigid i :: VerboseLevel
i, SizeMeta m :: MetaId
m xs :: [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 [0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-1])
    (SizeMeta m :: MetaId
m xs :: [VerboseLevel]
xs, SizeMeta l :: MetaId
l ys :: [VerboseLevel]
ys)
         -- try to invert xs on ys
       | Just ys' :: [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 (\ y :: 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 [0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-1]) VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
l [VerboseLevel]
ys')
         -- try to invert ys on xs
       | Just xs' :: [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 (\ x :: 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 [0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
ysVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-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 "tc.size.solve" 70 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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 "tc.size.solve" 10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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 "tc.size.solve" 10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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 ("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
$ \ (m :: MetaId
m, _, tel :: 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 "tc.size.solve" 15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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
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 "tc.size.solve" 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
$ \ (m :: MetaId
m, _) ->
            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size.solve" 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
$ \ cl :: 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 metas :: [(MetaId, VerboseLevel)]
metas cs :: [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 (m :: a
m, ar :: 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
$ \ i :: 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 a :: OldSizeExpr
a n :: VerboseLevel
n b :: 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 i :: 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 m :: MetaId
m _) = 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
    Nothing  -> TCMT IO Bool
cannotSolve
    Just sol :: Solution
sol -> do
      VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.solve" 10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "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 v :: Term
v 0 = Term
v
          plus v :: Term
v n :: 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
- 1)

          inst :: (a, SizeExpr) -> m ()
inst (i :: a
i, e :: 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 W.Infinite) = Term
infty
                term (W.SizeVar j :: VerboseLevel
j n :: 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
- 1) VerboseLevel
n
                term _                        = 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 "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 "tc.size.solve" 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
<+> ":="
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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 W.Infinite) = Bool
True
                isInf _                        = 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