{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.MetaVars where

import Prelude hiding (null)

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

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

import Agda.Interaction.Options

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

import Agda.TypeChecking.Monad
-- import Agda.TypeChecking.Monad.Builtin
-- import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Substitute
import qualified Agda.TypeChecking.SyntacticEquality as SynEq
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Free
import Agda.TypeChecking.Lock
import Agda.TypeChecking.Level (levelType)
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.SizedTypes (boundedSizeMetaHook, isSizeProblem)
import {-# SOURCE #-} Agda.TypeChecking.CheckInternal
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import Agda.TypeChecking.Warnings (warning)

-- import Agda.TypeChecking.CheckInternal
-- import {-# SOURCE #-} Agda.TypeChecking.CheckInternal (checkInternal)
import Agda.TypeChecking.MetaVars.Occurs

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

import Agda.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 -> [Arg Term] -> Term -> CompareAs -> TCM ()
assignV CompareDirection
dir MetaId
x [Arg Term]
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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
args) Term
v (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ CompareDirection
-> MetaId -> [Arg Term] -> Term -> CompareAs -> TCM ()
assign CompareDirection
dir MetaId
x [Arg Term]
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 [Char]] -> Term -> TCM ()
assignTerm' MetaId
m [Arg [Char]]
tel Term
v = TCM () -> TCM () -> TCM ()
forall a. TCM a -> TCM a -> TCM a
ifImpureConv (MetaId -> [Arg [Char]] -> Term -> TCM ()
assignTermTCM' MetaId
m [Arg [Char]]
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 Int
findIdx [a]
vs a
v = a -> [a] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
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] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.blocked" Int
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 [Char]] -> Term -> TCM ()
assignTerm MetaId
x [Arg [Char]]
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 [Char]] -> Term -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> [Arg [Char]] -> Term -> m ()
assignTerm' MetaId
x [Arg [Char]]
tel Term
v

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

    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Int
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' Term (Type'' Term Term)] -> 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' Term (Type'' Term Term)] -> m a -> m a
addContext (Arg [Char] -> Dom' Term (Type'' Term Term)
dummyFromArg (Arg [Char] -> Dom' Term (Type'' Term Term))
-> [Arg [Char]] -> [Dom' Term (Type'' Term Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg [Char]]
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)
      , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"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 [Char] -> TCMT IO Doc) -> [Arg [Char]] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Arg [Char] -> [Char]) -> Arg [Char] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg [Char] -> [Char]
forall e. Arg e -> e
unArg) [Arg [Char]]
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
             }
         }
    MetaId -> TCM ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
etaExpandListeners MetaId
x
    MetaId -> TCM ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
