{-# 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 hiding (forM, forM_)
import Control.Monad.Except
import Control.Monad.Trans.Maybe

import Data.Either
import Data.Foldable (forM_)
import qualified Data.Foldable as Fold
import Data.Function
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.Syntax as Size
import Agda.TypeChecking.SizedTypes.Utils
import Agda.TypeChecking.SizedTypes.WarshallSolver as Size

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.Utils.Pretty (Pretty, prettyShow)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.VarSet as VarSet

import Agda.Utils.Impossible

type CC = ProblemConstraint

-- | 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
/= :: DefaultToInfty -> DefaultToInfty -> Bool
$c/= :: DefaultToInfty -> DefaultToInfty -> Bool
== :: DefaultToInfty -> DefaultToInfty -> Bool
$c== :: 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
min :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
$cmin :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
max :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
$cmax :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
>= :: DefaultToInfty -> DefaultToInfty -> Bool
$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
compare :: DefaultToInfty -> DefaultToInfty -> Ordering
$ccompare :: DefaultToInfty -> DefaultToInfty -> Ordering
Ord, Int -> DefaultToInfty -> ShowS
[DefaultToInfty] -> ShowS
DefaultToInfty -> String
(Int -> DefaultToInfty -> ShowS)
-> (DefaultToInfty -> String)
-> ([DefaultToInfty] -> ShowS)
-> Show DefaultToInfty
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DefaultToInfty] -> ShowS
$cshowList :: [DefaultToInfty] -> ShowS
show :: DefaultToInfty -> String
$cshow :: DefaultToInfty -> String
showsPrec :: Int -> DefaultToInfty -> ShowS
$cshowsPrec :: Int -> 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.

  let norm :: ProblemConstraint -> m ProblemConstraint
norm ProblemConstraint
c = (Constraint -> m Constraint)
-> Closure Constraint -> m (Closure Constraint)
forall (m :: * -> *) a b.
(MonadTCEnv m, ReadTCState m) =>
(a -> m b) -> Closure a -> m (Closure b)
mapClosure Constraint -> m Constraint
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) m (Closure Constraint)
-> (Closure Constraint -> ProblemConstraint) -> m ProblemConstraint
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Closure Constraint
cl -> ProblemConstraint
c { theConstraint :: Closure Constraint
theConstraint = Closure Constraint
cl }
  [ProblemConstraint]
cs0 <- (ProblemConstraint -> TCMT IO ProblemConstraint)
-> [ProblemConstraint] -> TCMT IO [ProblemConstraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ProblemConstraint -> TCMT IO ProblemConstraint
forall {m :: * -> *}.
MonadReduce m =>
ProblemConstraint -> m ProblemConstraint
norm ([ProblemConstraint] -> TCMT IO [ProblemConstraint])
-> TCMT IO [ProblemConstraint] -> TCMT IO [ProblemConstraint]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Comparison -> Bool) -> TCMT IO [ProblemConstraint]
S.takeSizeConstraints (Comparison -> Comparison -> Bool
forall a. Eq a => a -> a -> Bool
== Comparison
CmpLeq)
    -- NOTE: this deletes the size constraints from the constraint set!
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ProblemConstraint] -> Bool
forall a. Null a => a -> Bool
null [ProblemConstraint]
cs0) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.size.solve" Int
40 (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
$
      String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ( String
"Solving constraints (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ DefaultToInfty -> String
forall a. Show a => a -> String
show DefaultToInfty
flag String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")" ) TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (ProblemConstraint -> TCMT IO Doc)
-> [ProblemConstraint] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ProblemConstraint]
cs0
  let -- Error for giving up
      cannotSolve :: TCM a -- Defined, but not currently used
      cannotSolve :: forall a. TCM a
cannotSolve = 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
. Doc -> TypeError
GenericDocError (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] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (TCMT IO Doc
"Cannot solve size constraints" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (ProblemConstraint -> TCMT IO Doc)
-> [ProblemConstraint] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ProblemConstraint]
cs0)

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

  -- Get all size metas.
  Set MetaId
sizeMetaSet <- [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList ([MetaId] -> Set MetaId)
-> ([(MetaId, Type, Tele (Dom Type))] -> [MetaId])
-> [(MetaId, Type, Tele (Dom Type))]
-> Set MetaId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((MetaId, Type, Tele (Dom Type)) -> MetaId)
-> [(MetaId, Type, Tele (Dom Type))] -> [MetaId]
forall a b. (a -> b) -> [a] -> [b]
map (\ (MetaId
x, Type
_t, Tele (Dom Type)
_tel) -> MetaId
x) ([(MetaId, Type, Tele (Dom Type))] -> Set MetaId)
-> TCMT IO [(MetaId, Type, Tele (Dom Type))]
-> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> TCMT IO [(MetaId, Type, Tele (Dom Type))]
S.getSizeMetas Bool
True

  -- Pair each constraint with its list of size metas occurring in it.
  [(ProblemConstraint, [Int])]
cms <- [ProblemConstraint]
-> (ProblemConstraint -> TCMT IO (ProblemConstraint, [Int]))
-> TCMT IO [(ProblemConstraint, [Int])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ProblemConstraint]
cs0 ((ProblemConstraint -> TCMT IO (ProblemConstraint, [Int]))
 -> TCMT IO [(ProblemConstraint, [Int])])
-> (ProblemConstraint -> TCMT IO (ProblemConstraint, [Int]))
-> TCMT IO [(ProblemConstraint, [Int])]
forall a b. (a -> b) -> a -> b
$ \ ProblemConstraint
cl -> Closure Constraint
-> (Constraint -> TCMT IO (ProblemConstraint, [Int]))
-> TCMT IO (ProblemConstraint, [Int])
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
cl) ((Constraint -> TCMT IO (ProblemConstraint, [Int]))
 -> TCMT IO (ProblemConstraint, [Int]))
-> (Constraint -> TCMT IO (ProblemConstraint, [Int]))
-> TCMT IO (ProblemConstraint, [Int])
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, [Int]) -> TCMT IO (ProblemConstraint, [Int])
forall (m :: * -> *) a. Monad m => a -> m a
return (ProblemConstraint
cl, (MetaId -> Int) -> [MetaId] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> Int
metaId ([MetaId] -> [Int])
-> (Set MetaId -> [MetaId]) -> Set MetaId -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList (Set MetaId -> [Int]) -> Set MetaId -> [Int]
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 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 :: forall a b. (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 ([ProblemConstraint]
clcs, [(ProblemConstraint, List1 Int)]
othercs) = [Either ProblemConstraint (ProblemConstraint, List1 Int)]
-> ([ProblemConstraint], [(ProblemConstraint, List1 Int)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either ProblemConstraint (ProblemConstraint, List1 Int)]
 -> ([ProblemConstraint], [(ProblemConstraint, List1 Int)]))
-> [Either ProblemConstraint (ProblemConstraint, List1 Int)]
-> ([ProblemConstraint], [(ProblemConstraint, List1 Int)])
forall a b. (a -> b) -> a -> b
$ ((ProblemConstraint, [Int])
 -> Either ProblemConstraint (ProblemConstraint, List1 Int))
-> [(ProblemConstraint, [Int])]
-> [Either ProblemConstraint (ProblemConstraint, List1 Int)]
forall a b. (a -> b) -> [a] -> [b]
map (ProblemConstraint, [Int])
-> Either ProblemConstraint (ProblemConstraint, List1 Int)
forall a b. (a, [b]) -> Either a (a, List1 b)
classify [(ProblemConstraint, [Int])]
cms

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

  -- 3. Solve each cluster

  -- Solve the closed constraints, one by one.

  [ProblemConstraint] -> (ProblemConstraint -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [ProblemConstraint]
clcs ((ProblemConstraint -> TCM ()) -> TCM ())
-> (ProblemConstraint -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ ProblemConstraint
c -> () () -> TCMT IO (Set MetaId) -> TCM ()
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.

  Set MetaId
constrainedMetas <- [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set MetaId] -> Set MetaId)
-> TCMT IO [Set MetaId] -> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [NonEmpty ProblemConstraint]
-> (NonEmpty ProblemConstraint -> TCMT IO (Set MetaId))
-> TCMT IO [Set MetaId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM  ([NonEmpty ProblemConstraint]
ccs) ((NonEmpty ProblemConstraint -> TCMT IO (Set MetaId))
 -> TCMT IO [Set MetaId])
-> (NonEmpty ProblemConstraint -> TCMT IO (Set MetaId))
-> TCMT IO [Set MetaId]
forall a b. (a -> b) -> a -> b
$ \ (NonEmpty ProblemConstraint
cs :: List1 CC) -> do

      String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc)
-> (ProblemConstraint -> String)
-> ProblemConstraint
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> String
forall a. Show a => a -> String
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 :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
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 -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Context -> Int)
-> (Closure Constraint -> Context) -> Closure Constraint -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> Context
envContext (TCEnv -> Context)
-> (Closure Constraint -> TCEnv) -> Closure Constraint -> Context
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 (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.
        [ProblemConstraint]
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)
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

        String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
          ( TCMT IO Doc
"converted size constraints to context: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
              Tele (Dom Type)
tel <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
              TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
tel
          ) TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (ProblemConstraint -> TCMT IO Doc)
-> [ProblemConstraint] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc)
-> (ProblemConstraint -> TCMT IO Doc)
-> ProblemConstraint
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM) [ProblemConstraint]
cs'

        -- Solve the converted constraints.
        DefaultToInfty -> [ProblemConstraint] -> TCMT IO (Set MetaId)
