{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.SizedTypes where

import Prelude hiding (null)

import Control.Monad
import Control.Monad.Except ( MonadError(..) )
import Control.Monad.Writer ( MonadWriter(..), WriterT(..), runWriterT )

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

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

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

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

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

import Agda.Utils.Impossible

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

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

-- | Precondition: Term is reduced and not blocked.
--   Throws a 'patternViolation' if undecided
checkSizeNeverZero :: Term -> TCM Bool
checkSizeNeverZero :: Term -> TCMT IO Bool
checkSizeNeverZero Term
u = do
  SizeView
v <- Term -> TCMT IO SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
  case SizeView
v of
    SizeView
SizeInf     -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- OK, infty is never 0.
    SizeSuc{}   -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  -- OK, a + 1 is never 0.
    OtherSize Term
u ->
      case Term
u of
        Var VerboseLevel
i [] -> VerboseLevel -> TCMT IO Bool
checkSizeVarNeverZero VerboseLevel
i
        -- neutral sizes cannot be guaranteed > 0
        Term
_ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- -- | A size variable is never zero if it is the strict upper bound of
-- --   some other size variable in context.
-- --   Eg. @i : Size, j : Size< i@ |- i is never zero.
-- --   Throws a 'patternViolation' if undecided.
-- checkSizeVarNeverZero :: Int -> TCM Bool
-- checkSizeVarNeverZero i = do
--   -- Looking for a variable j : Size< i, we can restrict to the last i
--   -- entries, as this variable necessarily has been defined later than i.
--   doms <- take i <$> getContext
--   -- We raise each type to make sense in the current context.
--   let ts = zipWith raise [1..] $ map (snd . unDom) doms
--   reportSDoc "tc.size" 15 $ sep
--     [ "checking that size " <+> prettyTCM (var i) <+> " is never 0"
--     , "in context " <+> do sep $ map prettyTCM ts
--     ]
--   foldr f (return False) ts
--   where
--   f t cont = do
--     -- If we encounter a blocked type in the context, we cannot
--     -- definitely say no.
--     let yes     = return True
--         no      = cont
--         perhaps = cont >>= \ res -> if res then return res else patternViolation
--     ifBlocked t (\ _ _ -> perhaps) $ \ t -> do
--       caseMaybeM (isSizeType t) no $ \ b -> do
--         case b of
--           BoundedNo -> no
--           BoundedLt u -> ifBlocked u (\ _ _ -> perhaps) $ \ u -> do
--             case u of
--                Var i' [] | i == i' -> yes
--                _ -> no


-- | Checks that a size variable is ensured to be @> 0@.
--   E.g. variable @i@ cannot be zero in context
--   @(i : Size) (j : Size< ↑ ↑ i) (k : Size< j) (k' : Size< k)@.
--   Throws a 'patternViolation' if undecided.
checkSizeVarNeverZero :: Int -> TCM Bool
checkSizeVarNeverZero :: VerboseLevel -> TCMT IO Bool
checkSizeVarNeverZero VerboseLevel
i = do
  VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"checkSizeVarNeverZero" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
i)
  -- Looking for the minimal value for size variable i,
  -- we can restrict to the last i
  -- entries, as only these can contain i in an upper bound.
  [Type]
ts <- (Dom' Term (Name, Type) -> Type)
-> [Dom' Term (Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) ([Dom' Term (Name, Type)] -> [Type])
-> ([Dom' Term (Name, Type)] -> [Dom' Term (Name, Type)])
-> [Dom' Term (Name, Type)]
-> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel
-> [Dom' Term (Name, Type)] -> [Dom' Term (Name, Type)]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
i ([Dom' Term (Name, Type)] -> [Type])
-> TCMT IO [Dom' Term (Name, Type)] -> TCMT IO [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Dom' Term (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
getContext
  -- If we encountered a blocking meta in the context, we cannot
  -- say ``no'' for sure.
  (VerboseLevel
n, Set Blocker
blockers) <- WriterT (Set Blocker) TCM VerboseLevel
-> TCM (VerboseLevel, Set Blocker)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT (Set Blocker) TCM VerboseLevel
 -> TCM (VerboseLevel, Set Blocker))
-> WriterT (Set Blocker) TCM VerboseLevel
-> TCM (VerboseLevel, Set Blocker)
forall a b. (a -> b) -> a -> b
$ [Type] -> [VerboseLevel] -> WriterT (Set Blocker) TCM VerboseLevel
minSizeValAux [Type]
ts ([VerboseLevel] -> WriterT (Set Blocker) TCM VerboseLevel)
-> [VerboseLevel] -> WriterT (Set Blocker) TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. a -> [a]
repeat VerboseLevel
0
  let blocker :: Blocker
blocker = Set Blocker -> Blocker
unblockOnAll Set Blocker
blockers
  if VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else
    if Blocker
blocker Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock
      then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      else Blocker -> TCMT IO Bool
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
blocker
  where
  -- Compute the least valuation for size context ts above the
  -- given valuation and return its last value.
  minSizeValAux :: [Type] -> [Int] -> WriterT (Set Blocker) TCM Int
  minSizeValAux :: [Type] -> [VerboseLevel] -> WriterT (Set Blocker) TCM VerboseLevel
minSizeValAux [Type]
_        []      = WriterT (Set Blocker) TCM VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__
  minSizeValAux []       (VerboseLevel
n : [VerboseLevel]
_) = VerboseLevel -> WriterT (Set Blocker) TCM VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseLevel
n
  minSizeValAux (Type
t : [Type]
ts) (VerboseLevel
n : [VerboseLevel]
ns) = do
    VerboseKey
-> VerboseLevel -> TCM Doc -> WriterT (Set Blocker) TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size" VerboseLevel
60 (TCM Doc -> WriterT (Set Blocker) TCM ())
-> TCM Doc -> WriterT (Set Blocker) TCM ()
forall a b. (a -> b) -> a -> b
$
       VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text (VerboseKey
"minSizeVal (n:ns) = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [VerboseLevel] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. VerboseLevel -> [a] -> [a]
take ([Type] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Type]
ts VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
2) ([VerboseLevel] -> [VerboseLevel])
-> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ VerboseLevel
nVerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. a -> [a] -> [a]
:[VerboseLevel]
ns) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
             VerboseKey
" t =") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative 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 (Set Blocker) TCM VerboseLevel
cont = [Type] -> [VerboseLevel] -> WriterT (Set Blocker) TCM VerboseLevel
minSizeValAux [Type]
ts [VerboseLevel]
ns
        perhaps :: Blocker -> WriterT (Set Blocker) TCM VerboseLevel
perhaps Blocker
x = Set Blocker -> WriterT (Set Blocker) TCM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Blocker -> Set Blocker
forall a. a -> Set a
Set.singleton Blocker
x) WriterT (Set Blocker) TCM ()
-> WriterT (Set Blocker) TCM VerboseLevel
-> WriterT (Set Blocker) TCM VerboseLevel
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriterT (Set Blocker) TCM VerboseLevel
cont
    -- If we encounter a blocked type in the context, we cannot
    -- give a definite answer.
    Type
-> (Blocker -> Type -> WriterT (Set Blocker) TCM VerboseLevel)
-> (NotBlocked -> Type -> WriterT (Set Blocker) TCM VerboseLevel)
-> WriterT (Set Blocker) TCM VerboseLevel
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
x Type
_ -> Blocker -> WriterT (Set Blocker) TCM VerboseLevel
perhaps Blocker
x) ((NotBlocked -> Type -> WriterT (Set Blocker) TCM VerboseLevel)
 -> WriterT (Set Blocker) TCM VerboseLevel)
-> (NotBlocked -> Type -> WriterT (Set Blocker) TCM VerboseLevel)
-> WriterT (Set Blocker) TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
      WriterT (Set Blocker) TCM (Maybe BoundedSize)
-> WriterT (Set Blocker) TCM VerboseLevel
-> (BoundedSize -> WriterT (Set Blocker) TCM VerboseLevel)
-> WriterT (Set Blocker) TCM VerboseLevel
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCMT IO (Maybe BoundedSize)
-> WriterT (Set Blocker) TCM (Maybe BoundedSize)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (Maybe BoundedSize)
 -> WriterT (Set Blocker) TCM (Maybe BoundedSize))
