{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Mikan.TypeChecking.MetaVars where

import Prelude hiding (null)

import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )
import Control.Monad.Trans.Maybe

import Data.IntMap qualified as IntMap
import Data.List qualified as List
import Data.Map.Strict qualified as MapS
import Data.Set qualified as Set
import Data.Foldable qualified as Fold
import Data.Traversable qualified as Trav
import Data.Text.Short qualified as TS

import Mikan.Interaction.Options

import Mikan.Syntax.Abstract.Name as A
import Mikan.Syntax.Common
import Mikan.Syntax.Info ( MetaKind( InstanceMeta, UnificationMeta ), MetaNameSuggestion)
import Mikan.Syntax.Info qualified as A
import Mikan.Syntax.Internal
import Mikan.Syntax.Internal.Generic
import Mikan.Syntax.Internal.MetaVars
import Mikan.Syntax.Position (getRange, killRange)

import Mikan.TypeChecking.Monad
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Sort
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.Constraints
import Mikan.TypeChecking.Free
import Mikan.TypeChecking.Level (levelType)
import Mikan.TypeChecking.Records
import Mikan.TypeChecking.Pretty
import Mikan.TypeChecking.Opacity (canSolveMetaOpaquely)
import Mikan.TypeChecking.EtaContract
import Mikan.TypeChecking.Conversion.Errors
import {-# SOURCE #-} Mikan.TypeChecking.CheckInternal
import {-# SOURCE #-} Mikan.TypeChecking.Conversion

import Mikan.TypeChecking.MetaVars.Occurs

import Mikan.Utils.BiMap qualified as BiMap
import Mikan.Utils.Function
import Mikan.Utils.List
import Mikan.Utils.List1 (List1, pattern (:|))
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Size
import Mikan.Utils.Tuple
import Mikan.Utils.Permutation
import Mikan.Syntax.Common.Pretty (Pretty, prettyShow, render)
import Mikan.Interaction.Options.ProfileOptions qualified as Profile
import Mikan.Utils.Singleton
import Mikan.Utils.Graph.TopSort qualified as Graph
import Mikan.Utils.VarSet (VarSet)
import Mikan.Utils.VarSet qualified as VarSet

import Mikan.Utils.Impossible

instance MonadMetaSolver TCM where
  newMeta' :: forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMeta' MetaInstantiation
inst Frozen
frozen MetaInfo
mi MetaPriority
p Permutation
perm Judgement a
j = TCM MetaId -> TCM MetaId -> TCM MetaId
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
forall a.
MetaInstantiation
-> Frozen
-> MetaInfo
-> MetaPriority
-> Permutation
-> Judgement a
-> TCM MetaId
newMetaTCM' MetaInstantiation
inst Frozen
frozen MetaInfo
mi MetaPriority
p Permutation
perm Judgement a
j) (TCM MetaId -> TCM MetaId) -> TCM MetaId -> TCM MetaId
forall a b. (a -> b) -> a -> b
$
    Blocker -> TCM MetaId
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock -- TODO: does this happen?

  assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assignV CompareDirection
dir MetaId
x Args
args Term
v CompareAs
t = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper CompareDirection
dir MetaId
x ((Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
args) Term
v (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign CompareDirection
dir MetaId
x Args
args Term
v CompareAs
t) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    bv <- Term -> TCMT IO (Maybe Blocker)
forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Term
v
    let blocker = Maybe Blocker
-> (Blocker -> Blocker)
-> (Blocker -> Blocker -> Blocker)
-> Blocker
-> Blocker
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Blocker
bv Blocker -> Blocker
forall a. a -> a
id Blocker -> Blocker -> Blocker
unblockOnEither (Blocker -> Blocker) -> Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
x
    patternViolation blocker

  assignTerm' :: MetaId -> [Arg ShortText] -> Term -> TCM ()
assignTerm' MetaId
m [Arg ShortText]
tel Term
v = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (MetaId -> [Arg ShortText] -> Term -> TCM ()
assignTermTCM' MetaId
m [Arg ShortText]
tel Term
v) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    bv <- Term -> TCMT IO (Maybe Blocker)
forall t (m :: * -> *).
(Reduce t, IsMeta t, MonadReduce m) =>
t -> m (Maybe Blocker)
isBlocked Term
v
    let blocker = Maybe Blocker
-> (Blocker -> Blocker)
-> (Blocker -> Blocker -> Blocker)
-> Blocker
-> Blocker
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Blocker
bv Blocker -> Blocker
forall a. a -> a
id Blocker -> Blocker -> Blocker
unblockOnEither (Blocker -> Blocker) -> Blocker -> Blocker
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
m
    patternViolation blocker

  etaExpandMeta :: [MetaClass] -> MetaId -> TCM ()
etaExpandMeta [MetaClass]
x MetaId
y = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv ([MetaClass] -> MetaId -> TCM ()
etaExpandMetaTCM [MetaClass]
x MetaId
y) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVar MetaId
x MetaVariable -> MetaVariable
y = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM MetaId
x MetaVariable -> MetaVariable
y) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock -- TODO: does this happen?

  {-# INLINE speculateMetas #-}
   -- Right now we roll back the full state when aborting.
   -- TODO: only roll back the metavariables
  speculateMetas :: TCM () -> TCM KeepMetas -> TCM ()
speculateMetas TCM ()
fallback TCM KeepMetas
m = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv
    (do (a, s) <- TCM KeepMetas -> TCM (KeepMetas, TCState)
forall a. TCM a -> TCM (a, TCState)
localTCStateSaving TCM KeepMetas
m
        case a of
          KeepMetas
KeepMetas     -> TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
s
          KeepMetas
RollBackMetas -> TCM ()
fallback)
    (TCM KeepMetas
m TCM KeepMetas -> (KeepMetas -> TCM ()) -> TCM ()
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      KeepMetas
KeepMetas     -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      KeepMetas
RollBackMetas -> TCM ()
fallback)


-- | Find position of a value in a list.
--   Used to change metavar argument indices during assignment.
--
--   @reverse@ is necessary because we are directly abstracting over the list.
--
findIdx :: Eq a => [a] -> a -> Maybe Int
findIdx :: forall a. Eq a => [a] -> a -> Maybe Nat
findIdx [a]
vs a
v = a -> [a] -> Maybe Nat
forall a. Eq a => a -> [a] -> Maybe Nat
List.elemIndex a
v ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
vs)

-- | Does the given local meta-variable have a twin meta-variable?

hasTwinMeta :: MetaId -> TCM Bool
hasTwinMeta :: MetaId -> TCM Bool
hasTwinMeta MetaId
x = do
    m <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
    return $! isJust $ mvTwin m

-- | Check whether a meta variable is a place holder for a blocked term.
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm :: MetaId -> TCM Bool
isBlockedTerm MetaId
x = do
    [Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.blocked" Nat
12 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"is " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
" a blocked term? "
    i <- MetaId -> TCMT IO MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
    let r = case MetaInstantiation
i of
            BlockedConst{}                 -> Bool
True
            PostponedTypeCheckingProblem{} -> Bool
True
            InstV{}                        -> Bool
False
            OpenMeta{}                     -> Bool
False
    reportSLn "tc.meta.blocked" 12 $
      if r then "  yes, because " ++! prettyShow i else "  no"
    return r

isEtaExpandable :: [MetaClass] -> MetaId -> TCM Bool
isEtaExpandable :: [MetaClass] -> MetaId -> TCM Bool
isEtaExpandable [MetaClass]
classes MetaId
x = do
    i <- MetaId -> TCMT IO MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x
    return $! case i of
      OpenMeta MetaKind
UnificationMeta       -> Bool
True
      OpenMeta MetaKind
InstanceMeta          -> MetaClass
Records MetaClass -> [MetaClass] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [MetaClass]
classes
      InstV{}                        -> Bool
False
      BlockedConst{}                 -> Bool
False
      PostponedTypeCheckingProblem{} -> Bool
False

-- * Performing the assignment

-- | Performing the meta variable assignment.
--
--   The instantiation should not be an 'InstV' and the 'MetaId'
--   should point to something 'Open' or a 'BlockedConst'.
--   Further, the meta variable may not be 'Frozen'.
assignTerm :: MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTerm :: MetaId -> [Arg ShortText] -> Term -> TCM ()
assignTerm MetaId
x [Arg ShortText]
tel Term
v = do
     -- verify (new) invariants
    TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> TCM Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    MetaId -> [Arg ShortText] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg ShortText] -> Term -> m ()
assignTerm' MetaId
x [Arg ShortText]
tel Term
v

-- | Skip frozen check.  Used for eta expanding frozen metas.
assignTermTCM' :: MetaId -> [Arg ArgName] -> Term -> TCM ()
assignTermTCM' :: MetaId -> [Arg ShortText] -> Term -> TCM ()
assignTermTCM' MetaId
x [Arg ShortText]
tel Term
v = do
    let dummyFromArg :: Arg ShortText -> Dom' t Type
dummyFromArg (Arg ArgInfo
i ShortText
n) = ArgInfo -> ShortText -> Type -> Dom' t Type
forall a t. ArgInfo -> ShortText -> a -> Dom' t a
defaultNamedArgDom ArgInfo
i ShortText
n Type
HasCallStack => Type
__DUMMY_TYPE__

    [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"assignTerm" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" := " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
        [Dom Type] -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
[Dom Type] -> m a -> m a
addContext (Arg ShortText -> Dom Type
forall {t}. Arg ShortText -> Dom' t Type
dummyFromArg (Arg ShortText -> Dom Type) -> [Arg ShortText] -> [Dom Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg ShortText]
tel) (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v)
      , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList_ ((Arg ShortText -> TCMT IO Doc) -> [Arg ShortText] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (ShortText -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (ShortText -> TCMT IO Doc)
-> (Arg ShortText -> ShortText) -> Arg ShortText -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg ShortText -> ShortText
forall e. Arg e -> e
unArg) [Arg ShortText]
tel)
      ]
     -- verify (new) invariants
    TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCEnv Bool -> TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eAssignMetas) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

    ProfileOption -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => ProfileOption -> m () -> m ()
whenProfile ProfileOption
Profile.Metas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return () {-tickMax "max-open-metas" . (fromIntegral . size) =<< getOpenMetas-}
    HasCallStack => MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
MetaId -> (MetaVariable -> MetaVariable) -> TCM ()
updateMetaVarTCM MetaId
x ((MetaVariable -> MetaVariable) -> TCM ())
-> (MetaVariable -> MetaVariable) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ MetaVariable
mv ->
      MetaVariable
mv { mvInstantiation = InstV $ Instantiation
             { instTel = tel
             , instBody = v
             -- Andreas, 2022-04-28, issue #5875:
             -- Can't killRange the meta-solution, since this will destroy
             -- ranges of termination errors (and potentially other passes
             -- that run on internal syntax)!
             -- , instBody = killRange v
             }
         }

    -- issue agda#8636: we have to wake up constraints that are blocked
    -- on this meta /before/ we can eta-expand metas that this is
    -- blocking, because the well-formedness of constraints blocked on
    -- eta-expansion may depend on the satisfiability of constraints
    -- blocked on this meta
    MetaId -> TCM ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
wakeupConstraints MetaId
x
    MetaId -> TCM ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandListeners MetaId
x

    [Char] -> Nat -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Nat
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"completed assignment of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
x

-- * Creating meta variables.

-- | Create a sort meta that may be instantiated with 'Inf' (Typeω).
newSortMeta :: TCM Sort
newSortMeta :: TCM Sort
newSortMeta = Args -> TCM Sort
forall (m :: * -> *). MonadMetaSolver m => Args -> m Sort
newSortMetaCtx (Args -> TCM Sort) -> TCMT IO Args -> TCM Sort
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs

-- | Create a sort meta that may be instantiated with 'Inf' (Typeω).
newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort
newSortMetaCtx :: forall (m :: * -> *). MonadMetaSolver m => Args -> m Sort
newSortMetaCtx Args
vs = do
    i   <- m MetaInfo
forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
    tel <- getContextTelescope
    let t = Tele (Dom Type) -> Type -> Teletype
teleType Tele (Dom Type)
tel Type
HasCallStack => Type
__DUMMY_TYPE__
    x   <- newMeta Instantiable i normalMetaPriority (idP $ size tel) $ IsSort () t
    reportSDoc "tc.meta.new" 50 $
      "new sort meta" <+> prettyTCM x <+> ":" <+> prettyTCM t
    return $! MetaS x $ map' Apply vs

newTypeMeta' :: Comparison -> Sort -> TCM Type
newTypeMeta' :: Comparison -> Sort -> TCM Type
newTypeMeta' Comparison
cmp Sort
s = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type)
-> ((MetaId, Term) -> Term) -> (MetaId, Term) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId, Term) -> Term
forall a b. (a, b) -> b
snd ((MetaId, Term) -> Type) -> TCMT IO (MetaId, Term) -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
cmp (Sort -> Type
sort Sort
s)

newTypeMeta :: Sort -> TCM Type
newTypeMeta :: Sort -> TCM Type
newTypeMeta = Comparison -> Sort -> TCM Type
newTypeMeta' Comparison
CmpLeq

newTypeMeta_ ::  TCM Type
newTypeMeta_ :: TCM Type
newTypeMeta_  = Comparison -> Sort -> TCM Type
newTypeMeta' Comparison
CmpEq (Sort -> TCM Type) -> TCM Sort -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCM Sort -> TCM Sort
forall (m :: * -> *) a. (MonadTCEnv m, MonadDebug m) => m a -> m a
workOnTypes (TCM Sort -> TCM Sort) -> TCM Sort -> TCM Sort
forall a b. (a -> b) -> a -> b
$ TCM Sort
newSortMeta)
-- TODO: (this could be made work with new uni-poly)
-- Andreas, 2011-04-27: If a type meta gets solved, than we do not have to check
-- that it has a sort.  The sort comes from the solution.
-- newTypeMeta_  = newTypeMeta Inf

newLevelMeta :: TCM Level
newLevelMeta :: TCM Level
newLevelMeta = do
  (x, v) <- RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpEq (Type -> TCMT IO (MetaId, Term))