solveSizeConstraints_ DefaultToInfty
flag [ProblemConstraint]
cs'

  -- 4. Possibly set remaining metas to infinity.

  -- Andreas, issue 1862: do not default to ∞ always, could be too early.
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (DefaultToInfty
flag DefaultToInfty -> DefaultToInfty -> Bool
forall a. Eq a => a -> a -> Bool
== DefaultToInfty
DefaultToInfty) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

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

    -- Set the unconstrained, open size metas to ∞.
    [(MetaId, Type, Tele (Dom Type))]
ms <- Bool -> TCMT IO [(MetaId, Type, Tele (Dom Type))]
S.getSizeMetas Bool
False -- do not get interaction metas
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(MetaId, Type, Tele (Dom Type))] -> Bool
forall a. Null a => a -> Bool
null [(MetaId, Type, Tele (Dom Type))]
ms) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      Term
inf <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
      [(MetaId, Type, Tele (Dom Type))]
-> ((MetaId, Type, Tele (Dom Type)) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(MetaId, Type, Tele (Dom Type))]
ms (((MetaId, Type, Tele (Dom Type)) -> TCM ()) -> TCM ())
-> ((MetaId, Type, Tele (Dom Type)) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (MetaId
m, Type
t, Tele (Dom Type)
tel) -> do
        Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
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 :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
        String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
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
prettyTCM Term
inf
        Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta Int
0 MetaId
m Type
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) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) Term
inf

  -- -- Double check.
  -- 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.
  [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


-- | 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  = TCEnv -> ModuleName
envCurrentModule (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
delta = TCEnv -> Context
envContext (TCEnv -> Context) -> TCEnv -> Context
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.
  Tele (Dom Type)
delta1 <- TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type))
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type)))
-> TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type)
-> (Section -> Tele (Dom Type)) -> Maybe Section -> Tele (Dom Type)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Tele (Dom Type)
forall a. Null a => a
empty (Section -> Lens' (Tele (Dom Type)) Section -> Tele (Dom Type)
forall o i. o -> Lens' i o -> i
^. Lens' (Tele (Dom Type)) Section
secTelescope) (Maybe Section -> Tele (Dom Type))
-> TCMT IO (Maybe Section) -> TCMT IO (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO (Maybe Section)
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Maybe Section)
getSection ModuleName
modN
  -- The number of locals of the constraint.
  let delta2 :: Int
delta2 = Context -> Int
forall a. Sized a => a -> Int
size Context
delta Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta1
  Bool -> MaybeT (TCMT IO) () -> MaybeT (TCMT IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
delta2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) MaybeT (TCMT IO) ()
forall a. HasCallStack => a
__IMPOSSIBLE__

  -- The current module M and context Γ.
  ModuleName
modM  <- MaybeT (TCMT IO) ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  Int
gamma <- TCM Int -> MaybeT (TCMT IO) Int
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Int -> MaybeT (TCMT IO) Int)
-> TCM Int -> MaybeT (TCMT IO) Int
forall a b. (a -> b) -> a -> b
$ TCM Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
  -- The current module telescope.
  -- Could also be empty, if we are in the front matter or telescope of the top-level module.
  Tele (Dom Type)
gamma1 <-TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type))
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type)))
-> TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type)
-> (Section -> Tele (Dom Type)) -> Maybe Section -> Tele (Dom Type)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Tele (Dom Type)
forall a. Null a => a
empty (Section -> Lens' (Tele (Dom Type)) Section -> Tele (Dom Type)
forall o i. o -> Lens' i o -> i
^. Lens' (Tele (Dom Type)) Section
secTelescope) (Maybe Section -> Tele (Dom Type))
-> TCMT IO (Maybe Section) -> TCMT IO (Tele (Dom Type))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO (Maybe Section)
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Maybe Section)
getSection ModuleName
modM
  -- The current locals.
  let gamma2 :: Int
gamma2 = Int
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma1

  -- Γ ⊢ σ : Δ₁
  Substitution' Term