wakeupConstraints MetaId
x
    [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Int
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 cannot be instantiated with 'Inf' (Setω).
newSortMetaBelowInf :: TCM Sort
newSortMetaBelowInf :: TCM (Sort' Term)
newSortMetaBelowInf = do
  x <- TCM (Sort' Term)
newSortMeta
  hasBiggerSort x
  return x

-- | Create a sort meta that may be instantiated with 'Inf' (Setω).
newSortMeta :: TCM Sort
newSortMeta :: TCM (Sort' Term)
newSortMeta =
  TCM Bool
-> TCM (Sort' Term) -> TCM (Sort' Term) -> TCM (Sort' Term)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism ([Arg Term] -> TCM (Sort' Term)
forall (m :: * -> *).
MonadMetaSolver m =>
[Arg Term] -> m (Sort' Term)
newSortMetaCtx ([Arg Term] -> TCM (Sort' Term))
-> TCMT IO [Arg Term] -> TCM (Sort' Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [Arg Term]
forall (m :: * -> *). MonadTCEnv m => m [Arg Term]
getContextArgs)
  -- else (no universe polymorphism)
  (TCM (Sort' Term) -> TCM (Sort' Term))
-> TCM (Sort' Term) -> TCM (Sort' Term)
forall a b. (a -> b) -> a -> b
$ do i   <- TCMT IO MetaInfo
forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
       let j = () -> Type'' Term Term -> Judgement ()
forall a. a -> Type'' Term Term -> Judgement a
IsSort () Type'' Term Term
HasCallStack => Type'' Term Term
__DUMMY_TYPE__
       x   <- newMeta Instantiable i normalMetaPriority (idP 0) j
       reportSDoc "tc.meta.new" 50 $
         "new sort meta" <+> prettyTCM x
       return $! MetaS x []

-- | Create a sort meta that may be instantiated with 'Inf' (Setω).
newSortMetaCtx :: MonadMetaSolver m => Args -> m Sort
newSortMetaCtx :: forall (m :: * -> *).
MonadMetaSolver m =>
[Arg Term] -> m (Sort' Term)
newSortMetaCtx [Arg Term]
vs = do
    i   <- m MetaInfo
forall (m :: * -> *). (MonadTCEnv m, ReadTCState m) => m MetaInfo
createMetaInfo
    tel <- getContextTelescope
    let t = Tele (Dom' Term (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
telePi_ Tele (Dom' Term (Type'' Term Term))
tel Type'' Term Term
HasCallStack => Type'' Term Term
__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' Term -> TCM (Type'' Term Term)
newTypeMeta' Comparison
cmp Sort' Term
s = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type'' Term Term)
-> ((MetaId, Term) -> Term) -> (MetaId, Term) -> Type'' Term Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId, Term) -> Term
forall a b. (a, b) -> b
snd ((MetaId, Term) -> Type'' Term Term)
-> TCMT IO (MetaId, Term) -> TCM (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RunMetaOccursCheck
-> Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
cmp (Sort' Term -> Type'' Term Term
sort Sort' Term
s)

newTypeMeta :: Sort -> TCM Type
newTypeMeta :: Sort' Term -> TCM (Type'' Term Term)
newTypeMeta = Comparison -> Sort' Term -> TCM (Type'' Term Term)
newTypeMeta' Comparison
CmpLeq

newTypeMeta_ ::  TCM Type
newTypeMeta_ :: TCM (Type'' Term Term)
newTypeMeta_  = Comparison -> Sort' Term -> TCM (Type'' Term Term)
newTypeMeta' Comparison
CmpEq (Sort' Term -> TCM (Type'' Term Term))
-> TCM (Sort' Term) -> TCM (Type'' Term Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCM (Sort' Term) -> TCM (Sort' Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM (Sort' Term) -> TCM (Sort' Term))
-> TCM (Sort' Term) -> TCM (Sort' Term)
forall a b. (a -> b) -> a -> b
$ TCM (Sort' Term)
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'' Term Term -> TCMT IO (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpEq (Type'' Term Term -> TCMT IO (MetaId, Term))
-> TCM (Type'' Term Term) -> TCMT IO (MetaId, Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM (Type'' Term Term)
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
m (Type'' Term Term)
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 :: [Char] -> Type'' Term Term -> TCMT IO (MetaId, Term)
newInstanceMeta [Char]
s Type'' Term Term
t = do
  vs  <- TCMT IO [Arg Term]
forall (m :: * -> *). MonadTCEnv m => m [Arg Term]
getContextArgs
  ctx <- getContextTelescope
  newInstanceMetaCtx s (telePi_ ctx t) vs

newInstanceMetaCtx :: MetaNameSuggestion -> Type -> Args -> TCM (MetaId, Term)
newInstanceMetaCtx :: [Char] -> Type'' Term Term -> [Arg Term] -> TCMT IO (MetaId, Term)
newInstanceMetaCtx [Char]
s Type'' Term Term
t [Arg Term]
vs = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.new" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
    [ TCMT IO Doc
"new instance meta:"
    , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
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 _ <- telView t
  let perm = Int -> Permutation
idP (Tele (Dom' Term (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term (Type'' Term Term))
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
-> [Char]
-> Comparison
-> Type'' Term Term
-> TCMT IO (MetaId, Term)
newNamedValueMeta RunMetaOccursCheck
b [Char]
s Comparison
cmp Type'' Term Term
t = do
  (x, v) <- RunMetaOccursCheck
-> Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newValueMeta RunMetaOccursCheck
b Comparison
cmp Type'' Term Term
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
-> [Char]
-> Comparison
-> Type'' Term Term
-> TCMT IO (MetaId, Term)
newNamedValueMeta' RunMetaOccursCheck
b [Char]
s Comparison
cmp Type'' Term Term
t = do
  (x, v) <- RunMetaOccursCheck
-> Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newValueMeta' RunMetaOccursCheck
b Comparison
cmp Type'' Term Term
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'' Term Term
-> TCMT IO (MetaId, Term)
newValueMetaOfKind MetaInfo
info = case MetaInfo -> MetaKind
A.metaKind MetaInfo
info of
  MetaKind
UnificationMeta -> RunMetaOccursCheck
-> Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newValueMeta
  MetaKind
InstanceMeta -> \ RunMetaOccursCheck
_run Comparison
_cmp -> [Char] -> Type'' Term Term -> TCMT IO (MetaId, Term)
newInstanceMeta (MetaInfo -> [Char]
A.metaNameSuggestion MetaInfo
info)

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

newValueMetaCtx ::
  Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> TCM (MetaId, Term)
newValueMetaCtx :: Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO (MetaId, Term)
newValueMetaCtx Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type'' Term Term
t Tele (Dom' Term (Type'' Term Term))
tel Permutation
perm [Arg Term]
ctx =
  (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'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO (MetaId, Term)
newValueMetaCtx' Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type'' Term Term
t Tele (Dom' Term (Type'' Term Term))
tel Permutation
perm [Arg Term]
ctx

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

newValueMetaCtx' ::
  Frozen -> RunMetaOccursCheck -> Comparison -> Type -> Telescope -> Permutation -> Args -> TCM (MetaId, Term)
newValueMetaCtx' :: Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO (MetaId, Term)
newValueMetaCtx' Frozen
frozen RunMetaOccursCheck
b Comparison
cmp Type'' Term Term
a Tele (Dom' Term (Type'' Term Term))
tel Permutation
perm [Arg Term]
vs = do
  i <- RunMetaOccursCheck -> TCMT IO MetaInfo
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
RunMetaOccursCheck -> m MetaInfo
createMetaInfo' RunMetaOccursCheck
b
  let t     = Tele (Dom' Term (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
telePi_ Tele (Dom' Term (Type'' Term Term))
tel Type'' Term Term
a
  x <- newMeta frozen i normalMetaPriority perm (HasType () cmp t)
  modality <- currentModality
  reportSDoc "tc.meta.new" 50 $ fsep
    [ text $ "new meta (" ++! show (i ^. lensIsAbstract) ++! "):"
    , nest 2 $ prettyTCM vs <+> "|-"
    , nest 2 $ pretty x <+> ":" <+> pretty modality <+> 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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
vs
  boundedSizeMetaHook u tel a
  return (x, u)

newTelMeta :: Telescope -> TCM Args
newTelMeta :: Tele (Dom' Term (Type'' Term Term)) -> TCMT IO [Arg Term]
newTelMeta Tele (Dom' Term (Type'' Term Term))
tel = Type'' Term Term -> TCMT IO [Arg Term]
newArgsMeta (Tele (Dom' Term (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
forall t.
Abstract t =>
Tele (Dom' Term (Type'' Term Term)) -> t -> t
abstract Tele (Dom' Term (Type'' Term Term))
tel (Type'' Term Term -> Type'' Term Term)
-> Type'' Term Term -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ Type'' Term Term
HasCallStack => Type'' Term Term
__DUMMY_TYPE__)

type Condition = Dom Type -> Abs Type -> Bool

trueCondition :: Condition
trueCondition :: Condition
trueCondition Dom' Term (Type'' Term Term)
_ Abs (Type'' Term Term)
_ = Bool
True

newArgsMeta :: Type -> TCM Args
newArgsMeta :: Type'' Term Term -> TCMT IO [Arg Term]
newArgsMeta = Condition -> Type'' Term Term -> TCMT IO [Arg Term]
newArgsMeta' Condition
trueCondition

newArgsMeta' :: Condition -> Type -> TCM Args
newArgsMeta' :: Condition -> Type'' Term Term -> TCMT IO [Arg Term]
newArgsMeta' Condition
condition Type'' Term Term
t = do
  args <- TCMT IO [Arg Term]
forall (m :: * -> *). MonadTCEnv m => m [Arg Term]
getContextArgs
  tel  <- getContextTelescope
  newArgsMetaCtx' Instantiable condition t tel (idP $ size tel) args

newArgsMetaCtx :: Type -> Telescope -> Permutation -> Args -> TCM Args
newArgsMetaCtx :: Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO [Arg Term]
newArgsMetaCtx = Frozen
-> Condition
-> Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO [Arg Term]
newArgsMetaCtx' Frozen
Instantiable Condition
trueCondition

newArgsMetaCtx'' :: MetaNameSuggestion -> Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> TCM Args
newArgsMetaCtx'' :: [Char]
-> Frozen
-> Condition
-> Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO [Arg Term]
newArgsMetaCtx'' [Char]
pref Frozen
frozen Condition
condition (El Sort' Term
s Term
tm) Tele (Dom' Term (Type'' Term Term))
tel Permutation
perm [Arg Term]
ctx = do
  tm <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
tm
  case tm of
    Pi dom :: Dom' Term (Type'' Term Term)
dom@(Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom -> Type'' Term Term
a) Abs (Type'' Term Term)
codom | Condition
condition Dom' Term (Type'' Term Term)
dom Abs (Type'' Term Term)
codom -> do
      let info :: ArgInfo
info = (Dom' Term (Type'' Term Term)
dom Dom' Term (Type'' Term Term)
-> Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
-> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo)
          mod :: Modality
mod  = ArgInfo -> Modality
forall a. LensModality a => a -> Modality
getModality (Dom' Term (Type'' Term Term)
dom Dom' Term (Type'' Term Term)
-> Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
-> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom' Term (Type'' Term Term)) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo)
          -- Issue #3031: It's not enough to applyModalityToContext, since most (all?)
          -- of the context lives in tel. Don't forget the arguments in ctx.
          tel' :: Tele (Dom' Term (Type'' Term Term))
tel' = ListTel -> Tele (Dom' Term (Type'' Term Term))
telFromList (ListTel -> Tele (Dom' Term (Type'' Term Term)))
-> ListTel -> Tele (Dom' Term (Type'' Term Term))
forall a b. (a -> b) -> a -> b
$
                 (Dom ([Char], Type'' Term Term) -> Dom ([Char], Type'' Term Term))
-> ListTel -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map' (Modality
mod Modality
-> Dom ([Char], Type'' Term Term) -> Dom ([Char], Type'' Term Term)
forall a. LensModality a => Modality -> a -> a
`inverseApplyModalityButNotQuantity`) (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$
                 Tele (Dom' Term (Type'' Term Term)) -> ListTel
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom' Term (Type'' Term Term))
tel
          ctx' :: [Arg Term]
ctx' = (Arg Term -> Arg Term) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> [a] -> [b]
map' (Modality
mod Modality -> Arg Term -> Arg Term
forall a. LensModality a => Modality -> a -> a
`inverseApplyModalityButNotQuantity`) [Arg Term]
ctx
      (m, u) <- Dom' Term (Type'' Term Term)
-> TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term)
forall e a. Dom e -> TCM a -> TCM a
applyDomToContext Dom' Term (Type'' Term Term)
dom (TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term))
-> TCMT IO (MetaId, Term) -> TCMT IO (MetaId, Term)
forall a b. (a -> b) -> a -> b
$
                  Frozen
-> RunMetaOccursCheck
-> Comparison
-> Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO (MetaId, Term)
newValueMetaCtx Frozen
frozen RunMetaOccursCheck
RunMetaOccursCheck Comparison
CmpLeq Type'' Term Term
a Tele (Dom' Term (Type'' Term Term))
tel' Permutation
perm [Arg Term]
ctx'
      -- Jesper, 2021-05-05: When creating a metavariable from a
      -- generalizable variable, we must set the modality at which it
      -- will be generalized.  Don't do this for other metavariables,
      -- as they should keep the default modality (see #5363).
      whenM ((== YesGeneralizeVar) <$> viewTC eGeneralizeMetas) $
        setMetaGeneralizableArgInfo m $ hideOrKeepInstance info
      setMetaNameSuggestion m (suffixNameSuggestion pref (absName codom))
      args <- newArgsMetaCtx'' pref frozen condition (codom `absApp` u) tel perm ctx
      return $! Arg info u : args
    Term
_  -> [Arg Term] -> TCMT IO [Arg Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []

newArgsMetaCtx' :: Frozen -> Condition -> Type -> Telescope -> Permutation -> Args -> TCM Args
newArgsMetaCtx' :: Frozen
-> Condition
-> Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO [Arg Term]
newArgsMetaCtx' = [Char]
-> Frozen
-> Condition
-> Type'' Term Term
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO [Arg Term]
newArgsMetaCtx'' [Char]
forall a. Monoid a => a
mempty

-- | Create a metavariable of record type. This is actually one metavariable
--   for each field.
newRecordMeta :: QName -> Args -> TCM Term
newRecordMeta :: QName -> [Arg Term] -> TCMT IO Term
newRecordMeta QName
r [Arg Term]
pars = do
  args <- TCMT IO [Arg Term]
forall (m :: * -> *). MonadTCEnv m => m [Arg Term]
getContextArgs
  tel  <- getContextTelescope
  newRecordMetaCtx mempty Instantiable r pars tel (idP $ size tel) args

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 -> Permutation -> Args -> TCM Term
newRecordMetaCtx :: [Char]
-> Frozen
-> QName
-> [Arg Term]
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO Term
newRecordMetaCtx [Char]
pref Frozen
frozen QName
r [Arg Term]
pars Tele (Dom' Term (Type'' Term Term))
tel Permutation
perm [Arg Term]
ctx = 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' Term (Type'' Term Term))
-> [Arg Term] -> Tele (Dom' Term (Type'' Term Term))
forall t. Apply t => t -> [Arg Term] -> t
apply (RecordData -> Tele (Dom' Term (Type'' Term Term))
_recTel RecordData
rdef) [Arg Term]
pars
  fields <- newArgsMetaCtx'' pref frozen trueCondition
              (telePi_ ftel __DUMMY_TYPE__) tel perm ctx
  return $! Con con ConOSystem $! map' Apply fields

newQuestionMark :: InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark :: InteractionId
-> Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
newQuestionMark InteractionId
ii Comparison
cmp = (Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term))
-> InteractionId
-> Comparison
-> Type'' Term Term
-> TCMT IO (MetaId, Term)
newQuestionMark' (RunMetaOccursCheck
-> Comparison -> Type'' Term Term -> 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'' Term Term -> TCMT IO (MetaId, Term))
-> InteractionId
-> Comparison
-> Type'' Term Term
-> TCMT IO (MetaId, Term)
newQuestionMark' Comparison -> Type'' Term Term -> TCMT IO (MetaId, Term)
new InteractionId
ii Comparison
cmp Type'' Term Term
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'' Term Term -> TCMT IO (MetaId, Term)
new Comparison
cmp Type'' Term Term
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' ContextEntry -> [Name]
contextNames' Context' ContextEntry
gamma
    let dxs  = Context' ContextEntry -> [Name]
contextNames' Context' ContextEntry
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] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
gxs
    let dlen = [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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 Int
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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
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"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [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"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Name] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
dxs
            ]
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
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"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ([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"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ([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
$! (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Int -> Term
var [Int
dlen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
glen .. Int
dlen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

      -- Case: record variable in the context.
      Just Int
k -> do
        -- Verify that the contexts relate as expected.
        let g0len :: Int
g0len = [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
dxs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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 (Int
d2len, Int
g1len) = [Name] -> [Name] -> (Int, Int)
forall a. Eq a => [a] -> [a] -> (Int, Int)
findOverlap (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take' Int
k [Name]
dys) [Name]
gys
        [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.interaction" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (TCMT IO Doc -> TCMT IO Doc) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2)
          [ TCMT IO Doc
"k     =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
k
          , TCMT IO Doc
"glen  =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
glen
          , TCMT IO Doc
"g0len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
g0len
          , TCMT IO Doc
"g1len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
g1len
          , TCMT IO Doc
"d2len =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Int
d2len
          ]
        -- The Γ₀ part should match.
        Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop (Int
glen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
g0len) [Name]
gxs [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Name]
dxs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
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)"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [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)"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [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` Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take' Int
g1len) [Name]
gys (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop Int
d2len [Name]
dys) ) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
          [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
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)"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [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)"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [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) = Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt' Int
g1len ([Term] -> ([Term], [Term])) -> [Term] -> ([Term], [Term])
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Int -> Term
var [Int
d2len..Int
dlenInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
        -- We need to expand the record var @v@ into the correct number of fields.
        let numFields :: Int
numFields = Int
glen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
g1len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
g0len
        if Int
numFields Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
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'' Term Term
t = Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom (Dom' Term (Type'' Term Term) -> Type'' Term Term)
-> Dom' Term (Type'' Term Term) -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ ContextEntry -> Dom' Term (Type'' Term Term)
ctxEntryDom (ContextEntry -> Dom' Term (Type'' Term Term))
-> ContextEntry -> Dom' Term (Type'' Term Term)
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
$
                  Int -> Context' ContextEntry -> Maybe ContextEntry
cxLookup Int
k Context' ContextEntry
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
. Int -> [Dom QName] -> [Dom QName]
forall a. Int -> [a] -> [a]
take' Int
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'' Term Term -> TCMT IO [Dom QName]
Type'' Term Term -> TCMT IO [Dom QName]
getRecordTypeFields Type'' Term Term
t
          -- Check that the record field names match
          -- the supposed record field names from the context of the original meta.
          let gfs = Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take' Int
numFields (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop Int
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] -> [Arg Term] -> [Arg Term]
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) ([Arg Term] -> [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Context' ContextEntry -> [Arg Term]
contextArgs Context' ContextEntry
gamma
    -- Take the permutation into account (see TC.Monad.MetaVars.getMetaContextArgs).
    let vs = Permutation -> [Arg Term] -> [Arg Term]
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) Permutation
p) [Arg Term]
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'' Term Term -> TCMT IO Term -> TCMT IO Term
blockTerm Type'' Term Term
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 Term -> Term -> ProblemId -> TCMT IO Term
blockTermOnProblem Type'' Term Term
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 `or2M` isSizeProblem pid)
      (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 $ telePi_ 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'' Term Term -> ProblemId -> TCM (Type'' Term Term)
blockTypeOnProblem (El Sort' Term
s Term
a) ProblemId
pid = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type'' Term Term)
-> TCMT IO Term -> TCM (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type'' Term Term -> Term -> ProblemId -> TCMT IO Term
blockTermOnProblem (Sort' Term -> Type'' Term Term
sort Sort' Term
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'' Term Term -> TCM Blocker
unblockedTester Type'' Term Term
t = Type'' Term Term
-> (Blocker -> Type'' Term Term -> TCM Blocker)
-> (NotBlocked -> Type'' Term Term -> 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'' Term Term
t (\ Blocker
b Type'' Term Term
_ -> Blocker -> TCM Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
b) (\ NotBlocked
_ Type'' Term Term
_ -> 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 = do
  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 (CheckExpr Comparison
_ Expr
_ Type'' Term Term
t)         = Type'' Term Term -> TCM Blocker
unblockedTester Type'' Term Term
t
    unblock (CheckArgs Comparison
_ ExpandHidden
_ Expr
_ [NamedArg Expr]
_ Type'' Term Term
t Type'' Term Term
_ ArgsCheckState CheckedTarget -> TCMT IO Term
_) = Type'' Term Term -> TCM Blocker
unblockedTester Type'' Term Term
t  -- The type of the head of the application.
    unblock (CheckProjAppToKnownPrincipalArg Comparison
_ Expr
_ ProjOrigin
_ AmbiguousQName
_ Expr
_ [NamedArg Expr]
_ Type'' Term Term
_ Int
_ Term
_ Type'' Term Term
t PrincipalArgTypeMetas
_) = Type'' Term Term -> TCM Blocker
unblockedTester Type'' Term Term
t -- The type of the principal argument
    unblock (CheckLambda Comparison
_ Arg (List1 (WithHiding Name), Maybe (Type'' Term Term))
_ Expr
_ Type'' Term Term
t)     = Type'' Term Term -> TCM Blocker
unblockedTester Type'' Term Term
t
    unblock (DoQuoteTerm Comparison
_ Term
_ Type'' Term Term
_)       = 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.

-- | 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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"impossible" Int
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'' Term Term
problemType TypeCheckingProblem
p
  m   <- newMeta' (PostponedTypeCheckingProblem cl)
                  Instantiable i normalMetaPriority (idP (size tel))
         $ HasType () CmpLeq $ telePi_ tel t
  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'' Term Term
problemType (CheckExpr Comparison
_ Expr
_ Type'' Term Term
t         ) = Type'' Term Term
t
problemType (CheckArgs Comparison
_ ExpandHidden
_ Expr
_ [NamedArg Expr]
_ Type'' Term Term
_ Type'' Term Term
t ArgsCheckState CheckedTarget -> TCMT IO Term
_ ) = Type'' Term Term
t  -- The target type of the application.
problemType (CheckProjAppToKnownPrincipalArg Comparison
_ Expr
_ ProjOrigin
_ AmbiguousQName
_ Expr
_ [NamedArg Expr]
_ Type'' Term Term
t Int
_ Term
_ Type'' Term Term
_ PrincipalArgTypeMetas
_) = Type'' Term Term
t -- The target type of the application
problemType (CheckLambda Comparison
_ Arg (List1 (WithHiding Name), Maybe (Type'' Term Term))
_ Expr
_ Type'' Term Term
t     ) = Type'' Term Term
t
problemType (DoQuoteTerm Comparison
_ Term
_ Type'' Term Term
t)        = Type'' Term Term
t
problemType (DisambiguateConstructor (ConstructorDisambiguationData QName
_ List1 (QName, Type'' Term Term, ConHead)
_ [NamedArg Expr]
_ Type'' Term Term
t) ConHead -> TCMT IO Term
_) = Type'' Term Term
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] -> Int -> [Char] -> TCM () -> TCM ()
forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.meta.eta" Int
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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Int
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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Int
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 Type'' Term Term
a -> do

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

        TelV tel b <- Type'' Term Term -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type'' Term Term -> m (TelV (Type'' Term Term))
telView Type'' Term Term
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 (flattenTel 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 :: [Arg Term]
ps = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
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
$
                      [Char]
-> Frozen
-> QName
-> [Arg Term]
-> Tele (Dom' Term (Type'' Term Term))
-> Permutation
-> [Arg Term]
-> TCMT IO Term
newRecordMetaCtx (MetaInfo -> [Char]
miNameSuggestion (MetaVariable -> MetaInfo
mvInfo MetaVariable
meta))
                        (MetaVariable -> Frozen
mvFrozen MetaVariable
meta) QName
r [Arg Term]
ps Tele (Dom' Term (Type'' Term Term))
tel (Int -> Permutation
idP (Int -> Permutation) -> Int -> Permutation
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term (Type'' Term Term))
tel) ([Arg Term] -> TCMT IO Term) -> [Arg Term] -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term (Type'' Term Term)) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom' Term (Type'' Term Term))
tel
                    reportSDoc "tc.meta.eta" 15 $ sep
                        [ "eta expanding: " <+> pretty m <+> " --> "
                        , nest 2 $ prettyTCM u
                        ]
                    -- Andreas, 2019-03-18, AIM XXIX, issue #3597
                    -- When meta is frozen instantiate it with in-turn frozen metas.
                    inTopContext $ do
                      -- 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 -> [Arg Term] -> TCM Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
QName -> [Arg Term] -> m Bool
isSingletonRecord QName
r [Arg Term]
ps) TCM ()
expand TCM ()
dontExpand
                else TCM ()
dontExpand
            ) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ {- else -} TCM Bool -> TCM () -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([TCM Bool] -> TCM Bool
forall (f :: * -> *) (m :: * -> *).
(Foldable f, Monad m) =>
f (m Bool) -> m Bool
andM [ Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCM Bool) -> Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$! MetaClass
Levels MetaClass -> [MetaClass] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [MetaClass]
kinds
                            , TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
typeInType
                            , (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
lvl Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe Term -> Bool) -> TCMT IO (Maybe Term) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinLevel
                            ]) (do
              [Char] -> Int -> [Char] -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.eta" Int
20 ([Char] -> TCM ()) -> [Char] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Expanding level meta to 0 (type-in-type)"
              -- Andreas, 2012-03-30: No need for occurrence check etc.
              -- we directly assign the solution for the meta
              TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ MetaId -> [Arg [Char]] -> Term -> TCM ()
assignTerm MetaId
m (Tele (Dom' Term (Type'' Term Term)) -> [Arg [Char]]
forall a. TelToArgs a => a -> [Arg [Char]]
telToArgs Tele (Dom' Term (Type'' Term Term))
tel) (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Level -> Term
Level (Level -> Term) -> Level -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
           ) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ {- else -} 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] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.eta" Int
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

-- | Is the term an @rewrite function?
--   Does not need to do reduction because of syntactic restrictions on
--   the placement of @rewrite
isRewPi :: Term -> Bool
isRewPi :: Term -> Bool
isRewPi (Pi Dom' Term (Type'' Term Term)
a Abs (Type'' Term Term)
b) = Maybe (RewDom' Term) -> Bool
forall a. Maybe a -> Bool
isJust (Dom' Term (Type'' Term Term) -> Maybe (RewDom' Term)
forall t e. Dom' t e -> Maybe (RewDom' t)
rewDom Dom' Term (Type'' Term Term)
a) Bool -> Bool -> Bool
|| Term -> Bool
isRewPi (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl (Type'' Term Term -> Term) -> Type'' Term Term -> Term
forall a b. (a -> b) -> a -> b
$ Abs (Type'' Term Term) -> Type'' Term Term
forall a. Abs a -> a
unAbs Abs (Type'' Term Term)
b)
isRewPi Term
_        = Bool
False

{-# 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] -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Int
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] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"tc.meta.assign" Int
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

allRewDoms :: Tele (Dom Type) -> [RewDom]
allRewDoms :: Tele (Dom' Term (Type'' Term Term)) -> [RewDom' Term]
allRewDoms = (Dom' Term (Type'' Term Term) -> Maybe (RewDom' Term))
-> [Dom' Term (Type'' Term Term)] -> [RewDom' Term]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Dom' Term (Type'' Term Term) -> Maybe (RewDom' Term)
forall t e. Dom' t e -> Maybe (RewDom' t)
rewDom ([Dom' Term (Type'' Term Term)] -> [RewDom' Term])
-> (Tele (Dom' Term (Type'' Term Term))
    -> [Dom' Term (Type'' Term Term)])
-> Tele (Dom' Term (Type'' Term Term))
-> [RewDom' Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom' Term (Type'' Term Term))
-> [Dom' Term (Type'' Term Term)]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel

-- | Gets the set of variables constrained by local rewrite rules
--
--   We specifically care about variables that occur exactly as LHSs of local
--   rewrite rules. Unification problems under such local rewrite rules might
--   appear outside the pattern fragment after rewriting arguments, but if the
--   argument is constrained in the meta's context, we know it is uniquely
--   determined up to defeq and can proceed.
rewConstrained :: Tele (Dom Type) -> TCM VarSet
rewConstrained :: Tele (Dom' Term (Type'' Term Term)) -> TCM VarSet
rewConstrained Tele (Dom' Term (Type'' Term Term))
tel = TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
localRewritingOption TCM Bool -> (Bool -> TCM VarSet) -> TCM VarSet
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
  Bool
True  -> VarSet -> TCM VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarSet -> TCM VarSet) -> VarSet -> TCM VarSet
forall a b. (a -> b) -> a -> b
$! (RewDom' Term -> VarSet) -> [RewDom' Term] -> VarSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (RewriteRule -> VarSet
rewConstrained' (RewriteRule -> VarSet)
-> (RewDom' Term -> RewriteRule) -> RewDom' Term -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteRule -> Maybe RewriteRule -> RewriteRule
forall a. a -> Maybe a -> a
fromMaybe RewriteRule
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe RewriteRule -> RewriteRule)
-> (RewDom' Term -> Maybe RewriteRule)
-> RewDom' Term
-> RewriteRule
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewDom' Term -> Maybe RewriteRule
forall t. RewDom' t -> Maybe RewriteRule
rewDomRew) ([RewDom' Term] -> VarSet) -> [RewDom' Term] -> VarSet
forall a b. (a -> b) -> a -> b
$! Tele (Dom' Term (Type'' Term Term)) -> [RewDom' Term]
allRewDoms Tele (Dom' Term (Type'' Term Term))
tel
  Bool
False -> VarSet -> TCM VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarSet
forall a. Monoid a => a
mempty
  where
    rewConstrained' :: RewriteRule -> VarSet
    rewConstrained' :: RewriteRule -> VarSet
rewConstrained' (RewriteRule Tele (Dom' Term (Type'' Term Term))
EmptyTel (RewVarHead Int
x) [] Term
_ Type'' Term Term
_) =
      Int -> VarSet
VarSet.singleton Int
x
    rewConstrained' (RewriteRule Tele (Dom' Term (Type'' Term Term))
_ (RewVarHead Int
x) [] Term
_ Type'' Term Term
_) =
      VarSet
forall a. HasCallStack => a
__IMPOSSIBLE__
    rewConstrained' RewriteRule
_ =
      VarSet
VarSet.empty

-- | 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 -> [Arg Term] -> Term -> CompareAs -> TCM ()
assign CompareDirection
dir MetaId
x [Arg Term]
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 -> Type'' Term Term
forall a. Judgement a -> Type'' Term Term
jMetaType (Judgement MetaId -> Type'' Term Term)
-> Judgement MetaId -> Type'' Term Term
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: " <+> prettyTCM 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
      _ <- TCMT IO (Maybe Cubical) -> MaybeT (TCMT IO) Cubical
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
      (x, ip, args) <- MaybeT (isInteractionMetaB x args)
      lift $ tryAddBoundary dir x ip args v target

  case (v, mvJudgement mvar) of
      (Sort Sort' Term
s, HasType{}) -> Sort' Term -> TCM ()
hasBiggerSort Sort' Term
s
      (Term, Judgement MetaId)
_                   -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

  -- Instantiating metas with @rewrite functions is never allowed to ensure
  -- quantification is always prenex
  when (isRewPi v) $ do
    warning $ InferredLocalRewrite x v
    patternViolation neverUnblock

  -- 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.

  cumulativity <- optCumulativity <$> pragmaOptions

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

  case (target , mvJudgement mvar) of
    -- Case 1 (comparing term to meta as types)
    (AsTypes{}   , HasType MetaId
_ Comparison
cmp0 Type'' Term Term
t) -> do
        let cmp :: Comparison
cmp   = if Bool
cumulativity then Comparison
cmp0 else Comparison
CmpEq
            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 (Type'' Term Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type'' Term Term
t) -- TODO: make piApplyM' compute unblocker
        t' <- TCMT IO Empty
-> Type'' Term Term -> [Arg Term] -> TCM (Type'' Term Term)
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> [Arg Term] -> m (Type'' Term Term)
piApplyM' TCMT IO Empty
abort Type'' Term Term
t [Arg Term]
args
        s <- shouldBeSort t'
        checkSolutionSort cmp s v

    -- Case 2 (comparing term to type-level meta as terms, with --cumulativity)
    (AsTermsOf{} , HasType MetaId
_ Comparison
cmp Type'' Term Term
t)
      | Bool
cumulativity -> 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 (Type'' Term Term -> Blocker
forall t. AllMetas t => t -> Blocker
unblockOnAnyMetaIn Type'' Term Term
t)
          t' <- TCMT IO Empty
-> Type'' Term Term -> [Arg Term] -> TCM (Type'' Term Term)
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> a -> m (Type'' Term Term)
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
m Empty -> Type'' Term Term -> [Arg Term] -> m (Type'' Term Term)
piApplyM' TCMT IO Empty
abort Type'' Term Term
t [Arg Term]
args
          TelV tel t'' <- telView t'
          addContext tel $ ifNotSort t'' (return ()) $ \Sort' Term
s -> do
            let v' :: Term
v' = Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise (Tele (Dom' Term (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term (Type'' Term Term))
tel) Term
v Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` Tele (Dom' Term (Type'' Term Term)) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom' Term (Type'' Term Term))
tel
            Comparison -> Sort' Term -> Term -> TCM ()
checkSolutionSort Comparison
cmp Sort' Term
s Term
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 ()
    (AsSizes{}   , Judgement MetaId
_              ) -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- TODO: should we do something similar for sizes?



  -- 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

  -- 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

  -- Turn the assignment problem @_X args >= SizeLt u@ into
  -- @_X args = SizeLt (_Y args@ and constraint
  -- @_Y args >= u@.
  subtypingForSizeLt dir x mvar t args v $ \ Term
v -> do

    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Int
25 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v = " 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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Int
45 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
      cxt <- TCMT IO (Tele (Dom' Term (Type'' Term Term)))
forall (m :: * -> *).
MonadTCEnv m =>
m (Tele (Dom' Term (Type'' Term Term)))
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.

    [Arg Term]
-> (Term, CompareAs)
-> ([Arg Term] -> (Term, CompareAs) -> TCM ())
-> TCM ()
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 [Arg Term]
args (Term
v, CompareAs
target) (([Arg Term] -> (Term, CompareAs) -> TCM ()) -> TCM ())
-> ([Arg Term] -> (Term, CompareAs) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ [Arg Term]
args (Term
v, CompareAs
target) -> do

      cxt <- TCMT IO (Tele (Dom' Term (Type'' Term Term)))
forall (m :: * -> *).
MonadTCEnv m =>
m (Tele (Dom' Term (Type'' Term Term)))
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

      let
                vars              = [Arg Term] -> VarMap
forall t. Free t => t -> VarMap
freeVarMap [Arg Term]
args
                relevantVL        = (VarOcc' MetaSet -> Bool) -> VarMap -> [Int]
filterVarMapToList VarOcc' MetaSet -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant VarMap
vars
                shapeIrrelevantVL = (VarOcc' MetaSet -> Bool) -> VarMap -> [Int]
filterVarMapToList VarOcc' MetaSet -> Bool
forall a. LensRelevance a => a -> Bool
isShapeIrrelevant VarMap
vars
                irrelevantVL      = (VarOcc' MetaSet -> Bool) -> VarMap -> [Int]
filterVarMapToList ((Bool -> Bool -> Bool)
-> (VarOcc' MetaSet -> Bool)
-> (VarOcc' MetaSet -> Bool)
-> VarOcc' MetaSet
-> Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
(&&) VarOcc' MetaSet -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant VarOcc' MetaSet -> Bool
forall o a. LensFlexRig o a => o -> Bool
isUnguarded) VarMap
vars
            -- Andreas, 2011-10-06 only irrelevant vars that are direct
            -- arguments to the meta, hence, can be abstracted over, may
            -- appear on the rhs.  (test/fail/Issue483b)
            -- Update 2011-03-27: Also irr. vars under record constructors.
            -- Andreas, 2019-06-25:  The reason is that when solving
            -- @X args = v@ we drop all irrelevant arguments that
            -- are not variables (after flattening of record constructors).
            -- (See isVarOrIrrelevant in inverseSubst.)
            -- Thus, the occurs-check needs to ensure only these variables
            -- are mentioned on the rhs.
            -- In the terminology of free variable analysis, the retained
            -- irrelevant variables are exactly the Unguarded ones.
            -- Jesper, 2019-10-15: This is actually wrong since it
            -- will lead to pruning of metas that should not be
            -- pruned, see #4136.

      reportSDoc "tc.meta.assign" 20 $
          let pr (Var Int
n []) = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
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)
               , "fvars lhs (relevant)        :" <+> sep (map' (text . show) relevantVL)
               , "fvars lhs (shape-irrelevant):" <+> sep (map' (text . show) shapeIrrelevantVL)
               , "fvars lhs (irrelevant)      :" <+> sep (map' (text . show) irrelevantVL)
               ]

      -- 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.
      -- Herein, distinguish relevant and irrelevant vars,
      -- since when abstracting irrelevant lhs vars, they may only occur
      -- irrelevantly on rhs.
      -- v <- liftTCM $ occursCheck x (relevantVL, nonstrictVL, irrelevantVL) v
      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 -> Int
forall a. TermSize a => a -> Int
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
      -- Ulf, 2011-09-22: we need to respect irrelevant vars as well, otherwise
      -- we'll build solutions where the irrelevant terms are not valid
      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 = [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args
      TelV mTel _ <- telViewUpToPath n t

      -- We should never prune local rewrite rules
      let noPrune = VarSet -> VarSet -> VarSet
VarSet.union VarSet
fvs (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term (Type'' Term Term)) -> VarSet
theRewVars Tele (Dom' Term (Type'' Term Term))
cxt

      -- Check that the arguments are variables
      mids <- do
        res <- runExceptT $ inverseSubst' (const False) mTel args
        case res of
          -- all args are variables
          Right [(Int, Term)]
ids -> do
            [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Int
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 (((Int, Term) -> TCMT IO Doc) -> [(Int, Term)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Int, Term) -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [(Int, Term)]
ids)
            [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Int
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 (((Int, Term) -> TCMT IO Doc) -> [(Int, Term)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Int, Term) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => (Int, Term) -> m Doc
prettyTCM [(Int, Term)]
ids)
            let boundVars :: VarSet
boundVars = [Int] -> VarSet
VarSet.fromList ([Int] -> VarSet) -> [Int] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Int, Term) -> Int) -> [(Int, Term)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map' (Int, Term) -> Int
forall a b. (a, b) -> a
fst [(Int, Term)]
ids
            if VarSet
fvs VarSet -> VarSet -> Bool
`VarSet.isSubsetOf` VarSet
boundVars
              then Maybe [(Int, Term)] -> TCMT IO (Maybe [(Int, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [(Int, Term)] -> TCMT IO (Maybe [(Int, Term)]))
-> Maybe [(Int, Term)] -> TCMT IO (Maybe [(Int, Term)])
forall a b. (a -> b) -> a -> b
$ [(Int, Term)] -> Maybe [(Int, Term)]
forall a. a -> Maybe a
Just [(Int, Term)]
ids
              else Maybe [(Int, Term)] -> TCMT IO (Maybe [(Int, Term)])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(Int, 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 [(Int, Term)]
forall a. Maybe a
Nothing Maybe [(Int, Term)]
-> TCMT IO (Maybe ()) -> TCMT IO (Maybe [(Int, 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  -> [(Int, Term)] -> Maybe [(Int, Term)]
forall a. a -> Maybe a
Just ([(Int, Term)] -> Maybe [(Int, Term)])
-> TCMT IO [(Int, Term)] -> TCMT IO (Maybe [(Int, Term)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> [Arg Term] -> VarSet -> TCMT IO [(Int, Term)]
forall a. MetaId -> [Arg Term] -> VarSet -> TCM a
attemptPruning MetaId
x [Arg Term]
args VarSet
noPrune
          -- we have a projected variable which could not be eta-expanded away:
          -- same as neutral
          Left ProjVar{}   -> [(Int, Term)] -> Maybe [(Int, Term)]
forall a. a -> Maybe a
Just ([(Int, Term)] -> Maybe [(Int, Term)])
-> TCMT IO [(Int, Term)] -> TCMT IO (Maybe [(Int, Term)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> [Arg Term] -> VarSet -> TCMT IO [(Int, Term)]
forall a. MetaId -> [Arg Term] -> VarSet -> TCM a
attemptPruning MetaId
x [Arg Term]
args VarSet
noPrune

      case mids of  -- vv Ulf 2014-07-13: actually not needed after all: attemptInertRHSImprovement x args v
        Maybe [(Int, 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 [(Int, Term)]
ids -> do
          -- Check linearity
          ids <- do
            res <- ExceptT () (TCMT IO) [(Int, Term)] -> TCM (Either () [(Int, Term)])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT () (TCMT IO) [(Int, Term)]
 -> TCM (Either () [(Int, Term)]))
-> ExceptT () (TCMT IO) [(Int, Term)]
-> TCM (Either () [(Int, Term)])
forall a b. (a -> b) -> a -> b
$ [(Int, Term)] -> ExceptT () (TCMT IO) [(Int, Term)]
checkLinearity {- (`VarSet.member` fvs) -} [(Int, Term)]
ids
            case res of
              -- case: linear
              Right [(Int, Term)]
ids -> [(Int, Term)] -> TCMT IO [(Int, Term)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, 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 noPrune

          -- Check ids is time respecting.
          () <- do
            let idvars = ((Int, Term) -> (Int, VarSet)) -> [(Int, Term)] -> [(Int, VarSet)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Term -> VarSet) -> (Int, Term) -> (Int, VarSet)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Term -> VarSet
forall t. Free t => t -> VarSet
freeVarSet) [(Int, Term)]
ids
            -- earlierThan α v := v "arrives" before α
            let earlierThan a
l a
j = a
j a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
l
            forM_ ids $ \(Int
i,Term
u) -> do
              d <- Int -> TCMT IO (Dom' Term (Type'' Term Term))
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Dom' Term (Type'' Term Term))
domOfBV Int
i
              case getLock (getArgInfo d) of
                Lock
IsNotLock -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                IsLock{} -> do
                let us :: VarSet
us = [VarSet] -> VarSet
forall (f :: * -> *). Foldable f => f VarSet -> VarSet
VarSet.unions ([VarSet] -> VarSet) -> [VarSet] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Int, VarSet) -> VarSet) -> [(Int, VarSet)] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map' (Int, VarSet) -> VarSet
forall a b. (a, b) -> b
snd ([(Int, VarSet)] -> [VarSet]) -> [(Int, VarSet)] -> [VarSet]
forall a b. (a -> b) -> a -> b
$ ((Int, VarSet) -> Bool) -> [(Int, VarSet)] -> [(Int, VarSet)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
earlierThan Int
i (Int -> Bool) -> ((Int, VarSet) -> Int) -> (Int, VarSet) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, VarSet) -> Int
forall a b. (a, b) -> a
fst) [(Int, VarSet)]
idvars
                -- us Earlier than u
                TCM Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Tele (Dom' Term (Type'' Term Term)) -> TCM Bool -> TCM Bool
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom' Term (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom' Term (Type'' Term Term))
mTel (TCM Bool -> TCM Bool) -> TCM Bool -> TCM Bool
forall a b. (a -> b) -> a -> b
$ Term -> VarSet -> TCM Bool
checkEarlierThan Term
u VarSet
us) (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 (MetaId -> Blocker
unblockOnMeta MetaId
x)  -- If the earlier check hard-fails we need to
                                                      -- solve this meta in some other way.

          -- Check subtyping constraints on the context variables.

          -- Intuition: suppose @_X : (x : A) → B@, then to turn
          --   @
          --     Γ(x : A') ⊢ _X x =?= v : B'@
          --   @
          -- into
          --   @
          --     Γ ⊢ _X =?= λ x → v
          --   @
          -- we need to check that @A <: A'@ (due to contravariance).
          let sigma = [Term] -> Substitution' Term
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution' Term) -> [Term] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
args
          hasSubtyping <- optCumulativity <$> pragmaOptions
          when hasSubtyping $ forM_ ids $ \(Int
i , Term
u) -> do
            -- @u@ is a (projected) variable, so we can infer its type
            a  <- Substitution' (SubstArg (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (Type'' Term Term))
sigma (Type'' Term Term -> Type'' Term Term)
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tele (Dom' Term (Type'' Term Term))
-> TCM (Type'' Term Term) -> TCM (Type'' Term Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom' Term (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom' Term (Type'' Term Term))
mTel (Term -> TCM (Type'' Term Term)
infer Term
u)
            a' <- typeOfBV i
            checkSubtypeIsEqual a' a
              `catchError` \case
                TypeError{} -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation (MetaId -> Blocker
unblockOnMeta MetaId
x) -- If the subtype check hard-fails we need to
                TCErr
err         -> TCErr -> TCM ()
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err                     -- solve this meta in some other way.

          -- 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 -> [Arg Term] -> VarSet -> TCM a
attemptPruning MetaId
x [Arg Term]
args VarSet
noPrune = do
      -- non-linear lhs: we cannot solve, but prune
      killResult <- MetaId -> [Arg Term] -> (Int -> Bool) -> TCM PruneResult
prune MetaId
x [Arg Term]
args ((Int -> Bool) -> TCM PruneResult)
-> (Int -> Bool) -> TCM PruneResult
forall a b. (a -> b) -> a -> b
$ (Int -> 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
-> [Arg Term] -> m (Maybe (MetaId, InteractionId, [Arg Term]))
isInteractionMetaB MetaId
mid [Arg Term]
args =
  MaybeT m (MetaId, InteractionId, [Arg Term])
-> m (Maybe (MetaId, InteractionId, [Arg Term]))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m (MetaId, InteractionId, [Arg Term])
 -> m (Maybe (MetaId, InteractionId, [Arg Term])))
-> MaybeT m (MetaId, InteractionId, [Arg Term])
-> m (Maybe (MetaId, InteractionId, [Arg Term]))
forall a b. (a -> b) -> a -> b
$ MetaId
-> [Arg Term] -> MaybeT m (MetaId, InteractionId, [Arg Term])
forall {m :: * -> *} {c}.
ReadTCState m =>
MetaId -> c -> MaybeT m (MetaId, InteractionId, c)
here MetaId
mid [Arg Term]
args MaybeT m (MetaId, InteractionId, [Arg Term])
-> MaybeT m (MetaId, InteractionId, [Arg Term])
-> MaybeT m (MetaId, InteractionId, [Arg Term])
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, as long as we ignore
    -- blocking
    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
instantiateBlockingFull (MetaId -> Elims -> Term
MetaV MetaId
mid (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> [Arg Term] -> Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term]
args))) MaybeT m Term
-> (Term -> MaybeT m (MetaId, InteractionId, [Arg Term]))
-> MaybeT m (MetaId, InteractionId, [Arg Term])
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, [Arg Term])
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)

    instantiateBlockingFull :: Term -> m Term
instantiateBlockingFull = Lens' TCState Bool -> (Bool -> Bool) -> m Term -> m Term
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stInstantiateBlocking (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (m Term -> m Term) -> (Term -> m Term) -> Term -> m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> m Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull

    there :: Term -> MaybeT m (MetaId, InteractionId, Args)
    there :: Term -> MaybeT m (MetaId, InteractionId, [Arg Term])
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, [Arg Term])
there (Abs Term -> SubstArg Term -> Term
forall a. Subst a => Abs a -> SubstArg a -> a
absApp Abs Term
as (Int -> Term
var Int
0))
    there Term
_ = MaybeT m (MetaId, InteractionId, [Arg Term])
forall a. MaybeT m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

{- UNUSED
-- | When faced with @_X us == D vs@ for an inert D we can solve this by
--   @_X xs := D _Ys@ with new constraints @_Yi us == vi@. This is important
--   for instance arguments, where knowing the head D might enable progress.
attemptInertRHSImprovement :: MetaId -> Args -> Term -> TCM ()
attemptInertRHSImprovement m args v = do
  reportSDoc "tc.meta.inert" 30 $ vcat
    [ "attempting inert rhs improvement"
    , nest 2 $ sep [ prettyTCM (MetaV m $ map' Apply args) <+> "=="
                   , prettyTCM v ] ]
  -- Check that the right-hand side has the form D vs, for some inert constant D.
  -- Returns the type of D and a function to build an application of D.
  (a, mkRHS) <- ensureInert v
  -- Check that all arguments to the meta are neutral and does not have head D.
  -- If there are non-neutral arguments there could be solutions to the meta
  -- that computes over these arguments. If D is an argument to the meta we get
  -- multiple solutions (for instance: _M Nat == Nat can be solved by both
  -- _M := \ x -> x and _M := \ x -> Nat).
  mapM_ (ensureNeutral (mkRHS []) . unArg) args
  tel <- theTel <$> (telView =<< getMetaType m)
  -- When attempting shortcut meta solutions, metas aren't necessarily fully
  -- eta expanded. If this is the case we skip inert improvement.
  when (length args < size tel) $ do
    reportSDoc "tc.meta.inert" 30 $ "not fully applied"
    patternViolation
  -- Solve the meta with _M := \ xs -> D (_Y1 xs) .. (_Yn xs), for fresh metas
  -- _Yi.
  metaArgs <- inTopContext $ addContext tel $ newArgsMeta a
  let varArgs = map' Apply $ reverse $ zipWith' (\i a -> var i <$ a) [0..] (reverse args)
      sol     = mkRHS metaArgs
      argTel  = map' ("x" <$) args
  reportSDoc "tc.meta.inert" 30 $ nest 2 $ vcat
    [ "a       =" <+> prettyTCM a
    , "tel     =" <+> prettyTCM tel
    , "metas   =" <+> prettyList (map' prettyTCM metaArgs)
    , "sol     =" <+> prettyTCM sol
    ]
  assignTerm m argTel sol
  patternViolation  -- throwing a pattern violation here lets the constraint
                    -- machinery worry about restarting the comparison.
  where
    ensureInert :: Term -> TCM (Type, Args -> Term)
    ensureInert v = do
      let notInert = do
            reportSDoc "tc.meta.inert" 30 $ nest 2 $ "not inert:" <+> prettyTCM v
            patternViolation
          toArgs elims =
            case allApplyElims elims of
              Nothing -> do
                reportSDoc "tc.meta.inert" 30 $ nest 2 $ "can't do projections from inert"
                patternViolation
              Just args -> return args
      case v of
        Var x elims -> (, Var x . map' Apply) <$> typeOfBV x
        Con c ci args  -> notInert -- (, Con c ci) <$> defType <$> getConstInfo (conName c)
        Def f elims -> do
          def <- getConstInfo f
          let good = return (defType def, Def f . map' Apply)
          case theDef def of
            Axiom{}       -> good
            Datatype{}    -> good
            Record{}      -> good
            Function{}    -> notInert
            Primitive{}   -> notInert
            Constructor{} -> __IMPOSSIBLE__

        Pi{}       -> notInert -- this is actually inert but improving doesn't buy us anything for Pi
        Lam{}      -> notInert
        Sort{}     -> notInert
        Lit{}      -> notInert
        Level{}    -> notInert
        MetaV{}    -> notInert
        DontCare{} -> notInert

    ensureNeutral :: Term -> Term -> TCM ()
    ensureNeutral rhs v = do
      b <- reduceB v
      let notNeutral v = do
            reportSDoc "tc.meta.inert" 30 $ nest 2 $ "not neutral:" <+> prettyTCM v
            patternViolation
          checkRHS arg
            | arg == rhs = do
              reportSDoc "tc.meta.inert" 30 $ nest 2 $ "argument shares head with RHS:" <+> prettyTCM arg
              patternViolation
            | otherwise  = return ()
      case b of
        Blocked{}      -> notNeutral v
        NotBlocked r v ->                      -- Andrea(s) 2014-12-06 can r be useful?
          case v of
            Var x _    -> checkRHS (Var x [])
            Def f _    -> checkRHS (Def f [])
            Pi{}       -> return ()
            Sort{}     -> return ()
            Level{}    -> return ()
            Lit{}      -> notNeutral v
            DontCare{} -> notNeutral v
            Con{}      -> notNeutral v
            Lam{}      -> notNeutral v
            MetaV{}    -> __IMPOSSIBLE__
-- END UNUSED -}

-- | @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 -> Type -> [Int] -> Term -> TCM ()
assignMeta :: Int -> MetaId -> Type'' Term Term -> [Int] -> Term -> TCM ()
assignMeta Int
m MetaId
x Type'' Term Term
t [Int]
ids Term
v = do
  let n :: Int
n    = [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ids
      cand :: [(Int, Term)]
cand = [(Int, Term)] -> [(Int, Term)]
forall a. Ord a => [a] -> [a]
List.sort ([(Int, Term)] -> [(Int, Term)]) -> [(Int, Term)] -> [(Int, Term)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Term] -> [(Int, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip' [Int]
ids ([Term] -> [(Int, Term)]) -> [Term] -> [(Int, Term)]
forall a b. (a -> b) -> a -> b
$ (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Int -> Term
var ([Int] -> [Term]) -> [Int] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n
  Int
-> MetaId
-> Type'' Term Term
-> Int
-> [(Int, Term)]
-> Term
-> TCM ()
assignMeta' Int
m MetaId
x Type'' Term Term
t Int
n [(Int, 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 -> Type -> Int -> SubstCand -> Term -> TCM ()
assignMeta' :: Int
-> MetaId
-> Type'' Term Term
-> Int
-> [(Int, Term)]
-> Term
-> TCM ()
assignMeta' Int
m MetaId
x Type'' Term Term
t Int
n [(Int, Term)]
ids Term
v = do
  -- we are linear, so we can solve!
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Int
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 :: Int -> [(Int, Term)] -> [Maybe Term]
assocToList Int
i = \case
        [(Int, Term)]
_           | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
m -> []
        ((Int
j,Term
u) : [(Int, Term)]
l) | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
u  Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Int -> [(Int, Term)] -> [Maybe Term]
assocToList (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Int, Term)]
l
        [(Int, Term)]
l                    -> Maybe Term
forall a. Maybe a
Nothing Maybe Term -> [Maybe Term] -> [Maybe Term]
forall a. a -> [a] -> [a]
: Int -> [(Int, Term)] -> [Maybe Term]
assocToList (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [(Int, Term)]
l
      ivs :: [Maybe Term]
ivs = Int -> [(Int, Term)] -> [Maybe Term]
assocToList Int
0 [(Int, Term)]
ids
      rho :: Substitution' Term
rho = Impossible
-> [Maybe Term] -> Substitution' Term -> Substitution' Term
forall a.
DeBruijn a =>
Impossible -> [Maybe a] -> Substitution' a -> Substitution' a
prependS Impossible
HasCallStack => Impossible
impossible [Maybe Term]
ivs (Substitution' Term -> Substitution' Term)
-> Substitution' Term -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Int -> Substitution' Term
forall a. Int -> Substitution' a
raiseS Int
n
      v' :: Term
v'  = Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg Term)
rho Term
v

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

  -- Variables corresponding to local rewrite rules
  let rVars = VarSet -> [Int]
VarSet.toDescList (VarSet -> [Int]) -> VarSet -> [Int]
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term (Type'' Term Term)) -> VarSet
theRewVars Tele (Dom' Term (Type'' Term Term))
cxt
  -- Variables not strengthened away
  let notDropped = [Int] -> VarSet
VarSet.fromList ([Int] -> VarSet) -> [Int] -> VarSet
forall a b. (a -> b) -> a -> b
$ ((Int, Term) -> Int) -> [(Int, Term)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Term) -> Int
forall a b. (a, b) -> a
fst [(Int, 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@(TelV mTel a), bs) <- telViewUpToPathBoundary n t
    reportSDoc "tc.meta.assign" 30 $ "tel'  =" <+> prettyTCM mTel
    reportSDoc "tc.meta.assign" 30 $ "#args =" <+> text (show n)

    -- Solving metas in contexts with extra local rewrite rules is
    -- problematic because solutions that appear unique locally may not be
    -- globally unique.
    -- We fix this by checking that every local rewrite rule in the solution
    -- context is mapped to a local rewrite rule in the meta's context.
    -- This is conservative, but should at least be pretty fast.

    stillRews <- addContext mTel $ forM rVars \Int
i -> do
      if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> VarSet -> Bool
VarSet.member Int
i VarSet
notDropped then Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False else do
      case Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView (Term -> Maybe Int) -> Term -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> Int -> Term
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' Term
rho Int
i of
        Just Int
i' -> do
          Maybe (RewDom' Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (RewDom' Term) -> Bool)
-> (Dom' Term (Type'' Term Term) -> Maybe (RewDom' Term))
-> Dom' Term (Type'' Term Term)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Type'' Term Term) -> Maybe (RewDom' Term)
forall t e. Dom' t e -> Maybe (RewDom' t)
rewDom (Dom' Term (Type'' Term Term) -> Bool)
-> TCMT IO (Dom' Term (Type'' Term Term)) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO (Dom' Term (Type'' Term Term))
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Dom' Term (Type'' Term Term))
domOfBV Int
i'
        Maybe Int
Nothing -> Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

    -- The current context has a rewrite rule which does not appear to be
    -- in the meta's
    unless (and stillRews) $ patternViolation neverUnblock

    -- 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!

    -- Perform the assignment (and wake constraints).

    v' <- blockOnBoundary telv bs v'

    -- Andreas, 2013-10-25 double check solution before assigning
    whenM (optDoubleCheck  <$> pragmaOptions) $ do
      m <- lookupLocalMeta x
      reportSDoc "tc.meta.check" 30 $ "double checking solution"
      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'
  where
    blockOnBoundary :: TelView -> Boundary -> Term -> TCM Term
    blockOnBoundary :: TelV (Type'' Term Term) -> Boundary -> Term -> TCMT IO Term
blockOnBoundary TelV (Type'' Term Term)
telv         (Boundary []) Term
v = Term -> TCMT IO Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
    blockOnBoundary (TelV Tele (Dom' Term (Type'' Term Term))
tel Type'' Term Term
t) (Boundary [(Int, (Term, Term))]
bs) Term
v = Tele (Dom' Term (Type'' Term Term)) -> 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' Term (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom' Term (Type'' Term Term))
tel (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
      Type'' Term Term -> TCMT IO Term -> TCMT IO Term
blockTerm Type'' Term Term
t (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ do
        neg <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg
        forM_ bs $ \ (Int
i,(Term
x,Term
y)) -> do
          let r :: Term
r = Int -> Term
var Int
i
          Term -> Type'' Term Term -> Term -> Term -> TCM ()
equalTermOnFace (Term
neg Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term
r) Type'' Term Term
t Term
x Term
v
          Term -> Type'' Term Term -> Term -> Term -> TCM ()
equalTermOnFace Term
r  Type'' Term Term
t Term
y Term
v
        return 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 :: Int
n = [Arg [Char]] -> Int
forall a. Sized a => a -> Int
size (Instantiation -> [Arg [Char]]
instTel Instantiation
inst)
          t :: Type'' Term Term
t = Judgement MetaId -> Type'' Term Term
forall a. Judgement a -> Type'' Term Term
jMetaType (Judgement MetaId -> Type'' Term Term)
-> Judgement MetaId -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
m
      (telv@(TelV tel a),bs) <- Int
-> Type'' Term Term -> TCMT IO (TelV (Type'' Term Term), Boundary)
forall (m :: * -> *).
PureTCM m =>
Int -> Type'' Term Term -> m (TelV (Type'' Term Term), Boundary)
telViewUpToPathBoundary Int
n Type'' Term Term
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'' Term Term -> TCM ()
checkSolutionForMeta MetaId
x MetaVariable
m Term
v Type'' Term Term
a = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Int
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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        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'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
        ctx <- TCMT IO (Context' ContextEntry)
forall (m :: * -> *). MonadTCEnv m => m (Context' ContextEntry)
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 Term -> Term -> Call
CheckMetaSolution (MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange MetaVariable
m) MetaId
x Type'' Term Term
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 TypeOf Term
Type'' Term 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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.check" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
        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'' Term Term -> TCM (Sort' Term)
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadError TCErr m) =>
Type'' Term Term -> m (Sort' Term)
shouldBeSort (Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
HasCallStack => Sort' Term
__DUMMY_SORT__ Term
v)
      traceCall (CheckMetaSolution (getRange m) x (sort (univSort s)) (Sort s)) $
        inferInternal s

-- | Given two types @a@ and @b@ with @a <: b@, check that @a == b@.
checkSubtypeIsEqual :: Type -> Type -> TCM ()
checkSubtypeIsEqual :: Type'' Term Term -> Type'' Term Term -> TCM ()
checkSubtypeIsEqual Type'' Term Term
a Type'' Term Term
b = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.subtype" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"checking that subtype" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
a TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
    TCMT IO Doc
"of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
b TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"is actually equal."
  Type'' Term Term
-> Type'' Term Term
-> (Type'' Term Term -> Type'' Term Term -> TCM ())
-> (Type'' Term Term -> Type'' Term Term -> TCM ())
-> TCM ()
forall a (m :: * -> *) b.
(Instantiate a, SynEq a, MonadReduce m) =>
a -> a -> (a -> a -> m b) -> (a -> a -> m b) -> m b
SynEq.checkSyntacticEquality Type'' Term Term
a Type'' Term Term
b (\Type'' Term Term
_ Type'' Term Term
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((Type'' Term Term -> Type'' Term Term -> TCM ()) -> TCM ())
-> (Type'' Term Term -> Type'' Term Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Type'' Term Term
a Type'' Term Term
b -> do
    cumulativity <- PragmaOptions -> Bool
optCumulativity (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
    abortIfBlocked (unEl b) >>= \case
      Sort Sort' Term
sb -> Term -> TCMT IO Term
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
a) TCMT IO Term -> (Term -> 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
        Sort Sort' Term
sa | Bool
cumulativity -> Sort' Term -> Sort' Term -> TCM ()
equalSort Sort' Term
sa Sort' Term
sb
                             | Bool
otherwise    -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Dummy{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO: this shouldn't happen but
                             -- currently does because of generalized
                             -- metas being created in a dummy context
        Term
a -> 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
a) -- TODO: can this happen?
      Pi Dom' Term (Type'' Term Term)
b1 Abs (Type'' Term Term)
b2 -> Term -> TCMT IO Term
forall (m :: * -> *) t.
(MonadReduce m, MonadBlock m, IsMeta t, Reduce t) =>
t -> m t
abortIfBlocked (Type'' Term Term -> Term
forall t a. Type'' t a -> a
unEl Type'' Term Term
a) TCMT IO Term -> (Term -> 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
        Pi Dom' Term (Type'' Term Term)
a1 Abs (Type'' Term Term)
a2
          | Dom' Term (Type'' Term Term) -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom' Term (Type'' Term Term)
a1 Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom' Term (Type'' Term Term) -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom' Term (Type'' Term Term)
b1 -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock -- Can we recover from this?
          | Dom' Term (Type'' Term Term) -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  Dom' Term (Type'' Term Term)
a1 Quantity -> Quantity -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom' Term (Type'' Term Term) -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  Dom' Term (Type'' Term Term)
b1 -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
          | Dom' Term (Type'' Term Term) -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion  Dom' Term (Type'' Term Term)
a1 Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom' Term (Type'' Term Term) -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion  Dom' Term (Type'' Term Term)
b1 -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
          | Dom' Term (Type'' Term Term) -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity Dom' Term (Type'' Term Term)
a1 PolarityModality -> PolarityModality -> Bool
forall a. Eq a => a -> a -> Bool
/= Dom' Term (Type'' Term Term) -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity Dom' Term (Type'' Term Term)
b1 -> Blocker -> TCM ()
forall a. Blocker -> TCMT IO a
forall (m :: * -> *) a. MonadBlock m => Blocker -> m a
patternViolation Blocker
neverUnblock
          | Bool
otherwise -> do
              Type'' Term Term -> Type'' Term Term -> TCM ()
checkSubtypeIsEqual (Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom' Term (Type'' Term Term)
b1) (Dom' Term (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
unDom Dom' Term (Type'' Term Term)
a1)
              Dom' Term (Type'' Term Term)
-> Abs (Type'' Term Term) -> (Type'' Term Term -> TCM ()) -> TCM ()
forall a (m :: * -> *) b.
(Subst a, MonadAddContext m) =>
Dom' Term (Type'' Term Term) -> Abs a -> (a -> m b) -> m b
underAbstractionAbs Dom' Term (Type'' Term Term)
a1 Abs (Type'' Term Term)
a2 ((Type'' Term Term -> TCM ()) -> TCM ())
-> (Type'' Term Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \Type'' Term Term
a2' -> Type'' Term Term -> Type'' Term Term -> TCM ()
checkSubtypeIsEqual Type'' Term Term
a2' (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
absBody Abs (Type'' Term Term)
b2)
        Dummy{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- TODO: this shouldn't happen but
                             -- currently does because of generalized
                             -- metas being created in a dummy context
        Term
a -> 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
a)
      -- TODO: check subtyping for Size< types
      Term
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- | Turn the assignment problem @_X args <= SizeLt u@ into
-- @_X args = SizeLt (_Y args)@ and constraint
-- @_Y args <= u@.
subtypingForSizeLt
  :: CompareDirection -- ^ @dir@
  -> MetaId           -- ^ The local meta-variable @x@.
  -> MetaVariable     -- ^ Its associated information @mvar <- lookupLocalMeta x@.
  -> Type             -- ^ Its type @t = jMetaType $ mvJudgement mvar@
  -> Args             -- ^ Its arguments.
  -> Term             -- ^ Its to-be-assigned value @v@, such that @x args `dir` v@.
  -> (Term -> TCM ()) -- ^ Continuation taking its possibly assigned value.
  -> TCM ()
subtypingForSizeLt :: CompareDirection
-> MetaId
-> MetaVariable
-> Type'' Term Term
-> [Arg Term]
-> Term
-> (Term -> TCM ())
-> TCM ()
subtypingForSizeLt CompareDirection
DirEq MetaId
x MetaVariable
mvar Type'' Term Term
t [Arg Term]
args Term
v Term -> TCM ()
cont = Term -> TCM ()
cont Term
v
subtypingForSizeLt CompareDirection
dir   MetaId
x MetaVariable
mvar Type'' Term Term
t [Arg Term]
args Term
v Term -> TCM ()
cont = do
  let fallback :: TCM ()
fallback = Term -> TCM ()
cont Term
v
  -- Check whether we have built-ins SIZE and SIZELT
  (mSize, mSizeLt) <- TCMT IO (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  caseMaybe mSize   fallback $ \ QName
qSize   -> do
    Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe QName
mSizeLt TCM ()
fallback ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ QName
qSizeLt -> do
      -- Check whether v is a SIZELT
      v <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
      case v of
        Def QName
q [Apply (Arg ArgInfo
ai Term
u)] | QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
qSizeLt -> do
          -- Clone the meta into a new size meta @y@.
          -- To this end, we swap the target of t for Size.
          TelV tel _ <- Type'' Term Term -> TCMT IO (TelV (Type'' Term Term))
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type'' Term Term -> m (TelV (Type'' Term Term))
telView Type'' Term Term
t
          let size = QName -> Type'' Term Term
sizeType_ QName
qSize
              t'   = Tele (Dom' Term (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
telePi Tele (Dom' Term (Type'' Term Term))
tel Type'' Term Term
size
          y <- newMeta Instantiable (mvInfo mvar) (mvPriority mvar) (mvPermutation mvar)
                       (HasType __IMPOSSIBLE__ CmpLeq t')
          -- Note: no eta-expansion of new meta possible/necessary.
          -- Add the size constraint @y args `dir` u@.
          let yArgs = MetaId -> Elims -> Term
MetaV MetaId
y (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
args
          addConstraint (unblockOnMeta y) $ dirToCmp (`ValueCmp` AsSizes) dir yArgs u
          -- We continue with the new assignment problem, and install
          -- an exception handler, since we created a meta and a constraint,
          -- so we cannot fall back to the original handler.
          let xArgs = MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map' Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
args
              v'    = QName -> Elims -> Term
Def QName
qSizeLt [Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Term
yArgs]
              c     = (Comparison -> Term -> Term -> Constraint)
-> CompareDirection -> Term -> Term -> Constraint
forall a c.
(Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp (Comparison -> CompareAs -> Term -> Term -> Constraint
`ValueCmp` (Type'' Term Term -> CompareAs
AsTermsOf Type'' Term Term
sizeUniv)) CompareDirection
dir Term
xArgs Term
v'
          catchConstraint c $ cont v'
        Term
_ -> TCM ()
fallback

-- | 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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Int
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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Int
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 Int
i [(ProjOrigin, QName)]
_) -> Int -> (a, b) -> TCM c -> ((a, b) -> TCM c) -> TCM c
forall a c.
(PrettyTCM a, TermSubst a) =>
Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Int
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) =>
Int -> a -> TCM c -> (a -> TCM c) -> TCM c
etaExpandProjectedVar Int
i a
v TCM c
fail a -> TCM c
succeed = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Int
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 (Int -> Term
var Int
i)
  -- We don't eta-expand variables which occur in local rewrite rules
  -- In principle, I think we could handle this safely, but it is tricky
  tel <- TCMT IO (Tele (Dom' Term (Type'' Term Term)))
forall (m :: * -> *).
MonadTCEnv m =>
m (Tele (Dom' Term (Type'' Term Term)))
getContextTelescope
  if i `VarSet.member` inRewVars tel then fail else
    caseMaybeM (etaExpandBoundVar i) fail $ \ (Tele (Dom' Term (Type'' Term Term))
delta, Substitution' Term
sigma, Substitution' Term
tau) -> do
    [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign.proj" Int
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 (Int -> Term
var Int
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' Term (Type'' Term Term)) -> TCM c -> TCM c
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom' Term (Type'' Term Term)) -> m a -> m a
addContext Tele (Dom' Term (Type'' Term Term))
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' Term
Substitution' (SubstArg a)
tau a
v

-- | 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 Int
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] -> [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
$ Int -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Int
i [(ProjOrigin, QName)]
qs
      -- Andreas, 2015-09-12 Issue #1316:
      -- Also look in inductive record constructors
      Con (ConHead QName
_ IsRecord{} Induction
Inductive [Arg QName]
_) ConInfo
_ Elims
es
        | Just [Arg Term]
vs <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
        -> [Arg Term] -> Either ProjectedVar ()
forall a. NoProjectedVar a => a -> Either ProjectedVar ()
noProjectedVar [Arg Term]
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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta" Int
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 -> [Char] -> Term -> TCMT IO Term
forall (m :: * -> *).
(MonadTCEnv m, HasOptions m) =>
ArgInfo -> [Char] -> Term -> m Term
etaLam ArgInfo
ai (Abs Term -> [Char]
forall a. Abs a -> [Char]
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 -> [Arg Term] -> TCMT IO Term)
-> TCMT IO Term
forall (m :: * -> *).
HasConstInfo m =>
ConHead
-> ConInfo
-> Elims
-> (QName -> ConHead -> ConInfo -> [Arg Term] -> m Term)
-> m Term
etaCon ConHead
c ConInfo
ci Elims
es ((QName -> ConHead -> ConInfo -> [Arg Term] -> TCMT IO Term)
 -> TCMT IO Term)
-> (QName -> ConHead -> ConInfo -> [Arg Term] -> TCMT IO Term)
-> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \ QName
r ConHead
c ConInfo
ci [Arg Term]
args -> do
        args <- [Arg Term] -> TCMT IO [Arg Term]
forall a. ReduceAndEtaContract a => a -> TCM a
reduceAndEtaContract [Arg Term]
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 :: [(Int, Term)] -> ExceptT () (TCMT IO) [(Int, Term)]
checkLinearity [(Int, Term)]
ids = do
  -- see issue #920
  [(Int, Term)] -> [(Int, Term)]
[(Int, Term)] -> [Item [(Int, Term)]]
forall l. IsList l => l -> [Item l]
List1.toList ([(Int, Term)] -> [(Int, Term)])
-> ExceptT () (TCMT IO) [(Int, Term)]
-> ExceptT () (TCMT IO) [(Int, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NonEmpty (Int, Term) -> ExceptT () (TCMT IO) (Int, Term))
-> [NonEmpty (Int, Term)] -> ExceptT () (TCMT IO) [(Int, 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 NonEmpty (Int, Term) -> ExceptT () (TCMT IO) (Int, Term)
makeLinear (((Int, Term) -> Int) -> [(Int, Term)] -> [NonEmpty (Int, Term)]
forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
List1.groupOn (Int, Term) -> Int
forall a b. (a, b) -> a
fst [(Int, 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 :: NonEmpty (Int, Term) -> ExceptT () (TCMT IO) (Int, Term)
makeLinear ((Int, Term)
p       :| []) = (Int, Term) -> ExceptT () (TCMT IO) (Int, Term)
forall a. a -> ExceptT () (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int, Term)
p
    makeLinear (p :: (Int, Term)
p@(Int
i,Term
t) :| [(Int, Term)]
_ ) =
      ExceptT () (TCMT IO) Bool
-> ExceptT () (TCMT IO) (Int, Term)
-> ExceptT () (TCMT IO) (Int, Term)
-> ExceptT () (TCMT IO) (Int, 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'' Term Term -> TCM (Either Blocker Bool))
-> Type'' Term Term
-> 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'' Term Term -> BlockT (TCMT IO) Bool)
-> Type'' Term Term
-> TCM (Either Blocker Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type'' Term Term -> BlockT (TCMT IO) Bool
forall (m :: * -> *).
(PureTCM m, MonadBlock m) =>
Type'' Term Term -> m Bool
isSingletonTypeModuloRelevance (Type'' Term Term -> ExceptT () (TCMT IO) (Either Blocker Bool))
-> ExceptT () (TCMT IO) (Type'' Term Term)
-> ExceptT () (TCMT IO) (Either Blocker Bool)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> ExceptT () (TCMT IO) (Type'' Term Term)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m) =>
Int -> m (Type'' Term Term)
typeOfBV Int
i)
        ((Int, Term) -> ExceptT () (TCMT IO) (Int, Term)
forall a. a -> ExceptT () (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int, Term)
p)
        (() -> ExceptT () (TCMT IO) (Int, 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' Term (Type'' Term Term))
-> [Arg Term]
-> ExceptT InvertExcept (TCMT IO) [(Int, Term)]
inverseSubst' Term -> Bool
skip Tele (Dom' Term (Type'' Term Term))
tel [Arg Term]
args = ((Arg Int, Term) -> (Int, Term))
-> [(Arg Int, Term)] -> [(Int, Term)]
forall a b. (a -> b) -> [a] -> [b]
map' ((Arg Int -> Int) -> (Arg Int, Term) -> (Int, 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 Int -> Int
forall e. Arg e -> e
unArg) ([(Arg Int, Term)] -> [(Int, Term)])
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Int, Term)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
loop ([Arg Term] -> [Term] -> [(Arg Term, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip' [Arg Term]
args [Term]
terms)
  where
  loop :: [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
loop  = ([(Arg Int, Term)]
 -> (Arg Term, Term)
 -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)])
-> [(Arg Int, Term)]
-> [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [(Arg Int, Term)]
-> (Arg Term, Term)
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
isVarOrIrrelevant []
  terms :: [Term]
terms = (Int -> Term) -> [Int] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map' Int -> Term
var (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom ([Arg Term] -> Int
forall a. Sized a => a -> Int
size [Arg Term]
args))
  failure :: Term -> ExceptT InvertExcept (TCMT IO) [(Arg Int, 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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Int
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
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
args
      , TCMT IO Doc
"  aborting assignment" ]
    InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Int, 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 Int, Term)]
-> (Arg Term, Term)
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
isVarOrIrrelevant [(Arg Int, Term)]
vars (Arg ArgInfo
info Term
v, Term
t) = do
    -- We need to identify arguments to the meta that are fully constrained by
    -- local rewrite rules
    -- These are simply ignored when building the inverse substitution
    -- (analogously to irrelevant arguments)
    constrained <- TCM VarSet -> ExceptT InvertExcept (TCMT IO) VarSet
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 VarSet -> ExceptT InvertExcept (TCMT IO) VarSet)
-> TCM VarSet -> ExceptT InvertExcept (TCMT IO) VarSet
forall a b. (a -> b) -> a -> b
$ Tele (Dom' Term (Type'' Term Term)) -> TCM VarSet
rewConstrained Tele (Dom' Term (Type'' Term Term))
tel
    case t of
      Var Int
x [] | Int
x Int -> VarSet -> Bool
`VarSet.member` VarSet
constrained -> 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] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.meta.assign" Int
60 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
                [ TCMT IO Doc
"argument is constrained by rewrite rule"
                , TCMT IO Doc
"  arg = " 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
"  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 (Int -> Term
var Int
x)
                ]
        [(Arg Int, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Int, Term)]
vars
      Term
_ -> do
        let irr :: Bool
irr | ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info = Bool
True
                | 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 Int
i [] -> [(Arg Int, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Arg Int, Term)]
 -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)])
-> [(Arg Int, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a b. (a -> b) -> a -> b
$! (ArgInfo -> Int -> Arg Int
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Int
i, Term
t) (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
`cons` [(Arg Int, Term)]
vars

          -- π i := x  try to eta-expand projection π away!
          Var Int
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 Int, 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 Int, Term)])
-> InvertExcept -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a b. (a -> b) -> a -> b
$ ProjectedVar -> InvertExcept
ProjVar (ProjectedVar -> InvertExcept) -> ProjectedVar -> InvertExcept
forall a b. (a -> b) -> a -> b
$ Int -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Int
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 Int, Term)]
fallback
                 | ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info = [(Arg Int, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Int, Term)]
vars
                 | Term -> Bool
skip Term
tm           = [(Arg Int, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Int, Term)]
vars
                 | Bool
otherwise         = Term -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
failure Term
tm
            irrProj <- PragmaOptions -> Bool
optIrrelevantProjections (PragmaOptions -> Bool)
-> ExceptT InvertExcept (TCMT IO) PragmaOptions
-> ExceptT InvertExcept (TCMT IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExceptT InvertExcept (TCMT IO) PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
            lift (isEtaRecordConstructor $ conName c) >>= \case
              -- Andreas, 2019-11-10, issue #4185: only for eta-records
              Just (QName
_, RecordData{ _recFields :: RecordData -> [Dom QName]
_recFields = [Dom QName]
fs })
                | [Dom QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom QName]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Elims -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Elims
es
                , ArgInfo -> Bool
forall a. LensQuantity a => a -> Bool
hasQuantity0 ArgInfo
info Bool -> Bool -> Bool
|| (Dom QName -> Bool) -> [Dom QName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Dom QName -> Bool
forall a. LensQuantity a => a -> Bool
usableQuantity [Dom QName]
fs     -- Andreas, 2019-11-12/17, issue #4168b
                , Bool
irrProj Bool -> Bool -> Bool
|| (Dom QName -> Bool) -> [Dom QName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Dom QName -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant [Dom QName]
fs -> 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')
                          , argInfoModality :: Modality
argInfoModality = Modality
                            { modRelevance :: Relevance
modRelevance  = Relevance -> Relevance -> Relevance
forall a. Ord a => a -> a -> a
max (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info) (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info')
                            , modQuantity :: Quantity
modQuantity   = Quantity -> Quantity -> Quantity
forall a. Ord a => a -> a -> a
max (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  ArgInfo
info) (ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  ArgInfo
info')
                            , modCohesion :: Cohesion
modCohesion   = Cohesion -> Cohesion -> Cohesion
forall a. Ord a => a -> a -> a
max (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion  ArgInfo
info) (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion  ArgInfo
info')
                            , modPolarity :: PolarityModality
modPolarity   = PolarityModality -> PolarityModality -> PolarityModality
addPolarity (ArgInfo -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity ArgInfo
info) (ArgInfo -> PolarityModality
forall a. LensModalPolarity a => a -> PolarityModality
getModalPolarity ArgInfo
info') -- XXX
                            }
                          , 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
                          , argInfoAnnotation :: Annotation
argInfoAnnotation    = ArgInfo -> Annotation
argInfoAnnotation ArgInfo
info'
                          }
                      vs :: [Arg Term]
vs = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
                  res <- [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
loop ([(Arg Term, Term)]
 -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)])
-> [(Arg Term, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Dom QName -> (Arg Term, Term))
-> [Arg Term] -> [Dom QName] -> [(Arg Term, Term)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' Arg Term -> Dom QName -> (Arg Term, Term)
aux [Arg Term]
vs [Dom QName]
fs
                  return $! res `append` vars
                | Bool
otherwise -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
fallback
              Maybe (QName, RecordData)
_ -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
fallback

          -- An irrelevant argument which is not an irrefutable pattern is dropped
          Term
_ | Bool
irr -> [(Arg Int, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Arg Int, 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 Int, 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 Int
i [])] <- Elims -> Maybe [Arg Term]
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 Int, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a. a -> ExceptT InvertExcept (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Arg Int, Term)]
 -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)])
-> [(Arg Int, Term)]
-> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> Int -> Arg Int
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Int
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 Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
`cons` [(Arg Int, Term)]
vars

          Def{}      -> ExceptT InvertExcept (TCMT IO) [(Arg Int, 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 Int, Term)]
failure Term
tm
          tm :: Term
tm@Lit{}   -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
failure Term
tm
          tm :: Term
tm@MetaV{} -> Term -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
failure Term
tm
          Pi{}       -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
          Sort{}     -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
          Level{}    -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall {a}. ExceptT InvertExcept (TCMT IO) a
neutralArg
          DontCare{} -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall a. HasCallStack => a
__IMPOSSIBLE__ -- Ruled out by stripDontCare
          Dummy DummyTermKind
s Elims
_  -> [Char] -> ExceptT InvertExcept (TCMT IO) [(Arg Int, Term)]
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> [Char]
forall a. Show a => a -> [Char]
show DummyTermKind
s)

  -- managing an assoc list where duplicate indizes cannot be irrelevant vars
  append :: Res -> Res -> Res
  append :: [(Arg Int, Term)] -> [(Arg Int, Term)] -> [(Arg Int, Term)]
append [(Arg Int, Term)]
res [(Arg Int, Term)]
vars = ((Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)])
-> [(Arg Int, Term)] -> [(Arg Int, Term)] -> [(Arg Int, Term)]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
cons [(Arg Int, Term)]
vars [(Arg Int, Term)]
res

  -- adding an irrelevant entry only if not present
  cons :: (Arg Nat, Term) -> Res -> Res
  cons :: (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
cons a :: (Arg Int, Term)
a@(Arg ArgInfo
ai Int
i, Term
t) [(Arg Int, Term)]
vars
    | ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
ai = Bool
-> ([(Arg Int, Term)] -> [(Arg Int, Term)])
-> [(Arg Int, Term)]
-> [(Arg Int, Term)]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (((Arg Int, Term) -> Bool) -> [(Arg Int, Term)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool)
-> ((Arg Int, Term) -> Int) -> (Arg Int, Term) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Int -> Int
forall e. Arg e -> e
unArg (Arg Int -> Int)
-> ((Arg Int, Term) -> Arg Int) -> (Arg Int, Term) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Int, Term) -> Arg Int
forall a b. (a, b) -> a
fst) [(Arg Int, Term)]
vars) ((Arg Int, Term)
a (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
forall a. a -> [a] -> [a]
:) [(Arg Int, Term)]
vars
    | Bool
otherwise       = (Arg Int, Term)
a (Arg Int, Term) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
forall a. a -> [a] -> [a]
:  -- adding a relevant entry
        -- filter out duplicate irrelevants
        ((Arg Int, Term) -> Bool) -> [(Arg Int, Term)] -> [(Arg Int, Term)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Arg Int, Term) -> Bool) -> (Arg Int, Term) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ a :: (Arg Int, Term)
a@(Arg ArgInfo
info Int
j, Term
t) -> ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isIrrelevant ArgInfo
info Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j)) [(Arg Int, Term)]
vars

-- | 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
-> [Arg Term]
-> TCM
     (Maybe
        (MetaVariable, IntMap Bool, [(Int, Term)], Substitution' Term))
isFaceConstraint MetaId
mid [Arg Term]
args = MaybeT
  (TCMT IO)
  (MetaVariable, IntMap Bool, [(Int, Term)], Substitution' Term)
-> TCM
     (Maybe
        (MetaVariable, IntMap Bool, [(Int, Term)], Substitution' Term))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT
   (TCMT IO)
   (MetaVariable, IntMap Bool, [(Int, Term)], Substitution' Term)
 -> TCM
      (Maybe
         (MetaVariable, IntMap Bool, [(Int, Term)], Substitution' Term)))
-> MaybeT
     (TCMT IO)
     (MetaVariable, IntMap Bool, [(Int, Term)], Substitution' Term)
-> TCM
     (Maybe
        (MetaVariable, IntMap Bool, [(Int, Term)], Substitution' Term))
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 -> Type'' Term Term
forall a. Judgement a -> Type'' Term Term
jMetaType (Judgement MetaId -> Type'' Term Term)
-> Judgement MetaId -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mvar
    n = [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args

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

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

  m           <- getContextSize
  TelV tel' _ <- telViewUpToPath 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' Term (Type'' Term Term)))
forall (m :: * -> *).
MonadTCEnv m =>
m (Tele (Dom' Term (Type'' Term Term)))
getContextTelescope

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

    over  = Tele (Dom' Term (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term (Type'' Term Term))
tel' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Tele (Dom' Term (Type'' Term Term)) -> Int
forall a. Sized a => a -> Int
size Tele (Dom' Term (Type'' Term Term))
tel''
    endps = [(Int, Bool)] -> IntMap Bool
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Bool)] -> IntMap Bool) -> [(Int, Bool)] -> IntMap Bool
forall a b. (a -> b) -> a -> b
$ [Maybe (Int, Bool)] -> [(Int, Bool)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Int, Bool)] -> [(Int, Bool)])
-> [Maybe (Int, Bool)] -> [(Int, Bool)]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Int -> Maybe (Int, Bool))
-> [Arg Term] -> [Int] -> [Maybe (Int, Bool)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' (\Arg Term
a Int
i -> Arg Term -> Int -> Maybe (Int, Bool)
fin Arg Term
a (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
over)) [Arg Term]
args (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
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
-> [Arg Term]
-> Term
-> CompareAs
-> TCM ()
tryAddBoundary CompareDirection
dir MetaId
x InteractionId
iid [Arg Term]
args Term
v CompareAs
target = do
  [Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.ip.boundary" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ TCMT IO Doc
"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) -> [Arg Term] -> Elims
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Arg Term]
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 -> Type'' Term Term
forall a. Judgement a -> Type'' Term Term
jMetaType (Judgement MetaId -> Type'' Term Term)
-> Judgement MetaId -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mvar
    n = [Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args
    rhsv = Term -> VarSet
forall t. Free t => t -> VarSet
freeVarSet Term
v

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

  TelV tel' _ <- telViewUpToPath 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' Term (Type'' Term Term)) -> Term -> Term
forall t.
Abstract t =>
Tele (Dom' Term (Type'' Term Term)) -> t -> t
abstract Tele (Dom' Term (Type'' Term Term))
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' Term
Substitution' (SubstArg Term)
rho Term
v
    -- We store the boundary faces directly as lambdas for simplicity.

    enterClosure mvar $ \Range
_ -> do
      [Char] -> Int -> TCMT IO Doc -> MaybeT (TCMT IO) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.ip.boundary" Int
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' Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Substitution' Term
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 (Type'' Term Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type'' Term Term -> m Doc
prettyTCM Type'' Term Term
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 -> Int
forall a. TermSize a => a -> Int
termSize Term
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Term -> Int
forall a. TermSize a => a -> Int
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 :: TCM ()
openMetasToPostulates :: TCM ()
openMetasToPostulates = 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 <$> useTC stOpenMetaStore
  forM_ ms $ \ (MetaId
x, MetaVariable
mv) -> do
    let t :: Type'' Term Term
t = Type'' Term Term -> Type'' Term Term
dummyTypeToOmega (Type'' Term Term -> Type'' Term Term)
-> Type'' Term Term -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ Judgement MetaId -> Type'' Term Term
forall a. Judgement a -> Type'' Term Term
jMetaType (Judgement MetaId -> Type'' Term Term)
-> Judgement MetaId -> Type'' Term Term
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' <- Doc -> [Char]
forall a. Doc a -> [Char]
render (Doc -> [Char]) -> TCMT IO Doc -> TCMT IO [Char]
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 = [Char]
"unsolved#meta." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++! (Char -> Bool) -> [Char] -> [Char]
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_') [Char]
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 [Char]]
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 Setω. This will crash the serializer (issue #3730). To avoid this we replace dummy type
    -- codomains by Setω.
    dummyTypeToOmega :: Type'' Term Term -> Type'' Term Term
dummyTypeToOmega Type'' Term Term
t =
      case Type'' Term Term -> TelV (Type'' Term Term)
telView' Type'' Term Term
t of
        TelV Tele (Dom' Term (Type'' Term Term))
tel (El Sort' Term
_ Dummy{}) -> Tele (Dom' Term (Type'' Term Term))
-> Type'' Term Term -> Type'' Term Term
forall t.
Abstract t =>
Tele (Dom' Term (Type'' Term Term)) -> t -> t
abstract Tele (Dom' Term (Type'' Term Term))
tel (Sort' Term -> Type'' Term Term
sort (Sort' Term -> Type'' Term Term) -> Sort' Term -> Type'' Term Term
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
UType Integer
0)
        TelV (Type'' Term Term)
_ -> Type'' Term Term
t

-- | 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 (Type'' Term Term) -> Set MetaId
forall m.
Monoid m =>
(MetaId -> m) -> Maybe (Type'' Term Term) -> 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 (Type'' Term Term) -> Set MetaId)
-> TCMT IO (Maybe (Type'' Term Term)) -> TCMT IO (Set MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                MetaId -> TCMT IO (Maybe (Type'' Term Term))
forall {m :: * -> *}.
MonadReduce m =>
MetaId -> m (Maybe (Type'' Term Term))
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 (Type'' Term Term))
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 (Type'' Term Term) -> m (Maybe (Type'' Term Term))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Type'' Term Term)
forall a. Maybe a
Nothing
        HasType{ jMetaType :: forall a. Judgement a -> Type'' Term Term
jMetaType = Type'' Term Term
t } -> Type'' Term Term -> Maybe (Type'' Term Term)
forall a. a -> Maybe a
Just (Type'' Term Term -> Maybe (Type'' Term Term))
-> m (Type'' Term Term) -> m (Maybe (Type'' Term Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type'' Term Term -> m (Type'' Term Term)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type'' Term Term
t