{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Level.Solve where

import Control.Monad.Except ( catchError )

import qualified Data.Map.Strict as MapS
import Data.Maybe

import Agda.Interaction.Options

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

import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars.Mention
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope

import Agda.Utils.Functor
import Agda.Utils.Monad

-- | Run the given action.
--   If @--cumulativity@ is off, that's it.
--
--   Otherwise, at the end, take all new metavariables of
--   type level for which the only constraints are upper bounds on the
--   level, and instantiate them to the lowest level.
defaultOpenLevelsToZero :: (PureTCM m, MonadMetaSolver m) => m a -> m a
defaultOpenLevelsToZero :: forall (m :: * -> *) a.
(PureTCM m, MonadMetaSolver m) =>
m a -> m a
defaultOpenLevelsToZero m a
f = m Bool -> m a -> m a -> m a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> m PragmaOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) m a
f (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ do
  (result, newMetas) <- m a -> m (a, LocalMetaStores)
forall (m :: * -> *) a.
ReadTCState m =>
m a -> m (a, LocalMetaStores)
metasCreatedBy m a
f
  defaultLevelsToZero (openMetas newMetas)
  return result

defaultLevelsToZero ::
  forall m. (PureTCM m, MonadMetaSolver m) => LocalMetaStore -> m ()
defaultLevelsToZero :: forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
LocalMetaStore -> m ()
defaultLevelsToZero LocalMetaStore
xs = [MetaId] -> m ()
loop ([MetaId] -> m ()) -> m [MetaId] -> m ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [MetaId] -> m [MetaId]
openLevelMetas (LocalMetaStore -> [MetaId]
forall k a. Map k a -> [k]
MapS.keys LocalMetaStore
xs)
  where
    loop :: [MetaId] -> m ()
    loop :: [MetaId] -> m ()
loop [MetaId]
xs = do
      let isOpen :: MetaId -> f Bool
isOpen MetaId
x = MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool) -> f MetaInstantiation -> f Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> f MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
      xs <- (MetaId -> m Bool) -> [MetaId] -> m [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> m Bool
forall {f :: * -> *}. ReadTCState f => MetaId -> f Bool
isOpen [MetaId]
xs
      allMetaTypes <- getOpenMetas >>= traverse metaType
      let notInTypeOfMeta MetaId
x = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ MetaId -> [Type] -> Bool
forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x [Type]
allMetaTypes
      progress <- forM xs $ \MetaId
x -> do
        cs <- (ProblemConstraint -> Bool)
-> [ProblemConstraint] -> [ProblemConstraint]
forall a. (a -> Bool) -> [a] -> [a]
filter (MetaId -> ProblemConstraint -> Bool
forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x) ([ProblemConstraint] -> [ProblemConstraint])
-> m [ProblemConstraint] -> m [ProblemConstraint]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAllConstraints
        if | notInTypeOfMeta x , all (`isUpperBoundFor` x) cs -> do
               m <- lookupMeta x
               TelV tel t <- telView =<< metaType x
               addContext tel $ assignV DirEq x (teleArgs tel) (Level $ ClosedLevel 0) (AsTermsOf t)
               return True
             `catchError` \TCErr
_ -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
           | otherwise -> return False

      when (or progress) $ (loop xs)

    openLevelMetas :: [MetaId] -> m [MetaId]
    openLevelMetas :: [MetaId] -> m [MetaId]
openLevelMetas [MetaId]
xs = (MetaId -> m Bool) -> [MetaId] -> m [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Maybe InteractionId -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe InteractionId -> Bool)
-> (MetaId -> m (Maybe InteractionId)) -> MetaId -> m Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> m (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta) [MetaId]
xs
      m [MetaId] -> ([MetaId] -> m [MetaId]) -> m [MetaId]
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (MetaId -> m Bool) -> [MetaId] -> m [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((DoGeneralize -> Bool) -> m DoGeneralize -> m Bool
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DoGeneralize -> DoGeneralize -> Bool
forall a. Eq a => a -> a -> Bool
== DoGeneralize
NoGeneralize) (m DoGeneralize -> m Bool)
-> (MetaId -> m DoGeneralize) -> MetaId -> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaId -> m DoGeneralize
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m DoGeneralize
isGeneralizableMeta)
      m [MetaId] -> ([MetaId] -> m [MetaId]) -> m [MetaId]
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (MetaId -> m Bool) -> [MetaId] -> m [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> m Bool
isLevelMeta

    isLevelMeta :: MetaId -> m Bool
    isLevelMeta :: MetaId -> m Bool
isLevelMeta MetaId
x = do
      TelV tel t <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> m (TelV Type)) -> m Type -> m (TelV Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
      addContext tel $ isLevelType t

    isUpperBoundFor :: ProblemConstraint -> MetaId -> Bool
    isUpperBoundFor :: ProblemConstraint -> MetaId -> Bool
isUpperBoundFor ProblemConstraint
c MetaId
x = case Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) of
      LevelCmp Comparison
CmpLeq Level
l Level
u -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ MetaId -> Level -> Bool
forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
x Level
u
      Constraint
_                   -> Bool
False