sigma <- TCM (Substitution' Term) -> MaybeT (TCMT IO) (Substitution' Term)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Substitution' Term) -> MaybeT (TCMT IO) (Substitution' Term))
-> TCM (Substitution' Term)
-> MaybeT (TCMT IO) (Substitution' Term)
forall a b. (a -> b) -> a -> b
$ Substitution' Term
-> Maybe (Substitution' Term) -> Substitution' Term
forall a. a -> Maybe a -> a
fromMaybe Substitution' Term
forall a. Substitution' a
idS (Maybe (Substitution' Term) -> Substitution' Term)
-> TCMT IO (Maybe (Substitution' Term)) -> TCM (Substitution' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO (Maybe (Substitution' Term))
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ModuleName -> m (Maybe (Substitution' Term))
getModuleParameterSub ModuleName
modN

  -- Debug printing.
  String -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.constr.cast" Int
40 (TCMT IO Doc -> MaybeT (TCMT IO) ())
-> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"casting constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ do
    Tele (Dom Type)
tel <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
    TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
      [ TCMT IO Doc
"current module                = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
modM
      , TCMT IO Doc
"current module telescope      = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
gamma1
      , TCMT IO Doc
"current context               = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
tel
      , TCMT IO Doc
"constraint module             = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ModuleName
modN
      , TCMT IO Doc
"constraint module telescope   = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Tele (Dom Type)
delta1
      , TCMT IO Doc
"constraint context            = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Tele (Dom Type) -> TCMT IO Doc)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Closure Constraint
-> (Constraint -> TCMT IO (Tele (Dom Type)))
-> TCMT IO (Tele (Dom Type))
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
cl (TCMT IO (Tele (Dom Type))
-> Constraint -> TCMT IO (Tele (Dom Type))
forall a b. a -> b -> a
const (TCMT IO (Tele (Dom Type))
 -> Constraint -> TCMT IO (Tele (Dom Type)))
-> TCMT IO (Tele (Dom Type))
-> Constraint
-> TCMT IO (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope))
      , TCMT IO Doc
"constraint                    = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Closure Constraint -> (Constraint -> TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
cl Constraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM
      , TCMT IO Doc
"module parameter substitution = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution' Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Substitution' Term
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.
  Bool -> MaybeT (TCMT IO) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Int
gamma2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0)

  -- Shortcut for modN == modM:
  -- Raise constraint from Δ to Γ, if possible.
  -- This might save us some strengthening.
  if ModuleName
modN ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
modM then Int -> Constraint -> MaybeT (TCMT IO) Constraint
forall {m :: * -> *} {b}.
(Monad m, Alternative m, Free b, Subst b) =>
Int -> b -> m b
raiseMaybe (Int
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
- Context -> Int
forall a. Sized a => a -> Int
size Context
delta) (Constraint -> MaybeT (TCMT IO) Constraint)
-> Constraint -> MaybeT (TCMT IO) Constraint
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> Constraint
forall a. Closure a -> a
clValue Closure Constraint
cl else do

  -- Strengthen constraint to Δ₁ ⊢ c
  Constraint
c <- Int -> Constraint -> MaybeT (TCMT IO) Constraint
forall {m :: * -> *} {b}.
(Monad m, Alternative m, Free b, Subst b) =>
Int -> b -> m b
raiseMaybe (-Int
delta2) (Constraint -> MaybeT (TCMT IO) Constraint)
-> Constraint -> MaybeT (TCMT IO) Constraint
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> Constraint
forall a. Closure a -> a
clValue Closure Constraint
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)
  Int
fv <- TCM Int -> MaybeT (TCMT IO) Int
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Int -> MaybeT (TCMT IO) Int)
-> TCM Int -> MaybeT (TCMT IO) Int
forall a b. (a -> b) -> a -> b
$ ModuleName -> TCM Int
forall (m :: * -> *).
(Functor m, Applicative m, MonadTCEnv m, ReadTCState m) =>
ModuleName -> m Int
getModuleFreeVars ModuleName
modN
  Bool -> MaybeT (TCMT IO) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (TCMT IO) ()) -> Bool -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ Int
fv Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta1

  -- Γ ⊢ c[σ]
  Constraint -> MaybeT (TCMT IO) Constraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Constraint -> MaybeT (TCMT IO) Constraint)
-> Constraint -> MaybeT (TCMT IO) Constraint
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Constraint) -> Constraint -> Constraint
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Constraint)
sigma Constraint
c
  where
    raiseMaybe :: Int -> b -> m b
raiseMaybe Int
n b
c = do
      -- Fine if we have to weaken or strengthening is safe.
      Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
|| (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
List.all (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= -Int
n) (IntSet -> [Int]
VarSet.toList (IntSet -> [Int]) -> IntSet -> [Int]
forall a b. (a -> b) -> a -> b
$ b -> IntSet
forall t. Free t => t -> IntSet
allFreeVars b
c)
      b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> m b) -> b -> m b
forall a b. (a -> b) -> a -> b
$ Int -> b -> b
forall a. Subst a => Int -> a -> a
raise Int
n b
c


-- | 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 = TCEnv -> CheckpointId
envCurrentCheckpoint (TCEnv -> CheckpointId) -> TCEnv -> CheckpointId
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure Constraint
cl
  Substitution' Term
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' (Maybe (Substitution' Term)) TCEnv
-> MaybeT (TCMT IO) (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC (Lens' (Maybe (Substitution' Term)) TCEnv
 -> MaybeT (TCMT IO) (Maybe (Substitution' Term)))
-> Lens' (Maybe (Substitution' Term)) TCEnv
-> 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' (Map CheckpointId (Substitution' Term)) TCEnv
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'
     (Maybe (Substitution' Term))
     (Map CheckpointId (Substitution' Term))
forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key CheckpointId
cp)
          (do
            -- We are not in a descendant of the constraint checkpoint.
            -- Here be dragons!!
            Context
gamma <- (TCEnv -> Context) -> MaybeT (TCMT IO) Context
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Context
envContext -- The target context
            let findInGamma :: Dom' Term (Name, Type) -> Maybe Int
findInGamma (Dom {unDom :: forall t e. Dom' t e -> e
unDom = (Name
x, Type
t)}) =
                  -- match by name (hazardous)
                  -- This is one of the seven deadly sins (not respecting alpha).
                  (Dom' Term (Name, Type) -> Bool) -> Context -> Maybe Int
forall a. (a -> Bool) -> [a] -> Maybe Int
List.findIndex ((Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==) (Name -> Bool)
-> (Dom' Term (Name, Type) -> Name)
-> Dom' Term (Name, Type)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
gamma
            let delta :: Context
delta = TCEnv -> Context
envContext (TCEnv -> Context) -> TCEnv -> Context
forall a b. (a -> b) -> a -> b
$ Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure Constraint
cl
                cand :: [Maybe Int]
cand  = (Dom' Term (Name, Type) -> Maybe Int) -> Context -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (Name, Type) -> Maybe Int
findInGamma Context
delta
            -- The domain of our substitution
            let coveredVars :: IntSet
coveredVars = [Int] -> IntSet
VarSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
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.
            Bool -> MaybeT (TCMT IO) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT (TCMT IO) ()) -> Bool -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ All -> Bool
getAll (All -> Bool) -> All -> Bool
forall a b. (a -> b) -> a -> b
$ SingleVar All -> IgnoreSorts -> Constraint -> All
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Bool -> All
All (Bool -> All) -> (Int -> Bool) -> SingleVar All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> IntSet -> Bool
`VarSet.member` IntSet
coveredVars)) IgnoreSorts
IgnoreAll (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue Closure Constraint
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__.
            Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term))
-> Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term)
forall a b. (a -> b) -> a -> b
$ [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ (Maybe Int -> Term) -> [Maybe Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> (Int -> Term) -> Maybe Int -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term
HasCallStack => Term
__DUMMY_TERM__ Int -> Term
var) [Maybe Int]
cand
          ) Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term)
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.
  Closure Constraint
cl' <- Constraint -> MaybeT (TCMT IO) (Closure Constraint)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure (Constraint -> MaybeT (TCMT IO) (Closure Constraint))
-> Constraint -> MaybeT (TCMT IO) (Closure Constraint)
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Constraint) -> Constraint -> Constraint
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Constraint)
sigma (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue Closure Constraint
cl)
  ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint)
-> ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
forall a b. (a -> b) -> a -> b
$ ProblemConstraint
c { theConstraint :: Closure Constraint
theConstraint = Closure Constraint
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 -> [CC] -> 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.
  [(ProblemConstraint, HypSizeConstraint)]
ccs :: [(CC,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 (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.
  [(ProblemConstraint, HypSizeConstraint)]
ccs' <- [[(ProblemConstraint, HypSizeConstraint)]]
-> [(ProblemConstraint, HypSizeConstraint)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(ProblemConstraint, HypSizeConstraint)]]
 -> [(ProblemConstraint, HypSizeConstraint)])
-> TCMT IO [[(ProblemConstraint, HypSizeConstraint)]]
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [(ProblemConstraint, HypSizeConstraint)]
-> ((ProblemConstraint, HypSizeConstraint)
    -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
-> TCMT IO [[(ProblemConstraint, HypSizeConstraint)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ProblemConstraint, HypSizeConstraint)]
ccs (((ProblemConstraint, HypSizeConstraint)
  -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
 -> TCMT IO [[(ProblemConstraint, HypSizeConstraint)]])
-> ((ProblemConstraint, HypSizeConstraint)
    -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
-> TCMT IO [[(ProblemConstraint, HypSizeConstraint)]]
forall a b. (a -> b) -> a -> b
$ \ (ProblemConstraint
c0, HypSizeConstraint Context
cxt [Int]
hids [SizeConstraint]
hs SizeConstraint
sc) -> do
      case CTrans NamedRigid SizeMeta -> CTrans NamedRigid SizeMeta
forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
simplify1 (\ SizeConstraint
sc -> [SizeConstraint] -> Either String [SizeConstraint]
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeConstraint
sc]) SizeConstraint
sc of
        Left String
_ -> TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
-> (Doc -> TypeError)
-> Doc
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
-> TCMT IO Doc -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
          TCMT IO Doc
"Contradictory size constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ProblemConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM ProblemConstraint
c0
        Right [SizeConstraint]
cs -> [(ProblemConstraint, HypSizeConstraint)]
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
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))
-> (SizeConstraint -> HypSizeConstraint)
-> SizeConstraint
-> (ProblemConstraint, HypSizeConstraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context
-> [Int] -> [SizeConstraint] -> SizeConstraint -> HypSizeConstraint
HypSizeConstraint Context
cxt [Int]
hids [SizeConstraint]
hs (SizeConstraint -> (ProblemConstraint, HypSizeConstraint))
-> [SizeConstraint] -> [(ProblemConstraint, HypSizeConstraint)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SizeConstraint]
cs

  -- Cluster constraints according to the meta variables they mention.
  -- @csNoM@ are the constraints that do not mention any meta.
  let ([(ProblemConstraint, HypSizeConstraint)]
csNoM, [((ProblemConstraint, HypSizeConstraint), List1 Int)]
csMs) = (((ProblemConstraint, HypSizeConstraint)
 -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int))
-> [(ProblemConstraint, HypSizeConstraint)]
-> ([(ProblemConstraint, HypSizeConstraint)],
    [((ProblemConstraint, HypSizeConstraint), List1 Int)])
forall a b. (a -> Maybe b) -> [a] -> ([a], [b])
`List.partitionMaybe` [(ProblemConstraint, HypSizeConstraint)]
ccs') (((ProblemConstraint, HypSizeConstraint)
  -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int))
 -> ([(ProblemConstraint, HypSizeConstraint)],
     [((ProblemConstraint, HypSizeConstraint), List1 Int)]))
