{-# LANGUAGE NondecreasingIndentation #-}

-- | Solving size constraints under hypotheses.
--
-- The size solver proceeds as follows:
--
-- 1. Get size constraints, cluster into connected components.
--
--    All size constraints that mention the same metas go into the same
--    cluster.  Each cluster can be solved by itself.
--
--    Constraints that do not fit our format are ignored.
--    We check whether our computed solution fulfills them as well
--    in the last step.
--
-- 2. Find a joint context for each cluster.
--
--    Each constraint comes with its own typing context, which
--    contains size hypotheses @j : Size< i@.  We need to find a
--    common super context in which all constraints of a cluster live,
--    and raise all constraints to this context.
--
--    There might not be a common super context.  Then we are screwed,
--    since our solver is not ready to deal with such a situation.  We
--    will blatantly refuse to solve this cluster and blame it on the
--    user.
--
-- 3. Convert the joint context into a hypothesis graph.
--
--    This is straightforward.  Each de Bruijn index becomes a
--    rigid variable, each typing assumption @j : Size< i@ becomes an
--    arc.
--
-- 4. Convert the constraints into a constraint graph.
--
--    Here we need to convert @MetaV@s into flexible variables.
--
-- 5. Run the solver
--
-- 6. Convert the solution into meta instantiations.
--
-- 7. Double-check whether the constraints are solved.

-- Opportunities for optimization:
--
-- - NamedRigids has some cost to retrieve variable names
--   just for the sake of debug printing.

module Agda.TypeChecking.SizedTypes.Solve where

import Prelude hiding (null)

import Control.Monad.Except ( catchError )
import Control.Monad.Trans.Maybe

import Data.Either
import Data.Foldable (forM_)
import qualified Data.Foldable as Fold
import Data.Function (on)
import qualified Data.List as List
import Data.Monoid
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (forM)

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

import Agda.TypeChecking.Monad as TCM hiding (Offset)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Free
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints as C

import qualified Agda.TypeChecking.SizedTypes as S
import Agda.TypeChecking.SizedTypes.Pretty
import Agda.TypeChecking.SizedTypes.Syntax as Size
import Agda.TypeChecking.SizedTypes.Utils
import Agda.TypeChecking.SizedTypes.WarshallSolver as Size hiding (simplify1)

import Agda.Utils.Cluster
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List1 (List1, pattern (:|), nonEmpty, (<|))
import qualified Agda.Utils.List as List
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty (Pretty, prettyShow)
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.VarSet (VarSet)

import Agda.Utils.Impossible

-- | Flag to control the behavior of size solver.
data DefaultToInfty
  = DefaultToInfty      -- ^ Instantiate all unconstrained size variables to ∞.
  | DontDefaultToInfty  -- ^ Leave unconstrained size variables unsolved.
  deriving (DefaultToInfty -> DefaultToInfty -> Bool
(DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> Bool) -> Eq DefaultToInfty
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DefaultToInfty -> DefaultToInfty -> Bool
== :: DefaultToInfty -> DefaultToInfty -> Bool
$c/= :: DefaultToInfty -> DefaultToInfty -> Bool
/= :: DefaultToInfty -> DefaultToInfty -> Bool
Eq, Eq DefaultToInfty
Eq DefaultToInfty =>
(DefaultToInfty -> DefaultToInfty -> Ordering)
-> (DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> DefaultToInfty)
-> (DefaultToInfty -> DefaultToInfty -> DefaultToInfty)
-> Ord DefaultToInfty
DefaultToInfty -> DefaultToInfty -> Bool
DefaultToInfty -> DefaultToInfty -> Ordering
DefaultToInfty -> DefaultToInfty -> DefaultToInfty
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DefaultToInfty -> DefaultToInfty -> Ordering
compare :: DefaultToInfty -> DefaultToInfty -> Ordering
$c< :: DefaultToInfty -> DefaultToInfty -> Bool
< :: DefaultToInfty -> DefaultToInfty -> Bool
$c<= :: DefaultToInfty -> DefaultToInfty -> Bool
<= :: DefaultToInfty -> DefaultToInfty -> Bool
$c> :: DefaultToInfty -> DefaultToInfty -> Bool
> :: DefaultToInfty -> DefaultToInfty -> Bool
$c>= :: DefaultToInfty -> DefaultToInfty -> Bool
>= :: DefaultToInfty -> DefaultToInfty -> Bool
$cmax :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
max :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
$cmin :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
min :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
Ord, Int -> DefaultToInfty -> ShowS
[DefaultToInfty] -> ShowS
DefaultToInfty -> [Char]
(Int -> DefaultToInfty -> ShowS)
-> (DefaultToInfty -> [Char])
-> ([DefaultToInfty] -> ShowS)
-> Show DefaultToInfty
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DefaultToInfty -> ShowS
showsPrec :: Int -> DefaultToInfty -> ShowS
$cshow :: DefaultToInfty -> [Char]
show :: DefaultToInfty -> [Char]
$cshowList :: [DefaultToInfty] -> ShowS
showList :: [DefaultToInfty] -> ShowS
Show)

-- | Solve size constraints involving hypotheses.

solveSizeConstraints :: DefaultToInfty -> TCM ()
solveSizeConstraints :: DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
flag =  do

  -- 1. Take out the size constraints normalised.

  -- NOTE: this deletes the size constraints from the constraint set!
  cs0 :: [ProblemConstraint]
    <- TCMT IO [ProblemConstraint]
-> (ProblemConstraint -> TCMT IO ProblemConstraint)
-> TCMT IO [ProblemConstraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
m (t a) -> (a -> m b) -> m (t b)
forMM ((Comparison -> Bool) -> TCMT IO [ProblemConstraint]
S.takeSizeConstraints (Comparison -> Comparison -> Bool
forall a. Eq a => a -> a -> Bool
== Comparison
CmpLeq)) ((ProblemConstraint -> TCMT IO ProblemConstraint)
 -> TCMT IO [ProblemConstraint])
-> (ProblemConstraint -> TCMT IO ProblemConstraint)
-> TCMT IO [ProblemConstraint]
forall a b. (a -> b) -> a -> b
$ \ (ProblemConstraint
c :: ProblemConstraint) -> do
      (Constraint -> TCMT IO Constraint)
-> Closure Constraint -> TCMT IO (Closure Constraint)
forall (m :: * -> *) a b.
(MonadTCEnv m, ReadTCState m) =>
(a -> m b) -> Closure a -> m (Closure b)
mapClosure Constraint -> TCMT IO Constraint
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) TCMT IO (Closure Constraint)
-> (Closure Constraint -> ProblemConstraint)
-> TCMT IO ProblemConstraint
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Closure Constraint
cl -> ProblemConstraint
c { theConstraint = cl }

  unless (null cs0) $
    reportSDoc "tc.size.solve" 40 $ vcat $
      text ( "Solving constraints (" ++ show flag ++ ")" ) : map prettyTCM cs0

  -- 2. Cluster the constraints by common size metas.

  -- Get all size metas.
  sizeMetaSet <- Set.fromList . map (\ (MetaId
x, Type'' Term Term
_t, Tele (Dom (Type'' Term Term))
_tel) -> MetaId
x) <$> S.getSizeMetas True

  -- Pair each constraint with its list of size metas occurring in it.
  cms <- forM cs0 $ \ ProblemConstraint
cl -> Closure Constraint
-> (Constraint -> TCMT IO (ProblemConstraint, [MetaId]))
-> TCMT IO (ProblemConstraint, [MetaId])
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
cl) ((Constraint -> TCMT IO (ProblemConstraint, [MetaId]))
 -> TCMT IO (ProblemConstraint, [MetaId]))
-> (Constraint -> TCMT IO (ProblemConstraint, [MetaId]))
-> TCMT IO (ProblemConstraint, [MetaId])
forall a b. (a -> b) -> a -> b
$ \ Constraint
c -> do

    -- @allMetas@ does not reduce or instantiate;
    -- this is why we require the size constraints to be normalised.
    (ProblemConstraint, [MetaId])
-> TCMT IO (ProblemConstraint, [MetaId])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProblemConstraint
cl, Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList (Set MetaId -> [MetaId]) -> Set MetaId -> [MetaId]
forall a b. (a -> b) -> a -> b
$
      Set MetaId