-> TCM Type -> TCMT IO (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
  return $! case v of
    Level Level
l    -> Level
l
    Term
_          -> Term -> Level
forall t. t -> Level' t
atomicLevel Term
v

-- | @newInstanceMeta s t cands@ creates a new instance metavariable
--   of type the output type of @t@ with name suggestion @s@.
newInstanceMeta :: MetaNameSuggestion -> Type -> TCM (MetaId, Term)
newInstanceMeta :: ShortText -> Type -> TCMT IO (MetaId, Term)
newInstanceMeta ShortText
s Type
t = do
  vs  <- TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
  ctx <- getContextTelescope
  newInstanceMetaCtx s (teleType ctx t) vs

newInstanceMetaCtx :: MetaNameSuggestion -> Teletype -> Args -> TCM (MetaId, Term)
newInstanceMetaCtx :: ShortText -> Teletype -> Args -> TCMT IO (MetaId, Term)
newInstanceMetaCtx ShortText
s Teletype
t Args
vs = do
  [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.new" Nat
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ TCMT IO Doc
"new instance meta:"
    , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Args -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Args -> m Doc
prettyTCM Args
vs TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"|-"
    ]
  -- Andreas, 2017-10-04, issue #2753: no metaOccurs check for instance metas
  i0 <- RunMetaOccursCheck -> TCMT IO MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
DontRunMetaOccursCheck

  let i = MetaInfo
i0 { miNameSuggestion = s }
  TelV tel _ <- teleView t
  let perm = Nat -> Permutation
idP (Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel)

  x <- newMeta' (OpenMeta InstanceMeta) Instantiable i normalMetaPriority perm (HasType () CmpLeq t)
  reportSDoc "tc.meta.new" 50 $ fsep
    [ nest 2 $ pretty x <+> ":" <+> prettyTCM t
    ]
  r <- getMetaRange x
  let c = Range -> MetaId -> Maybe [Candidate] -> Constraint
FindInstance Range
r MetaId
x Maybe [Candidate]
forall a. Maybe a
Nothing
  addAwakeConstraint alwaysUnblock c
  etaExpandMetaSafe x
  return (x, MetaV x $ map' Apply vs)

-- | Create a new value meta with specific dependencies, possibly η-expanding in the process.
newNamedValueMeta :: RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> TCM (MetaId, Term)
newNamedValueMeta :: RunMetaOccursCheck
-> ShortText -> Comparison -> Type -> TCMT IO (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
b ShortText
s Comparison
cmp Type
t = do
  (x, v) <- RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
newValueMeta RunMetaOccursCheck
b Comparison
cmp Type
t
  setMetaNameSuggestion x s
  return (x, v)

-- | Create a new value meta with specific dependencies without η-expanding.
newNamedValueMeta' :: RunMetaOccursCheck -> MetaNameSuggestion -> Comparison -> Type -> TCM (MetaId, Term)
newNamedValueMeta' :: RunMetaOccursCheck
-> ShortText -> Comparison -> Type -> TCMT IO (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
b ShortText
s Comparison
cmp Type
t = do
  (x, v) <- RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
newValueMeta' RunMetaOccursCheck
b Comparison
cmp Type
t
  setMetaNameSuggestion x s
  return (x, v)

newValueMetaOfKind ::
     A.MetaInfo
  -> RunMetaOccursCheck  -- ^ Ignored for instance metas.
  -> Comparison          -- ^ Ignored for instance metas.
  -> Type
  -> TCM (MetaId, Term)
newValueMetaOfKind :: MetaInfo
-> RunMetaOccursCheck
-> Comparison
-> Type
-> TCMT IO (MetaId, Term)
newValueMetaOfKind MetaInfo
info = case MetaInfo -> MetaKind
A.metaKind MetaInfo
info of
  MetaKind
UnificationMeta -> RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
newValueMeta
  MetaKind
InstanceMeta -> \ RunMetaOccursCheck
_run Comparison
_cmp -> ShortText -> Type -> TCMT IO (MetaId, Term)
newInstanceMeta (MetaInfo -> ShortText
A.metaNameSuggestion MetaInfo
info)

-- | Create a new metavariable, possibly η-expanding in the process.
-- See 'newValueMetaCtx''.
newValueMeta :: RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term)
newValueMeta :: RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
newValueMeta RunMetaOccursCheck
b Comparison
cmp Type
t = do
  vs  <- TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
  ctx <- getContextTelescope
  newValueMetaCtx Instantiable b cmp t ctx (idP $ size ctx) vs

-- | Create a new metavariable with a provided thinning,
-- possibly η-expanding in the process. See 'newValueMetaCtx''.
newValueMetaCtx :: Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> TCM (MetaId, Term)
newValueMetaCtx :: Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCMT IO (MetaId, Term)
newValueMetaCtx Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
t Tele (Dom Type)
ctx Permutation
thin Args
vs =
  (Term -> TCMT IO Term) -> (MetaId, Term) -> TCMT IO (MetaId, Term)
forall (m :: * -> *) b d a.
Functor m =>
(b -> m d) -> (a, b) -> m (a, d)
secondM Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ((MetaId, Term) -> TCMT IO (MetaId, Term))
-> TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCMT IO (MetaId, Term)
newValueMetaCtx' Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
t Tele (Dom Type)
ctx Permutation
thin Args
vs

-- | Create a new metavariable without η-expanding.
-- See 'newValueMetaCtx''.
newValueMeta' :: RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term)
newValueMeta' :: RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
newValueMeta' RunMetaOccursCheck
b Comparison
cmp Type
t = do
  vs  <- TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
  ctx <- getContextTelescope
  newValueMetaCtx' Instantiable b cmp t ctx (idP $ size ctx) vs

-- | Create a new metavariable with a provided thinning, without η-expanding.
newValueMetaCtx'
  :: Frozen
  -- ^ Should the new metavariable be frozen?
  -> RunMetaOccursCheck
  -- ^ Allow this meta to appear in its own solution
  -- (for interaction points, generalised variables, and instance metas).
  -> Comparison
  -- ^ Are we checking or infering the type?
  -> Type
  -- ^ The type of the meta, in context @Δ@.
  -> Telescope
  -- ^ Thinned context @Δ@ that the metavariable depends on.
  -> Permutation
  -- ^ Thinning @Γ ⊢ Δ@ to get from the current context to the thinned context.
  -> Args
  -- ^ A substitution @Γ ⊢ Δ@ from the current context to the
  -- thinned context; usually the same as the thinning.
  -> TCM (MetaId, Term)
newValueMetaCtx' :: Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCMT IO (MetaId, Term)
newValueMetaCtx' Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type
a Tele (Dom Type)
ctx Permutation
thin Args
vs = do
  i <- RunMetaOccursCheck -> TCMT IO MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
b
  let t = Tele (Dom Type) -> Type -> Teletype
teleType Tele (Dom Type)
ctx Type
a
  x <- newMeta frozen i normalMetaPriority thin (HasType () cmp t)
  reportSDoc "tc.meta.new" 50 $ fsep
    [ text $ "new meta (" ++! show (i ^. lensIsAbstract) ++! "):"
    , nest 2 $ prettyTCM vs <+> "|-"
    , nest 2 $ pretty x <+> ":" <+> prettyTCM t
    ]
  etaExpandMetaSafe x
  -- Andreas, 2012-09-24: for Metas X : Size< u add constraint X+1 <= u
  let u = MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
vs
  return (x, u)

{-# INLINE newTelMeta #-}
-- | Create a telescope of metavariables @?x0 : A, ?x1 : B ?x0, ?x2 : C ?x0 ?x1, ...@
-- from a telescope @(a : A) (b : B a) (c : C a b) ...@.
newTelMeta :: Telescope -> TCM Args
newTelMeta :: Tele (Dom Type) -> TCMT IO Args
newTelMeta Tele (Dom Type)
tel = do
  vs  <- TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
  ctx <- getContextTelescope
  newTelMetaCtx mempty Instantiable tel ctx (idP $ size ctx) vs

-- | Create a telescope of metavariables @?x0 : A, ?x1 : B ?x0, ?x2 : C ?x0 ?x1, ...@
-- from a telescope @(a : A) (b : B a) (c : C a b) ...@ in the current context while
-- applying a substitution to the telescope of types.
--
-- @newTelMetaSubst tel rho@ is a fused version of @newTelMeta (applySubst rho tel)@.
-- If you do not need to apply a substitution, use 'newTelMeta'.
{-# INLINE newTelMetaSubst #-}
newTelMetaSubst
  :: Telescope
  -- ^ A telescope of types in context @Θ@ to create metas for.
  -> Substitution
  -- ^ A substitution @ρ : Γ ⊢ Θ@ from the current context that will be
  -- applied to all types in the telescope.
  -> TCM Args
newTelMetaSubst :: Tele (Dom Type) -> Substitution -> TCMT IO Args
newTelMetaSubst Tele (Dom Type)
tel Substitution
rho = do
  vs  <- TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
  ctx <- getContextTelescope
  newTelMetaCtxSubst mempty Instantiable tel rho ctx (idP $ size ctx) vs

{-# INLINE newTelMetaCtx #-}
-- | Create a telescope of metavariables @?x0 : A, ?x1 : B ?x0, ?x2 : C ?x0 ?x1, ...@
-- from a telescope @(a : A) (b : B a) (c : C a b) ...@ in the provided
-- context. See 'newTelMetaCtxSubst'.
newTelMetaCtx :: MetaNameSuggestion -> Frozen -> Telescope -> Telescope -> Permutation -> Args -> TCM Args
newTelMetaCtx :: ShortText
-> Frozen
-> Tele (Dom Type)
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCMT IO Args
newTelMetaCtx = \ShortText
pref Frozen
frozen Tele (Dom Type)
tel Tele (Dom Type)
ctx Permutation
thin Args
vs -> ShortText
-> Frozen
-> Tele (Dom Type)
-> Substitution
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCMT IO Args
newTelMetaCtxSubst ShortText
pref Frozen
frozen Tele (Dom Type)
tel Substitution
forall a. Substitution' a
IdS Tele (Dom Type)
ctx Permutation
thin Args
vs

-- | Create a telescope of metavariables @?x0 : A, ?x1 : B ?x0, ?x2 : C ?x0 ?x1, ...@
-- from a telescope @(a : A) (b : B a) (c : C a b) ...@ in the provided
-- context.
--
-- This is a low-level interface to creating telescopes of metas.
-- Most users will probably want to use 'newTelMeta' or 'newTelMetaSubst'.
newTelMetaCtxSubst
  :: MetaNameSuggestion
  -- ^ Name suggestion to be used as a /prefix/ of the name suggestions
  -- for the metas that represent each field.
  -> Frozen
  -- ^ Should the new metavariable be frozen?
  -> Telescope
  -- ^ A telescope of types in context @Θ@ to create metas for.
  -> Substitution
  -- ^ A substitution @ρ : Δ ⊢ Θ@ that will be applied to all types in the telescope.
  -> Telescope
  -- ^ Thinned context @Δ@ that the telescope of metavariables depends on.
  -> Permutation
  -- ^ Thinning @Γ ⊢ Δ@ to get from the current context to the thinned context.
  -> Args
  -- ^ A substitution @Γ ⊢ Δ@ from the current context to the
  -- thinned context; usually the same as the thinning.
  -> TCM Args
newTelMetaCtxSubst :: ShortText
-> Frozen
-> Tele (Dom Type)
-> Substitution
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCMT IO Args
newTelMetaCtxSubst ShortText
pref Frozen
frozen Tele (Dom Type)
EmptyTel Substitution
rho Tele (Dom Type)
ctx Permutation
thin Args
vs = Args -> TCMT IO Args
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
newTelMetaCtxSubst ShortText
pref Frozen
frozen (ExtendTel Dom Type
a Abs (Tele (Dom Type))
tel) Substitution
rho Tele (Dom Type)
ctx Permutation
thin Args
vs = do
  let info :: ArgInfo
info = Dom Type
a Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo
  let aInst :: Type
aInst = Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Type)
rho (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)
  (m, u) <- Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCMT IO (MetaId, Term)
newValueMetaCtx Frozen
frozen RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type
aInst Tele (Dom Type)
ctx Permutation
thin Args
vs
  setMetaNameSuggestion m (suffixNameSuggestion pref (absName tel))
  metas <- newTelMetaCtxSubst pref frozen (unAbs tel) (applyWhen (isAbs tel) (u :#) rho) ctx thin vs
  pure $! Arg info u : metas

-- | Create an element of a record type by
-- applying the constructor to fresh metavariables for each of the fields.
newRecordMeta
  :: QName
  -- ^ Name of the record type.
  -> Args
  -- ^ Record paramaters.
  -> TCM Term
newRecordMeta :: QName -> Args -> TCMT IO Term
newRecordMeta QName
r Args
pars = do
  vs  <- TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
  ctx <- getContextTelescope
  newRecordMetaCtx mempty Instantiable r pars ctx (idP $ size ctx) vs

newRecordMetaCtx
  :: MetaNameSuggestion
  -- ^ Name suggestion to be used as a /prefix/ of the name suggestions
  -- for the metas that represent each field
  -> Frozen
  -- ^ Should the meta be created frozen?
  -> QName
  -- ^ Name of record type
  -> Args
  -- ^ Parameters of record type.
  -> Telescope
  -- ^ Thinned context @Δ@ that the metavariable depends on.
  -> Permutation
  -- ^ Thinning @Γ ⊢ Δ@ to get from the current context to the thinned context.
  -> Args
  -- ^ A substitution @Γ ⊢ Δ@ from the current context to the
  -- thinned context; usually the same as the thinning.
  -> TCM Term
newRecordMetaCtx :: ShortText
-> Frozen
-> QName
-> Args
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCMT IO Term
newRecordMetaCtx ShortText
pref Frozen
frozen QName
r Args
pars Tele (Dom Type)
ctx Permutation
thin Args
vs = do
  rdef   <- QName -> TCMT IO RecordData
forall (m :: * -> *).
(HasCallStack, HasConstInfo m, ReadTCState m,
 MonadError TCErr m) =>
QName -> m RecordData
getRecordDef QName
r
  let con = KillRangeT ConHead
forall a. KillRange a => KillRangeT a
killRange KillRangeT ConHead -> KillRangeT ConHead
forall a b. (a -> b) -> a -> b
$ RecordData -> ConHead
_recConHead RecordData
rdef
  -- Get the record field types as telescope.
  let ftel = Tele (Dom Type) -> Args -> Tele (Dom Type)
forall t. Apply t => t -> Args -> t
apply (RecordData -> Tele (Dom Type)
_recTel RecordData
rdef) Args
pars
  fields <- newTelMetaCtx pref frozen ftel ctx thin vs
  return $! Con con ConOSystem $! map' Apply fields

newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark :: InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
newQuestionMark InteractionId
ii Comparison
cmp = (Comparison -> Type -> TCMT IO (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
newQuestionMark' (RunMetaOccursCheck -> Comparison -> Type -> TCMT IO (MetaId, Term)
newValueMeta' RunMetaOccursCheck
RunMetaOccursCheck) InteractionId
ii Comparison
cmp

-- Since we are type-checking some code twice, e.g., record declarations
-- for the sake of the record constructor type and then again for the sake
-- of the record module (issue #434), we may encounter an interaction point
-- for which we already have a meta.  In this case, we want to reuse the meta.
-- Otherwise we get two meta for one interaction point which are not connected,
-- and e.g. Agda might solve one in some way
-- and the user the other in some other way...
--
-- New reference: Andreas, 2021-07-21, issues #5478 and #5463
-- Old reference: Andreas, 2016-07-29, issue 1720-2
-- See also: issue #2257
newQuestionMark'
  :: (Comparison -> Type -> TCM (MetaId, Term))
  -> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark' :: (Comparison -> Type -> TCMT IO (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCMT IO (MetaId, Term)
newQuestionMark' Comparison -> Type -> TCMT IO (MetaId, Term)
new InteractionId
ii Comparison
cmp Type
t = InteractionId -> TCMT IO (Maybe MetaId)
forall (m :: * -> *).
ReadTCState m =>
InteractionId -> m (Maybe MetaId)
lookupInteractionMeta InteractionId
ii TCMT IO (Maybe MetaId)
-> (Maybe MetaId -> TCMT IO (MetaId, Term))
-> TCMT IO (MetaId, Term)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case

  -- Case: new meta.
  Maybe MetaId
Nothing -> do
    -- Do not run check for recursive occurrence of meta in definitions,
    -- because we want to give the recursive solution interactively (Issue 589)
    (x, m) <- Comparison -> Type -> TCMT IO (MetaId, Term)
new Comparison
cmp Type
t
    connectInteractionPoint ii x
    return (x, m)

  -- Case: existing meta.
  Just MetaId
x -> do
    -- Get the context Γ in which the meta was created.
    MetaVar
      { mvInfo = MetaInfo{ miClosRange = Closure{ clEnv = view eContext -> gamma }}
      , mvPermutation = p
      } <- MetaVariable -> Maybe MetaVariable -> MetaVariable
forall a. a -> Maybe a -> a
fromMaybe MetaVariable
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe MetaVariable -> MetaVariable)
-> TCMT IO (Maybe MetaVariable) -> TCMT IO MetaVariable
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
x

    -- Get the current context Δ.
    delta <- getContext
    -- A bit hazardous:
    -- we base our decisions on the names of the context entries.
    -- Ideally, Agda would organize contexts in ancestry trees
    -- with substitutions to move between parent and child.
    let gxs  = Context -> [Name]
contextNames' Context
gamma
    let dxs  = Context -> [Name]
contextNames' Context
delta
    let gys  = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' Name -> Name
nameCanonical [Name]
gxs
    let dys  = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map' Name -> Name
nameCanonical [Name]
dxs
    let glen = [Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Name]
gxs
    let dlen = [Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Name]
dxs
    reportSDoc "tc.interaction" 20 $ vcat
      [ "reusing meta"
      , nest 2 $ "creation context:" <+> prettyTCM gamma
      -- , nest 2 $ "creation context:" <+> pretty gxs
      , nest 2 $ "reusage  context:" <+> prettyTCM delta
      -- , nest 2 $ "reusage  context:" <+> pretty dxs
      ]

    -- When checking a record declaration (e.g. Σ), creation context Γ
    -- might be of the forms Γ₀,Γ₁ or Γ₀,fst,Γ₁ or Γ₀,fst,snd,Γ₁ whereas
    -- Δ is of the form Γ₀,r,Γ₁,{Δ₂} for record variable r.
    -- So first find the record variable in Δ.
    rev_args <- case List.findIndex nameIsRecordName dxs of

      -- Case: no record variable in the context.
      -- Test whether Δ is an extension of Γ.
      Maybe Nat
Nothing -> do
        Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ([Name]
gys [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf` [Name]
dys) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"expecting meta-creation context"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
            , TCMT IO Doc
"to be a suffix of the meta-reuse context"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
            ]
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"expecting meta-creation context"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([Name] -> [Char]) -> [Name] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> [Char]
forall a. Show a => a -> [Char]
show) [Name]
gxs
            , TCMT IO Doc
"to be a suffix of the meta-reuse context"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> ([Name] -> [Char]) -> [Name] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Name] -> [Char]
forall a. Show a => a -> [Char]
show) [Name]
dxs
            ]
          TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        -- Apply the meta to |Γ| arguments from Δ.
        [Term] -> TCMT IO [Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$! (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Nat -> Term
var [Nat
dlen Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
glen .. Nat
dlen Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]

      -- Case: record variable in the context.
      Just Nat
k -> do
        -- Verify that the contexts relate as expected.
        let g0len :: Nat
g0len = [Name] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Name]
dxs Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
k Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1
        -- Find out the Δ₂ and Γ₁ parts.
        -- However, as they do not share common ancestry, the @nameId@s differ,
        -- so we consider only the original concrete names in gys and dys.
        -- This is a bit risky... blame goes to #434.
        let (Nat
d2len, Nat
g1len) = [Name] -> [Name] -> (Nat, Nat)
forall a. Eq a => [a] -> [a] -> (Nat, Nat)
findOverlap (Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
take' Nat
k [Name]
dys) [Name]
gys
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.interaction" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc -> TCMT IO Doc) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2)
          [ TCMT IO Doc
"k     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Nat -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
k
          , TCMT IO Doc
"glen  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Nat -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
glen
          , TCMT IO Doc
"g0len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Nat -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
g0len
          , TCMT IO Doc
"g1len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Nat -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
g1len
          , TCMT IO Doc
"d2len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Nat -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Nat
d2len
          ]
        -- The Γ₀ part should match.
        Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
drop (Nat
glen Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
g0len) [Name]
gxs [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
drop (Nat
k Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [Name]
dxs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"expecting meta-creation context (with fields instead of record var)"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
            , TCMT IO Doc
"to share ancestry (suffix) with the meta-reuse context (with record var)"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
            ]
          TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        -- The Γ₁ part should match.
        Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless ( ([Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Name] -> [Name] -> Bool)
-> ([Name] -> [Name]) -> [Name] -> [Name] -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
take' Nat
g1len) [Name]
gys (Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
drop Nat
d2len [Name]
dys) ) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
            [ TCMT IO Doc
"expecting meta-creation context (with fields instead of record var)"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
gxs
            , TCMT IO Doc
"to be an expansion of the meta-reuse context (with record var)"
            , Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
            ]
          TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        let ([Term]
vs1, Term
v : [Term]
vs0) = Nat -> [Term] -> ([Term], [Term])
forall a. Nat -> [a] -> ([a], [a])
splitAt' Nat
g1len ([Term] -> ([Term], [Term])) -> [Term] -> ([Term], [Term])
forall a b. (a -> b) -> a -> b
$ (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Nat -> Term
var [Nat
d2len..Nat
dlenNat -> Nat -> Nat
forall a. Num a => a -> a -> a
-Nat
1]
        -- We need to expand the record var @v@ into the correct number of fields.
        let numFields :: Nat
numFields = Nat
glen Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
g1len Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
g0len
        if Nat
numFields Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
0 then [Term] -> TCMT IO [Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$! [Term]
vs1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++! [Term]
vs0 else do
          -- Get the record type.
          let t :: Type
t = Dom Type -> Type
forall t e. Dom' t e -> e
unDom (Dom Type -> Type) -> Dom Type -> Type
forall a b. (a -> b) -> a -> b
$ ContextEntry -> Dom Type
ctxEntryDom (ContextEntry -> Dom Type) -> ContextEntry -> Dom Type
forall a b. (a -> b) -> a -> b
$ ContextEntry -> Maybe ContextEntry -> ContextEntry
forall a. a -> Maybe a -> a
fromMaybe ContextEntry
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ContextEntry -> ContextEntry)
-> Maybe ContextEntry -> ContextEntry
forall a b. (a -> b) -> a -> b
$
                  Nat -> Context -> Maybe ContextEntry
cxLookup Nat
k Context
delta
          -- Get the record field names.
          fs <- [Dom QName] -> [Dom QName]
forall a. [a] -> [a]
reverse ([Dom QName] -> [Dom QName])
-> ([Dom QName] -> [Dom QName]) -> [Dom QName] -> [Dom QName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [Dom QName] -> [Dom QName]
forall a. Nat -> [a] -> [a]
take' Nat
numFields ([Dom QName] -> [Dom QName])
-> TCMT IO [Dom QName] -> TCMT IO [Dom QName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack => Type -> TCMT IO [Dom QName]
Type -> TCMT IO [Dom QName]
getRecordTypeFields Type
t
          -- Check that the record field names match
          -- the supposed record field names from the context of the original meta.
          let gfs = Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
take' Nat
numFields (Nat -> [Name] -> [Name]
forall a. Nat -> [a] -> [a]
drop Nat
g1len [Name]
gxs)
          reportSDoc "tc.interaction" 30 $ vcat $ map' (nest 2)
            [ "fs    =" <+> pretty fs
            , "gfs   =" <+> pretty gfs
            ]
          -- NameIds do not match, so we have to revert to the concrete name.
          -- unless (gfs == map' (qnameName . unDom) fs) __IMPOSSIBLE__
          unless (((==) `on` map' nameCanonical) gfs (map' (qnameName . unDom) fs)) __IMPOSSIBLE__
          -- Field arguments to the original meta are projections from the record var.
          let vfs = (Dom QName -> Term) -> [Dom QName] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' ((\ QName
x -> Term
v Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
x]) (QName -> Term) -> (Dom QName -> QName) -> Dom QName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom QName -> QName
forall t e. Dom' t e -> e
unDom) [Dom QName]
fs
          -- These are the final args to the original meta:
          return $! vs1 ++! vfs ++! vs0

    -- Use ArgInfo from Γ.
    let args = (Term -> Arg Term -> Arg Term) -> [Term] -> Args -> Args
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' Term -> Arg Term -> Arg Term
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
(<$) ([Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
rev_args) (Args -> Args) -> Args -> Args
forall a b. (a -> b) -> a -> b
$ Context -> Args
contextArgs Context
gamma
    -- Take the permutation into account (see TC.Monad.MetaVars.getMetaContextArgs).
    let vs = Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute (Nat -> Permutation -> Permutation
takeP (Args -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args) Permutation
p) Args
args
    reportSDoc "tc.interaction" 20 $ vcat
      [ "meta reuse arguments:" <+> prettyTCM vs ]
    return (x, MetaV x $ map' Apply vs)

-- | Construct a blocked constant if there are constraints.
blockTerm :: Type -> TCM Term -> TCM Term
blockTerm :: Type -> TCMT IO Term -> TCMT IO Term
blockTerm Type
t TCMT IO Term
blocker = do
  (pid, v) <- TCMT IO Term -> TCMT IO (ProblemId, Term)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem TCMT IO Term
blocker
  blockTermOnProblem t v pid

blockTermOnProblem :: Type -> Term -> ProblemId -> TCM Term
blockTermOnProblem :: Type -> Term -> ProblemId -> TCMT IO Term
blockTermOnProblem Type
t Term
v ProblemId
pid = do
  -- Andreas, 2012-09-27 do not block on unsolved size constraints
  solved <- ProblemId -> TCM Bool
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
ProblemId -> m Bool
isProblemSolved ProblemId
pid
  ifM (return solved)
      (v <$ reportSLn "tc.meta.blocked" 20 ("Not blocking because " ++! show pid ++! " is " ++
                                            if solved then "solved" else "a size problem")) $ do
    i   <- createMetaInfo
    es  <- map' Apply <$> getContextArgs
    tel <- getContextTelescope
    x   <- newMeta' (BlockedConst $ abstract tel v)
      Instantiable i lowMetaPriority
      (idP $ size tel)
      (HasType () CmpLeq $ teleType tel t)
      -- we don't instantiate blocked terms

    inTopContext $ addConstraint (unblockOnProblem pid) (UnBlock x)
    reportSDoc "tc.meta.blocked" 20 $ vcat
      [ "blocked" <+> prettyTCM x <+> ":=" <+> inTopContext
        (prettyTCM $ abstract tel v)
      , "     by" <+> (prettyTCM =<< getConstraintsForProblem pid)
      ]
    inst <- isInstantiatedMeta x
    if inst
      then instantiate (MetaV x es)
      else do
        -- We don't return the blocked term instead create a fresh metavariable
        -- that we compare against the blocked term once it's unblocked. This way
        -- blocked terms can be instantiated before they are unblocked, thus making
        -- constraint solving a bit more robust against instantiation order.
        -- Andreas, 2015-05-22: DontRunMetaOccursCheck to avoid Issue585-17.
        (m', v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t
        reportSDoc "tc.meta.blocked" 30
          $   "setting twin of"
          <+> prettyTCM m'
          <+> "to be"
          <+> prettyTCM x
        updateMetaVar m' (\MetaVariable
mv -> MetaVariable
mv { mvTwin = Just x })
        i   <- fresh
        -- This constraint is woken up when unblocking, so it doesn't need a problem id.
        cmp <- buildProblemConstraint_ (unblockOnMeta x) (ValueCmp CmpEq (AsTermsOf t) v (MetaV x es))
        reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp
        listenToMeta (CheckConstraint i cmp) x
        return v

blockTypeOnProblem :: Type -> ProblemId -> TCM Type
blockTypeOnProblem :: Type -> ProblemId -> TCM Type
blockTypeOnProblem (El Sort
s Term
a) ProblemId
pid = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Term -> ProblemId -> TCMT IO Term
blockTermOnProblem (Sort -> Type
sort Sort
s) Term
a ProblemId
pid

-- | @unblockedTester t@ returns a 'Blocker' for @t@.
--
--   Auxiliary function used when creating a postponed type checking problem.
unblockedTester :: Type -> TCM Blocker
unblockedTester :: Type -> TCM Blocker
unblockedTester Type
t = Type
-> (Blocker -> Type -> TCM Blocker)
-> (NotBlocked -> Type -> TCM Blocker)
-> TCM Blocker
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
b Type
_ -> Blocker -> TCM Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
b) (\ NotBlocked
_ Type
_ -> Blocker -> TCM Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock)

-- | Create a postponed type checking problem @e : t@ that waits for type @t@
--   to unblock (become instantiated or its constraints resolved).
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ :: TypeCheckingProblem -> TCMT IO Term
postponeTypeCheckingProblem_ TypeCheckingProblem
p = TypeCheckingProblem -> Blocker -> TCMT IO Term
postponeTypeCheckingProblem TypeCheckingProblem
p (Blocker -> TCMT IO Term) -> TCM Blocker -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypeCheckingProblem -> TCM Blocker
unblock TypeCheckingProblem
p where
  unblock :: TypeCheckingProblem -> TCM Blocker
unblock (CheckWithApp Comparison
_ Type
_ WithAppHead
_ QName
_ Elims
_ List1 Expr
_)    = TCM Blocker
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Used with explicit blocker only.
  unblock (CheckWithAppHead Comparison
_ Type
_ Expr
_ Term
_ List1 Expr
_)  = TCM Blocker
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Used with explicit blocker only.
  unblock (DoQuoteTerm Comparison
_ Term
_ Type
_)           = TCM Blocker
forall a. HasCallStack => a
__IMPOSSIBLE__ -- also quoteTerm problems
  unblock (DisambiguateConstructor ConstructorDisambiguationData
_ ConHead -> TCMT IO Term
_) = TCM Blocker
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Used with explicit blocker only.
  unblock (CheckExpr Comparison
_ Expr
_ Type
t)             = Type -> TCM Blocker
unblockedTester Type
t
  unblock (CheckArgs Comparison
_ ExpandHidden
_ Expr
_ [NamedArg Expr]
_ Type
t Type
_ ArgsCheckState CheckedTarget -> TCMT IO Term
_)     = Type -> TCM Blocker
unblockedTester Type
t  -- The type of the head of the application.
  unblock (CheckProjAppToKnownPrincipalArg Comparison
_ Expr
_ ProjOrigin
_ AmbiguousQName
_ Expr
_ [NamedArg Expr]
_ Type
_ Nat
_ Term
_ Type
t PrincipalArgTypeMetas
_) = Type -> TCM Blocker
unblockedTester Type
t -- The type of the principal argument

-- | Create a postponed type checking problem @e : t@ that waits for conditon
--   @unblock@.  A new meta is created in the current context that has as
--   instantiation the postponed type checking problem.  An 'UnBlock' constraint
--   is added for this meta, which links to this meta.
postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem :: TypeCheckingProblem -> Blocker -> TCMT IO Term
postponeTypeCheckingProblem TypeCheckingProblem
p Blocker
unblock | Blocker
unblock Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
== Blocker
alwaysUnblock = do
  [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Nat
2 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Postponed without blocker:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> TypeCheckingProblem -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeCheckingProblem -> m Doc
prettyTCM TypeCheckingProblem
p
  TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
postponeTypeCheckingProblem TypeCheckingProblem
p Blocker
unblock = do
  i   <- RunMetaOccursCheck -> TCMT IO MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
DontRunMetaOccursCheck
  tel <- getContextTelescope
  cl  <- buildClosure p
  let
    t = TypeCheckingProblem -> Type
problemType TypeCheckingProblem
p
    !tt = Tele (Dom Type) -> Type -> Teletype
teleType Tele (Dom Type)
tel Type
t
  m   <- newMeta' (PostponedTypeCheckingProblem cl)
                  Instantiable i normalMetaPriority (idP (size tel))
         $ HasType () CmpLeq tt
  reportSDoc "tc.meta.postponed" 20 $ vcat
    [ "new meta" <+> inTopContext (prettyTCM m) <+>
      ":" <+> inTopContext (prettyTCM $ telePi_ tel t)
    , "for postponed typechecking problem" <+> prettyTCM p
    ]

  -- Create the meta that we actually return
  -- Andreas, 2012-03-15
  -- This is an alias to the pptc meta, in order to allow pruning (issue 468)
  -- and instantiation.
  -- Since this meta's solution comes from user code, we do not need
  -- to run the extended occurs check (metaOccurs) to exclude
  -- non-terminating solutions.
  es  <- map' Apply <$> getContextArgs
  (_, v) <- newValueMeta DontRunMetaOccursCheck CmpLeq t
  cmp <- buildProblemConstraint_ (unblockOnMeta m) (ValueCmp CmpEq (AsTermsOf t) v (MetaV m es))
  reportSDoc "tc.constr.add" 20 $ "adding constraint" <+> prettyTCM cmp
  i   <- liftTCM fresh
  listenToMeta (CheckConstraint i cmp) m
  addConstraint unblock (UnBlock m)
  return v

-- | Type of the term that is produced by solving the 'TypeCheckingProblem'.
problemType :: TypeCheckingProblem -> Type
problemType :: TypeCheckingProblem -> Type
problemType (CheckExpr Comparison
_ Expr
_ Type
t         ) = Type
t
problemType (CheckArgs Comparison
_ ExpandHidden
_ Expr
_ [NamedArg Expr]
_ Type
_ Type
t ArgsCheckState CheckedTarget -> TCMT IO Term
_ ) = Type
t  -- The target type of the application.
problemType (CheckProjAppToKnownPrincipalArg Comparison
_ Expr
_ ProjOrigin
_ AmbiguousQName
_ Expr
_ [NamedArg Expr]
_ Type
t Nat
_ Term
_ Type
_ PrincipalArgTypeMetas
_) = Type
t -- The target type of the application
problemType (DoQuoteTerm Comparison
_ Term
_ Type
t)        = Type
t
problemType (DisambiguateConstructor (ConstructorDisambiguationData QName
_ List1 (QName, Type, ConHead)
_ [NamedArg Expr]
_ Type
t) ConHead -> TCMT IO Term
_) = Type
t
problemType (CheckWithApp Comparison
_ Type
t WithAppHead
_ QName
_ Elims
_ List1 Expr
_ )   = Type
t
problemType (CheckWithAppHead Comparison
_ Type
t Expr
_ Term
_ List1 Expr
_ ) = Type
t

-- | Eta-expand a local meta-variable, if it is of the specified kind.
--   Don't do anything if the meta-variable is a blocked term.
etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM ()
etaExpandMetaTCM :: [MetaClass] -> MetaId -> TCM ()
etaExpandMetaTCM [MetaClass]
kinds MetaId
m =
 TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM ((Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCM Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
m) TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` Lens' TCEnv Bool -> TCM Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eAssignMetas TCM Bool -> TCM Bool -> TCM Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M` [MetaClass] -> MetaId -> TCM Bool
isEtaExpandable [MetaClass]
kinds MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> Nat -> [Char] -> TCM () -> TCM ()
forall a. [Char] -> Nat -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Nat -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.meta.eta" Nat
20 ([Char]
"etaExpandMeta " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! MetaId -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow MetaId
m) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    let waitFor :: Blocker -> TCM ()
waitFor Blocker
b = do
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
            TCMT IO Doc
"postponing eta-expansion of meta variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              TCMT IO Doc
"which is blocked by" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM Blocker
b
          (MetaId -> TCM ()) -> Set MetaId -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Listener -> MetaId -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
Listener -> MetaId -> m ()
listenToMeta (MetaId -> Listener
EtaExpand MetaId
m)) (Set MetaId -> TCM ()) -> Set MetaId -> TCM ()
forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
b
        dontExpand :: TCM ()
dontExpand = do
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
            TCMT IO Doc
"we do not expand meta variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
              [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"(requested was expansion of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [MetaClass] -> [Char]
forall a. Show a => a -> [Char]
show [MetaClass]
kinds [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! [Char]
")")
    meta <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
    case mvJudgement meta of
      IsSort{} -> TCM ()
dontExpand
      HasType MetaId
_ Comparison
cmp Teletype
a -> do

        [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"considering eta-expansion at type "
          , Teletype -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Teletype -> m Doc
prettyTCM Teletype
a
          , [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
" raw: "
          , Teletype -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Teletype
a
          ]

        TelV tel b <- Teletype -> TCMT IO (TelV Type)
forall (m :: * -> *). MonadReduce m => Teletype -> m (TelV Type)
teleView Teletype
a
        reportSDoc "tc.meta.eta" 40 $ sep
          [ text "considering eta-expansion at type"
          , addContext tel (prettyTCM b)
          , text "under telescope"
          , prettyTCM tel
          ]

        -- Eta expanding metas with a domFinite will just make sure
        -- they go unsolved: conversion will compare them at the
        -- different cases for the domain, so it will not find the
        -- solution for the whole meta.
        if any domIsFinite tel then dontExpand else do

        -- Issue #3774: continue with the right context for b
        addContext tel $ do

        -- if the target type @b@ of @m@ is a meta variable @x@ itself
        -- (@NonBlocked (MetaV{})@),
        -- or it is blocked by a meta-variable @x@ (@Blocked@), we cannot
        -- eta expand now, we have to postpone this.  Once @x@ is
        -- instantiated, we can continue eta-expanding m.  This is realized
        -- by adding @m@ to the listeners of @x@.
        ifBlocked (unEl b) (\ Blocker
x Term
_ -> Blocker -> TCM ()
waitFor Blocker
x) $ \ NotBlocked
_ Term
t -> case Term
t of
          lvl :: Term
lvl@(Def QName
r Elims
es) ->
            TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> TCM Bool
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m Bool
isEtaRecord QName
r) {- then -} (do
              let ps :: Args
ps = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
              let expand :: TCM ()
expand = do
                    u <- MetaVariable -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTrace m => MetaVariable -> m a -> m a
withMetaInfo' MetaVariable
meta (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
                      ShortText
-> Frozen
-> QName
-> Args
-> Tele (Dom Type)
-> Permutation
-> Args
-> TCMT IO Term
newRecordMetaCtx (MetaInfo -> ShortText
miNameSuggestion (MetaVariable -> MetaInfo
mvInfo MetaVariable
meta))
                        (MetaVariable -> Frozen
mvFrozen MetaVariable
meta) QName
r Args
ps Tele (Dom Type)
tel (Nat -> Permutation
idP (Nat -> Permutation) -> Nat -> Permutation
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel) (Args -> TCMT IO Term) -> Args -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> Args
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
tel
                    -- Andreas, 2019-03-18, AIM XXIX, issue #3597
                    -- When meta is frozen instantiate it with in-turn frozen metas.
                    inTopContext $ do
                      reportSDoc "tc.meta.eta" 15 $ sep
                          [ "eta expanding: " <+> pretty m <+> colon <+> prettyTCM t <+> " --> "
                          , nest 2 $ pretty u
                          ]
                      -- Andreas, 2012-03-29: No need for occurrence check etc.
                      -- we directly assign the solution for the meta
                      -- 2012-05-23: We also bypass the check for frozen.
                      noConstraints $ assignTerm' m (telToArgs tel) u  -- should never produce any constraints
              if MetaClass
Records MetaClass -> [MetaClass] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaClass]
kinds then
                TCM ()
expand
               else if (MetaClass
SingletonRecords MetaClass -> [MetaClass] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaClass]
kinds) then
                (Blocker -> TCM ()) -> TCM () -> TCM ()
forall a. (Blocker -> TCMT IO a) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadBlock m =>
(Blocker -> m a) -> m a -> m a
catchPatternErr (\Blocker
x -> Blocker -> TCM ()
waitFor Blocker
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
                 TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> Args -> TCM Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> Args -> m Bool
isSingletonRecord QName
r Args
ps) TCM ()
expand TCM ()
dontExpand
                else TCM ()
dontExpand
            ) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
dontExpand
          Term
_ -> TCM ()
dontExpand

-- | Eta expand blocking metavariables of record type, and reduce the
-- blocked thing.

etaExpandBlocked :: (MonadMetaSolver m, IsMeta t, Reduce t)
                 => Blocked t -> m (Blocked t)
etaExpandBlocked :: forall (m :: * -> *) t.
(MonadMetaSolver m, IsMeta t, Reduce t) =>
Blocked t -> m (Blocked t)
etaExpandBlocked t :: Blocked t
t@NotBlocked{} = Blocked t -> m (Blocked t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t
etaExpandBlocked t :: Blocked t
t@(Blocked Blocker
_ t
v) | Just{} <- t -> Maybe MetaId
forall a. IsMeta a => a -> Maybe MetaId
isMeta t
v = Blocked t -> m (Blocked t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t
etaExpandBlocked (Blocked Blocker
b t
t)  = do
  [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Nat
30 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Eta expanding blockers" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Blocker
b
  (MetaId -> m ()) -> Set MetaId -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([MetaClass] -> MetaId -> m ()
forall (m :: * -> *).
MonadMetaSolver m =>
[MetaClass] -> MetaId -> m ()
etaExpandMeta [MetaClass
Records]) (Set MetaId -> m ()) -> Set MetaId -> m ()
forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
b
  t <- t -> m (Blocked t)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB t
t
  case t of
    Blocked Blocker
b' t
_ | Blocker
b Blocker -> Blocker -> Bool
forall a. Eq a => a -> a -> Bool
/= Blocker
b' -> Blocked t -> m (Blocked t)
forall (m :: * -> *) t.
(MonadMetaSolver m, IsMeta t, Reduce t) =>
Blocked t -> m (Blocked t)
etaExpandBlocked Blocked t
t
    Blocked t
_                      -> Blocked t -> m (Blocked t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked t
t

{-# SPECIALIZE assignWrapper :: CompareDirection -> MetaId -> Elims -> Term -> TCM () -> TCM () #-}
assignWrapper :: (MonadMetaSolver m)
              => CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper :: forall (m :: * -> *).
MonadMetaSolver m =>
CompareDirection -> MetaId -> Elims -> Term -> m () -> m ()
assignWrapper CompareDirection
dir MetaId
x Elims
es Term
v m ()
doAssign = do
  m Bool -> m () -> m () -> m ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (Lens' TCEnv Bool -> m Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eAssignMetas) m ()
forall {b}. m b
dontAssign (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ {- else -} do
    [Char] -> Nat -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
10 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ do
      TCMT IO Doc
"term" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
":" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! CompareDirection -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow CompareDirection
dir) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
    m () -> m ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
nowSolvingConstraints m ()
doAssign m () -> m () -> m ()
forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
`finally` m ()
forall (m :: * -> *). MonadConstraint m => m ()
solveAwakeConstraints

  where dontAssign :: m b
dontAssign = do
          [Char] -> Nat -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Nat
10 [Char]
"don't assign metas"
          Blocker -> m b
forall a. Blocker -> m a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
alwaysUnblock  -- retry again when we are allowed to instantiate metas

-- | Miller pattern unification:
--
--   @assign dir x vs v a@ solves problem @x vs <=(dir) v : a@ for meta @x@
--   if @vs@ are distinct variables (linearity check)
--   and @v@ depends only on these variables
--   and does not contain @x@ itself (occurs check).
--
--   This is the basic story, but we have added some features:
--
--   1. Pruning.
--   2. Benign cases of non-linearity.
--   3. @vs@ may contain record patterns.
--
--   For a reference to some of these extensions, read
--   Andreas Abel and Brigitte Pientka's TLCA 2011 paper.

assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> TCM ()
assign CompareDirection
dir MetaId
x Args
args Term
v CompareAs
target = Blocker -> TCM () -> TCM ()
forall (m :: * -> *) a.
(PureTCM m, MonadBlock m) =>
Blocker -> m a -> m a
addOrUnblocker (MetaId -> Blocker
unblockOnMeta MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do

  mvar <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x  -- information associated with meta x
  let t = Judgement MetaId -> Teletype
forall a. Judgement a -> Teletype
jMetaType (Judgement MetaId -> Teletype) -> Judgement MetaId -> Teletype
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mvar

  -- Andreas, 2011-05-20 TODO!
  -- full normalization  (which also happens during occurs check)
  -- is too expensive! (see Issue 415)
  -- need to do something cheaper, especially if
  -- we are dealing with a Miller pattern that can be solved
  -- immediately!
  -- Ulf, 2011-08-25 DONE!
  -- Just instantiating the top-level meta, which is cheaper. The occurs
  -- check will first try without unfolding any definitions (treating
  -- arguments to definitions as flexible), if that fails it tries again
  -- with full unfolding.
  reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
  v <- instantiate v
  reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
  reportSDoc "tc.meta.assign" 45 $
    "MetaVars.assign: assigning meta " <+> prettyTCM (MetaV x []) <+>
    " with args " <+> prettyList_ (map' (prettyTCM . unArg) args) <+>
    " to " <+> prettyTCM v
  reportSDoc "tc.meta.assign" 45 $
    "MetaVars.assign: type of meta: " <+> pretty t

  reportSDoc "tc.meta.assign" 75 $
    text "MetaVars.assign: assigning meta  " <> pretty x <> text "  with args  " <> pretty args <> text "  to  " <> pretty v

  let
    boundary Term
v = MaybeT (TCMT IO) () -> TCMT IO (Maybe ())
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT do
      (x, ip, args) <- TCMT IO (Maybe (MetaId, InteractionId, Args))
-> MaybeT (TCMT IO) (MetaId, InteractionId, Args)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (MetaId -> Args -> TCMT IO (Maybe (MetaId, InteractionId, Args))
forall (m :: * -> *).
MonadPretty m =>
MetaId -> Args -> m (Maybe (MetaId, InteractionId, Args))
isInteractionMetaB MetaId
x Args
args)
      lift $ tryAddBoundary dir x ip args v target

  -- Jesper, 2019-09-13: When --no-sort-comparison is enabled,
  -- we equate the sort of the solution with the sort of the
  -- metavariable, in order to solve metavariables in sorts.
  -- Jesper, 2020-04-22: We do this before any of the other steps
  -- because comparing the sorts might lead to some metavariables
  -- being solved, which can help with pruning (see #4615).
  -- Jesper, 2020-08-25: --no-sort-comparison is now the default
  -- behaviour.
  --
  -- Under most circumstances, the conversion checker guarantees that
  -- the solution for the meta has the correct type, so there is no
  -- need to check anything. However, there are two circumstances in
  -- which we do need to check the type of the solution:
  --
  -- 1. When comparing two types they are not guaranteed to have the
  --    same sort.
  --
  -- 2. When --cumulativity is enabled the same can happen when
  --    comparing two terms at a sort type.

  let checkSolutionSort Comparison
cmp Sort
s Term
v = do
        s' <- Term -> TCM Sort
forall (m :: * -> *).
(PureTCM m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
v
        reportSDoc "tc.meta.assign" 40 $
          "Instantiating sort" <+> prettyTCM s <+>
          "to sort" <+> prettyTCM s' <+> "of solution" <+> prettyTCM v
        nowConversionChecking' cmp (MetaV x (Apply <$> args)) v (FailAsTermsOf (sort s) (sort s')) $
          compareSort cmp s' s

  case (target , mvJudgement mvar) of
    -- Case 1 (comparing term to meta as types)
    (AsTypes{}   , HasType MetaId
_ Comparison
cmp0 Teletype
t) -> do
      let abort :: TCMT IO Empty
abort = Blocker -> TCMT IO Empty
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCMT IO Empty) -> TCM Blocker -> TCMT IO Empty
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Blocker -> TCM Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker (Teletype -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Teletype
t) -- TODO: make piApplyM' compute unblocker
      s <- Type -> TCM Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort (Type -> TCM Sort) -> TCM Type -> TCM Sort
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Empty -> Teletype -> Args -> TCM Type
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
m Empty -> Teletype -> Args -> m Type
teleApplyM TCMT IO Empty
abort Teletype
t Args
args
      checkSolutionSort CmpEq s v

    (AsTypes{}   , IsSort{}       ) -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (AsTermsOf{} , Judgement MetaId
_              ) -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


  -- We don't instantiate frozen mvars
  when (mvFrozen mvar == Frozen) $ do
    reportSLn "tc.meta.assign" 25 $ "aborting: meta is frozen!"
    -- IApplyConfluence can contribute boundary conditions to frozen metas
    void $ boundary v
    patternViolation neverUnblock

  -- Check that the reducibility of the current environment is
  -- 'compatible' with that of the meta, given its type.
  --
  -- Blocking is a conservative solution, and we could imagine running
  -- the double-checker instead (with the meta's reducibility env.). But
  -- given that the double checker is (a) fiddly and (b) slow, let's
  -- block until someone complains.
  !abs_okay <- canSolveMetaOpaquely (mvInfo mvar) t
  when (not abs_okay) $ do
    reportSDoc "tc.meta.assign" 25 $ "aborting: current env unfolds more than meta knows about!"
    patternViolation neverUnblock

  -- We never get blocked terms here anymore. TODO: we actually do. why?
  whenM (isBlockedTerm x) $ do
    reportSLn "tc.meta.assign" 25 $ "aborting: meta is a blocked term!"
    patternViolation (unblockOnMeta x)

  -- Andreas, 2010-10-15 I want to see whether rhs is blocked
  reportSLn "tc.meta.assign" 50 $ "MetaVars.assign: I want to see whether rhs is blocked"
  reportSDoc "tc.meta.assign" 25 $ do
    v0 <- reduceB v
    case v0 of
      Blocked Blocker
m0 Term
_ -> TCMT IO Doc
"r.h.s. blocked on:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM Blocker
m0
      NotBlocked{} -> TCMT IO Doc
"r.h.s. not blocked"

  reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
  reportSDoc "tc.meta.assign.proj" 45 $ do
    cxt <- getContextTelescope
    vcat
      [ "context before projection expansion"
      , nest 2 $ inTopContext $ prettyTCM cxt
      ]

  -- Normalise and eta contract the arguments to the meta. These are
  -- usually small, and simplifying might let us instantiate more metas.
  -- Also, try to expand away projected vars in meta args.

  expandProjectedVars args (v, target) $ \ Args
args (Term
v, CompareAs
target) -> do

    cxt <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
getContextTelescope
    reportSDoc "tc.meta.assign.proj" 45 $ do
      vcat
        [ "context after projection expansion"
        , nest 2 $ inTopContext $ prettyTCM cxt
        ]

    -- Andreas, 2019-11-16, issue #4159:
    -- We would like to save the work we put into expanding projected variables.
    -- However, the Conversion checker speculatively tries some assignment
    -- in some places (e.g. shortcut) and relies on an exception to be thrown
    -- to try other alternatives next.
    -- If we catch the exception here, this (brittle) mechanism will be broken.
    -- Maybe one possibility would be to rethrow the exception with the
    -- new constraint.  Then, further up, it could be decided whether
    -- to discard the new constraint and do something different,
    -- or add the new constraint when postponing.

    -- BEGIN attempt #4159
    -- let constraint = case v of
    --       -- Sort s -> dirToCmp SortCmp dir (MetaS x $ map' Apply args) s
    --       _      -> dirToCmp (\ cmp -> ValueCmp cmp target) dir (MetaV x $ map' Apply args) v
    -- reportSDoc "tc.meta.assign.catch" 40 $ sep
    --   [ "assign: catching constraint:"
    --   , prettyTCM constraint
    --   ]
    -- -- reportSDoc "tc.meta.assign.catch" 60 $ sep
    -- --   [ "assign: catching constraint:"
    -- --   , pretty constraint
    -- --   ]
    -- reportSDoc "tc.meta.assign.catch" 80 $ sep
    --   [ "assign: catching constraint (raw):"
    --   , (text . show) constraint
    --   ]
    -- catchConstraint constraint $ do
    -- END attempt #4159


    -- Andreas, 2011-04-21 do the occurs check first
    -- e.g. _1 x (suc x) = suc (_2 x y)
    -- even though the lhs is not a pattern, we can prune the y from _2

    reportSDoc "tc.meta.assign" 20 $
        let pr (Var Nat
n []) = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Nat -> [Char]
forall a. Show a => a -> [Char]
show Nat
n)
            pr (Def QName
c []) = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c
            pr Term
_          = m Doc
".."
        in vcat
              [ "mvar args:" <+> sep (map' (pr . unArg) args)
              ]

    let !vars = Args -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Args
args

    -- Check that the x doesn't occur in the right hand side.
    -- Prune mvars on rhs such that they can only depend on lhs vars.
    v <- liftTCM $ occursCheck x vars v

    reportSLn "tc.meta.assign" 15 "passed occursCheck"
    reportSDoc "tc.meta.assign" 25 $ "v = " <+> prettyTCM v
    verboseS "tc.meta.assign" 30 $ do
      let n = Term -> Nat
forall a. TermSize a => a -> Nat
termSize Term
v
      when (n > 200) $ reportSDoc "tc.meta.assign" 30 $
        sep [ "size" <+> text (show n)
--              , nest 2 $ "type" <+> prettyTCM t
            , nest 2 $ "term" <+> prettyTCM v
            ]

    -- Check linearity of @ids@
    -- Andreas, 2010-09-24: Herein, ignore the variables which are not
    -- free in v
    let fvs = Term -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Term
v
    reportSDoc "tc.meta.assign" 20 $
      "fvars rhs:" <+> sep (map' (text . show) $ VarSet.toAscList fvs)

    let n = Args -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args
    TelV mTel _ <- teleViewUpToPath n t

    -- Check that the arguments are variables
    mids <- do
      res <- runExceptT $ inverseSubst' (const False) mTel args
      case res of
        -- all args are variables
        Right [(Nat, Term)]
ids -> do
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"inverseSubst returns:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (((Nat, Term) -> TCMT IO Doc) -> [(Nat, Term)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Nat, Term) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Nat, Term)]
ids)
          [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
            TCMT IO Doc
"inverseSubst returns:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep (((Nat, Term) -> TCMT IO Doc) -> [(Nat, Term)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Nat, Term) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => (Nat, Term) -> m Doc
prettyTCM [(Nat, Term)]
ids)
          let boundVars :: VarSet
boundVars = [Nat] -> VarSet
VarSet.fromList ([Nat] -> VarSet) -> [Nat] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Nat, Term) -> Nat) -> [(Nat, Term)] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map' (Nat, Term) -> Nat
forall a b. (a, b) -> a
fst [(Nat, Term)]
ids
          if VarSet
fvs VarSet -> VarSet -> Bool
`VarSet.isSubsetOf` VarSet
boundVars
            then Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)]))
-> Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall a b. (a -> b) -> a -> b
$ [(Nat, Term)] -> Maybe [(Nat, Term)]
forall a. a -> Maybe a
Just [(Nat, Term)]
ids
            else Maybe [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(Nat, Term)]
forall a. Maybe a
Nothing
        -- we have proper values as arguments which could be cased on
        -- here, we cannot prune, since offending vars could be eliminated
        Left (CantInvert Term
tm) -> Maybe [(Nat, Term)]
forall a. Maybe a
Nothing Maybe [(Nat, Term)]
-> TCMT IO (Maybe ()) -> TCMT IO (Maybe [(Nat, Term)])
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term -> TCMT IO (Maybe ())
boundary Term
v
        -- we have non-variables, but these are not eliminateable
        Left InvertExcept
NeutralArg  -> [(Nat, Term)] -> Maybe [(Nat, Term)]
forall a. a -> Maybe a
Just ([(Nat, Term)] -> Maybe [(Nat, Term)])
-> TCMT IO [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> Args -> VarSet -> TCMT IO [(Nat, Term)]
forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs
        -- we have a projected variable which could not be eta-expanded away:
        -- same as neutral
        Left ProjVar{}   -> [(Nat, Term)] -> Maybe [(Nat, Term)]
forall a. a -> Maybe a
Just ([(Nat, Term)] -> Maybe [(Nat, Term)])
-> TCMT IO [(Nat, Term)] -> TCMT IO (Maybe [(Nat, Term)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> Args -> VarSet -> TCMT IO [(Nat, Term)]
forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
fvs

    case mids of  -- vv Ulf 2014-07-13: actually not needed after all: attemptInertRHSImprovement x args v
      Maybe [(Nat, Term)]
Nothing  -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (Blocker -> TCM ()) -> TCM Blocker -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Blocker -> TCM Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker (Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
v)  -- TODO: more precise
      Just [(Nat, Term)]
ids -> do
        -- Check linearity
        ids <- do
          res <- ExceptT () (TCMT IO) [(Nat, Term)] -> TCM (Either () [(Nat, Term)])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT () (TCMT IO) [(Nat, Term)]
 -> TCM (Either () [(Nat, Term)]))
-> ExceptT () (TCMT IO) [(Nat, Term)]
-> TCM (Either () [(Nat, Term)])
forall a b. (a -> b) -> a -> b
$ [(Nat, Term)] -> ExceptT () (TCMT IO) [(Nat, Term)]
checkLinearity {- (`VarSet.member` fvs) -} [(Nat, Term)]
ids
          case res of
            -- case: linear
            Right [(Nat, Term)]
ids -> [(Nat, Term)] -> TCMT IO [(Nat, Term)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Nat, Term)]
ids
            -- case: non-linear variables that could possibly be pruned
            -- If pruning fails we need to unblock on any meta in the rhs, since they might get
            -- rid of the dependency on the non-linear variable. TODO: be more precise (all metas
            -- using non-linear variables need to be solved).
            Left ()   -> do
              block <- Blocker -> TCM Blocker
forall (m :: * -> *). PureTCM m => Blocker -> m Blocker
updateBlocker (Blocker -> TCM Blocker) -> Blocker -> TCM Blocker
forall a b. (a -> b) -> a -> b
$ Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Term
v
              addOrUnblocker block $ attemptPruning x args fvs

        -- Solve.
        m <- getContextSize
        assignMeta' m x t n ids v
  where
    -- Try to remove meta arguments from lhs that mention variables not occurring on rhs.
    attemptPruning
      :: MetaId
      -- Meta-variable (lhs)
      -> Args
      -- Meta arguments (lhs)
      -> VarSet
      -- Variables we do not want to prune
      -- (e.g. those occurring on the rhs)
      -> TCM a
    attemptPruning :: forall a. MetaId -> Args -> VarSet -> TCM a
attemptPruning MetaId
x Args
args VarSet
noPrune = do
      -- non-linear lhs: we cannot solve, but prune
      killResult <- MetaId -> Args -> (Nat -> Bool) -> TCM PruneResult
prune MetaId
x Args
args (Nat -> VarSet -> Bool
`VarSet.member` VarSet
noPrune)
      let success = PruneResult
killResult PruneResult -> [PruneResult] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PruneResult
PrunedSomething,PruneResult
PrunedEverything]
      reportSDoc "tc.meta.assign" 10 $
        "pruning" <+> prettyTCM x <+> do text $ if success then "succeeded" else "failed"
      blocker <- if
        | success   -> return alwaysUnblock  -- If pruning succeeded we want to retry right away
        | otherwise -> unblockOnAnyMetaIn . MetaV x . map' Apply <$> instantiateFull args
             -- TODO: could be more precise: only unblock on metas
             --       applied to offending variables
      patternViolation blocker

-- | Is the given metavariable application secretly an interaction point
-- application? Ugly.
isInteractionMetaB
  :: forall m. (MonadPretty m)
  => MetaId
  -> Args
  -> m (Maybe (MetaId, InteractionId, Args))
isInteractionMetaB :: forall (m :: * -> *).
MonadPretty m =>
MetaId -> Args -> m (Maybe (MetaId, InteractionId, Args))
isInteractionMetaB MetaId
mid Args
args =
  MaybeT m (MetaId, InteractionId, Args)
-> m (Maybe (MetaId, InteractionId, Args))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m (MetaId, InteractionId, Args)
 -> m (Maybe (MetaId, InteractionId, Args)))
-> MaybeT m (MetaId, InteractionId, Args)
-> m (Maybe (MetaId, InteractionId, Args))
forall a b. (a -> b) -> a -> b
$ MetaId -> Args -> MaybeT m (MetaId, InteractionId, Args)
forall {m :: * -> *} {c}.
ReadTCState m =>
MetaId -> c -> MaybeT m (MetaId, InteractionId, c)
here MetaId
mid Args
args MaybeT m (MetaId, InteractionId, Args)
-> MaybeT m (MetaId, InteractionId, Args)
-> MaybeT m (MetaId, InteractionId, Args)
forall a. MaybeT m a -> MaybeT m a -> MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` do
    -- If the meta isn't literally an interaction point it might still
    -- be instantiable to an interaction point
    m Term -> MaybeT m Term
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Term -> m Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (MetaId -> Elims -> Term
MetaV MetaId
mid (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Args -> Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Args
args))) MaybeT m Term
-> (Term -> MaybeT m (MetaId, InteractionId, Args))
-> MaybeT m (MetaId, InteractionId, Args)
forall a b. MaybeT m a -> (a -> MaybeT m b) -> MaybeT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term -> MaybeT m (MetaId, InteractionId, Args)
there
  where
    here :: MetaId -> c -> MaybeT m (MetaId, InteractionId, c)
here MetaId
mid c
args = do
      iid <- m (Maybe InteractionId) -> MaybeT m InteractionId
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (MetaId -> m (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
mid)
      pure (mid, iid, args)

    there :: Term -> MaybeT m (MetaId, InteractionId, Args)
    there :: Term -> MaybeT m (MetaId, InteractionId, Args)
there (MetaV MetaId
m Elims
args) = do
      iid  <- m (Maybe InteractionId) -> MaybeT m InteractionId
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (MetaId -> m (Maybe InteractionId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe InteractionId)
isInteractionMeta MetaId
m)
      args <- MaybeT (pure (allApplyElims args))
      pure (m, iid, args)
    -- It might be the case that the inner meta (the interaction point)
    -- exists in a larger context, so instantiating the outer meta (the
    -- original argument) will produce lambdas.
    --
    -- Since the boundary code runs in the inner, larger context, we can
    -- peel off the lambdas without running afoul of the scope.
    there (Lam ArgInfo
_ Abs Term
as) = Term -> MaybeT m (MetaId, InteractionId, Args)
there (Abs Term -> SubstArg Term -> Term
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Term
as (Nat -> Term
var Nat
0))
    there Term
_ = MaybeT m (MetaId, InteractionId, Args)
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- | @assignMeta m x t ids u@ solves @x ids = u@ for meta @x@ of type @t@,
--   where term @u@ lives in a context of length @m@.
--   Precondition: @ids@ is linear.
assignMeta :: Int -> MetaId -> Teletype -> [Int] -> Term -> TCM ()
assignMeta :: Nat -> MetaId -> Teletype -> [Nat] -> Term -> TCM ()
assignMeta Nat
m MetaId
x Teletype
t [Nat]
ids Term
v = do
  let n :: Nat
n    = [Nat] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Nat]
ids
      cand :: [(Nat, Term)]
cand = [(Nat, Term)] -> [(Nat, Term)]
forall a. Ord a => [a] -> [a]
List.sort ([(Nat, Term)] -> [(Nat, Term)]) -> [(Nat, Term)] -> [(Nat, Term)]
forall a b. (a -> b) -> a -> b
$ [Nat] -> [Term] -> [(Nat, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip' [Nat]
ids ([Term] -> [(Nat, Term)]) -> [Term] -> [(Nat, Term)]
forall a b. (a -> b) -> a -> b
$ (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Nat -> Term
var ([Nat] -> [Term]) -> [Nat] -> [Term]
forall a b. (a -> b) -> a -> b
$ Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n
  Nat -> MetaId -> Teletype -> Nat -> [(Nat, Term)] -> Term -> TCM ()
assignMeta' Nat
m MetaId
x Teletype
t Nat
n [(Nat, Term)]
cand Term
v

-- | @assignMeta' m x t ids u@ solves @x = [ids]u@ for meta @x@ of type @t@,
--   where term @u@ lives in a context of length @m@,
--   and @ids@ is a partial substitution.
assignMeta' :: Int -> MetaId -> Teletype -> Int -> SubstCand -> Term -> TCM ()
assignMeta' :: Nat -> MetaId -> Teletype -> Nat -> [(Nat, Term)] -> Term -> TCM ()
assignMeta' Nat
m MetaId
x Teletype
t Nat
n [(Nat, Term)]
ids Term
v = do
  -- we are linear, so we can solve!
  [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"preparing to instantiate: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v

  -- Rename the variables in v to make it suitable for abstraction over ids.
  -- Basically, if
  --   Γ   = a b c d e
  --   ids = d b e
  -- then
  --   v' = (λ a b c d e. v) _ 1 _ 2 0
  --
  -- Andreas, 2013-10-25 Solve using substitutions:
  -- Convert assocList @ids@ (which is sorted) into substitution,
  -- filling in __IMPOSSIBLE__ for the missing terms, e.g.
  -- [(0,0),(1,2),(3,1)] --> [0, 2, __IMP__, 1, __IMP__]
  -- ALT 1: O(m * size ids), serves as specification
  -- let ivs = [fromMaybe __IMPOSSIBLE__ $ lookup i ids | i <- [0..m-1]]
  -- ALT 2: O(m)
  let assocToList :: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList Nat
i = \case
        [(Nat, Term)]
_           | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
m -> []
        ((Nat
j,Term
u) : [(Nat, Term)]
l) | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
u  Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [(Nat, Term)]
l
        [(Nat, Term)]
l                    -> Maybe Term
forall a. Maybe a
Nothing Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [(Nat, Term)]
l
      ivs :: [Maybe Term]
ivs = Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList Nat
0 [(Nat, Term)]
ids
      rho :: Substitution
rho = Impossible -> [Maybe Term] -> Substitution -> Substitution
forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
HasCallStack => Impossible
impossible [Maybe Term]
ivs (Substitution -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution
forall a. Nat -> Substitution' a
raiseS Nat
n
      v' :: Term
v'  = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
rho Term
v

  cxt <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
getContextTelescope

  -- Variables not strengthened away
  let notDropped = [Nat] -> VarSet
VarSet.fromList ([Nat] -> VarSet) -> [Nat] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Nat, Term) -> Nat) -> [(Nat, Term)] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Nat, Term) -> Nat
forall a b. (a, b) -> a
fst [(Nat, Term)]
ids

  -- Metas are top-level so we do the assignment at top-level.
  inTopContext $ do

    -- Andreas, 2011-04-18 to work with irrelevant parameters
    -- we need to construct tel' from the type of the meta variable
    -- (no longer from ids which may not be the complete variable list
    -- any more)
    reportSDoc "tc.meta.assign" 15 $ "type of meta =" <+> prettyTCM t

    (TelV mTel a, bs) <- teleViewUpToPathBoundary n t
    reportSDoc "tc.meta.assign" 30 $ "tel'  =" <+> prettyTCM mTel
    reportSDoc "tc.meta.assign" 30 $ "#args =" <+> text (show n)

    -- Andreas, 2013-09-17 (AIM XVIII): if t does not provide enough
    -- types for the arguments, it might be blocked by a meta;
    -- then we give up. (Issue 903)
    when (size mTel < n) $ do
      a <- abortIfBlocked a
      reportSDoc "impossible" 10 $ "not enough pis, but not blocked?" <?> pretty a
      __IMPOSSIBLE__   -- If we get here it was _not_ blocked by a meta!

    -- Check that the term conforms to its expected boundary if the
    -- meta's spine contains eliminations corresponding to @Path@s in
    -- its type.
    v' <- case bs of
      -- avoid doing context/constraint set manipulations if there is no
      -- boundary (mostly as an optimisation, though somewhat observable
      -- in "unsolved constraints" errors):
      Boundary [] -> Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v'
      Boundary
_           -> Tele (Dom Type) -> TCMT IO Term -> TCMT IO Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
mTel (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Term -> TCMT IO Term
blockTerm Type
a (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Type -> Boundary -> Term -> TCMT IO Term
equalTermToBoundary Type
a Boundary
bs Term
v'

    -- Andreas, 2013-10-25 double check solution before assigning
    whenM (optDoubleCheck  <$> pragmaOptions) $ do
      m <- lookupLocalMeta x
      reportSDoc "tc.meta.check" 30 $ vcat
        [ "double checking solution"
        , nest 2 $ "t    =" <+> pretty t
        , nest 2 $ "a    =" <+> pretty a
        , nest 2 $ "mTel =" <+> pretty mTel
        ]
      catchConstraint (CheckMetaInst x) $
        addContext mTel $ checkSolutionForMeta x m v' a

    reportSDoc "tc.meta.assign" 10 $
      "solving" <+> prettyTCM x <+> ":=" <+> prettyTCM (abstract mTel v')

    assignTerm x (telToArgs mTel) v'

-- | Check that the instantiation of the given metavariable fits the
--   type of the metavariable. If the metavariable is not yet
--   instantiated, add a constraint to check the instantiation later.
checkMetaInst :: MetaId -> TCM ()
checkMetaInst :: MetaId -> TCM ()
checkMetaInst MetaId
x = do
  m <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
  let postpone = Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint (MetaId -> Blocker
unblockOnMeta MetaId
x) (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Constraint
CheckMetaInst MetaId
x
  case mvInstantiation m of
    BlockedConst{} -> TCM ()
postpone
    PostponedTypeCheckingProblem{} -> TCM ()
postpone
    OpenMeta{} -> TCM ()
postpone
    InstV Instantiation
inst -> do
      let n :: Nat
n = [Arg ShortText] -> Nat
forall a. Sized a => a -> Nat
size (Instantiation -> [Arg ShortText]
instTel Instantiation
inst)
          t :: Teletype
t = Judgement MetaId -> Teletype
forall a. Judgement a -> Teletype
jMetaType (Judgement MetaId -> Teletype) -> Judgement MetaId -> Teletype
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m
      (telv@(TelV tel a),bs) <- Nat -> Teletype -> TCMT IO (TelV Type, Boundary)
forall (m :: * -> *).
PureTCM m =>
Nat -> Teletype -> m (TelV Type, Boundary)
teleViewUpToPathBoundary Nat
n Teletype
t
      catchConstraint (CheckMetaInst x) $ addContext tel $
        checkSolutionForMeta x m (instBody inst) a

-- | Check that the instantiation of the metavariable with the given
--   term is well-typed.
checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta :: MetaId -> MetaVariable -> Term -> Type -> TCM ()
checkSolutionForMeta MetaId
x MetaVariable
m Term
v Type
a = do
  [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checking solution for meta" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x
  case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m of
    HasType{ jComparison :: forall a. Judgement a -> Comparison
jComparison = Comparison
cmp } -> do
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" : " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
        ctx <- TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
        inTopContext $ "in context: " <+> prettyTCM (PrettyContext ctx)
      Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> MetaId -> Type -> Term -> Call
CheckMetaSolution (MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange MetaVariable
m) MetaId
x Type
a Term
v) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
        Term -> Comparison -> TypeOf Term -> TCM ()
forall a. CheckInternal a => a -> Comparison -> TypeOf a -> TCM ()
checkInternal Term
v Comparison
cmp Type
TypeOf Term
a
    IsSort{}  -> TCM () -> TCM ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Nat -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" is a sort"
      s <- Type -> TCM Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type -> m Sort
shouldBeSort (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
HasCallStack => Sort
__DUMMY_SORT__ Term
v)
      traceCall (CheckMetaSolution (getRange m) x (sort (univSort s)) (Sort s)) $
        inferInternal s

-- | Eta-expand bound variables like @z@ in @X (fst z)@.
expandProjectedVars
  :: ( Pretty a, PrettyTCM a, NoProjectedVar a
     -- , Normalise a, TermLike a, Subst Term a
     , ReduceAndEtaContract a
     , PrettyTCM b, TermSubst b
     )
  => a  -- ^ Meta variable arguments.
  -> b  -- ^ Right hand side.
  -> (a -> b -> TCM c)
  -> TCM c
expandProjectedVars :: forall a b c.
(Pretty a, PrettyTCM a, NoProjectedVar a, ReduceAndEtaContract a,
 PrettyTCM b, TermSubst b) =>
a -> b -> (a -> b -> TCM c) -> TCM c
expandProjectedVars a
args b
v a -> b -> TCM c
ret = (a, b) -> TCM c
loop (a
args, b
v) where
  loop :: (a, b) -> TCM c
loop (a
args, b
v) = do
    [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"meta args: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
args
    args <- TCM a -> TCM a
forall a. TCM a -> TCM a
callByName (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ a -> TCM a
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract a
args
    reportSDoc "tc.meta.assign.proj" 45 $ "norm args: " <+> prettyTCM args
    reportSDoc "tc.meta.assign.proj" 85 $ "norm args: " <+> pretty args
    let done = a -> b -> TCM c
ret a
args b
v
    case noProjectedVar args of
      Right ()              -> do
        [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
          TCMT IO Doc
"no projected var found in args: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
args
        TCM c
done
      Left (ProjectedVar Nat
i [(ProjOrigin, QName)]
_) -> Nat -> (a, b) -> TCM c -> ((a, b) -> TCM c) -> TCM c
forall a c.
(PrettyTCM a, TermSubst a) =>
Nat -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Nat
i (a
args, b
v) TCM c
done (a, b) -> TCM c
loop

-- | Eta-expand a de Bruijn index of record type in context and passed term(s).
etaExpandProjectedVar :: (PrettyTCM a, TermSubst a) => Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar :: forall a c.
(PrettyTCM a, TermSubst a) =>
Nat -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Nat
i a
v TCM c
fail a -> TCM c
succeed = do
  [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
40 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"trying to expand projected variable" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Nat -> Term
var Nat
i)
  tel <- TCMT IO (Tele (Dom Type))
forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
getContextTelescope
  caseMaybeM (etaExpandBoundVar i) fail $ \ (Tele (Dom Type)
delta, Substitution
sigma, Substitution
tau) -> do
  [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Nat
25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"eta-expanding var " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Nat -> Term
var Nat
i) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCMT IO Doc
" in terms " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
v
  TCM c -> TCM c
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
unsafeInTopContext (TCM c -> TCM c) -> TCM c -> TCM c
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCM c -> TCM c
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta (TCM c -> TCM c) -> TCM c -> TCM c
forall a b. (a -> b) -> a -> b
$
    a -> TCM c
succeed (a -> TCM c) -> a -> TCM c
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg a)
tau a
v

-- | A de Bruijn index under some projections.
data ProjectedVar = ProjectedVar
  { ProjectedVar -> Nat
pvIndex :: Int
  , ProjectedVar -> [(ProjOrigin, QName)]
prProjs :: [(ProjOrigin, QName)]
  }
  deriving (Nat -> ProjectedVar -> [Char] -> [Char]
[ProjectedVar] -> [Char] -> [Char]
ProjectedVar -> [Char]
(Nat -> ProjectedVar -> [Char] -> [Char])
-> (ProjectedVar -> [Char])
-> ([ProjectedVar] -> [Char] -> [Char])
-> Show ProjectedVar
forall a.
(Nat -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Nat -> ProjectedVar -> [Char] -> [Char]
showsPrec :: Nat -> ProjectedVar -> [Char] -> [Char]
$cshow :: ProjectedVar -> [Char]
show :: ProjectedVar -> [Char]
$cshowList :: [ProjectedVar] -> [Char] -> [Char]
showList :: [ProjectedVar] -> [Char] -> [Char]
Show)

-- | Ignore 'ProjOrigin' in equality test.

instance Eq ProjectedVar where
  ProjectedVar Nat
i [(ProjOrigin, QName)]
prjs == :: ProjectedVar -> ProjectedVar -> Bool
== ProjectedVar Nat
i' [(ProjOrigin, QName)]
prjs' =
    Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
i' Bool -> Bool -> Bool
&& ((ProjOrigin, QName) -> QName) -> [(ProjOrigin, QName)] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (ProjOrigin, QName) -> QName
forall a b. (a, b) -> b
snd [(ProjOrigin, QName)]
prjs [QName] -> [QName] -> Bool
forall a. Eq a => a -> a -> Bool
== ((ProjOrigin, QName) -> QName) -> [(ProjOrigin, QName)] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (ProjOrigin, QName) -> QName
forall a b. (a, b) -> b
snd [(ProjOrigin, QName)]
prjs'

viewProjectedVar :: Term -> Maybe ProjectedVar
viewProjectedVar :: Term -> Maybe ProjectedVar
viewProjectedVar = \case
  Var Nat
i Elims
es -> Nat -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Nat
i ([(ProjOrigin, QName)] -> ProjectedVar)
-> Maybe [(ProjOrigin, QName)] -> Maybe ProjectedVar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Elim -> Maybe (ProjOrigin, QName))
-> Elims -> Maybe [(ProjOrigin, QName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es
  Term
_ -> Maybe ProjectedVar
forall a. Maybe a
Nothing

unviewProjectedVar :: ProjectedVar -> Term
unviewProjectedVar :: ProjectedVar -> Term
unviewProjectedVar (ProjectedVar Nat
i [(ProjOrigin, QName)]
prjs) = Nat -> Elims -> Term
Var Nat
i (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ ((ProjOrigin, QName) -> Elim) -> [(ProjOrigin, QName)] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map ((ProjOrigin -> QName -> Elim) -> (ProjOrigin, QName) -> Elim
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj) [(ProjOrigin, QName)]
prjs

-- | Check whether one of the meta args is a projected var.
class NoProjectedVar a where
  noProjectedVar :: a -> Either ProjectedVar ()

  default noProjectedVar
    :: (NoProjectedVar b, Foldable t, t b ~ a)
    => a -> Either ProjectedVar ()
  noProjectedVar = (b -> Either ProjectedVar ()) -> t b -> Either ProjectedVar ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
Fold.mapM_ b -> Either ProjectedVar ()
forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar

instance NoProjectedVar a => NoProjectedVar (Arg a)
instance NoProjectedVar a => NoProjectedVar [a]

instance NoProjectedVar Term where
  noProjectedVar :: Term -> Either ProjectedVar ()
noProjectedVar = \case
      Var Nat
i Elims
es
        | qs :: [(ProjOrigin, QName)]
qs@((ProjOrigin, QName)
_:[(ProjOrigin, QName)]
_) <- (Maybe (ProjOrigin, QName) -> Maybe (ProjOrigin, QName))
-> [Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)]
forall a b. (a -> Maybe b) -> [a] -> Prefix b
takeWhileJust Maybe (ProjOrigin, QName) -> Maybe (ProjOrigin, QName)
forall a. a -> a
id ([Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)])
-> [Maybe (ProjOrigin, QName)] -> [(ProjOrigin, QName)]
forall a b. (a -> b) -> a -> b
$ (Elim -> Maybe (ProjOrigin, QName))
-> Elims -> [Maybe (ProjOrigin, QName)]
forall a b. (a -> b) -> [a] -> [b]
map' Elim -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es
        -> ProjectedVar -> Either ProjectedVar ()
forall a b. a -> Either a b
Left (ProjectedVar -> Either ProjectedVar ())
-> ProjectedVar -> Either ProjectedVar ()
forall a b. (a -> b) -> a -> b
$ Nat -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Nat
i [(ProjOrigin, QName)]
qs
      -- Andreas, 2015-09-12 Issue #1316:
      -- Also look in inductive record constructors
      Con (ConHead QName
_ IsRecord{} Induction
Inductive [QName]
_) ConInfo
_ Elims
es
        | Just Args
vs <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        -> Args -> Either ProjectedVar ()
forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar Args
vs
      Term
_ -> () -> Either ProjectedVar ()
forall a. a -> Either ProjectedVar a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Normalize just far enough to be able to eta-contract maximally.
class (TermLike a, TermSubst a, Reduce a) => ReduceAndEtaContract a where
  reduceAndEtaContract :: a -> TCM a

  default reduceAndEtaContract
    :: (Traversable f, ReduceAndEtaContract b, f b ~ a)
    => a -> TCM a
  reduceAndEtaContract = (b -> TCMT IO b) -> f b -> TCMT IO (f b)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> f a -> m (f b)
Trav.mapM b -> TCMT IO b
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract

instance ReduceAndEtaContract a => ReduceAndEtaContract [a]
instance ReduceAndEtaContract a => ReduceAndEtaContract (Arg a)

instance ReduceAndEtaContract Term where
  reduceAndEtaContract :: Term -> TCMT IO Term
reduceAndEtaContract Term
u = do
    [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"trying to eta-contract u =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
    u <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
u
    reportSDoc "tc.meta" 30 $ "               reduced u =" <+> prettyTCM u
    case u of
      -- In case of lambda or record constructor, it makes sense to
      -- reduce further.
      Lam ArgInfo
ai Abs Term
bAbs -> Abs Term -> (Term -> TCMT IO Term) -> TCMT IO Term
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Abs a -> (a -> m b) -> m b
underAbstraction_ Abs Term
bAbs ((Term -> TCMT IO Term) -> TCMT IO Term)
-> (Term -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \Term
b ->
        ArgInfo -> ShortText -> Term -> TCMT IO Term
forall (m :: * -> *).
MonadTCEnv m =>
ArgInfo -> ShortText -> Term -> m Term
etaLam ArgInfo
ai (Abs Term -> ShortText
forall a. Abs a -> ShortText
absName Abs Term
bAbs) (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract Term
b
      Con ConHead
c ConInfo
ci Elims
es -> ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> Args -> TCMT IO Term)
-> TCMT IO Term
forall (m :: * -> *).
HasConstInfo m =>
ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> Args -> m Term)
-> m Term
etaCon ConHead
c ConInfo
ci Elims
es ((QName -> ConHead -> ConInfo -> Args -> TCMT IO Term)
 -> TCMT IO Term)
-> (QName -> ConHead -> ConInfo -> Args -> TCMT IO Term)
-> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ QName
r ConHead
c ConInfo
ci Args
args -> do
        args <- Args -> TCMT IO Args
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract Args
args
        etaContractRecord r c ci args
      Term
v -> Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

{- UNUSED, BUT KEEP!
-- Wrong attempt at expanding bound variables.
-- The following code curries meta instead.

-- | @etaExpandProjectedVar mvar x t n qs@
--
--   @mvar@ is the meta var info.
--   @x@ is the meta variable we are trying to solve for.
--   @t@ is its type.
--   @n@ is the number of the meta arg we want to curry (starting at 0).
--   @qs@ is the projection path along which we curry.
--
etaExpandProjectedVar :: MetaVariable -> MetaId -> Type -> Int -> [QName] -> TCM a
etaExpandProjectedVar mvar x t n qs = inTopContext $ do
  (_, uncurry, t') <- curryAt t n
  let TelV tel a = telView' t'
      perm       = idP (size tel)
  y <- newMeta (mvInfo mvar) (mvPriority mvar) perm (HasType __IMPOSSIBLE__ t')
  assignTerm' x (uncurry $ MetaV y [])
  patternViolation
-}

{-
  -- first, strip the leading n domains (which remain unchanged)
  TelV gamma core <- telViewUpTo n t
  case unEl core of
    -- There should be at least one domain left
    Pi (Dom ai a) b -> do
      -- Eta-expand @dom@ along @qs@ into a telescope @tel@, computing a substitution.
      -- For now, we only eta-expand once.
      -- This might trigger another call to @etaExpandProjectedVar@ later.
      -- A more efficient version does all the eta-expansions at once here.
      (r, pars, def) <- fromMaybe __IMPOSSIBLE__ <$> isRecordType a
      unless (recEtaEquality def) __IMPOSSIBLE__
      let tel = recTel def `apply` pars
          m   = size tel
          v   = Con (recConHead def) $ map' var $ downFrom m
          b'  = raise m b `absApp` v
          fs  = recFields def
          vs  = zipWith' (\ f i -> Var i [Proj f]) fs $ downFrom m
          -- v = c (n-1) ... 1 0
      (tel, u) <- etaExpandAtRecordType a $ var 0
      -- TODO: compose argInfo ai with tel.
      -- Substitute into @b@.
      -- Abstract over @tel@.
      -- Abstract over @gamma@.
      -- Create new meta.
      -- Solve old meta, using substitution.
      patternViolation
    _ -> __IMPOSSIBLE__
-}

type FVs = VarSet
type SubstCand = [(Int,Term)] -- ^ a possibly non-deterministic substitution

-- | Turn non-det substitution into proper substitution, if possible.
--   Otherwise, raise the error.
checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
checkLinearity :: [(Nat, Term)] -> ExceptT () (TCMT IO) [(Nat, Term)]
checkLinearity [(Nat, Term)]
ids = do
  -- see issue #920
  [(Nat, Term)] -> [(Nat, Term)]
[(Nat, Term)] -> [Item [(Nat, Term)]]
forall l. IsList l => l -> [Item l]
List1.toList ([(Nat, Term)] -> [(Nat, Term)])
-> ExceptT () (TCMT IO) [(Nat, Term)]
-> ExceptT () (TCMT IO) [(Nat, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (List1 (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term))
-> [List1 (Nat, Term)] -> ExceptT () (TCMT IO) [(Nat, Term)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM List1 (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
makeLinear (((Nat, Term) -> Nat) -> [(Nat, Term)] -> [List1 (Nat, Term)]
forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
List1.groupOn (Nat, Term) -> Nat
forall a b. (a, b) -> a
fst [(Nat, Term)]
ids)
  where
    -- Non-determinism can be healed if type is singleton. [Issue 593]
    -- (Same as for irrelevance.)
    makeLinear :: List1 (Int, Term) -> ExceptT () TCM (Int, Term)
    makeLinear :: List1 (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
makeLinear ((Nat, Term)
p       :| []) = (Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
forall a. a -> ExceptT () (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat, Term)
p
    makeLinear (p :: (Nat, Term)
p@(Nat
i,Term
t) :| [(Nat, Term)]
_ ) =
      ExceptT () (TCMT IO) Bool
-> ExceptT () (TCMT IO) (Nat, Term)
-> ExceptT () (TCMT IO) (Nat, Term)
-> ExceptT () (TCMT IO) (Nat, Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Bool -> Either Blocker Bool
forall a b. b -> Either a b
Right Bool
True Either Blocker Bool -> Either Blocker Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) (Either Blocker Bool -> Bool)
-> ExceptT () (TCMT IO) (Either Blocker Bool)
-> ExceptT () (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do TCM (Either Blocker Bool)
-> ExceptT () (TCMT IO) (Either Blocker Bool)
forall (m :: * -> *) a. Monad m => m a -> ExceptT () m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Either Blocker Bool)
 -> ExceptT () (TCMT IO) (Either Blocker Bool))
-> (Type -> TCM (Either Blocker Bool))
-> Type
-> ExceptT () (TCMT IO) (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BlockT (TCMT IO) Bool -> TCM (Either Blocker Bool)
forall (m :: * -> *) a. BlockT m a -> m (Either Blocker a)
runBlocked (BlockT (TCMT IO) Bool -> TCM (Either Blocker Bool))
-> (Type -> BlockT (TCMT IO) Bool)
-> Type
-> TCM (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> BlockT (TCMT IO) Bool
forall (m :: * -> *). (PureTCM m, MonadBlock m) => Type -> m Bool
isSingletonTypeModuloRelevance (Type -> ExceptT () (TCMT IO) (Either Blocker Bool))
-> ExceptT () (TCMT IO) Type
-> ExceptT () (TCMT IO) (Either Blocker Bool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Nat -> ExceptT () (TCMT IO) Type
forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Nat -> m Type
typeOfBV Nat
i)
        ((Nat, Term) -> ExceptT () (TCMT IO) (Nat, Term)
forall a. a -> ExceptT () (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Nat, Term)
p)
        (() -> ExceptT () (TCMT IO) (Nat, Term)
forall a. () -> ExceptT () (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ())

-- Intermediate result in the following function
type Res = [(Arg Nat, Term)]

-- | Exceptions raised when substitution cannot be inverted.
data InvertExcept
  = CantInvert Term           -- ^ Cannot recover.
  | NeutralArg                -- ^ A potentially neutral arg: can't invert, but can try pruning.
  | ProjVar ProjectedVar      -- ^ Try to eta-expand var to remove projs.

-- | Check that arguments @args@ to a metavar are in pattern fragment.
--   Assumes all arguments already in whnf and eta-reduced.
--   Parameters are represented as @Var@s so @checkArgs@ really
--   checks that all args are @Var@s and returns the "substitution"
--   to be applied to the rhs of the equation to solve.
--   (If @args@ is considered a substitution, its inverse is returned.)
--
--   The returned list might not be ordered.
--   Linearity, i.e., whether the substitution is deterministic,
--   has to be checked separately.
--
inverseSubst' ::
     (Term -> Bool) -> Tele (Dom Type) -> Args
  -> ExceptT InvertExcept TCM SubstCand
inverseSubst' :: (Term -> Bool)
-> Tele (Dom Type)
-> Args
-> ExceptT InvertExcept (TCMT IO) [(Nat, Term)]
inverseSubst' Term -> Bool
skip Tele (Dom Type)
tel Args
args = ((Arg Nat, Term) -> (Nat, Term))
-> [(Arg Nat, Term)] -> [(Nat, Term)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Arg Nat -> Nat) -> (Arg Nat, Term) -> (Nat, Term)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Arg Nat -> Nat
forall e. Arg e -> e
unArg) ([(Arg Nat, Term)] -> [(Nat, Term)])
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Nat, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
loop (Args -> [Term] -> [(Arg Term, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip' Args
args [Term]
terms)
  where
  loop :: [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
loop  = ([(Arg Nat, Term)]
 -> (Arg Term, Term)
 -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> [(Arg Nat, Term)]
-> [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [(Arg Nat, Term)]
-> (Arg Term, Term)
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
isVarOrIrrelevant []
  terms :: [Term]
terms = (Nat -> Term) -> [Nat] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Nat -> Term
var (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom (Args -> Nat
forall a. Sized a => a -> Nat
size Args
args))
  failure :: Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
c = do
    TCM () -> ExceptT InvertExcept (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m a -> ExceptT InvertExcept m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> ExceptT InvertExcept (TCMT IO) ())
-> TCM () -> ExceptT InvertExcept (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Nat
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
      [ TCMT IO Doc
"not all arguments are variables: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Args -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Args -> m Doc
prettyTCM Args
args
      , TCMT IO Doc
"  aborting assignment" ]
    InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. InvertExcept -> ExceptT InvertExcept (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Term -> InvertExcept
CantInvert Term
c)
  neutralArg :: ExceptT InvertExcept (TCMT IO) a
neutralArg = InvertExcept -> ExceptT InvertExcept (TCMT IO) a
forall a. InvertExcept -> ExceptT InvertExcept (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError InvertExcept
NeutralArg

  isVarOrIrrelevant :: Res -> (Arg Term, Term) -> ExceptT InvertExcept TCM Res
  isVarOrIrrelevant :: [(Arg Nat, Term)]
-> (Arg Term, Term)
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
isVarOrIrrelevant [(Arg Nat, Term)]
vars (Arg ArgInfo
info Term
v, Term
t) = do
    let irr :: Bool
irr | DontCare{} <- Term
v   = Bool
True
            | Bool
otherwise         = Bool
False
    ineg <- PrimitiveId -> ExceptT InvertExcept (TCMT IO) (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtinINeg
    case stripDontCare v of
      -- i := x
      Var Nat
i [] -> [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Arg Nat, Term)]
 -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a b. (a -> b) -> a -> b
$! (ArgInfo -> Nat -> Arg Nat
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Nat
i, Term
t) (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
forall a. a -> [a] -> [a]
: [(Arg Nat, Term)]
vars

      -- π i := x  try to eta-expand projection π away!
      Var Nat
i Elims
es | Just [(ProjOrigin, QName)]
qs <- (Elim -> Maybe (ProjOrigin, QName))
-> Elims -> Maybe [(ProjOrigin, QName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim Elims
es ->
        InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. InvertExcept -> ExceptT InvertExcept (TCMT IO) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a b. (a -> b) -> a -> b
$ ProjectedVar -> InvertExcept
ProjVar (ProjectedVar -> InvertExcept) -> ProjectedVar -> InvertExcept
forall a b. (a -> b) -> a -> b
$ Nat -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Nat
i [(ProjOrigin, QName)]
qs

      -- (i, j) := x  becomes  [i := fst x, j := snd x]
      -- Andreas, 2013-09-17 but only if constructor is fully applied
      tm :: Term
tm@(Con ConHead
c ConInfo
ci Elims
es) -> do
        let fallback :: ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
fallback
             | Term -> Bool
skip Term
tm           = [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Nat, Term)]
vars
             | Bool
otherwise         = Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
tm
        TCM (Maybe (QName, RecordData))
-> ExceptT InvertExcept (TCMT IO) (Maybe (QName, RecordData))
forall (m :: * -> *) a. Monad m => m a -> ExceptT InvertExcept m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (QName -> TCM (Maybe (QName, RecordData))
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isEtaRecordConstructor (QName -> TCM (Maybe (QName, RecordData)))
-> QName -> TCM (Maybe (QName, RecordData))
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
conName ConHead
c) ExceptT InvertExcept (TCMT IO) (Maybe (QName, RecordData))
-> (Maybe (QName, RecordData)
    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a b.
ExceptT InvertExcept (TCMT IO) a
-> (a -> ExceptT InvertExcept (TCMT IO) b)
-> ExceptT InvertExcept (TCMT IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          -- Andreas, 2019-11-10, issue #4185: only for eta-records
          Just (QName
_, RecordData{ _recFields :: RecordData -> [Dom QName]
_recFields = [Dom QName]
fs })
            | [Dom QName] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Dom QName]
fs Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Elims -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Elims
es -> do
              let aux :: Arg Term -> Dom QName -> (Arg Term, Term)
aux (Arg ArgInfo
_ Term
v) dom :: Dom QName
dom@(Dom QName -> QName
forall t e. Dom' t e -> e
unDom -> QName
f) = (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
v,) (Term -> (Arg Term, Term)) -> Term -> (Arg Term, Term)
forall a b. (a -> b) -> a -> b
$ Term
t Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
                    where
                    info' :: ArgInfo
info' = Dom QName
dom Dom QName -> Getting ArgInfo (Dom QName) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom QName) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo
                    ai :: ArgInfo
ai = ArgInfo
                      { argInfoHiding :: Hiding
argInfoHiding   = Hiding -> Hiding -> Hiding
forall a. Ord a => a -> a -> a
min (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info')
                      , argInfoOrigin :: Origin
argInfoOrigin   = Origin -> Origin -> Origin
forall a. Ord a => a -> a -> a
min (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info) (ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info')
                      , argInfoFreeVariables :: FreeVariables
argInfoFreeVariables = FreeVariables
unknownFreeVariables
                      }
                  vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
              res <- [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
loop ([(Arg Term, Term)]
 -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Dom QName -> (Arg Term, Term))
-> Args -> [Dom QName] -> [(Arg Term, Term)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' Arg Term -> Dom QName -> (Arg Term, Term)
aux Args
vs [Dom QName]
fs
              return $! res ++ vars
            | Bool
otherwise -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
fallback
          Maybe (QName, RecordData)
_ -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
fallback

      -- An irrelevant argument which is not an irrefutable pattern is dropped
      Term
_ | Bool
irr -> [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Nat, Term)]
vars

      -- Distinguish args that can be eliminated (Con,Lit,Lam,unsure) ==> failure
      -- from those that can only put somewhere as a whole ==> neutralArg
      Var{}      -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg

      -- primINeg i := x becomes i := primINeg x
      -- (primINeg is a definitional involution)
      Def QName
qn Elims
es | Just [Arg ArgInfo
_ (Var Nat
i [])] <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, QName -> Maybe QName
forall a. a -> Maybe a
Just QName
qn Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
ineg ->
        [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Arg Nat, Term)]
 -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)])
-> [(Arg Nat, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> Nat -> Arg Nat
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Nat
i, QName -> Elims -> Term
Def QName
qn [Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
t)]) (Arg Nat, Term) -> [(Arg Nat, Term)] -> [(Arg Nat, Term)]
forall a. a -> [a] -> [a]
: [(Arg Nat, Term)]
vars

      Def{}      -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg  -- Note that this Def{} is in normal form and might be prunable.
      tm :: Term
tm@Lam{}   -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
tm
      tm :: Term
tm@Lit{}   -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
tm
      tm :: Term
tm@MetaV{} -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
failure Term
tm
      Pi{}       -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
      Sort{}     -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
      Level{}    -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
      DontCare{} -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Ruled out by stripDontCare
      Dummy DummyTermKind
s Elims
_  -> [Char] -> ExceptT InvertExcept (TCMT IO) [(Arg Nat, Term)]
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> [Char]
forall a. Show a => a -> [Char]
show DummyTermKind
s)

-- | If the given metavariable application represents a face, return:
--
--    * The metavariable information;
--    * The actual face, as an assignment of booleans to variables;
--
--    * The substitution candidate resulting from @inverseSubst'@. This
--    is guaranteed to be linear and deterministic.
--
--    * The actual substitution, mapping from the constraint context to
--    the metavariable's context.
--
--  Put concisely, a face constraint is an equation in the pattern
--  fragment modulo the presence of endpoints (@i0@ and @i1@) in the
--  telescope. In more detail, a face constraint has the form
--
--    @?0 Δ (i = i0) (j = i0) Γ (k = i1) Θ (l = i0) = t@
--
--  where all the greek letters consist entirely of distinct bound
--  variables (and, of course, arbitrarily many endpoints are allowed
--  between each substitution fragment).
isFaceConstraint
  :: MetaId
  -> Args
  -> TCM (Maybe (MetaVariable, IntMap.IntMap Bool, SubstCand, Substitution))
isFaceConstraint :: MetaId
-> Args
-> TCM
     (Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution))
isFaceConstraint MetaId
mid Args
args = MaybeT
  (TCMT IO) (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)
-> TCM
     (Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
   (TCMT IO) (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)
 -> TCM
      (Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)))
-> MaybeT
     (TCMT IO) (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution)
-> TCM
     (Maybe (MetaVariable, IntMap Bool, [(Nat, Term)], Substitution))
forall a b. (a -> b) -> a -> b
$ do
  iv   <- MaybeT (TCMT IO) (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  mvar <- lookupLocalMeta mid  -- information associated with meta x
  -- Make sure that this is actually an interaction point:
  (_, _, _) <- MaybeT $ isInteractionMetaB mid args

  let
    t = Judgement MetaId -> Teletype
forall a. Judgement a -> Teletype
jMetaType (Judgement MetaId -> Teletype) -> Judgement MetaId -> Teletype
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mvar
    n = Args -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args

    isEndpoint Term
tm = Maybe (Nat, Bool) -> Bool
forall a. Maybe a -> Bool
isJust (Arg Term -> Nat -> Maybe (Nat, Bool)
fin (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
tm) Nat
0)

    fin (Arg ArgInfo
_ Term
tm) Nat
i = case Term -> IntervalView
iv Term
tm of
      IntervalView
IOne  -> (Nat, Bool) -> Maybe (Nat, Bool)
forall a. a -> Maybe a
Just (Nat
i, Bool
True)
      IntervalView
IZero -> (Nat, Bool) -> Maybe (Nat, Bool)
forall a. a -> Maybe a
Just (Nat
i, Bool
False)
      IntervalView
_     -> Maybe (Nat, Bool)
forall a. Maybe a
Nothing

  m           <- getContextSize
  TelV tel' _ <- teleViewUpToPath n t

  -- The logic here is essentially the same as for actually solving the
  -- meta.. We just return the pieces instead of doing the assignment.
  -- We must check the "face condition" (the relaxed pattern condition)
  -- and check linearity of the substitution candidate, otherwise the
  -- equation can't be inverted into a face constraint.
  sub <- MaybeT $ either (const Nothing) Just <$> runExceptT
    (inverseSubst' isEndpoint tel' args)
  ids <- MaybeT $ either (const Nothing) Just <$> runExceptT
    (checkLinearity sub)

  tel''       <- enterClosure mvar $ \Range
_ -> MaybeT (TCMT IO) (Tele (Dom Type))
forall (m :: * -> *). MonadTCEnv m => m (Tele (Dom Type))
getContextTelescope

  let
    assocToList Nat
i = \case
      [(Nat, Term)]
_           | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
>= Nat
m -> []
      ((Nat
j,Term
u) : [(Nat, Term)]
l) | Nat
i Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
j -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
u  Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [(Nat, Term)]
l
      [(Nat, Term)]
l                    -> Maybe Term
forall a. Maybe a
Nothing Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [(Nat, Term)]
l
    ivs = Nat -> [(Nat, Term)] -> [Maybe Term]
assocToList Nat
0 [(Nat, Term)]
ids
    rho = Impossible -> [Maybe Term] -> Substitution -> Substitution
forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
HasCallStack => Impossible
impossible [Maybe Term]
ivs (Substitution -> Substitution) -> Substitution -> Substitution
forall a b. (a -> b) -> a -> b
$ Nat -> Substitution
forall a. Nat -> Substitution' a
raiseS Nat
n

    over  = Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel' Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Tele (Dom Type) -> Nat
forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel''
    endps = [(Nat, Bool)] -> IntMap Bool
forall a. [(Nat, a)] -> IntMap a
IntMap.fromList ([(Nat, Bool)] -> IntMap Bool) -> [(Nat, Bool)] -> IntMap Bool
forall a b. (a -> b) -> a -> b
$ [Maybe (Nat, Bool)] -> [(Nat, Bool)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Nat, Bool)] -> [(Nat, Bool)])
-> [Maybe (Nat, Bool)] -> [(Nat, Bool)]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Nat -> Maybe (Nat, Bool))
-> Args -> [Nat] -> [Maybe (Nat, Bool)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' (\Arg Term
a Nat
i -> Arg Term -> Nat -> Maybe (Nat, Bool)
fin Arg Term
a (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
over)) Args
args (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n)

  reportSDoc "tc.ip.boundary" 45 $ vcat
    [ "ivs   =" <+> prettyTCM ivs
    , "tel'  =" <+> prettyTCM tel'
    , "tel'' =" <+> prettyTCM tel''
    , "ids   =" <+> prettyTCM ids
    , "sub   =" <+> prettyTCM sub
    , "endps =" <+> pretty endps
    ]

  guard (not (IntMap.null endps))
  -- Can happen when the metavariable's context does not yet know about
  -- an interval variable it will be applied to later, eg in the partial
  -- argument to hcomp:
  guard (all (>= 0) (IntMap.keys endps))
  -- In that case we fail here — when the user writes some more
  -- patterns, they'll become positive
  pure (mvar, endps, ids, rho)

-- | Record a "face" equation onto an interaction point into the actual
-- interaction point boundary. Takes all the same arguments as
-- @assignMeta'@.
tryAddBoundary :: CompareDirection -> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
tryAddBoundary :: CompareDirection
-> MetaId -> InteractionId -> Args -> Term -> CompareAs -> TCM ()
tryAddBoundary CompareDirection
dir MetaId
x InteractionId
iid Args
args Term
v CompareAs
target = do
  [Char] -> Nat -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.ip.boundary" Nat
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"boundary: looking at equational constraint"
    , Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (MetaId -> Elims -> Term
MetaV MetaId
x (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Args -> Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Args
args)) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"=?" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
    ]
  iv   <- TCMT IO (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  mvar <- lookupLocalMeta x  -- information associated with meta x

  let
    t = Judgement MetaId -> Teletype
forall a. Judgement a -> Teletype
jMetaType (Judgement MetaId -> Teletype) -> Judgement MetaId -> Teletype
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mvar
    n = Args -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length Args
args
    rhsv = Term -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Term
v

    allVars :: SubstCand -> Bool
    allVars [(Nat, Term)]
sub = VarSet
rhsv VarSet -> VarSet -> Bool
`VarSet.isSubsetOf` [Nat] -> VarSet
VarSet.fromList (((Nat, Term) -> Nat) -> [(Nat, Term)] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map' (Nat, Term) -> Nat
forall a b. (a, b) -> a
fst [(Nat, Term)]
sub)

  TelV tel' _ <- teleViewUpToPath n t

  void . runMaybeT $ do
    -- Make sure we're looking at a face constraint:
    (_, endps, ids, rho) <- MaybeT $ isFaceConstraint x args
    -- And that the non-endpoint parts of the 'Args' cover the free
    -- variables of the RHS:
    guard (allVars ids)

    -- ρ is a substitution from the "constraint context" (the context
    -- we're in) to the metavariable's context. moreover, v[ρ] is
    -- well-scoped in the meta's context.
    let v' = Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel' (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg Term)
rho Term
v
    -- We store the boundary faces directly as lambdas for simplicity.

    enterClosure mvar $ \Range
_ -> do
      [Char] -> Nat -> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.ip.boundary" Nat
30 (TCMT IO Doc -> MaybeT (TCMT IO) ())
-> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
        [ TCMT IO Doc
"recovered interaction point boundary"
        , TCMT IO Doc
"  endps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> IntMap Bool -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty IntMap Bool
endps
        , TCMT IO Doc
"  rho   =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Substitution -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution
rho
        , TCMT IO Doc
"  t     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Teletype -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Teletype -> m Doc
prettyTCM Teletype
t)
        , TCMT IO Doc
"  v'    =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v')
        ]

      let
        -- Always store the constraint with the smaller termSize:
        upd :: IPBoundary' Term -> IPBoundary' Term
upd (IPBoundary Map (IntMap Bool) Term
m) = case IntMap Bool -> Map (IntMap Bool) Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
MapS.lookup IntMap Bool
endps Map (IntMap Bool) Term
m of
          Just Term
t -> if Term -> Nat
forall a. TermSize a => a -> Nat
termSize Term
t Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Term -> Nat
forall a. TermSize a => a -> Nat
termSize Term
v'
            then Map (IntMap Bool) Term -> IPBoundary' Term
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary Map (IntMap Bool) Term
m
            else Map (IntMap Bool) Term -> IPBoundary' Term
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary (Map (IntMap Bool) Term -> IPBoundary' Term)
-> Map (IntMap Bool) Term -> IPBoundary' Term
forall a b. (a -> b) -> a -> b
$ IntMap Bool
-> Term -> Map (IntMap Bool) Term -> Map (IntMap Bool) Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert IntMap Bool
endps Term
v' Map (IntMap Bool) Term
m
          Maybe Term
Nothing -> Map (IntMap Bool) Term -> IPBoundary' Term
forall t. Map (IntMap Bool) t -> IPBoundary' t
IPBoundary (Map (IntMap Bool) Term -> IPBoundary' Term)
-> Map (IntMap Bool) Term -> IPBoundary' Term
forall a b. (a -> b) -> a -> b
$ IntMap Bool
-> Term -> Map (IntMap Bool) Term -> Map (IntMap Bool) Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
MapS.insert IntMap Bool
endps Term
v' Map (IntMap Bool) Term
m
        f :: InteractionPoint -> InteractionPoint
f InteractionPoint
ip = InteractionPoint
ip{ ipBoundary = upd (ipBoundary ip) }

      TCM () -> MaybeT (TCMT IO) ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> MaybeT (TCMT IO) ()) -> TCM () -> MaybeT (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ (InteractionPoints -> InteractionPoints) -> TCM ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(InteractionPoints -> InteractionPoints) -> m ()
modifyInteractionPoints ((InteractionPoint -> InteractionPoint)
-> InteractionId -> InteractionPoints -> InteractionPoints
forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(v -> v) -> k -> BiMap k v -> BiMap k v
BiMap.adjust InteractionPoint -> InteractionPoint
f InteractionId
iid)

-- | Turn open metas into postulates.
--
--   Preconditions:
--
--   1. We are 'inTopContext'.
--
--   2. 'envCurrentModule' is set to the top-level module.
--
openMetasToPostulates' :: (MetaId -> MetaVariable -> Bool) -> TCM ()
openMetasToPostulates' :: (MetaId -> MetaVariable -> Bool) -> TCM ()
openMetasToPostulates' MetaId -> MetaVariable -> Bool
freeze = do
  m <- Lens' TCEnv ModuleName -> TCMT IO ModuleName
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (ModuleName -> f ModuleName) -> TCEnv -> f TCEnv
Lens' TCEnv ModuleName
eCurrentModule

  -- Go through all open metas.
  ms <- MapS.assocs . MapS.filterWithKey freeze <$> useTC stOpenMetaStore
  forM_ ms $ \ (MetaId
x, MetaVariable
mv) -> do
    let t :: Type
t = Teletype -> Type
dummyTypeToOmega (Teletype -> Type) -> Teletype -> Type
forall a b. (a -> b) -> a -> b
$ Judgement MetaId -> Teletype
forall a. Judgement a -> Teletype
jMetaType (Judgement MetaId -> Teletype) -> Judgement MetaId -> Teletype
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv

    -- Create a name for the new postulate.
    let r :: Range
r = Closure Range -> Range
forall a. Closure a -> a
clValue (Closure Range -> Range) -> Closure Range -> Range
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Closure Range
miClosRange (MetaInfo -> Closure Range) -> MetaInfo -> Closure Range
forall a b. (a -> b) -> a -> b
$ MetaVariable -> MetaInfo
mvInfo MetaVariable
mv
    s' <- [Char] -> ShortText
TS.pack ([Char] -> ShortText) -> (Doc -> [Char]) -> Doc -> ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
forall a. Doc a -> [Char]
render (Doc -> ShortText) -> TCMT IO Doc -> TCMT IO ShortText
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x -- Using _ is a bad idea, as it prints as prefix op
    let s = ShortText
"unsolved#meta." ShortText -> ShortText -> ShortText
forall a. Semigroup a => a -> a -> a
<> (Char -> Bool) -> ShortText -> ShortText
TS.filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') ShortText
s'
    n <- freshName r s
    let q = ModuleName -> Name -> QName
A.QName ModuleName
m Name
n

    -- Debug.
    reportSDoc "meta.postulate" 20 $ vcat
      [ text ("Turning " ++! if isSortMeta_ mv then "sort" else "value" ++! " meta ")
          <+> prettyTCM x <+> " into postulate."
      , nest 2 $ vcat
        [ "Name: " <+> prettyTCM q
        , "Type: " <+> prettyTCM t
        ]
      ]

    -- Add the new postulate to the signature.
    addConstant' q defaultArgInfo t defaultAxiom

    -- Solve the meta.
    let inst = Instantiation -> MetaInstantiation
InstV (Instantiation -> MetaInstantiation)
-> Instantiation -> MetaInstantiation
forall a b. (a -> b) -> a -> b
$ Instantiation
                 { instTel :: [Arg ShortText]
instTel = [], instBody :: Term
instBody = QName -> Elims -> Term
Def QName
q [] }
    updateMetaVar x $ \ MetaVariable
mv0 -> MetaVariable
mv0 { mvInstantiation = inst }
    return ()
  where
    -- Unsolved sort metas can have a type ending in a Dummy if they are allowed to be instantiated
    -- to Typeω. This will crash the serializer (issue #3730). To avoid this we replace dummy type
    -- codomains by Typeω.
    dummyTypeToOmega :: Teletype -> Type
dummyTypeToOmega Teletype
t = case Teletype -> (Tele (Dom Type), Type)
unpackTeletype Teletype
t of
      (Tele (Dom Type)
tel, El Sort
_ Dummy{}) -> Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort
forall t. Univ -> Integer -> Sort' t
Inf Univ
UType Integer
0)
      (Tele (Dom Type), Type)
_ -> HasCallStack => Teletype -> Args -> Type
Teletype -> Args -> Type
teleApply Teletype
t []

openMetasToPostulates :: TCM ()
openMetasToPostulates :: TCM ()
openMetasToPostulates = (MetaId -> MetaVariable -> Bool) -> TCM ()
openMetasToPostulates' \MetaId
_ MetaVariable
_ -> Bool
True

-- | Sort metas in dependency order.
dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])
dependencySortMetas :: [MetaId] -> TCM (Maybe [MetaId])
dependencySortMetas [MetaId]
metas = do
  metaGraph <- [[(MetaId, MetaId)]] -> [(MetaId, MetaId)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(MetaId, MetaId)]] -> [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]] -> TCMT IO [(MetaId, MetaId)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [MetaId]
-> (MetaId -> TCMT IO [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [MetaId]
metas ((MetaId -> TCMT IO [(MetaId, MetaId)])
 -> TCMT IO [[(MetaId, MetaId)]])
-> (MetaId -> TCMT IO [(MetaId, MetaId)])
-> TCMT IO [[(MetaId, MetaId)]]
forall a b. (a -> b) -> a -> b
$ \ MetaId
m -> do
      deps <- (MetaId -> Set MetaId) -> Maybe Teletype -> Set MetaId
forall m. Monoid m => (MetaId -> m) -> Maybe Teletype -> m
forall t m. (AllMetas t, Monoid m) => (MetaId -> m) -> t -> m
allMetas (\MetaId
m' -> if MetaId
m' MetaId -> Set MetaId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set MetaId
metas'
                               then MetaId -> Set MetaId
forall el coll. Singleton el coll => el -> coll
singleton MetaId
m'
                               else Set MetaId
forall a. Monoid a => a
mempty) (Maybe Teletype -> Set MetaId)
-> TCMT IO (Maybe Teletype) -> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                MetaId -> TCMT IO (Maybe Teletype)
forall {m :: * -> *}. MonadReduce m => MetaId -> m (Maybe Teletype)
getType MetaId
m
      return [ (m, m') | m' <- Set.toList deps ]

  return $! Graph.topSort metas' metaGraph

  where
    metas' :: Set MetaId
metas' = [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList [MetaId]
metas

    -- Sort metas don't have types, but we still want to sort them.
    getType :: MetaId -> m (Maybe Teletype)
getType MetaId
m = do
      j <- MetaId -> m (Judgement MetaId)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Judgement MetaId)
lookupMetaJudgement MetaId
m
      case j of
        IsSort{}                 -> Maybe Teletype -> m (Maybe Teletype)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Teletype
forall a. Maybe a
Nothing
        HasType{ jMetaType :: forall a. Judgement a -> Teletype
jMetaType = Teletype
t } -> Teletype -> Maybe Teletype
forall a. a -> Maybe a
Just (Teletype -> Maybe Teletype) -> m Teletype -> m (Maybe Teletype)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Teletype -> m Teletype
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Teletype
t