-> ((ProblemConstraint, HypSizeConstraint)
    -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int))
-> ([(ProblemConstraint, HypSizeConstraint)],
    [((ProblemConstraint, HypSizeConstraint), List1 Int)])
forall a b. (a -> b) -> a -> b
$ \ p :: (ProblemConstraint, HypSizeConstraint)
p@(ProblemConstraint
c0, HypSizeConstraint
c) ->
        (List1 Int -> ((ProblemConstraint, HypSizeConstraint), List1 Int))
-> Maybe (List1 Int)
-> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ProblemConstraint, HypSizeConstraint)
p,) (Maybe (List1 Int)
 -> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int))
-> Maybe (List1 Int)
-> Maybe ((ProblemConstraint, HypSizeConstraint), List1 Int)
forall a b. (a -> b) -> a -> b
$ [Int] -> Maybe (List1 Int)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([Int] -> Maybe (List1 Int)) -> [Int] -> Maybe (List1 Int)
forall a b. (a -> b) -> a -> b
$ (SizeMeta -> Int) -> [SizeMeta] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (MetaId -> Int
metaId (MetaId -> Int) -> (SizeMeta -> MetaId) -> SizeMeta -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeMeta -> MetaId
sizeMetaId) ([SizeMeta] -> [Int]) -> [SizeMeta] -> [Int]
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 (CC,HypSizeConstraint)]
      css :: [List1 (ProblemConstraint, HypSizeConstraint)]
css = [((ProblemConstraint, HypSizeConstraint), List1 Int)]
-> [List1 (ProblemConstraint, HypSizeConstraint)]
forall a. [(a, List1 Int)] -> [NonEmpty a]
cluster' [((ProblemConstraint, HypSizeConstraint), List1 Int)]
csMs

  -- Check that the closed constraints are valid.
  Maybe (List1 (ProblemConstraint, HypSizeConstraint))