sizeMetaSet Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` (MetaId -> Set MetaId) -> Constraint -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> Constraint -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall el coll. Singleton el coll => el -> coll
singleton Constraint
c)

  -- Now, some constraints may have no metas (clcs), the others have at least one (othercs).
  let classify :: (a, [b]) -> Either a (a, List1 b)
      classify (a
cl, [])     = a -> Either a (a, List1 b)
forall a b. a -> Either a b
Left  a
cl
      classify (a
cl, (b
x:[b]
xs)) = (a, List1 b) -> Either a (a, List1 b)
forall a b. b -> Either a b
Right (a
cl, b
x b -> [b] -> List1 b
forall a. a -> [a] -> NonEmpty a
:| [b]
xs)
  let (clcs, othercs) = partitionEithers $ map classify cms

  -- We cluster the constraints by their metas.
  let ccs = [(ProblemConstraint, List1 MetaId)] -> [NonEmpty ProblemConstraint]
forall c a. Ord c => [(a, NonEmpty c)] -> [NonEmpty a]
cluster' [(ProblemConstraint, List1 MetaId)]
othercs

  -- 3. Solve each cluster

  -- Solve the closed constraints, one by one.

  forM_ clcs $ \ ProblemConstraint
c -> () () -> TCMT IO (Set MetaId) -> TCM ()
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ DefaultToInfty -> [ProblemConstraint] -> TCMT IO (Set MetaId)
solveSizeConstraints_ DefaultToInfty
flag [ProblemConstraint
c]

  -- Solve the clusters.

  constrainedMetas <- Set.unions <$> do
    forM  (ccs) $ \ (NonEmpty ProblemConstraint
cs :: List1 ProblemConstraint) -> do

      [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        TCMT IO Doc
"size constraint cluster:" TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> NonEmpty (TCMT IO Doc)
forall a. a -> NonEmpty a -> NonEmpty a
<| (ProblemConstraint -> TCMT IO Doc)
-> NonEmpty ProblemConstraint -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (ProblemConstraint -> [Char])
-> ProblemConstraint
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> [Char]
forall a. Show a => a -> [Char]
show) NonEmpty ProblemConstraint
cs

      -- Convert each constraint in the cluster to the largest context.
      -- (Keep fingers crossed).

      Closure Constraint
-> (Constraint -> TCMT IO (Set MetaId)) -> TCMT IO (Set MetaId)
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure ((Closure Constraint -> Closure Constraint -> Ordering)
-> NonEmpty (Closure Constraint) -> Closure Constraint
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
Fold.maximumBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (Closure Constraint -> Int)
-> Closure Constraint
-> Closure Constraint
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Context' ContextEntry -> Int
forall a. Context' a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Context' ContextEntry -> Int)
-> (Closure Constraint -> Context' ContextEntry)
-> Closure Constraint
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
-> TCEnv -> Context' ContextEntry
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext (TCEnv -> Context' ContextEntry)
-> (Closure Constraint -> TCEnv)
-> Closure Constraint
-> Context' ContextEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv)) (NonEmpty (Closure Constraint) -> Closure Constraint)
-> NonEmpty (Closure Constraint) -> Closure Constraint
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> Closure Constraint)
-> NonEmpty ProblemConstraint -> NonEmpty (Closure Constraint)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProblemConstraint -> Closure Constraint
theConstraint NonEmpty ProblemConstraint
cs) ((Constraint -> TCMT IO (Set MetaId)) -> TCMT IO (Set MetaId))
-> (Constraint -> TCMT IO (Set MetaId)) -> TCMT IO (Set MetaId)
forall a b. (a -> b) -> a -> b
$ \ Constraint
_ -> do
        -- Get all constraints that can be cast to the longest context.
        cs' :: [ProblemConstraint] <- List1 (Maybe ProblemConstraint) -> [ProblemConstraint]
forall a. List1 (Maybe a) -> [a]
List1.catMaybes (List1 (Maybe ProblemConstraint) -> [ProblemConstraint])
-> TCMT IO (List1 (Maybe ProblemConstraint))
-> TCMT IO [ProblemConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          (ProblemConstraint -> TCMT IO (Maybe ProblemConstraint))
-> NonEmpty ProblemConstraint
-> TCMT IO (List1 (Maybe ProblemConstraint))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM (MaybeT (TCMT IO) ProblemConstraint
-> TCMT IO (Maybe ProblemConstraint)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) ProblemConstraint
 -> TCMT IO (Maybe ProblemConstraint))
-> (ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint)
-> ProblemConstraint
-> TCMT IO (Maybe ProblemConstraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
castConstraintToCurrentContext) NonEmpty ProblemConstraint
cs

        reportSDoc "tc.size.solve" 20 $ vcat $
          ( "converted size constraints to context: " <+> do
              tel <- getContextTelescope
              inTopContext $ prettyTCM tel
          ) : map (nest 2 . prettyTCM) cs'

        -- Solve the converted constraints.
        solveSizeConstraints_ flag cs'

  -- 4. Possibly set remaining metas to infinity.

  -- Andreas, issue 1862: do not default to ∞ always, could be too early.
  when (flag == DefaultToInfty) $ do

    -- let constrainedMetas = Set.fromList $ concat $
    --       for cs0 $ \ Closure{ clValue = ValueCmp _ _ u v } ->
    --         allMetas u ++ allMetas v

    -- Set the unconstrained, open size metas to ∞.
    ms <- S.getSizeMetas False -- do not get interaction metas
    unless (null ms) $ do
      inf <- primSizeInf
      forM_ ms $ \ (MetaId
m, Type'' Term Term
t, Tele (Dom (Type'' Term Term))
tel) -> do
        Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (MetaId
m MetaId -> Set MetaId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set MetaId
constrainedMetas) (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 (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"solution " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
          TCMT IO Doc
" := "      TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
inf
        Int -> MetaId -> Type'' Term Term -> [Int] -> Term -> TCM ()
assignMeta Int
0 MetaId
m Type'' Term Term
t (Int -> [Int]
forall a. Integral a => a -> [a]
List.downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
tel) Term
inf

  -- -- Double check.
  -- let -- Error for giving up
  --     cannotSolve :: TCM a
  --     cannotSolve = typeError . GenericDocError =<<
  --       vcat ("Cannot solve size constraints" : map prettyTCM cs0)
  -- unless (null cs0 && null ms) $ do
  --   flip catchError (const cannotSolve) $
  --     noConstraints $
  --       forM_ cs0 $ \ cl -> enterClosure cl solveConstraint

  -- 5. Make sure we did not lose any constraints.

  -- This is necessary since we have removed the size constraints.
  forM_ cs0 $ withConstraint solveConstraint


-- | TODO: this does not actually work!
--
--   We would like to use a constraint @c@ created in context @Δ@ from module @N@
--   in the current context @Γ@ and current module @M@.
--
--   @Δ@ is module tel @Δ₁@ of @N@ extended by some local bindings @Δ₂@.
--   @Γ@ is the current context.
--   The module parameter substitution from current @M@ to @N@ be
--   @Γ ⊢ σ : Δ₁@.
--
--   If @M == N@, we do not need the parameter substitution.  We try raising.
--
--   We first strengthen @Δ ⊢ c@ to live in @Δ₁@ and obtain @c₁ = strengthen Δ₂ c@.
--   We then transport @c₁@ to @Γ@ and obtain @c₂ = applySubst σ c₁@.
--
--   This works for different modules, but if @M == N@ we should not strengthen
--   and then weaken, because strengthening is a partial operation.
--   We should rather lift the substitution @σ@ by @Δ₂@ and then
--   raise by @Γ₂ - Δ₂@.
--   This "raising" might be a strengthening if @Γ₂@ is shorter than @Δ₂@.
--
--   (TODO: If the module substitution does not exist, because @N@ is not
--   a parent of @M@, we cannot use the constraint, as it has been created
--   in an unrelated context.)

castConstraintToCurrentContext' :: Closure TCM.Constraint -> MaybeT TCM TCM.Constraint
castConstraintToCurrentContext' :: Closure Constraint -> MaybeT (TCMT IO) Constraint
castConstraintToCurrentContext' Closure Constraint
cl = do
  let modN :: ModuleName
modN  = Getting ModuleName TCEnv ModuleName -> TCEnv -> ModuleName
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ModuleName TCEnv ModuleName
Lens' TCEnv ModuleName
eCurrentModule (TCEnv -> ModuleName) -> TCEnv -> ModuleName
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure Constraint
cl
      delta :: Context' ContextEntry
delta = Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
-> TCEnv -> Context' ContextEntry
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext (TCEnv -> Context' ContextEntry) -> TCEnv -> Context' ContextEntry
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure Constraint
cl
  -- The module telescope of the constraint.
  -- The constraint could come from the module telescope of the top level module.
  -- In this case, it does not live in any module!
  -- Thus, getSection can return Nothing.
  delta1 <- TCMT IO (Tele (Dom (Type'' Term Term)))
-> MaybeT (TCMT IO) (Tele (Dom (Type'' Term Term)))
forall a. TCM a -> MaybeT (TCMT IO) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (Tele (Dom (Type'' Term Term)))
 -> MaybeT (TCMT IO) (Tele (Dom (Type'' Term Term))))
-> TCMT IO (Tele (Dom (Type'' Term Term)))
-> MaybeT (TCMT IO) (Tele (Dom (Type'' Term Term)))
forall a b. (a -> b) -> a -> b
$ Tele (Dom (Type'' Term Term))
-> (Section -> Tele (Dom (Type'' Term Term)))
-> Maybe Section
-> Tele (Dom (Type'' Term Term))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Tele (Dom (Type'' Term Term))
forall a. Null a => a
empty (Section
-> Getting
     (Tele (Dom (Type'' Term Term)))
     Section
     (Tele (Dom (Type'' Term Term)))
-> Tele (Dom (Type'' Term Term))
forall s a. s -> Getting a s a -> a
^. Getting
  (Tele (Dom (Type'' Term Term)))
  Section
  (Tele (Dom (Type'' Term Term)))
Lens' Section (Tele (Dom (Type'' Term Term)))
secTelescope) (Maybe Section -> Tele (Dom (Type'' Term Term)))
-> TCMT IO (Maybe Section)
-> TCMT IO (Tele (Dom (Type'' Term Term)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO (Maybe Section)
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe Section)
getSection ModuleName
modN
  -- The number of locals of the constraint.
  let delta2 = Context' ContextEntry -> Int
forall a. Sized a => a -> Int
size Context' ContextEntry
delta Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
delta1
  unless (delta2 >= 0) __IMPOSSIBLE__

  -- The current module M and context Γ.
  modM  <- currentModule
  gamma <- liftTCM $ getContextSize
  -- The current module telescope.
  -- Could also be empty, if we are in the front matter or telescope of the top-level module.
  gamma1 <-liftTCM $ maybe empty (^. secTelescope) <$> getSection modM
  -- The current locals.
  let gamma2 = Int
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom (Type'' Term Term))
gamma1

  -- Γ ⊢ σ : Δ₁
  sigma <- liftTCM $ fromMaybe idS <$> getModuleParameterSub modN

  -- Debug printing.
  reportSDoc "tc.constr.cast" 40 $ "casting constraint" $$ do
    tel <- getContextTelescope
    inTopContext $ nest 2 $ vcat $
      [ "current module                = " <+> prettyTCM modM
      , "current module telescope      = " <+> prettyTCM gamma1
      , "current context               = " <+> prettyTCM tel
      , "constraint module             = " <+> prettyTCM modN
      , "constraint module telescope   = " <+> prettyTCM delta1
      , "constraint context            = " <+> (prettyTCM =<< enterClosure cl (const $ getContextTelescope))
      , "constraint                    = " <+> enterClosure cl prettyTCM
      , "module parameter substitution = " <+> prettyTCM sigma
      ]

  -- If gamma2 < 0, we must be in the wrong context.
  -- E.g. we could have switched to the empty context even though
  -- we are still inside a module with parameters.
  -- In this case, we cannot safely convert the constraint,
  -- since the module parameter substitution may be wrong.
  guard (gamma2 >= 0)

  -- Shortcut for modN == modM:
  -- Raise constraint from Δ to Γ, if possible.
  -- This might save us some strengthening.
  if modN == modM then raiseMaybe (gamma - size delta) $ clValue cl else do

  -- Strengthen constraint to Δ₁ ⊢ c
  c <- raiseMaybe (-delta2) $ clValue cl

  -- Ulf, 2016-11-09: I don't understand what this function does when M and N
  -- are not related. Certainly things can go terribly wrong (see
  -- test/Succeed/Issue2223b.agda)
  fv <- liftTCM $ getModuleFreeVars modN
  guard $ fv == size delta1

  -- Γ ⊢ c[σ]
  return $ applySubst sigma c
  where
    raiseMaybe :: Int -> a -> f a
raiseMaybe Int
n a
c
      -- We are always fine to weaken.
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> f a) -> a -> f a
forall a b. (a -> b) -> a -> b
$ Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
n a
c
      | Bool
otherwise =
        case VarSet -> Maybe Int
VarSet.lookupMin (VarSet -> Maybe Int) -> VarSet -> Maybe Int
forall a b. (a -> b) -> a -> b
$ a -> VarSet
forall t. Free t => t -> VarSet
freeVarSet a
c of
          Maybe Int
Nothing -> a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> f a) -> a -> f a
forall a b. (a -> b) -> a -> b
$ Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
n a
c
          Just Int
k | -Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k -> a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> f a) -> a -> f a
forall a b. (a -> b) -> a -> b
$ Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
n a
c
                 | Bool
otherwise -> f a
forall a. f a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

{-# SPECIALIZE allFreeVarIgnoreAll :: (Int -> Bool) -> TCM.Constraint -> Bool #-}

-- | A hazardous hack, may the Gods have mercy on us.
--
--   To cast to the current context, we match the context of the
--   given constraint by 'CtxId', and as fallback, by variable name (douh!).
--
--   This hack lets issue 2046 go through.

castConstraintToCurrentContext :: ProblemConstraint -> MaybeT TCM ProblemConstraint
castConstraintToCurrentContext :: ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
castConstraintToCurrentContext ProblemConstraint
c = do
  -- The checkpoint of the contraint
  let cl :: Closure Constraint
cl = ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c
      cp :: CheckpointId
cp = Getting CheckpointId TCEnv CheckpointId -> TCEnv -> CheckpointId
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting CheckpointId TCEnv CheckpointId
Lens' TCEnv CheckpointId
eCurrentCheckpoint (TCEnv -> CheckpointId) -> TCEnv -> CheckpointId
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure Constraint
cl
  sigma <- MaybeT (TCMT IO) (Maybe (Substitution' Term))
-> MaybeT (TCMT IO) (Substitution' Term)
-> (Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term))
-> MaybeT (TCMT IO) (Substitution' Term)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Lens' TCEnv (Maybe (Substitution' Term))
-> MaybeT (TCMT IO) (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Lens' TCEnv (Maybe (Substitution' Term))
 -> MaybeT (TCMT IO) (Maybe (Substitution' Term)))
-> Lens' TCEnv (Maybe (Substitution' Term))
-> MaybeT (TCMT IO) (Maybe (Substitution' Term))
forall a b. (a -> b) -> a -> b
$ (Map CheckpointId (Substitution' Term)
 -> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map CheckpointId (Substitution' Term))
eCheckpoints ((Map CheckpointId (Substitution' Term)
  -> f (Map CheckpointId (Substitution' Term)))
 -> TCEnv -> f TCEnv)
-> ((Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
    -> Map CheckpointId (Substitution' Term)
    -> f (Map CheckpointId (Substitution' Term)))
-> (Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
-> TCEnv
-> f TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckpointId
-> Lens'
     (Map CheckpointId (Substitution' Term))
     (Maybe (Substitution' Term))
forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
key CheckpointId
cp)
          (do
            -- We are not in a descendant of the constraint checkpoint.
            -- Here be dragons!!
            gamma <- MaybeT (TCMT IO) (Context' ContextEntry)
forall (m :: * -> *). MonadTCEnv m => m (Context' ContextEntry)
getContext -- The target context
            let findInGamma ContextEntry
ce =
                  -- match by name (hazardous)
                  -- This is one of the seven deadly sins (not respecting alpha).
                  (ContextEntry -> Bool) -> [ContextEntry] -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex ((Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Name -> Name -> Bool)
-> (ContextEntry -> Name) -> ContextEntry -> ContextEntry -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ContextEntry -> Name
ctxEntryName) ContextEntry
ce) (Context' ContextEntry -> [ContextEntry]
forall a. Context' a -> [a]
cxEntries Context' ContextEntry
gamma)
            let delta = Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
-> TCEnv -> Context' ContextEntry
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext (TCEnv -> Context' ContextEntry) -> TCEnv -> Context' ContextEntry
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure Constraint
cl
                cand  = (ContextEntry -> Maybe Int) -> [ContextEntry] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map ContextEntry -> Maybe Int
findInGamma ([ContextEntry] -> [Maybe Int]) -> [ContextEntry] -> [Maybe Int]
forall a b. (a -> b) -> a -> b
$ Context' ContextEntry -> [ContextEntry]
forall a. Context' a -> [a]
cxEntries Context' ContextEntry
delta
            -- The domain of our substitution
            let coveredVars = [Int] -> VarSet
VarSet.fromList ([Int] -> VarSet) -> [Int] -> VarSet
forall a b. (a -> b) -> a -> b
$ [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Int] -> [Int]) -> [Maybe Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Maybe Int -> Int -> Maybe Int)
-> [Maybe Int] -> [Int] -> [Maybe Int]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Maybe Int -> Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
($>) [Maybe Int]
cand [Int
0..]
            -- Check that all the free variables of the constraint are contained in
            -- coveredVars.
            -- We ignore the free variables occurring in sorts.
            -- guard $ getAll $ runFree (All . (`VarSet.member` coveredVars)) IgnoreAll (clValue cl)
            guard $ allFreeVarIgnoreAll (`VarSet.member` coveredVars) (clValue cl)
            -- Turn cand into a substitution.
            -- Since we ignored the free variables in sorts, we better patch up
            -- the substitution with some dummy term rather than __IMPOSSIBLE__.
            return $ parallelS $ map (maybe __DUMMY_TERM__ var) cand
          ) Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term)
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return -- Phew, we've got the checkpoint! All is well.
  -- Apply substitution to constraint and pray that the Gods are merciful on us.
  cl' <- buildClosure $ applySubst sigma (clValue cl)
  return $ c { theConstraint = cl' }
  -- Note: the resulting constraint may not well-typed.
  -- Even if it is, it may map variables to their wrong counterpart.

-- | Return the size metas occurring in the simplified constraints.
--   A constraint like @↑ _j =< ∞ : Size@ simplifies to nothing,
--   so @_j@ would not be in this set.
solveSizeConstraints_ :: DefaultToInfty -> [ProblemConstraint] -> TCM (Set MetaId)
solveSizeConstraints_ :: DefaultToInfty -> [ProblemConstraint] -> TCMT IO (Set MetaId)
solveSizeConstraints_ DefaultToInfty
flag [ProblemConstraint]
cs0 = do
  -- Pair constraints with their representation as size constraints.
  -- Discard constraints that do not have such a representation.
  ccs :: [(ProblemConstraint, HypSizeConstraint)] <- [Maybe (ProblemConstraint, HypSizeConstraint)]
-> [(ProblemConstraint, HypSizeConstraint)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (ProblemConstraint, HypSizeConstraint)]
 -> [(ProblemConstraint, HypSizeConstraint)])
-> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)]
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [ProblemConstraint]
-> (ProblemConstraint
    -> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint)))
-> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ProblemConstraint]
cs0 ((ProblemConstraint
  -> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint)))
 -> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)])
-> (ProblemConstraint
    -> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint)))
-> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)]
forall a b. (a -> b) -> a -> b
$ \ ProblemConstraint
c0 -> (HypSizeConstraint -> (ProblemConstraint, HypSizeConstraint))
-> Maybe HypSizeConstraint
-> Maybe (ProblemConstraint, HypSizeConstraint)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProblemConstraint
c0,) (Maybe HypSizeConstraint
 -> Maybe (ProblemConstraint, HypSizeConstraint))
-> TCMT IO (Maybe HypSizeConstraint)
-> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProblemConstraint -> TCMT IO (Maybe HypSizeConstraint)
computeSizeConstraint ProblemConstraint
c0

  -- Simplify constraints and check for obvious inconsistencies.
  ccs' :: [(ProblemConstraint, HypSizeConstraint)] <- concat <$> do
    forM ccs $ \ cc :: (ProblemConstraint, HypSizeConstraint)
cc@(ProblemConstraint
c0 :: ProblemConstraint, HypSizeConstraint Context' ContextEntry
cxt [Int]
hids [Constraint' NamedRigid SizeMeta]
hs Constraint' NamedRigid SizeMeta
sc) -> do
      case CTrans NamedRigid SizeMeta -> CTrans NamedRigid SizeMeta
forall r f. Eq r => CTrans r f -> CTrans r f
simplify1 (\ Constraint' NamedRigid SizeMeta
sc -> [Constraint' NamedRigid SizeMeta]
-> Maybe [Constraint' NamedRigid SizeMeta]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [Constraint' NamedRigid SizeMeta
sc]) Constraint' NamedRigid SizeMeta
sc of
        Maybe [Constraint' NamedRigid SizeMeta]
Nothing -> TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
-> TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint, HypSizeConstraint) -> TypeError
ContradictorySizeConstraint (ProblemConstraint, HypSizeConstraint)
cc
        Just [Constraint' NamedRigid SizeMeta]
cs -> [(ProblemConstraint, HypSizeConstraint)]
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(ProblemConstraint, HypSizeConstraint)]
 -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
-> [(ProblemConstraint, HypSizeConstraint)]
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint
c0,) (HypSizeConstraint -> (ProblemConstraint, HypSizeConstraint))
-> (Constraint' NamedRigid SizeMeta -> HypSizeConstraint)
-> Constraint' NamedRigid SizeMeta
-> (ProblemConstraint, HypSizeConstraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context' ContextEntry
-> [Int]
-> [Constraint' NamedRigid SizeMeta]
-> Constraint' NamedRigid SizeMeta
-> HypSizeConstraint
HypSizeConstraint Context' ContextEntry
cxt [Int]
hids [Constraint' NamedRigid SizeMeta]
hs (Constraint' NamedRigid SizeMeta
 -> (ProblemConstraint, HypSizeConstraint))
-> [Constraint' NamedRigid SizeMeta]
-> [(ProblemConstraint, HypSizeConstraint)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Constraint' NamedRigid SizeMeta]
cs

  -- Cluster constraints according to the meta variables they mention.
  -- @csNoM@ are the constraints that do not mention any meta.
  let (csNoM, csMs) = (`List.partitionMaybe` ccs') $ \ p :: (ProblemConstraint, HypSizeConstraint)
p@(ProblemConstraint
c0, HypSizeConstraint
c) ->
        (List1 MetaId
 -> ((ProblemConstraint, HypSizeConstraint), List1 MetaId))
-> Maybe (List1 MetaId)
-> Maybe ((ProblemConstraint, HypSizeConstraint), List1 MetaId)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ProblemConstraint, HypSizeConstraint)
p,) (Maybe (List1 MetaId)
 -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 MetaId))
-> Maybe (List1 MetaId)
-> Maybe ((ProblemConstraint, HypSizeConstraint), List1 MetaId)
forall a b. (a -> b) -> a -> b
$ [MetaId] -> Maybe (List1 MetaId)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([MetaId] -> Maybe (List1 MetaId))
-> [MetaId] -> Maybe (List1 MetaId)
forall a b. (a -> b) -> a -> b
$ (SizeMeta -> MetaId) -> [SizeMeta] -> [MetaId]
forall a b. (a -> b) -> [a] -> [b]
map SizeMeta -> MetaId
sizeMetaId ([SizeMeta] -> [MetaId]) -> [SizeMeta] -> [MetaId]
forall a b. (a -> b) -> a -> b
$ Set SizeMeta -> [SizeMeta]
forall a. Set a -> [a]
Set.toList (Set SizeMeta -> [SizeMeta]) -> Set SizeMeta -> [SizeMeta]
forall a b. (a -> b) -> a -> b
$ HypSizeConstraint -> Set (FlexOf HypSizeConstraint)
forall a. Flexs a => a -> Set (FlexOf a)
flexs HypSizeConstraint
c
  -- @css@ are the clusters of constraints.
      css :: [List1 (ProblemConstraint, HypSizeConstraint)]
      css = [((ProblemConstraint, HypSizeConstraint), List1 MetaId)]
-> [List1 (ProblemConstraint, HypSizeConstraint)]
forall c a. Ord c => [(a, NonEmpty c)] -> [NonEmpty a]
cluster' [((ProblemConstraint, HypSizeConstraint), List1 MetaId)]
csMs

  -- Check that the closed constraints are valid.
  whenJust (nonEmpty csNoM) $ solveCluster flag

  -- Now, process the clusters.
  forM_ css $ solveCluster flag

  return $ Set.mapMonotonic sizeMetaId $ flexs $ map (snd . fst) csMs

-- | Solve a cluster of constraints sharing some metas.
--
solveCluster :: DefaultToInfty -> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
solveCluster :: DefaultToInfty
-> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
solveCluster DefaultToInfty
flag List1 (ProblemConstraint, HypSizeConstraint)
ccs = do
  let
    err :: TCM Doc -> TCM a
    err :: forall a. TCMT IO Doc -> TCM a
err TCMT IO Doc
mdoc = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (ProblemConstraint, HypSizeConstraint) -> Doc -> TypeError
CannotSolveSizeConstraints List1 (ProblemConstraint, HypSizeConstraint)
ccs (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Doc
mdoc
    cs :: List1 HypSizeConstraint
    cs :: List1 HypSizeConstraint
cs = ((ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint)
-> List1 (ProblemConstraint, HypSizeConstraint)
-> List1 HypSizeConstraint
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint
forall a b. (a, b) -> b
snd List1 (ProblemConstraint, HypSizeConstraint)
ccs
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Solving constraint cluster" TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> NonEmpty (TCMT IO Doc)
forall a. a -> NonEmpty a -> NonEmpty a
<| (HypSizeConstraint -> TCMT IO Doc)
-> List1 HypSizeConstraint -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HypSizeConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => HypSizeConstraint -> m Doc
prettyTCM List1 HypSizeConstraint
cs

  -- Find the super context of all contexts.
{-
  -- We use the @'ctxId'@s.
  let cis@(ci:cis') = for cs $ \ c -> (c, reverse $ map ctxId $ sizeContext c)
--  let cis@(ci:cis') = for cs $ \ c -> (c, reverse $ sizeHypIds c)
      max a@Left{}            _            = a
      max a@(Right ci@(c,is)) ci'@(c',is') =
        case preOrSuffix is is' of
          -- No common context:
          IsNofix    -> Left (ci, ci')
          IsPrefix{} -> Right ci'
          _          -> a
      res = foldl' max (Right ci) cis'
      noContext ((c,is),(c',is')) = typeError . GenericDocError =<< vcat
        [ "Cannot solve size constraints; the following constraints have no common typing context:"
        , prettyTCM c
        , prettyTCM c'
        ]
  flip (either noContext) res $ \ (HypSizeConstraint gamma hids hs _, _) -> do
-}
  -- We rely on the fact that contexts are only extended...
  -- Just take the longest context.
  let HypSizeConstraint Context' ContextEntry
gamma [Int]
hids [Constraint' NamedRigid SizeMeta]
hs Constraint' NamedRigid SizeMeta
_ = (HypSizeConstraint -> HypSizeConstraint -> Ordering)
-> List1 HypSizeConstraint -> HypSizeConstraint
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
Fold.maximumBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (HypSizeConstraint -> Int)
-> HypSizeConstraint
-> HypSizeConstraint
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Context' ContextEntry -> Int
forall a. Context' a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Context' ContextEntry -> Int)
-> (HypSizeConstraint -> Context' ContextEntry)
-> HypSizeConstraint
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HypSizeConstraint -> Context' ContextEntry
sizeContext)) List1 HypSizeConstraint
cs
  -- Length of longest context.
  let n :: Int
n = Context' ContextEntry -> Int
forall a. Sized a => a -> Int
size Context' ContextEntry
gamma

  -- Now convert all size constraints to the largest context.
      csL :: NonEmpty (Constraint' NamedRigid SizeMeta)
csL = List1 HypSizeConstraint
-> (HypSizeConstraint -> Constraint' NamedRigid SizeMeta)
-> NonEmpty (Constraint' NamedRigid SizeMeta)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
for List1 HypSizeConstraint
cs ((HypSizeConstraint -> Constraint' NamedRigid SizeMeta)
 -> NonEmpty (Constraint' NamedRigid SizeMeta))
-> (HypSizeConstraint -> Constraint' NamedRigid SizeMeta)
-> NonEmpty (Constraint' NamedRigid SizeMeta)
forall a b. (a -> b) -> a -> b
$ \ (HypSizeConstraint Context' ContextEntry
cxt [Int]
_ [Constraint' NamedRigid SizeMeta]
_ Constraint' NamedRigid SizeMeta
c) -> Int
-> Constraint' NamedRigid SizeMeta
-> Constraint' NamedRigid SizeMeta
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Context' ContextEntry -> Int
forall a. Sized a => a -> Int
size Context' ContextEntry
cxt) Constraint' NamedRigid SizeMeta
c
  -- Canonicalize the constraints.
  -- This is unsound in the presence of hypotheses.
      csC :: [SizeConstraint]
      csC :: [Constraint' NamedRigid SizeMeta]
csC = Bool
-> ([Constraint' NamedRigid SizeMeta]
    -> [Constraint' NamedRigid SizeMeta])
-> [Constraint' NamedRigid SizeMeta]
-> [Constraint' NamedRigid SizeMeta]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen ([Constraint' NamedRigid SizeMeta] -> Bool
forall a. Null a => a -> Bool
null [Constraint' NamedRigid SizeMeta]
hs) ((Constraint' NamedRigid SizeMeta
 -> Maybe (Constraint' NamedRigid SizeMeta))
-> [Constraint' NamedRigid SizeMeta]
-> [Constraint' NamedRigid SizeMeta]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Constraint' NamedRigid SizeMeta
-> Maybe (Constraint' NamedRigid SizeMeta)
canonicalizeSizeConstraint) ([Constraint' NamedRigid SizeMeta]
 -> [Constraint' NamedRigid SizeMeta])
-> [Constraint' NamedRigid SizeMeta]
-> [Constraint' NamedRigid SizeMeta]
forall a b. (a -> b) -> a -> b
$ NonEmpty (Constraint' NamedRigid SizeMeta)
-> [Item (NonEmpty (Constraint' NamedRigid SizeMeta))]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty (Constraint' NamedRigid SizeMeta)
csL
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
    [ TCMT IO Doc
"Size hypotheses" ] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
    (Constraint' NamedRigid SizeMeta -> TCMT IO Doc)
-> [Constraint' NamedRigid SizeMeta] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (HypSizeConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => HypSizeConstraint -> m Doc
prettyTCM (HypSizeConstraint -> TCMT IO Doc)
-> (Constraint' NamedRigid SizeMeta -> HypSizeConstraint)
-> Constraint' NamedRigid SizeMeta
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context' ContextEntry
-> [Int]
-> [Constraint' NamedRigid SizeMeta]
-> Constraint' NamedRigid SizeMeta
-> HypSizeConstraint
HypSizeConstraint Context' ContextEntry
gamma [Int]
hids [Constraint' NamedRigid SizeMeta]
hs) [Constraint' NamedRigid SizeMeta]
hs [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
    [ TCMT IO Doc
"Canonicalized constraints" ] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
    (Constraint' NamedRigid SizeMeta -> TCMT IO Doc)
-> [Constraint' NamedRigid SizeMeta] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (HypSizeConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => HypSizeConstraint -> m Doc
prettyTCM (HypSizeConstraint -> TCMT IO Doc)
-> (Constraint' NamedRigid SizeMeta -> HypSizeConstraint)
-> Constraint' NamedRigid SizeMeta
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context' ContextEntry
-> [Int]
-> [Constraint' NamedRigid SizeMeta]
-> Constraint' NamedRigid SizeMeta
-> HypSizeConstraint
HypSizeConstraint Context' ContextEntry
gamma [Int]
hids [Constraint' NamedRigid SizeMeta]
hs) [Constraint' NamedRigid SizeMeta]
csC

  -- -- ALT:
  -- -- Now convert all size constraints to de Bruijn levels.

  -- -- To get from indices in a context of length m <= n
  -- -- to levels into the target context of length n,
  -- -- we apply the following substitution:
  -- -- Index m-1 needs to be mapped to level 0,
  -- -- index m-2 needs to be mapped to level 1,
  -- -- index 0 needs to be mapped to level m-1,
  -- -- so the desired substitution is @downFrom m@.
  -- let sub m = applySubst $ parallelS $ map var $ downFrom m

  -- -- We simply reverse the context to get to de Bruijn levels.
  -- -- Of course, all types in the context are broken, but
  -- -- only need it for pretty printing constraints.
  -- gamma <- return $ reverse gamma

  -- -- We convert the hypotheses to de Bruijn levels.
  -- hs <- return $ sub n hs

  -- -- We get a form for pretty-printing
  -- let prettyC = prettyTCM . HypSizeConstraint gamma hids hs

  -- -- We convert the constraints to de Bruijn level format.
  -- let csC :: [SizeConstraint]
  --     csC = for cs $ \ (HypSizeConstraint cxt _ _ c) -> sub (size cxt) c

  -- reportSDoc "tc.size.solve" 30 $ vcat $
  --   [ "Size hypotheses" ]           ++ map prettyC hs ++
  --   [ "Canonicalized constraints" ] ++ map prettyC csC

  -- Convert size metas to flexible vars.
  let metas :: [SizeMeta]
      metas :: [SizeMeta]
metas = (Constraint' NamedRigid SizeMeta -> [SizeMeta])
-> [Constraint' NamedRigid SizeMeta] -> [SizeMeta]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((SizeMeta -> [SizeMeta])
-> Constraint' NamedRigid SizeMeta -> [SizeMeta]
forall m a. Monoid m => (a -> m) -> Constraint' NamedRigid a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (SizeMeta -> [SizeMeta] -> [SizeMeta]
forall a. a -> [a] -> [a]
:[])) [Constraint' NamedRigid SizeMeta]
csC
      csF   :: [Size.Constraint' NamedRigid MetaId]
      csF :: [Constraint' NamedRigid MetaId]
csF   = (Constraint' NamedRigid SizeMeta -> Constraint' NamedRigid MetaId)
-> [Constraint' NamedRigid SizeMeta]
-> [Constraint' NamedRigid MetaId]
forall a b. (a -> b) -> [a] -> [b]
map ((SizeMeta -> MetaId)
-> Constraint' NamedRigid SizeMeta -> Constraint' NamedRigid MetaId
forall a b.
(a -> b) -> Constraint' NamedRigid a -> Constraint' NamedRigid b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SizeMeta -> MetaId
sizeMetaId) [Constraint' NamedRigid SizeMeta]
csC

  -- Construct the hypotheses graph.
  let hyps :: [Constraint' NamedRigid MetaId]
hyps = (Constraint' NamedRigid SizeMeta -> Constraint' NamedRigid MetaId)
-> [Constraint' NamedRigid SizeMeta]
-> [Constraint' NamedRigid MetaId]
forall a b. (a -> b) -> [a] -> [b]
map ((SizeMeta -> MetaId)
-> Constraint' NamedRigid SizeMeta -> Constraint' NamedRigid MetaId
forall a b.
(a -> b) -> Constraint' NamedRigid a -> Constraint' NamedRigid b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SizeMeta -> MetaId
sizeMetaId) [Constraint' NamedRigid SizeMeta]
hs
  -- There cannot be negative cycles in hypotheses graph due to scoping.
  let hg :: HypGraph NamedRigid MetaId
hg = (TCMT IO Doc -> HypGraph NamedRigid MetaId)
-> (HypGraph NamedRigid MetaId -> HypGraph NamedRigid MetaId)
-> Either (TCMT IO Doc) (HypGraph NamedRigid MetaId)
-> HypGraph NamedRigid MetaId
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TCMT IO Doc -> HypGraph NamedRigid MetaId
forall a. HasCallStack => a
__IMPOSSIBLE__ HypGraph NamedRigid MetaId -> HypGraph NamedRigid MetaId
forall a. a -> a
id (Either (TCMT IO Doc) (HypGraph NamedRigid MetaId)
 -> HypGraph NamedRigid MetaId)
-> Either (TCMT IO Doc) (HypGraph NamedRigid MetaId)
-> HypGraph NamedRigid MetaId
forall a b. (a -> b) -> a -> b
$ Set NamedRigid
-> [Constraint' NamedRigid MetaId]
-> Either (TCMT IO Doc) (HypGraph NamedRigid MetaId)
forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
Set rigid
-> [Hyp' rigid flex] -> Either (TCMT IO Doc) (HypGraph rigid flex)
hypGraph ([Constraint' NamedRigid MetaId]
-> Set (RigidOf [Constraint' NamedRigid MetaId])
forall a. Rigids a => a -> Set (RigidOf a)
rigids [Constraint' NamedRigid MetaId]
csF) [Constraint' NamedRigid MetaId]
hyps

  -- -- Construct the constraint graph.
  -- --    g :: Size.Graph NamedRigid Int Label
  -- g <- either err return $ constraintGraph csF hg
  -- reportSDoc "tc.size.solve" 40 $ vcat $
  --   [ "Constraint graph"
  --   , text (show g)
  --   ]

  -- sol :: Solution NamedRigid Int <- either err return $ solveGraph Map.empty hg g
  -- either err return $ verifySolution hg csF sol

  -- Andreas, 2016-07-13, issue 2096.
  -- Running the solver once might result in unsolvable left-over constraints.
  -- We need to iterate the solver to detect this.
  sol :: Solution NamedRigid MetaId <- (TCMT IO Doc -> TCMT IO (Solution NamedRigid MetaId))
-> (Solution NamedRigid MetaId
    -> TCMT IO (Solution NamedRigid MetaId))
-> Either (TCMT IO Doc) (Solution NamedRigid MetaId)
-> TCMT IO (Solution NamedRigid MetaId)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TCMT IO Doc -> TCMT IO (Solution NamedRigid MetaId)
forall a. TCMT IO Doc -> TCM a
err Solution NamedRigid MetaId -> TCMT IO (Solution NamedRigid MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (TCMT IO Doc) (Solution NamedRigid MetaId)
 -> TCMT IO (Solution NamedRigid MetaId))
-> Either (TCMT IO Doc) (Solution NamedRigid MetaId)
-> TCMT IO (Solution NamedRigid MetaId)
forall a b. (a -> b) -> a -> b
$
    Polarities MetaId
-> HypGraph NamedRigid MetaId
-> [Constraint' NamedRigid MetaId]
-> Solution NamedRigid MetaId
-> Either (TCMT IO Doc) (Solution NamedRigid MetaId)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either (TCMT IO Doc) (Solution r f)
iterateSolver Polarities MetaId
forall k a. Map k a
Map.empty HypGraph NamedRigid MetaId
hg [Constraint' NamedRigid MetaId]
csF Solution NamedRigid MetaId
forall r f. Solution r f
emptySolution

  -- Convert solution to meta instantiation.
  solved <- fmap Set.unions $ forM (Map.assocs $ theSolution sol) $ \ (MetaId
m, SizeExpr' NamedRigid MetaId
a) -> do
    Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (SizeExpr' NamedRigid MetaId -> Bool
forall a. ValidOffset a => a -> Bool
validOffset SizeExpr' NamedRigid MetaId
a) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- Solution does not contain metas
    u <- DBSizeExpr -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr (DBSizeExpr -> TCMT IO Term) -> DBSizeExpr -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ (MetaId -> SizeMeta) -> SizeExpr' NamedRigid MetaId -> DBSizeExpr
forall a b.
(a -> b) -> SizeExpr' NamedRigid a -> SizeExpr' NamedRigid b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MetaId -> SizeMeta
forall a. HasCallStack => a
__IMPOSSIBLE__ SizeExpr' NamedRigid MetaId
a
    let SizeMeta _ xs = fromMaybe __IMPOSSIBLE__ $
          List.find ((m ==) . sizeMetaId) metas
    -- Check that solution is well-scoped
    let ys = NamedRigid -> Int
rigidIndex (NamedRigid -> Int) -> [NamedRigid] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set NamedRigid -> [NamedRigid]
forall a. Set a -> [a]
Set.toList (SizeExpr' NamedRigid MetaId
-> Set (RigidOf (SizeExpr' NamedRigid MetaId))
forall a. Rigids a => a -> Set (RigidOf a)
rigids SizeExpr' NamedRigid MetaId
a)
        ok = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
xs) [Int]
ys -- TODO: more efficient
    -- unless ok $ err "ill-scoped solution for size meta variable"
    u <- if ok then return u else primSizeInf
    t <- getMetaType m
    reportSDoc "tc.size.solve" 20 $ unsafeModifyContext (const gamma) $ do
      let args = (Int -> Elim' Term) -> [Int] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> (Int -> Arg Term) -> Int -> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) [Int]
xs
      "solution " <+> prettyTCM (MetaV m args) <+> " := " <+> prettyTCM u
    reportSDoc "tc.size.solve" 60 $ vcat
      [ text $ "  xs = " ++ show xs
      , text $ "  u  = " ++ show u
      ]
    ifM (isFrozen m `or2M` (not <$> viewTC eAssignMetas)) (return Set.empty) $ do
      assignMeta n m t xs u
      return $ Set.singleton m
    -- WRONG:
    -- let partialSubst = List.sort $ zip xs $ map var $ downFrom n
    -- assignMeta' n m t (length xs) partialSubst u
    -- WRONG: assign DirEq m (map (defaultArg . var) xs) u

  -- Possibly set remaining size metas to ∞ (issue 1862)
  -- unless we have an interaction meta in the cluster (issue 2095).

  ims <- Set.fromList <$> getInteractionMetas

  --  ms = unsolved size metas from cluster
  let ms = [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList ((SizeMeta -> MetaId) -> [SizeMeta] -> [MetaId]
forall a b. (a -> b) -> [a] -> [b]
map SizeMeta -> MetaId
sizeMetaId [SizeMeta]
metas) Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set MetaId
solved
  --  Make sure they do not contain an interaction point
  let noIP = Set MetaId -> Set MetaId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set MetaId
ims Set MetaId
ms

  unless (null ms) $ reportSDoc "tc.size.solve" 30 $ fsep $
    "cluster did not solve these size metas: " : map prettyTCM (Set.toList ms)

  solvedAll <- do
    -- If no metas are left, we have solved this cluster completely.
    if Set.null ms                then return True  else do
    -- Otherwise, we can solve it completely if we are allowed to set to ∞.
    if flag == DontDefaultToInfty then return False else do
    -- Which is only the case when we have no interaction points in the cluster.
    if not noIP                   then return False else do
    -- Try to set all unconstrained size metas to ∞.
    inf <- primSizeInf
    and <$> do
      forM (Set.toList ms) $ \ MetaId
m -> do
        -- If one variable is frozen, we cannot set it (and hence not all) to ∞
        let no :: TCMT IO Bool
no = do
              [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
                Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is frozen, cannot set it to ∞"
              Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` do Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eAssignMetas) TCMT IO Bool