-> TCMT IO (Maybe BoundedSize)
-> WriterT (Set Blocker) 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 (Set Blocker) TCM VerboseLevel
cont ((BoundedSize -> WriterT (Set Blocker) TCM VerboseLevel)
 -> WriterT (Set Blocker) TCM VerboseLevel)
-> (BoundedSize -> WriterT (Set Blocker) TCM VerboseLevel)
-> WriterT (Set Blocker) TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ \ BoundedSize
b -> do
        case BoundedSize
b of
          BoundedSize
BoundedNo -> WriterT (Set Blocker) TCM VerboseLevel
cont
          BoundedLt Term
u -> Term
-> (Blocker -> Term -> WriterT (Set Blocker) TCM VerboseLevel)
-> (NotBlocked -> Term -> WriterT (Set Blocker) TCM VerboseLevel)
-> WriterT (Set Blocker) TCM VerboseLevel
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
u (\ Blocker
x Term
_ -> Blocker -> WriterT (Set Blocker) TCM VerboseLevel
perhaps Blocker
x) ((NotBlocked -> Term -> WriterT (Set Blocker) TCM VerboseLevel)
 -> WriterT (Set Blocker) TCM VerboseLevel)
-> (NotBlocked -> Term -> WriterT (Set Blocker) TCM VerboseLevel)
-> WriterT (Set Blocker) TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
u -> do
            VerboseKey
-> VerboseLevel -> VerboseKey -> WriterT (Set Blocker) TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size" VerboseLevel
60 (VerboseKey -> WriterT (Set Blocker) TCM ())
-> VerboseKey -> WriterT (Set Blocker) TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"minSizeVal upper bound u = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show Term
u
            DeepSizeView
v <- TCM DeepSizeView -> WriterT (Set Blocker) TCM DeepSizeView
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM DeepSizeView -> WriterT (Set Blocker) TCM DeepSizeView)
-> TCM DeepSizeView -> WriterT (Set Blocker) TCM DeepSizeView
forall a b. (a -> b) -> a -> b
$ Term -> TCM DeepSizeView
forall (m :: * -> *).
(PureTCM m, MonadTCError m) =>
Term -> m DeepSizeView
deepSizeView Term
u
            case DeepSizeView