-> (List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
-> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust ([(ProblemConstraint, HypSizeConstraint)]
-> Maybe (List1 (ProblemConstraint, HypSizeConstraint))
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty [(ProblemConstraint, HypSizeConstraint)]
csNoM) ((List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
 -> TCM ())
-> (List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
-> TCM ()
forall a b. (a -> b) -> a -> b
$ DefaultToInfty
-> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
solveCluster DefaultToInfty
flag

  -- Now, process the clusters.
  [List1 (ProblemConstraint, HypSizeConstraint)]
-> (List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
-> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [List1 (ProblemConstraint, HypSizeConstraint)]
css ((List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
 -> TCM ())
-> (List1 (ProblemConstraint, HypSizeConstraint) -> TCM ())
-> TCM ()
forall a b. (a -> b) -> a -> b
$ DefaultToInfty
-> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
solveCluster DefaultToInfty
flag

  Set MetaId -> TCMT IO (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCMT IO (Set MetaId))
-> Set MetaId -> TCMT IO (Set MetaId)
forall a b. (a -> b) -> a -> b
$ (SizeMeta -> MetaId) -> Set SizeMeta -> Set MetaId
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic SizeMeta -> MetaId
sizeMetaId (Set SizeMeta -> Set MetaId) -> Set SizeMeta -> Set MetaId
forall a b. (a -> b) -> a -> b
$ [HypSizeConstraint] -> Set (FlexOf [HypSizeConstraint])
forall a. Flexs a => a -> Set (FlexOf a)
flexs ([HypSizeConstraint] -> Set (FlexOf [HypSizeConstraint]))
-> [HypSizeConstraint] -> Set (FlexOf [HypSizeConstraint])
forall a b. (a -> b) -> a -> b
$ (((ProblemConstraint, HypSizeConstraint), List1 Int)
 -> HypSizeConstraint)
-> [((ProblemConstraint, HypSizeConstraint), List1 Int)]
-> [HypSizeConstraint]
forall a b. (a -> b) -> [a] -> [b]
map ((ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint
forall a b. (a, b) -> b
snd ((ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint)
-> (((ProblemConstraint, HypSizeConstraint), List1 Int)
    -> (ProblemConstraint, HypSizeConstraint))
-> ((ProblemConstraint, HypSizeConstraint), List1 Int)
-> HypSizeConstraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ProblemConstraint, HypSizeConstraint), List1 Int)
-> (ProblemConstraint, HypSizeConstraint)
forall a b. (a, b) -> a
fst) [((ProblemConstraint, HypSizeConstraint), List1 Int)]
csMs

-- | Solve a cluster of constraints sharing some metas.
--
solveCluster :: DefaultToInfty -> List1 (CC, HypSizeConstraint) -> TCM ()
solveCluster :: DefaultToInfty
-> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
solveCluster DefaultToInfty
flag List1 (ProblemConstraint, HypSizeConstraint)
ccs = do
  let cs :: NonEmpty HypSizeConstraint
cs = ((ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint)
-> List1 (ProblemConstraint, HypSizeConstraint)
-> NonEmpty HypSizeConstraint
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
  let prettyCs :: [TCMT IO Doc]
prettyCs   = (HypSizeConstraint -> TCMT IO Doc)
-> [HypSizeConstraint] -> [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
prettyTCM ([HypSizeConstraint] -> [TCMT IO Doc])
-> [HypSizeConstraint] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ NonEmpty HypSizeConstraint -> [HypSizeConstraint]
forall a. NonEmpty a -> [a]
List1.toList NonEmpty HypSizeConstraint
cs
  let err :: String -> TCMT IO (Solution NamedRigid Int)
err String
reason = TypeError -> TCMT IO (Solution NamedRigid Int)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Solution NamedRigid Int))
-> (Doc -> TypeError) -> Doc -> TCMT IO (Solution NamedRigid Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO (Solution NamedRigid Int))
-> TCMT IO Doc -> TCMT IO (Solution NamedRigid Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        [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
$
          [ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"Cannot solve size constraints" ] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [TCMT IO Doc]
prettyCs [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
          [ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"Reason: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
reason ]
  String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"Solving constraint cluster" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: [TCMT IO Doc]
prettyCs
  -- 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
gamma [Int]
hids [SizeConstraint]
hs SizeConstraint
_ = (HypSizeConstraint -> HypSizeConstraint -> Ordering)
-> NonEmpty 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 -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Context -> Int)
-> (HypSizeConstraint -> Context) -> HypSizeConstraint -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HypSizeConstraint -> Context
sizeContext)) NonEmpty HypSizeConstraint
cs
  -- Length of longest context.
  let n :: Int
n = Context -> Int
forall a. Sized a => a -> Int
size Context
gamma

  -- Now convert all size constraints to the largest context.
      csL :: NonEmpty SizeConstraint
csL = NonEmpty HypSizeConstraint
-> (HypSizeConstraint -> SizeConstraint) -> NonEmpty SizeConstraint
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for NonEmpty HypSizeConstraint
cs ((HypSizeConstraint -> SizeConstraint) -> NonEmpty SizeConstraint)
-> (HypSizeConstraint -> SizeConstraint) -> NonEmpty SizeConstraint
forall a b. (a -> b) -> a -> b
$ \ (HypSizeConstraint Context
cxt [Int]
_ [SizeConstraint]
_ SizeConstraint
c) -> Int -> SizeConstraint -> SizeConstraint
forall a. Subst a => Int -> a -> a
raise (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Context -> Int
forall a. Sized a => a -> Int
size Context
cxt) SizeConstraint
c
  -- Canonicalize the constraints.
  -- This is unsound in the presence of hypotheses.
      csC :: [SizeConstraint]
      csC :: [SizeConstraint]
csC = Bool
-> ([SizeConstraint] -> [SizeConstraint])
-> [SizeConstraint]
-> [SizeConstraint]
forall a. Bool -> (a -> a) -> a -> a
applyWhen ([SizeConstraint] -> Bool
forall a. Null a => a -> Bool
null [SizeConstraint]
hs) ((SizeConstraint -> Maybe SizeConstraint)
-> [SizeConstraint] -> [SizeConstraint]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SizeConstraint -> Maybe SizeConstraint
canonicalizeSizeConstraint) ([SizeConstraint] -> [SizeConstraint])
-> [SizeConstraint] -> [SizeConstraint]
forall a b. (a -> b) -> a -> b
$ NonEmpty SizeConstraint -> [SizeConstraint]
forall a. NonEmpty a -> [a]
List1.toList NonEmpty SizeConstraint
csL
  String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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]
++
    (SizeConstraint -> TCMT IO Doc)
-> [SizeConstraint] -> [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
prettyTCM (HypSizeConstraint -> TCMT IO Doc)
-> (SizeConstraint -> HypSizeConstraint)
-> SizeConstraint
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context
-> [Int] -> [SizeConstraint] -> SizeConstraint -> HypSizeConstraint
HypSizeConstraint Context
gamma [Int]
hids [SizeConstraint]
hs) [SizeConstraint]
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]
++
    (SizeConstraint -> TCMT IO Doc)
-> [SizeConstraint] -> [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
prettyTCM (HypSizeConstraint -> TCMT IO Doc)
-> (SizeConstraint -> HypSizeConstraint)
-> SizeConstraint
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context
-> [Int] -> [SizeConstraint] -> SizeConstraint -> HypSizeConstraint
HypSizeConstraint Context
gamma [Int]
hids [SizeConstraint]
hs) [SizeConstraint]
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 = (SizeConstraint -> [SizeMeta]) -> [SizeConstraint] -> [SizeMeta]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((SizeMeta -> [SizeMeta]) -> SizeConstraint -> [SizeMeta]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (SizeMeta -> [SizeMeta] -> [SizeMeta]
forall a. a -> [a] -> [a]
:[])) [SizeConstraint]
csC
      csF   :: [Size.Constraint' NamedRigid Int]
      csF :: [Constraint' NamedRigid Int]
csF   = (SizeConstraint -> Constraint' NamedRigid Int)
-> [SizeConstraint] -> [Constraint' NamedRigid Int]
forall a b. (a -> b) -> [a] -> [b]
map ((SizeMeta -> Int) -> SizeConstraint -> Constraint' NamedRigid Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MetaId -> Int
metaId (MetaId -> Int) -> (SizeMeta -> MetaId) -> SizeMeta -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeMeta -> MetaId
sizeMetaId)) [SizeConstraint]
csC

  -- Construct the hypotheses graph.
  let hyps :: [Constraint' NamedRigid Int]
hyps = (SizeConstraint -> Constraint' NamedRigid Int)
-> [SizeConstraint] -> [Constraint' NamedRigid Int]
forall a b. (a -> b) -> [a] -> [b]
map ((SizeMeta -> Int) -> SizeConstraint -> Constraint' NamedRigid Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MetaId -> Int
metaId (MetaId -> Int) -> (SizeMeta -> MetaId) -> SizeMeta -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeMeta -> MetaId
sizeMetaId)) [SizeConstraint]
hs
  -- There cannot be negative cycles in hypotheses graph due to scoping.
  let hg :: HypGraph NamedRigid Int
hg = (String -> HypGraph NamedRigid Int)
-> (HypGraph NamedRigid Int -> HypGraph NamedRigid Int)
-> Either String (HypGraph NamedRigid Int)
-> HypGraph NamedRigid Int
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> HypGraph NamedRigid Int
forall a. HasCallStack => a
__IMPOSSIBLE__ HypGraph NamedRigid Int -> HypGraph NamedRigid Int
forall a. a -> a
id (Either String (HypGraph NamedRigid Int)
 -> HypGraph NamedRigid Int)
-> Either String (HypGraph NamedRigid Int)
-> HypGraph NamedRigid Int
forall a b. (a -> b) -> a -> b
$ Set NamedRigid
-> [Constraint' NamedRigid Int]
-> Either String (HypGraph NamedRigid Int)
forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
Set rigid
-> [Hyp' rigid flex] -> Either String (HypGraph rigid flex)
hypGraph ([Constraint' NamedRigid Int]
-> Set (RigidOf [Constraint' NamedRigid Int])
forall a. Rigids a => a -> Set (RigidOf a)
rigids [Constraint' NamedRigid Int]
csF) [Constraint' NamedRigid Int]
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.
  Solution NamedRigid Int
sol :: Solution NamedRigid Int <- (String -> TCMT IO (Solution NamedRigid Int))
-> (Solution NamedRigid Int -> TCMT IO (Solution NamedRigid Int))
-> Either String (Solution NamedRigid Int)
-> TCMT IO (Solution NamedRigid Int)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> TCMT IO (Solution NamedRigid Int)
err Solution NamedRigid Int -> TCMT IO (Solution NamedRigid Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (Solution NamedRigid Int)
 -> TCMT IO (Solution NamedRigid Int))
-> Either String (Solution NamedRigid Int)
-> TCMT IO (Solution NamedRigid Int)
forall a b. (a -> b) -> a -> b
$
    Polarities Int
-> HypGraph NamedRigid Int
-> [Constraint' NamedRigid Int]
-> Solution NamedRigid Int
-> Either String (Solution NamedRigid Int)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either String (Solution r f)
iterateSolver Polarities Int
forall k a. Map k a
Map.empty HypGraph NamedRigid Int
hg [Constraint' NamedRigid Int]
csF Solution NamedRigid Int
forall r f. Solution r f
emptySolution

  -- Convert solution to meta instantiation.
  Set MetaId
solved <- ([Set MetaId] -> Set MetaId)
-> TCMT IO [Set MetaId] -> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Set MetaId] -> Set MetaId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (TCMT IO [Set MetaId] -> TCMT IO (Set MetaId))
-> TCMT IO [Set MetaId] -> TCMT IO (Set MetaId)
forall a b. (a -> b) -> a -> b
$ [(Int, SizeExpr' NamedRigid Int)]
-> ((Int, SizeExpr' NamedRigid Int) -> TCMT IO (Set MetaId))
-> TCMT IO [Set MetaId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Map Int (SizeExpr' NamedRigid Int)
-> [(Int, SizeExpr' NamedRigid Int)]
forall k a. Map k a -> [(k, a)]
Map.assocs (Map Int (SizeExpr' NamedRigid Int)
 -> [(Int, SizeExpr' NamedRigid Int)])
-> Map Int (SizeExpr' NamedRigid Int)
-> [(Int, SizeExpr' NamedRigid Int)]
forall a b. (a -> b) -> a -> b
$ Solution NamedRigid Int -> Map Int (SizeExpr' NamedRigid Int)
forall rigid flex.
Solution rigid flex -> Map flex (SizeExpr' rigid flex)
theSolution Solution NamedRigid Int
sol) (((Int, SizeExpr' NamedRigid Int) -> TCMT IO (Set MetaId))
 -> TCMT IO [Set MetaId])
-> ((Int, SizeExpr' NamedRigid Int) -> TCMT IO (Set MetaId))
-> TCMT IO [Set MetaId]
forall a b. (a -> b) -> a -> b
$ \ (Int
m, SizeExpr' NamedRigid Int
a) -> do
    Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SizeExpr' NamedRigid Int -> Bool
forall a. ValidOffset a => a -> Bool
validOffset SizeExpr' NamedRigid Int
a) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- Solution does not contain metas
    Term
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
$ (Int -> SizeMeta) -> SizeExpr' NamedRigid Int -> DBSizeExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> SizeMeta
forall a. HasCallStack => a
__IMPOSSIBLE__ SizeExpr' NamedRigid Int
a
    let x :: MetaId
x = Int -> MetaId
MetaId Int
m
    let SizeMeta MetaId
_ [Int]
xs = SizeMeta -> Maybe SizeMeta -> SizeMeta
forall a. a -> Maybe a -> a
fromMaybe SizeMeta
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe SizeMeta -> SizeMeta) -> Maybe SizeMeta -> SizeMeta
forall a b. (a -> b) -> a -> b
$
          (SizeMeta -> Bool) -> [SizeMeta] -> Maybe SizeMeta
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Int
mInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool) -> (SizeMeta -> Int) -> SizeMeta -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> Int
metaId (MetaId -> Int) -> (SizeMeta -> MetaId) -> SizeMeta -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeMeta -> MetaId
sizeMetaId) [SizeMeta]
metas
    -- Check that solution is well-scoped
    let ys :: [Int]
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 Int
-> Set (RigidOf (SizeExpr' NamedRigid Int))
forall a. Rigids a => a -> Set (RigidOf a)
rigids SizeExpr' NamedRigid Int
a)
        ok :: Bool
ok = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> [Int] -> 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"
    Term
u <- if Bool
ok then Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u else TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
    Type
t <- MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
x
    String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Context -> Context) -> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext (Context -> Context -> Context
forall a b. a -> b -> a
const Context
gamma) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
      let args :: Elims
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
      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
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x Elims
args) 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
prettyTCM Term
u
    String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.size.solve" Int
60 (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
      [ String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"  xs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show [Int]
xs
      , String -> TCMT IO Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCMT IO Doc) -> String -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ String
"  u  = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
u
      ]
    TCMT IO Bool
-> TCMT IO (Set MetaId)
-> TCMT IO (Set MetaId)
-> TCMT IO (Set MetaId)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas)) (Set MetaId -> TCMT IO (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return Set MetaId
forall a. Set a
Set.empty) (TCMT IO (Set MetaId) -> TCMT IO (Set MetaId))
-> TCMT IO (Set MetaId) -> TCMT IO (Set MetaId)
forall a b. (a -> b) -> a -> b
$ do
      Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta Int
n MetaId
x Type
t [Int]
xs Term
u
      Set MetaId -> TCMT IO (Set MetaId)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set MetaId -> TCMT IO (Set MetaId))
-> Set MetaId -> TCMT IO (Set MetaId)
forall a b. (a -> b) -> a -> b
$ MetaId -> Set MetaId
forall a. a -> Set a
Set.singleton MetaId
x
    -- WRONG:
    -- let partialSubst = List.sort $ zip xs $ map var $ downFrom n
    -- assignMeta' n x t (length xs) partialSubst u
    -- WRONG: assign DirEq x (map (defaultArg . var) xs) u

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

  Set MetaId
ims <- [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList ([MetaId] -> Set MetaId)
-> TCMT IO [MetaId] -> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas

  --  ms = unsolved size metas from cluster
  let ms :: Set MetaId
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 :: Bool
noIP = Set MetaId -> Set MetaId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set MetaId
ims Set MetaId
ms

  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set MetaId -> Bool
forall a. Null a => a -> Bool
null Set MetaId
ms) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
fsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"cluster did not solve these size metas: " TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (MetaId -> TCMT IO Doc) -> [MetaId] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList Set MetaId
ms)

  Bool
solvedAll <- do
    -- If no metas are left, we have solved this cluster completely.
    if Set MetaId -> Bool
forall a. Set a -> Bool
Set.null Set MetaId
ms                then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True  else do
    -- Otherwise, we can solve it completely if we are allowed to set to ∞.
    if DefaultToInfty
flag DefaultToInfty -> DefaultToInfty -> Bool
forall a. Eq a => a -> a -> Bool
== DefaultToInfty
DontDefaultToInfty then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
    -- Which is only the case when we have no interaction points in the cluster.
    if Bool -> Bool
not Bool
noIP                   then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
    -- Try to set all unconstrained size metas to ∞.
    Term
inf <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> TCMT IO [Bool] -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      [MetaId] -> (MetaId -> TCMT IO Bool) -> TCMT IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList Set MetaId
ms) ((MetaId -> TCMT IO Bool) -> TCMT IO [Bool])
-> (MetaId -> TCMT IO Bool) -> TCMT IO [Bool]
forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> do
        -- If one variable is frozen, we cannot set it (and hence not all) to ∞
        let no :: TCMT IO Bool
no = do
              String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
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 (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 :: * -> *).
(MonadFail 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
<$> (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas) 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
          String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
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
prettyTCM Term
inf
          Type
t <- MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
metaType MetaId
m
          TelV Tele (Dom Type)
tel Type
core <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
          TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool)
-> TCMT IO (Maybe BoundedSize) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
core) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
          Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta Int
0 MetaId
m Type
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) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel) Term
inf
          Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

  -- Double check.
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
solvedAll (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let cs0 :: NonEmpty ProblemConstraint
cs0 = ((ProblemConstraint, HypSizeConstraint) -> ProblemConstraint)
-> List1 (ProblemConstraint, HypSizeConstraint)
-> NonEmpty ProblemConstraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProblemConstraint, HypSizeConstraint) -> ProblemConstraint
forall a b. (a, b) -> a
fst List1 (ProblemConstraint, HypSizeConstraint)
ccs
        -- Error for giving up
        cannotSolve :: TCM ()
cannotSolve = TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (TCMT IO Doc
"Cannot solve size constraints" TCMT IO Doc -> 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProblemConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM NonEmpty ProblemConstraint
cs0)
    (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
$
        NonEmpty ProblemConstraint
-> (ProblemConstraint -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ NonEmpty 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

-- | Collect constraints from a typing context, looking for SIZELT hypotheses.
getSizeHypotheses :: Context -> TCM [(Nat, SizeConstraint)]
getSizeHypotheses :: Context -> TCM [(Int, SizeConstraint)]
getSizeHypotheses Context
gamma = (Context -> Context)
-> TCM [(Int, SizeConstraint)] -> TCM [(Int, SizeConstraint)]
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext (Context -> Context -> Context
forall a b. a -> b -> a
const Context
gamma) (TCM [(Int, SizeConstraint)] -> TCM [(Int, SizeConstraint)])
-> TCM [(Int, SizeConstraint)] -> TCM [(Int, SizeConstraint)]
forall a b. (a -> b) -> a -> b
$ do
  (Maybe QName
_, Maybe QName
msizelt) <- TCMT IO (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  Maybe QName
-> TCM [(Int, SizeConstraint)]
-> (QName -> TCM [(Int, SizeConstraint)])
-> TCM [(Int, SizeConstraint)]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe QName
msizelt ([(Int, SizeConstraint)] -> TCM [(Int, SizeConstraint)]
forall (m :: * -> *) a. Monad m => a -> m a
return []) ((QName -> TCM [(Int, SizeConstraint)])
 -> TCM [(Int, SizeConstraint)])
-> (QName -> TCM [(Int, SizeConstraint)])
-> TCM [(Int, SizeConstraint)]
forall a b. (a -> b) -> a -> b
$ \ QName
sizelt -> do
    -- Traverse the context from newest to oldest de Bruijn Index
    [Maybe (Int, SizeConstraint)] -> [(Int, SizeConstraint)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Int, SizeConstraint)] -> [(Int, SizeConstraint)])
-> TCMT IO [Maybe (Int, SizeConstraint)]
-> TCM [(Int, SizeConstraint)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      [(Int, Dom' Term (Name, Type))]
-> ((Int, Dom' Term (Name, Type))
    -> TCMT IO (Maybe (Int, SizeConstraint)))
-> TCMT IO [Maybe (Int, SizeConstraint)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Int] -> Context -> [(Int, Dom' Term (Name, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] Context
gamma) (((Int, Dom' Term (Name, Type))
  -> TCMT IO (Maybe (Int, SizeConstraint)))
 -> TCMT IO [Maybe (Int, SizeConstraint)])
-> ((Int, Dom' Term (Name, Type))
    -> TCMT IO (Maybe (Int, SizeConstraint)))
-> TCMT IO [Maybe (Int, SizeConstraint)]
forall a b. (a -> b) -> a -> b
$ \ (Int
i, Dom' Term (Name, Type)
ce) -> do
        -- Get name and type of variable i.
        let (Name
x, Type
t) = Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom Dom' Term (Name, Type)
ce
            s :: String
s      = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
        Term
t <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term) -> (Type -> Term) -> Type -> 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) -> (Type -> Term) -> Type -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> TCMT IO Term) -> Type -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type
t
        case Term
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, SizeConstraint))
-> (DBSizeExpr -> TCMT IO (Maybe (Int, SizeConstraint)))
-> TCMT IO (Maybe (Int, SizeConstraint))
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, SizeConstraint)
-> TCMT IO (Maybe (Int, SizeConstraint))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Int, SizeConstraint)
forall a. Maybe a
Nothing) ((DBSizeExpr -> TCMT IO (Maybe (Int, SizeConstraint)))
 -> TCMT IO (Maybe (Int, SizeConstraint)))
-> (DBSizeExpr -> TCMT IO (Maybe (Int, SizeConstraint)))
-> TCMT IO (Maybe (Int, SizeConstraint))
forall a b. (a -> b) -> a -> b
$ \ DBSizeExpr
a ->
              Maybe (Int, SizeConstraint)
-> TCMT IO (Maybe (Int, SizeConstraint))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Int, SizeConstraint)
 -> TCMT IO (Maybe (Int, SizeConstraint)))
-> Maybe (Int, SizeConstraint)
-> TCMT IO (Maybe (Int, SizeConstraint))
forall a b. (a -> b) -> a -> b
$ (Int, SizeConstraint) -> Maybe (Int, SizeConstraint)
forall a. a -> Maybe a
Just ((Int, SizeConstraint) -> Maybe (Int, SizeConstraint))
-> (Int, SizeConstraint) -> Maybe (Int, SizeConstraint)
forall a b. (a -> b) -> a -> b
$ (Int
i, DBSizeExpr -> Cmp -> DBSizeExpr -> SizeConstraint
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 (String -> Int -> NamedRigid
NamedRigid String
s Int
i) Offset
0) Cmp
Lt DBSizeExpr
a)
          Term
_ -> Maybe (Int, SizeConstraint)
-> TCMT IO (Maybe (Int, SizeConstraint))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Int, SizeConstraint)
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 :: SizeConstraint -> Maybe SizeConstraint
canonicalizeSizeConstraint c :: SizeConstraint
c@(Constraint DBSizeExpr
a Cmp
cmp DBSizeExpr
b) = SizeConstraint -> Maybe SizeConstraint
forall a. a -> Maybe a
Just SizeConstraint
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
-}

-- | Identifiers for rigid variables.
data NamedRigid = NamedRigid
  { NamedRigid -> String
rigidName  :: String   -- ^ Name for printing in debug messages.
  , NamedRigid -> Int
rigidIndex :: Int      -- ^ De Bruijn index.
  } deriving (Int -> NamedRigid -> ShowS
[NamedRigid] -> ShowS
NamedRigid -> String
(Int -> NamedRigid -> ShowS)
-> (NamedRigid -> String)
-> ([NamedRigid] -> ShowS)
-> Show NamedRigid
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NamedRigid] -> ShowS
$cshowList :: [NamedRigid] -> ShowS
show :: NamedRigid -> String
$cshow :: NamedRigid -> String
showsPrec :: Int -> NamedRigid -> ShowS
$cshowsPrec :: Int -> NamedRigid -> ShowS
Show)

instance Eq NamedRigid where == :: NamedRigid -> NamedRigid -> Bool
(==) = Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Int -> Int -> Bool)
-> (NamedRigid -> Int) -> NamedRigid -> NamedRigid -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` NamedRigid -> Int
rigidIndex
instance Ord NamedRigid where compare :: NamedRigid -> NamedRigid -> Ordering
compare = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (NamedRigid -> Int) -> NamedRigid -> NamedRigid -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` NamedRigid -> Int
rigidIndex
instance Pretty NamedRigid where pretty :: NamedRigid -> Doc
pretty = String -> Doc
P.text (String -> Doc) -> (NamedRigid -> String) -> NamedRigid -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedRigid -> String
rigidName
instance Plus NamedRigid Int NamedRigid where
  plus :: NamedRigid -> Int -> NamedRigid
plus (NamedRigid String
x Int
i) Int
j = String -> Int -> NamedRigid
NamedRigid String
x (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j)

-- | Size metas in size expressions.
data SizeMeta = SizeMeta
  { SizeMeta -> MetaId
sizeMetaId   :: MetaId
  -- TODO to fix issue 300?
  -- , sizeMetaPerm :: Permutation -- ^ Permutation from the current context
  --                               --   to the context of the meta.
  , SizeMeta -> [Int]
sizeMetaArgs :: [Int]       -- ^ De Bruijn indices.
  } deriving (Int -> SizeMeta -> ShowS
[SizeMeta] -> ShowS
SizeMeta -> String
(Int -> SizeMeta -> ShowS)
-> (SizeMeta -> String) -> ([SizeMeta] -> ShowS) -> Show SizeMeta
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SizeMeta] -> ShowS
$cshowList :: [SizeMeta] -> ShowS
show :: SizeMeta -> String
$cshow :: SizeMeta -> String
showsPrec :: Int -> SizeMeta -> ShowS
$cshowsPrec :: Int -> SizeMeta -> ShowS
Show)

-- | An equality which ignores the meta arguments.
instance Eq  SizeMeta where == :: SizeMeta -> SizeMeta -> Bool
(==)    = MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
(==)    (MetaId -> MetaId -> Bool)
-> (SizeMeta -> MetaId) -> SizeMeta -> SizeMeta -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SizeMeta -> MetaId
sizeMetaId
-- | An order which ignores the meta arguments.
instance Ord SizeMeta where compare :: SizeMeta -> SizeMeta -> Ordering
compare = MetaId -> MetaId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (MetaId -> MetaId -> Ordering)
-> (SizeMeta -> MetaId) -> SizeMeta -> SizeMeta -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SizeMeta -> MetaId
sizeMetaId

instance Pretty SizeMeta where pretty :: SizeMeta -> Doc
pretty = MetaId -> Doc
forall a. Pretty a => a -> Doc
P.pretty (MetaId -> Doc) -> (SizeMeta -> MetaId) -> SizeMeta -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizeMeta -> MetaId
sizeMetaId

instance PrettyTCM SizeMeta where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SizeMeta -> m Doc
prettyTCM (SizeMeta MetaId
x [Int]
es) = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (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]
es)

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__

-- | Size expression with de Bruijn indices.
type DBSizeExpr = SizeExpr' NamedRigid SizeMeta

-- deriving instance Functor     (SizeExpr' Int)
-- deriving instance Foldable    (SizeExpr' Int)
-- deriving instance Traversable (SizeExpr' Int)

-- | 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 DBSizeExpr)
Substitution' (SubstArg SizeMeta)
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 :: Int
rigidIndex = Int
j } Offset
n
          Term
_        -> DBSizeExpr
forall a. HasCallStack => a
__IMPOSSIBLE__

type SizeConstraint = Constraint' NamedRigid SizeMeta

instance Subst SizeConstraint where
  type SubstArg SizeConstraint = Term
  applySubst :: Substitution' (SubstArg SizeConstraint)
-> SizeConstraint -> SizeConstraint
applySubst Substitution' (SubstArg SizeConstraint)
sigma (Constraint DBSizeExpr
a Cmp
cmp DBSizeExpr
b) =
    DBSizeExpr -> Cmp -> DBSizeExpr -> SizeConstraint
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 SizeConstraint)
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 SizeConstraint)
Substitution' (SubstArg DBSizeExpr)
sigma DBSizeExpr
b)

-- | Assumes we are in the right context.
instance PrettyTCM (SizeConstraint) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => SizeConstraint -> m Doc
prettyTCM (Constraint DBSizeExpr
a Cmp
cmp DBSizeExpr
b) = do
    Term
u <- DBSizeExpr -> m Term
forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr DBSizeExpr
a
    Term
v <- DBSizeExpr -> m Term
forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr DBSizeExpr
b
    Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Cmp -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Cmp
cmp m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v

-- | Size constraint with de Bruijn indices.
data HypSizeConstraint = HypSizeConstraint
  { HypSizeConstraint -> Context
sizeContext    :: Context
  , HypSizeConstraint -> [Int]
sizeHypIds     :: [Nat] -- ^ DeBruijn indices
  , HypSizeConstraint -> [SizeConstraint]
sizeHypotheses :: [SizeConstraint]  -- ^ Living in @Context@.
  , HypSizeConstraint -> SizeConstraint
sizeConstraint :: SizeConstraint    -- ^ Living in @Context@.
  }

instance Flexs HypSizeConstraint where
  type FlexOf HypSizeConstraint = SizeMeta
  flexs :: HypSizeConstraint -> Set (FlexOf HypSizeConstraint)
flexs (HypSizeConstraint Context
_ [Int]
_ [SizeConstraint]
hs SizeConstraint
c) = [SizeConstraint] -> Set (FlexOf [SizeConstraint])
forall a. Flexs a => a -> Set (FlexOf a)
flexs [SizeConstraint]
hs Set SizeMeta -> Set SizeMeta -> Set SizeMeta
forall a. Monoid a => a -> a -> a
`mappend` SizeConstraint -> Set (FlexOf SizeConstraint)
forall a. Flexs a => a -> Set (FlexOf a)
flexs SizeConstraint
c

instance PrettyTCM HypSizeConstraint where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => HypSizeConstraint -> m Doc
prettyTCM (HypSizeConstraint Context
cxt [Int]
_ [SizeConstraint]
hs SizeConstraint
c) =
    (Context -> Context) -> m Doc -> m Doc
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext (Context -> Context -> Context
forall a b. a -> b -> a
const Context
cxt) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ do
      let cxtNames :: [Name]
cxtNames = [Name] -> [Name]
forall a. [a] -> [a]
reverse ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ (Dom' Term (Name, Type) -> Name) -> Context -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) Context
cxt
      -- text ("[#cxt=" ++ show (size cxt) ++ "]") <+> do
      [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Name]
cxtNames) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do
      Bool -> (m Doc -> m Doc) -> m Doc -> m Doc
forall a. Bool -> (a -> a) -> a -> a
applyUnless ([SizeConstraint] -> Bool
forall a. Null a => a -> Bool
null [SizeConstraint]
hs)
       (([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat (m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
", " ([m Doc] -> [m Doc]) -> [m Doc] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ (SizeConstraint -> m Doc) -> [SizeConstraint] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map SizeConstraint -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [SizeConstraint]
hs) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"|-") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>)
       (SizeConstraint -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM SizeConstraint
c)

-- | 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
cxt = TCEnv -> Context
envContext (TCEnv -> Context) -> TCEnv -> Context
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 -> Context)
-> TCMT IO (Maybe HypSizeConstraint)
-> TCMT IO (Maybe HypSizeConstraint)
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext (Context -> Context -> Context
forall a b. a -> b -> a
const Context
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
        String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"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
prettyTCM ProblemConstraint
c
          ]
        Maybe DBSizeExpr
ma <- Term -> TCMT IO (Maybe DBSizeExpr)
sizeExpr Term
u
        Maybe DBSizeExpr
mb <- Term -> TCMT IO (Maybe DBSizeExpr)
sizeExpr Term
v
        ([Int]
hids, [SizeConstraint]
hs) <- [(Int, SizeConstraint)] -> ([Int], [SizeConstraint])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Int, SizeConstraint)] -> ([Int], [SizeConstraint]))
-> TCM [(Int, SizeConstraint)] -> TCMT IO ([Int], [SizeConstraint])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> TCM [(Int, SizeConstraint)]
getSizeHypotheses Context
cxt
        let mk :: DBSizeExpr -> DBSizeExpr -> HypSizeConstraint
mk DBSizeExpr
a DBSizeExpr
b = Context
-> [Int] -> [SizeConstraint] -> SizeConstraint -> HypSizeConstraint
HypSizeConstraint Context
cxt [Int]
hids [SizeConstraint]
hs (SizeConstraint -> HypSizeConstraint)
-> SizeConstraint -> HypSizeConstraint
forall a b. (a -> b) -> a -> b
$ DBSizeExpr -> Cmp -> DBSizeExpr -> SizeConstraint
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.
        Maybe HypSizeConstraint -> TCMT IO (Maybe HypSizeConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe HypSizeConstraint -> TCMT IO (Maybe HypSizeConstraint))
-> Maybe HypSizeConstraint -> TCMT IO (Maybe HypSizeConstraint)
forall a b. (a -> b) -> a -> b
$ DBSizeExpr -> DBSizeExpr -> HypSizeConstraint
mk (DBSizeExpr -> DBSizeExpr -> HypSizeConstraint)
-> Maybe DBSizeExpr -> Maybe (DBSizeExpr -> HypSizeConstraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DBSizeExpr
ma Maybe (DBSizeExpr -> HypSizeConstraint)
-> Maybe DBSizeExpr -> Maybe HypSizeConstraint
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DBSizeExpr
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
  Term
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.
  String -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.conv.size" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"sizeExpr:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
  SizeView
s <- Term -> TCMT IO SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
  case SizeView
s of
    SizeView
SizeInf     -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
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 (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 []    -> (\ String
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 (String -> Int -> NamedRigid
NamedRigid String
x Int
i) Offset
0) (String -> Maybe DBSizeExpr)
-> (Name -> String) -> Name -> Maybe DBSizeExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Pretty a => a -> String
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 :: * -> *).
(Applicative m, MonadFail 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)
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 (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 (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

-- | Turn a de size expression into a term.
unSizeExpr :: HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr :: forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr DBSizeExpr
a =
  case DBSizeExpr
a of
    DBSizeExpr
Infty         -> Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSizeInf
    Rigid NamedRigid
r (O Int
n) -> do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
n (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ NamedRigid -> Int
rigidIndex NamedRigid
r
    Flex (SizeMeta MetaId
x [Int]
es) (O Int
n) -> do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
n (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (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]
es
    Const{} -> m Term
forall a. HasCallStack => a
__IMPOSSIBLE__