no (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ {-else-} do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"solution " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
            TCMT IO Doc
" := "      TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
inf
          t <- MetaId -> TCMT IO (Type'' Term Term)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Type'' Term Term)
metaType MetaId
m
          TelV tel core <- telView t
          unlessM (isJust <$> isSizeType core) __IMPOSSIBLE__
          assignMeta 0 m t (List.downFrom $ size tel) inf
          return True

  -- Double check.
  when solvedAll $ do
      noConstraints $ mapM_ (withConstraint solveConstraint . fst) ccs
    `catchError` \ TCErr
_ ->
      TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ List1 (ProblemConstraint, HypSizeConstraint) -> Doc -> TypeError
CannotSolveSizeConstraints List1 (ProblemConstraint, HypSizeConstraint)
ccs Doc
forall a. Null a => a
empty

-- | Collect constraints from a typing context, looking for SIZELT hypotheses.
getSizeHypotheses :: Context -> TCM [(Nat, SizeConstraint)]
getSizeHypotheses :: Context' ContextEntry
-> TCM [(Int, Constraint' NamedRigid SizeMeta)]
getSizeHypotheses Context' ContextEntry
gamma = (Context' ContextEntry -> Context' ContextEntry)
-> TCM [(Int, Constraint' NamedRigid SizeMeta)]
-> TCM [(Int, Constraint' NamedRigid SizeMeta)]
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
unsafeModifyContext (Context' ContextEntry
-> Context' ContextEntry -> Context' ContextEntry
forall a b. a -> b -> a
const Context' ContextEntry
gamma) (TCM [(Int, Constraint' NamedRigid SizeMeta)]
 -> TCM [(Int, Constraint' NamedRigid SizeMeta)])
-> TCM [(Int, Constraint' NamedRigid SizeMeta)]
-> TCM [(Int, Constraint' NamedRigid SizeMeta)]
forall a b. (a -> b) -> a -> b
$ do
  (_, msizelt) <- TCMT IO (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  caseMaybe msizelt (return []) $ \ QName
sizelt -> do
    -- Traverse the context from newest to oldest de Bruijn Index
    [Maybe (Int, Constraint' NamedRigid SizeMeta)]
-> [(Int, Constraint' NamedRigid SizeMeta)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Int, Constraint' NamedRigid SizeMeta)]
 -> [(Int, Constraint' NamedRigid SizeMeta)])
-> TCMT IO [Maybe (Int, Constraint' NamedRigid SizeMeta)]
-> TCM [(Int, Constraint' NamedRigid SizeMeta)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      [(Int, ContextEntry)]
-> ((Int, ContextEntry)
    -> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta)))
-> TCMT IO [Maybe (Int, Constraint' NamedRigid SizeMeta)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ((Int -> ContextEntry -> (Int, ContextEntry))
-> Context' ContextEntry -> [(Int, ContextEntry)]
forall a.
(Int -> ContextEntry -> a) -> Context' ContextEntry -> [a]
cxWithIndex (,) Context' ContextEntry
gamma) (((Int, ContextEntry)
  -> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta)))
 -> TCMT IO [Maybe (Int, Constraint' NamedRigid SizeMeta)])
-> ((Int, ContextEntry)
    -> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta)))
-> TCMT IO [Maybe (Int, Constraint' NamedRigid SizeMeta)]
forall a b. (a -> b) -> a -> b
$ \case
        (Int
i, CtxVar Name
x Dom (Type'' Term Term)
a) -> do
          -- Get name and type of variable i.
          let s :: [Char]
s = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
          t <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term)
-> (Dom (Type'' Term Term) -> Term)
-> Dom (Type'' Term Term)
-> TCMT IO Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i) (Term -> Term)
-> (Dom (Type'' Term Term) -> Term)
-> Dom (Type'' Term Term)
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl (Type'' Term Term -> Term)
-> (Dom (Type'' Term Term) -> Type'' Term Term)
-> Dom (Type'' Term Term)
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom (Dom (Type'' Term Term) -> TCMT IO Term)
-> Dom (Type'' Term Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Dom (Type'' Term Term)
a
          case t of
            Def QName
d [Apply Arg Term
u] | QName
d QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt -> do
              TCMT IO (Maybe DBSizeExpr)
-> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta))
-> (DBSizeExpr
    -> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta)))
-> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta))
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Term -> TCMT IO (Maybe DBSizeExpr)
sizeExpr (Term -> TCMT IO (Maybe DBSizeExpr))
-> Term -> TCMT IO (Maybe DBSizeExpr)
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u) (Maybe (Int, Constraint' NamedRigid SizeMeta)
-> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Int, Constraint' NamedRigid SizeMeta)
forall a. Maybe a
Nothing) ((DBSizeExpr
  -> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta)))
 -> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta)))
-> (DBSizeExpr
    -> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta)))
-> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta))
forall a b. (a -> b) -> a -> b
$ \ DBSizeExpr
a ->
                Maybe (Int, Constraint' NamedRigid SizeMeta)
-> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Int, Constraint' NamedRigid SizeMeta)
 -> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta)))
-> Maybe (Int, Constraint' NamedRigid SizeMeta)
-> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta))
forall a b. (a -> b) -> a -> b
$ (Int, Constraint' NamedRigid SizeMeta)
-> Maybe (Int, Constraint' NamedRigid SizeMeta)
forall a. a -> Maybe a
Just ((Int, Constraint' NamedRigid SizeMeta)
 -> Maybe (Int, Constraint' NamedRigid SizeMeta))
-> (Int, Constraint' NamedRigid SizeMeta)
-> Maybe (Int, Constraint' NamedRigid SizeMeta)
forall a b. (a -> b) -> a -> b
$ (Int
i, DBSizeExpr -> Cmp -> DBSizeExpr -> Constraint' NamedRigid SizeMeta
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (NamedRigid -> Offset -> DBSizeExpr
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid ([Char] -> Int -> NamedRigid
NamedRigid [Char]
s Int
i) Offset
0) Cmp
Lt DBSizeExpr
a)
            Term
_ -> Maybe (Int, Constraint' NamedRigid SizeMeta)
-> TCMT IO (Maybe (Int, Constraint' NamedRigid SizeMeta))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Int, Constraint' NamedRigid SizeMeta)
forall a. Maybe a
Nothing

-- | Convert size constraint into form where each meta is applied
--   to indices @n-1,...,1,0@ 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.
--
--   Cf. @SizedTypes.oldCanonicalizeSizeConstraint@.
--
--   Fixes (the rather artificial) issue 300.
--   But it is unsound when pruned metas occur and triggers issue 1914.
--   Thus we deactivate it.
--   This needs to be properly implemented, possibly using the
--   metaPermuatation of each meta variable.

canonicalizeSizeConstraint :: SizeConstraint -> Maybe (SizeConstraint)
canonicalizeSizeConstraint :: Constraint' NamedRigid SizeMeta
-> Maybe (Constraint' NamedRigid SizeMeta)
canonicalizeSizeConstraint c :: Constraint' NamedRigid SizeMeta
c@(Constraint DBSizeExpr
a Cmp
cmp DBSizeExpr
b) = Constraint' NamedRigid SizeMeta
-> Maybe (Constraint' NamedRigid SizeMeta)
forall a. a -> Maybe a
Just Constraint' NamedRigid SizeMeta
c
{-
  case (a,b) of

    -- Case flex-flex
    (Flex (SizeMeta m xs) n, Flex (SizeMeta l ys) n')
         -- try to invert xs on ys
       | let len = size xs
       , Just ys' <- mapM (\ y -> (len-1 -) <$> findIndex (==y) xs) ys ->
           return $ Constraint (Flex (SizeMeta m $ downFrom len) n)
                           cmp (Flex (SizeMeta l ys') n')
         -- try to invert ys on xs
       | let len = size ys
       , Just xs' <- mapM (\ x -> (len-1 -) <$> findIndex (==x) ys) xs ->
           return $ Constraint (Flex (SizeMeta m xs') n)
                           cmp (Flex (SizeMeta l $ downFrom len) n')
         -- give up
       | otherwise -> Nothing

    -- Case flex-rigid
    (Flex (SizeMeta m xs) n, Rigid (NamedRigid x i) n') -> do
      let len = size xs
      j <- (len-1 -) <$> findIndex (==i) xs
      return $ Constraint (Flex (SizeMeta m $ downFrom len) n)
                      cmp (Rigid (NamedRigid x j) n')

    -- Case rigid-flex
    (Rigid (NamedRigid x i) n, Flex (SizeMeta m xs) n') -> do
      let len = size xs
      j <- (len-1 -) <$> findIndex (==i) xs
      return $ Constraint (Rigid (NamedRigid x j) n)
                      cmp (Flex (SizeMeta m $ downFrom len) n')

    -- Case flex-const
    (Flex (SizeMeta m xs) n, _)      ->
      return $ Constraint (Flex (SizeMeta m $ downFrom $ size xs) n) cmp b

    -- Case const-flex
    (_, Flex (SizeMeta m xs) n') -> do
      return $ Constraint a cmp (Flex (SizeMeta m $ downFrom $ size xs) n')

    -- Case no flex
    _ -> return c
-}

instance Subst SizeMeta where
  type SubstArg SizeMeta = Term
  applySubst :: Substitution' (SubstArg SizeMeta) -> SizeMeta -> SizeMeta
applySubst Substitution' (SubstArg SizeMeta)
sigma (SizeMeta MetaId
x [Int]
es) = MetaId -> [Int] -> SizeMeta
SizeMeta MetaId
x ((Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Int
raise [Int]
es)
    where
      raise :: Int -> Int
raise Int
i =
        case Substitution' Term -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' Term
Substitution' (SubstArg SizeMeta)
sigma Int
i of
          Var Int
j [] -> Int
j
          Term
_        -> Int
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Only for 'raise'.
instance Subst (SizeExpr' NamedRigid SizeMeta) where
  type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term
  applySubst :: Substitution' (SubstArg DBSizeExpr) -> DBSizeExpr -> DBSizeExpr
applySubst Substitution' (SubstArg DBSizeExpr)
sigma DBSizeExpr
a =
    case DBSizeExpr
a of
      DBSizeExpr
Infty   -> DBSizeExpr
a
      Const{} -> DBSizeExpr
a
      Flex  SizeMeta
x Offset
n -> SizeMeta -> Offset -> DBSizeExpr
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex (Substitution' (SubstArg SizeMeta) -> SizeMeta -> SizeMeta
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg SizeMeta)
Substitution' (SubstArg DBSizeExpr)
sigma SizeMeta
x) Offset
n
      Rigid NamedRigid
r Offset
n ->
        case Substitution' Term -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' Term
Substitution' (SubstArg DBSizeExpr)
sigma (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ NamedRigid -> Int
rigidIndex NamedRigid
r of
          Var Int
j [] -> NamedRigid -> Offset -> DBSizeExpr
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid NamedRigid
r{ rigidIndex = j } Offset
n
          Term
_        -> DBSizeExpr
forall a. HasCallStack => a
__IMPOSSIBLE__

instance Subst SizeConstraint where
  type SubstArg SizeConstraint = Term
  applySubst :: Substitution' (SubstArg (Constraint' NamedRigid SizeMeta))
-> Constraint' NamedRigid SizeMeta
-> Constraint' NamedRigid SizeMeta
applySubst Substitution' (SubstArg (Constraint' NamedRigid SizeMeta))
sigma (Constraint DBSizeExpr
a Cmp
cmp DBSizeExpr
b) =
    DBSizeExpr -> Cmp -> DBSizeExpr -> Constraint' NamedRigid SizeMeta
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Constraint (Substitution' (SubstArg DBSizeExpr) -> DBSizeExpr -> DBSizeExpr
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Constraint' NamedRigid SizeMeta))
Substitution' (SubstArg DBSizeExpr)
sigma DBSizeExpr
a) Cmp
cmp (Substitution' (SubstArg DBSizeExpr) -> DBSizeExpr -> DBSizeExpr
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Constraint' NamedRigid SizeMeta))
Substitution' (SubstArg DBSizeExpr)
sigma DBSizeExpr
b)

-- | Turn a constraint over de Bruijn indices into a size constraint.
computeSizeConstraint :: ProblemConstraint -> TCM (Maybe HypSizeConstraint)
computeSizeConstraint :: ProblemConstraint -> TCMT IO (Maybe HypSizeConstraint)
computeSizeConstraint ProblemConstraint
c = do
  let cxt :: Context' ContextEntry
cxt = Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
-> TCEnv -> Context' ContextEntry
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (Context' ContextEntry) TCEnv (Context' ContextEntry)
Lens' TCEnv (Context' ContextEntry)
eContext (TCEnv -> Context' ContextEntry) -> TCEnv -> Context' ContextEntry
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv (Closure Constraint -> TCEnv) -> Closure Constraint -> TCEnv
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c
  (Context' ContextEntry -> Context' ContextEntry)
-> TCMT IO (Maybe HypSizeConstraint)
-> TCMT IO (Maybe HypSizeConstraint)
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context' ContextEntry -> Context' ContextEntry) -> tcm a -> tcm a
unsafeModifyContext (Context' ContextEntry
-> Context' ContextEntry -> Context' ContextEntry
forall a b. a -> b -> a
const Context' ContextEntry
cxt) (TCMT IO (Maybe HypSizeConstraint)
 -> TCMT IO (Maybe HypSizeConstraint))
-> TCMT IO (Maybe HypSizeConstraint)
-> TCMT IO (Maybe HypSizeConstraint)
forall a b. (a -> b) -> a -> b
$ do
    case Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> Closure Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c of
      ValueCmp Comparison
CmpLeq CompareAs
_ Term
u Term
v -> do
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
          [ TCMT IO Doc
"converting size constraint"
          , ProblemConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyTCM ProblemConstraint
c
          ]
        ma <- Term -> TCMT IO (Maybe DBSizeExpr)
sizeExpr Term
u
        mb <- sizeExpr v
        (hids, hs) <- unzip <$> getSizeHypotheses cxt
        let mk DBSizeExpr
a DBSizeExpr
b = Context' ContextEntry
-> [Int]
-> [Constraint' NamedRigid SizeMeta]
-> Constraint' NamedRigid SizeMeta
-> HypSizeConstraint
HypSizeConstraint Context' ContextEntry
cxt [Int]
hids [Constraint' NamedRigid SizeMeta]
hs (Constraint' NamedRigid SizeMeta -> HypSizeConstraint)
-> Constraint' NamedRigid SizeMeta -> HypSizeConstraint
forall a b. (a -> b) -> a -> b
$ DBSizeExpr -> Cmp -> DBSizeExpr -> Constraint' NamedRigid SizeMeta
forall rigid flex.
SizeExpr' rigid flex
-> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
Size.Constraint DBSizeExpr
a Cmp
Le DBSizeExpr
b
        -- We only create a size constraint if both terms can be
        -- parsed to our format of size expressions.
        return $ mk <$> ma <*> mb
      Constraint
_ -> TCMT IO (Maybe HypSizeConstraint)
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Turn a term into a size expression.
--
--   Returns 'Nothing' if the term isn't a proper size expression.

sizeExpr :: Term -> TCM (Maybe DBSizeExpr)
sizeExpr :: Term -> TCMT IO (Maybe DBSizeExpr)
sizeExpr Term
u = do
  u <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u -- Andreas, 2009-02-09.
                -- This is necessary to surface the solutions of metavariables.
  reportSDoc "tc.conv.size" 60 $ "sizeExpr:" <+> prettyTCM u
  s <- sizeView u
  case s of
    SizeView
SizeInf     -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr))
-> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a b. (a -> b) -> a -> b
$ DBSizeExpr -> Maybe DBSizeExpr
forall a. a -> Maybe a
Just DBSizeExpr
forall rigid flex. SizeExpr' rigid flex
Infty
    SizeSuc Term
u   -> (DBSizeExpr -> DBSizeExpr) -> Maybe DBSizeExpr -> Maybe DBSizeExpr
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DBSizeExpr -> Offset -> DBSizeExpr
forall a b c. Plus a b c => a -> b -> c
`plus` (Offset
1 :: Offset)) (Maybe DBSizeExpr -> Maybe DBSizeExpr)
-> TCMT IO (Maybe DBSizeExpr) -> TCMT IO (Maybe DBSizeExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO (Maybe DBSizeExpr)
sizeExpr Term
u
    OtherSize Term
u -> case Term
u of
      Var Int
i []    -> (\ [Char]
x -> DBSizeExpr -> Maybe DBSizeExpr
forall a. a -> Maybe a
Just (DBSizeExpr -> Maybe DBSizeExpr) -> DBSizeExpr -> Maybe DBSizeExpr
forall a b. (a -> b) -> a -> b
$ NamedRigid -> Offset -> DBSizeExpr
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid ([Char] -> Int -> NamedRigid
NamedRigid [Char]
x Int
i) Offset
0) ([Char] -> Maybe DBSizeExpr)
-> (Name -> [Char]) -> Name -> Maybe DBSizeExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> Maybe DBSizeExpr)
-> TCMT IO Name -> TCMT IO (Maybe DBSizeExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Name
forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Name
nameOfBV Int
i
--      MetaV m es  -> return $ Just $ Flex (SizeMeta m es) 0
      MetaV MetaId
m Elims
es | Just [Int]
xs <- (Elim' Term -> Maybe Int) -> Elims -> Maybe [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> Maybe Int
isVar Elims
es, [Int] -> Bool
forall a. Ord a => [a] -> Bool
List.fastDistinct [Int]
xs
                  -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr))
-> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a b. (a -> b) -> a -> b
$ DBSizeExpr -> Maybe DBSizeExpr
forall a. a -> Maybe a
Just (DBSizeExpr -> Maybe DBSizeExpr) -> DBSizeExpr -> Maybe DBSizeExpr
forall a b. (a -> b) -> a -> b
$ SizeMeta -> Offset -> DBSizeExpr
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex (MetaId -> [Int] -> SizeMeta
SizeMeta MetaId
m [Int]
xs) Offset
0
      Term
_           -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DBSizeExpr
forall a. Maybe a
Nothing
  where
    isVar :: Elim' Term -> Maybe Int
isVar (Proj{})  = Maybe Int
forall a. Maybe a
Nothing
    isVar (IApply Term
_ Term
_ Term
v) = Elim' Term -> Maybe Int
isVar (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v))
    isVar (Apply Arg Term
v) = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v of
      Var Int
i [] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
      Term
_        -> Maybe Int
forall a. Maybe a
Nothing