v of
              -- Variable 0 has bound @(< j + m)@
              -- meaning that @minval(j) > n - m@, i.e., @minval(j) >= n+1-m@.
              -- Thus, we update the min value for @j@ with function @(max (n+1-m))@.
              DSizeVar (ProjectedVar VerboseLevel
j []) VerboseLevel
m -> do
                VerboseKey
-> VerboseLevel -> VerboseKey -> WriterT (Set Blocker) TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size" VerboseLevel
60 (VerboseKey -> WriterT (Set Blocker) TCM ())
-> VerboseKey -> WriterT (Set Blocker) TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"minSizeVal upper bound v = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ DeepSizeView -> VerboseKey
forall a. Show a => a -> VerboseKey
show DeepSizeView
v
                let ns' :: [VerboseLevel]
ns' = VerboseLevel
-> (VerboseLevel -> VerboseLevel)
-> [VerboseLevel]
-> [VerboseLevel]
forall a. VerboseLevel -> (a -> a) -> [a] -> [a]
List.updateAt VerboseLevel
j (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Ord a => a -> a -> a
max (VerboseLevel -> VerboseLevel -> VerboseLevel)
-> VerboseLevel -> VerboseLevel -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ VerboseLevel
nVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
1VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
m) [VerboseLevel]
ns
                VerboseKey
-> VerboseLevel -> VerboseKey -> WriterT (Set Blocker) TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"tc.size" VerboseLevel
60 (VerboseKey -> WriterT (Set Blocker) TCM ())
-> VerboseKey -> WriterT (Set Blocker) TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"minSizeVal ns' = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [VerboseLevel] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. VerboseLevel -> [a] -> [a]
take ([Type] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Type]
ts VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1) [VerboseLevel]
ns')
                [Type] -> [VerboseLevel] -> WriterT (Set Blocker) TCM VerboseLevel
minSizeValAux [Type]
ts [VerboseLevel]
ns'
              DSizeMeta MetaId
x [Elim]
_ VerboseLevel
_ -> Blocker -> WriterT (Set Blocker) TCM VerboseLevel
perhaps (MetaId -> Blocker
unblockOnMeta MetaId
x)
              DeepSizeView
_ -> WriterT (Set Blocker) 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 :: PureTCM m => Nat -> m BoundedSize
isBounded :: VerboseLevel -> m BoundedSize
isBounded VerboseLevel
i = Type -> m BoundedSize
forall (m :: * -> *). PureTCM m => Type -> m BoundedSize
isBoundedSizeType (Type -> m BoundedSize) -> m Type -> m BoundedSize
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseLevel -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i

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

isBoundedSizeType :: PureTCM m => Type -> m BoundedSize
isBoundedSizeType :: Type -> m BoundedSize
isBoundedSizeType Type
t =
  Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) m Term -> (Term -> m BoundedSize) -> m BoundedSize
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Def QName
x [Apply Arg Term
u] -> do
      Maybe Term
sizelt <- VerboseKey -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getBuiltin' VerboseKey
builtinSizeLt
      BoundedSize -> m BoundedSize
forall (m :: * -> *) a. Monad m => a -> m a
return (BoundedSize -> m BoundedSize) -> BoundedSize -> m BoundedSize
forall a b. (a -> b) -> a -> b
$ if (Term -> Maybe Term
forall a. a -> Maybe a
Just (QName -> [Elim] -> Term
Def QName
x []) Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Term
sizelt) then Term -> BoundedSize
BoundedLt (Term -> BoundedSize) -> Term -> BoundedSize
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u else BoundedSize
BoundedNo
    Term
_ -> BoundedSize -> m BoundedSize
forall (m :: * -> *) a. Monad m => a -> m a
return BoundedSize
BoundedNo

-- | Whenever we create a bounded size meta, add a constraint
--   expressing the bound. First argument is the new meta and must be a @MetaV{}@.
--   In @boundedSizeMetaHook v tel a@, @tel@ includes the current context.
boundedSizeMetaHook
  :: ( MonadConstraint m
     , MonadTCEnv m
     , ReadTCState m
     , MonadAddContext m
     , HasOptions m
     , HasBuiltins m
     )
  => Term -> Telescope -> Type -> m ()
boundedSizeMetaHook :: Term -> Telescope -> Type -> m ()
boundedSizeMetaHook v :: Term
v@(MetaV MetaId
x [Elim]
_) Telescope
tel0 Type
a = do
  Maybe BoundedSize
res <- Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
a
  case Maybe BoundedSize
res of
    Just (BoundedLt Term
u) -> do
      VerboseLevel
n <- m VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
      let tel :: Telescope
