{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.SizedTypes where
import Prelude hiding (null)
import Control.Monad.Writer
import qualified Data.Foldable as Fold
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.Map as Map
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import {-# SOURCE #-} Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.Constraints
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Functor
import Agda.Utils.List as List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (Pretty)
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import qualified Agda.Utils.Pretty as P
import qualified Agda.Utils.Warshall as W
import Agda.Utils.Impossible
checkSizeLtSat :: Term -> TCM ()
checkSizeLtSat :: Term -> TCM ()
checkSizeLtSat t :: Term
t = TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCMT IO Bool
haveSizeLt (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size" 10 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
Telescope
tel <- TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
[TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
[ "checking that " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> " is not an empty type of sizes"
, if Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel then TCM Doc
forall a. Null a => a
empty else do
"in context " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel)
]
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size" 60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "- raw type = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show Term
t
let postpone :: Term -> TCM ()
postpone :: Term -> TCM ()
postpone t :: Term
t = do
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size.lt" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
[ "- postponing `not empty type of sizes' check for " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t ]
Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Constraint
CheckSizeLtSat Term
t
let ok :: TCM ()
ok :: TCM ()
ok = VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.lt" 20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "- succeeded: not an empty type of sizes"
Term
-> (MetaId -> Term -> TCM ())
-> (NotBlocked -> Term -> TCM ())
-> TCM ()
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
t ((Term -> TCM ()) -> MetaId -> Term -> TCM ()
forall a b. a -> b -> a
const Term -> TCM ()
postpone) ((NotBlocked -> Term -> TCM ()) -> TCM ())
-> (NotBlocked -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ _ t :: Term
t -> do
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.lt" 20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "- type is not blocked"
TCMT IO (Maybe BoundedSize)
-> TCM () -> (BoundedSize -> TCM ()) -> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Term -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Term
t) TCM ()
ok ((BoundedSize -> TCM ()) -> TCM ())
-> (BoundedSize -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ b :: BoundedSize
b -> do
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.lt" 20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " - type is a size type"
case BoundedSize
b of
BoundedNo -> TCM ()
ok
BoundedLt b :: Term
b -> do
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size.lt" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ " - type is SIZELT" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
b
Term
-> (MetaId -> Term -> TCM ())
-> (NotBlocked -> Term -> TCM ())
-> TCM ()
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
b (\ _ _ -> Term -> TCM ()
postpone Term
t) ((NotBlocked -> Term -> TCM ()) -> TCM ())
-> (NotBlocked -> Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ _ b :: Term
b -> do
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.lt" 20 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ " - size bound is not blocked"
Constraint -> TCM () -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Constraint -> m () -> m ()
catchConstraint (Term -> Constraint
CheckSizeLtSat Term
t) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Term -> TCMT IO Bool
checkSizeNeverZero Term
b) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> (Doc -> TypeError) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM ()) -> TCM Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
"Possibly empty type of sizes " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
t
checkSizeNeverZero :: Term -> TCM Bool
checkSizeNeverZero :: Term -> TCMT IO Bool
checkSizeNeverZero u :: Term
u = do
SizeView
v <- Term -> TCMT IO SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
case SizeView
v of
SizeInf -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
SizeSuc{} -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
OtherSize u :: Term
u ->
case Term
u of
Var i :: VerboseLevel
i [] -> VerboseLevel -> TCMT IO Bool
checkSizeVarNeverZero VerboseLevel
i
_ -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
checkSizeVarNeverZero :: Int -> TCM Bool
checkSizeVarNeverZero :: VerboseLevel -> TCMT IO Bool
checkSizeVarNeverZero i :: VerboseLevel
i = do
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ "checkSizeVarNeverZero" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (VerboseLevel -> Term
var VerboseLevel
i)
[Type]
ts <- (Dom' Term (Name, Type) -> Type)
-> [Dom' Term (Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) ([Dom' Term (Name, Type)] -> [Type])
-> ([Dom' Term (Name, Type)] -> [Dom' Term (Name, Type)])
-> [Dom' Term (Name, Type)]
-> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel
-> [Dom' Term (Name, Type)] -> [Dom' Term (Name, Type)]
forall a. VerboseLevel -> [a] -> [a]
take VerboseLevel
i ([Dom' Term (Name, Type)] -> [Type])
-> TCMT IO [Dom' Term (Name, Type)] -> TCMT IO [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Dom' Term (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
getContext
(n :: VerboseLevel
n, Any meta :: Bool
meta) <- WriterT Any TCM VerboseLevel -> TCM (VerboseLevel, Any)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT Any TCM VerboseLevel -> TCM (VerboseLevel, Any))
-> WriterT Any TCM VerboseLevel -> TCM (VerboseLevel, Any)
forall a b. (a -> b) -> a -> b
$ [Type] -> [VerboseLevel] -> WriterT Any TCM VerboseLevel
minSizeValAux [Type]
ts ([VerboseLevel] -> WriterT Any TCM VerboseLevel)
-> [VerboseLevel] -> WriterT Any TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. a -> [a]
repeat 0
if VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else
if Bool
meta then TCMT IO Bool
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation else Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
where
minSizeValAux :: [Type] -> [Int] -> WriterT Any TCM Int
minSizeValAux :: [Type] -> [VerboseLevel] -> WriterT Any TCM VerboseLevel
minSizeValAux _ [] = WriterT Any TCM VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__
minSizeValAux [] (n :: VerboseLevel
n : _) = VerboseLevel -> WriterT Any TCM VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return VerboseLevel
n
minSizeValAux (t :: Type
t : ts :: [Type]
ts) (n :: VerboseLevel
n : ns :: [VerboseLevel]
ns) = do
VerboseKey -> VerboseLevel -> TCM Doc -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size" 60 (TCM Doc -> WriterT Any TCM ()) -> TCM Doc -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$
VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text ("minSizeVal (n:ns) = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [VerboseLevel] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. VerboseLevel -> [a] -> [a]
take ([Type] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Type]
ts VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ 2) ([VerboseLevel] -> [VerboseLevel])
-> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> a -> b
$ VerboseLevel
nVerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. a -> [a] -> [a]
:[VerboseLevel]
ns) VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++
" t =") TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (VerboseKey -> TCM Doc
forall (m :: * -> *). Monad m => VerboseKey -> m Doc
text (VerboseKey -> TCM Doc) -> (Type -> VerboseKey) -> Type -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> VerboseKey
forall a. Show a => a -> VerboseKey
show) Type
t
let cont :: WriterT Any TCM VerboseLevel
cont = [Type] -> [VerboseLevel] -> WriterT Any TCM VerboseLevel
minSizeValAux [Type]
ts [VerboseLevel]
ns
perhaps :: WriterT Any TCM VerboseLevel
perhaps = Any -> WriterT Any TCM ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True) WriterT Any TCM ()
-> WriterT Any TCM VerboseLevel -> WriterT Any TCM VerboseLevel
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> WriterT Any TCM VerboseLevel
cont
Type
-> (MetaId -> Type -> WriterT Any TCM VerboseLevel)
-> (NotBlocked -> Type -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ _ _ -> WriterT Any TCM VerboseLevel
perhaps) ((NotBlocked -> Type -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel)
-> (NotBlocked -> Type -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ \ _ t :: Type
t -> do
WriterT Any TCM (Maybe BoundedSize)
-> WriterT Any TCM VerboseLevel
-> (BoundedSize -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TCMT IO (Maybe BoundedSize) -> WriterT Any TCM (Maybe BoundedSize)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO (Maybe BoundedSize)
-> WriterT Any TCM (Maybe BoundedSize))
-> TCMT IO (Maybe BoundedSize)
-> WriterT Any TCM (Maybe BoundedSize)
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
t) WriterT Any TCM VerboseLevel
cont ((BoundedSize -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel)
-> (BoundedSize -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ \ b :: BoundedSize
b -> do
case BoundedSize
b of
BoundedNo -> WriterT Any TCM VerboseLevel
cont
BoundedLt u :: Term
u -> Term
-> (MetaId -> Term -> WriterT Any TCM VerboseLevel)
-> (NotBlocked -> Term -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
u (\ _ _ -> WriterT Any TCM VerboseLevel
perhaps) ((NotBlocked -> Term -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel)
-> (NotBlocked -> Term -> WriterT Any TCM VerboseLevel)
-> WriterT Any TCM VerboseLevel
forall a b. (a -> b) -> a -> b
$ \ _ u :: Term
u -> do
VerboseKey -> VerboseLevel -> VerboseKey -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size" 60 (VerboseKey -> WriterT Any TCM ())
-> VerboseKey -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$ "minSizeVal upper bound u = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Term -> VerboseKey
forall a. Show a => a -> VerboseKey
show Term
u
DeepSizeView
v <- TCM DeepSizeView -> WriterT Any TCM DeepSizeView
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM DeepSizeView -> WriterT Any TCM DeepSizeView)
-> TCM DeepSizeView -> WriterT Any TCM DeepSizeView
forall a b. (a -> b) -> a -> b
$ Term -> TCM DeepSizeView
deepSizeView Term
u
case DeepSizeView
v of
DSizeVar j :: VerboseLevel
j m :: VerboseLevel
m -> do
VerboseKey -> VerboseLevel -> VerboseKey -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size" 60 (VerboseKey -> WriterT Any TCM ())
-> VerboseKey -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$ "minSizeVal upper bound v = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ DeepSizeView -> VerboseKey
forall a. Show a => a -> VerboseKey
show DeepSizeView
v
let ns' :: [VerboseLevel]
ns' = VerboseLevel
-> (VerboseLevel -> VerboseLevel)
-> [VerboseLevel]
-> [VerboseLevel]
forall a. VerboseLevel -> (a -> a) -> [a] -> [a]
List.updateAt VerboseLevel
j (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Ord a => a -> a -> a
max (VerboseLevel -> VerboseLevel -> VerboseLevel)
-> VerboseLevel -> VerboseLevel -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ VerboseLevel
nVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+1VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
m) [VerboseLevel]
ns
VerboseKey -> VerboseLevel -> VerboseKey -> WriterT Any TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size" 60 (VerboseKey -> WriterT Any TCM ())
-> VerboseKey -> WriterT Any TCM ()
forall a b. (a -> b) -> a -> b
$ "minSizeVal ns' = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [VerboseLevel] -> VerboseKey
forall a. Show a => a -> VerboseKey
show (VerboseLevel -> [VerboseLevel] -> [VerboseLevel]
forall a. VerboseLevel -> [a] -> [a]
take ([Type] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Type]
ts VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ 1) [VerboseLevel]
ns')
[Type] -> [VerboseLevel] -> WriterT Any TCM VerboseLevel
minSizeValAux [Type]
ts [VerboseLevel]
ns'
DSizeMeta{} -> WriterT Any TCM VerboseLevel
perhaps
_ -> WriterT Any TCM VerboseLevel
cont
isBounded :: (MonadReduce m, MonadTCEnv m, HasBuiltins m)
=> Nat -> m BoundedSize
isBounded :: VerboseLevel -> m BoundedSize
isBounded i :: VerboseLevel
i = do
Type
t <- Type -> m Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> m Type) -> m Type -> m Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseLevel -> m Type
forall (m :: * -> *).
(Applicative m, MonadFail m, MonadTCEnv m) =>
VerboseLevel -> m Type
typeOfBV VerboseLevel
i
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
Def x :: QName
x [Apply u :: Arg Term
u] -> do
Maybe Term
sizelt <- VerboseKey -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => VerboseKey -> m (Maybe Term)
getBuiltin' VerboseKey
builtinSizeLt
BoundedSize -> m BoundedSize
forall (m :: * -> *) a. Monad m => a -> m a
return (BoundedSize -> m BoundedSize) -> BoundedSize -> m BoundedSize
forall a b. (a -> b) -> a -> b
$ if (Term -> Maybe Term
forall a. a -> Maybe a
Just (QName -> Elims -> Term
Def QName
x []) Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Term
sizelt) then Term -> BoundedSize
BoundedLt (Term -> BoundedSize) -> Term -> BoundedSize
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u else BoundedSize
BoundedNo
_ -> BoundedSize -> m BoundedSize
forall (m :: * -> *) a. Monad m => a -> m a
return BoundedSize
BoundedNo
boundedSizeMetaHook
:: ( MonadConstraint m
, MonadTCEnv m
, ReadTCState m
, MonadAddContext m
, HasOptions m
, HasBuiltins m
)
=> Term -> Telescope -> Type -> m ()
boundedSizeMetaHook :: Term -> Telescope -> Type -> m ()
boundedSizeMetaHook v :: Term
v tel0 :: Telescope
tel0 a :: Type
a = do
Maybe BoundedSize
res <- Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
a
case Maybe BoundedSize
res of
Just (BoundedLt u :: Term
u) -> do
VerboseLevel
n <- m VerboseLevel
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m VerboseLevel
getContextSize
let tel :: Telescope
tel | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> 0 = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> ListTel -> ListTel
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
n (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (VerboseKey, t)]
telToList Telescope
tel0
| Bool
otherwise = Telescope
tel0
Telescope -> m () -> m ()
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
Term
v <- VerboseLevel -> Term -> m Term
forall (m :: * -> *).
HasBuiltins m =>
VerboseLevel -> Term -> m Term
sizeSuc 1 (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term -> Term
forall t a. Subst t a => VerboseLevel -> a -> a
raise (Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel) Term
v Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Telescope -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Telescope
tel
Constraint -> m ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpLeq CompareAs
AsSizes Term
v Term
u
_ -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
trySizeUniv
:: MonadConversion m
=> Comparison -> CompareAs -> Term -> Term
-> QName -> Elims -> QName -> Elims -> m ()
trySizeUniv :: Comparison
-> CompareAs
-> Term
-> Term
-> QName
-> Elims
-> QName
-> Elims
-> m ()
trySizeUniv cmp :: Comparison
cmp t :: CompareAs
t m :: Term
m n :: Term
n x :: QName
x els1 :: Elims
els1 y :: QName
y els2 :: Elims
els2 = do
let failure :: m a
failure = TypeError -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m a) -> TypeError -> m a
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
m Term
n CompareAs
t
forceInfty :: Arg Term -> m ()
forceInfty u :: Arg Term
u = Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
CmpEq (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u) (Term -> m ()) -> m Term -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
(size :: QName
size, sizelt :: QName
sizelt) <- (m (QName, QName)
-> (TCErr -> m (QName, QName)) -> m (QName, QName))
-> (TCErr -> m (QName, QName))
-> m (QName, QName)
-> m (QName, QName)
forall a b c. (a -> b -> c) -> b -> a -> c
flip m (QName, QName) -> (TCErr -> m (QName, QName)) -> m (QName, QName)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (m (QName, QName) -> TCErr -> m (QName, QName)
forall a b. a -> b -> a
const m (QName, QName)
forall a. m a
failure) (m (QName, QName) -> m (QName, QName))
-> m (QName, QName) -> m (QName, QName)
forall a b. (a -> b) -> a -> b
$ do
Def size :: QName
size _ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
Def sizelt :: QName
sizelt _ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeLt
(QName, QName) -> m (QName, QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
size, QName
sizelt)
case (Comparison
cmp, Elims
els1, Elims
els2) of
(CmpLeq, [_], []) | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
size -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(_, [Apply u :: Arg Term
u], []) | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
size -> Arg Term -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh VerboseLevel m) =>
Arg Term -> m ()
forceInfty Arg Term
u
(_, [], [Apply u :: Arg Term
u]) | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
size Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sizelt -> Arg Term -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh VerboseLevel m) =>
Arg Term -> m ()
forceInfty Arg Term
u
_ -> m ()
forall a. m a
failure
deepSizeView :: Term -> TCM DeepSizeView
deepSizeView :: Term -> TCM DeepSizeView
deepSizeView v :: Term
v = do
Def inf :: QName
inf [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
Def suc :: QName
suc [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
let loop :: Term -> m DeepSizeView
loop v :: Term
v = do
Term
v <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
case Term
v of
Def x :: QName
x [] | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
inf -> DeepSizeView -> m DeepSizeView
forall (m :: * -> *) a. Monad m => a -> m a
return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
forall a b. (a -> b) -> a -> b
$ DeepSizeView
DSizeInf
Def x :: QName
x [Apply u :: Arg Term
u] | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
suc -> QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ QName
suc (DeepSizeView -> DeepSizeView) -> m DeepSizeView -> m DeepSizeView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m DeepSizeView
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u)
Var i :: VerboseLevel
i [] -> DeepSizeView -> m DeepSizeView
forall (m :: * -> *) a. Monad m => a -> m a
return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> VerboseLevel -> DeepSizeView
DSizeVar VerboseLevel
i 0
MetaV x :: MetaId
x us :: Elims
us -> DeepSizeView -> m DeepSizeView
forall (m :: * -> *) a. Monad m => a -> m a
return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> VerboseLevel -> DeepSizeView
DSizeMeta MetaId
x Elims
us 0
_ -> DeepSizeView -> m DeepSizeView
forall (m :: * -> *) a. Monad m => a -> m a
return (DeepSizeView -> m DeepSizeView) -> DeepSizeView -> m DeepSizeView
forall a b. (a -> b) -> a -> b
$ Term -> DeepSizeView
DOtherSize Term
v
Term -> TCM DeepSizeView
forall (m :: * -> *). MonadReduce m => Term -> m DeepSizeView
loop Term
v
sizeMaxView :: (MonadReduce m, HasBuiltins m) => Term -> m SizeMaxView
sizeMaxView :: Term -> m SizeMaxView
sizeMaxView v :: Term
v = do
Maybe QName
inf <- VerboseKey -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinDefName VerboseKey
builtinSizeInf
Maybe QName
suc <- VerboseKey -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinDefName VerboseKey
builtinSizeSuc
Maybe QName
max <- VerboseKey -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getBuiltinDefName VerboseKey
builtinSizeMax
let loop :: Term -> f SizeMaxView
loop v :: Term
v = do
Term
v <- Term -> f Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
case Term
v of
Def x :: QName
x [] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
inf -> SizeMaxView -> f SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> f SizeMaxView) -> SizeMaxView -> f SizeMaxView
forall a b. (a -> b) -> a -> b
$ DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
forall a b. (a -> b) -> a -> b
$ DeepSizeView
DSizeInf
Def x :: QName
x [Apply u :: Arg Term
u] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
suc -> QName -> SizeMaxView -> SizeMaxView
maxViewSuc_ (Maybe QName -> QName
forall a. HasCallStack => Maybe a -> a
fromJust Maybe QName
suc) (SizeMaxView -> SizeMaxView) -> f SizeMaxView -> f SizeMaxView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f SizeMaxView
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u)
Def x :: QName
x [Apply u1 :: Arg Term
u1, Apply u2 :: Arg Term
u2] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
max -> SizeMaxView -> SizeMaxView -> SizeMaxView
maxViewMax (SizeMaxView -> SizeMaxView -> SizeMaxView)
-> f SizeMaxView -> f (SizeMaxView -> SizeMaxView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f SizeMaxView
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u1) f (SizeMaxView -> SizeMaxView) -> f SizeMaxView -> f SizeMaxView
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> f SizeMaxView
loop (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u2)
Var i :: VerboseLevel
i [] -> SizeMaxView -> f SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> f SizeMaxView) -> SizeMaxView -> f SizeMaxView
forall a b. (a -> b) -> a -> b
$ DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> VerboseLevel -> DeepSizeView
DSizeVar VerboseLevel
i 0
MetaV x :: MetaId
x us :: Elims
us -> SizeMaxView -> f SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> f SizeMaxView) -> SizeMaxView -> f SizeMaxView
forall a b. (a -> b) -> a -> b
$ DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> VerboseLevel -> DeepSizeView
DSizeMeta MetaId
x Elims
us 0
_ -> SizeMaxView -> f SizeMaxView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeMaxView -> f SizeMaxView) -> SizeMaxView -> f SizeMaxView
forall a b. (a -> b) -> a -> b
$ DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton (DeepSizeView -> SizeMaxView) -> DeepSizeView -> SizeMaxView
forall a b. (a -> b) -> a -> b
$ Term -> DeepSizeView
DOtherSize Term
v
Term -> m SizeMaxView
forall (f :: * -> *). MonadReduce f => Term -> f SizeMaxView
loop Term
v
compareSizes :: (MonadConversion m) => Comparison -> Term -> Term -> m ()
compareSizes :: Comparison -> Term -> Term -> m ()
compareSizes cmp :: Comparison
cmp u :: Term
u v :: Term
v = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket "tc.conv.size" 10 "compareSizes" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.conv.size" 10 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
[ "Comparing sizes"
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Comparison -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp
, Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
]
]
VerboseKey -> VerboseLevel -> m () -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS "tc.conv.size" 60 (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
Term
u <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
Term
v <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.conv.size" 60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ Term -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Term
u TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Comparison -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Comparison
cmp
, Term -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Term
v
]
SizeMaxView
us <- Term -> m SizeMaxView
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Term -> m SizeMaxView
sizeMaxView Term
u
SizeMaxView
vs <- Term -> m SizeMaxView
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Term -> m SizeMaxView
sizeMaxView Term
v
Comparison -> SizeMaxView -> SizeMaxView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> SizeMaxView -> SizeMaxView -> m ()
compareMaxViews Comparison
cmp SizeMaxView
us SizeMaxView
vs
compareMaxViews :: (MonadConversion m) => Comparison -> SizeMaxView -> SizeMaxView -> m ()
compareMaxViews :: Comparison -> SizeMaxView -> SizeMaxView -> m ()
compareMaxViews cmp :: Comparison
cmp us :: SizeMaxView
us vs :: SizeMaxView
vs = case (Comparison
cmp, SizeMaxView
us, SizeMaxView
vs) of
(CmpLeq, _, (DSizeInf :| _)) -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(cmp :: Comparison
cmp, u :: DeepSizeView
u:|[], v :: DeepSizeView
v:|[]) -> Comparison -> DeepSizeView -> DeepSizeView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
cmp DeepSizeView
u DeepSizeView
v
(CmpLeq, us :: SizeMaxView
us, v :: DeepSizeView
v:|[]) -> SizeMaxView -> (DeepSizeView -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Fold.forM_ SizeMaxView
us ((DeepSizeView -> m ()) -> m ()) -> (DeepSizeView -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ u :: DeepSizeView
u -> Comparison -> DeepSizeView -> DeepSizeView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
cmp DeepSizeView
u DeepSizeView
v
(CmpLeq, us :: SizeMaxView
us, vs :: SizeMaxView
vs) -> SizeMaxView -> (DeepSizeView -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
Fold.forM_ SizeMaxView
us ((DeepSizeView -> m ()) -> m ()) -> (DeepSizeView -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ u :: DeepSizeView
u -> DeepSizeView -> SizeMaxView -> m ()
forall (m :: * -> *).
MonadConversion m =>
DeepSizeView -> SizeMaxView -> m ()
compareBelowMax DeepSizeView
u SizeMaxView
vs
(CmpEq, us :: SizeMaxView
us, vs :: SizeMaxView
vs) -> do
Comparison -> SizeMaxView -> SizeMaxView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> SizeMaxView -> SizeMaxView -> m ()
compareMaxViews Comparison
CmpLeq SizeMaxView
us SizeMaxView
vs
Comparison -> SizeMaxView -> SizeMaxView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> SizeMaxView -> SizeMaxView -> m ()
compareMaxViews Comparison
CmpLeq SizeMaxView
vs SizeMaxView
us
compareBelowMax :: (MonadConversion m) => DeepSizeView -> SizeMaxView -> m ()
compareBelowMax :: DeepSizeView -> SizeMaxView -> m ()
compareBelowMax u :: DeepSizeView
u vs :: SizeMaxView
vs = VerboseKey -> VerboseLevel -> VerboseKey -> m () -> m ()
forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m a -> m a
verboseBracket "tc.conv.size" 45 "compareBelowMax" (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.conv.size" 45 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
[ DeepSizeView -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty DeepSizeView
u
, Comparison -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Comparison
CmpLeq
, SizeMaxView -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty SizeMaxView
vs
]
m () -> m () -> m ()
forall b (m :: * -> *) a. MonadError b m => m a -> m a -> m a
alt (m () -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ (m () -> m () -> m ()) -> NonEmpty (m ()) -> m ()
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
Fold.foldr1 m () -> m () -> m ()
forall b (m :: * -> *) a. MonadError b m => m a -> m a -> m a
alt (NonEmpty (m ()) -> m ()) -> NonEmpty (m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ (DeepSizeView -> m ()) -> SizeMaxView -> NonEmpty (m ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Comparison -> DeepSizeView -> DeepSizeView -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews Comparison
CmpLeq DeepSizeView
u) SizeMaxView
vs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.conv.size" 45 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
[ "compareBelowMax: giving up"
]
Term
u <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
u
Term
v <- SizeMaxView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
SizeMaxView -> m Term
unMaxView SizeMaxView
vs
Type
size <- m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
Comparison -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
giveUp Comparison
CmpLeq Type
size Term
u Term
v
where
alt :: m a -> m a -> m a
alt c1 :: m a
c1 c2 :: m a
c2 = m a
c1 m a -> (b -> m a) -> m a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` m a -> b -> m a
forall a b. a -> b -> a
const m a
c2
compareSizeViews :: (MonadConversion m) => Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews :: Comparison -> DeepSizeView -> DeepSizeView -> m ()
compareSizeViews cmp :: Comparison
cmp s1' :: DeepSizeView
s1' s2' :: DeepSizeView
s2' = do
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.conv.size" 45 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
hsep
[ "compareSizeViews"
, DeepSizeView -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty DeepSizeView
s1'
, Comparison -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty Comparison
cmp
, DeepSizeView -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty DeepSizeView
s2'
]
Type
size <- m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType
let (s1 :: DeepSizeView
s1, s2 :: DeepSizeView
s2) = (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
removeSucs (DeepSizeView
s1', DeepSizeView
s2')
withUnView :: (Term -> Term -> m b) -> m b
withUnView cont :: Term -> Term -> m b
cont = do
Term
u <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s1
Term
v <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s2
Term -> Term -> m b
cont Term
u Term
v
failure :: m b
failure = (Term -> Term -> m b) -> m b
forall (m :: * -> *) b.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
(Term -> Term -> m b) -> m b
withUnView ((Term -> Term -> m b) -> m b) -> (Term -> Term -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \ u :: Term
u v :: Term
v -> TypeError -> m b
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m b) -> TypeError -> m b
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
u Term
v CompareAs
AsSizes
continue :: Comparison -> m ()
continue cmp :: Comparison
cmp = (Term -> Term -> m ()) -> m ()
forall (m :: * -> *) b.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
(Term -> Term -> m b) -> m b
withUnView ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> CompareAs -> Term -> Term -> m ()
compareAtom Comparison
cmp CompareAs
AsSizes
case (Comparison
cmp, DeepSizeView
s1, DeepSizeView
s2) of
(CmpLeq, _, DSizeInf) -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(CmpEq, DSizeInf, DSizeInf) -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(CmpEq, DSizeVar{}, DSizeInf) -> m ()
forall b. m b
failure
(_ , DSizeInf, DSizeVar{}) -> m ()
forall b. m b
failure
(_ , DSizeInf, _ ) -> Comparison -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh VerboseLevel m) =>
Comparison -> m ()
continue Comparison
CmpEq
(CmpLeq, DSizeVar i :: VerboseLevel
i n :: VerboseLevel
n, DSizeVar j :: VerboseLevel
j m :: VerboseLevel
m) | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== VerboseLevel
j -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
m) m ()
forall b. m b
failure
(CmpLeq, DSizeVar i :: VerboseLevel
i n :: VerboseLevel
n, DSizeVar j :: VerboseLevel
j m :: VerboseLevel
m) | VerboseLevel
i VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
/= VerboseLevel
j -> do
BoundedSize
res <- VerboseLevel -> m BoundedSize
forall (m :: * -> *).
(MonadReduce m, MonadTCEnv m, HasBuiltins m) =>
VerboseLevel -> m BoundedSize
isBounded VerboseLevel
i
case BoundedSize
res of
BoundedNo -> m ()
forall b. m b
failure
BoundedLt u' :: Term
u' -> do
Term
v <- DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView DeepSizeView
s2
if VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then do
Term
u'' <- VerboseLevel -> Term -> m Term
forall (m :: * -> *).
HasBuiltins m =>
VerboseLevel -> Term -> m Term
sizeSuc (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 1) Term
u'
Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u'' Term
v
else Comparison -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Term -> Term -> m ()
compareSizes Comparison
cmp Term
u' (Term -> m ()) -> m Term -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseLevel -> Term -> m Term
forall (m :: * -> *).
HasBuiltins m =>
VerboseLevel -> Term -> m Term
sizeSuc 1 Term
v
(CmpLeq, s1 :: DeepSizeView
s1, s2 :: DeepSizeView
s2) -> (Term -> Term -> m ()) -> m ()
forall (m :: * -> *) b.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
(Term -> Term -> m b) -> m b
withUnView ((Term -> Term -> m ()) -> m ()) -> (Term -> Term -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ u :: Term
u v :: Term
v -> do
m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Term -> Term -> m Bool
forall (m :: * -> *). MonadConversion m => Term -> Term -> m Bool
trivial Term
u Term
v) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Comparison -> Type -> Term -> Term -> m ()
giveUp Comparison
CmpLeq Type
size Term
u Term
v
(CmpEq, s1 :: DeepSizeView
s1, s2 :: DeepSizeView
s2) -> Comparison -> m ()
forall (m :: * -> *).
(MonadMetaSolver m, MonadWarning m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh VerboseLevel m) =>
Comparison -> m ()
continue Comparison
cmp
giveUp :: (MonadConversion m) => Comparison -> Type -> Term -> Term -> m ()
giveUp :: Comparison -> Type -> Term -> Term -> m ()
giveUp cmp :: Comparison
cmp size :: Type
size u :: Term
u v :: Term
v =
m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((TCEnv -> Bool) -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envAssignMetas)
(Constraint -> m ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
addConstraint (Constraint -> m ()) -> Constraint -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> CompareAs -> Term -> Term -> Constraint
ValueCmp Comparison
CmpLeq CompareAs
AsSizes Term
u Term
v)
(TypeError -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ Comparison -> Term -> Term -> CompareAs -> TypeError
UnequalTerms Comparison
cmp Term
u Term
v CompareAs
AsSizes)
trivial :: (MonadConversion m) => Term -> Term -> m Bool
trivial :: Term -> Term -> m Bool
trivial u :: Term
u v :: Term
v = do
a :: (OldSizeExpr, VerboseLevel)
a@(e :: OldSizeExpr
e , n :: VerboseLevel
n ) <- Term -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
u
b :: (OldSizeExpr, VerboseLevel)
b@(e' :: OldSizeExpr
e', n' :: VerboseLevel
n') <- Term -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
v
let triv :: Bool
triv = OldSizeExpr
e OldSizeExpr -> OldSizeExpr -> Bool
forall a. Eq a => a -> a -> Bool
== OldSizeExpr
e' Bool -> Bool -> Bool
&& VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
<= VerboseLevel
n'
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.conv.size" 60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$
VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ if Bool
triv then "trivial constraint" else TCM Doc
forall a. Null a => a
empty
, (OldSizeExpr, VerboseLevel) -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (OldSizeExpr, VerboseLevel)
a TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> "<="
, (OldSizeExpr, VerboseLevel) -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty (OldSizeExpr, VerboseLevel)
b
]
Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
triv
m Bool -> (TCErr -> m Bool) -> m Bool
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isSizeProblem :: (ReadTCState m, HasOptions m, HasBuiltins m) => ProblemId -> m Bool
isSizeProblem :: ProblemId -> m Bool
isSizeProblem pid :: ProblemId
pid = do
Term -> Maybe BoundedSize
test <- m (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
(ProblemConstraint -> Bool) -> [ProblemConstraint] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test (Bool -> Comparison -> Bool
forall a b. a -> b -> a
const Bool
True) (Closure Constraint -> Bool)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) ([ProblemConstraint] -> Bool) -> m [ProblemConstraint] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProblemId -> m [ProblemConstraint]
forall (m :: * -> *).
ReadTCState m =>
ProblemId -> m [ProblemConstraint]
getConstraintsForProblem ProblemId
pid
isSizeConstraint :: (HasOptions m, HasBuiltins m) => (Comparison -> Bool) -> Closure Constraint -> m Bool
isSizeConstraint :: (Comparison -> Bool) -> Closure Constraint -> m Bool
isSizeConstraint p :: Comparison -> Bool
p c :: Closure Constraint
c = m (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest m (Term -> Maybe BoundedSize)
-> ((Term -> Maybe BoundedSize) -> Bool) -> m Bool
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ test :: Term -> Maybe BoundedSize
test -> (Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test Comparison -> Bool
p Closure Constraint
c
mkIsSizeConstraint :: (Term -> Maybe BoundedSize) -> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint :: (Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint test :: Term -> Maybe BoundedSize
test = (Type -> Bool)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
isSizeConstraint_ ((Type -> Bool)
-> (Comparison -> Bool) -> Closure Constraint -> Bool)
-> (Type -> Bool)
-> (Comparison -> Bool)
-> Closure Constraint
-> Bool
forall a b. (a -> b) -> a -> b
$ Maybe BoundedSize -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BoundedSize -> Bool)
-> (Type -> Maybe BoundedSize) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe BoundedSize
test (Term -> Maybe BoundedSize)
-> (Type -> Term) -> Type -> Maybe BoundedSize
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Term
forall t a. Type'' t a -> a
unEl
isSizeConstraint_
:: (Type -> Bool)
-> (Comparison -> Bool)
-> Closure Constraint
-> Bool
isSizeConstraint_ :: (Type -> Bool)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
isSizeConstraint_ _isSizeType :: Type -> Bool
_isSizeType p :: Comparison -> Bool
p Closure{ clValue :: forall a. Closure a -> a
clValue = ValueCmp cmp :: Comparison
cmp AsSizes _ _ } = Comparison -> Bool
p Comparison
cmp
isSizeConstraint_ isSizeType :: Type -> Bool
isSizeType p :: Comparison -> Bool
p Closure{ clValue :: forall a. Closure a -> a
clValue = ValueCmp cmp :: Comparison
cmp (AsTermsOf s :: Type
s) _ _ } = Comparison -> Bool
p Comparison
cmp Bool -> Bool -> Bool
&& Type -> Bool
isSizeType Type
s
isSizeConstraint_ _isSizeType :: Type -> Bool
_isSizeType _ _ = Bool
False
takeSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]
takeSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]
takeSizeConstraints p :: Comparison -> Bool
p = do
Term -> Maybe BoundedSize
test <- TCMT IO (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
(ProblemConstraint -> Closure Constraint)
-> [ProblemConstraint] -> [Closure Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint ([ProblemConstraint] -> [Closure Constraint])
-> TCMT IO [ProblemConstraint] -> TCM [Closure Constraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ProblemConstraint -> Bool) -> TCMT IO [ProblemConstraint]
forall (m :: * -> *).
MonadConstraint m =>
(ProblemConstraint -> Bool) -> m [ProblemConstraint]
takeConstraints ((Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test Comparison -> Bool
p (Closure Constraint -> Bool)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint)
getSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]
getSizeConstraints :: (Comparison -> Bool) -> TCM [Closure Constraint]
getSizeConstraints p :: Comparison -> Bool
p = do
Term -> Maybe BoundedSize
test <- TCMT IO (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
(Closure Constraint -> Bool)
-> [Closure Constraint] -> [Closure Constraint]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Term -> Maybe BoundedSize)
-> (Comparison -> Bool) -> Closure Constraint -> Bool
mkIsSizeConstraint Term -> Maybe BoundedSize
test Comparison -> Bool
p) ([Closure Constraint] -> [Closure Constraint])
-> ([ProblemConstraint] -> [Closure Constraint])
-> [ProblemConstraint]
-> [Closure Constraint]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Closure Constraint)
-> [ProblemConstraint] -> [Closure Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint ([ProblemConstraint] -> [Closure Constraint])
-> TCMT IO [ProblemConstraint] -> TCM [Closure Constraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAllConstraints
getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
getSizeMetas :: Bool -> TCM [(MetaId, Type, Telescope)]
getSizeMetas interactionMetas :: Bool
interactionMetas = do
Term -> Maybe BoundedSize
test <- TCMT IO (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest
[Maybe (MetaId, Type, Telescope)] -> [(MetaId, Type, Telescope)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (MetaId, Type, Telescope)] -> [(MetaId, Type, Telescope)])
-> TCMT IO [Maybe (MetaId, Type, Telescope)]
-> TCM [(MetaId, Type, Telescope)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas TCMT IO [MetaId]
-> ([MetaId] -> TCMT IO [Maybe (MetaId, Type, Telescope)])
-> TCMT IO [Maybe (MetaId, Type, Telescope)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= do
(MetaId -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> [MetaId] -> TCMT IO [Maybe (MetaId, Type, Telescope)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((MetaId -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> [MetaId] -> TCMT IO [Maybe (MetaId, Type, Telescope)])
-> (MetaId -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> [MetaId]
-> TCMT IO [Maybe (MetaId, Type, Telescope)]
forall a b. (a -> b) -> a -> b
$ \ m :: MetaId
m -> do
let no :: TCMT IO (Maybe a)
no = Maybe a -> TCMT IO (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
MetaVariable
mi <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mi of
_ | BlockedConst{} <- MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mi -> TCMT IO (Maybe (MetaId, Type, Telescope))
forall a. TCMT IO (Maybe a)
no
HasType _ cmp :: Comparison
cmp a :: Type
a -> do
TelV tel :: Telescope
tel b :: Type
b <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
Maybe BoundedSize
-> TCMT IO (Maybe (MetaId, Type, Telescope))
-> (BoundedSize -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> TCMT IO (Maybe (MetaId, Type, Telescope))
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Term -> Maybe BoundedSize
test (Term -> Maybe BoundedSize) -> Term -> Maybe BoundedSize
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
b) TCMT IO (Maybe (MetaId, Type, Telescope))
forall a. TCMT IO (Maybe a)
no ((BoundedSize -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> (BoundedSize -> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> TCMT IO (Maybe (MetaId, Type, Telescope))
forall a b. (a -> b) -> a -> b
$ \ _ -> do
let yes :: TCMT IO (Maybe (MetaId, Type, Telescope))
yes = Maybe (MetaId, Type, Telescope)
-> TCMT IO (Maybe (MetaId, Type, Telescope))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (MetaId, Type, Telescope)
-> TCMT IO (Maybe (MetaId, Type, Telescope)))
-> Maybe (MetaId, Type, Telescope)
-> TCMT IO (Maybe (MetaId, Type, Telescope))
forall a b. (a -> b) -> a -> b
$ (MetaId, Type, Telescope) -> Maybe (MetaId, Type, Telescope)
forall a. a -> Maybe a
Just (MetaId
m, Type
a, Telescope
tel)
if Bool
interactionMetas then TCMT IO (Maybe (MetaId, Type, Telescope))
yes else do
TCMT IO Bool
-> TCMT IO (Maybe (MetaId, Type, Telescope))
-> TCMT IO (Maybe (MetaId, Type, Telescope))
-> TCMT IO (Maybe (MetaId, Type, Telescope))
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Maybe InteractionId -> Bool
forall a. Maybe a -> Bool
isJust (Maybe InteractionId -> Bool)
-> TCMT IO (Maybe InteractionId) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
m) TCMT IO (Maybe (MetaId, Type, Telescope))
forall a. TCMT IO (Maybe a)
no TCMT IO (Maybe (MetaId, Type, Telescope))
yes
_ -> TCMT IO (Maybe (MetaId, Type, Telescope))
forall a. TCMT IO (Maybe a)
no
data OldSizeExpr
= SizeMeta MetaId [Int]
| Rigid Int
deriving (OldSizeExpr -> OldSizeExpr -> Bool
(OldSizeExpr -> OldSizeExpr -> Bool)
-> (OldSizeExpr -> OldSizeExpr -> Bool) -> Eq OldSizeExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OldSizeExpr -> OldSizeExpr -> Bool
$c/= :: OldSizeExpr -> OldSizeExpr -> Bool
== :: OldSizeExpr -> OldSizeExpr -> Bool
$c== :: OldSizeExpr -> OldSizeExpr -> Bool
Eq, VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey
[OldSizeExpr] -> VerboseKey -> VerboseKey
OldSizeExpr -> VerboseKey
(VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey)
-> (OldSizeExpr -> VerboseKey)
-> ([OldSizeExpr] -> VerboseKey -> VerboseKey)
-> Show OldSizeExpr
forall a.
(VerboseLevel -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [OldSizeExpr] -> VerboseKey -> VerboseKey
$cshowList :: [OldSizeExpr] -> VerboseKey -> VerboseKey
show :: OldSizeExpr -> VerboseKey
$cshow :: OldSizeExpr -> VerboseKey
showsPrec :: VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey
$cshowsPrec :: VerboseLevel -> OldSizeExpr -> VerboseKey -> VerboseKey
Show)
instance Pretty OldSizeExpr where
pretty :: OldSizeExpr -> Doc
pretty (SizeMeta m :: MetaId
m _) = VerboseKey -> Doc
P.text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ "X" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (MetaId -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral MetaId
m :: Int)
pretty (Rigid i :: VerboseLevel
i) = VerboseKey -> Doc
P.text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ "c" VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
i
data OldSizeConstraint
= Leq OldSizeExpr Int OldSizeExpr
deriving (VerboseLevel -> OldSizeConstraint -> VerboseKey -> VerboseKey
[OldSizeConstraint] -> VerboseKey -> VerboseKey
OldSizeConstraint -> VerboseKey
(VerboseLevel -> OldSizeConstraint -> VerboseKey -> VerboseKey)
-> (OldSizeConstraint -> VerboseKey)
-> ([OldSizeConstraint] -> VerboseKey -> VerboseKey)
-> Show OldSizeConstraint
forall a.
(VerboseLevel -> a -> VerboseKey -> VerboseKey)
-> (a -> VerboseKey) -> ([a] -> VerboseKey -> VerboseKey) -> Show a
showList :: [OldSizeConstraint] -> VerboseKey -> VerboseKey
$cshowList :: [OldSizeConstraint] -> VerboseKey -> VerboseKey
show :: OldSizeConstraint -> VerboseKey
$cshow :: OldSizeConstraint -> VerboseKey
showsPrec :: VerboseLevel -> OldSizeConstraint -> VerboseKey -> VerboseKey
$cshowsPrec :: VerboseLevel -> OldSizeConstraint -> VerboseKey -> VerboseKey
Show)
instance Pretty OldSizeConstraint where
pretty :: OldSizeConstraint -> Doc
pretty (Leq a :: OldSizeExpr
a n :: VerboseLevel
n b :: OldSizeExpr
b)
| VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> "=<" Doc -> Doc -> Doc
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b
| VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
> 0 = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> "=<" Doc -> Doc -> Doc
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b Doc -> Doc -> Doc
P.<+> "+" Doc -> Doc -> Doc
P.<+> VerboseKey -> Doc
P.text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show VerboseLevel
n)
| Bool
otherwise = OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
a Doc -> Doc -> Doc
P.<+> "+" Doc -> Doc -> Doc
P.<+> VerboseKey -> Doc
P.text (VerboseLevel -> VerboseKey
forall a. Show a => a -> VerboseKey
show (-VerboseLevel
n)) Doc -> Doc -> Doc
P.<+> "=<" Doc -> Doc -> Doc
P.<+> OldSizeExpr -> Doc
forall a. Pretty a => a -> Doc
P.pretty OldSizeExpr
b
oldComputeSizeConstraints :: [Closure Constraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints :: [Closure Constraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [] = [OldSizeConstraint] -> TCM [OldSizeConstraint]
forall (m :: * -> *) a. Monad m => a -> m a
return []
oldComputeSizeConstraints cs :: [Closure Constraint]
cs = [Maybe OldSizeConstraint] -> [OldSizeConstraint]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe OldSizeConstraint] -> [OldSizeConstraint])
-> TCMT IO [Maybe OldSizeConstraint] -> TCM [OldSizeConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Constraint -> TCMT IO (Maybe OldSizeConstraint))
-> [Constraint] -> TCMT IO [Maybe OldSizeConstraint]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Constraint -> TCMT IO (Maybe OldSizeConstraint)
oldComputeSizeConstraint [Constraint]
leqs
where
gammas :: [[Dom' Term (Name, Type)]]
gammas = (Closure Constraint -> [Dom' Term (Name, Type)])
-> [Closure Constraint] -> [[Dom' Term (Name, Type)]]
forall a b. (a -> b) -> [a] -> [b]
map (TCEnv -> [Dom' Term (Name, Type)]
envContext (TCEnv -> [Dom' Term (Name, Type)])
-> (Closure Constraint -> TCEnv)
-> Closure Constraint
-> [Dom' Term (Name, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> TCEnv
forall a. Closure a -> TCEnv
clEnv) [Closure Constraint]
cs
ls :: [Constraint]
ls = (Closure Constraint -> Constraint)
-> [Closure Constraint] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map Closure Constraint -> Constraint
forall a. Closure a -> a
clValue [Closure Constraint]
cs
ns :: [VerboseLevel]
ns = ([Dom' Term (Name, Type)] -> VerboseLevel)
-> [[Dom' Term (Name, Type)]] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map [Dom' Term (Name, Type)] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [[Dom' Term (Name, Type)]]
gammas
waterLevel :: VerboseLevel
waterLevel = [VerboseLevel] -> VerboseLevel
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [VerboseLevel]
ns
leqs :: [Constraint]
leqs = (VerboseLevel -> Constraint -> Constraint)
-> [VerboseLevel] -> [Constraint] -> [Constraint]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VerboseLevel -> Constraint -> Constraint
forall t a. Subst t a => VerboseLevel -> a -> a
raise ((VerboseLevel -> VerboseLevel) -> [VerboseLevel] -> [VerboseLevel]
forall a b. (a -> b) -> [a] -> [b]
map (VerboseLevel
waterLevel VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-) [VerboseLevel]
ns) [Constraint]
ls
oldComputeSizeConstraint :: Constraint -> TCM (Maybe OldSizeConstraint)
oldComputeSizeConstraint :: Constraint -> TCMT IO (Maybe OldSizeConstraint)
oldComputeSizeConstraint c :: Constraint
c =
case Constraint
c of
ValueCmp CmpLeq _ u :: Term
u v :: Term
v -> do
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size.solve" 50 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
[ "converting size constraint"
, Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Constraint
c
]
(a :: OldSizeExpr
a, n :: VerboseLevel
n) <- Term -> TCMT IO (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
u
(b :: OldSizeExpr
b, m :: VerboseLevel
m) <- Term -> TCMT IO (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
v
Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint))
-> Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
forall a b. (a -> b) -> a -> b
$ OldSizeConstraint -> Maybe OldSizeConstraint
forall a. a -> Maybe a
Just (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq OldSizeExpr
a (VerboseLevel
m VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
n) OldSizeExpr
b
TCMT IO (Maybe OldSizeConstraint)
-> (TCErr -> TCMT IO (Maybe OldSizeConstraint))
-> TCMT IO (Maybe OldSizeConstraint)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ err :: TCErr
err -> case TCErr
err of
PatternErr{} -> Maybe OldSizeConstraint -> TCMT IO (Maybe OldSizeConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe OldSizeConstraint
forall a. Maybe a
Nothing
_ -> TCErr -> TCMT IO (Maybe OldSizeConstraint)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
_ -> TCMT IO (Maybe OldSizeConstraint)
forall a. HasCallStack => a
__IMPOSSIBLE__
oldSizeExpr :: (MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m)
=> Term -> m (OldSizeExpr, Int)
oldSizeExpr :: Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr u :: Term
u = do
Term
u <- Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.conv.size" 60 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ "oldSizeExpr:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u
SizeView
s <- Term -> m SizeView
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
u
case SizeView
s of
SizeInf -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
SizeSuc u :: Term
u -> (VerboseLevel -> VerboseLevel)
-> (OldSizeExpr, VerboseLevel) -> (OldSizeExpr, VerboseLevel)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+1) ((OldSizeExpr, VerboseLevel) -> (OldSizeExpr, VerboseLevel))
-> m (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *).
(MonadReduce m, MonadDebug m, MonadError TCErr m, HasBuiltins m) =>
Term -> m (OldSizeExpr, VerboseLevel)
oldSizeExpr Term
u
OtherSize u :: Term
u -> case Term
u of
Var i :: VerboseLevel
i [] -> (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
i, 0)
MetaV m :: MetaId
m es :: Elims
es | Just xs :: [VerboseLevel]
xs <- (Elim' Term -> Maybe VerboseLevel) -> Elims -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Elim' Term -> Maybe VerboseLevel
isVar Elims
es, [VerboseLevel] -> Bool
forall a. Ord a => [a] -> Bool
fastDistinct [VerboseLevel]
xs
-> (OldSizeExpr, VerboseLevel) -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel]
xs, 0)
_ -> m (OldSizeExpr, VerboseLevel)
forall (m :: * -> *) a. MonadError TCErr m => m a
patternViolation
where
isVar :: Elim' Term -> Maybe VerboseLevel
isVar (Proj{}) = Maybe VerboseLevel
forall a. Maybe a
Nothing
isVar (IApply _ _ v :: Term
v) = Elim' Term -> Maybe VerboseLevel
isVar (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v))
isVar (Apply v :: Arg Term
v) = case Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v of
Var i :: VerboseLevel
i [] -> VerboseLevel -> Maybe VerboseLevel
forall a. a -> Maybe a
Just VerboseLevel
i
_ -> Maybe VerboseLevel
forall a. Maybe a
Nothing
flexibleVariables :: OldSizeConstraint -> [(MetaId, [Int])]
flexibleVariables :: OldSizeConstraint -> [(MetaId, [VerboseLevel])]
flexibleVariables (Leq a :: OldSizeExpr
a _ b :: OldSizeExpr
b) = OldSizeExpr -> [(MetaId, [VerboseLevel])]
flex OldSizeExpr
a [(MetaId, [VerboseLevel])]
-> [(MetaId, [VerboseLevel])] -> [(MetaId, [VerboseLevel])]
forall a. [a] -> [a] -> [a]
++ OldSizeExpr -> [(MetaId, [VerboseLevel])]
flex OldSizeExpr
b
where
flex :: OldSizeExpr -> [(MetaId, [VerboseLevel])]
flex (Rigid _) = []
flex (SizeMeta m :: MetaId
m xs :: [VerboseLevel]
xs) = [(MetaId
m, [VerboseLevel]
xs)]
oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint
oldCanonicalizeSizeConstraint :: OldSizeConstraint -> Maybe OldSizeConstraint
oldCanonicalizeSizeConstraint c :: OldSizeConstraint
c@(Leq a :: OldSizeExpr
a n :: VerboseLevel
n b :: OldSizeExpr
b) =
case (OldSizeExpr
a,OldSizeExpr
b) of
(Rigid{}, Rigid{}) -> OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return OldSizeConstraint
c
(SizeMeta m :: MetaId
m xs :: [VerboseLevel]
xs, Rigid i :: VerboseLevel
i) -> do
VerboseLevel
j <- (VerboseLevel -> Bool) -> [VerboseLevel] -> Maybe VerboseLevel
forall a. (a -> Bool) -> [a] -> Maybe VerboseLevel
List.findIndex (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==VerboseLevel
i) [VerboseLevel]
xs
OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-1]) VerboseLevel
n (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
j)
(Rigid i :: VerboseLevel
i, SizeMeta m :: MetaId
m xs :: [VerboseLevel]
xs) -> do
VerboseLevel
j <- (VerboseLevel -> Bool) -> [VerboseLevel] -> Maybe VerboseLevel
forall a. (a -> Bool) -> [a] -> Maybe VerboseLevel
List.findIndex (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==VerboseLevel
i) [VerboseLevel]
xs
OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (VerboseLevel -> OldSizeExpr
Rigid VerboseLevel
j) VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-1])
(SizeMeta m :: MetaId
m xs :: [VerboseLevel]
xs, SizeMeta l :: MetaId
l ys :: [VerboseLevel]
ys)
| Just ys' :: [VerboseLevel]
ys' <- (VerboseLevel -> Maybe VerboseLevel)
-> [VerboseLevel] -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ y :: VerboseLevel
y -> (VerboseLevel -> Bool) -> [VerboseLevel] -> Maybe VerboseLevel
forall a. (a -> Bool) -> [a] -> Maybe VerboseLevel
List.findIndex (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==VerboseLevel
y) [VerboseLevel]
xs) [VerboseLevel]
ys ->
OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
xsVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-1]) VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
l [VerboseLevel]
ys')
| Just xs' :: [VerboseLevel]
xs' <- (VerboseLevel -> Maybe VerboseLevel)
-> [VerboseLevel] -> Maybe [VerboseLevel]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ x :: VerboseLevel
x -> (VerboseLevel -> Bool) -> [VerboseLevel] -> Maybe VerboseLevel
forall a. (a -> Bool) -> [a] -> Maybe VerboseLevel
List.findIndex (VerboseLevel -> VerboseLevel -> Bool
forall a. Eq a => a -> a -> Bool
==VerboseLevel
x) [VerboseLevel]
ys) [VerboseLevel]
xs ->
OldSizeConstraint -> Maybe OldSizeConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (OldSizeConstraint -> Maybe OldSizeConstraint)
-> OldSizeConstraint -> Maybe OldSizeConstraint
forall a b. (a -> b) -> a -> b
$ OldSizeExpr -> VerboseLevel -> OldSizeExpr -> OldSizeConstraint
Leq (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
m [VerboseLevel]
xs') VerboseLevel
n (MetaId -> [VerboseLevel] -> OldSizeExpr
SizeMeta MetaId
l [0..[VerboseLevel] -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size [VerboseLevel]
ysVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-1])
| Bool
otherwise -> Maybe OldSizeConstraint
forall a. Maybe a
Nothing
oldSolveSizeConstraints :: TCM ()
oldSolveSizeConstraints :: TCM ()
oldSolveSizeConstraints = TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM TCMT IO Bool
haveSizedTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.solve" 70 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Considering to solve size constraints"
[Closure Constraint]
cs0 <- (Comparison -> Bool) -> TCM [Closure Constraint]
getSizeConstraints (Comparison -> Comparison -> Bool
forall a. Eq a => a -> a -> Bool
== Comparison
CmpLeq)
[OldSizeConstraint]
cs <- [Closure Constraint] -> TCM [OldSizeConstraint]
oldComputeSizeConstraints [Closure Constraint]
cs0
[(MetaId, Type, Telescope)]
ms <- Bool -> TCM [(MetaId, Type, Telescope)]
getSizeMetas Bool
True
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([OldSizeConstraint] -> Bool
forall a. Null a => a -> Bool
null [OldSizeConstraint]
cs) Bool -> Bool -> Bool
|| Bool -> Bool
not ([(MetaId, Type, Telescope)] -> Bool
forall a. Null a => a -> Bool
null [(MetaId, Type, Telescope)]
ms)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.solve" 10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Solving size constraints " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [OldSizeConstraint] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [OldSizeConstraint]
cs
[OldSizeConstraint]
cs <- [OldSizeConstraint] -> TCM [OldSizeConstraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([OldSizeConstraint] -> TCM [OldSizeConstraint])
-> [OldSizeConstraint] -> TCM [OldSizeConstraint]
forall a b. (a -> b) -> a -> b
$ (OldSizeConstraint -> Maybe OldSizeConstraint)
-> [OldSizeConstraint] -> [OldSizeConstraint]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe OldSizeConstraint -> Maybe OldSizeConstraint
oldCanonicalizeSizeConstraint [OldSizeConstraint]
cs
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.solve" 10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Canonicalized constraints: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [OldSizeConstraint] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [OldSizeConstraint]
cs
let
cannotSolve :: TCMT IO b
cannotSolve = TypeError -> TCMT IO b
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO b) -> (Doc -> TypeError) -> Doc -> TCMT IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO b) -> TCM Doc -> TCMT IO b
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
[TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ("Cannot solve size constraints" TCM Doc -> [TCM Doc] -> [TCM Doc]
forall a. a -> [a] -> [a]
: (Closure Constraint -> TCM Doc)
-> [Closure Constraint] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Closure Constraint -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Closure Constraint]
cs0)
metas0 :: [(MetaId, Int)]
metas0 :: [(MetaId, VerboseLevel)]
metas0 = ((MetaId, VerboseLevel) -> (MetaId, VerboseLevel))
-> [(MetaId, VerboseLevel)] -> [(MetaId, VerboseLevel)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
List.nubOn (MetaId, VerboseLevel) -> (MetaId, VerboseLevel)
forall a. a -> a
id ([(MetaId, VerboseLevel)] -> [(MetaId, VerboseLevel)])
-> [(MetaId, VerboseLevel)] -> [(MetaId, VerboseLevel)]
forall a b. (a -> b) -> a -> b
$ ((MetaId, [VerboseLevel]) -> (MetaId, VerboseLevel))
-> [(MetaId, [VerboseLevel])] -> [(MetaId, VerboseLevel)]
forall a b. (a -> b) -> [a] -> [b]
map (([VerboseLevel] -> VerboseLevel)
-> (MetaId, [VerboseLevel]) -> (MetaId, VerboseLevel)
forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd [VerboseLevel] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length) ([(MetaId, [VerboseLevel])] -> [(MetaId, VerboseLevel)])
-> [(MetaId, [VerboseLevel])] -> [(MetaId, VerboseLevel)]
forall a b. (a -> b) -> a -> b
$ (OldSizeConstraint -> [(MetaId, [VerboseLevel])])
-> [OldSizeConstraint] -> [(MetaId, [VerboseLevel])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap OldSizeConstraint -> [(MetaId, [VerboseLevel])]
flexibleVariables [OldSizeConstraint]
cs
metas1 :: [(MetaId, Int)]
metas1 :: [(MetaId, VerboseLevel)]
metas1 = [(MetaId, Type, Telescope)]
-> ((MetaId, Type, Telescope) -> Maybe (MetaId, VerboseLevel))
-> [(MetaId, VerboseLevel)]
forall a b. [a] -> (a -> Maybe b) -> [b]
forMaybe [(MetaId, Type, Telescope)]
ms (((MetaId, Type, Telescope) -> Maybe (MetaId, VerboseLevel))
-> [(MetaId, VerboseLevel)])
-> ((MetaId, Type, Telescope) -> Maybe (MetaId, VerboseLevel))
-> [(MetaId, VerboseLevel)]
forall a b. (a -> b) -> a -> b
$ \ (m :: MetaId
m, _, tel :: Telescope
tel) ->
Maybe (MetaId, VerboseLevel)
-> (VerboseLevel -> Maybe (MetaId, VerboseLevel))
-> Maybe VerboseLevel
-> Maybe (MetaId, VerboseLevel)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((MetaId, VerboseLevel) -> Maybe (MetaId, VerboseLevel)
forall a. a -> Maybe a
Just (MetaId
m, Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
tel)) (Maybe (MetaId, VerboseLevel)
-> VerboseLevel -> Maybe (MetaId, VerboseLevel)
forall a b. a -> b -> a
const Maybe (MetaId, VerboseLevel)
forall a. Maybe a
Nothing) (Maybe VerboseLevel -> Maybe (MetaId, VerboseLevel))
-> Maybe VerboseLevel -> Maybe (MetaId, VerboseLevel)
forall a b. (a -> b) -> a -> b
$
MetaId -> [(MetaId, VerboseLevel)] -> Maybe VerboseLevel
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
m [(MetaId, VerboseLevel)]
metas0
metas :: [(MetaId, VerboseLevel)]
metas = [(MetaId, VerboseLevel)]
metas0 [(MetaId, VerboseLevel)]
-> [(MetaId, VerboseLevel)] -> [(MetaId, VerboseLevel)]
forall a. [a] -> [a] -> [a]
++ [(MetaId, VerboseLevel)]
metas1
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.solve" 15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Metas: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [(MetaId, VerboseLevel)] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [(MetaId, VerboseLevel)]
metas0 VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ", " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [(MetaId, VerboseLevel)] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [(MetaId, VerboseLevel)]
metas1
VerboseKey -> VerboseLevel -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> m () -> m ()
verboseS "tc.size.solve" 20 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
[(MetaId, VerboseLevel)]
-> ((MetaId, VerboseLevel) -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(MetaId, VerboseLevel)]
metas (((MetaId, VerboseLevel) -> TCM ()) -> TCM ())
-> ((MetaId, VerboseLevel) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (m :: MetaId
m, _) ->
VerboseKey -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size.solve" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Judgement MetaId -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Judgement MetaId -> TCM Doc)
-> TCMT IO (Judgement MetaId) -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaVariable -> Judgement MetaId
mvJudgement (MetaVariable -> Judgement MetaId)
-> TCMT IO MetaVariable -> TCMT IO (Judgement MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ([(MetaId, VerboseLevel)] -> [OldSizeConstraint] -> TCMT IO Bool
oldSolver [(MetaId, VerboseLevel)]
metas [OldSizeConstraint]
cs) TCM ()
forall b. TCMT IO b
cannotSolve
(TCM () -> (TCErr -> TCM ()) -> TCM ())
-> (TCErr -> TCM ()) -> TCM () -> TCM ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip TCM () -> (TCErr -> TCM ()) -> TCM ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError (TCM () -> TCErr -> TCM ()
forall a b. a -> b -> a
const TCM ()
forall b. TCMT IO b
cannotSolve) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
[Closure Constraint] -> (Closure Constraint -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Closure Constraint]
cs0 ((Closure Constraint -> TCM ()) -> TCM ())
-> (Closure Constraint -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ cl :: Closure Constraint
cl -> Closure Constraint -> (Constraint -> TCM ()) -> TCM ()
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Constraint
cl Constraint -> TCM ()
forall (m :: * -> *). MonadConstraint m => Constraint -> m ()
solveConstraint
oldSolver
:: [(MetaId, Int)]
-> [OldSizeConstraint]
-> TCM Bool
oldSolver :: [(MetaId, VerboseLevel)] -> [OldSizeConstraint] -> TCMT IO Bool
oldSolver metas :: [(MetaId, VerboseLevel)]
metas cs :: [OldSizeConstraint]
cs = do
let cannotSolve :: TCMT IO Bool
cannotSolve = Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
mkFlex :: (a, a) -> Constraint
mkFlex (m :: a
m, ar :: a
ar) = VerboseLevel -> (VerboseLevel -> Bool) -> Constraint
W.NewFlex (a -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
m) ((VerboseLevel -> Bool) -> Constraint)
-> (VerboseLevel -> Bool) -> Constraint
forall a b. (a -> b) -> a -> b
$ \ i :: VerboseLevel
i -> VerboseLevel -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral VerboseLevel
i a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
ar
mkConstr :: OldSizeConstraint -> Constraint
mkConstr (Leq a :: OldSizeExpr
a n :: VerboseLevel
n b :: OldSizeExpr
b) = Node -> VerboseLevel -> Node -> Constraint
W.Arc (OldSizeExpr -> Node
mkNode OldSizeExpr
a) VerboseLevel
n (OldSizeExpr -> Node
mkNode OldSizeExpr
b)
mkNode :: OldSizeExpr -> Node
mkNode (Rigid i :: VerboseLevel
i) = Rigid -> Node
W.Rigid (Rigid -> Node) -> Rigid -> Node
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Rigid
W.RVar VerboseLevel
i
mkNode (SizeMeta m :: MetaId
m _) = VerboseLevel -> Node
W.Flex (VerboseLevel -> Node) -> VerboseLevel -> Node
forall a b. (a -> b) -> a -> b
$ MetaId -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral MetaId
m
case Constraints -> Maybe Solution
W.solve (Constraints -> Maybe Solution) -> Constraints -> Maybe Solution
forall a b. (a -> b) -> a -> b
$ ((MetaId, VerboseLevel) -> Constraint)
-> [(MetaId, VerboseLevel)] -> Constraints
forall a b. (a -> b) -> [a] -> [b]
map (MetaId, VerboseLevel) -> Constraint
forall a a. (Integral a, Num a, Ord a) => (a, a) -> Constraint
mkFlex [(MetaId, VerboseLevel)]
metas Constraints -> Constraints -> Constraints
forall a. [a] -> [a] -> [a]
++ (OldSizeConstraint -> Constraint)
-> [OldSizeConstraint] -> Constraints
forall a b. (a -> b) -> [a] -> [b]
map OldSizeConstraint -> Constraint
mkConstr [OldSizeConstraint]
cs of
Nothing -> TCMT IO Bool
cannotSolve
Just sol :: Solution
sol -> do
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "tc.size.solve" 10 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Solved constraints: " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Solution -> VerboseKey
forall a. Show a => a -> VerboseKey
show Solution
sol
Term
suc <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
Term
infty <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
let plus :: Term -> t -> Term
plus v :: Term
v 0 = Term
v
plus v :: Term
v n :: t
n = Term
suc Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term -> t -> Term
plus Term
v (t
n t -> t -> t
forall a. Num a => a -> a -> a
- 1)
inst :: (a, SizeExpr) -> m ()
inst (i :: a
i, e :: SizeExpr
e) = do
let m :: MetaId
m = a -> MetaId
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
i
ar :: VerboseLevel
ar = VerboseLevel -> Maybe VerboseLevel -> VerboseLevel
forall a. a -> Maybe a -> a
fromMaybe VerboseLevel
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe VerboseLevel -> VerboseLevel)
-> Maybe VerboseLevel -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ MetaId -> [(MetaId, VerboseLevel)] -> Maybe VerboseLevel
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup MetaId
m [(MetaId, VerboseLevel)]
metas
term :: SizeExpr -> Term
term (W.SizeConst W.Infinite) = Term
infty
term (W.SizeVar j :: VerboseLevel
j n :: VerboseLevel
n) | VerboseLevel
j VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
ar = Term -> VerboseLevel -> Term
forall t. (Eq t, Num t) => Term -> t -> Term
plus (VerboseLevel -> Term
var (VerboseLevel -> Term) -> VerboseLevel -> Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel
ar VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
j VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 1) VerboseLevel
n
term _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
tel :: [Arg VerboseKey]
tel = VerboseLevel -> Arg VerboseKey -> [Arg VerboseKey]
forall a. VerboseLevel -> a -> [a]
replicate VerboseLevel
ar (Arg VerboseKey -> [Arg VerboseKey])
-> Arg VerboseKey -> [Arg VerboseKey]
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Arg VerboseKey
forall a. a -> Arg a
defaultArg "s"
v :: Term
v = SizeExpr -> Term
term SizeExpr
e
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "tc.size.solve" 20 (TCM Doc -> m ()) -> TCM Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
[ MetaId -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty MetaId
m TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ":="
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
]
let isInf :: SizeExpr -> Bool
isInf (W.SizeConst W.Infinite) = Bool
True
isInf _ = Bool
False
m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (((SizeExpr -> Bool
isInf SizeExpr
e Bool -> Bool -> Bool
&&) (Bool -> Bool)
-> (Maybe InteractionId -> Bool) -> Maybe InteractionId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe InteractionId -> Bool
forall a. Maybe a -> Bool
isJust (Maybe InteractionId -> Bool) -> m (Maybe InteractionId) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
m) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` MetaId -> m Bool
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
MetaId -> [Arg VerboseKey] -> Term -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg VerboseKey] -> Term -> m ()
assignTerm MetaId
m [Arg VerboseKey]
tel Term
v
((VerboseLevel, SizeExpr) -> TCM ())
-> [(VerboseLevel, SizeExpr)] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (VerboseLevel, SizeExpr) -> TCM ()
forall (m :: * -> *) a.
(MonadMetaSolver m, Integral a) =>
(a, SizeExpr) -> m ()
inst ([(VerboseLevel, SizeExpr)] -> TCM ())
-> [(VerboseLevel, SizeExpr)] -> TCM ()
forall a b. (a -> b) -> a -> b
$ Solution -> [(VerboseLevel, SizeExpr)]
forall k a. Map k a -> [(k, a)]
Map.toList Solution
sol
Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True