{-# LANGUAGE NondecreasingIndentation #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Mikan.Interaction.BasicOps where

import Prelude hiding (null)

import Control.Monad.Except   ( MonadError(..) )
import Control.Monad.State    ( MonadState(..), evalState )
import Control.Monad.Identity ( runIdentity )
import Control.Monad.Trans.Maybe

import Data.Map qualified as Map
import Data.IntMap qualified as IntMap
import Data.Map.Strict qualified as MapS
import Data.Set qualified as Set
import Data.List qualified as List
import Data.Bifunctor (first, second)
import Data.Maybe
import Data.Monoid
import Data.Function (on)
import Data.Text (Text)
import Data.Text qualified as T
import Data.Text.Short (ShortText)
import Data.Text.Short qualified as TS

import Mikan.Interaction.Base
import Mikan.Interaction.Errors
import Mikan.Interaction.Output
import Mikan.Interaction.Options
import Mikan.Interaction.Response (Goals, ResponseContextEntry(..))

import Mikan.Syntax.Concrete qualified as C -- ToDo: Remove with instance of ToConcrete
import Mikan.Syntax.Position
import Mikan.Syntax.Abstract as A hiding (Open, Apply, Assign)
import Mikan.Syntax.Abstract.Views as A
import Mikan.Syntax.Abstract.Pretty
import Mikan.Syntax.Common
import Mikan.Syntax.Concrete.Operators (parseApplication)
import Mikan.Syntax.Info (MetaInfo(..),emptyMetaInfo,exprNoRange,defaultAppInfo_,defaultAppInfo)
import Mikan.Syntax.Info qualified as Info
import Mikan.Syntax.Internal as I
import Mikan.Syntax.Literal
import Mikan.Syntax.Translation.InternalToAbstract
import Mikan.Syntax.Translation.AbstractToConcrete
import Mikan.Syntax.Translation.ConcreteToAbstract
import Mikan.Syntax.Scope.Base
import Mikan.Syntax.Scope.Monad
import Mikan.Syntax.Fixity(Precedence(..), argumentCtx_)
import Mikan.Syntax.Parser

import Mikan.TheTypeChecker
import Mikan.TypeChecking.Conversion.Errors
import Mikan.TypeChecking.Constraints
import Mikan.TypeChecking.Conversion
import Mikan.TypeChecking.Errors.Deferred
import Mikan.TypeChecking.Errors ( getAllWarnings, Verbalize(..) )
import Mikan.TypeChecking.Monad as M hiding (MetaInfo)
import Mikan.TypeChecking.MetaVars
import Mikan.TypeChecking.MetaVars.Mention
import Mikan.TypeChecking.Reduce
import Mikan.TypeChecking.Substitute
import Mikan.TypeChecking.Telescope.Path
import Mikan.TypeChecking.Telescope
import Mikan.TypeChecking.With
import Mikan.TypeChecking.Coverage
import Mikan.TypeChecking.Coverage.SplitPattern ( SplitPattern )
import Mikan.TypeChecking.Records
import Mikan.TypeChecking.Pretty ( PrettyTCM, prettyTCM )
import Mikan.TypeChecking.Pretty.Constraint (prettyRangeConstraint)
import Mikan.TypeChecking.IApplyConfluence
import Mikan.TypeChecking.Primitive
import Mikan.TypeChecking.ProjectionLike (reduceProjectionLike)
import Mikan.TypeChecking.Names
import Mikan.TypeChecking.Free
import Mikan.TypeChecking.CheckInternal
import Mikan.TypeChecking.Pretty qualified as TP
import Mikan.TypeChecking.Warnings
  ( warning, WhichWarnings(..), classifyWarnings, isMetaTCWarning
  , WarningsAndNonFatalErrors )

import Mikan.Termination.TermCheck (termMutual)

import Mikan.Utils.Function (applyWhen)
import Mikan.Utils.Functor
import Mikan.Utils.Lens
import Mikan.Utils.List
import Mikan.Utils.List1 (List1, pattern (:|))
import Mikan.Utils.List1 qualified as List1
import Mikan.Utils.Maybe
import Mikan.Utils.Monad
import Mikan.Utils.Null
import Mikan.Syntax.Common.Pretty as P
import Mikan.Utils.Permutation
import Mikan.Utils.Size
import Mikan.Utils.String
import Mikan.Utils.WithDefault ( WithDefault'(Value) )
import Mikan.Utils.Tuple.Strict (Pair(..))
import Mikan.Utils.Tuple.Strict qualified as Strict
import Mikan.Utils.Maybe.Strict qualified as Strict
import Mikan.Utils.BiMap qualified as BiMap

import Mikan.Utils.Impossible

-- | Get the information associated to an interaction point.
{-# SPECIALIZE lookupInteractionPoint :: InteractionId -> TCM InteractionPoint #-}
lookupInteractionPoint
  :: (ReadTCState m, MonadError TCErr m, MonadTCEnv m)
  => InteractionId -> m InteractionPoint
lookupInteractionPoint :: forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii =
  m InteractionPoint
-> m (Maybe InteractionPoint) -> m InteractionPoint
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (InteractionError -> m InteractionPoint
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m InteractionPoint)
-> InteractionError -> m InteractionPoint
forall a b. (a -> b) -> a -> b
$ InteractionId -> InteractionError
NoSuchInteractionPoint InteractionId
ii) (m (Maybe InteractionPoint) -> m InteractionPoint)
-> m (Maybe InteractionPoint) -> m InteractionPoint
forall a b. (a -> b) -> a -> b
$
    InteractionId
-> BiMap InteractionId InteractionPoint -> Maybe InteractionPoint
forall k v. Ord k => k -> BiMap k v -> Maybe v
BiMap.lookup InteractionId
ii (BiMap InteractionId InteractionPoint -> Maybe InteractionPoint)
-> m (BiMap InteractionId InteractionPoint)
-> m (Maybe InteractionPoint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' TCState (BiMap InteractionId InteractionPoint)
-> m (BiMap InteractionId InteractionPoint)
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useR (BiMap InteractionId InteractionPoint
 -> f (BiMap InteractionId InteractionPoint))
-> TCState -> f TCState
Lens' TCState (BiMap InteractionId InteractionPoint)
stInteractionPoints

{-# SPECIALIZE lookupInteractionId :: InteractionId -> TCM MetaId #-}
-- | Get 'MetaId' for an interaction point.
--   Precondition: interaction point is connected.
lookupInteractionId
  :: (ReadTCState m, MonadError TCErr m, MonadTCEnv m)
  => InteractionId -> m MetaId
lookupInteractionId :: forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii =
  m MetaId -> m (Maybe MetaId) -> m MetaId
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (InteractionError -> m MetaId
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> m MetaId) -> InteractionError -> m MetaId
forall a b. (a -> b) -> a -> b
$ InteractionId -> InteractionError
NoActionForInteractionPoint InteractionId
ii) (m (Maybe MetaId) -> m MetaId) -> m (Maybe MetaId) -> m MetaId
forall a b. (a -> b) -> a -> b
$
    InteractionPoint -> Maybe MetaId
ipMeta (InteractionPoint -> Maybe MetaId)
-> m InteractionPoint -> m (Maybe MetaId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> m InteractionPoint
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii

-- | Get the 'Range' for an interaction point.
{-# SPECIALIZE getInteractionRange :: InteractionId -> TCM Range #-}
getInteractionRange
  :: (MonadInteractionPoints m, MonadDebug m, MonadError TCErr m)
  => InteractionId -> m Range
getInteractionRange :: forall (m :: * -> *).
(MonadInteractionPoints m, MonadDebug m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange = InteractionPoint -> Range
ipRange (InteractionPoint -> Range)
-> (InteractionId -> m InteractionPoint)
-> InteractionId
-> m Range
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> InteractionId -> m InteractionPoint
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint

-- | Set the 'Range' for an interaction point.
{-# SPECIALIZE setInteractionRange :: Range -> InteractionId -> TCM () #-}
setInteractionRange :: (MonadInteractionPoints m, MonadDebug m)
  => Range -> InteractionId -> m ()
setInteractionRange :: forall (m :: * -> *).
(MonadInteractionPoints m, MonadDebug m) =>
Range -> InteractionId -> m ()
setInteractionRange Range
r InteractionId
ii = do
  (BiMap InteractionId InteractionPoint
 -> BiMap InteractionId InteractionPoint)
-> m ()
forall (m :: * -> *).
MonadInteractionPoints m =>
(BiMap InteractionId InteractionPoint
 -> BiMap InteractionId InteractionPoint)
-> m ()
modifyInteractionPoints ((BiMap InteractionId InteractionPoint
  -> BiMap InteractionId InteractionPoint)
 -> m ())
-> (BiMap InteractionId InteractionPoint
    -> BiMap InteractionId InteractionPoint)
-> m ()
forall a b. (a -> b) -> a -> b
$ (InteractionPoint -> Maybe InteractionPoint)
-> InteractionId
-> BiMap InteractionId InteractionPoint
-> BiMap InteractionId InteractionPoint
forall k v.
(Ord k, Ord (Tag v), HasTag v) =>
(v -> Maybe v) -> k -> BiMap k v -> BiMap k v
BiMap.update (\ InteractionPoint
ip -> InteractionPoint -> Maybe InteractionPoint
forall a. a -> Maybe a
Just InteractionPoint
ip{ ipRange = r }) InteractionId
ii
  () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

getInteractionScope ::
  (MonadDebug m, ReadTCState m, MonadError TCErr m,
   MonadTCEnv m) =>
  InteractionId -> m ScopeInfo
getInteractionScope :: forall (m :: * -> *).
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope =
  MetaVariable -> ScopeInfo
getMetaScope (MetaVariable -> ScopeInfo)
-> (MetaId -> m MetaVariable) -> MetaId -> m ScopeInfo
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta (MetaId -> m ScopeInfo)
-> (InteractionId -> m MetaId) -> InteractionId -> m ScopeInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< InteractionId -> m MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId

withInteractionId ::
  (MonadDebug m, MonadError TCErr m, MonadTrace m, MonadTCM m) =>
  InteractionId -> m a -> m a
withInteractionId :: forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m, MonadTrace m, MonadTCM m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i m a
ret = do
  m <- InteractionId -> m MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
  withMetaId m $ withBatchedErrors ret

-- | Parses an expression.
parseExpr :: Range -> String -> TCM C.Expr
parseExpr :: Range -> [Char] -> TCM Expr
parseExpr Range
rng [Char]
s = do
  (C.ExprWhere e wh, attrs) <-
    PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes)
forall a. PM a -> TCM a
runPM (PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes))
-> PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes)
forall a b. (a -> b) -> a -> b
$ Parser ExprWhere -> Range -> Text -> PM (ExprWhere, Attributes)
forall a. Parser a -> Range -> Text -> PM (a, Attributes)
parseRangeString Parser ExprWhere
exprWhereParser Range
rng ([Char] -> Text
T.pack [Char]
s)
  unless (null wh) $ typeError UnexpectedWhere
  return e

parseExprIn :: InteractionId -> Range -> String -> TCM Expr
parseExprIn :: InteractionId -> Range -> [Char] -> TCM Expr
parseExprIn InteractionId
ii Range
rng [Char]
s = do
    e <- Range -> [Char] -> TCM Expr
parseExpr Range
rng [Char]
s
    -- Andreas, 2019-08-19, issue #4007
    -- We need to be in the TCEnv of the meta variable
    -- such that the scope checker can label the clause
    -- of a parsed extended lambda as IsAbstract if the
    -- interaction point was created in AbstractMode.
    withInteractionId ii $ concreteToAbstract_ e

-- | Get the arguments of a 'MetaVariable' in the current context, along
-- with its instantiated type.
--
-- The type of the metavariable is re-abstracted over (as per 'telePi')
-- to remove incidental dependent quantification introduced by the
-- representation of metavariable types.
getMetaArgsType :: MetaVariable -> TCM (I.Args, I.Type)
getMetaArgsType :: MetaVariable -> TCM (Args, Type)
getMetaArgsType MetaVariable
mv = do
  ctx <- MetaVariable -> TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => MetaVariable -> m Args
getMetaContextArgs MetaVariable
mv
  ty <- instantiateFull $ jMetaType (mvJudgement mv)
  teleApply' ty ctx
    (\Telescope
tel Type
ty -> do
      -- can't do reduction here otherwise the Goals list is always
      -- reduced
      let TelV Telescope
tel' Type
ty' = Type -> TelV Type
telView' Type
ty
      (Args, Type) -> TCM (Args, Type)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Args
ctx, Telescope -> Type -> Type
telePi (Telescope
tel Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Telescope
tel') Type
ty'))
    (\Type
_ Args
_    -> TCM (Args, Type)
forall a. HasCallStack => a
__IMPOSSIBLE__)

-- Type check the given expression and assign its value to the meta
-- Precondition: we are in the context where the given meta was created.
giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term
giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term
giveExpr UseForce
force Maybe InteractionId
mii MetaId
mi Expr
e = do
    mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
    let t = case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
              IsSort{}    -> Teletype
forall a. HasCallStack => a
__IMPOSSIBLE__
              HasType MetaId
_ Comparison
_ Teletype
t -> Teletype
t
    reportSDoc "interaction.give" 20 $
      "give: meta type =" TP.<+> prettyTCM t
    -- Here, we must be in the same context where the meta was created.
    -- Thus, we can safely apply its type to the context variables.
    (ctx, t') <- getMetaArgsType mv
    traceCall (CheckExprCall CmpLeq e t') $ do
      reportSDoc "interaction.give" 20 $ do
        a <- viewTC eAbstractMode
        TP.hsep
          [ TP.text ("give(" ++ show a ++ "): instantiated meta type =")
          , prettyTCM t'
          ]
      -- Andreas, 2020-05-27 AIM XXXII, issue #4679
      -- Clear envMutualBlock since cubical only executes
      -- certain checks (checkIApplyConfluence) for an extended lambda
      -- when not in a mutual block.
      v <- locallyTC eMutualBlock (const Nothing) $
        checkExpr e t'
      reportSDoc "interaction.give" 40 $ "give: checked expression:" TP.<+> pure (pretty v)
      case mvInstantiation mv of

        InstV{} -> do
          v' <- Term -> TCM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
mi (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
ctx
          reportSDoc "interaction.give" 20 $ TP.sep
            [ "meta was already set to value v' = " TP.<+> prettyTCM v'
            , "now comparing it to given value v = " TP.<+> prettyTCM v
            , "in context " TP.<+> inTopContext (prettyTCM ctx)
            ]
          equalTerm t' v v'

        MetaInstantiation
_ -> do -- updateMeta mi v
          [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"interaction.give" Int
20 [Char]
"give: meta unassigned, assigning..."
          args <- TCMT IO Args
forall (m :: * -> *). MonadTCEnv m => m Args
getContextArgs
          nowSolvingConstraints $ assign DirEq mi args v (AsTermsOf t')

      reportSDoc "interaction.give" 20 $ "give: meta variable updated!"
      unless (force == WithForce) $ redoChecks mii
      wakeupConstraints mi
      return v

-- | After a give, redo termination etc. checks for function which was complemented.
redoChecks :: Maybe InteractionId -> TCM ()
redoChecks :: Maybe InteractionId -> TCMT IO ()
redoChecks Maybe InteractionId
Nothing = () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
redoChecks (Just InteractionId
ii) = do
  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"interaction.give" Int
20 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [Char]
"give: redoing termination check for function surrounding " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ InteractionId -> [Char]
forall a. Show a => a -> [Char]
show InteractionId
ii
  ip <- InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
  case ipClause ip of
    IPClause
IPNoClause -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    IPClause{ipcQName :: IPClause -> QName
ipcQName = QName
f} -> do
      mb <- Definition -> MutualId
defMutual (Definition -> MutualId) -> TCMT IO Definition -> TCMT IO MutualId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
f
      terErrs <- localTC (set eMutualBlock (Just mb)) $ termMutual []
      List1.unlessNull terErrs $ warning . TerminationIssue
  -- TODO redo positivity check!

-- | Auxiliary definition for 'give' and 'elaborate_give'.
give_ ::
     Bool           -- ^ Elaborating?
  -> UseForce       -- ^ Skip safety checks?
  -> InteractionId  -- ^ Hole.
  -> Expr           -- ^ The expression to give.
  -> TCM Term       -- ^ Value of the expression
give_ :: Bool -> UseForce -> InteractionId -> Expr -> TCM Term
give_ Bool
elaborating UseForce
force InteractionId
ii Expr
e = do
  mi  <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e
  reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e
  -- Try to give mi := e
  withInteractionId ii do
    setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.
    applyWhen elaborating (locallyTC eCurrentlyElaborating $ const True) do
      -- Andreas, 2025-05-02, issue #7842 reproduces this error
      let err Blocker
_blocker = InteractionError -> TCM Term
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> TCM Term) -> InteractionError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Expr -> InteractionError
CannotGive Expr
e
      catchPatternErr err do
        giveExpr force (Just ii) mi e

-- | Try to fill hole by expression.
--
--   Returns the given expression unchanged
--   (for convenient generalization to @'refine'@).
give ::
     UseForce       -- ^ Skip safety checks?
  -> InteractionId  -- ^ Hole.
  -> Expr           -- ^ The expression to give.
  -> TCM Expr       -- ^ If successful, the very expression is returned unchanged.
give :: UseForce -> InteractionId -> Expr -> TCM Expr
give UseForce
force InteractionId
ii Expr
e = do
  _ <- Bool -> UseForce -> InteractionId -> Expr -> TCM Term
give_ Bool
False UseForce
force InteractionId
ii Expr
e
  removeInteractionPoint ii
  return e

-- | Try to fill hole by elaborated expression.
elaborate_give
  :: Rewrite        -- ^ Normalise result?
  -> UseForce       -- ^ Skip safety checks?
  -> InteractionId  -- ^ Hole.
  -> Expr           -- ^ The expression to give.
  -> TCM Expr       -- ^ If successful, return the elaborated expression.
elaborate_give :: Rewrite -> UseForce -> InteractionId -> Expr -> TCM Expr
elaborate_give Rewrite
norm UseForce
force InteractionId
ii Expr
e = InteractionId -> TCM Expr -> TCM Expr
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m, MonadTrace m, MonadTCM m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ do
  v <- Bool -> UseForce -> InteractionId -> Expr -> TCM Term
give_ Bool
True UseForce
force InteractionId
ii Expr
e
  reportSDoc "interaction.give" 40 $ "v = " TP.<+> pure (pretty v)
  -- Reduce projection-likes before quoting, otherwise instance
  -- selection may fail on reload (see #6203).
  nv <- reduceProjectionLike =<< normalForm norm v
  locallyTC ePrintMetasBare (const True) $ reify nv

-- | Try to refine hole by expression @e@.
--
--   This amounts to successively try to give @e@, @e ?@, @e ? ?@, ...
--   Returns the successfully given expression.
refine
  :: UseForce       -- ^ Skip safety checks when giving?
  -> InteractionId  -- ^ Hole.
  -> Expr           -- ^ The expression to refine the hole with.
                    --   Precondition: it was parsed in the context of the hole
                    --   so its ranges are correct.
  -> TCM Expr       -- ^ The successfully given expression.
refine :: UseForce -> InteractionId -> Expr -> TCM Expr
refine UseForce
force InteractionId
ii Expr
e = do
  [Char] -> Int -> TCMT IO (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO (Doc Aspects) -> m ()
reportSDoc [Char]
"interaction.refine" Int
10 (TCMT IO (Doc Aspects) -> TCMT IO ())
-> TCMT IO (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    TCMT IO (Doc Aspects)
"refining with expression" TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.<+> Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Expr -> m (Doc Aspects)
prettyTCM Expr
e
  [Char] -> Int -> TCMT IO (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO (Doc Aspects) -> m ()
reportSDoc [Char]
"interaction.refine" Int
50 (TCMT IO (Doc Aspects) -> TCMT IO ())
-> TCMT IO (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    [Char] -> TCMT IO (Doc Aspects)
forall (m :: * -> *). Applicative m => [Char] -> m (Doc Aspects)
TP.text ([Char] -> TCMT IO (Doc Aspects))
-> [Char] -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Expr -> [Char]
forall a. Show a => a -> [Char]
show (Expr -> [Char]) -> Expr -> [Char]
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope Expr
e
  -- Andreas, 2025-11-12, issue #8197
  -- We use the range of @e@ which might contain questionmarks
  -- so that the new questionmarks appended to @e@
  -- can receive a 'Range' relatively correct to the ranges
  -- of the questionmarks withing @e@.
  let range :: Range
range = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
  scope <- InteractionId -> TCMT IO ScopeInfo
forall (m :: * -> *).
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii
  -- We try to append up to 10 meta variables
  tryRefine 10 range scope e
  where
    -- This wrapper around 'try' makes 'range' and 'scope' available there.
    tryRefine :: Int -> Range -> ScopeInfo  -> Expr -> TCM Expr
    tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine Int
nrOfMetas Range
range ScopeInfo
scope = TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
withHardErrors (TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe TCErr -> Expr -> TCM Expr
try Int
nrOfMetas Maybe TCErr
forall a. Maybe a
Nothing
      where
        try :: Int -> Maybe TCErr -> Expr -> TCM Expr
        try :: Int -> Maybe TCErr -> Expr -> TCM Expr
try Int
0 Maybe TCErr
err Expr
e = do
          [Char] -> Int -> TCMT IO (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO (Doc Aspects) -> m ()
reportSDoc [Char]
"interaction.refine" Int
30 (TCMT IO (Doc Aspects) -> TCMT IO ())
-> TCMT IO (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO (Doc Aspects)
"final error:" TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.$$ Maybe TCErr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *).
MonadPretty m =>
Maybe TCErr -> m (Doc Aspects)
prettyTCM Maybe TCErr
err
          InteractionError -> TCM Expr
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (InteractionError -> TCM Expr) -> InteractionError -> TCM Expr
forall a b. (a -> b) -> a -> b
$ [Char] -> InteractionError
CannotRefine case Maybe TCErr
err of
            Just (TypeError CallStack
_ TCState
_ Closure SomeDiagnostic
cl) | Just (ConversionError Comparison
_ FailedCompareAs
_ I.Pi{} Term
_ ConversionErrorContext
_) <- SomeDiagnostic -> Maybe ConversionError
forall a. Diagnostic a => SomeDiagnostic -> Maybe a
fromSomeDiagnostic (Closure SomeDiagnostic -> SomeDiagnostic
forall a. Closure a -> a
clValue Closure SomeDiagnostic
cl) ->
              [Char]
"functions with 10 or more arguments"
            Maybe TCErr
_ -> [Char]
""
        try Int
n Maybe TCErr
_ Expr
e = UseForce -> InteractionId -> Expr -> TCM Expr
give UseForce
force InteractionId
ii Expr
e TCM Expr -> (TCErr -> TCM Expr) -> TCM Expr
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> do
          [Char] -> Int -> TCMT IO (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO (Doc Aspects) -> m ()
reportSDoc [Char]
"interaction.refine" Int
30 (TCMT IO (Doc Aspects) -> TCMT IO ())
-> TCMT IO (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO (Doc Aspects)
"retrying because of error:" TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.$$ TCErr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => TCErr -> m (Doc Aspects)
prettyTCM TCErr
err
          Int -> Maybe TCErr -> Expr -> TCM Expr
try (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (TCErr -> Maybe TCErr
forall a. a -> Maybe a
Just TCErr
err) (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM Expr
appMeta Expr
e

        -- Apply A.Expr to a new meta
        appMeta :: Expr -> TCM Expr
        appMeta :: Expr -> TCM Expr
appMeta Expr
e = do
          -- Andreas, 2013-05-01 conflate range to its right margin to ensure that appended metas are last in numbering.
          -- This fixes issue 841.
          let rng :: Range
rng = Range -> Range
rightMargin Range
range
          -- Make new interaction point
          ii <- Bool -> Range -> Maybe Int -> TCMT IO InteractionId
forall (m :: * -> *).
MonadInteractionPoints m =>
Bool -> Range -> Maybe Int -> m InteractionId
registerInteractionPoint Bool
False Range
rng Maybe Int
forall a. Maybe a
Nothing
          let info = Info.MetaInfo
                { metaRange :: Range
Info.metaRange = Range
rng
                , metaScope :: ScopeInfo
Info.metaScope = ASetter ScopeInfo ScopeInfo PrecedenceStack PrecedenceStack
-> PrecedenceStack -> ScopeInfo -> ScopeInfo
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter ScopeInfo ScopeInfo PrecedenceStack PrecedenceStack
Lens' ScopeInfo PrecedenceStack
scopePrecedence [Precedence
argumentCtx_] ScopeInfo
scope
                    -- Ulf, 2017-09-07: The `argumentCtx_` above is causing #737.
                    -- If we're building an operator application the precedence
                    -- should be something else.
                , metaNumber :: Maybe MetaId
metaNumber = Maybe MetaId
forall a. Maybe a
Nothing -- in order to print just as ?, not ?n
                , metaNameSuggestion :: ShortText
metaNameSuggestion = ShortText
""
                , metaKind :: MetaKind
metaKind           = MetaKind
Info.UnificationMeta
                }
              metaVar = MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
info InteractionId
ii

              count Name
x a
e = Sum b -> b
forall a. Sum a -> a
getSum (Sum b -> b) -> Sum b -> b
forall a b. (a -> b) -> a -> b
$ (Expr -> Sum b) -> a -> Sum b
forall m. FoldExprFn m a
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> Sum b
isX a
e
                where isX :: Expr -> Sum b
isX (A.Var Name
y) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = b -> Sum b
forall a. a -> Sum a
Sum b
1
                      isX Expr
_                  = Sum b
forall a. Monoid a => a
mempty

              lamView (A.Lam ExprInfo
_ (DomainFree TacticAttribute
_ NamedArg Binder
x) Expr
e) = (Binder, Expr) -> Maybe (Binder, Expr)
forall a. a -> Maybe a
Just (NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x, Expr
e)
              lamView (A.Lam ExprInfo
i (DomainFull (TBind Range
r TypedBindingInfo
t (NamedArg Binder
x :| [NamedArg Binder]
xs) Expr
a)) Expr
e) =
                [NamedArg Binder]
-> Maybe (Binder, Expr)
-> (NonEmpty (NamedArg Binder) -> Maybe (Binder, Expr))
-> Maybe (Binder, Expr)
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [NamedArg Binder]
xs {-then-} ((Binder, Expr) -> Maybe (Binder, Expr)
forall a. a -> Maybe a
Just (NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x, Expr
e)) {-else-} ((NonEmpty (NamedArg Binder) -> Maybe (Binder, Expr))
 -> Maybe (Binder, Expr))
-> (NonEmpty (NamedArg Binder) -> Maybe (Binder, Expr))
-> Maybe (Binder, Expr)
forall a b. (a -> b) -> a -> b
$ \ NonEmpty (NamedArg Binder)
xs ->
                  (Binder, Expr) -> Maybe (Binder, Expr)
forall a. a -> Maybe a
Just (NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x, ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (TypedBinding -> LamBinding
DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. (a -> b) -> a -> b
$ Range
-> TypedBindingInfo
-> NonEmpty (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
t NonEmpty (NamedArg Binder)
xs Expr
a) Expr
e)
              lamView Expr
_ = Maybe (Binder, Expr)
forall a. Maybe a
Nothing

              -- reduce beta-redexes where the argument is used at most once
              smartApp AppInfo
i Expr
e NamedArg Expr
arg =
                case ((Binder, Expr) -> (BindName, Expr))
-> Maybe (Binder, Expr) -> Maybe (BindName, Expr)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Binder -> BindName) -> (Binder, Expr) -> (BindName, Expr)
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 Binder -> BindName
forall a. Binder' a -> a
A.binderName) (Expr -> Maybe (Binder, Expr)
lamView (Expr -> Maybe (Binder, Expr)) -> Expr -> Maybe (Binder, Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
unScope Expr
e) of
                  Just (A.BindName{unBind :: BindName -> Name
unBind = Name
x}, Expr
e) | Name -> Expr -> Integer
forall {b} {a}. (Num b, ExprLike a) => Name -> a -> b
count Name
x Expr
e Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2 -> (Expr -> Expr) -> Expr -> Expr
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
subX Expr
e
                    where subX :: Expr -> Expr
subX (A.Var Name
y) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg Expr
arg
                          subX Expr
e = Expr
e
                  Maybe (BindName, Expr)
_ -> AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
i Expr
e NamedArg Expr
arg
          return $ smartApp (defaultAppInfo range) e $ defaultNamedArg metaVar

{-| Evaluate the given expression in the current environment -}
evalInCurrent :: ComputeMode -> Expr -> TCM Expr
evalInCurrent :: ComputeMode -> Expr -> TCM Expr
evalInCurrent ComputeMode
cmode Expr
e = do
  (v, _t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
  vb <- reduceB v
  reportSDoc "interaction.eval" 30 $ "evaluated to" TP.<+> TP.pretty vb
  v  <- pure $ ignoreBlocking vb
  reify =<< if cmode == HeadCompute then pure v else normalise v


evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
evalInMeta InteractionId
ii ComputeMode
cmode Expr
e =
   do   m <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
        mi <- getMetaInfo <$> lookupLocalMeta m
        withMetaInfo mi $
            evalInCurrent cmode e

-- | Modifier for interactive commands,
--   specifying the amount of normalization in the output.
--
normalForm :: (Reduce t, Simplify t, Instantiate t, Normalise t) => Rewrite -> t -> TCM t
normalForm :: forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm = \case
  Rewrite
AsIs         -> t -> TCM t
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate   -- #4975: reify will also instantiate by for goal-type-and-context-and-check
  Rewrite
Instantiated -> t -> TCM t
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate   --        we get a top-level fresh meta which has disappeared from state by the
  Rewrite
HeadNormal   -> t -> TCM t
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce        --        time we get to reification. Hence instantiate here.
  Rewrite
Simplified   -> t -> TCM t
forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify
  Rewrite
Normalised   -> t -> TCM t
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise

-- | Evaluate the given expression in the current environment
--   with allowed reductions modified according to 'ComputeMode'.
computeInCurrent :: ComputeMode -> Expr -> TCM Expr
computeInCurrent :: ComputeMode -> Expr -> TCM Expr
computeInCurrent ComputeMode
cmode Expr
e =
  ComputeMode -> TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => ComputeMode -> m a -> m a
withComputeIgnoreAbstract ComputeMode
cmode (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ ComputeMode -> Expr -> TCM Expr
evalInCurrent ComputeMode
cmode Expr
e

-- | Modify the allowed reductions according to 'ComputeMode'.
{-# SPECIALIZE withComputeIgnoreAbstract :: ComputeMode -> TCM a -> TCM a #-}
withComputeIgnoreAbstract :: MonadTCEnv m => ComputeMode -> m a -> m a
withComputeIgnoreAbstract :: forall (m :: * -> *) a. MonadTCEnv m => ComputeMode -> m a -> m a
withComputeIgnoreAbstract ComputeMode
cmode =
  Bool -> (m a -> m a) -> m a -> m a
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen (ComputeMode -> Bool
computeIgnoreAbstract ComputeMode
cmode) ((m a -> m a) -> m a -> m a) -> (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$
    m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions (m a -> m a) -> (m a -> m a) -> m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode

computeIgnoreAbstract :: ComputeMode -> Bool
computeIgnoreAbstract :: ComputeMode -> Bool
computeIgnoreAbstract ComputeMode
DefaultCompute  = Bool
False
computeIgnoreAbstract ComputeMode
HeadCompute     = Bool
False
computeIgnoreAbstract ComputeMode
IgnoreAbstract  = Bool
True
computeIgnoreAbstract ComputeMode
UseShowInstance = Bool
False

computeWrapInput :: ComputeMode -> String -> String
computeWrapInput :: ComputeMode -> [Char] -> [Char]
computeWrapInput ComputeMode
UseShowInstance [Char]
s = [Char]
"show (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
computeWrapInput ComputeMode
_               [Char]
s = [Char]
s

showComputed :: ComputeMode -> Expr -> TCM Doc
showComputed :: ComputeMode -> Expr -> TCMT IO (Doc Aspects)
showComputed ComputeMode
UseShowInstance Expr
e =
  case Expr
e of
    A.Lit ExprInfo
_ (LitString ShortText
s) -> Doc Aspects -> TCMT IO (Doc Aspects)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ShortText -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty ShortText
s)
    Expr
_                     -> (Doc Aspects
"Expected applying `show` to the given value to produce a string literal, but got:" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
$$) (Doc Aspects -> Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop Expr
e
showComputed ComputeMode
_ Expr
e = Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop Expr
e

-- | Modifier for interactive commands,
--   specifying whether safety checks should be ignored.
outputFormId :: OutputForm a b -> b
outputFormId :: forall a b. OutputForm a b -> b
outputFormId (OutputForm Range
_ [ProblemId]
_ Blocker
_ OutputConstraint_boot TCErr a b
o) = OutputConstraint_boot TCErr a b -> b
forall {tcErr} {a} {b}. OutputConstraint_boot tcErr a b -> b
out OutputConstraint_boot TCErr a b
o
  where
    out :: OutputConstraint_boot tcErr a b -> b
out = \case
      OfType b
i a
_                 -> b
i
      CmpInType Comparison
_ a
_ b
i b
_          -> b
i
      CmpElim [Polarity]
_ a
_ (b
i:[b]
_) [b]
_        -> b
i
      CmpElim [Polarity]
_ a
_ [] [b]
_           -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
      JustType b
i                 -> b
i
      CmpLevels Comparison
_ b
i b
_            -> b
i
      CmpTypes Comparison
_ b
i b
_             -> b
i
      CmpTeles Comparison
_ b
i b
_             -> b
i
      JustSort b
i                 -> b
i
      CmpSorts Comparison
_ b
i b
_             -> b
i
      Assign b
i a
_                 -> b
i
      TypedAssign b
i a
_ a
_          -> b
i
      PostponedCheckArgs b
i [a]
_ a
_ a
_ -> b
i
      IsEmptyType a
_              -> b
forall a. HasCallStack => a
__IMPOSSIBLE__   -- Should never be used on IsEmpty constraints
      FindInstanceOF b
_ a
_ [(a, a, a)]
_        -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
      ResolveInstanceOF QName
_        -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
      PTSInstance b
i b
_            -> b
i
      PostponedCheckFunDef{}     -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
      DataSort QName
_ b
i               -> b
i
      CheckLock b
i b
_              -> b
i

instance Reify ProblemConstraint where
  type ReifiesTo ProblemConstraint = Closure (OutputForm Expr Expr)
  reify :: forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify (PConstr Set ProblemId
pids Blocker
unblock Closure Constraint
cl) = Closure Constraint
-> (Constraint -> m (OutputForm Expr Expr))
-> m (Closure (OutputForm Expr Expr))
forall (m :: * -> *) a b.
(MonadTCEnv m, ReadTCState m) =>
Closure a -> (a -> m b) -> m (Closure b)
withClosure Closure Constraint
cl ((Constraint -> m (OutputForm Expr Expr))
 -> m (Closure (OutputForm Expr Expr)))
-> (Constraint -> m (OutputForm Expr Expr))
-> m (Closure (OutputForm Expr Expr))
forall a b. (a -> b) -> a -> b
$ \ Constraint
c ->
    Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr Expr Expr
-> OutputForm Expr Expr
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm (Constraint -> Range
forall a. HasRange a => a -> Range
getRange Constraint
c) (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
pids) Blocker
unblock (OutputConstraint_boot TCErr Expr Expr -> OutputForm Expr Expr)
-> m (OutputConstraint_boot TCErr Expr Expr)
-> m (OutputForm Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Constraint -> m (ReifiesTo Constraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Constraint -> m (ReifiesTo Constraint)
reify Constraint
c

reifyElimToExpr :: MonadReify m => I.Elim -> m Expr
reifyElimToExpr :: forall (m :: * -> *). MonadReify m => Elim' Term -> m Expr
reifyElimToExpr = \case
    I.IApply Term
_ Term
_ Term
v -> ShortText -> Arg Expr -> Expr
appl ShortText
"iapply" (Arg Expr -> Expr) -> m (Arg Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> m (ReifiesTo (Arg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Term -> m (ReifiesTo (Arg Term))
reify (Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term
v) -- TODO Andrea: endpoints?
    I.Apply Arg Term
v -> ShortText -> Arg Expr -> Expr
appl ShortText
"apply" (Arg Expr -> Expr) -> m (Arg Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> m (ReifiesTo (Arg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Term -> m (ReifiesTo (Arg Term))
reify Arg Term
v
    I.Proj ProjOrigin
_o QName
f -> ShortText -> Arg Expr -> Expr
appl ShortText
"proj" (Arg Expr -> Expr) -> m (Arg Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> m (ReifiesTo (Arg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Term -> m (ReifiesTo (Arg Term))
reify ((Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
I.Def QName
f []) :: Arg Term)
  where
    appl :: ShortText -> Arg Expr -> Expr
    appl :: ShortText -> Arg Expr -> Expr
appl ShortText
s Arg Expr
v = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Literal -> Expr
A.Lit ExprInfo
forall a. Null a => a
empty (ShortText -> Literal
LitString ShortText
s)) (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ (Expr -> Named NamedName Expr) -> Arg Expr -> NamedArg Expr
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Named NamedName Expr
forall a name. a -> Named name a
unnamed Arg Expr
v

instance Reify Constraint where
  type ReifiesTo Constraint = OutputConstraint Expr Expr

  reify :: forall (m :: * -> *).
MonadReify m =>
Constraint -> m (ReifiesTo Constraint)
reify (ValueCmp Comparison
cmp (AsTermsOf Type
t) Term
u Term
v) = Comparison
-> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
CmpInType Comparison
cmp (Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
u m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
  reify (ValueCmp Comparison
cmp CompareAs
AsTypes Term
u Term
v) = Comparison -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpTypes Comparison
cmp (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
u m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
  reify (ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v) = Comparison
-> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
CmpInType Comparison
cmp (Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
ty) m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Term -> Term
lam_o Term
u) m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Term -> Term
lam_o Term
v)
    where
      lam_o :: Term -> Term
lam_o = ArgInfo -> Abs Term -> Term
I.Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortText -> Term -> Abs Term
forall a. ShortText -> a -> Abs a
NoAbs ShortText
"_"
      ty :: m Type
ty = Names -> NamesT m Type -> m Type
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT m Type -> m Type) -> NamesT m Type -> m Type
forall a b. (a -> b) -> a -> b
$ do
        p <- Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(Monad m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
p
        t <- open t
        pPi' "o" p (\ NamesT m Term
o -> NamesT m Type
t)
  reify (ElimCmp [Polarity]
cmp [IsForced]
_ Type
t Term
v Elims
es1 Elims
es2) =
    [Polarity]
-> Expr
-> [Expr]
-> [Expr]
-> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
[Polarity] -> a -> [b] -> [b] -> OutputConstraint_boot tcErr a b
CmpElim [Polarity]
cmp (Expr -> [Expr] -> [Expr] -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m ([Expr] -> [Expr] -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t m ([Expr] -> [Expr] -> OutputConstraint_boot TCErr Expr Expr)
-> m [Expr] -> m ([Expr] -> OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Elim' Term -> m Expr) -> Elims -> m [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> m Expr
forall (m :: * -> *). MonadReify m => Elim' Term -> m Expr
reifyElimToExpr Elims
es1
                            m ([Expr] -> OutputConstraint_boot TCErr Expr Expr)
-> m [Expr] -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Elim' Term -> m Expr) -> Elims -> m [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> m Expr
forall (m :: * -> *). MonadReify m => Elim' Term -> m Expr
reifyElimToExpr Elims
es2
  reify (LevelCmp Comparison
cmp Level
t Level
t')    = Comparison -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpLevels Comparison
cmp (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
reify Level
t m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
reify Level
t'
  reify (SortCmp Comparison
cmp Sort
s Sort
s')     = Comparison -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpSorts Comparison
cmp (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s'
  reify (UnquoteTactic Term
tac Term
_ Type
goal) = do
      tac <- AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Expr
A.Unquote ExprInfo
exprNoRange) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
tac
      OfType tac <$> reify goal
  reify (UnBlock MetaId
m) = do
      mi <- MetaId -> m MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
      m' <- reify (MetaV m [])
      case mi of
        BlockedConst Term
t -> do
          e  <- Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
t
          return $ Assign m' e
        PostponedTypeCheckingProblem Closure TypeCheckingProblem
cl -> Closure TypeCheckingProblem
-> (TypeCheckingProblem
    -> m (OutputConstraint_boot TCErr Expr Expr))
-> m (OutputConstraint_boot TCErr Expr Expr)
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl ((TypeCheckingProblem -> m (OutputConstraint_boot TCErr Expr Expr))
 -> m (OutputConstraint_boot TCErr Expr Expr))
-> (TypeCheckingProblem
    -> m (OutputConstraint_boot TCErr Expr Expr))
-> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. (a -> b) -> a -> b
$ \case
          CheckExpr Comparison
cmp Expr
e Type
a -> do
              a  <- Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
a
              return $ TypedAssign m' e a
          CheckWithApp Comparison
cmp Type
a WithAppHead
hd QName
_ Elims
_ List1 Expr
as -> do
              a  <- Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
a
              return $ TypedAssign m' (A.WithApp exprNoRange (wahExpr hd) as) a
          CheckWithAppHead Comparison
cmp Type
a Expr
hd Term
_ List1 Expr
as -> do
              a  <- Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
a
              return $ TypedAssign m' (A.WithApp exprNoRange hd as) a
          CheckArgs Comparison
_ ExpandHidden
_ Expr
_ [NamedArg Expr]
args Type
t0 Type
t1 ArgsCheckState CheckedTarget -> TCM Term
_ -> do
            t0 <- Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t0
            t1 <- reify t1
            return $ PostponedCheckArgs m' (map (namedThing . unArg) args) t0 t1
          CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
_ AmbiguousQName
_ Expr
_ [NamedArg Expr]
_ Type
t Int
_ Term
_ Type
_ PrincipalArgTypeMetas
_ -> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. b -> a -> a -> OutputConstraint_boot tcErr a b
TypedAssign Expr
m' Expr
e (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t
          DoQuoteTerm Comparison
cmp Term
v Type
t -> do
            tm <- AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Expr
A.QuoteTerm ExprInfo
exprNoRange) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
            OfType tm <$> reify t
          DisambiguateConstructor (ConstructorDisambiguationData QName
c0 List1 (QName, Type, ConHead)
_cands [NamedArg Expr]
args Type
t) ConHead -> TCM Term
_cont -> do
            t <- Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t
            return $ TypedAssign m' (foldl (A.App empty)  (A.Con $ unambiguous c0) args) t
        OpenMeta{}  -> m (OutputConstraint_boot TCErr Expr Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
        InstV{} -> m (OutputConstraint_boot TCErr Expr Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
  reify (FindInstance Range
_ MetaId
m Maybe [Candidate]
mcands) = Expr
-> Expr
-> [(Expr, Expr, Expr)]
-> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
b -> a -> [(a, a, a)] -> OutputConstraint_boot tcErr a b
FindInstanceOF
    (Expr
 -> Expr
 -> [(Expr, Expr, Expr)]
 -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m (Expr
      -> [(Expr, Expr, Expr)] -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (MetaId -> Elims -> Term
MetaV MetaId
m [])
    m (Expr
   -> [(Expr, Expr, Expr)] -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m ([(Expr, Expr, Expr)]
      -> OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m)
    m ([(Expr, Expr, Expr)] -> OutputConstraint_boot TCErr Expr Expr)
-> m [(Expr, Expr, Expr)]
-> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Candidate]
-> (Candidate -> m (Expr, Expr, Expr)) -> m [(Expr, Expr, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Candidate] -> Maybe [Candidate] -> [Candidate]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Candidate]
mcands) (\ (Candidate CandidateKind
q Term
tm Type
ty OverlapMode
_) -> do
          (,,) (Expr -> Expr -> Expr -> (Expr, Expr, Expr))
-> m Expr -> m (Expr -> Expr -> (Expr, Expr, Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
tm m (Expr -> Expr -> (Expr, Expr, Expr))
-> m Expr -> m (Expr -> (Expr, Expr, Expr))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
tm m (Expr -> (Expr, Expr, Expr)) -> m Expr -> m (Expr, Expr, Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
ty)
  reify (ResolveInstanceHead KwRange
kwr QName
q) = ReifiesTo Constraint -> m (ReifiesTo Constraint)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ReifiesTo Constraint -> m (ReifiesTo Constraint))
-> ReifiesTo Constraint -> m (ReifiesTo Constraint)
forall a b. (a -> b) -> a -> b
$ QName -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. QName -> OutputConstraint_boot tcErr a b
ResolveInstanceOF QName
q
  reify (IsEmpty Range
r Type
a) = Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. a -> OutputConstraint_boot tcErr a b
IsEmptyType (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
a
  reify (CheckFunDef DefInfo
i QName
q [Clause]
cs TCErr
err) = do
    a <- Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
q
    return $ PostponedCheckFunDef q a err
  reify (HasPTSRule Dom Type
a Abs Sort
b) = do
    (a,(x,b)) <- (Type, Abs Sort) -> m (ReifiesTo (Type, Abs Sort))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
(Type, Abs Sort) -> m (ReifiesTo (Type, Abs Sort))
reify (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a,Abs Sort
b)
    return $ PTSInstance a b
  reify (CheckDataSort QName
q Sort
s) = QName -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. QName -> b -> OutputConstraint_boot tcErr a b
DataSort QName
q (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s
  reify (CheckMetaInst MetaId
m) = do
    t <- Judgement MetaId -> Teletype
forall a. Judgement a -> Teletype
jMetaType (Judgement MetaId -> Teletype)
-> (MetaVariable -> Judgement MetaId) -> MetaVariable -> Teletype
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement (MetaVariable -> Teletype) -> m MetaVariable -> m Teletype
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
    OfType <$> reify (MetaV m []) <*> reify t
  reify (CheckType Type
t) = Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. b -> OutputConstraint_boot tcErr a b
JustType (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t
  {-# SPECIALIZE reify :: Constraint -> TCM (ReifiesTo Constraint) #-}

instance (Pretty a, Pretty b) => PrettyTCM (OutputForm a b) where
  prettyTCM :: forall (m :: * -> *).
MonadPretty m =>
OutputForm a b -> m (Doc Aspects)
prettyTCM (OutputForm Range
r [ProblemId]
pids Blocker
unblock OutputConstraint_boot TCErr a b
c) =
    Range -> [ProblemId] -> Blocker -> Doc Aspects -> m (Doc Aspects)
forall (m :: * -> *) (f :: * -> *).
(MonadPretty m, Foldable f, Null (f ProblemId)) =>
Range -> f ProblemId -> Blocker -> Doc Aspects -> m (Doc Aspects)
prettyRangeConstraint Range
r [ProblemId]
pids Blocker
unblock (OutputConstraint_boot TCErr a b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty OutputConstraint_boot TCErr a b
c)
  {-# SPECIALIZE prettyTCM :: (Pretty a, Pretty b) => (OutputForm a b) -> TCM Doc #-}

instance (Pretty a, Pretty b) => Pretty (OutputForm a b) where
  pretty :: OutputForm a b -> Doc Aspects
pretty (OutputForm Range
r [ProblemId]
pids Blocker
unblock OutputConstraint_boot TCErr a b
c) =
    OutputConstraint_boot TCErr a b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty OutputConstraint_boot TCErr a b
c Doc Aspects -> Doc Aspects -> Doc Aspects
<?>
      [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ Range -> Doc Aspects
forall {a} {a}. Pretty a => a -> Doc a
prange Range
r, Doc Aspects -> Doc Aspects
parensNonEmpty ([Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [Blocker -> Doc Aspects
blockedOn Blocker
unblock, [ProblemId] -> Doc Aspects
forall {a}. Pretty a => [a] -> Doc Aspects
prPids [ProblemId]
pids]) ]
    where
      prPids :: [a] -> Doc Aspects
prPids []    = Doc Aspects
forall a. Null a => a
empty
      prPids [a
pid] = Doc Aspects
"belongs to problem" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
pid
      prPids [a]
pids  = Doc Aspects
"belongs to problems" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
fsep (Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
forall (t :: * -> *).
Foldable t =>
Doc Aspects -> t (Doc Aspects) -> [Doc Aspects]
punctuate Doc Aspects
"," ([Doc Aspects] -> [Doc Aspects]) -> [Doc Aspects] -> [Doc Aspects]
forall a b. (a -> b) -> a -> b
$ (a -> Doc Aspects) -> [a] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty [a]
pids)

      comma :: Doc Aspects
comma | [ProblemId] -> Bool
forall a. Null a => a -> Bool
null [ProblemId]
pids = Doc Aspects
forall a. Null a => a
empty
            | Bool
otherwise = Doc Aspects
","

      blockedOn :: Blocker -> Doc Aspects
blockedOn (UnblockOnAll Set Blocker
bs) | Set Blocker -> Bool
forall a. Set a -> Bool
Set.null Set Blocker
bs = Doc Aspects
forall a. Null a => a
empty
      blockedOn (UnblockOnAny Set Blocker
bs) | Set Blocker -> Bool
forall a. Set a -> Bool
Set.null Set Blocker
bs = Doc Aspects
"stuck" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Semigroup a => a -> a -> a
<> Doc Aspects
comma
      blockedOn Blocker
u = Doc Aspects
"blocked on" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> (Blocker -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Blocker
u Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Semigroup a => a -> a -> a
<> Doc Aspects
comma)

      prange :: a -> Doc a
prange a
r | [Char] -> Bool
forall a. Null a => a -> Bool
null [Char]
s = Doc a
forall a. Null a => a
empty
               | Bool
otherwise = [Char] -> Doc a
forall a. [Char] -> Doc a
text ([Char] -> Doc a) -> [Char] -> Doc a
forall a b. (a -> b) -> a -> b
$ [Char]
" [ at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ]"
        where s :: [Char]
s = a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow a
r

instance (Pretty a, Pretty b) => Pretty (OutputConstraint a b) where
  pretty :: OutputConstraint a b -> Doc Aspects
pretty OutputConstraint a b
oc =
    case OutputConstraint a b
oc of
      OfType b
e a
t           -> b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
e Doc Aspects -> a -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> a -> Doc Aspects
.: a
t
      JustType b
e           -> Doc Aspects
"Type" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
e
      JustSort b
e           -> Doc Aspects
"Sort" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
e
      CmpInType Comparison
cmp a
t b
e b
e' -> Comparison -> b -> b -> Doc Aspects
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc Aspects
pcmp Comparison
cmp b
e b
e' Doc Aspects -> a -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> a -> Doc Aspects
.: a
t
      CmpElim [Polarity]
cmp a
t [b]
e [b]
e'   -> [Polarity] -> [b] -> [b] -> Doc Aspects
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc Aspects
pcmp [Polarity]
cmp [b]
e [b]
e' Doc Aspects -> a -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> a -> Doc Aspects
.: a
t
      CmpTypes  Comparison
cmp b
t b
t'   -> Comparison -> b -> b -> Doc Aspects
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc Aspects
pcmp Comparison
cmp b
t b
t'
      CmpLevels Comparison
cmp b
t b
t'   -> Comparison -> b -> b -> Doc Aspects
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc Aspects
pcmp Comparison
cmp b
t b
t'
      CmpTeles  Comparison
cmp b
t b
t'   -> Comparison -> b -> b -> Doc Aspects
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc Aspects
pcmp Comparison
cmp b
t b
t'
      CmpSorts Comparison
cmp b
s b
s'    -> Comparison -> b -> b -> Doc Aspects
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc Aspects
pcmp Comparison
cmp b
s b
s'
      Assign b
m a
e           -> Doc Aspects -> Doc Aspects -> Doc Aspects -> Doc Aspects
bin (b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
m) Doc Aspects
":=" (a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
e)
      TypedAssign b
m a
e a
a    -> Doc Aspects -> Doc Aspects -> Doc Aspects -> Doc Aspects
bin (b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
m) Doc Aspects
":=" (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> Doc Aspects -> Doc Aspects -> Doc Aspects
bin (a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
e) Doc Aspects
":?" (a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
a)
      PostponedCheckArgs b
m [a]
es a
t0 a
t1 ->
        Doc Aspects -> Doc Aspects -> Doc Aspects -> Doc Aspects
bin (b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
m) Doc Aspects
":=" (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ (Doc Aspects -> Doc Aspects
parens (Doc Aspects
"_" Doc Aspects -> a -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> a -> Doc Aspects
.: a
t0) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
fsep ((a -> Doc Aspects) -> [a] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map (Doc Aspects -> Doc Aspects
paren (Doc Aspects -> Doc Aspects)
-> (a -> Doc Aspects) -> a -> Doc Aspects
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty) [a]
es)) Doc Aspects -> a -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> a -> Doc Aspects
.: a
t1
        where paren :: Doc Aspects -> Doc Aspects
paren Doc Aspects
d = Bool -> Doc Aspects -> Doc Aspects
mparens ((Char -> Bool) -> [Char] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
' ', Char
'\n']) ([Char] -> Bool) -> [Char] -> Bool
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> [Char]
forall a. Show a => a -> [Char]
show Doc Aspects
d) Doc Aspects
d
      IsEmptyType a
a        -> Doc Aspects
"Is empty:" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
a
      FindInstanceOF b
s a
t [(a, a, a)]
cs -> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat
        [ Doc Aspects
"Resolve instance argument" Doc Aspects -> Doc Aspects -> Doc Aspects
<?> (b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
s Doc Aspects -> a -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> a -> Doc Aspects
.: a
t)
        , Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects
"Candidate:"
        , Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
4 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat [ Doc Aspects -> Doc Aspects -> Doc Aspects -> Doc Aspects
bin (a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
q) Doc Aspects
"=" (a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
v) Doc Aspects -> a -> Doc Aspects
forall {a}. Pretty a => Doc Aspects -> a -> Doc Aspects
.: a
t | (a
q, a
v, a
t) <- [(a, a, a)]
cs ] ]
      ResolveInstanceOF QName
q ->
        Doc Aspects
"Resolve output type of instance" Doc Aspects -> Doc Aspects -> Doc Aspects
<?> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
q
      PTSInstance b
a b
b      -> Doc Aspects
"PTS instance for" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> (b, b) -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (b
a, b
b)
      PostponedCheckFunDef QName
q a
a TCErr
_err ->
        [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat [ Doc Aspects
"Check definition of" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty QName
q Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
":" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
a ]
             -- , nest 2 "stuck because" <?> pretty err ] -- We don't have Pretty for TCErr
      DataSort QName
q b
s         -> Doc Aspects
"Sort" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
s Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"allows data/record definitions"
      CheckLock b
t b
lk       -> Doc Aspects
"Check lock" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
lk Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"allows" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
t
    where
      bin :: Doc Aspects -> Doc Aspects -> Doc Aspects -> Doc Aspects
bin Doc Aspects
a Doc Aspects
op Doc Aspects
b = [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [Doc Aspects
a, Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects
op Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
b]
      pcmp :: a -> a -> a -> Doc Aspects
pcmp a
cmp a
a a
b = Doc Aspects -> Doc Aspects -> Doc Aspects -> Doc Aspects
bin (a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
a) (a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
cmp) (a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
b)
      Doc Aspects
val .: :: Doc Aspects -> a -> Doc Aspects
.: a
ty = Doc Aspects -> Doc Aspects -> Doc Aspects -> Doc Aspects
bin Doc Aspects
val Doc Aspects
":" (a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
ty)


instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b) where
    type ConOfAbs (OutputForm a b) = OutputForm (ConOfAbs a) (ConOfAbs b)
    toConcrete :: forall (m :: * -> *).
MonadToConcrete m =>
OutputForm a b -> m (ConOfAbs (OutputForm a b))
toConcrete (OutputForm Range
r [ProblemId]
pid Blocker
u OutputConstraint_boot TCErr a b
c) = Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
-> OutputForm_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range
r [ProblemId]
pid Blocker
u (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
 -> OutputForm_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (OutputForm_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OutputConstraint_boot TCErr a b
-> m (ConOfAbs (OutputConstraint_boot TCErr a b))
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *).
MonadToConcrete m =>
OutputConstraint_boot TCErr a b
-> m (ConOfAbs (OutputConstraint_boot TCErr a b))
toConcrete OutputConstraint_boot TCErr a b
c

instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b) where
    type ConOfAbs (OutputConstraint a b) = OutputConstraint (ConOfAbs a) (ConOfAbs b)

    toConcrete :: forall (m :: * -> *).
MonadToConcrete m =>
OutputConstraint a b -> m (ConOfAbs (OutputConstraint a b))
toConcrete (OfType b
e a
t) = ConOfAbs b
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
OfType (ConOfAbs b
 -> ConOfAbs a
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs a
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
e m (ConOfAbs a
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
t
    toConcrete (JustType b
e) = ConOfAbs b -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> OutputConstraint_boot tcErr a b
JustType (ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
e
    toConcrete (JustSort b
e) = ConOfAbs b -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> OutputConstraint_boot tcErr a b
JustSort (ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
e
    toConcrete (CmpInType Comparison
cmp a
t b
e b
e') =
      Comparison
-> ConOfAbs a
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
CmpInType Comparison
cmp (ConOfAbs a
 -> ConOfAbs b
 -> ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m (ConOfAbs b
      -> ConOfAbs b
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
t m (ConOfAbs b
   -> ConOfAbs b
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs b
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> m (ConOfAbs b)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e
                                               m (ConOfAbs b
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> m (ConOfAbs b)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e'
    toConcrete (CmpElim [Polarity]
cmp a
t [b]
e [b]
e') =
      [Polarity]
-> ConOfAbs a
-> [ConOfAbs b]
-> [ConOfAbs b]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
[Polarity] -> a -> [b] -> [b] -> OutputConstraint_boot tcErr a b
CmpElim [Polarity]
cmp (ConOfAbs a
 -> [ConOfAbs b]
 -> [ConOfAbs b]
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m ([ConOfAbs b]
      -> [ConOfAbs b]
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
t m ([ConOfAbs b]
   -> [ConOfAbs b]
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m [ConOfAbs b]
-> m ([ConOfAbs b]
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> [b] -> m (ConOfAbs [b])
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx [b]
e m ([ConOfAbs b]
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m [ConOfAbs b]
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> [b] -> m (ConOfAbs [b])
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx [b]
e'
    toConcrete (CmpTypes Comparison
cmp b
e b
e') = Comparison
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpTypes Comparison
cmp (ConOfAbs b
 -> ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs b
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> b -> m (ConOfAbs b)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e
                                                  m (ConOfAbs b
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> m (ConOfAbs b)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e'
    toConcrete (CmpLevels Comparison
cmp b
e b
e') = Comparison
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpLevels Comparison
cmp (ConOfAbs b
 -> ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs b
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> b -> m (ConOfAbs b)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e
                                                    m (ConOfAbs b
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> m (ConOfAbs b)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e'
    toConcrete (CmpTeles Comparison
cmp b
e b
e') = Comparison
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpTeles Comparison
cmp (ConOfAbs b
 -> ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs b
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
e m (ConOfAbs b
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
e'
    toConcrete (CmpSorts Comparison
cmp b
e b
e') = Comparison
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpSorts Comparison
cmp (ConOfAbs b
 -> ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs b
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> b -> m (ConOfAbs b)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e
                                                  m (ConOfAbs b
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> m (ConOfAbs b)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e'
    toConcrete (Assign b
m a
e) = m (ConOfAbs (OutputConstraint a b))
-> m (ConOfAbs (OutputConstraint a b))
forall (m :: * -> *) a. MonadToConcrete m => m a -> m a
noTakenNames (m (ConOfAbs (OutputConstraint a b))
 -> m (ConOfAbs (OutputConstraint a b)))
-> m (ConOfAbs (OutputConstraint a b))
-> m (ConOfAbs (OutputConstraint a b))
forall a b. (a -> b) -> a -> b
$ ConOfAbs b
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
Assign (ConOfAbs b
 -> ConOfAbs a
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs a
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
m m (ConOfAbs a -> ConOfAbs (OutputConstraint a b))
-> m (ConOfAbs a) -> m (ConOfAbs (OutputConstraint a b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
e
    toConcrete (TypedAssign b
m a
e a
a) = ConOfAbs b
-> ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> a -> a -> OutputConstraint_boot tcErr a b
TypedAssign (ConOfAbs b
 -> ConOfAbs a
 -> ConOfAbs a
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs a
      -> ConOfAbs a
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
m m (ConOfAbs a
   -> ConOfAbs a
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m (ConOfAbs a
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
e
                                                                  m (ConOfAbs a
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
a
    toConcrete (PostponedCheckArgs b
m [a]
args a
t0 a
t1) =
      ConOfAbs b
-> [ConOfAbs a]
-> ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
b -> [a] -> a -> a -> OutputConstraint_boot tcErr a b
PostponedCheckArgs (ConOfAbs b
 -> [ConOfAbs a]
 -> ConOfAbs a
 -> ConOfAbs a
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m ([ConOfAbs a]
      -> ConOfAbs a
      -> ConOfAbs a
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
m m ([ConOfAbs a]
   -> ConOfAbs a
   -> ConOfAbs a
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m [ConOfAbs a]
-> m (ConOfAbs a
      -> ConOfAbs a
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [a] -> m (ConOfAbs [a])
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => [a] -> m (ConOfAbs [a])
toConcrete [a]
args m (ConOfAbs a
   -> ConOfAbs a
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m (ConOfAbs a
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m (ConOfAbs a)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
toConcrete a
t0 m (ConOfAbs a
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m (ConOfAbs a)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
toConcrete a
t1
    toConcrete (IsEmptyType a
a) = ConOfAbs a -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. a -> OutputConstraint_boot tcErr a b
IsEmptyType (ConOfAbs a
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
a
    toConcrete (FindInstanceOF b
s a
t [(a, a, a)]
cs) =
      ConOfAbs b
-> ConOfAbs a
-> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
b -> a -> [(a, a, a)] -> OutputConstraint_boot tcErr a b
FindInstanceOF (ConOfAbs b
 -> ConOfAbs a
 -> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs a
      -> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
s m (ConOfAbs a
   -> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m ([(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m (ConOfAbs a)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
toConcrete a
t
                     m ([(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((a, a, a) -> m (ConOfAbs a, ConOfAbs a, ConOfAbs a))
-> [(a, a, a)] -> m [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
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 (\(a
q,a
tm,a
ty) -> (,,) (ConOfAbs a
 -> ConOfAbs a
 -> ConOfAbs a
 -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
-> m (ConOfAbs a)
-> m (ConOfAbs a
      -> ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (ConOfAbs a)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
toConcrete a
q m (ConOfAbs a
   -> ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
-> m (ConOfAbs a)
-> m (ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m (ConOfAbs a)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
toConcrete a
tm m (ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
-> m (ConOfAbs a) -> m (ConOfAbs a, ConOfAbs a, ConOfAbs a)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m (ConOfAbs a)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
toConcrete a
ty) [(a, a, a)]
cs
    toConcrete (ResolveInstanceOF QName
q) = ConOfAbs (OutputConstraint a b)
-> m (ConOfAbs (OutputConstraint a b))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ConOfAbs (OutputConstraint a b)
 -> m (ConOfAbs (OutputConstraint a b)))
-> ConOfAbs (OutputConstraint a b)
-> m (ConOfAbs (OutputConstraint a b))
forall a b. (a -> b) -> a -> b
$ QName -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. QName -> OutputConstraint_boot tcErr a b
ResolveInstanceOF QName
q
    toConcrete (PTSInstance b
a b
b) = ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> b -> OutputConstraint_boot tcErr a b
PTSInstance (ConOfAbs b
 -> ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs b
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
a m (ConOfAbs b
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
b
    toConcrete (DataSort QName
a b
b)  = QName
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. QName -> b -> OutputConstraint_boot tcErr a b
DataSort QName
a (ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
b
    toConcrete (CheckLock b
a b
b) = ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> b -> OutputConstraint_boot tcErr a b
CheckLock (ConOfAbs b
 -> ConOfAbs b
 -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs b
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
a m (ConOfAbs b
   -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
b
    toConcrete (PostponedCheckFunDef QName
q a
a TCErr
err) = QName
-> ConOfAbs a
-> TCErr
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
QName -> a -> tcErr -> OutputConstraint_boot tcErr a b
PostponedCheckFunDef QName
q (ConOfAbs a
 -> TCErr -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m (TCErr
      -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (ConOfAbs a)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => a -> m (ConOfAbs a)
toConcrete a
a m (TCErr -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> m TCErr
-> m (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCErr -> m TCErr
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TCErr
err

instance (Pretty a, Pretty b) => Pretty (OutputConstraint' a b) where
  pretty :: OutputConstraint' a b -> Doc Aspects
pretty (OfType' b
e a
t) = b -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty b
e Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
":" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty a
t

instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b) where
  type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)
  toConcrete :: forall (m :: * -> *).
MonadToConcrete m =>
OutputConstraint' a b -> m (ConOfAbs (OutputConstraint' a b))
toConcrete (OfType' b
e a
t) = ConOfAbs b
-> ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b)
forall a b. b -> a -> OutputConstraint' a b
OfType' (ConOfAbs b
 -> ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs b)
-> m (ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> m (ConOfAbs b)
forall a (m :: * -> *).
(ToConcrete a, MonadToConcrete m) =>
a -> m (ConOfAbs a)
forall (m :: * -> *). MonadToConcrete m => b -> m (ConOfAbs b)
toConcrete b
e m (ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b))
-> m (ConOfAbs a)
-> m (OutputConstraint' (ConOfAbs a) (ConOfAbs b))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
t

instance Reify a => Reify (IPBoundary' a) where
  type ReifiesTo (IPBoundary' a) = IPBoundary' (ReifiesTo a)
  reify :: forall (m :: * -> *).
MonadReify m =>
IPBoundary' a -> m (ReifiesTo (IPBoundary' a))
reify = (a -> m (ReifiesTo a))
-> IPBoundary' a -> m (IPBoundary' (ReifiesTo a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> IPBoundary' a -> f (IPBoundary' b)
traverse a -> m (ReifiesTo a)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => a -> m (ReifiesTo a)
reify

instance ToConcrete a => ToConcrete (IPBoundary' a) where
  type ConOfAbs (IPBoundary' a) = IPBoundary' (ConOfAbs a)

  toConcrete :: forall (m :: * -> *).
MonadToConcrete m =>
IPBoundary' a -> m (ConOfAbs (IPBoundary' a))
toConcrete = (a -> m (ConOfAbs a))
-> IPBoundary' a -> m (IPBoundary' (ConOfAbs a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> IPBoundary' a -> f (IPBoundary' b)
traverse (Precedence -> a -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadToConcrete m, ToConcrete a) =>
Precedence -> a -> m (ConOfAbs a)
toConcreteCtx Precedence
TopCtx)

instance Pretty c => Pretty (IPFace' c) where
  pretty :: IPFace' c -> Doc Aspects
pretty (IPFace' [(c, c)]
eqs c
val) = do
    let
      xs :: [Doc Aspects]
xs = ((c, c) -> Doc Aspects) -> [(c, c)] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map (\ (c
l,c
r) -> c -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty c
l Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"=" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> c -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty c
r) [(c, c)]
eqs
      -- rhs = case over of
      --         Overapplied    -> "=" <+> pretty meta
      --         NotOverapplied -> mempty
    [Doc Aspects] -> Doc Aspects
forall {a}. Pretty a => [a] -> Doc Aspects
prettyList_ [Doc Aspects]
xs Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects
"⊢" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> c -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty c
val -- <+> rhs

prettyConstraints :: [Closure Constraint] -> TCM [OutputForm C.Expr C.Expr]
prettyConstraints :: [Closure Constraint] -> TCM [OutputForm Expr Expr]
prettyConstraints [Closure Constraint]
cs = do
  [Closure Constraint]
-> (Closure Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Closure Constraint]
cs ((Closure Constraint -> TCMT IO (OutputForm Expr Expr))
 -> TCM [OutputForm Expr Expr])
-> (Closure Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ \ Closure Constraint
c -> do
            cl <- ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify (Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
forall a. Set a
Set.empty Blocker
alwaysUnblock Closure Constraint
c)
            enterClosure cl abstractToConcrete_

namedMetaOf :: OutputConstraint A.Expr a -> a
namedMetaOf :: forall a. OutputConstraint Expr a -> a
namedMetaOf (OfType a
i Expr
_) = a
i
namedMetaOf (JustType a
i) = a
i
namedMetaOf (JustSort a
i) = a
i
namedMetaOf (Assign a
i Expr
_) = a
i
namedMetaOf OutputConstraint_boot TCErr Expr a
_ = a
forall a. HasCallStack => a
__IMPOSSIBLE__

getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm C.Expr C.Expr]
getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm Expr Expr]
getConstraintsMentioning Rewrite
norm MetaId
m = (ProblemConstraint -> TCMT IO ProblemConstraint)
-> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getConstrs ProblemConstraint -> TCMT IO ProblemConstraint
forall {m :: * -> *} {b}.
(InstantiateFull b, MonadReduce m) =>
b -> m b
instantiateBlockingFull (MetaId -> ProblemConstraint -> Bool
forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
m)
  -- could be optimized by not doing a full instantiation up front, with a more clever mentionsMeta.
  where
    instantiateBlockingFull :: b -> m b
instantiateBlockingFull b
p
      = Lens' TCState Bool -> (Bool -> Bool) -> m b -> m b
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 b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$
          b -> m b
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull b
p

    nay :: MaybeT TCM Elims
    nay :: MaybeT (TCMT IO) Elims
nay = TCM (Maybe Elims) -> MaybeT (TCMT IO) Elims
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCM (Maybe Elims) -> MaybeT (TCMT IO) Elims)
-> TCM (Maybe Elims) -> MaybeT (TCMT IO) Elims
forall a b. (a -> b) -> a -> b
$ Maybe Elims -> TCM (Maybe Elims)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Elims
forall a. Maybe a
Nothing

    -- Trying to find the actual meta application, as long as it's not
    -- buried too deep.
    -- We could look further but probably not under binders as that would mess with
    -- the call to @unifyElimsMeta@ below.
    hasHeadMeta :: Constraint -> Maybe Elims
hasHeadMeta Constraint
c =
      case Constraint
c of
        ValueCmp Comparison
_ CompareAs
_ Term
u Term
v           -> Term -> Maybe Elims
isMeta Term
u Maybe Elims -> Maybe Elims -> Maybe Elims
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Maybe Elims
isMeta Term
v
        ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v -> Term -> Maybe Elims
isMeta Term
u Maybe Elims -> Maybe Elims -> Maybe Elims
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Maybe Elims
isMeta Term
v
        -- TODO: extend to other comparisons?
        ElimCmp [Polarity]
cmp [IsForced]
fs Type
t Term
v Elims
as Elims
bs   -> Maybe Elims
forall a. Maybe a
Nothing
        LevelCmp Comparison
cmp Level
u Level
v           -> Maybe Elims
forall a. Maybe a
Nothing
        SortCmp Comparison
cmp Sort
a Sort
b            -> Maybe Elims
forall a. Maybe a
Nothing
        UnBlock{}                  -> Maybe Elims
forall a. Maybe a
Nothing
        FindInstance{}             -> Maybe Elims
forall a. Maybe a
Nothing
        ResolveInstanceHead{}      -> Maybe Elims
forall a. Maybe a
Nothing
        IsEmpty Range
r Type
t                -> Term -> Maybe Elims
isMeta (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t)
        CheckFunDef{}              -> Maybe Elims
forall a. Maybe a
Nothing
        HasPTSRule Dom Type
a Abs Sort
b             -> Maybe Elims
forall a. Maybe a
Nothing
        UnquoteTactic{}            -> Maybe Elims
forall a. Maybe a
Nothing
        CheckDataSort QName
_ Sort
s          -> Sort -> Maybe Elims
isMetaS Sort
s
        CheckMetaInst{}            -> Maybe Elims
forall a. Maybe a
Nothing
        CheckType Type
t                -> Term -> Maybe Elims
isMeta (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t)

    isMeta :: Term -> Maybe Elims
    isMeta :: Term -> Maybe Elims
isMeta (MetaV MetaId
m' Elims
es_m) | MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m' = Elims -> Maybe Elims
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elims
es_m
    isMeta Term
_  = Maybe Elims
forall a. Maybe a
Nothing

    isMetaS :: I.Sort -> Maybe Elims
    isMetaS :: Sort -> Maybe Elims
isMetaS (MetaS MetaId
m' Elims
es_m)
      | MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m' = Elims -> Maybe Elims
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elims
es_m
    isMetaS Sort
_  = Maybe Elims
forall a. Maybe a
Nothing

    getConstrs :: (ProblemConstraint -> TCMT IO ProblemConstraint)
-> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getConstrs ProblemConstraint -> TCMT IO ProblemConstraint
g ProblemConstraint -> Bool
f = TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr])
-> TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ do
      cs <- Constraints -> Constraints
stripConstraintPids (Constraints -> Constraints)
-> (Constraints -> Constraints) -> Constraints -> Constraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Bool) -> Constraints -> Constraints
forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
f (Constraints -> Constraints)
-> TCMT IO Constraints -> TCMT IO Constraints
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ProblemConstraint -> TCMT IO ProblemConstraint)
-> Constraints -> TCMT IO Constraints
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 ProblemConstraint -> TCMT IO ProblemConstraint
g (Constraints -> TCMT IO Constraints)
-> TCMT IO Constraints -> TCMT IO Constraints
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
M.getAllConstraints)
      cs <- caseMaybeM (traverse lookupInteractionPoint =<< isInteractionMeta m) (pure cs) $ \InteractionPoint
ip -> do
        let
          boundary :: Set (IntMap Bool)
boundary = Map (IntMap Bool) Term -> Set (IntMap Bool)
forall k a. Map k a -> Set k
MapS.keysSet (IPBoundary' Term -> Map (IntMap Bool) Term
forall t. IPBoundary' t -> Map (IntMap Bool) t
getBoundary (InteractionPoint -> IPBoundary' Term
ipBoundary InteractionPoint
ip))
          isRedundant :: Constraint -> TCMT IO Bool
isRedundant Constraint
c = case Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims (Elims -> Maybe Args) -> Maybe Elims -> Maybe Args
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Constraint -> Maybe Elims
hasHeadMeta Constraint
c of
            Just Args
apps -> TCMT
  IO (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> TCMT IO Bool
-> ((MetaVariable, IntMap Bool, SubstCand, Substitution)
    -> TCMT IO Bool)
-> TCMT IO Bool
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (MetaId
-> Args
-> TCMT
     IO (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
m Args
apps) (Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) (((MetaVariable, IntMap Bool, SubstCand, Substitution)
  -> TCMT IO Bool)
 -> TCMT IO Bool)
-> ((MetaVariable, IntMap Bool, SubstCand, Substitution)
    -> TCMT IO Bool)
-> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ \(MetaVariable
_, IntMap Bool
endps, SubstCand
_, Substitution
_) ->
              Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ IntMap Bool -> Set (IntMap Bool) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IntMap Bool
endps Set (IntMap Bool)
boundary
            Maybe Args
Nothing -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
        (ProblemConstraint -> TCMT IO Bool)
-> Constraints -> TCMT IO Constraints
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Closure Constraint
 -> (Constraint -> TCMT IO Bool) -> TCMT IO Bool)
-> (Constraint -> TCMT IO Bool)
-> Closure Constraint
-> TCMT IO Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Closure Constraint -> (Constraint -> TCMT IO Bool) -> TCMT IO Bool
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure ((Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (TCMT IO Bool -> TCMT IO Bool)
-> (Constraint -> TCMT IO Bool) -> Constraint -> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> TCMT IO Bool
isRedundant) (Closure Constraint -> TCMT IO Bool)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) Constraints
cs

      reportSDoc "tc.constr.mentioning" 20 $ "getConstraintsMentioning"
      forM cs $ \(PConstr Set ProblemId
s Blocker
ub Closure Constraint
c) -> do
        [Char] -> Int -> TCMT IO (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO (Doc Aspects) -> m ()
reportSDoc [Char]
"tc.constr.mentioning" Int
20 (TCMT IO (Doc Aspects) -> TCMT IO ())
-> TCMT IO (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO (Doc Aspects)
"constraint:  " TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.<+> Closure Constraint -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *).
MonadPretty m =>
Closure Constraint -> m (Doc Aspects)
prettyTCM Closure Constraint
c
        c <- Rewrite -> Closure Constraint -> TCM (Closure Constraint)
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Closure Constraint
c
        let hm = Constraint -> Maybe Elims
hasHeadMeta (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue Closure Constraint
c)
        reportSDoc "tc.constr.mentioning" 20 $ "constraint:  " TP.<+> prettyTCM c
        reportSDoc "tc.constr.mentioning" 20 $ "hasHeadMeta: " TP.<+> prettyTCM hm
        case allApplyElims =<< hm of
          Just Args
as_m -> do
            -- unifyElimsMeta tries to move the constraint into
            -- (an extension of) the context where @m@ comes from.
            MetaId
-> Args
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall a.
MetaId
-> Args
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCM a)
-> TCM a
unifyElimsMeta MetaId
m Args
as_m Closure Constraint
c (([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
 -> TCMT IO (OutputForm Expr Expr))
-> ([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall a b. (a -> b) -> a -> b
$ \ [(Term, Term)]
eqs Constraint
c -> do
              (Closure (OutputForm Expr Expr)
 -> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
 -> TCMT IO (OutputForm Expr Expr))
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> Closure (OutputForm Expr Expr)
-> TCMT IO (OutputForm Expr Expr)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Closure (OutputForm Expr Expr)
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr)
OutputForm Expr Expr -> TCMT IO (ConOfAbs (OutputForm Expr Expr))
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ (Closure (OutputForm Expr Expr) -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (Closure (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr))
ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify (ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr)))
-> (Closure Constraint -> ProblemConstraint)
-> Closure Constraint
-> TCMT IO (Closure (OutputForm Expr Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
s Blocker
ub (Closure Constraint -> TCMT IO (Closure (OutputForm Expr Expr)))
-> TCM (Closure Constraint)
-> TCMT IO (Closure (OutputForm Expr Expr))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Constraint -> TCM (Closure Constraint)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Constraint
c
          Maybe Args
_ -> do
            cl <- ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify (ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint))
-> ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall a b. (a -> b) -> a -> b
$ Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
s Blocker
ub Closure Constraint
c
            enterClosure cl abstractToConcrete_

-- Copied from Agda.TypeChecking.Pretty.Warning.prettyConstraints
stripConstraintPids :: Constraints -> Constraints
stripConstraintPids :: Constraints -> Constraints
stripConstraintPids Constraints
cs = (ProblemConstraint -> ProblemConstraint -> Ordering)
-> Constraints -> Constraints
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Bool -> Bool -> Ordering)
-> (ProblemConstraint -> Bool)
-> ProblemConstraint
-> ProblemConstraint
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ProblemConstraint -> Bool
isBlocked) (Constraints -> Constraints) -> Constraints -> Constraints
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> ProblemConstraint)
-> Constraints -> Constraints
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> ProblemConstraint
stripPids Constraints
cs
  where
    isBlocked :: ProblemConstraint -> Bool
isBlocked = Bool -> Bool
not (Bool -> Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ProblemId -> Bool
forall a. Null a => a -> Bool
null (Set ProblemId -> Bool)
-> (ProblemConstraint -> Set ProblemId)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Set ProblemId
allBlockingProblems (Blocker -> Set ProblemId)
-> (ProblemConstraint -> Blocker)
-> ProblemConstraint
-> Set ProblemId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker
    interestingPids :: Set ProblemId
interestingPids = [Set ProblemId] -> Set ProblemId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set ProblemId] -> Set ProblemId)
-> [Set ProblemId] -> Set ProblemId
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> Set ProblemId)
-> Constraints -> [Set ProblemId]
forall a b. (a -> b) -> [a] -> [b]
map (Blocker -> Set ProblemId
allBlockingProblems (Blocker -> Set ProblemId)
-> (ProblemConstraint -> Blocker)
-> ProblemConstraint
-> Set ProblemId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker) Constraints
cs
    stripPids :: ProblemConstraint -> ProblemConstraint
stripPids (PConstr Set ProblemId
pids Blocker
unblock Closure Constraint
c) = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set ProblemId
pids Set ProblemId
interestingPids) Blocker
unblock Closure Constraint
c

{-# SPECIALIZE interactionIdToMetaId :: InteractionId -> TCM MetaId #-}
-- | Converts an 'InteractionId' to a 'MetaId'.
interactionIdToMetaId :: ReadTCState m => InteractionId -> m MetaId
interactionIdToMetaId :: forall (m :: * -> *). ReadTCState m => InteractionId -> m MetaId
interactionIdToMetaId InteractionId
i = do
  h <- m ModuleNameHash
forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash
  return MetaId
    { metaId     = fromIntegral i
    , metaModule = h
    }

-- | Get meta solutions and constraints.
getConstraints :: Rewrite -> TCM [OutputForm C.Expr C.Expr]
getConstraints :: Rewrite -> TCM [OutputForm Expr Expr]
getConstraints Rewrite
norm = do
    cs <- Constraints -> Constraints
stripConstraintPids (Constraints -> Constraints)
-> TCMT IO Constraints -> TCMT IO Constraints
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
M.getAllConstraints
    cs <- forM cs \ (ProblemConstraint
c :: ProblemConstraint) -> do
            cl <- ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr))
ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify (ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr)))
-> TCMT IO ProblemConstraint
-> TCMT IO (Closure (OutputForm Expr Expr))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite -> ProblemConstraint -> TCMT IO ProblemConstraint
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm ProblemConstraint
c
            enterClosure cl abstractToConcrete_
    ss <- mapM toOutputForm =<< getSolvedInteractionPoints True norm -- get all
    return $ ss ++ cs
  where
    toOutputForm :: (InteractionId, MetaId, Expr) -> m (OutputForm Expr Expr)
toOutputForm (InteractionId
ii, MetaId
mi, Expr
e) = do
      mv <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> m MetaVariable -> m (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
      withMetaInfo mv $ do
        mi <- interactionIdToMetaId ii
        let m = MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
emptyMetaInfo{ metaNumber = Just mi } InteractionId
ii
        let oform :: OutputForm Expr Expr
            oform = Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr Expr Expr
-> OutputForm Expr Expr
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock (OutputConstraint_boot TCErr Expr Expr -> OutputForm Expr Expr)
-> OutputConstraint_boot TCErr Expr Expr -> OutputForm Expr Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
Assign Expr
m Expr
e
        abstractToConcrete_ oform

-- | Reify the boundary of an interaction point as something that can be
-- shown to the user.
getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' C.Expr]
getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' Expr]
getIPBoundary Rewrite
norm InteractionId
ii = InteractionId -> TCM [IPFace' Expr] -> TCM [IPFace' Expr]
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m, MonadTrace m, MonadTCM m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM [IPFace' Expr] -> TCM [IPFace' Expr])
-> TCM [IPFace' Expr] -> TCM [IPFace' Expr]
forall a b. (a -> b) -> a -> b
$ do
  ip <- InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii

  io <- primIOne
  iz <- primIZero

  lookupInteractionMeta ii >>= \case
    Just MetaId
mi -> do
      mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi

      telv@(TelV tel a) <- teleView $ jMetaType $ mvJudgement mv

      reportSDoc "tc.ip.boundary" 30 $ TP.vcat
        [ "reifying interaction point boundary"
        , "tel:       " TP.<+> prettyTCM tel
        , "meta:      " TP.<+> prettyTCM mi
        ]
      reportSDoc "tc.ip.boundary" 30 $ "boundary:  " TP.<+> pure (pretty (getBoundary (ipBoundary ip)))

      withInteractionId ii $ do
      -- The boundary is a map associating terms (lambda abstractions)
      -- to IntMap Bools. The meta solver will wrap each LHS in lambdas
      -- corresponding to the interaction point's context. Each key of
      -- the boundary has a subset of (the interval variables in) the
      -- interaction point's context as a keysSet.
      as <- getContextArgs
      let
        c = Expr -> TCM Expr
Expr -> TCMT IO (ConOfAbs Expr)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ (Expr -> TCM Expr) -> (Term -> TCM Expr) -> Term -> TCM Expr
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> TCM Expr
Term -> TCMT IO (ReifiesTo Term)
forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked (Term -> TCM Expr) -> (Term -> TCM Term) -> Term -> TCM Expr
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Rewrite -> Term -> TCM Term
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm
        go (IntMap Bool
im, Term
rhs) = do
          [Char] -> Int -> TCMT IO (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO (Doc Aspects) -> m ()
reportSDoc [Char]
"tc.ip.boundary" Int
30 (TCMT IO (Doc Aspects) -> TCMT IO ())
-> TCMT IO (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m (Doc Aspects)) -> m (Doc Aspects)
TP.vcat
            [ TCMT IO (Doc Aspects)
"reifying constraint for face" TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.<+> IntMap Bool -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a.
(Applicative m, Pretty a) =>
a -> m (Doc Aspects)
TP.pretty IntMap Bool
im
            ]
          [Char] -> Int -> TCMT IO (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO (Doc Aspects) -> m ()
reportSDoc [Char]
"tc.ip.boundary" Int
30 (TCMT IO (Doc Aspects) -> TCMT IO ())
-> TCMT IO (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO (Doc Aspects)
"term " TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.<+> Term -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Term -> m (Doc Aspects)
TP.prettyTCM Term
rhs
          -- Since the RHS is a lambda we have to apply it to the
          -- context:
          rhs <- Term -> TCM Expr
c (Term
rhs Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
as)

          -- Reify the IntMap Bool as a list of (i = i0) (j = i1) terms:
          eqns <- forM (IntMap.toList im) $ \(Int
a, Bool
b) -> do
            a <- Term -> TCM Expr
c (Int -> Elims -> Term
I.Var Int
a [])
            (,) a <$> c (if b then io else iz)
          pure $ IPFace' eqns rhs
      traverse go $ MapS.toList (getBoundary (ipBoundary ip))
    Maybe MetaId
Nothing -> [IPFace' Expr] -> TCM [IPFace' Expr]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' C.Expr])
typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' Expr])
typeAndFacesInMeta InteractionId
ii Rewrite
norm Expr
expr = InteractionId
-> TCM (Expr, [IPFace' Expr]) -> TCM (Expr, [IPFace' Expr])
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m, MonadTrace m, MonadTCM m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM (Expr, [IPFace' Expr]) -> TCM (Expr, [IPFace' Expr]))
-> TCM (Expr, [IPFace' Expr]) -> TCM (Expr, [IPFace' Expr])
forall a b. (a -> b) -> a -> b
$ do
  (ex, ty) <- Expr -> TCM (Term, Type)
inferExpr Expr
expr
  ty <- normalForm norm ty
  ip <- lookupInteractionPoint ii

  io <- primIOne
  iz <- primIZero
  let
    go IntMap Bool
im = do
      let
        c :: Term -> TCM Expr
c = Expr -> TCM Expr
Expr -> TCMT IO (ConOfAbs Expr)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ (Expr -> TCM Expr) -> (Term -> TCM Expr) -> Term -> TCM Expr
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> TCM Expr
Term -> TCMT IO (ReifiesTo Term)
forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked (Term -> TCM Expr) -> (Term -> TCM Term) -> Term -> TCM Expr
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Rewrite -> Term -> TCM Term
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm
        fa :: [(Int, Bool)]
fa = IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Bool
im
        face :: (Int, Bool) -> Substitution
face (Int
i, Bool
m) = Int -> Term -> Substitution
forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
i (Term -> Substitution) -> Term -> Substitution
forall a b. (a -> b) -> a -> b
$ if Bool
m then Term
io else Term
iz
        sub :: Substitution
sub = ((Int, Bool) -> Substitution -> Substitution)
-> Substitution -> [(Int, Bool)] -> Substitution
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Int, Bool)
f Substitution
s -> Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS ((Int, Bool) -> Substitution
face (Int, Bool)
f) Substitution
s) Substitution
forall a. Substitution' a
idS [(Int, Bool)]
fa
      eqns <- [(Int, Bool)]
-> ((Int, Bool) -> TCMT IO (Expr, Expr)) -> TCMT IO [(Expr, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, Bool)]
fa (((Int, Bool) -> TCMT IO (Expr, Expr)) -> TCMT IO [(Expr, Expr)])
-> ((Int, Bool) -> TCMT IO (Expr, Expr)) -> TCMT IO [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$ \(Int
a, Bool
b) -> do
        a <- Term -> TCM Expr
c (Int -> Elims -> Term
I.Var Int
a [])
        (,) a <$> c (if b then io else iz)
      fmap (IPFace' eqns) . c =<< simplify (applySubst sub ex)

  faces <- traverse go $ MapS.keys (getBoundary (ipBoundary ip))
  ty <- reifyUnblocked ty
  pure (ty, faces)

-- | Goals and Warnings

getGoals :: TCM Goals
getGoals :: TCM Goals
getGoals = Rewrite -> Rewrite -> TCM Goals
getGoals' Rewrite
AsIs Rewrite
Simplified
  -- visible metas (as-is)
  -- hidden metas (unsolved implicit arguments simplified)

getGoals'
  :: Rewrite    -- ^ Degree of normalization of goals.
  -> Rewrite    -- ^ Degree of normalization of hidden goals.
  -> TCM Goals
getGoals' :: Rewrite -> Rewrite -> TCM Goals
getGoals' Rewrite
normVisible Rewrite
normHidden = do
  visibleMetas <- Rewrite -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
typesOfVisibleMetas Rewrite
normVisible
  hiddenMetas <- typesOfHiddenMetas normHidden
  return (visibleMetas, hiddenMetas)

-- | Print open metas nicely.
prettyGoals :: Goals -> TCM Doc
prettyGoals :: Goals -> TCMT IO (Doc Aspects)
prettyGoals ([OutputConstraint_boot TCErr Expr InteractionId]
ims, [OutputConstraint Expr NamedMeta]
hms) = do
  di <- [OutputConstraint_boot TCErr Expr InteractionId]
-> (OutputConstraint_boot TCErr Expr InteractionId
    -> TCMT IO (Doc Aspects))
-> TCMT IO [Doc Aspects]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [OutputConstraint_boot TCErr Expr InteractionId]
ims ((OutputConstraint_boot TCErr Expr InteractionId
  -> TCMT IO (Doc Aspects))
 -> TCMT IO [Doc Aspects])
-> (OutputConstraint_boot TCErr Expr InteractionId
    -> TCMT IO (Doc Aspects))
-> TCMT IO [Doc Aspects]
forall a b. (a -> b) -> a -> b
$ \ OutputConstraint_boot TCErr Expr InteractionId
i ->
    InteractionId -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m, MonadTrace m, MonadTCM m) =>
InteractionId -> m a -> m a
withInteractionId (OutputForm Expr InteractionId -> InteractionId
forall a b. OutputForm a b -> b
outputFormId (OutputForm Expr InteractionId -> InteractionId)
-> OutputForm Expr InteractionId -> InteractionId
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr Expr InteractionId
-> OutputForm Expr InteractionId
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint_boot TCErr Expr InteractionId
i) (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$
      OutputConstraint_boot TCErr Expr InteractionId
-> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop OutputConstraint_boot TCErr Expr InteractionId
i
  dh <- mapM pr hms
  return $ vcat $ di ++ dh
  where
    pr :: OutputConstraint A.Expr NamedMeta -> TCM Doc
    pr :: OutputConstraint Expr NamedMeta -> TCMT IO (Doc Aspects)
pr OutputConstraint Expr NamedMeta
m = do
      let i :: MetaId
i = NamedMeta -> MetaId
nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
forall a b. (a -> b) -> a -> b
$ OutputConstraint Expr NamedMeta -> NamedMeta
forall a. OutputConstraint Expr a -> a
namedMetaOf OutputConstraint Expr NamedMeta
m
      r <- MetaId -> TCMT IO Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
i
      d <- withMetaId i (prettyATop m)
      return $ d <+> "[ at" <+> pretty r <+> "]"

getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
getWarningsAndNonFatalErrors = do
  mws <- WhichWarnings -> TCMT IO (Set TCWarning)
forall (m :: * -> *).
(MonadWarning m, MonadTCM m) =>
WhichWarnings -> m (Set TCWarning)
getAllWarnings WhichWarnings
AllWarnings
  let notMetaWarnings = (TCWarning -> Bool) -> Set TCWarning -> Set TCWarning
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Bool
isMetaTCWarning) Set TCWarning
mws
  return case notMetaWarnings of
    Set TCWarning
ws | Bool -> Bool
not (Set TCWarning -> Bool
forall a. Set a -> Bool
Set.null Set TCWarning
ws) -> Set TCWarning -> WarningsAndNonFatalErrors
classifyWarnings Set TCWarning
ws
    Set TCWarning
_ -> WarningsAndNonFatalErrors
forall a. Null a => a
empty

-- | Collecting the context of the given meta-variable.
getResponseContext
  :: Rewrite      -- ^ Normalise?
  -> InteractionId
  -> TCM [ResponseContextEntry]
getResponseContext :: Rewrite -> InteractionId -> TCM [ResponseContextEntry]
getResponseContext Rewrite
norm InteractionId
ii = InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta InteractionId
ii Rewrite
norm

-- | @getSolvedInteractionPoints True@ returns all solutions,
--   even if just solved by another, non-interaction meta.
--
--   @getSolvedInteractionPoints False@ only returns metas that
--   are solved by a non-meta.

getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints :: Bool -> Rewrite -> TCMT IO [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints Bool
all Rewrite
norm = [[(InteractionId, MetaId, Expr)]]
-> [(InteractionId, MetaId, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(InteractionId, MetaId, Expr)]]
 -> [(InteractionId, MetaId, Expr)])
-> TCMT IO [[(InteractionId, MetaId, Expr)]]
-> TCMT IO [(InteractionId, MetaId, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  ((InteractionId, MetaId)
 -> TCMT IO [(InteractionId, MetaId, Expr)])
-> [(InteractionId, MetaId)]
-> TCMT IO [[(InteractionId, MetaId, Expr)]]
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 (InteractionId, MetaId) -> TCMT IO [(InteractionId, MetaId, Expr)]
solution ([(InteractionId, MetaId)]
 -> TCMT IO [[(InteractionId, MetaId, Expr)]])
-> TCMT IO [(InteractionId, MetaId)]
-> TCMT IO [[(InteractionId, MetaId, Expr)]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [(InteractionId, MetaId)]
forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas
  where
    solution :: (InteractionId, MetaId) -> TCMT IO [(InteractionId, MetaId, Expr)]
solution (InteractionId
i, MetaId
m) = do
      mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
      withMetaInfo (getMetaInfo mv) $ do
        args  <- getContextArgs
        scope <- getScope
        let sol Term
v = do
              -- Andreas, 2014-02-17 exclude metas solved by metas
              v <- Term -> TCM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v
              let isMeta = case Term
v of MetaV{} -> Bool
True; Term
_ -> Bool
False
              if isMeta && not all then return [] else do
                e <- blankNotInScope =<< reify =<< normalForm norm v
                return [(i, m, ScopedExpr scope e)]
            unsol = [a] -> TCMT IO [a]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        case mvInstantiation mv of
          InstV{}                        -> Term -> TCMT IO [(InteractionId, MetaId, Expr)]
sol (MetaId -> Elims -> Term
MetaV MetaId
m (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args)
          OpenMeta{}                     -> TCMT IO [(InteractionId, MetaId, Expr)]
forall {a}. TCMT IO [a]
unsol
          BlockedConst{}                 -> TCMT IO [(InteractionId, MetaId, Expr)]
forall {a}. TCMT IO [a]
unsol
          PostponedTypeCheckingProblem{} -> TCMT IO [(InteractionId, MetaId, Expr)]
forall {a}. TCMT IO [a]
unsol

typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI Rewrite
norm MetaId
mi =
     do mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
        withMetaInfo (getMetaInfo mv) $
          rewriteJudg mv (mvJudgement mv)
   where
    rewriteJudg :: MetaVariable -> Judgement MetaId ->
                   TCM (OutputConstraint Expr NamedMeta)
    rewriteJudg :: MetaVariable
-> Judgement MetaId -> TCM (OutputConstraint Expr NamedMeta)
rewriteJudg MetaVariable
mv (HasType MetaId
i Comparison
cmp Teletype
t) = do
      ms <- MetaId -> TCMT IO ShortText
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m ShortText
getMetaNameSuggestion MetaId
i
      (vs, t) <- getMetaArgsType mv
      t <- normalForm norm t
      let x = ShortText -> MetaId -> NamedMeta
NamedMeta ShortText
ms MetaId
i
      reportSDoc "interactive.meta" 10 $ TP.vcat
        [ TP.text $ unwords ["permuting", show i, "with", show $ mvPermutation mv]
        , TP.nest 2 $ TP.vcat
          [ "len  =" TP.<+> TP.text (show $ length vs)
          , "args =" TP.<+> prettyTCM vs
          , "t    =" TP.<+> prettyTCM t
          , "x    =" TP.<+> TP.pretty x
          ]
        ]
      reportSDoc "interactive.meta.scope" 90 $ TP.text $ show $ getMetaScope mv
      -- Andreas, 2016-01-19, issue #1783: need piApplyM instead of just piApply
      OfType x <$> reifyUnblocked t
    rewriteJudg MetaVariable
mv (IsSort MetaId
i Teletype
t) = do
      ms <- MetaId -> TCMT IO ShortText
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m ShortText
getMetaNameSuggestion MetaId
i
      return $ JustSort $ NamedMeta ms i


typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta :: Rewrite
-> InteractionId
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
typeOfMeta Rewrite
norm InteractionId
ii = Rewrite
-> (InteractionId, MetaId)
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
typeOfMeta' Rewrite
norm ((InteractionId, MetaId)
 -> TCM (OutputConstraint_boot TCErr Expr InteractionId))
-> (MetaId -> (InteractionId, MetaId))
-> MetaId
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionId
ii,) (MetaId -> TCM (OutputConstraint_boot TCErr Expr InteractionId))
-> TCMT IO MetaId
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii

typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta' :: Rewrite
-> (InteractionId, MetaId)
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
typeOfMeta' Rewrite
norm (InteractionId
ii, MetaId
mi) = (NamedMeta -> InteractionId)
-> OutputConstraint Expr NamedMeta
-> OutputConstraint_boot TCErr Expr InteractionId
forall a b.
(a -> b)
-> OutputConstraint_boot TCErr Expr a
-> OutputConstraint_boot TCErr Expr b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\NamedMeta
_ -> InteractionId
ii) (OutputConstraint Expr NamedMeta
 -> OutputConstraint_boot TCErr Expr InteractionId)
-> TCM (OutputConstraint Expr NamedMeta)
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI Rewrite
norm MetaId
mi

typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
typesOfVisibleMetas Rewrite
norm =
  TCM [OutputConstraint_boot TCErr Expr InteractionId]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [OutputConstraint_boot TCErr Expr InteractionId]
 -> TCM [OutputConstraint_boot TCErr Expr InteractionId])
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
forall a b. (a -> b) -> a -> b
$ ((InteractionId, MetaId)
 -> TCM (OutputConstraint_boot TCErr Expr InteractionId))
-> [(InteractionId, MetaId)]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
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 (Rewrite
-> (InteractionId, MetaId)
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
typeOfMeta' Rewrite
norm) ([(InteractionId, MetaId)]
 -> TCM [OutputConstraint_boot TCErr Expr InteractionId])
-> TCMT IO [(InteractionId, MetaId)]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [(InteractionId, MetaId)]
forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas

typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas Rewrite
norm = TCM [OutputConstraint Expr NamedMeta]
-> TCM [OutputConstraint Expr NamedMeta]
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [OutputConstraint Expr NamedMeta]
 -> TCM [OutputConstraint Expr NamedMeta])
-> TCM [OutputConstraint Expr NamedMeta]
-> TCM [OutputConstraint Expr NamedMeta]
forall a b. (a -> b) -> a -> b
$ do
  is    <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
  store <- MapS.filterWithKey (implicit is) <$> useR stOpenMetaStore

  -- Suppress reporting *any* unsolved metas if there are metas standing
  -- for type errors.
  if any mvError store
    then pure []
    else mapM (typeOfMetaMI norm) $ MapS.keys store

  where
  implicit :: t a -> a -> MetaVariable -> Bool
implicit t a
is a
x MetaVariable
m | Maybe MetaId -> Bool
forall a. Maybe a -> Bool
isJust (MetaVariable -> Maybe MetaId
mvTwin MetaVariable
m) = Bool
False
  implicit t a
is a
x MetaVariable
m =
    case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
m of
      M.InstV{}        -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      M.OpenMeta MetaKind
_     -> a
x a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t a
is  -- OR: True in case of InstanceMeta !?
      M.BlockedConst{} -> Bool
False
      M.PostponedTypeCheckingProblem{} -> Bool
False

-- | Create type of application of new helper function that would solve the goal.
metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr C.Name)
metaHelperType :: Rewrite
-> InteractionId
-> Range
-> [Char]
-> TCM (OutputConstraint' Expr Name)
metaHelperType Rewrite
norm InteractionId
ii Range
rng [Char]
s = InteractionId
-> TCM (OutputConstraint' Expr Name)
-> TCM (OutputConstraint' Expr Name)
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m, MonadTrace m, MonadTCM m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii do
    -- Parse the raw application.
    ce <- Range -> [Char] -> TCM Expr
parseExpr Range
rng [Char]
s
    -- Operator-parse into simple application of @h@ to @cargs@.
    (h, cargs) <- applicationView [] ce
    -- Scope check arguments
    args <- mapM (fmap deepUnscope . concreteToAbstract_) cargs
      -- Andreas, 2025-09-14:
      -- The 'deepUnscope' has been taken from the previous version of the implementation.
      -- Removing it changes the way the type of the helper function is printed,
      -- sometimes for the better, sometimes for the worse.
      -- TODO: investigate why and how this 'deepUnscope' affects the printing,
      -- and whether we should remove it here.

    cxtNames <- getContextNames
    reportSDoc "interaction.helper" 30 $ TP.vcat $
      [ "args =" TP.<+> prettyTCM args
      , "cxt  =" TP.<+> prettyTCM cxtNames
      ]
    enclosingFunctionName <- ipcQName . view eClause <$> getEnv
    (_, a0) <- getMetaArgsType =<< lookupLocalMeta =<< lookupInteractionId ii

    -- Konstantin, 2022-10-23: We don't want to print section parameters in helper type.
    freeVars <- getCurrentModuleFreeVars
    ctx <- getContext
    let contextForAbstracting = Int -> Context -> [ContextEntry]
cxTake (Context -> Int
forall a. Sized a => a -> Int
size Context
ctx Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
freeVars) Context
ctx

    -- Andreas, 2019-10-11: I actually prefer pi-types over ->.
    let runInPrintingEnvironment = (TCEnv -> TCEnv) -> TCM Expr -> TCM Expr
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (ASetter TCEnv TCEnv Bool Bool -> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Bool Bool
Lens' TCEnv Bool
ePrintDomainFreePi Bool
True (TCEnv -> TCEnv) -> (TCEnv -> TCEnv) -> TCEnv -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter TCEnv TCEnv Bool Bool -> Bool -> TCEnv -> TCEnv
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter TCEnv TCEnv Bool Bool
Lens' TCEnv Bool
ePrintMetasBare Bool
True)
                                 (TCM Expr -> TCM Expr)
-> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Impossible -> Int -> TCM Expr -> TCM Expr
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible ([ContextEntry] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ContextEntry]
contextForAbstracting)
                                 (TCM Expr -> TCM Expr)
-> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM Expr -> TCM Expr
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withoutPrintingGeneralization
                                 (TCM Expr -> TCM Expr)
-> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
dontFoldLetBindings

    case mapM (isVar . namedArg) args of

     -- Andreas, 2019-10-11
     -- If all arguments are variables, there is no need to abstract.
     -- We simply make exactly the given arguments visible and all other hidden.
     -- Andreas, 2025-10-22, issue #8150:
     -- Also, the arguments need to be in the same order as in the context.
     Just [Name]
xs | [Name]
xs [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSubsequenceOf` [Name]
cxtNames -> do
      let inXs :: Name -> Bool
inXs = [Name] -> Name -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [Name]
xs
      let hideButXs :: ContextEntry -> ContextEntry
hideButXs ContextEntry
ce = Hiding -> ContextEntry -> ContextEntry
forall a. LensHiding a => Hiding -> a -> a
setHiding (if Name -> Bool
inXs (ContextEntry -> Name
ctxEntryName ContextEntry
ce) then Hiding
NotHidden else Hiding
Hidden) ContextEntry
ce
      let tel :: Telescope
tel = Context -> Telescope
contextToTel (Context -> Telescope)
-> ([ContextEntry] -> Context) -> [ContextEntry] -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ContextEntry] -> Context
forall a. [a] -> Context' a
Context ([ContextEntry] -> Context)
-> ([ContextEntry] -> [ContextEntry]) -> [ContextEntry] -> Context
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ContextEntry -> ContextEntry) -> [ContextEntry] -> [ContextEntry]
forall a b. (a -> b) -> [a] -> [b]
map ContextEntry -> ContextEntry
hideButXs ([ContextEntry] -> Telescope) -> [ContextEntry] -> Telescope
forall a b. (a -> b) -> a -> b
$ [ContextEntry]
contextForAbstracting
      Name -> Expr -> OutputConstraint' Expr Name
forall a b. b -> a -> OutputConstraint' a b
OfType' Name
h (Expr -> OutputConstraint' Expr Name)
-> TCM Expr -> TCM (OutputConstraint' Expr Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        TCM Expr -> TCM Expr
runInPrintingEnvironment (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ Type -> TCM (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (Type -> TCM (ReifiesTo Type)) -> Type -> TCM (ReifiesTo Type)
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> Type
telePiVisible Telescope
tel Type
a0

     -- If some arguments are not variables or not in the right order (in this case, @args@ is not empty).
     Maybe [Name]
_ -> do
      -- cleanupType relies on with arguments being named 'w',
      -- so we'd better rename any actual 'w's to avoid confusion.
      let tel :: Telescope
tel = Identity Telescope -> Telescope
forall a. Identity a -> a
runIdentity (Identity Telescope -> Telescope)
-> ([ContextEntry] -> Identity Telescope)
-> [ContextEntry]
-> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ShortText -> Identity ShortText)
-> Telescope -> Identity Telescope
forall (f :: * -> *).
Applicative f =>
(ShortText -> f ShortText) -> Telescope -> f Telescope
onNamesTel ShortText -> Identity ShortText
forall {a} {m :: * -> *}. (Eq a, IsString a, Monad m) => a -> m a
unW (Telescope -> Identity Telescope)
-> ([ContextEntry] -> Telescope)
-> [ContextEntry]
-> Identity Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Telescope
contextToTel (Context -> Telescope)
-> ([ContextEntry] -> Context) -> [ContextEntry] -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ContextEntry] -> Context
forall a. [a] -> Context' a
Context ([ContextEntry] -> Telescope) -> [ContextEntry] -> Telescope
forall a b. (a -> b) -> a -> b
$
                [ContextEntry]
contextForAbstracting
      let a :: Type
a = Identity Type -> Type
forall a. Identity a -> a
runIdentity (Identity Type -> Type) -> (Type -> Identity Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ShortText -> Identity ShortText) -> Type -> Identity Type
forall (m :: * -> *).
Applicative m =>
(ShortText -> m ShortText) -> Type -> m Type
onNames ShortText -> Identity ShortText
forall {a} {m :: * -> *}. (Eq a, IsString a, Monad m) => a -> m a
unW (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
a0
      vtys <- (NamedArg Expr -> TCMT IO (Arg (Term, EqualityView)))
-> NonEmpty (NamedArg Expr)
-> TCMT IO (NonEmpty (Arg (Term, EqualityView)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM (\ NamedArg Expr
a -> ((Term, Type) -> Arg (Term, EqualityView))
-> TCM (Term, Type) -> TCMT IO (Arg (Term, EqualityView))
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> (Term, EqualityView) -> Arg (Term, EqualityView)
forall e. ArgInfo -> e -> Arg e
Arg (NamedArg Expr -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Expr
a) ((Term, EqualityView) -> Arg (Term, EqualityView))
-> ((Term, Type) -> (Term, EqualityView))
-> (Term, Type)
-> Arg (Term, EqualityView)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> EqualityView) -> (Term, Type) -> (Term, EqualityView)
forall a b. (a -> b) -> (Term, a) -> (Term, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> EqualityView
OtherType) (TCM (Term, Type) -> TCMT IO (Arg (Term, EqualityView)))
-> TCM (Term, Type) -> TCMT IO (Arg (Term, EqualityView))
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Term, Type)
inferExpr (Expr -> TCM (Term, Type)) -> Expr -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg Expr
a) (NonEmpty (NamedArg Expr)
 -> TCMT IO (NonEmpty (Arg (Term, EqualityView))))
-> NonEmpty (NamedArg Expr)
-> TCMT IO (NonEmpty (Arg (Term, EqualityView)))
forall a b. (a -> b) -> a -> b
$
        NonEmpty (NamedArg Expr)
-> [NamedArg Expr] -> NonEmpty (NamedArg Expr)
forall a. List1 a -> [a] -> List1 a
List1.fromListSafe NonEmpty (NamedArg Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__ [NamedArg Expr]
args
      -- Remember the arity of a
      TelV atel _ <- telView a
      let arity = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
atel
          -- The module parameters are already absent from tel
          (delta1, delta2, _, a', vtys') = splitTelForWith 0 tel a vtys
      a <- runInPrintingEnvironment $ do
        reify =<< cleanupType arity args =<< normalForm norm =<< fst <$> withFunctionType delta1 vtys' delta2 a' empty
      reportSDoc "interaction.helper" 10 do
        let extractOtherType = \case { OtherType Type
a -> Type
a; EqualityView
_ -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__ }
        let (vs, as)   = List1.unzipWith (fmap extractOtherType . unArg) vtys
        let (vs', as') = List1.unzipWith (fmap extractOtherType . unArg) vtys'
        TP.vcat
          [ "generating helper function"
          , TP.nest 2 $ "tel    = " TP.<+> inTopContext (prettyTCM tel)
          , TP.nest 2 $ "a      = " TP.<+> prettyTCM a
          , TP.nest 2 $ "vs     = " TP.<+> prettyTCM vs
          , TP.nest 2 $ "as     = " TP.<+> prettyTCM as
          , TP.nest 2 $ "delta1 = " TP.<+> inTopContext (prettyTCM delta1)
          , TP.nest 2 $ "delta2 = " TP.<+> inTopContext (addContext delta1 $ prettyTCM delta2)
          , TP.nest 2 $ "a'     = " TP.<+> inTopContext (addContext delta1 $ addContext delta2 $ prettyTCM a')
          , TP.nest 2 $ "as'    = " TP.<+> inTopContext (addContext delta1 $ prettyTCM as')
          , TP.nest 2 $ "vs'    = " TP.<+> inTopContext (addContext delta1 $ prettyTCM vs')
          ]
      return $ OfType' h a
  where
    failure :: TCMT IO a
failure = InteractionError -> TCMT IO a
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError InteractionError
ExpectedApplication

    -- An application view for concrete expressions that rejects operator applications.
    -- Takes a suffix of the arguments in left-to-right order (e.g. the empty list)
    -- and returns the head and the arguments in left-to-right order.
    applicationView :: [NamedArg C.Expr] -> C.Expr -> TCM (C.Name, [NamedArg C.Expr])
    applicationView :: [NamedArg Expr] -> Expr -> TCM (Name, [NamedArg Expr])
applicationView [NamedArg Expr]
args = \case
      C.Ident (C.QName Name
x) -> (Name, [NamedArg Expr]) -> TCM (Name, [NamedArg Expr])
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x, [NamedArg Expr]
args)
      C.App Range
_ Expr
e NamedArg Expr
e1        -> [NamedArg Expr] -> Expr -> TCM (Name, [NamedArg Expr])
applicationView (NamedArg Expr
e1 NamedArg Expr -> [NamedArg Expr] -> [NamedArg Expr]
forall a. a -> [a] -> [a]
: [NamedArg Expr]
args) Expr
e
      C.RawApp Range
_ List2 Expr
es       -> [NamedArg Expr] -> Expr -> TCM (Name, [NamedArg Expr])
applicationView [NamedArg Expr]
args (Expr -> TCM (Name, [NamedArg Expr]))
-> TCM Expr -> TCM (Name, [NamedArg Expr])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< List2 Expr -> TCM Expr
parseApplication List2 Expr
es
      C.Paren Range
_ Expr
e         -> [NamedArg Expr] -> Expr -> TCM (Name, [NamedArg Expr])
applicationView [NamedArg Expr]
args Expr
e
      -- Allowing operator applications would not make sense.
      -- C.OpApp _ x _ args -> failure
      Expr
_ -> TCM (Name, [NamedArg Expr])
forall {a}. TCMT IO a
failure

    isVar :: A.Expr -> Maybe A.Name
    isVar :: Expr -> Maybe Name
isVar = \case
      A.Var Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
      Expr
_ -> Maybe Name
forall a. Maybe a
Nothing
    cleanupType :: Int -> [NamedArg Expr] -> Type -> TCM Type
cleanupType Int
arity [NamedArg Expr]
args Type
t = do
      -- Get the arity of t
      TelV ttel _ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
      -- Compute the number of pi-types subject to stripping.
      let n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ttel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
arity
      -- It cannot be negative, otherwise we would have performed a
      -- negative number of with-abstractions.
      unless (n >= 0) __IMPOSSIBLE__
      return $ evalState (renameVars $ stripUnused n t) args

    getBody :: Expr -> Expr
getBody (A.Let ExprInfo
_ List1 LetBinding
_ Expr
e)      = Expr
e
    getBody Expr
_                  = Expr
forall a. HasCallStack => a
__IMPOSSIBLE__

    -- Strip the non-dependent abstractions from the first n abstractions.
    stripUnused :: t -> Type -> Type
stripUnused t
n (El Sort
s Term
v) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ t -> Term -> Term
strip t
n Term
v
    strip :: t -> Term -> Term
strip t
0 = Term -> Term
forall a. a -> a
id
    strip t
n = \case
      I.Pi Dom Type
a Abs Type
b -> case t -> Type -> Type
stripUnused (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) (Type -> Type) -> Abs Type -> Abs Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b of
        Abs Type
b | Abs Type -> ShortText
forall a. Abs a -> ShortText
absName Abs Type
b ShortText -> ShortText -> Bool
forall a. Eq a => a -> a -> Bool
== ShortText
"w"   -> Dom Type -> Abs Type -> Term
I.Pi Dom Type
a Abs Type
b
        NoAbs ShortText
_ Type
b              -> Type -> Term
forall t a. Type'' t a -> a
unEl Type
b
        Abs ShortText
s Type
b | Int
0 Int -> Type -> Bool
forall t. Free t => Int -> t -> Bool
`freeIn` Type
b -> Dom Type -> Abs Type -> Term
I.Pi (Dom Type -> Dom Type
forall a. LensHiding a => a -> a
hide Dom Type
a) (ShortText -> Type -> Abs Type
forall a. ShortText -> a -> Abs a
Abs ShortText
s Type
b)
                | Bool
otherwise    -> Impossible -> Term -> Term
forall a. Subst a => Impossible -> a -> a
strengthen Impossible
HasCallStack => Impossible
impossible (Type -> Term
forall t a. Type'' t a -> a
unEl Type
b)
      Term
v -> Term
v  -- todo: handle if goal type is a Pi

    -- renameVars = onNames (stringToArgName <.> renameVar . argNameToString)
    renameVars :: Type -> State [NamedArg Expr] Type
renameVars = (ShortText -> StateT [NamedArg Expr] Identity ShortText)
-> Type -> State [NamedArg Expr] Type
forall (m :: * -> *).
Applicative m =>
(ShortText -> m ShortText) -> Type -> m Type
onNames ShortText -> StateT [NamedArg Expr] Identity ShortText
renameVar

    -- onNames :: Applicative m => (ArgName -> m ArgName) -> I.Type -> m I.Type
    onNames :: Applicative m => (ShortText -> m ShortText) -> I.Type -> m I.Type
    onNames :: forall (m :: * -> *).
Applicative m =>
(ShortText -> m ShortText) -> Type -> m Type
onNames ShortText -> m ShortText
f (El Sort
s Term
v) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ShortText -> m ShortText) -> Term -> m Term
forall {f :: * -> *}.
Applicative f =>
(ShortText -> f ShortText) -> Term -> f Term
onNamesTm ShortText -> m ShortText
f Term
v

    onNamesTel :: Applicative f => (ShortText -> f ShortText) -> I.Telescope -> f I.Telescope
    onNamesTel :: forall (f :: * -> *).
Applicative f =>
(ShortText -> f ShortText) -> Telescope -> f Telescope
onNamesTel ShortText -> f ShortText
f Telescope
I.EmptyTel = Telescope -> f Telescope
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Telescope
forall a. Tele a
I.EmptyTel
    onNamesTel ShortText -> f ShortText
f (I.ExtendTel Dom Type
a Abs Telescope
b) = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
I.ExtendTel (Dom Type -> Abs Telescope -> Telescope)
-> f (Dom Type) -> f (Abs Telescope -> Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> f Type) -> Dom Type -> f (Dom Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' Term a -> f (Dom' Term b)
traverse ((ShortText -> f ShortText) -> Type -> f Type
forall (m :: * -> *).
Applicative m =>
(ShortText -> m ShortText) -> Type -> m Type
onNames ShortText -> f ShortText
f) Dom Type
a f (Abs Telescope -> Telescope) -> f (Abs Telescope) -> f Telescope
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ShortText -> f ShortText)
-> ((ShortText -> f ShortText) -> Telescope -> f Telescope)
-> Abs Telescope
-> f (Abs Telescope)
forall {f :: * -> *} {t} {a}.
Applicative f =>
(ShortText -> f ShortText)
-> ((ShortText -> f ShortText) -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs ShortText -> f ShortText
f (ShortText -> f ShortText) -> Telescope -> f Telescope
forall (f :: * -> *).
Applicative f =>
(ShortText -> f ShortText) -> Telescope -> f Telescope
onNamesTel Abs Telescope
b

    onNamesTm :: (ShortText -> f ShortText) -> Term -> f Term
onNamesTm ShortText -> f ShortText
f = \case
      I.Var Int
x Elims
es   -> Int -> Elims -> Term
I.Var Int
x (Elims -> Term) -> f Elims -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ShortText -> f ShortText) -> Elims -> f Elims
onNamesElims ShortText -> f ShortText
f Elims
es
      I.Def QName
q Elims
es   -> QName -> Elims -> Term
I.Def QName
q (Elims -> Term) -> f Elims -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ShortText -> f ShortText) -> Elims -> f Elims
onNamesElims ShortText -> f ShortText
f Elims
es
      I.Con ConHead
c ConInfo
ci Elims
args -> ConHead -> ConInfo -> Elims -> Term
I.Con ConHead
c ConInfo
ci (Elims -> Term) -> f Elims -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ShortText -> f ShortText) -> Elims -> f Elims
onNamesArgs ShortText -> f ShortText
f Elims
args
      I.Lam ArgInfo
i Abs Term
b    -> ArgInfo -> Abs Term -> Term
I.Lam ArgInfo
i (Abs Term -> Term) -> f (Abs Term) -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ShortText -> f ShortText)
-> ((ShortText -> f ShortText) -> Term -> f Term)
-> Abs Term
-> f (Abs Term)
forall {f :: * -> *} {t} {a}.
Applicative f =>
(ShortText -> f ShortText)
-> ((ShortText -> f ShortText) -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs ShortText -> f ShortText
f (ShortText -> f ShortText) -> Term -> f Term
onNamesTm Abs Term
b
      I.Pi Dom Type
a Abs Type
b     -> Dom Type -> Abs Type -> Term
I.Pi (Dom Type -> Abs Type -> Term)
-> f (Dom Type) -> f (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> f Type) -> Dom Type -> f (Dom Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' Term a -> f (Dom' Term b)
traverse ((ShortText -> f ShortText) -> Type -> f Type
forall (m :: * -> *).
Applicative m =>
(ShortText -> m ShortText) -> Type -> m Type
onNames ShortText -> f ShortText
f) Dom Type
a f (Abs Type -> Term) -> f (Abs Type) -> f Term
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ShortText -> f ShortText)
-> ((ShortText -> f ShortText) -> Type -> f Type)
-> Abs Type
-> f (Abs Type)
forall {f :: * -> *} {t} {a}.
Applicative f =>
(ShortText -> f ShortText)
-> ((ShortText -> f ShortText) -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs ShortText -> f ShortText
f (ShortText -> f ShortText) -> Type -> f Type
forall (m :: * -> *).
Applicative m =>
(ShortText -> m ShortText) -> Type -> m Type
onNames Abs Type
b
      I.DontCare Term
v -> Term -> Term
I.DontCare (Term -> Term) -> f Term -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ShortText -> f ShortText) -> Term -> f Term
onNamesTm ShortText -> f ShortText
f Term
v
      v :: Term
v@I.Lit{}    -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
      v :: Term
v@I.Sort{}   -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
      v :: Term
v@I.Level{}  -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
      v :: Term
v@I.MetaV{}  -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
      v :: Term
v@I.Dummy{}  -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
    onNamesElims :: (ShortText -> f ShortText) -> Elims -> f Elims
onNamesElims ShortText -> f ShortText
f = (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Elim' Term -> f (Elim' Term)) -> Elims -> f Elims)
-> (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
forall a b. (a -> b) -> a -> b
$ (Term -> f Term) -> Elim' Term -> f (Elim' Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse ((Term -> f Term) -> Elim' Term -> f (Elim' Term))
-> (Term -> f Term) -> Elim' Term -> f (Elim' Term)
forall a b. (a -> b) -> a -> b
$ (ShortText -> f ShortText) -> Term -> f Term
onNamesTm ShortText -> f ShortText
f
    onNamesArgs :: (ShortText -> f ShortText) -> Elims -> f Elims
onNamesArgs ShortText -> f ShortText
f  = (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Elim' Term -> f (Elim' Term)) -> Elims -> f Elims)
-> (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
forall a b. (a -> b) -> a -> b
$ (Term -> f Term) -> Elim' Term -> f (Elim' Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse ((Term -> f Term) -> Elim' Term -> f (Elim' Term))
-> (Term -> f Term) -> Elim' Term -> f (Elim' Term)
forall a b. (a -> b) -> a -> b
$ (ShortText -> f ShortText) -> Term -> f Term
onNamesTm ShortText -> f ShortText
f
    onNamesAbs :: (ShortText -> f ShortText)
-> ((ShortText -> f ShortText) -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs ShortText -> f ShortText
f   = (ShortText -> f ShortText)
-> (ShortText -> f ShortText)
-> ((ShortText -> f ShortText) -> t -> f a)
-> Abs t
-> f (Abs a)
forall {f :: * -> *} {t} {t} {a}.
Applicative f =>
t
-> (ShortText -> f ShortText)
-> (t -> t -> f a)
-> Abs t
-> f (Abs a)
onNamesAbs' ShortText -> f ShortText
f (ShortText -> ShortText
stringToArgName (ShortText -> ShortText)
-> (ShortText -> f ShortText) -> ShortText -> f ShortText
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> ShortText -> f ShortText
f (ShortText -> f ShortText)
-> (ShortText -> ShortText) -> ShortText -> f ShortText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortText -> ShortText
argNameToString)
    onNamesAbs' :: t
-> (ShortText -> f ShortText)
-> (t -> t -> f a)
-> Abs t
-> f (Abs a)
onNamesAbs' t
f ShortText -> f ShortText
f' t -> t -> f a
nd (Abs   ShortText
s t
x) = ShortText -> a -> Abs a
forall a. ShortText -> a -> Abs a
Abs   (ShortText -> a -> Abs a) -> f ShortText -> f (a -> Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ShortText -> f ShortText
f' ShortText
s f (a -> Abs a) -> f a -> f (Abs a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> t -> f a
nd t
f t
x
    onNamesAbs' t
f ShortText -> f ShortText
f' t -> t -> f a
nd (NoAbs ShortText
s t
x) = ShortText -> a -> Abs a
forall a. ShortText -> a -> Abs a
NoAbs (ShortText -> a -> Abs a) -> f ShortText -> f (a -> Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ShortText -> f ShortText
f' ShortText
s f (a -> Abs a) -> f a -> f (Abs a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> t -> f a
nd t
f t
x

    unW :: a -> m a
unW a
"w" = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
".w"
    unW a
s   = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
s

    renameVar :: ShortText -> StateT [NamedArg Expr] Identity ShortText
renameVar ShortText
"w" = StateT [NamedArg Expr] Identity ShortText
betterName
    renameVar ShortText
s   = ShortText -> StateT [NamedArg Expr] Identity ShortText
forall a. a -> StateT [NamedArg Expr] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ShortText
s

    betterName :: StateT [NamedArg Expr] Identity ShortText
betterName = do
      xs <- StateT [NamedArg Expr] Identity [NamedArg Expr]
forall s (m :: * -> *). MonadState s m => m s
get
      case xs of
        []         -> StateT [NamedArg Expr] Identity ShortText
forall a. HasCallStack => a
__IMPOSSIBLE__
        NamedArg Expr
arg : [NamedArg Expr]
args -> do
          [NamedArg Expr] -> StateT [NamedArg Expr] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [NamedArg Expr]
args
          ShortText -> StateT [NamedArg Expr] Identity ShortText
forall a. a -> StateT [NamedArg Expr] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (ShortText -> StateT [NamedArg Expr] Identity ShortText)
-> ShortText -> StateT [NamedArg Expr] Identity ShortText
forall a b. (a -> b) -> a -> b
$ if
            | Arg ArgInfo
_ (Named Maybe NamedName
_ (A.Var Name
x)) <- NamedArg Expr
arg -> [Char] -> ShortText
TS.pack (Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Name -> [Char]) -> Name -> [Char]
forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete Name
x)
            | Just ShortText
x <- NamedArg Expr -> Maybe ShortText
forall a.
(LensNamed a, NameOf a ~ NamedName) =>
a -> Maybe ShortText
bareNameOf NamedArg Expr
arg         -> ShortText -> ShortText
argNameToString ShortText
x
            | Bool
otherwise                        -> ShortText
"w"


-- | Gives a list of names and corresponding types.
--   This list includes not only the local variables in scope, but also the let-bindings.

contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta InteractionId
ii Rewrite
norm = InteractionId
-> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m, MonadTrace m, MonadTCM m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM [ResponseContextEntry] -> TCM [ResponseContextEntry])
-> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
forall a b. (a -> b) -> a -> b
$ do
  info <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> TCMT IO MetaVariable -> TCMT IO (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta (MetaId -> TCMT IO MetaVariable)
-> TCMT IO MetaId -> TCMT IO MetaVariable
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii)
  withMetaInfo info $ do
    -- List of local variables.
    cxt <- getContext
    let localVars = Context -> [ContextEntry]
flattenContext Context
cxt
    -- List of let-bindings.
    letVars <- Map.toAscList <$> viewTC eLetBindings
    -- Reify the types and filter out bindings without a name.
    (++) <$> forMaybeM localVars mkVar
         <*> forMaybeM letVars mkLet

  where
    mkVar :: ContextEntry -> TCM (Maybe ResponseContextEntry)
    mkVar :: ContextEntry -> TCMT IO (Maybe ResponseContextEntry)
mkVar (CtxVar Name
name dom :: Dom Type
dom@(Dom Type -> Type
forall t e. Dom' t e -> e
unDom -> Type
t)) = do
      let ai :: ArgInfo
ai = Dom Type
dom Dom Type -> Getting ArgInfo (Dom Type) ArgInfo -> ArgInfo
forall s a. s -> Getting a s a -> a
^. Getting ArgInfo (Dom Type) ArgInfo
forall t e (f :: * -> *).
Functor f =>
(ArgInfo -> f ArgInfo) -> Dom' t e -> f (Dom' t e)
dInfo
      if ArgInfo -> Name -> Bool
shouldHide ArgInfo
ai Name
name then Maybe ResponseContextEntry -> TCMT IO (Maybe ResponseContextEntry)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ResponseContextEntry
forall a. Maybe a
Nothing else ResponseContextEntry -> Maybe ResponseContextEntry
forall a. a -> Maybe a
Just (ResponseContextEntry -> Maybe ResponseContextEntry)
-> TCMT IO ResponseContextEntry
-> TCMT IO (Maybe ResponseContextEntry)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        let n :: Name
n = Name -> Name
nameConcrete Name
name
        x  <- Name -> TCMT IO (ConOfAbs Name)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ Name
name
        let s = Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
C.isInScope Name
x
        ty <- reifyUnblocked =<< normalForm norm t
        return $ ResponseContextEntry n x (Arg ai ty) Nothing s

    mkLet :: (Name, Open M.LetBinding) -> TCM (Maybe ResponseContextEntry)
    mkLet :: (Name, Open LetBinding) -> TCMT IO (Maybe ResponseContextEntry)
mkLet (Name
name, Open LetBinding
lb) = do
      LetBinding isAxiom _ tm !dom <- Open LetBinding -> TCMT IO LetBinding
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open LetBinding
lb
      if shouldHide (domInfo dom) name then return Nothing else Just <$> do
        let n = Name -> Name
nameConcrete Name
name
        x  <- abstractToConcrete_ name
        let s = Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
C.isInScope Name
x
        ty <- reifyUnblocked =<< normalForm norm dom
              -- Remove let bindings from x and later, to avoid folding to x = x, or using bindings
              -- not introduced when x was defined.
        mv <- case isAxiom of
          -- Andreas, 2026-01-29, issue #8344: do not print bindings for 'LetAxiom's.
          IsAxiom
YesAxiom -> Maybe Expr -> TCMT IO (Maybe Expr)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Expr
forall a. Maybe a
Nothing
          IsAxiom
NoAxiom  -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> TCM Expr -> TCMT IO (Maybe Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Name -> TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => Name -> m a -> m a
removeLetBindingsFrom Name
name (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ Term -> TCM Expr
Term -> TCMT IO (ReifiesTo Term)
forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked (Term -> TCM Expr) -> TCM Term -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite -> Term -> TCM Term
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Term
tm
        return $ ResponseContextEntry n x ty mv s

    shouldHide :: ArgInfo -> A.Name -> Bool
    shouldHide :: ArgInfo -> Name -> Bool
shouldHide ArgInfo
ai Name
n = Bool -> Bool
not (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai) Bool -> Bool -> Bool
&& (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
n Bool -> Bool -> Bool
|| Name -> Bool
nameIsRecordName Name
n)

-- | Returns the type of the expression in the current environment
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
norm Expr
e =
    do  (_,t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
        v <- normalForm norm t
        reifyUnblocked v



typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
ii Rewrite
norm Expr
e =
   do   m <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
        mi <- getMetaInfo <$> lookupLocalMeta m
        withMetaInfo mi $
            typeInCurrent norm e

-- | The intro tactic.
--
-- Returns the terms (as strings) that can be
-- used to refine the goal. Uses the coverage checker
-- to find out which constructors are possible.
--
introTactic :: Bool -> InteractionId -> TCM [String]
introTactic :: Bool -> InteractionId -> TCM [[Char]]
introTactic Bool
pmLambda InteractionId
ii = do
  mi <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  mv <- lookupLocalMeta mi
  withMetaInfo (getMetaInfo mv) $ case mvJudgement mv of
    HasType MetaId
_ Comparison
_ Teletype
t -> do
        (as, t) <- MetaVariable -> TCM (Args, Type)
getMetaArgsType MetaVariable
mv

        -- Andreas, 2013-03-05 Issue 810: skip hidden domains in introduction
        -- of constructor.
        TelV tel' t <- telViewUpTo' (-1) notVisible t
        -- if we cannot introduce a constructor, we try a lambda
        let fallback = do
              TelV tel _ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
              reportSDoc "interaction.intro" 20 $ TP.sep
                [ "introTactic/fallback"
                , "tel' = " TP.<+> prettyTCM tel'
                , "tel  = " TP.<+> prettyTCM tel
                ]
              case (tel', tel) of
                (Telescope
EmptyTel, Telescope
EmptyTel) -> [[Char]] -> TCM [[Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
                (Telescope, Telescope)
_ -> ListTel -> TCM [[Char]]
introFun (Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ShortText, t)]
telToList Telescope
tel' ListTel -> ListTel -> ListTel
forall a. [a] -> [a] -> [a]
++ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ShortText, t)]
telToList Telescope
tel)

        case unEl t of
          I.Def QName
d Elims
_ -> do
            def <- QName -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m Definition
getConstInfo QName
d
            case theDef def of
              Datatype{}    -> Telescope -> TCM [[Char]] -> TCM [[Char]]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel' (TCM [[Char]] -> TCM [[Char]]) -> TCM [[Char]] -> TCM [[Char]]
forall a b. (a -> b) -> a -> b
$ AllowAmbiguousNames -> Type -> TCM [[Char]]
introData AllowAmbiguousNames
AmbiguousNothing Type
t
              Record{ recNamedCon :: Defn -> Bool
recNamedCon = Bool
name }
                | Bool
name      -> Telescope -> TCM [[Char]] -> TCM [[Char]]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel' (TCM [[Char]] -> TCM [[Char]]) -> TCM [[Char]] -> TCM [[Char]]
forall a b. (a -> b) -> a -> b
$ AllowAmbiguousNames -> Type -> TCM [[Char]]
introData AllowAmbiguousNames
AmbiguousConProjs Type
t
                | Bool
otherwise -> Telescope -> TCM [[Char]] -> TCM [[Char]]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel' (TCM [[Char]] -> TCM [[Char]]) -> TCM [[Char]] -> TCM [[Char]]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [[Char]]
introRec QName
d
              Defn
_ -> TCM [[Char]]
fallback
          Term
_ -> TCM [[Char]]
fallback
     TCM [[Char]] -> (TCErr -> TCM [[Char]]) -> TCM [[Char]]
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> [[Char]] -> TCM [[Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Judgement MetaId
_ -> TCM [[Char]]
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    conName :: [NamedArg SplitPattern] -> [I.ConHead]
    conName :: [NamedArg SplitPattern] -> [ConHead]
conName [NamedArg SplitPattern
p] = [ ConHead
c | I.ConP ConHead
c ConPatternInfo
_ [NamedArg SplitPattern]
_ <- [NamedArg SplitPattern -> SplitPattern
forall a. NamedArg a -> a
namedArg NamedArg SplitPattern
p] ]
    conName [NamedArg SplitPattern]
_   = [ConHead]
forall a. HasCallStack => a
__IMPOSSIBLE__

    showUnambiguousConName :: AllowAmbiguousNames -> ConHead -> TCM String
    showUnambiguousConName :: AllowAmbiguousNames -> ConHead -> TCM [Char]
showUnambiguousConName AllowAmbiguousNames
amb ConHead
c = Doc Aspects -> [Char]
forall a. Doc a -> [Char]
render (Doc Aspects -> [Char])
-> (QName -> Doc Aspects) -> QName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (QName -> [Char]) -> TCMT IO QName -> TCM [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
      AllowAmbiguousNames -> QName -> TCMT IO QName
forall (m :: * -> *).
MonadAbsToCon m =>
AllowAmbiguousNames -> QName -> m QName
abstractToConcreteQName AllowAmbiguousNames
amb (QName -> TCMT IO QName) -> QName -> TCMT IO QName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
I.conName ConHead
c

    showTCM :: PrettyTCM a => a -> TCM String
    showTCM :: forall a. PrettyTCM a => a -> TCM [Char]
showTCM = Doc Aspects -> [Char]
forall a. Doc a -> [Char]
render (Doc Aspects -> [Char])
-> (a -> TCMT IO (Doc Aspects)) -> a -> TCM [Char]
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> a -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => a -> m (Doc Aspects)
prettyTCM

    introFun :: ListTel -> TCM [String]
    introFun :: ListTel -> TCM [[Char]]
introFun ListTel
tel = Telescope -> TCM [[Char]] -> TCM [[Char]]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel' (TCM [[Char]] -> TCM [[Char]]) -> TCM [[Char]] -> TCM [[Char]]
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> Int -> TCMT IO (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO (Doc Aspects) -> m ()
reportSDoc [Char]
"interaction.intro" Int
10 (TCMT IO (Doc Aspects) -> TCMT IO ())
-> TCMT IO (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do TCMT IO (Doc Aspects)
"introFun" TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.<+> Telescope -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Telescope -> m (Doc Aspects)
prettyTCM (ListTel -> Telescope
telFromList ListTel
tel)
        imp <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
        let okHiding0 Hiding
h = Bool
imp Bool -> Bool -> Bool
|| Hiding
h Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
NotHidden
            -- if none of the vars were displayed, we would get a parse error
            -- thus, we switch to displaying all
            allHidden   = Bool -> Bool
not ((Hiding -> Bool) -> [Hiding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Hiding -> Bool
okHiding0 [Hiding]
hs)
            okHiding    = if Bool
allHidden then Bool -> Hiding -> Bool
forall a b. a -> b -> a
const Bool
True else Hiding -> Bool
okHiding0
        vars <- -- setShowImplicitArguments (imp || allHidden) $
                applyWhen allHidden withShowAllArguments $
                  mapM showTCM [ setHiding h $ defaultArg $ var i :: Arg Term
                               | (h, i) <- zip hs $ downFrom n
                               , okHiding h
                               ]
        if pmLambda
           then return [ unwords $ ["λ", "{"] ++ vars ++ ["→", "?", "}"] ]
           else return [ unwords $ ["λ"]      ++ vars ++ ["→", "?"] ]
      where
        n :: Int
n = ListTel -> Int
forall a. Sized a => a -> Int
size ListTel
tel
        hs :: [Hiding]
hs   = (Dom (ShortText, Type) -> Hiding) -> ListTel -> [Hiding]
forall a b. (a -> b) -> [a] -> [b]
map Dom (ShortText, Type) -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ListTel
tel
        tel' :: Telescope
tel' = ListTel -> Telescope
telFromList [ ((ShortText, Type) -> (ShortText, Type))
-> Dom (ShortText, Type) -> Dom (ShortText, Type)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ShortText, Type) -> (ShortText, Type)
forall {a} {b}. (Eq a, IsString a) => (a, b) -> (a, b)
makeName Dom (ShortText, Type)
b | Dom (ShortText, Type)
b <- ListTel
tel ]
        makeName :: (a, b) -> (a, b)
makeName (a
"_", b
t) = (a
"x", b
t)
        makeName (a
x, b
t)   = (a
x, b
t)

    contextDimensions :: TCM Int
    contextDimensions :: TCM Int
contextDimensions = do
      let
        go :: a -> Telescope -> f a
go a
n Telescope
EmptyTel = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
n
        go a
n (ExtendTel Dom Type
dom Abs Telescope
abs) = do
          n' <- Type -> f Bool
forall (m :: * -> *). MonadTCM m => Type -> m Bool
isInterval (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom) f Bool -> (Bool -> a) -> f a
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
            Bool
True  -> a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
1
            Bool
False -> a
n
          underAbstraction dom abs $ go n'
      Int -> Telescope -> TCM Int
forall {f :: * -> *} {a}.
(MonadTCM f, Num a, MonadAddContext f) =>
a -> Telescope -> f a
go Int
0 (Telescope -> TCM Int) -> TCMT IO Telescope -> TCM Int
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope

    introData :: AllowAmbiguousNames -> I.Type -> TCM [String]
    introData :: AllowAmbiguousNames -> Type -> TCM [[Char]]
introData AllowAmbiguousNames
amb Type
t = do
      let tel :: Telescope
tel  = ListTel -> Telescope
telFromList [(ShortText, Type) -> Dom (ShortText, Type)
forall a t. a -> Dom' t a
defaultDom (ShortText
"_", Type
t)]
          pat :: [Arg (Named name DeBruijnPattern)]
pat  = [Named name DeBruijnPattern -> Arg (Named name DeBruijnPattern)
forall a. a -> Arg a
defaultArg (Named name DeBruijnPattern -> Arg (Named name DeBruijnPattern))
-> Named name DeBruijnPattern -> Arg (Named name DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> Named name DeBruijnPattern
forall a name. a -> Named name a
unnamed (DeBruijnPattern -> Named name DeBruijnPattern)
-> DeBruijnPattern -> Named name DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ ShortText -> Int -> DeBruijnPattern
forall a. DeBruijn a => ShortText -> Int -> a
deBruijnNamedVar ShortText
"c" Int
0]

      -- Gallais, 2023-08-24: #6787 we need to locally enable the K rule
      -- to figure out that refl is a valid constructor for refl ≡ refl,
      -- or for x ≡ x at neutral type.
      r <- Lens' TCEnv Bool
-> (Bool -> Bool)
-> TCMT IO (Either SplitError Covering)
-> TCMT IO (Either SplitError Covering)
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eSplitOnStrict (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (TCMT IO (Either SplitError Covering)
 -> TCMT IO (Either SplitError Covering))
-> TCMT IO (Either SplitError Covering)
-> TCMT IO (Either SplitError Covering)
forall a b. (a -> b) -> a -> b
$ Induction
-> Telescope
-> [NamedArg DeBruijnPattern]
-> TCMT IO (Either SplitError Covering)
splitLast Induction
CoInductive Telescope
tel [NamedArg DeBruijnPattern]
forall {name}. [Arg (Named name DeBruijnPattern)]
pat

      -- If --cubical then we often get ambiguity because the coverage
      -- checker says most path constructors could also fit the hole. In
      -- that case we compute the number of interval variables in the
      -- context and drop any clauses that have more IApply patterns (=
      -- constructors that have a higher dimensionality) than the
      -- context.
      dim <- contextDimensions
      let dimension SplitClause
cl = [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([NamedArg SplitPattern] -> [Int]
forall p. IApplyVars p => p -> [Int]
iApplyVars (SplitClause -> [NamedArg SplitPattern]
scPats SplitClause
cl)) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
dim

      case r of
        Left SplitError
err -> [[Char]] -> TCM [[Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Right Covering
cov ->
           (ConHead -> TCM [Char]) -> [ConHead] -> TCM [[Char]]
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 (AllowAmbiguousNames -> ConHead -> TCM [Char]
showUnambiguousConName AllowAmbiguousNames
amb) ([ConHead] -> TCM [[Char]]) -> [ConHead] -> TCM [[Char]]
forall a b. (a -> b) -> a -> b
$ (SplitClause -> [ConHead]) -> [SplitClause] -> [ConHead]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([NamedArg SplitPattern] -> [ConHead]
conName ([NamedArg SplitPattern] -> [ConHead])
-> (SplitClause -> [NamedArg SplitPattern])
-> SplitClause
-> [ConHead]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitClause -> [NamedArg SplitPattern]
scPats) ([SplitClause] -> [ConHead]) -> [SplitClause] -> [ConHead]
forall a b. (a -> b) -> a -> b
$ (SplitClause -> Bool) -> [SplitClause] -> [SplitClause]
forall a. (a -> Bool) -> [a] -> [a]
filter SplitClause -> Bool
dimension ([SplitClause] -> [SplitClause]) -> [SplitClause] -> [SplitClause]
forall a b. (a -> b) -> a -> b
$ Covering -> [SplitClause]
splitClauses Covering
cov

    introRec :: QName -> TCM [String]
    introRec :: QName -> TCM [[Char]]
introRec QName
d = do
      hfs <- QName -> TCMT IO [Dom Name]
forall (m :: * -> *).
(HasCallStack, HasConstInfo m, ReadTCState m,
 MonadError TCErr m) =>
QName -> m [Dom Name]
getRecordFieldNames QName
d
      fs <- ifM showImplicitArguments
            (return $ map unDom hfs)
            (return [ unDom a | a <- hfs, visible a ])
      let e = KwRange -> Range -> RecordAssignments -> Expr
C.Rec KwRange
forall a. Null a => a
empty Range
forall a. Range' a
noRange (RecordAssignments -> Expr) -> RecordAssignments -> Expr
forall a b. (a -> b) -> a -> b
$ [Name]
fs [Name] -> (Name -> RecordAssignment) -> RecordAssignments
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Name
f ->
            FieldAssignment' Expr -> RecordAssignment
forall a b. a -> Either a b
Left (FieldAssignment' Expr -> RecordAssignment)
-> FieldAssignment' Expr -> RecordAssignment
forall a b. (a -> b) -> a -> b
$ Name -> Expr -> FieldAssignment' Expr
forall a. Name -> a -> FieldAssignment' a
C.FieldAssignment Name
f (Expr -> FieldAssignment' Expr) -> Expr -> FieldAssignment' Expr
forall a b. (a -> b) -> a -> b
$ Range -> Maybe Int -> Expr
C.QuestionMark Range
forall a. Range' a
noRange Maybe Int
forall a. Maybe a
Nothing
      return [ prettyShow e ]
      -- Andreas, 2019-02-25, remark:
      -- prettyShow is ok here since we are just printing something like
      -- record { f1 = ? ; ... ; fn = ?}
      -- which does not involve any qualified names, and the fi are C.Name.

-- | Runs the given computation as if in an anonymous goal at the end
--   of the top-level module.
--
--   Sets up current module, scope, and context.
atTopLevel :: TCM a -> TCM a
atTopLevel :: forall a. TCM a -> TCM a
atTopLevel TCM a
m = TCM a -> TCM a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
  let err :: a
err = a
forall a. HasCallStack => a
__IMPOSSIBLE__
    -- Andreas, 2024-08-03: cannot trigger this error:
    -- let err = genericError "The file has not been loaded yet."
  TCMT IO (Maybe (Pair ModuleName TopLevelModuleName))
-> TCM a -> (Pair ModuleName TopLevelModuleName -> TCM a) -> TCM a
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
Strict.caseMaybeM (Getter TCState (Maybe (Pair ModuleName TopLevelModuleName))
-> TCMT IO (Maybe (Pair ModuleName TopLevelModuleName))
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Maybe (Pair ModuleName TopLevelModuleName)
 -> f (Maybe (Pair ModuleName TopLevelModuleName)))
-> TCState -> f TCState
Lens' TCState (Maybe (Pair ModuleName TopLevelModuleName))
Getter TCState (Maybe (Pair ModuleName TopLevelModuleName))
stCurrentModule) TCM a
forall {a}. a
err ((Pair ModuleName TopLevelModuleName -> TCM a) -> TCM a)
-> (Pair ModuleName TopLevelModuleName -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \(ModuleName
current :!: TopLevelModuleName
topCurrent) -> do
    TCMT IO (Maybe ModuleInfo)
-> TCM a -> (ModuleInfo -> TCM a) -> TCM a
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
topCurrent) TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__ ((ModuleInfo -> TCM a) -> TCM a) -> (ModuleInfo -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ ModuleInfo
mi -> do
      let scope :: ScopeInfo
scope = Interface -> ScopeInfo
iInsideScope (Interface -> ScopeInfo) -> Interface -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
mi
      tel <- ModuleName -> TCMT IO Telescope
forall (m :: * -> *). ReadTCState m => ModuleName -> m Telescope
lookupSection ModuleName
current
      -- Get the names of the local variables from @scope@
      -- and put them into the context.
      --
      -- Andreas, 2017-04-24, issue #2552:
      --
      -- Delete the let-bound ones, since they are not represented
      -- in the module telescope.
      --
      -- This is a temporary fix until a better solution is available,
      -- e.g., when the module telescope represents let-bound variables.
      --
      -- Unfortunately, referring to let-bound variables
      -- from the top level module telescope will for now result in a not-in-scope error.
      let names :: [A.Name]
          names = (LocalVar -> Name) -> [LocalVar] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map LocalVar -> Name
localVar ([LocalVar] -> [Name]) -> [LocalVar] -> [Name]
forall a b. (a -> b) -> a -> b
$ (LocalVar -> Bool) -> [LocalVar] -> [LocalVar]
forall a. (a -> Bool) -> [a] -> [a]
filter ((BindingSource
LetBound BindingSource -> BindingSource -> Bool
forall a. Eq a => a -> a -> Bool
/=) (BindingSource -> Bool)
-> (LocalVar -> BindingSource) -> LocalVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalVar -> BindingSource
localBindingSource)
                               ([LocalVar] -> [LocalVar]) -> [LocalVar] -> [LocalVar]
forall a b. (a -> b) -> a -> b
$ ((Name, LocalVar) -> LocalVar) -> [(Name, LocalVar)] -> [LocalVar]
forall a b. (a -> b) -> [a] -> [b]
map (Name, LocalVar) -> LocalVar
forall a b. (a, b) -> b
snd ([(Name, LocalVar)] -> [LocalVar])
-> [(Name, LocalVar)] -> [LocalVar]
forall a b. (a -> b) -> a -> b
$ [(Name, LocalVar)] -> [(Name, LocalVar)]
forall a. [a] -> [a]
reverse ([(Name, LocalVar)] -> [(Name, LocalVar)])
-> [(Name, LocalVar)] -> [(Name, LocalVar)]
forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope ScopeInfo
-> Getting [(Name, LocalVar)] ScopeInfo [(Name, LocalVar)]
-> [(Name, LocalVar)]
forall s a. s -> Getting a s a -> a
^. Getting [(Name, LocalVar)] ScopeInfo [(Name, LocalVar)]
Lens' ScopeInfo [(Name, LocalVar)]
scopeLocals
      -- Andreas, 2016-12-31, issue #2371
      -- The following is an unnecessary complication, as shadowed locals
      -- are not in scope anyway (they are ambiguous).
      -- -- Replace the shadowed names by fresh names (such that they do not shadow imports)
      -- let mnames :: [Maybe A.Name]
      --     mnames = map (notShadowedLocal . snd) $ reverse $ scopeLocals scope
      -- names <- mapM (maybe freshNoName_ return) mnames
      let types :: [Dom I.Type]
          types = (Dom (ShortText, Type) -> Dom Type) -> ListTel -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map ((ShortText, Type) -> Type
forall a b. (a, b) -> b
snd ((ShortText, Type) -> Type) -> Dom (ShortText, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (ListTel -> [Dom Type]) -> ListTel -> [Dom Type]
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ShortText, t)]
telToList Telescope
tel
          gamma :: ListTel' A.Name
          gamma = ListTel' Name -> Maybe (ListTel' Name) -> ListTel' Name
forall a. a -> Maybe a -> a
fromMaybe ListTel' Name
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (ListTel' Name) -> ListTel' Name)
-> Maybe (ListTel' Name) -> ListTel' Name
forall a b. (a -> b) -> a -> b
$
                    (Name -> Dom Type -> Dom' Term (Name, Type))
-> [Name] -> [Dom Type] -> Maybe (ListTel' Name)
forall a b c. (a -> b -> c) -> [a] -> [b] -> Maybe [c]
zipWithSameLen (\ Name
x Dom Type
dom -> (Name
x,) (Type -> (Name, Type)) -> Dom Type -> Dom' Term (Name, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
dom) [Name]
names [Dom Type]
types
      reportSDoc "interaction.top" 20 $ TP.vcat
        [ "BasicOps.atTopLevel"
        , "  names = " TP.<+> TP.sep (map prettyA   names)
        , "  types = " TP.<+> TP.sep (map prettyTCM types)
        ]
      M.withCurrentModule current $
        evalWithScope scope $ do
          -- András, 2025-08-30: building fresh scope from interface
          recomputeInverseScope
          addContext gamma $ do
            -- We're going inside the top-level module, so we have to set the
            -- checkpoints for it and all its submodules to the new checkpoint.
            cp <- viewTC eCurrentCheckpoint
            setAllModuleCheckpoints cp
            m

-- | Parse a name.
parseName :: Range -> String -> TCM C.QName
parseName :: Range -> [Char] -> TCMT IO QName
parseName Range
r [Char]
s = do
  e <- Range -> [Char] -> TCM Expr
parseExpr Range
r [Char]
s
  maybe (typeError $ ExpectedIdentifier e) return $ isQName e

-- | Check whether an expression is a (qualified) identifier.
isQName :: C.Expr -> Maybe C.QName
isQName :: Expr -> Maybe QName
isQName = \case
  C.Ident QName
x                    -> QName -> Maybe QName
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
  Expr
_ -> Maybe QName
forall a. Maybe a
Nothing

isName :: C.Expr -> Maybe C.Name
isName :: Expr -> Maybe Name
isName = Expr -> Maybe QName
isQName (Expr -> Maybe QName)
-> (QName -> Maybe Name) -> Expr -> Maybe Name
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
  C.QName Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
  QName
_ -> Maybe Name
forall a. Maybe a
Nothing

-- | Returns the contents of the given module or record.

moduleContents
  :: Rewrite
     -- ^ How should the types be presented?
  -> Range
     -- ^ The range of the next argument.
  -> String
     -- ^ The module name.
  -> TCM ([C.Name], I.Telescope, [(C.Name, I.Type)])
     -- ^ Module names,
     --   context extension needed to print types,
     --   names paired up with corresponding types.

moduleContents :: Rewrite
-> Range -> [Char] -> TCM ([Name], Telescope, [(Name, Type)])
moduleContents Rewrite
norm Range
rng [Char]
s = Call
-> TCM ([Name], Telescope, [(Name, Type)])
-> TCM ([Name], Telescope, [(Name, Type)])
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
ModuleContents (TCM ([Name], Telescope, [(Name, Type)])
 -> TCM ([Name], Telescope, [(Name, Type)]))
-> TCM ([Name], Telescope, [(Name, Type)])
-> TCM ([Name], Telescope, [(Name, Type)])
forall a b. (a -> b) -> a -> b
$ do
  if [Char] -> Bool
forall a. Null a => a -> Bool
null ([Char] -> [Char]
trim [Char]
s) then Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
getModuleContents Rewrite
norm Maybe QName
forall a. Maybe a
Nothing else do
  e <- Range -> [Char] -> TCM Expr
parseExpr Range
rng [Char]
s
  case isQName e of
    -- If the expression is not a single identifier, it is not a module name
    -- and treated as a record expression.
    Maybe QName
Nothing -> Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
getRecordContents Rewrite
norm Expr
e
    -- Otherwise, if it is not in scope as a module name, it is treated
    -- as a record name.
    Just QName
x  -> do
      ms :: [AbstractModule] <- QName -> ScopeInfo -> [AbstractModule]
forall a. InScope a => QName -> ScopeInfo -> [a]
scopeLookup QName
x (ScopeInfo -> [AbstractModule])
-> TCMT IO ScopeInfo -> TCMT IO [AbstractModule]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
      if null ms then getRecordContents norm e else getModuleContents norm $ Just x

-- | Returns the contents of the given record identifier.

getRecordContents
  :: Rewrite  -- ^ Amount of normalization in types.
  -> C.Expr   -- ^ Expression presumably of record type.
  -> TCM ([C.Name], I.Telescope, [(C.Name, I.Type)])
              -- ^ Module names,
              --   context extension,
              --   names paired up with corresponding types.
getRecordContents :: Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
getRecordContents Rewrite
norm Expr
ce = do
  (_, t) <- Expr -> TCM (Term, Type)
inferExpr (Expr -> TCM (Term, Type)) -> TCM Expr -> TCM (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> ScopeM (AbsOfCon Expr)
forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
toAbstract Expr
ce
  isRecordType t >>= \case
    Maybe (QName, Args, RecordData)
Nothing -> TypeError -> TCM ([Name], Telescope, [(Name, Type)])
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM ([Name], Telescope, [(Name, Type)]))
-> TypeError -> TCM ([Name], Telescope, [(Name, Type)])
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
t
    Just (QName
q, Args
vs, RecordData{ _recFields :: RecordData -> [Dom QName]
_recFields = [Dom QName]
fs, _recTel :: RecordData -> Telescope
_recTel = Telescope
rtel }) -> do
      let xs :: [Name]
xs   = (Dom QName -> Name) -> [Dom QName] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
nameConcrete (Name -> Name) -> (Dom QName -> Name) -> Dom QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName (QName -> Name) -> (Dom QName -> QName) -> Dom QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom QName -> QName
forall t e. Dom' t e -> e
unDom) [Dom QName]
fs
          tel :: Telescope
tel  = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
rtel Args
vs
          doms :: [Dom Type]
doms = Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel
      -- Andreas, 2019-04-10, issue #3687: use flattenTel
      -- to bring types into correct scope.
      [Char] -> Int -> TCMT IO (Doc Aspects) -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO (Doc Aspects) -> m ()
reportSDoc [Char]
"interaction.contents.record" Int
20 (TCMT IO (Doc Aspects) -> TCMT IO ())
-> TCMT IO (Doc Aspects) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m (Doc Aspects)) -> m (Doc Aspects)
TP.vcat
        [ TCMT IO (Doc Aspects)
"getRecordContents"
        , TCMT IO (Doc Aspects)
"  cxt  = " TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.<+> (Telescope -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Telescope -> m (Doc Aspects)
prettyTCM (Telescope -> TCMT IO (Doc Aspects))
-> TCMT IO Telescope -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). MonadTCEnv m => m Telescope
getContextTelescope)
        , TCMT IO (Doc Aspects)
"  tel  = " TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.<+> Telescope -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Telescope -> m (Doc Aspects)
prettyTCM Telescope
tel
        , TCMT IO (Doc Aspects)
"  doms = " TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.<+> [Dom Type] -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *).
MonadPretty m =>
[Dom Type] -> m (Doc Aspects)
prettyTCM [Dom Type]
doms
        , TCMT IO (Doc Aspects)
"  doms'= " TCMT IO (Doc Aspects)
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
Applicative m =>
m (Doc Aspects) -> m (Doc Aspects) -> m (Doc Aspects)
TP.<+> Telescope -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel ([Dom Type] -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *).
MonadPretty m =>
[Dom Type] -> m (Doc Aspects)
prettyTCM [Dom Type]
doms)
        ]
      ts <- (Dom Type -> TCM Type) -> [Dom Type] -> TCMT IO [Type]
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 (Rewrite -> Type -> TCM Type
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm (Type -> TCM Type) -> (Dom Type -> Type) -> Dom Type -> TCM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Type
forall t e. Dom' t e -> e
unDom) [Dom Type]
doms
      return ([], tel, zip xs ts)

-- | Returns the contents of the given module.

getModuleContents
  :: Rewrite
       -- ^ Amount of normalization in types.
  -> Maybe C.QName
       -- ^ Module name, @Nothing@ if top-level module.
  -> TCM ([C.Name], I.Telescope, [(C.Name, I.Type)])
       -- ^ Module names,
       --   context extension,
       --   names paired up with corresponding types.
getModuleContents :: Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
getModuleContents Rewrite
norm Maybe QName
mm = do
  modScope <- case Maybe QName
mm of
    Maybe QName
Nothing -> TCMT IO Scope
getCurrentScope
    Just QName
m  -> ModuleName -> TCMT IO Scope
getNamedScope (ModuleName -> TCMT IO Scope)
-> (AbstractModule -> ModuleName)
-> AbstractModule
-> TCMT IO Scope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractModule -> ModuleName
amodName (AbstractModule -> TCMT IO Scope)
-> TCMT IO AbstractModule -> TCMT IO Scope
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO AbstractModule
resolveModule QName
m
  let modules :: ThingsInScope AbstractModule
      modules = Scope -> ThingsInScope AbstractModule
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
      names :: ThingsInScope AbstractName
      names = Scope -> ThingsInScope AbstractName
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
      xns = [ (Name
x,AbstractName
n) | (Name
x, List1 AbstractName
ns) <- ThingsInScope AbstractName -> [(Name, List1 AbstractName)]
forall k a. Map k a -> [(k, a)]
Map.toList ThingsInScope AbstractName
names, AbstractName
n <- List1 AbstractName -> [Item (List1 AbstractName)]
forall l. IsList l => l -> [Item l]
List1.toList List1 AbstractName
ns ]
  types <- forMaybeM xns $ \(Name
x, AbstractName
n) -> do
    QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
(HasConstInfo m, HasCallStack) =>
QName -> m (Either SigError Definition)
getConstInfo' (AbstractName -> QName
anameName AbstractName
n) TCMT IO (Either SigError Definition)
-> (Either SigError Definition -> TCMT IO (Maybe (Name, Type)))
-> TCMT IO (Maybe (Name, Type))
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
      Right Definition
d -> do
        t <- Rewrite -> Type -> TCM Type
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm (Type -> TCM Type) -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Definition -> TCMT IO Definition
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
Definition -> m Definition
instantiateDef Definition
d)
        return $ Just (x, t)
      Left{} -> Maybe (Name, Type) -> TCMT IO (Maybe (Name, Type))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Name, Type)
forall a. Maybe a
Nothing
  return (Map.keys modules, EmptyTel, types)


whyInScope :: FilePath -> String -> TCM WhyInScopeData
whyInScope :: [Char] -> [Char] -> TCM WhyInScopeData
whyInScope [Char]
cwd [Char]
s = do
  x     <- Range -> [Char] -> TCMT IO QName
parseName Range
forall a. Range' a
noRange [Char]
s
  scope <- getScope
  return $ WhyInScopeData
    x
    cwd
    (lookup x $ map (first C.QName) $ scope ^. scopeLocals)
    (scopeLookup x scope)
    (scopeLookup x scope)