{-# LANGUAGE NondecreasingIndentation #-}
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 (on)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Monoid
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (forM)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Internal.MetaVars
import Agda.TypeChecking.Monad as TCM hiding (Offset)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Free
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints as C
import qualified Agda.TypeChecking.SizedTypes as S
import Agda.TypeChecking.SizedTypes.Pretty
import Agda.TypeChecking.SizedTypes.Syntax as Size
import Agda.TypeChecking.SizedTypes.Utils
import Agda.TypeChecking.SizedTypes.WarshallSolver as Size hiding (simplify1)
import Agda.Utils.Cluster
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List1 (List1, pattern (:|), nonEmpty, (<|))
import qualified Agda.Utils.List as List
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty (Pretty, prettyShow)
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.Impossible
data DefaultToInfty
= DefaultToInfty
| DontDefaultToInfty
deriving (DefaultToInfty -> DefaultToInfty -> Bool
(DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> Bool) -> Eq DefaultToInfty
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DefaultToInfty -> DefaultToInfty -> Bool
== :: DefaultToInfty -> DefaultToInfty -> Bool
$c/= :: DefaultToInfty -> DefaultToInfty -> Bool
/= :: DefaultToInfty -> DefaultToInfty -> Bool
Eq, Eq DefaultToInfty
Eq DefaultToInfty =>
(DefaultToInfty -> DefaultToInfty -> Ordering)
-> (DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> Bool)
-> (DefaultToInfty -> DefaultToInfty -> DefaultToInfty)
-> (DefaultToInfty -> DefaultToInfty -> DefaultToInfty)
-> Ord DefaultToInfty
DefaultToInfty -> DefaultToInfty -> Bool
DefaultToInfty -> DefaultToInfty -> Ordering
DefaultToInfty -> DefaultToInfty -> DefaultToInfty
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DefaultToInfty -> DefaultToInfty -> Ordering
compare :: DefaultToInfty -> DefaultToInfty -> Ordering
$c< :: DefaultToInfty -> DefaultToInfty -> Bool
< :: DefaultToInfty -> DefaultToInfty -> Bool
$c<= :: DefaultToInfty -> DefaultToInfty -> Bool
<= :: DefaultToInfty -> DefaultToInfty -> Bool
$c> :: DefaultToInfty -> DefaultToInfty -> Bool
> :: DefaultToInfty -> DefaultToInfty -> Bool
$c>= :: DefaultToInfty -> DefaultToInfty -> Bool
>= :: DefaultToInfty -> DefaultToInfty -> Bool
$cmax :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
max :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
$cmin :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
min :: DefaultToInfty -> DefaultToInfty -> DefaultToInfty
Ord, Int -> DefaultToInfty -> ShowS
[DefaultToInfty] -> ShowS
DefaultToInfty -> [Char]
(Int -> DefaultToInfty -> ShowS)
-> (DefaultToInfty -> [Char])
-> ([DefaultToInfty] -> ShowS)
-> Show DefaultToInfty
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DefaultToInfty -> ShowS
showsPrec :: Int -> DefaultToInfty -> ShowS
$cshow :: DefaultToInfty -> [Char]
show :: DefaultToInfty -> [Char]
$cshowList :: [DefaultToInfty] -> ShowS
showList :: [DefaultToInfty] -> ShowS
Show)
solveSizeConstraints :: DefaultToInfty -> TCM ()
solveSizeConstraints :: DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
flag = do
cs0 :: [ProblemConstraint]
<- TCMT IO [ProblemConstraint]
-> (ProblemConstraint -> TCMT IO ProblemConstraint)
-> TCMT IO [ProblemConstraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
m (t a) -> (a -> m b) -> m (t b)
forMM ((Comparison -> Bool) -> TCMT IO [ProblemConstraint]
S.takeSizeConstraints (Comparison -> Comparison -> Bool
forall a. Eq a => a -> a -> Bool
== Comparison
CmpLeq)) ((ProblemConstraint -> TCMT IO ProblemConstraint)
-> TCMT IO [ProblemConstraint])
-> (ProblemConstraint -> TCMT IO ProblemConstraint)
-> TCMT IO [ProblemConstraint]
forall a b. (a -> b) -> a -> b
$ \ (ProblemConstraint
c :: ProblemConstraint) -> do
(Constraint -> TCMT IO Constraint)
-> Closure Constraint -> TCMT IO (Closure Constraint)
forall (m :: * -> *) a b.
(MonadTCEnv m, ReadTCState m) =>
(a -> m b) -> Closure a -> m (Closure b)
mapClosure Constraint -> TCMT IO Constraint
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) TCMT IO (Closure Constraint)
-> (Closure Constraint -> ProblemConstraint)
-> TCMT IO ProblemConstraint
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Closure Constraint
cl -> ProblemConstraint
c { theConstraint = cl }
unless (null cs0) $
reportSDoc "tc.size.solve" 40 $ vcat $
text ( "Solving constraints (" ++ show flag ++ ")" ) : map prettyTCM cs0
sizeMetaSet <- Set.fromList . map (\ (MetaId
x, Type
_t, Tele (Dom Type)
_tel) -> MetaId
x) <$> S.getSizeMetas True
cms <- forM cs0 $ \ ProblemConstraint
cl -> Closure Constraint
-> (Constraint -> TCMT IO (ProblemConstraint, [MetaId]))
-> TCMT IO (ProblemConstraint, [MetaId])
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
cl) ((Constraint -> TCMT IO (ProblemConstraint, [MetaId]))
-> TCMT IO (ProblemConstraint, [MetaId]))
-> (Constraint -> TCMT IO (ProblemConstraint, [MetaId]))
-> TCMT IO (ProblemConstraint, [MetaId])
forall a b. (a -> b) -> a -> b
$ \ Constraint
c -> do
(ProblemConstraint, [MetaId])
-> TCMT IO (ProblemConstraint, [MetaId])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProblemConstraint
cl, Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList (Set MetaId -> [MetaId]) -> Set MetaId -> [MetaId]
forall a b. (a -> b) -> a -> b
$
Set MetaId
sizeMetaSet Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` (MetaId -> Set MetaId) -> Constraint -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> Constraint -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas MetaId -> Set MetaId
forall el coll. Singleton el coll => el -> coll
singleton Constraint
c)
let classify :: (a, [b]) -> Either a (a, List1 b)
classify (a
cl, []) = a -> Either a (a, List1 b)
forall a b. a -> Either a b
Left a
cl
classify (a
cl, (b
x:[b]
xs)) = (a, List1 b) -> Either a (a, List1 b)
forall a b. b -> Either a b
Right (a
cl, b
x b -> [b] -> List1 b
forall a. a -> [a] -> NonEmpty a
:| [b]
xs)
let (clcs, othercs) = partitionEithers $ map classify cms
let ccs = [(ProblemConstraint, List1 MetaId)] -> [NonEmpty ProblemConstraint]
forall c a. Ord c => [(a, NonEmpty c)] -> [NonEmpty a]
cluster' [(ProblemConstraint, List1 MetaId)]
othercs
forM_ clcs $ \ ProblemConstraint
c -> () () -> TCMT IO (Set MetaId) -> TCM ()
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ DefaultToInfty -> [ProblemConstraint] -> TCMT IO (Set MetaId)
solveSizeConstraints_ DefaultToInfty
flag [ProblemConstraint
c]
constrainedMetas <- Set.unions <$> do
forM (ccs) $ \ (NonEmpty ProblemConstraint
cs :: List1 ProblemConstraint) -> do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"size constraint cluster:" TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> NonEmpty (TCMT IO Doc)
forall a. a -> NonEmpty a -> NonEmpty a
<| (ProblemConstraint -> TCMT IO Doc)
-> NonEmpty ProblemConstraint -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (ProblemConstraint -> [Char])
-> ProblemConstraint
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> [Char]
forall a. Show a => a -> [Char]
show) NonEmpty ProblemConstraint
cs
Closure Constraint
-> (Constraint -> TCMT IO (Set MetaId)) -> TCMT IO (Set MetaId)
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure ((Closure Constraint -> Closure Constraint -> Ordering)
-> NonEmpty (Closure Constraint) -> Closure Constraint
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
Fold.maximumBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (Closure Constraint -> Int)
-> Closure Constraint
-> Closure Constraint
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Context -> Int
forall a. [a] -> 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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProblemConstraint -> Closure Constraint
theConstraint NonEmpty ProblemConstraint
cs) ((Constraint -> TCMT IO (Set MetaId)) -> TCMT IO (Set MetaId))
-> (Constraint -> TCMT IO (Set MetaId)) -> TCMT IO (Set MetaId)
forall a b. (a -> b) -> a -> b
$ \ Constraint
_ -> do
cs' :: [ProblemConstraint] <- List1 (Maybe ProblemConstraint) -> [ProblemConstraint]
forall a. List1 (Maybe a) -> [a]
List1.catMaybes (List1 (Maybe ProblemConstraint) -> [ProblemConstraint])
-> TCMT IO (List1 (Maybe ProblemConstraint))
-> TCMT IO [ProblemConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
(ProblemConstraint -> TCMT IO (Maybe ProblemConstraint))
-> NonEmpty ProblemConstraint
-> TCMT IO (List1 (Maybe ProblemConstraint))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM (MaybeT (TCMT IO) ProblemConstraint
-> TCMT IO (Maybe ProblemConstraint)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TCMT IO) ProblemConstraint
-> TCMT IO (Maybe ProblemConstraint))
-> (ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint)
-> ProblemConstraint
-> TCMT IO (Maybe ProblemConstraint)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
castConstraintToCurrentContext) NonEmpty ProblemConstraint
cs
reportSDoc "tc.size.solve" 20 $ vcat $
( "converted size constraints to context: " <+> do
tel <- getContextTelescope
inTopContext $ prettyTCM tel
) : map (nest 2 . prettyTCM) cs'
solveSizeConstraints_ flag cs'
when (flag == DefaultToInfty) $ do
ms <- S.getSizeMetas False
unless (null ms) $ do
inf <- primSizeInf
forM_ ms $ \ (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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"solution " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
TCMT IO Doc
" := " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
inf
Int -> MetaId -> Type -> [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
forM_ cs0 $ withConstraint solveConstraint
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
delta1 <- TCMT IO (Tele (Dom Type)) -> MaybeT (TCMT IO) (Tele (Dom Type))
forall a. TCM a -> MaybeT (TCMT IO) a
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' Section (Tele (Dom Type)) -> Tele (Dom Type)
forall o i. o -> Lens' o i -> i
^. (Tele (Dom Type) -> f (Tele (Dom Type))) -> Section -> f Section
Lens' Section (Tele (Dom Type))
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
let 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
unless (delta2 >= 0) __IMPOSSIBLE__
modM <- currentModule
gamma <- liftTCM $ getContextSize
gamma1 <-liftTCM $ maybe empty (^. secTelescope) <$> getSection modM
let 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
sigma <- liftTCM $ fromMaybe idS <$> getModuleParameterSub modN
reportSDoc "tc.constr.cast" 40 $ "casting constraint" $$ do
tel <- getContextTelescope
inTopContext $ nest 2 $ vcat $
[ "current module = " <+> prettyTCM modM
, "current module telescope = " <+> prettyTCM gamma1
, "current context = " <+> prettyTCM tel
, "constraint module = " <+> prettyTCM modN
, "constraint module telescope = " <+> prettyTCM delta1
, "constraint context = " <+> (prettyTCM =<< enterClosure cl (const $ getContextTelescope))
, "constraint = " <+> enterClosure cl prettyTCM
, "module parameter substitution = " <+> prettyTCM sigma
]
guard (gamma2 >= 0)
if modN == modM then raiseMaybe (gamma - size delta) $ clValue cl else do
c <- raiseMaybe (-delta2) $ clValue cl
fv <- liftTCM $ getModuleFreeVars modN
guard $ fv == size delta1
return $ applySubst sigma c
where
raiseMaybe :: Int -> b -> m b
raiseMaybe Int
n b
c = do
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
||
IntSet -> Bool
IntSet.null ((IntSet, IntSet) -> IntSet
forall a b. (a, b) -> a
fst ((IntSet, IntSet) -> IntSet) -> (IntSet, IntSet) -> IntSet
forall a b. (a -> b) -> a -> b
$ Int -> IntSet -> (IntSet, IntSet)
IntSet.split (-Int
n) (IntSet -> (IntSet, IntSet)) -> IntSet -> (IntSet, IntSet)
forall a b. (a -> b) -> a -> b
$ b -> IntSet
forall t. Free t => t -> IntSet
allFreeVars b
c)
b -> m b
forall a. a -> m a
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
castConstraintToCurrentContext :: ProblemConstraint -> MaybeT TCM ProblemConstraint
castConstraintToCurrentContext :: ProblemConstraint -> MaybeT (TCMT IO) ProblemConstraint
castConstraintToCurrentContext ProblemConstraint
c = do
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
sigma <- MaybeT (TCMT IO) (Maybe (Substitution' Term))
-> MaybeT (TCMT IO) (Substitution' Term)
-> (Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term))
-> MaybeT (TCMT IO) (Substitution' Term)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Lens' TCEnv (Maybe (Substitution' Term))
-> MaybeT (TCMT IO) (Maybe (Substitution' Term))
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Lens' TCEnv (Maybe (Substitution' Term))
-> MaybeT (TCMT IO) (Maybe (Substitution' Term)))
-> Lens' TCEnv (Maybe (Substitution' Term))
-> MaybeT (TCMT IO) (Maybe (Substitution' Term))
forall a b. (a -> b) -> a -> b
$ (Map CheckpointId (Substitution' Term)
-> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv
Lens' TCEnv (Map CheckpointId (Substitution' Term))
eCheckpoints ((Map CheckpointId (Substitution' Term)
-> f (Map CheckpointId (Substitution' Term)))
-> TCEnv -> f TCEnv)
-> ((Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
-> Map CheckpointId (Substitution' Term)
-> f (Map CheckpointId (Substitution' Term)))
-> (Maybe (Substitution' Term) -> f (Maybe (Substitution' Term)))
-> TCEnv
-> f TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CheckpointId
-> Lens'
(Map CheckpointId (Substitution' Term))
(Maybe (Substitution' Term))
forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
key CheckpointId
cp)
(do
gamma <- (TCEnv -> Context) -> MaybeT (TCMT IO) Context
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Context
envContext
let findInGamma (Dom {unDom :: forall t e. Dom' t e -> e
unDom = (Name
x, Type
t)}) =
(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 = 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 = (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
let 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..]
guard $ getAll $ runFree (All . (`VarSet.member` coveredVars)) IgnoreAll (clValue cl)
return $ parallelS $ map (maybe __DUMMY_TERM__ var) cand
) Substitution' Term -> MaybeT (TCMT IO) (Substitution' Term)
forall a. a -> MaybeT (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return
cl' <- buildClosure $ applySubst sigma (clValue cl)
return $ c { theConstraint = cl' }
solveSizeConstraints_ :: DefaultToInfty -> [ProblemConstraint] -> TCM (Set MetaId)
solveSizeConstraints_ :: DefaultToInfty -> [ProblemConstraint] -> TCMT IO (Set MetaId)
solveSizeConstraints_ DefaultToInfty
flag [ProblemConstraint]
cs0 = do
ccs :: [(ProblemConstraint, HypSizeConstraint)] <- [Maybe (ProblemConstraint, HypSizeConstraint)]
-> [(ProblemConstraint, HypSizeConstraint)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (ProblemConstraint, HypSizeConstraint)]
-> [(ProblemConstraint, HypSizeConstraint)])
-> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)]
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
[ProblemConstraint]
-> (ProblemConstraint
-> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint)))
-> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ProblemConstraint]
cs0 ((ProblemConstraint
-> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint)))
-> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)])
-> (ProblemConstraint
-> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint)))
-> TCMT IO [Maybe (ProblemConstraint, HypSizeConstraint)]
forall a b. (a -> b) -> a -> b
$ \ ProblemConstraint
c0 -> (HypSizeConstraint -> (ProblemConstraint, HypSizeConstraint))
-> Maybe HypSizeConstraint
-> Maybe (ProblemConstraint, HypSizeConstraint)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProblemConstraint
c0,) (Maybe HypSizeConstraint
-> Maybe (ProblemConstraint, HypSizeConstraint))
-> TCMT IO (Maybe HypSizeConstraint)
-> TCMT IO (Maybe (ProblemConstraint, HypSizeConstraint))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProblemConstraint -> TCMT IO (Maybe HypSizeConstraint)
computeSizeConstraint ProblemConstraint
c0
ccs' :: [(ProblemConstraint, HypSizeConstraint)] <- concat <$> do
forM ccs $ \ cc :: (ProblemConstraint, HypSizeConstraint)
cc@(ProblemConstraint
c0 :: ProblemConstraint, 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] -> Maybe [SizeConstraint]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return [SizeConstraint
sc]) SizeConstraint
sc of
Maybe [SizeConstraint]
Nothing -> TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
-> TypeError -> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint, HypSizeConstraint) -> TypeError
ContradictorySizeConstraint (ProblemConstraint, HypSizeConstraint)
cc
Just [SizeConstraint]
cs -> [(ProblemConstraint, HypSizeConstraint)]
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(ProblemConstraint, HypSizeConstraint)]
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)])
-> [(ProblemConstraint, HypSizeConstraint)]
-> TCMT IO [(ProblemConstraint, HypSizeConstraint)]
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint
c0,) (HypSizeConstraint -> (ProblemConstraint, HypSizeConstraint))
-> (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
let (csNoM, csMs) = (`List.partitionMaybe` ccs') $ \ p :: (ProblemConstraint, HypSizeConstraint)
p@(ProblemConstraint
c0, HypSizeConstraint
c) ->
(List1 MetaId
-> ((ProblemConstraint, HypSizeConstraint), List1 MetaId))
-> Maybe (List1 MetaId)
-> Maybe ((ProblemConstraint, HypSizeConstraint), List1 MetaId)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ProblemConstraint, HypSizeConstraint)
p,) (Maybe (List1 MetaId)
-> Maybe ((ProblemConstraint, HypSizeConstraint), List1 MetaId))
-> Maybe (List1 MetaId)
-> Maybe ((ProblemConstraint, HypSizeConstraint), List1 MetaId)
forall a b. (a -> b) -> a -> b
$ [MetaId] -> Maybe (List1 MetaId)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([MetaId] -> Maybe (List1 MetaId))
-> [MetaId] -> Maybe (List1 MetaId)
forall a b. (a -> b) -> a -> b
$ (SizeMeta -> MetaId) -> [SizeMeta] -> [MetaId]
forall a b. (a -> b) -> [a] -> [b]
map SizeMeta -> MetaId
sizeMetaId ([SizeMeta] -> [MetaId]) -> [SizeMeta] -> [MetaId]
forall a b. (a -> b) -> a -> b
$ Set SizeMeta -> [SizeMeta]
forall a. Set a -> [a]
Set.toList (Set SizeMeta -> [SizeMeta]) -> Set SizeMeta -> [SizeMeta]
forall a b. (a -> b) -> a -> b
$ HypSizeConstraint -> Set (FlexOf HypSizeConstraint)
forall a. Flexs a => a -> Set (FlexOf a)
flexs HypSizeConstraint
c
css :: [List1 (ProblemConstraint, HypSizeConstraint)]
css = [((ProblemConstraint, HypSizeConstraint), List1 MetaId)]
-> [List1 (ProblemConstraint, HypSizeConstraint)]
forall c a. Ord c => [(a, NonEmpty c)] -> [NonEmpty a]
cluster' [((ProblemConstraint, HypSizeConstraint), List1 MetaId)]
csMs
whenJust (nonEmpty csNoM) $ solveCluster flag
forM_ css $ solveCluster flag
return $ Set.mapMonotonic sizeMetaId $ flexs $ map (snd . fst) csMs
solveCluster :: DefaultToInfty -> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
solveCluster :: DefaultToInfty
-> List1 (ProblemConstraint, HypSizeConstraint) -> TCM ()
solveCluster DefaultToInfty
flag List1 (ProblemConstraint, HypSizeConstraint)
ccs = do
let
err :: TCM Doc -> TCM a
err :: forall a. TCMT IO Doc -> TCM a
err TCMT IO Doc
mdoc = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 (ProblemConstraint, HypSizeConstraint) -> Doc -> TypeError
CannotSolveSizeConstraints List1 (ProblemConstraint, HypSizeConstraint)
ccs (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Doc
mdoc
cs :: List1 HypSizeConstraint
cs :: List1 HypSizeConstraint
cs = ((ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint)
-> List1 (ProblemConstraint, HypSizeConstraint)
-> List1 HypSizeConstraint
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ProblemConstraint, HypSizeConstraint) -> HypSizeConstraint
forall a b. (a, b) -> b
snd List1 (ProblemConstraint, HypSizeConstraint)
ccs
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (TCMT IO Doc) -> TCMT IO Doc)
-> NonEmpty (TCMT IO Doc) -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Solving constraint cluster" TCMT IO Doc -> NonEmpty (TCMT IO Doc) -> NonEmpty (TCMT IO Doc)
forall a. a -> NonEmpty a -> NonEmpty a
<| (HypSizeConstraint -> TCMT IO Doc)
-> List1 HypSizeConstraint -> NonEmpty (TCMT IO Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HypSizeConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => HypSizeConstraint -> m Doc
prettyTCM List1 HypSizeConstraint
cs
let HypSizeConstraint Context
gamma [Int]
hids [SizeConstraint]
hs SizeConstraint
_ = (HypSizeConstraint -> HypSizeConstraint -> Ordering)
-> List1 HypSizeConstraint -> HypSizeConstraint
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
Fold.maximumBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (HypSizeConstraint -> Int)
-> HypSizeConstraint
-> HypSizeConstraint
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Context -> Int
forall a. [a] -> 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)) List1 HypSizeConstraint
cs
let n :: Int
n = Context -> Int
forall a. Sized a => a -> Int
size Context
gamma
csL :: NonEmpty SizeConstraint
csL = List1 HypSizeConstraint
-> (HypSizeConstraint -> SizeConstraint) -> NonEmpty SizeConstraint
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
for List1 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
csC :: [SizeConstraint]
csC :: [SizeConstraint]
csC = Bool
-> ([SizeConstraint] -> [SizeConstraint])
-> [SizeConstraint]
-> [SizeConstraint]
forall b a. IsBool b => b -> (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 -> [Item (NonEmpty SizeConstraint)]
forall l. IsList l => l -> [Item l]
List1.toList NonEmpty SizeConstraint
csL
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"Size hypotheses" ] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
(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
forall (m :: * -> *). MonadPretty m => HypSizeConstraint -> 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
forall (m :: * -> *). MonadPretty m => HypSizeConstraint -> 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
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 m a. Monoid m => (a -> m) -> Constraint' NamedRigid a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (SizeMeta -> [SizeMeta] -> [SizeMeta]
forall a. a -> [a] -> [a]
:[])) [SizeConstraint]
csC
csF :: [Size.Constraint' NamedRigid MetaId]
csF :: [Constraint' NamedRigid MetaId]
csF = (SizeConstraint -> Constraint' NamedRigid MetaId)
-> [SizeConstraint] -> [Constraint' NamedRigid MetaId]
forall a b. (a -> b) -> [a] -> [b]
map ((SizeMeta -> MetaId)
-> SizeConstraint -> Constraint' NamedRigid MetaId
forall a b.
(a -> b) -> Constraint' NamedRigid a -> Constraint' NamedRigid b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SizeMeta -> MetaId
sizeMetaId) [SizeConstraint]
csC
let hyps :: [Constraint' NamedRigid MetaId]
hyps = (SizeConstraint -> Constraint' NamedRigid MetaId)
-> [SizeConstraint] -> [Constraint' NamedRigid MetaId]
forall a b. (a -> b) -> [a] -> [b]
map ((SizeMeta -> MetaId)
-> SizeConstraint -> Constraint' NamedRigid MetaId
forall a b.
(a -> b) -> Constraint' NamedRigid a -> Constraint' NamedRigid b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SizeMeta -> MetaId
sizeMetaId) [SizeConstraint]
hs
let hg :: HypGraph NamedRigid MetaId
hg = (TCMT IO Doc -> HypGraph NamedRigid MetaId)
-> (HypGraph NamedRigid MetaId -> HypGraph NamedRigid MetaId)
-> Either (TCMT IO Doc) (HypGraph NamedRigid MetaId)
-> HypGraph NamedRigid MetaId
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TCMT IO Doc -> HypGraph NamedRigid MetaId
forall a. HasCallStack => a
__IMPOSSIBLE__ HypGraph NamedRigid MetaId -> HypGraph NamedRigid MetaId
forall a. a -> a
id (Either (TCMT IO Doc) (HypGraph NamedRigid MetaId)
-> HypGraph NamedRigid MetaId)
-> Either (TCMT IO Doc) (HypGraph NamedRigid MetaId)
-> HypGraph NamedRigid MetaId
forall a b. (a -> b) -> a -> b
$ Set NamedRigid
-> [Constraint' NamedRigid MetaId]
-> Either (TCMT IO Doc) (HypGraph NamedRigid MetaId)
forall rigid flex.
(Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
Set rigid
-> [Hyp' rigid flex] -> Either (TCMT IO Doc) (HypGraph rigid flex)
hypGraph ([Constraint' NamedRigid MetaId]
-> Set (RigidOf [Constraint' NamedRigid MetaId])
forall a. Rigids a => a -> Set (RigidOf a)
rigids [Constraint' NamedRigid MetaId]
csF) [Constraint' NamedRigid MetaId]
hyps
sol :: Solution NamedRigid MetaId <- (TCMT IO Doc -> TCMT IO (Solution NamedRigid MetaId))
-> (Solution NamedRigid MetaId
-> TCMT IO (Solution NamedRigid MetaId))
-> Either (TCMT IO Doc) (Solution NamedRigid MetaId)
-> TCMT IO (Solution NamedRigid MetaId)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TCMT IO Doc -> TCMT IO (Solution NamedRigid MetaId)
forall a. TCMT IO Doc -> TCM a
err Solution NamedRigid MetaId -> TCMT IO (Solution NamedRigid MetaId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either (TCMT IO Doc) (Solution NamedRigid MetaId)
-> TCMT IO (Solution NamedRigid MetaId))
-> Either (TCMT IO Doc) (Solution NamedRigid MetaId)
-> TCMT IO (Solution NamedRigid MetaId)
forall a b. (a -> b) -> a -> b
$
Polarities MetaId
-> HypGraph NamedRigid MetaId
-> [Constraint' NamedRigid MetaId]
-> Solution NamedRigid MetaId
-> Either (TCMT IO Doc) (Solution NamedRigid MetaId)
forall r f.
(Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
Polarities f
-> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either (TCMT IO Doc) (Solution r f)
iterateSolver Polarities MetaId
forall k a. Map k a
Map.empty HypGraph NamedRigid MetaId
hg [Constraint' NamedRigid MetaId]
csF Solution NamedRigid MetaId
forall r f. Solution r f
emptySolution
solved <- fmap Set.unions $ forM (Map.assocs $ theSolution sol) $ \ (MetaId
m, SizeExpr' NamedRigid MetaId
a) -> do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SizeExpr' NamedRigid MetaId -> Bool
forall a. ValidOffset a => a -> Bool
validOffset SizeExpr' NamedRigid MetaId
a) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
u <- DBSizeExpr -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => DBSizeExpr -> m Term
unSizeExpr (DBSizeExpr -> TCMT IO Term) -> DBSizeExpr -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ (MetaId -> SizeMeta) -> SizeExpr' NamedRigid MetaId -> DBSizeExpr
forall a b.
(a -> b) -> SizeExpr' NamedRigid a -> SizeExpr' NamedRigid b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MetaId -> SizeMeta
forall a. HasCallStack => a
__IMPOSSIBLE__ SizeExpr' NamedRigid MetaId
a
let SizeMeta _ xs = fromMaybe __IMPOSSIBLE__ $
List.find ((m ==) . sizeMetaId) metas
let ys = NamedRigid -> Int
rigidIndex (NamedRigid -> Int) -> [NamedRigid] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set NamedRigid -> [NamedRigid]
forall a. Set a -> [a]
Set.toList (SizeExpr' NamedRigid MetaId
-> Set (RigidOf (SizeExpr' NamedRigid MetaId))
forall a. Rigids a => a -> Set (RigidOf a)
rigids SizeExpr' NamedRigid MetaId
a)
ok = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
xs) [Int]
ys
u <- if ok then return u else primSizeInf
t <- getMetaType m
reportSDoc "tc.size.solve" 20 $ unsafeModifyContext (const gamma) $ do
let args = (Int -> Elim' Term) -> [Int] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> (Int -> Arg Term) -> Int -> Elim' Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> (Int -> Term) -> Int -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
var) [Int]
xs
"solution " <+> prettyTCM (MetaV m args) <+> " := " <+> prettyTCM u
reportSDoc "tc.size.solve" 60 $ vcat
[ text $ " xs = " ++ show xs
, text $ " u = " ++ show u
]
ifM (isFrozen m `or2M` (not <$> asksTC envAssignMetas)) (return Set.empty) $ do
assignMeta n m t xs u
return $ Set.singleton m
ims <- Set.fromList <$> getInteractionMetas
let ms = [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList ((SizeMeta -> MetaId) -> [SizeMeta] -> [MetaId]
forall a b. (a -> b) -> [a] -> [b]
map SizeMeta -> MetaId
sizeMetaId [SizeMeta]
metas) Set MetaId -> Set MetaId -> Set MetaId
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set MetaId
solved
let noIP = Set MetaId -> Set MetaId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set MetaId
ims Set MetaId
ms
unless (null ms) $ reportSDoc "tc.size.solve" 30 $ fsep $
"cluster did not solve these size metas: " : map prettyTCM (Set.toList ms)
solvedAll <- do
if Set.null ms then return True else do
if flag == DontDefaultToInfty then return False else do
if not noIP then return False else do
inf <- primSizeInf
and <$> do
forM (Set.toList ms) $ \ MetaId
m -> do
let no :: TCMT IO Bool
no = do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is frozen, cannot set it to ∞"
Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` do Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (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
$ do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"solution " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
m []) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
TCMT IO Doc
" := " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
inf
t <- MetaId -> TCMT IO Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
m
TelV tel core <- telView t
unlessM (isJust <$> isSizeType core) __IMPOSSIBLE__
assignMeta 0 m t (List.downFrom $ size tel) inf
return True
when solvedAll $ do
noConstraints $ mapM_ (withConstraint solveConstraint . fst) ccs
`catchError` \ TCErr
_ ->
TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ List1 (ProblemConstraint, HypSizeConstraint) -> Doc -> TypeError
CannotSolveSizeConstraints List1 (ProblemConstraint, HypSizeConstraint)
ccs Doc
forall a. Null a => a
empty
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
(_, msizelt) <- TCMT IO (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
caseMaybe msizelt (return []) $ \ QName
sizelt -> do
[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
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 :: [Char]
s = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
t <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term) -> (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 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 a. a -> TCMT IO a
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 a. a -> TCMT IO a
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 ([Char] -> Int -> NamedRigid
NamedRigid [Char]
s Int
i) Offset
0) Cmp
Lt DBSizeExpr
a)
Term
_ -> Maybe (Int, SizeConstraint)
-> TCMT IO (Maybe (Int, SizeConstraint))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Int, SizeConstraint)
forall a. Maybe a
Nothing
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
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__
instance Subst (SizeExpr' NamedRigid SizeMeta) where
type SubstArg (SizeExpr' NamedRigid SizeMeta) = Term
applySubst :: Substitution' (SubstArg DBSizeExpr) -> DBSizeExpr -> DBSizeExpr
applySubst Substitution' (SubstArg DBSizeExpr)
sigma DBSizeExpr
a =
case DBSizeExpr
a of
DBSizeExpr
Infty -> DBSizeExpr
a
Const{} -> DBSizeExpr
a
Flex SizeMeta
x Offset
n -> SizeMeta -> Offset -> DBSizeExpr
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex (Substitution' (SubstArg SizeMeta) -> SizeMeta -> SizeMeta
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg SizeMeta)
Substitution' (SubstArg DBSizeExpr)
sigma SizeMeta
x) Offset
n
Rigid NamedRigid
r Offset
n ->
case Substitution' Term -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' Term
Substitution' (SubstArg DBSizeExpr)
sigma (Int -> Term) -> Int -> Term
forall a b. (a -> b) -> a -> b
$ NamedRigid -> Int
rigidIndex NamedRigid
r of
Var Int
j [] -> NamedRigid -> Offset -> DBSizeExpr
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid NamedRigid
r{ rigidIndex = j } Offset
n
Term
_ -> DBSizeExpr
forall a. HasCallStack => a
__IMPOSSIBLE__
instance Subst SizeConstraint where
type SubstArg SizeConstraint = Term
applySubst :: Substitution' (SubstArg 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)
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
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.size.solve" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"converting size constraint"
, ProblemConstraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ProblemConstraint -> m Doc
prettyTCM ProblemConstraint
c
]
ma <- Term -> TCMT IO (Maybe DBSizeExpr)
sizeExpr Term
u
mb <- sizeExpr v
(hids, hs) <- unzip <$> getSizeHypotheses cxt
let mk DBSizeExpr
a DBSizeExpr
b = Context
-> [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
return $ mk <$> ma <*> mb
Constraint
_ -> TCMT IO (Maybe HypSizeConstraint)
forall a. HasCallStack => a
__IMPOSSIBLE__
sizeExpr :: Term -> TCM (Maybe DBSizeExpr)
sizeExpr :: Term -> TCMT IO (Maybe DBSizeExpr)
sizeExpr Term
u = do
u <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
reportSDoc "tc.conv.size" 60 $ "sizeExpr:" <+> prettyTCM u
s <- sizeView u
case s of
SizeView
SizeInf -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr))
-> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a b. (a -> b) -> a -> b
$ DBSizeExpr -> Maybe DBSizeExpr
forall a. a -> Maybe a
Just DBSizeExpr
forall rigid flex. SizeExpr' rigid flex
Infty
SizeSuc Term
u -> (DBSizeExpr -> DBSizeExpr) -> Maybe DBSizeExpr -> Maybe DBSizeExpr
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DBSizeExpr -> Offset -> DBSizeExpr
forall a b c. Plus a b c => a -> b -> c
`plus` (Offset
1 :: Offset)) (Maybe DBSizeExpr -> Maybe DBSizeExpr)
-> TCMT IO (Maybe DBSizeExpr) -> TCMT IO (Maybe DBSizeExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO (Maybe DBSizeExpr)
sizeExpr Term
u
OtherSize Term
u -> case Term
u of
Var Int
i [] -> (\ [Char]
x -> DBSizeExpr -> Maybe DBSizeExpr
forall a. a -> Maybe a
Just (DBSizeExpr -> Maybe DBSizeExpr) -> DBSizeExpr -> Maybe DBSizeExpr
forall a b. (a -> b) -> a -> b
$ NamedRigid -> Offset -> DBSizeExpr
forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
Rigid ([Char] -> Int -> NamedRigid
NamedRigid [Char]
x Int
i) Offset
0) ([Char] -> Maybe DBSizeExpr)
-> (Name -> [Char]) -> Name -> Maybe DBSizeExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> Maybe DBSizeExpr)
-> TCMT IO Name -> TCMT IO (Maybe DBSizeExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Name
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
Int -> m Name
nameOfBV Int
i
MetaV MetaId
m Elims
es | Just [Int]
xs <- (Elim' Term -> Maybe Int) -> Elims -> Maybe [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> Maybe Int
isVar Elims
es, [Int] -> Bool
forall a. Ord a => [a] -> Bool
List.fastDistinct [Int]
xs
-> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr))
-> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a b. (a -> b) -> a -> b
$ DBSizeExpr -> Maybe DBSizeExpr
forall a. a -> Maybe a
Just (DBSizeExpr -> Maybe DBSizeExpr) -> DBSizeExpr -> Maybe DBSizeExpr
forall a b. (a -> b) -> a -> b
$ SizeMeta -> Offset -> DBSizeExpr
forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
Flex (MetaId -> [Int] -> SizeMeta
SizeMeta MetaId
m [Int]
xs) Offset
0
Term
_ -> Maybe DBSizeExpr -> TCMT IO (Maybe DBSizeExpr)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe DBSizeExpr
forall a. Maybe a
Nothing
where
isVar :: Elim' Term -> Maybe Int
isVar (Proj{}) = Maybe Int
forall a. Maybe a
Nothing
isVar (IApply Term
_ Term
_ Term
v) = Elim' Term -> Maybe Int
isVar (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v))
isVar (Apply Arg Term
v) = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v of
Var Int
i [] -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
Term
_ -> Maybe Int
forall a. Maybe a
Nothing