tel | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0     = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> ListTel -> ListTel
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
n (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
tel0
              | Bool
otherwise = Telescope
tel0
      Telescope -> m () -> m ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        Term
v <- VerboseLevel -> Term -> m Term
forall (m :: * -> *).
HasBuiltins m =>
VerboseLevel -> Term -> m Term
sizeSuc VerboseLevel
1 (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term -> Term
forall a. Subst 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
        Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (MetaId -> Blocker
unblockOnMeta MetaId
x) (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpLeq CompareAs
AsSizes Term
v Term
u
    Maybe BoundedSize
_ -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
boundedSizeMetaHook Term
_ Telescope
_ Type
_ = m ()
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | @trySizeUniv cmp t m n x els1 y els2@
--   is called as a last resort when conversion checking @m `cmp` n : t@
--   failed for definitions @m = x els1@ and @n = y els2@,
--   where the heads @x@ and @y@ are not equal.
--
--   @trySizeUniv@ accounts for subtyping between SIZELT and SIZE,
--   like @Size< i =< Size@.
--
--   If it does not succeed it reports failure of conversion check.
trySizeUniv
  :: MonadConversion m
  => Comparison -> CompareAs -> Term -> Term
  -> QName -> Elims -> QName -> Elims -> m ()
trySizeUniv :: Comparison
-> CompareAs
-> Term
-> Term
-> QName
-> [Elim]
-> QName
-> [Elim]
-> m ()
trySizeUniv Comparison
cmp CompareAs
t Term
m Term
n QName
x [Elim]
els1 QName
y [Elim]
els2 = do
  let failure :: forall m a. MonadTCError m => m a
      failure :: m a
failure = TypeError -> m a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
m Term
n CompareAs
t
      forceInfty :: Arg Term -> m ()
forceInfty Arg Term
u = Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
CmpEq (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u) (Term -> m ()) -> m Term -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  -- Get the SIZE built-ins.
  (QName
size, QName
sizelt) <- (m (QName, QName)
 -> (TCErr -> m (QName, QName)) -> m (QName, QName))
-> (TCErr -> m (QName, QName))
-> m (QName, QName)
-> m (QName, QName)
forall a b c. (a -> b -> c) -> b -> a -> c
flip m (QName, QName) -> (TCErr -> m (QName, QName)) -> m (QName, QName)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (m (QName, QName) -> TCErr -> m (QName, QName)
forall a b. a -> b -> a
const m (QName, QName)
forall (m :: * -> *) a. MonadTCError m => m a
failure) (m (QName, QName) -> m (QName, QName))
-> m (QName, QName) -> m (QName, QName)
forall a b. (a -> b) -> a -> b
$ do
     Def QName
size   [Elim]
_ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
     Def QName
sizelt [Elim]
_ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeLt
     (QName, QName) -> m (QName, QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
size, QName
sizelt)
  case (Comparison
cmp, [Elim]
els1, [Elim]
els2) of
     -- Case @Size< _ <= Size@: true.
     (Comparison
CmpLeq, [Elim
_], [])  | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
size -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     -- Case @Size< u = Size@: forces @u = ∞@.
     (Comparison
_, [Apply Arg Term
u], []) | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
size -> Arg Term -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh VerboseLevel m) =>
Arg Term -> m ()
forceInfty Arg Term
u
     (Comparison
_, [], [Apply Arg Term
u]) | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
size Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt -> Arg Term -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh VerboseLevel m) =>
Arg Term -> m ()
forceInfty Arg Term
u
     -- This covers all cases for SIZE and SIZELT.
     -- The remaining case is for @x@ and @y@ which are not size built-ins.
     (Comparison, [Elim], [Elim])
_                                             -> m ()
forall (m :: * -> *) a. MonadTCError m => m a
failure

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

-- | Compute the deep size view of a term.
--   Precondition: sized types are enabled.
deepSizeView :: (PureTCM m, MonadTCError m) => Term -> m DeepSizeView
deepSizeView :: Term -> m DeepSizeView
deepSizeView Term
v = do
  Def QName
inf [] <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  Def QName
suc [] <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
  let loop :: Term -> m DeepSizeView
loop Term
v =
        Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v m Term -> (Term -> m DeepSizeView) -> m DeepSizeView
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Def QName
x []        | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
inf -> DeepSizeView -> m DeepSizeView
forall (m :: * -> *) a. Monad m => a -> m a
return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
forall a b. (a -> b) -> a -> b
$ DeepSizeView
DSizeInf
          Def QName
x [Apply Arg Term
u] | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
suc -> QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ QName
suc (DeepSizeView -> DeepSizeView) -> m DeepSizeView -> m DeepSizeView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m DeepSizeView
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u)

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

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

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

-- | Compare two sizes.
compareSizes :: (MonadConversion m) => Comparison -> Term -> Term -> m ()
compareSizes :: Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u Term
v = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.conv.size" VerboseLevel
10 VerboseKey
"compareSizes" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
10 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCM Doc
"Comparing sizes"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Comparison -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp
                   , Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
                   ]
    ]
  VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS VerboseKey
"tc.conv.size" VerboseLevel
60 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    Term
u <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
    Term
v <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
      VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ Term -> TCM Doc
forall (m :: * -> *) a. (Applicative 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. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
                   ]
  SizeMaxView
us <- Term -> m SizeMaxView
forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
sizeMaxView Term
u
  SizeMaxView
vs <- Term -> m SizeMaxView
forall (m :: * -> *). PureTCM m => Term -> m SizeMaxView
sizeMaxView Term
v
  Comparison -> SizeMaxView -> SizeMaxView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> SizeMaxView -> SizeMaxView -> m ()
compareMaxViews Comparison
cmp SizeMaxView
us SizeMaxView
vs

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

-- | @compareBelowMax u vs@ checks @u <= max vs@.  Precondition: @size vs >= 2@
compareBelowMax :: (MonadConversion m) => DeepSizeView -> SizeMaxView -> m ()
compareBelowMax :: DeepSizeView -> SizeMaxView -> m ()
compareBelowMax DeepSizeView
u SizeMaxView
vs = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket VerboseKey
"tc.conv.size" VerboseLevel
45 VerboseKey
"compareBelowMax" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
45 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
    [ DeepSizeView -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeepSizeView
u
    , Comparison -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Comparison
CmpLeq
    , SizeMaxView -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty SizeMaxView
vs
    ]
  -- When trying several alternatives, we do not assign metas
  -- and also do not produce constraints (see 'giveUp' below).
  -- Andreas, 2019-03-28, issue #3600.
  m () -> m () -> m ()
forall b (m :: * -> *) a. MonadError b m => m a -> m a -> m a
alt (m () -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ (m () -> m () -> m ()) -> NonEmpty (m ()) -> m ()
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
Fold.foldr1 m () -> m () -> m ()
forall b (m :: * -> *) a. MonadError b m => m a -> m a -> m a
alt (NonEmpty (m ()) -> m ()) -> NonEmpty (m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ (DeepSizeView -> m ()) -> SizeMaxView -> NonEmpty (m ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Comparison -> DeepSizeView -> DeepSizeView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
CmpLeq DeepSizeView
u) SizeMaxView
vs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
45 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCM Doc
"compareBelowMax: giving up"
      ]
    Term
u <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
u
    Term
v <- SizeMaxView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
SizeMaxView -> m Term
unMaxView SizeMaxView
vs
    Type
size <- m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
    Comparison -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
giveUp Comparison
CmpLeq Type
size Term
u Term
v
  where
  alt :: m a -> m a -> m a
alt m a
c1 m a
c2 = m a
c1 m a -> (b -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` m a -> b -> m a
forall a b. a -> b -> a
const m a
c2

compareSizeViews :: (MonadConversion m) => Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
cmp DeepSizeView
s1' DeepSizeView
s2' = do
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
45 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
    [ TCM Doc
"compareSizeViews"
    , DeepSizeView -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeepSizeView
s1'
    , Comparison -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Comparison
cmp
    , DeepSizeView -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeepSizeView
s2'
    ]
  Type
size <- m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
  let (DeepSizeView
s1, DeepSizeView
s2) = (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
removeSucs (DeepSizeView
s1', DeepSizeView
s2')
      withUnView :: (Term -> Term -> m ()) -> m ()
withUnView Term -> Term -> m ()
cont = do
        Term
u <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s1
        Term
v <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s2
        Term -> Term -> m ()
cont Term
u Term
v
      failure :: m ()
failure = (Term -> Term -> m ()) -> m ()
withUnView ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Term
u Term
v -> TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
u Term
v CompareAs
AsSizes
      continue :: Comparison -> m ()
continue Comparison
cmp = (Term -> Term -> m ()) -> m ()
withUnView ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom Comparison
cmp CompareAs
AsSizes
  case (Comparison
cmp, DeepSizeView
s1, DeepSizeView
s2) of
    (Comparison
CmpLeq, DeepSizeView
_,            DeepSizeView
DSizeInf)   -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Comparison
CmpEq,  DeepSizeView
DSizeInf,     DeepSizeView
DSizeInf)   -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Comparison
CmpEq,  DSizeVar{},   DeepSizeView
DSizeInf)   -> m ()
failure
    (Comparison
_    ,  DeepSizeView
DSizeInf,     DSizeVar{}) -> m ()
failure
    (Comparison
_    ,  DeepSizeView
DSizeInf,     DeepSizeView
_         ) -> Comparison -> m ()
continue Comparison
CmpEq
    (Comparison
CmpLeq, DSizeVar ProjectedVar
i VerboseLevel
n, DSizeVar ProjectedVar
j VerboseLevel
m) | ProjectedVar
i ProjectedVar -> ProjectedVar -> Bool
forall a. Eq a => a -> a -> Bool
== ProjectedVar
j -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
m) m ()
failure
    (Comparison
CmpLeq, DSizeVar ProjectedVar
i VerboseLevel
n, DSizeVar ProjectedVar
j VerboseLevel
m) | ProjectedVar
i ProjectedVar -> ProjectedVar -> Bool
forall a. Eq a => a -> a -> Bool
/= ProjectedVar
j -> do
       BoundedSize
res <- ProjectedVar -> m BoundedSize
forall (m :: * -> *).
(MonadCheckInternal m, PureTCM m) =>
ProjectedVar -> m BoundedSize
isBoundedProjVar ProjectedVar
i
       case BoundedSize
res of
         BoundedSize
BoundedNo -> m ()
failure
         BoundedLt Term
u' -> do
            -- now we have i < u', in the worst case i+1 = u'
            -- and we want to check i+n <= v
            Term
v <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s2
            if VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0 then do
              Term
u'' <- VerboseLevel -> Term -> m Term
forall (m :: * -> *).
HasBuiltins m =>
VerboseLevel -> Term -> m Term
sizeSuc (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1) Term
u'
              Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u'' Term
v
             else Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u' (Term -> m ()) -> m Term -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseLevel -> Term -> m Term
forall (m :: * -> *).
HasBuiltins m =>
VerboseLevel -> Term -> m Term
sizeSuc VerboseLevel
1 Term
v
    (Comparison
CmpLeq, DeepSizeView
s1,        DeepSizeView
s2)         -> (Term -> Term -> m ()) -> m ()
withUnView ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ Term
u Term
v -> do
      m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Term -> Term -> m Bool
forall (m :: * -> *). MonadConversion m => Term -> Term -> m Bool
trivial Term
u Term
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
giveUp Comparison
CmpLeq Type
size Term
u Term
v
    (Comparison
CmpEq, DeepSizeView
s1, DeepSizeView
s2) -> Comparison -> m ()
continue Comparison
cmp

-- | If 'envAssignMetas' then postpone as constraint, otherwise, fail hard.
--   Failing is required if we speculatively test several alternatives.
giveUp :: (MonadConversion m) => Comparison -> Type -> Term -> Term -> m ()
giveUp :: Comparison -> Type -> Term -> Term -> m ()
giveUp Comparison
cmp Type
size Term
u Term
v =
  m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas)
    {-then-} (Blocker -> Constraint -> m ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
unblock (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpLeq CompareAs
AsSizes Term
u Term
v)
    {-else-} (TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
u Term
v CompareAs
AsSizes)
  where
    unblock :: Blocker
unblock = [Term] -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn [Term
u, Term
v]

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

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

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

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

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

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

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

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

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

{- ROLLED BACK
getSizeMetas :: TCM ([(MetaId, Int)], [SizeConstraint])
getSizeMetas = do
  ms <- getOpenMetas
  test <- isSizeTypeTest
  let sizeCon m = do
        let nothing  = return ([], [])
        mi <- lookupMeta m
        case mvJudgement mi of
          HasType _ a -> do
            TelV tel b <- telView =<< instantiateFull a
            let noConstr = return ([(m, size tel)], [])
            case test b of
              Nothing            -> nothing
              Just BoundedNo     -> noConstr
              Just (BoundedLt u) -> noConstr
{- WORKS NOT
              Just (BoundedLt u) -> flip catchError (const $ noConstr) $ do
                -- we assume the metavariable is used in an
                -- extension of its creation context
                ctxIds <- getContextId
                let a = SizeMeta m $ take (size tel) $ reverse ctxIds
                (b, n) <- oldSizeExpr u
                return ([(m, size tel)], [Leq a (n-1) b])
-}
          _ -> nothing
  (mss, css) <- unzip <$> mapM sizeCon ms
  return (concat mss, concat css)
-}

------------------------------------------------------------------------
-- * Size constraint solving.
------------------------------------------------------------------------

-- | Atomic size expressions.
data OldSizeExpr
  = SizeMeta MetaId [Int] -- ^ A size meta applied to de Bruijn indices.
  | Rigid Int             -- ^ A de Bruijn index.
  deriving (OldSizeExpr -> OldSizeExpr -> Bool
(OldSizeExpr -> OldSizeExpr -> Bool)
-> (OldSizeExpr -> OldSizeExpr -> Bool) -> Eq OldSizeExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OldSizeExpr -> OldSizeExpr -> Bool
$c/= :: OldSizeExpr -> OldSizeExpr -> Bool
== :: OldSizeExpr -> OldSizeExpr -> Bool
$c== :: OldSizeExpr -> OldSizeExpr -> Bool
Eq, VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey
[OldSizeExpr] -> VerboseKey -> VerboseKey
OldSizeExpr -> VerboseKey
(VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey)
-> (OldSizeExpr -> VerboseKey)
-> ([OldSizeExpr] -> VerboseKey -> VerboseKey)
-> Show OldSizeExpr
forall a.
(VerboseLevel -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [OldSizeExpr] -> VerboseKey -> VerboseKey
$cshowList :: [OldSizeExpr] -> VerboseKey -> VerboseKey
show :: OldSizeExpr -> VerboseKey
$cshow :: OldSizeExpr -> VerboseKey
showsPrec :: VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey
$cshowsPrec :: VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey
Show)

instance Pretty OldSizeExpr where
  pretty :: OldSizeExpr -> Doc
pretty (SizeMeta MetaId
m [VerboseLevel]
_) = VerboseKey -> Doc
P.text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"X" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (MetaId -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral MetaId
m :: Int)
  pretty (Rigid VerboseLevel
i)      = VerboseKey -> Doc
P.text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ VerboseKey
"c" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
i

-- | Size constraints we can solve.
data OldSizeConstraint
  = Leq OldSizeExpr Int OldSizeExpr
    -- ^ @Leq a +n b@ represents @a =< b + n@.
    --   @Leq a -n b@ represents @a + n =< b@.
  deriving (VerboseLevel -> OldSizeConstraint -> VerboseKey -> VerboseKey
[OldSizeConstraint] -> VerboseKey -> VerboseKey
OldSizeConstraint -> VerboseKey
(VerboseLevel -> OldSizeConstraint -> VerboseKey -> VerboseKey)
-> (OldSizeConstraint -> VerboseKey)
-> ([OldSizeConstraint] -> VerboseKey -> VerboseKey)
-> Show OldSizeConstraint
forall a.
(VerboseLevel -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [OldSizeConstraint] -> VerboseKey -> VerboseKey
$cshowList :: [OldSizeConstraint] -> VerboseKey -> VerboseKey
show :: OldSizeConstraint -> VerboseKey
$cshow :: OldSizeConstraint -> VerboseKey
showsPrec :: VerboseLevel -> OldSizeConstraint -> VerboseKey -> VerboseKey
$cshowsPrec :: VerboseLevel -> OldSizeConstraint -> VerboseKey -> VerboseKey
Show)

instance Pretty OldSizeConstraint where
  pretty :: OldSizeConstraint -> Doc
pretty (Leq OldSizeExpr
a VerboseLevel
n OldSizeExpr
b)
    | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
0    = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> Doc
"=<" Doc -> Doc -> Doc
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b
    | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> VerboseLevel
0     = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> Doc
"=<" Doc -> Doc -> Doc
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b Doc -> Doc -> Doc
P.<+> Doc
"+" Doc -> Doc -> Doc
P.<+> VerboseKey -> Doc
P.text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
n)
    | Bool
otherwise = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> Doc
"+" Doc -> Doc -> Doc
P.<+> VerboseKey -> Doc
P.text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (-VerboseLevel
n)) Doc -> Doc -> Doc
P.<+> Doc
"=<" Doc -> Doc -> Doc
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b

-- | Compute a set of size constraints that all live in the same context
--   from constraints over terms of type size that may live in different
--   contexts.
--
--   cf. 'Agda.TypeChecking.LevelConstraints.simplifyLevelConstraint'
oldComputeSizeConstraints :: [ProblemConstraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints :: [ProblemConstraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [] = [OldSizeConstraint] -> TCM [OldSizeConstraint]
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- special case to avoid maximum []
oldComputeSizeConstraints [ProblemConstraint]
cs = [Maybe OldSizeConstraint] -> [OldSizeConstraint]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe OldSizeConstraint] -> [OldSizeConstraint])
-> TCMT IO [Maybe OldSizeConstraint] -> TCM [OldSizeConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint -> TCMT IO (Maybe OldSizeConstraint))
-> [Constraint] -> TCMT IO [Maybe OldSizeConstraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Constraint -> TCMT IO (Maybe OldSizeConstraint)
oldComputeSizeConstraint [Constraint]
leqs
  where
    -- get the constraints plus contexts they are defined in
    gammas :: [[Dom' Term (Name, Type)]]
gammas       = (ProblemConstraint -> [Dom' Term (Name, Type)])
-> [ProblemConstraint] -> [[Dom' Term (Name, Type)]]
forall a b. (a -> b) -> [a] -> [b]
map (TCEnv -> [Dom' Term (Name, Type)]
envContext (TCEnv -> [Dom' Term (Name, Type)])
-> (ProblemConstraint -> TCEnv)
-> ProblemConstraint
-> [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 -> TCEnv)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) [ProblemConstraint]
cs
    ls :: [Constraint]
ls           = (ProblemConstraint -> Constraint)
-> [ProblemConstraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) [ProblemConstraint]
cs
    -- compute the longest context (common water level)
    ns :: [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 a. Subst a => VerboseLevel -> a -> a
raise ((VerboseLevel -> VerboseLevel) -> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel
waterLevel VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-) [VerboseLevel]
ns) [Constraint]
ls

-- | Turn a constraint over de Bruijn indices into a size constraint.
oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint)
oldComputeSizeConstraint :: Constraint -> TCMT IO (Maybe OldSizeConstraint)
oldComputeSizeConstraint Constraint
c =
  case Constraint
c of
    ValueCmp Comparison
CmpLeq CompareAs
_ Term
u Term
v -> do
        VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size.solve" VerboseLevel
50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCM Doc
"converting size constraint"
          , Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c
          ]
        (OldSizeExpr
a, VerboseLevel
n) <- Term -> TCMT IO (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
u
        (OldSizeExpr
b, VerboseLevel
m) <- Term -> TCMT IO (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
v
        Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint))
-> Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
forall a b. (a -> b) -> a -> b
$ OldSizeConstraint -> Maybe OldSizeConstraint
forall a. a -> Maybe a
Just (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq OldSizeExpr
a (VerboseLevel
m VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
n) OldSizeExpr
b
      TCMT IO (Maybe OldSizeConstraint)
-> (TCErr -> TCMT IO (Maybe OldSizeConstraint))
-> TCMT IO (Maybe OldSizeConstraint)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> case TCErr
err of
        PatternErr{} -> Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe OldSizeConstraint
forall a. Maybe a
Nothing
        TCErr
_            -> TCErr -> TCMT IO (Maybe OldSizeConstraint)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
    Constraint
_ -> TCMT IO (Maybe OldSizeConstraint)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Turn a term with de Bruijn indices into a size expression with offset.
--
--   Throws a 'patternViolation' if the term isn't a proper size expression.
oldSizeExpr :: (PureTCM m, MonadBlock m) => Term -> m (OldSizeExpr, Int)
oldSizeExpr :: Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
u = do
  Term
u <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u -- Andreas, 2009-02-09.
                -- This is necessary to surface the solutions of metavariables.
  VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.conv.size" VerboseLevel
60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"oldSizeExpr:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
  SizeView
s <- Term -> m SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
  case SizeView
s of
    SizeView
SizeInf     -> Blocker -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
    SizeSuc Term
u   -> (VerboseLevel -> VerboseLevel)
-> (OldSizeExpr, VerboseLevel) -> (OldSizeExpr, VerboseLevel)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+VerboseLevel
1) ((OldSizeExpr, VerboseLevel) -> (OldSizeExpr, VerboseLevel))
-> m (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
u
    OtherSize Term
u -> case Term
u of
      Var VerboseLevel
i []  -> (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
i, VerboseLevel
0)
      MetaV MetaId
m [Elim]
es | Just [VerboseLevel]
xs <- (Elim -> Maybe VerboseLevel) -> [Elim] -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Elim -> Maybe VerboseLevel
isVar [Elim]
es, [VerboseLevel] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [VerboseLevel]
xs
                -> (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel]
xs, VerboseLevel
0)
      Term
_ -> Blocker -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
  where
    isVar :: Elim -> Maybe VerboseLevel
isVar (Proj{})  = Maybe VerboseLevel
forall a. Maybe a
Nothing
    isVar (IApply Term
_ Term
_ Term
v) = Elim -> Maybe VerboseLevel
isVar (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v))
    isVar (Apply Arg Term
v) = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v of
      Var VerboseLevel
i [] -> VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
i
      Term
_        -> Maybe VerboseLevel
forall a. Maybe a
Nothing

-- | Compute list of size metavariables with their arguments
--   appearing in a constraint.
flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
flexibleVariables :: OldSizeConstraint -> [(MetaId, [VerboseLevel])]
flexibleVariables (Leq OldSizeExpr
a VerboseLevel
_ OldSizeExpr
b) = OldSizeExpr -> [(MetaId, [VerboseLevel])]
flex OldSizeExpr
a [(MetaId, [VerboseLevel])]
-> [(MetaId, [VerboseLevel])] -> [(MetaId, [VerboseLevel])]
forall a. [a] -> [a] -> [a]
++ OldSizeExpr -> [(MetaId, [VerboseLevel])]
flex OldSizeExpr
b
  where
    flex :: OldSizeExpr -> [(MetaId, [VerboseLevel])]
flex (Rigid VerboseLevel
_)       = []
    flex (SizeMeta MetaId
m [VerboseLevel]
xs) = [(MetaId
m, [VerboseLevel]
xs)]

-- | Convert size constraint into form where each meta is applied
--   to indices @0,1,..,n-1@ where @n@ is the arity of that meta.
--
--   @X[σ] <= t@ becomes @X[id] <= t[σ^-1]@
--
--   @X[σ] ≤ Y[τ]@ becomes @X[id] ≤ Y[τ[σ^-1]]@ or @X[σ[τ^1]] ≤ Y[id]@
--   whichever is defined.  If none is defined, we give up.
--
oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint
oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint
oldCanonicalizeSizeConstraint c :: OldSizeConstraint
c@(Leq OldSizeExpr
a VerboseLevel
n OldSizeExpr
b) =
  case (OldSizeExpr
a,OldSizeExpr
b) of
    (Rigid{}, Rigid{})       -> OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return OldSizeConstraint
c
    (SizeMeta MetaId
m [VerboseLevel]
xs, Rigid VerboseLevel
i) -> do
      VerboseLevel
j <- VerboseLevel -> [VerboseLevel] -> Maybe VerboseLevel
forall a. Eq a => a -> [a] -> Maybe VerboseLevel
List.elemIndex VerboseLevel
i [VerboseLevel]
xs
      OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel
0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1]) VerboseLevel
n (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
j)
    (Rigid VerboseLevel
i, SizeMeta MetaId
m [VerboseLevel]
xs) -> do
      VerboseLevel
j <- VerboseLevel -> [VerboseLevel] -> Maybe VerboseLevel
forall a. Eq a => a -> [a] -> Maybe VerboseLevel
List.elemIndex VerboseLevel
i [VerboseLevel]
xs
      OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
j) VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel
0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1])
    (SizeMeta MetaId
m [VerboseLevel]
xs, SizeMeta MetaId
l [VerboseLevel]
ys)
         -- try to invert xs on ys
       | Just [VerboseLevel]
ys' <- (VerboseLevel -> Maybe VerboseLevel)
-> [VerboseLevel] -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ VerboseLevel
y -> VerboseLevel -> [VerboseLevel] -> Maybe VerboseLevel
forall a. Eq a => a -> [a] -> Maybe VerboseLevel
List.elemIndex VerboseLevel
y [VerboseLevel]
xs) [VerboseLevel]
ys ->
           OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel
0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1]) VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
l [VerboseLevel]
ys')
         -- try to invert ys on xs
       | Just [VerboseLevel]
xs' <- (VerboseLevel -> Maybe VerboseLevel)
-> [VerboseLevel] -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ VerboseLevel
x -> VerboseLevel -> [VerboseLevel] -> Maybe VerboseLevel
forall a. Eq a => a -> [a] -> Maybe VerboseLevel
List.elemIndex VerboseLevel
x [VerboseLevel]
ys) [VerboseLevel]
xs ->
           OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel]
xs') VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
l [VerboseLevel
0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
ysVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1])
         -- give up
       | Bool
otherwise -> Maybe OldSizeConstraint
forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

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

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

    -- Double-checking the solution.

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


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

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

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

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

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

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

            VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"tc.size.solve" VerboseLevel
20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
              [ MetaId -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":="
              , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
              ]

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