{-# LANGUAGE NondecreasingIndentation #-}

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

module Agda.Interaction.BasicOps where

import Prelude hiding (null)

import Control.Arrow          ( first )
import Control.Monad          ( (>=>), forM, guard )
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Identity

import qualified Data.Map as Map
import qualified Data.Map.Strict as MapS
import qualified Data.Set as Set
import qualified Data.List as List
import Data.Maybe
import Data.Monoid
import Data.Function (on)
import Data.Text (Text)
import qualified Data.Text as T

import Agda.Interaction.Base
import Agda.Interaction.Options
import Agda.Interaction.Response (Goals, ResponseContextEntry(..))

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

import Agda.TheTypeChecker
import Agda.TypeChecking.ReconstructParameters
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Errors ( getAllWarnings, stringTCErr, Verbalize(..) )
import Agda.TypeChecking.Monad as M hiding (MetaInfo)
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.MetaVars.Mention
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.With
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.Match ( SplitPattern )
import Agda.TypeChecking.Records
import Agda.TypeChecking.Irrelevance (wakeIrrelevantVars)
import Agda.TypeChecking.Pretty ( PrettyTCM, prettyTCM )
import Agda.TypeChecking.Pretty.Constraint (prettyRangeConstraint)
import Agda.TypeChecking.IApplyConfluence
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Names
import Agda.TypeChecking.Free
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.SizedTypes.Solve
import qualified Agda.TypeChecking.Pretty as TP
import Agda.TypeChecking.Warnings
  ( runPM, warning, WhichWarnings(..), classifyWarnings, isMetaTCWarning
  , WarningsAndNonFatalErrors, emptyWarningsAndNonFatalErrors )

import Agda.Termination.TermCheck (termMutual)

import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty as P
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.String

import Agda.Utils.Impossible
import qualified Agda.Utils.SmallSet as SmallSet
import Agda.TypeChecking.ProjectionLike (reduceProjectionLike)

-- | Parses an expression.

parseExpr :: Range -> String -> TCM C.Expr
parseExpr :: Range -> ArgName -> TCM Expr
parseExpr Range
rng ArgName
s = do
  (C.ExprWhere Expr
e WhereClause
wh, CohesionAttributes
coh) <-
    forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ forall a.
Parser a -> Position -> ArgName -> PM (a, CohesionAttributes)
parsePosString Parser ExprWhere
exprWhereParser Position
pos ArgName
s
  CohesionAttributes -> ScopeM ()
checkCohesionAttributes CohesionAttributes
coh
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null WhereClause
wh) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
    ArgName
"where clauses are not supported in holes"
  forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
  where pos :: Position
pos = forall a. a -> Maybe a -> a
fromMaybe (Maybe RangeFile -> Position
startPos forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ forall a. Range' a -> Maybe (Position' a)
rStart Range
rng

parseExprIn :: InteractionId -> Range -> String -> TCM Expr
parseExprIn :: InteractionId -> Range -> ArgName -> TCM Expr
parseExprIn InteractionId
ii Range
rng ArgName
s = do
    MetaId
mId <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
    forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange MetaId
mId Range
rng
    Closure Range
mi  <- MetaVariable -> Closure Range
getMetaInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mId
    Expr
e   <- Range -> ArgName -> TCM Expr
parseExpr Range
rng ArgName
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.
    forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
mi forall a b. (a -> b) -> a -> b
$
      forall c. ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c)
concreteToAbstract (forall a. Closure a -> ScopeInfo
clScope Closure Range
mi) Expr
e

-- 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
    MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
    let t :: Type
t = case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
              IsSort{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
              HasType MetaId
_ Comparison
_ Type
t -> Type
t
    forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.give" Int
20 forall a b. (a -> b) -> a -> b
$
      TCMT IO Doc
"give: meta type =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
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.
    Args
ctx <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
    Type
t' <- Type
t forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
ctx) forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) Args
ctx
    forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
CmpLeq Expr
e Type
t') forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.give" Int
20 forall a b. (a -> b) -> a -> b
$ do
        AbstractMode
a <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> AbstractMode
envAbstractMode
        forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.hsep
          [ forall (m :: * -> *). Applicative m => ArgName -> m Doc
TP.text (ArgName
"give(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show AbstractMode
a forall a. [a] -> [a] -> [a]
++ ArgName
"): instantiated meta type =")
          , forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
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.
      Term
v <- forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' (Maybe MutualId) TCEnv
eMutualBlock (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$
        Expr -> Type -> TCM Term
checkExpr Expr
e Type
t'
      case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of

        InstV{} -> forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((Relevance
Irrelevant forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC forall a. LensRelevance a => a -> Relevance
getRelevance) forall a b. (a -> b) -> a -> b
$ do
          Term
v' <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
mi forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
ctx
          forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.give" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.sep
            [ TCMT IO Doc
"meta was already set to value v' = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v'
            , TCMT IO Doc
"now comparing it to given value v = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
            , TCMT IO Doc
"in context " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
ctx)
            ]
          forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t' Term
v Term
v'

        MetaInstantiation
_ -> do -- updateMeta mi v
          forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"interaction.give" Int
20 ArgName
"give: meta unassigned, assigning..."
          Args
args <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
          forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
nowSolvingConstraints forall a b. (a -> b) -> a -> b
$ CompareDirection
-> MetaId -> Args -> Term -> CompareAs -> ScopeM ()
assign CompareDirection
DirEq MetaId
mi Args
args Term
v (Type -> CompareAs
AsTermsOf Type
t')

      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.give" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"give: meta variable updated!"
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (UseForce
force forall a. Eq a => a -> a -> Bool
== UseForce
WithForce) forall a b. (a -> b) -> a -> b
$ Maybe InteractionId -> ScopeM ()
redoChecks Maybe InteractionId
mii
      forall (m :: * -> *). MonadMetaSolver m => MetaId -> m ()
wakeupConstraints MetaId
mi
      DefaultToInfty -> ScopeM ()
solveSizeConstraints DefaultToInfty
DontDefaultToInfty
      Bool
cubical <- forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      -- don't double check with cubical, because it gets in the way too often.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
cubical Bool -> Bool -> Bool
|| UseForce
force forall a. Eq a => a -> a -> Bool
== UseForce
WithForce) forall a b. (a -> b) -> a -> b
$ do
        -- Double check.
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.give" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"give: double checking"
        Term
vfull <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
v
        forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Comparison -> Type -> m ()
checkInternal Term
vfull Comparison
CmpLeq Type
t'
      forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

-- | After a give, redo termination etc. checks for function which was complemented.
redoChecks :: Maybe InteractionId -> TCM ()
redoChecks :: Maybe InteractionId -> ScopeM ()
redoChecks Maybe InteractionId
Nothing = forall (m :: * -> *) a. Monad m => a -> m a
return ()
redoChecks (Just InteractionId
ii) = do
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"interaction.give" Int
20 forall a b. (a -> b) -> a -> b
$
    ArgName
"give: redoing termination check for function surrounding " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show InteractionId
ii
  InteractionPoint
ip <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
  case InteractionPoint -> IPClause
ipClause InteractionPoint
ip of
    IPClause
IPNoClause -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    IPClause{ipcQName :: IPClause -> QName
ipcQName = QName
f} -> do
      MutualId
mb <- QName -> TCM MutualId
mutualBlockOf QName
f
      Result
terErrs <- forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envMutualBlock :: Maybe MutualId
envMutualBlock = forall a. a -> Maybe a
Just MutualId
mb }) forall a b. (a -> b) -> a -> b
$ [QName] -> TCMT IO Result
termMutual []
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null Result
terErrs) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ Result -> Warning
TerminationIssue Result
terErrs
  -- TODO redo positivity check!

-- | Try to fill hole by expression.
--
--   Returns the given expression unchanged
--   (for convenient generalization to @'refine'@).
give
  :: UseForce       -- ^ Skip safety checks?
  -> InteractionId  -- ^ Hole.
  -> Maybe Range
  -> Expr           -- ^ The expression to give.
  -> TCM Expr       -- ^ If successful, the very expression is returned unchanged.
give :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give UseForce
force InteractionId
ii Maybe Range
mr Expr
e = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
  -- if Range is given, update the range of the interaction meta
  MetaId
mi  <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Range
mr forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange MetaId
mi
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.give" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"giving expression" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.give" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
TP.text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. ExprLike a => a -> a
deepUnscope Expr
e
  -- Try to give mi := e
  Term
_ <- forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ do
     forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck MetaId
mi RunMetaOccursCheck
DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.
     UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term
giveExpr UseForce
force (forall a. a -> Maybe a
Just InteractionId
ii) MetaId
mi Expr
e
    forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ case
      -- Turn PatternErr into proper error:
      PatternErr{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Failed to give" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
      TCErr
err -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
  forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> m ()
removeInteractionPoint InteractionId
ii
  forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

-- | Try to fill hole by elaborated expression.
elaborate_give
  :: Rewrite        -- ^ Normalise result?
  -> UseForce       -- ^ Skip safety checks?
  -> InteractionId  -- ^ Hole.
  -> Maybe Range
  -> Expr           -- ^ The expression to give.
  -> TCM Expr       -- ^ If successful, return the elaborated expression.
elaborate_give :: Rewrite
-> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
elaborate_give Rewrite
norm UseForce
force InteractionId
ii Maybe Range
mr Expr
e = forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ do
  -- if Range is given, update the range of the interaction meta
  MetaId
mi  <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Range
mr forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange MetaId
mi
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.give" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"giving expression" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.give" Int
50 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
TP.text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. ExprLike a => a -> a
deepUnscope Expr
e
  -- Try to give mi := e
  Term
v <- forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ do
     forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck MetaId
mi RunMetaOccursCheck
DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.
     forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eCurrentlyElaborating (forall a b. a -> b -> a
const Bool
True) forall a b. (a -> b) -> a -> b
$
       UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term
giveExpr UseForce
force (forall a. a -> Maybe a
Just InteractionId
ii) MetaId
mi Expr
e
    forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ case
      -- Turn PatternErr into proper error:
      PatternErr{} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Failed to give" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
      TCErr
err -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
  MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
  -- Reduce projection-likes before quoting, otherwise instance
  -- selection may fail on reload (see #6203).
  Term
nv <- forall (m :: * -> *). PureTCM m => Term -> m Term
reduceProjectionLike forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Term
v
  forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
ePrintMetasBare (forall a b. a -> b -> a
const Bool
True) forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
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.
  -> Maybe Range
  -> Expr           -- ^ The expression to refine the hole with.
  -> TCM Expr       -- ^ The successfully given expression.
refine :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
refine UseForce
force InteractionId
ii Maybe Range
mr Expr
e = do
  MetaId
mi <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
  let range :: Range
range = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasRange a => a -> Range
getRange MetaVariable
mv) Maybe Range
mr
      scope :: ScopeInfo
scope = MetaVariable -> ScopeInfo
M.getMetaScope MetaVariable
mv
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.refine" Int
10 forall a b. (a -> b) -> a -> b
$
    TCMT IO Doc
"refining with expression" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
  forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.refine" Int
50 forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *). Applicative m => ArgName -> m Doc
TP.text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall a. ExprLike a => a -> a
deepUnscope Expr
e
  -- We try to append up to 10 meta variables
  Int -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine Int
10 Range
range ScopeInfo
scope Expr
e
  where
    tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
    tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine Int
nrOfMetas Range
r ScopeInfo
scope = Int -> Maybe TCErr -> Expr -> TCM Expr
try Int
nrOfMetas 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 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> TCErr
stringTCErr forall a b. (a -> b) -> a -> b
$ case Maybe TCErr
err of
           Just (TypeError CallStack
_ TCState
_ Closure TypeError
cl) | UnequalTerms Comparison
_ I.Pi{} Term
_ CompareAs
_ <- forall a. Closure a -> a
clValue Closure TypeError
cl ->
             ArgName
"Cannot refine functions with 10 or more arguments"
           Maybe TCErr
_ ->
             ArgName
"Cannot refine"
        try Int
n Maybe TCErr
_ Expr
e = UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give UseForce
force InteractionId
ii (forall a. a -> Maybe a
Just Range
r) Expr
e forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> Int -> Maybe TCErr -> Expr -> TCM Expr
try (Int
n forall a. Num a => a -> a -> a
- Int
1) (forall a. a -> Maybe a
Just TCErr
err) 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
          let rng :: Range
rng = Range -> Range
rightMargin Range
r -- Andreas, 2013-05-01 conflate range to its right margin to ensure that appended metas are last in numbering.  This fixes issue 841.
          -- Make new interaction point
          InteractionId
ii <- forall (m :: * -> *).
MonadInteractionPoints m =>
Bool -> Range -> Maybe Int -> m InteractionId
registerInteractionPoint Bool
False Range
rng forall a. Maybe a
Nothing
          let info :: MetaInfo
info = Info.MetaInfo
                { metaRange :: Range
Info.metaRange = Range
rng
                , metaScope :: ScopeInfo
Info.metaScope = forall i o. Lens' i o -> LensSet i o
set Lens' PrecedenceStack ScopeInfo
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 = forall a. Maybe a
Nothing -- in order to print just as ?, not ?n
                , metaNameSuggestion :: ArgName
metaNameSuggestion = ArgName
""
                }
              metaVar :: Expr
metaVar = MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
info InteractionId
ii

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

              lamView :: Expr -> Maybe (Binder, Expr)
lamView (A.Lam ExprInfo
_ (DomainFree TacticAttr
_ NamedArg Binder
x) Expr
e) = forall a. a -> Maybe a
Just (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) =
                forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [NamedArg Binder]
xs {-then-} (forall a. a -> Maybe a
Just (forall a. NamedArg a -> a
namedArg NamedArg Binder
x, Expr
e)) {-else-} forall a b. (a -> b) -> a -> b
$ \ NonEmpty (NamedArg Binder)
xs ->
                  forall a. a -> Maybe a
Just (forall a. NamedArg a -> a
namedArg NamedArg Binder
x, ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (TypedBinding -> LamBinding
DomainFull 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
_ = forall a. Maybe a
Nothing

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

-- Andreas, 2017-12-16:
-- Ulf, your attempt to fix #737 introduced regression #2873.
-- Going through concrete syntax does some arbitrary disambiguation
-- of constructors, which subsequently makes refine fail.
-- I am not convinced of the printing-parsing shortcut to address problems.
-- (Unless you prove the roundtrip property.)
--
--           rescopeExpr scope $ smartApp (defaultAppInfo r) e $ defaultNamedArg metaVar
-- -- | Turn an abstract expression into concrete syntax and then back into
-- --   abstract. This ensures that context precedences are set correctly for
-- --   abstract expressions built by hand. Used by refine above.
-- rescopeExpr :: ScopeInfo -> Expr -> TCM Expr
-- rescopeExpr scope = withScope_ scope . (concreteToAbstract_ <=< runAbsToCon . preserveInteractionIds . toConcrete)

{-| Evaluate the given expression in the current environment -}
evalInCurrent :: ComputeMode -> Expr -> TCM Expr
evalInCurrent :: ComputeMode -> Expr -> TCM Expr
evalInCurrent ComputeMode
cmode Expr
e = do
  (Term
v, Type
_t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
  forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCM Term
compute Term
v
  where compute :: Term -> TCM Term
compute | ComputeMode
cmode forall a. Eq a => a -> a -> Bool
== ComputeMode
HeadCompute = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce
                | Bool
otherwise            = forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise


evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
evalInMeta InteractionId
ii ComputeMode
cmode Expr
e =
   do   MetaId
m <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
        Closure Range
mi <- MetaVariable -> Closure Range
getMetaInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
        forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
mi forall a b. (a -> b) -> a -> b
$
            ComputeMode -> Expr -> TCM Expr
evalInCurrent ComputeMode
cmode Expr
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         -> 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 -> 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   -> forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce        --        time we get to reification. Hence instantiate here.
  Rewrite
Simplified   -> forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify
  Rewrite
Normalised   -> forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise

-- | Modifier for the interactive computation command,
--   specifying the mode of computation and result display.
--
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
True
  -- UseShowInstance requires the result to be a string literal so respecting
  -- abstract can only ever break things.

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

showComputed :: ComputeMode -> Expr -> TCM Doc
showComputed :: ComputeMode -> Expr -> TCMT IO Doc
showComputed ComputeMode
UseShowInstance Expr
e =
  case Expr
e of
    A.Lit ExprInfo
_ (LitString Text
s) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (ArgName -> Doc
text forall a b. (a -> b) -> a -> b
$ Text -> ArgName
T.unpack Text
s)
    Expr
_                     -> (Doc
"Not a string:" Doc -> Doc -> Doc
$$) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
showComputed ComputeMode
_ Expr
e = forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
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 a b
o) = forall {a} {b}. OutputConstraint a b -> b
out OutputConstraint a b
o
  where
    out :: OutputConstraint 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]
_           -> 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
_              -> forall a. HasCallStack => a
__IMPOSSIBLE__   -- Should never be used on IsEmpty constraints
      SizeLtSat{}                -> forall a. HasCallStack => a
__IMPOSSIBLE__
      FindInstanceOF b
_ a
_ [(a, a, a)]
_        -> forall a. HasCallStack => a
__IMPOSSIBLE__
      PTSInstance b
i b
_            -> b
i
      PostponedCheckFunDef{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__
      DataSort QName
_ b
i               -> b
i
      CheckLock b
i b
_              -> b
i
      UsableAtMod Modality
_ b
i            -> 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) = forall (m :: * -> *) a b.
(MonadTCEnv m, ReadTCState m) =>
Closure a -> (a -> m b) -> m (Closure b)
withClosure Closure Constraint
cl forall a b. (a -> b) -> a -> b
$ \ Constraint
c ->
    forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm (forall a. HasRange a => a -> Range
getRange Constraint
c) (forall a. Set a -> [a]
Set.toList Set ProblemId
pids) Blocker
unblock forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Constraint
c

reifyElimToExpr :: MonadReify m => I.Elim -> m Expr
reifyElimToExpr :: forall (m :: * -> *). MonadReify m => Elim -> m Expr
reifyElimToExpr = \case
    I.IApply Term
_ Term
_ Term
v -> Text -> Arg Expr -> Expr
appl Text
"iapply" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ Term
v) -- TODO Andrea: endpoints?
    I.Apply Arg Term
v -> Text -> Arg Expr -> Expr
appl Text
"apply" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Arg Term
v
    I.Proj ProjOrigin
_o QName
f -> Text -> Arg Expr -> Expr
appl Text
"proj" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify ((forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
I.Def QName
f []) :: Arg Term)
  where
    appl :: Text -> Arg Expr -> Expr
    appl :: Text -> Arg Expr -> Expr
appl Text
s Arg Expr
v = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Literal -> Expr
A.Lit forall a. Null a => a
empty (Text -> Literal
LitString Text
s)) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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) = forall a b. Comparison -> a -> b -> b -> OutputConstraint a b
CmpInType Comparison
cmp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
    reify (ValueCmp Comparison
cmp CompareAs
AsSizes Term
u Term
v) = forall a b. Comparison -> a -> b -> b -> OutputConstraint a b
CmpInType Comparison
cmp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
    reify (ValueCmp Comparison
cmp CompareAs
AsTypes Term
u Term
v) = forall a b. Comparison -> b -> b -> OutputConstraint a b
CmpTypes Comparison
cmp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
    reify (ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v) = forall a b. Comparison -> a -> b -> b -> OutputConstraint a b
CmpInType Comparison
cmp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
ty) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Term -> Term
lam_o Term
u) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (Term -> Term
lam_o Term
v)
      where
        lam_o :: Term -> Term
lam_o = ArgInfo -> Abs Term -> Term
I.Lam (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ArgName -> a -> Abs a
NoAbs ArgName
"_"
        ty :: m Type
ty = forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
          NamesT m Term
p <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
p
          NamesT m Type
t <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Type
t
          forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
ArgName
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' ArgName
"o" NamesT m Term
p (\ NamesT m Term
o -> NamesT m Type
t)
    reify (ElimCmp [Polarity]
cmp [IsForced]
_ Type
t Term
v Elims
es1 Elims
es2) =
      forall a b. [Polarity] -> a -> [b] -> [b] -> OutputConstraint a b
CmpElim [Polarity]
cmp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). MonadReify m => Elim -> m Expr
reifyElimToExpr Elims
es1
                              forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). MonadReify m => Elim -> m Expr
reifyElimToExpr Elims
es2
    reify (LevelCmp Comparison
cmp Level
t Level
t')    = forall a b. Comparison -> b -> b -> OutputConstraint a b
CmpLevels Comparison
cmp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Level
t'
    reify (SortCmp Comparison
cmp Sort
s Sort
s')     = forall a b. Comparison -> b -> b -> OutputConstraint a b
CmpSorts Comparison
cmp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Sort
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Sort
s'
    reify (UnquoteTactic Term
tac Term
_ Type
goal) = do
        Expr
tac <- AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Expr
A.Unquote ExprInfo
exprNoRange) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> NamedArg a
defaultNamedArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
tac
        forall a b. b -> a -> OutputConstraint a b
OfType Expr
tac forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
goal
    reify (UnBlock MetaId
m) = do
        MetaInstantiation
mi <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
        Expr
m' <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (MetaId -> Elims -> Term
MetaV MetaId
m [])
        case MetaInstantiation
mi of
          BlockedConst Term
t -> do
            Expr
e  <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
t
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> a -> OutputConstraint a b
Assign Expr
m' Expr
e
          PostponedTypeCheckingProblem Closure TypeCheckingProblem
cl -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl forall a b. (a -> b) -> a -> b
$ \case
            CheckExpr Comparison
cmp Expr
e Type
a -> do
                Expr
a  <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
a
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> a -> a -> OutputConstraint a b
TypedAssign Expr
m' Expr
e Expr
a
            CheckLambda Comparison
cmp (Arg ArgInfo
ai (List1 (WithHiding Name)
xs, Maybe Type
mt)) Expr
body Type
target -> do
              Expr
domType <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Underscore a => a
underscore) forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Maybe Type
mt
              Expr
target  <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
target
              let mkN :: WithHiding Name -> NamedArg Binder
mkN (WithHiding Hiding
h Name
x) = forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h forall a b. (a -> b) -> a -> b
$ forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
x
                  bs :: TypedBinding
bs = Range -> NonEmpty (NamedArg Binder) -> Expr -> TypedBinding
mkTBind forall a. Range' a
noRange (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WithHiding Name -> NamedArg Binder
mkN List1 (WithHiding Name)
xs) Expr
domType
                  e :: Expr
e  = ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
Info.exprNoRange (TypedBinding -> LamBinding
DomainFull TypedBinding
bs) Expr
body
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> a -> a -> OutputConstraint a b
TypedAssign Expr
m' Expr
e Expr
target
            CheckArgs Comparison
_ ExpandHidden
_ Range
_ [NamedArg Expr]
args Type
t0 Type
t1 ArgsCheckState CheckedTarget -> TCM Term
_ -> do
              Expr
t0 <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
t0
              Expr
t1 <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
t1
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> [a] -> a -> a -> OutputConstraint a b
PostponedCheckArgs Expr
m' (forall a b. (a -> b) -> [a] -> [b]
map (forall name a. Named name a -> a
namedThing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [NamedArg Expr]
args) Expr
t0 Expr
t1
            CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
_ List1 QName
_ [NamedArg Expr]
_ Type
t Int
_ Term
_ Type
_ PrincipalArgTypeMetas
_ -> forall a b. b -> a -> a -> OutputConstraint a b
TypedAssign Expr
m' Expr
e forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
t
            DoQuoteTerm Comparison
cmp Term
v Type
t -> do
              Expr
tm <- AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Expr
A.QuoteTerm ExprInfo
exprNoRange) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> NamedArg a
defaultNamedArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
v
              forall a b. b -> a -> OutputConstraint a b
OfType Expr
tm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
t
          Open{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__
          OpenInstance{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__
          InstV{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    reify (FindInstance MetaId
m Maybe [Candidate]
mcands) = forall a b. b -> a -> [(a, a, a)] -> OutputConstraint a b
FindInstanceOF
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (MetaId -> Elims -> Term
MetaV MetaId
m [])
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Candidate]
mcands) (\ (Candidate CandidateKind
q Term
tm Type
ty Bool
_) -> do
            (,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
tm forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
tm forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
ty)
    reify (IsEmpty Range
r Type
a) = forall a b. a -> OutputConstraint a b
IsEmptyType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
a
    reify (CheckSizeLtSat Term
a) = forall a b. a -> OutputConstraint a b
SizeLtSat  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
a
    reify (CheckFunDef Delayed
d DefInfo
i QName
q [Clause]
cs TCErr
err) = do
      Expr
a <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. QName -> a -> TCErr -> OutputConstraint a b
PostponedCheckFunDef QName
q Expr
a TCErr
err
    reify (HasBiggerSort Sort
a) = forall a b. b -> a -> OutputConstraint a b
OfType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Sort
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall t. Sort' t -> Sort' t
UnivSort Sort
a)
    reify (HasPTSRule Dom Type
a Abs Sort
b) = do
      (Expr
a,(Name
x,Expr
b)) <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall t e. Dom' t e -> e
unDom Dom Type
a,Abs Sort
b)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> b -> OutputConstraint a b
PTSInstance Expr
a Expr
b
    reify (CheckDataSort QName
q Sort
s) = forall a b. QName -> b -> OutputConstraint a b
DataSort QName
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Sort
s
    reify (CheckLockedVars Term
t Type
_ Arg Term
lk Type
_) = forall a b. b -> b -> OutputConstraint a b
CheckLock forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (forall e. Arg e -> e
unArg Arg Term
lk)
    reify (CheckMetaInst MetaId
m) = do
      Type
t <- forall a. Judgement a -> Type
jMetaType forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
      forall a b. b -> a -> OutputConstraint a b
OfType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify (MetaId -> Elims -> Term
MetaV MetaId
m []) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
t
    reify (CheckType Type
t) = forall a b. b -> OutputConstraint a b
JustType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Type
t
    reify (UsableAtModality WhyCheckModality
_ Maybe Sort
_ Modality
mod Term
t) = forall a b. Modality -> b -> OutputConstraint a b
UsableAtMod Modality
mod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify Term
t

instance (Pretty a, Pretty b) => PrettyTCM (OutputForm a b) where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => OutputForm a b -> m Doc
prettyTCM (OutputForm Range
r [ProblemId]
pids Blocker
unblock OutputConstraint a b
c) =
    forall (m :: * -> *) (f :: * -> *).
(MonadPretty m, Foldable f, Null (f ProblemId)) =>
Range -> f ProblemId -> Blocker -> Doc -> m Doc
prettyRangeConstraint Range
r [ProblemId]
pids Blocker
unblock (forall a. Pretty a => a -> Doc
pretty OutputConstraint a b
c)

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

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

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

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

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


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

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

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

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

instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b) where
  type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)
  toConcrete :: OutputConstraint' a b
-> AbsToCon (ConOfAbs (OutputConstraint' a b))
toConcrete (OfType' b
e a
t) = forall a b. b -> a -> OutputConstraint' a b
OfType' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. ToConcrete a => Precedence -> a -> AbsToCon (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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify

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

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

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

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

getConstraints :: TCM [OutputForm C.Expr C.Expr]
getConstraints :: TCM [OutputForm Expr Expr]
getConstraints = (ProblemConstraint -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getConstraints' forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
True

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 Expr 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 -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getConstrs forall {m :: * -> *} {b}.
(InstantiateFull b, MonadReduce m) =>
b -> m b
instantiateBlockingFull (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
      = forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' Bool TCState
stInstantiateBlocking (forall a b. a -> b -> a
const Bool
True) forall a b. (a -> b) -> a -> b
$
          forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull b
p

    -- 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 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 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   -> forall a. Maybe a
Nothing
        LevelCmp Comparison
cmp Level
u Level
v           -> forall a. Maybe a
Nothing
        SortCmp Comparison
cmp Sort
a Sort
b            -> forall a. Maybe a
Nothing
        UnBlock{}                  -> forall a. Maybe a
Nothing
        FindInstance{}             -> forall a. Maybe a
Nothing
        IsEmpty Range
r Type
t                -> Term -> Maybe Elims
isMeta (forall t a. Type'' t a -> a
unEl Type
t)
        CheckSizeLtSat Term
t           -> Term -> Maybe Elims
isMeta Term
t
        CheckFunDef{}              -> forall a. Maybe a
Nothing
        HasBiggerSort Sort
a            -> forall a. Maybe a
Nothing
        HasPTSRule Dom Type
a Abs Sort
b             -> forall a. Maybe a
Nothing
        UnquoteTactic{}            -> forall a. Maybe a
Nothing
        CheckDataSort QName
_ Sort
s          -> Sort -> Maybe Elims
isMetaS Sort
s
        CheckMetaInst{}            -> forall a. Maybe a
Nothing
        CheckType Type
t                -> Term -> Maybe Elims
isMeta (forall t a. Type'' t a -> a
unEl Type
t)
        CheckLockedVars Term
t Type
_ Arg Term
_ Type
_    -> Term -> Maybe Elims
isMeta Term
t
        UsableAtModality WhyCheckModality
_ Maybe Sort
ms Modality
_ Term
t  -> forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Sort
ms (Term -> Maybe Elims
isMeta Term
t) forall a b. (a -> b) -> a -> b
$ \ Sort
s -> Sort -> Maybe Elims
isMetaS Sort
s forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Maybe Elims
isMeta Term
t

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

    isMetaS :: Sort -> Maybe Elims
isMetaS (MetaS MetaId
m' Elims
es_m)
      | MetaId
m forall a. Eq a => a -> a -> Bool
== MetaId
m' = forall a. a -> Maybe a
Just Elims
es_m
    isMetaS Sort
_  = forall a. Maybe a
Nothing

    getConstrs :: (ProblemConstraint -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getConstrs ProblemConstraint -> TCM ProblemConstraint
g ProblemConstraint -> Bool
f = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      Constraints
cs <- Constraints -> Constraints
stripConstraintPids forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ProblemConstraint -> TCM ProblemConstraint
g forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m Constraints
M.getAllConstraints)
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"constr.ment" Int
20 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"getConstraintsMentioning"
      forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Constraints
cs forall a b. (a -> b) -> a -> b
$ \(PConstr Set ProblemId
s Blocker
ub Closure Constraint
c) -> do
        Closure Constraint
c <- forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Closure Constraint
c
        case forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Constraint -> Maybe Elims
hasHeadMeta (forall a. Closure a -> a
clValue Closure Constraint
c) of
          Just Args
as_m -> do
            -- unifyElimsMeta tries to move the constraint into
            -- (an extension of) the context where @m@ comes from.
            forall a.
MetaId
-> Args
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCM a)
-> TCM a
unifyElimsMeta MetaId
m Args
as_m Closure Constraint
c forall a b. (a -> b) -> a -> b
$ \ [(Term, Term)]
eqs Constraint
c -> do
              forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
s Blocker
ub forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Constraint
c
          Maybe Args
_ -> do
            Closure (OutputForm Expr Expr)
cl <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall a b. (a -> b) -> a -> b
$ Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
s Blocker
ub Closure Constraint
c
            forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure (OutputForm Expr Expr)
cl forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_

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

-- | Converts an 'InteractionId' to a 'MetaId'.

interactionIdToMetaId :: ReadTCState m => InteractionId -> m MetaId
interactionIdToMetaId :: forall (m :: * -> *). ReadTCState m => InteractionId -> m MetaId
interactionIdToMetaId InteractionId
i = do
  ModuleNameHash
h <- forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash
  forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
    { metaId :: Word64
metaId     = forall a b. (Integral a, Num b) => a -> b
fromIntegral InteractionId
i
    , metaModule :: ModuleNameHash
metaModule = ModuleNameHash
h
    }

getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm C.Expr C.Expr]
getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getConstraints' ProblemConstraint -> TCM ProblemConstraint
g ProblemConstraint -> Bool
f = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
    Constraints
cs <- Constraints -> Constraints
stripConstraintPids forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ProblemConstraint -> TCM ProblemConstraint
g forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m Constraints
M.getAllConstraints)
    [OutputForm Expr Expr]
cs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Constraints
cs forall a b. (a -> b) -> a -> b
$ \ProblemConstraint
c -> do
            Closure (OutputForm Expr Expr)
cl <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify ProblemConstraint
c
            forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure (OutputForm Expr Expr)
cl forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_
    [OutputForm Expr Expr]
ss <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *} {a}.
(MonadTrace m, ToConcrete a, MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
(InteractionId, MetaId, a) -> m (OutputForm (ConOfAbs a) Expr)
toOutputForm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints Bool
True Rewrite
AsIs -- get all
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [OutputForm Expr Expr]
ss forall a. [a] -> [a] -> [a]
++ [OutputForm Expr Expr]
cs
  where
    toOutputForm :: (InteractionId, MetaId, a) -> m (OutputForm (ConOfAbs a) Expr)
toOutputForm (InteractionId
ii, MetaId
mi, a
e) = do
      Closure Range
mv <- MetaVariable -> Closure Range
getMetaInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
      forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
mv forall a b. (a -> b) -> a -> b
$ do
        MetaId
mi <- forall (m :: * -> *). ReadTCState m => InteractionId -> m MetaId
interactionIdToMetaId InteractionId
ii
        let m :: Expr
m = MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
emptyMetaInfo{ metaNumber :: Maybe MetaId
metaNumber = forall a. a -> Maybe a
Just MetaId
mi } InteractionId
ii
        forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ forall a b. (a -> b) -> a -> b
$ forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm forall a. Range' a
noRange [] Blocker
alwaysUnblock forall a b. (a -> b) -> a -> b
$ forall a b. b -> a -> OutputConstraint a b
Assign Expr
m a
e


getIPBoundary :: Rewrite -> InteractionId -> TCM [IPBoundary' C.Expr]
getIPBoundary :: Rewrite -> InteractionId -> TCM [IPBoundary' Expr]
getIPBoundary Rewrite
norm InteractionId
ii = do
      InteractionPoint
ip <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
      case InteractionPoint -> IPClause
ipClause InteractionPoint
ip of
        IPClause { ipcBoundary :: IPClause -> [Closure (IPBoundary' Term)]
ipcBoundary = [Closure (IPBoundary' Term)]
cs } -> do
          forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Closure (IPBoundary' Term)]
cs forall a b. (a -> b) -> a -> b
$ \ Closure (IPBoundary' Term)
cl -> forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure (IPBoundary' Term)
cl forall a b. (a -> b) -> a -> b
$ \ IPBoundary' Term
b ->
            forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm IPBoundary' Term
b
        IPClause
IPNoClause -> forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | 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
  [OutputConstraint Expr InteractionId]
visibleMetas <- Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas Rewrite
normVisible
  [OutputConstraint Expr NamedMeta]
hiddenMetas <- Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas Rewrite
normHidden
  forall (m :: * -> *) a. Monad m => a -> m a
return ([OutputConstraint Expr InteractionId]
visibleMetas, [OutputConstraint Expr NamedMeta]
hiddenMetas)

-- | Print open metas nicely.
showGoals :: Goals -> TCM String
showGoals :: Goals -> TCM ArgName
showGoals ([OutputConstraint Expr InteractionId]
ims, [OutputConstraint Expr NamedMeta]
hms) = do
  [Doc]
di <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [OutputConstraint Expr InteractionId]
ims forall a b. (a -> b) -> a -> b
$ \ OutputConstraint Expr InteractionId
i ->
    forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (forall a b. OutputForm a b -> b
outputFormId forall a b. (a -> b) -> a -> b
$ forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint Expr InteractionId
i) forall a b. (a -> b) -> a -> b
$
      forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr InteractionId
i
  Names
dh <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM OutputConstraint Expr NamedMeta -> TCM ArgName
showA' [OutputConstraint Expr NamedMeta]
hms
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Names -> ArgName
unlines forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> ArgName
show [Doc]
di forall a. [a] -> [a] -> [a]
++ Names
dh
  where
    showA' :: OutputConstraint A.Expr NamedMeta -> TCM String
    showA' :: OutputConstraint Expr NamedMeta -> TCM ArgName
showA' OutputConstraint Expr NamedMeta
m = do
      let i :: MetaId
i = NamedMeta -> MetaId
nmid forall a b. (a -> b) -> a -> b
$ forall a. OutputConstraint Expr a -> a
namedMetaOf OutputConstraint Expr NamedMeta
m
      Range
r <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
i
      Doc
d <- forall (m :: * -> *) a.
(HasCallStack, MonadDebug m, MonadTCEnv m, MonadTrace m,
 ReadTCState m) =>
MetaId -> m a -> m a
withMetaId MetaId
i (forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr NamedMeta
m)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show Doc
d forall a. [a] -> [a] -> [a]
++ ArgName
"  [ at " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow Range
r forall a. [a] -> [a] -> [a]
++ ArgName
" ]"

getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
getWarningsAndNonFatalErrors = do
  [TCWarning]
mws <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
  let notMetaWarnings :: [TCWarning]
notMetaWarnings = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Bool
isMetaTCWarning) [TCWarning]
mws
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case [TCWarning]
notMetaWarnings of
    ws :: [TCWarning]
ws@(TCWarning
_:[TCWarning]
_) -> [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings [TCWarning]
ws
    [TCWarning]
_ -> WarningsAndNonFatalErrors
emptyWarningsAndNonFatalErrors

-- | 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 -> TCM [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints Bool
all Rewrite
norm = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InteractionId, MetaId) -> TCM [(InteractionId, MetaId, Expr)]
solution forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas
  where
    solution :: (InteractionId, MetaId) -> TCM [(InteractionId, MetaId, Expr)]
solution (InteractionId
i, MetaId
m) = do
      MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
      forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) forall a b. (a -> b) -> a -> b
$ do
        Args
args  <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
        ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
        let sol :: Term -> TCM [(InteractionId, MetaId, Expr)]
sol Term
v = do
              -- Andreas, 2014-02-17 exclude metas solved by metas
              Term
v <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v
              let isMeta :: Bool
isMeta = case Term
v of MetaV{} -> Bool
True; Term
_ -> Bool
False
              if Bool
isMeta Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
all then forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
                Expr
e <- forall (m :: * -> *) a. (MonadTCEnv m, BlankVars a) => a -> m a
blankNotInScope forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Term
v
                forall (m :: * -> *) a. Monad m => a -> m a
return [(InteractionId
i, MetaId
m, ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
scope Expr
e)]
            unsol :: TCMT IO [a]
unsol = forall (m :: * -> *) a. Monad m => a -> m a
return []
        case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
          InstV{}                        -> Term -> TCM [(InteractionId, MetaId, Expr)]
sol (MetaId -> Elims -> Term
MetaV MetaId
m forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply Args
args)
          Open{}                         -> forall {a}. TCMT IO [a]
unsol
          OpenInstance{}                 -> forall {a}. TCMT IO [a]
unsol
          BlockedConst{}                 -> forall {a}. TCMT IO [a]
unsol
          PostponedTypeCheckingProblem{} -> 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 MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
        forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) forall a b. (a -> b) -> a -> b
$
          MetaVariable
-> Judgement MetaId -> TCM (OutputConstraint Expr NamedMeta)
rewriteJudg MetaVariable
mv (MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
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 Type
t) = do
      ArgName
ms <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m ArgName
getMetaNameSuggestion MetaId
i
      -- Andreas, 2019-03-17, issue #3638:
      -- Need to put meta type into correct context _before_ normalizing,
      -- otherwise rewrite rules in parametrized modules will not fire.
      Args
vs <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
      Type
t <- Type
t forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
`piApplyM` forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (forall a. Sized a => a -> Int
size Args
vs) forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) Args
vs
      Type
t <- forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Type
t
      let x :: NamedMeta
x = ArgName -> MetaId -> NamedMeta
NamedMeta ArgName
ms MetaId
i
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interactive.meta" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.vcat
        [ forall (m :: * -> *). Applicative m => ArgName -> m Doc
TP.text forall a b. (a -> b) -> a -> b
$ Names -> ArgName
unwords [ArgName
"permuting", forall a. Show a => a -> ArgName
show MetaId
i, ArgName
"with", forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv]
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.vcat
          [ TCMT IO Doc
"len  =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
TP.text (forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
vs)
          , TCMT IO Doc
"args =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs
          , TCMT IO Doc
"t    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
          , TCMT IO Doc
"x    =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
TP.pretty NamedMeta
x
          ]
        ]
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interactive.meta.scope" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => ArgName -> m Doc
TP.text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> ArgName
show forall a b. (a -> b) -> a -> b
$ MetaVariable -> ScopeInfo
getMetaScope MetaVariable
mv
      -- Andreas, 2016-01-19, issue #1783: need piApplyM instead of just piApply
      forall a b. b -> a -> OutputConstraint a b
OfType NamedMeta
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked Type
t
    rewriteJudg MetaVariable
mv (IsSort MetaId
i Type
t) = do
      ArgName
ms <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m ArgName
getMetaNameSuggestion MetaId
i
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> OutputConstraint a b
JustSort forall a b. (a -> b) -> a -> b
$ ArgName -> MetaId -> NamedMeta
NamedMeta ArgName
ms MetaId
i


typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta :: Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta Rewrite
norm InteractionId
ii = Rewrite
-> (InteractionId, MetaId)
-> TCM (OutputConstraint Expr InteractionId)
typeOfMeta' Rewrite
norm forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionId
ii,) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadFail 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 Expr InteractionId)
typeOfMeta' Rewrite
norm (InteractionId
ii, MetaId
mi) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\NamedMeta
_ -> InteractionId
ii) 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 Expr InteractionId]
typesOfVisibleMetas Rewrite
norm =
  forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Rewrite
-> (InteractionId, MetaId)
-> TCM (OutputConstraint Expr InteractionId)
typeOfMeta' Rewrite
norm) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas

typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas Rewrite
norm = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
  [MetaId]
is    <- forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
  Map MetaId MetaVariable
store <- forall k a. (k -> a -> Bool) -> Map k a -> Map k a
MapS.filterWithKey (forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
t a -> a -> MetaVariable -> Bool
implicit [MetaId]
is) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useR Lens' (Map MetaId MetaVariable) TCState
stOpenMetaStore
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI Rewrite
norm) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
MapS.keys Map MetaId MetaVariable
store
  where
  implicit :: t a -> a -> MetaVariable -> Bool
implicit t a
is a
x MetaVariable
m | 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{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      MetaInstantiation
M.Open    -> a
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t a
is
      MetaInstantiation
M.OpenInstance -> a
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t a
is  -- OR: True !?
      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 Expr)
metaHelperType :: Rewrite
-> InteractionId
-> Range
-> ArgName
-> TCM (OutputConstraint' Expr Expr)
metaHelperType Rewrite
norm InteractionId
ii Range
rng ArgName
s = case ArgName -> Names
words ArgName
s of
  []    -> forall {a}. TCMT IO a
failure
  ArgName
f : Names
_ -> forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ do
    ArgName -> ScopeM ()
ensureName ArgName
f
    A.Application Expr
h [NamedArg Expr]
args <- Expr -> AppView' Expr
A.appView forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
getBody forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ExprLike a => a -> a
deepUnscope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> Range -> ArgName -> TCM Expr
parseExprIn InteractionId
ii Range
rng (ArgName
"let " forall a. [a] -> [a] -> [a]
++ ArgName
f forall a. [a] -> [a] -> [a]
++ ArgName
" = _ in " forall a. [a] -> [a] -> [a]
++ ArgName
s)
    Name -> Bool
inCxt   <- forall a. Ord a => [a] -> a -> Bool
hasElem forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
    Args
cxtArgs <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
    Type
a0      <- (Type -> Args -> Type
`piApply` Args
cxtArgs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii)
    case forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Expr -> Maybe Name
isVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg Expr]
args forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ [Name]
xs -> [Name]
xs forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Name -> Bool
inCxt [Name]
xs) 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.
     Just [Name]
xs -> do
      let inXs :: Name -> Bool
inXs = forall a. Ord a => [a] -> a -> Bool
hasElem [Name]
xs
      let hideButXs :: ContextEntry -> ContextEntry
hideButXs ContextEntry
dom = forall a. LensHiding a => Hiding -> a -> a
setHiding (if Name -> Bool
inXs forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall t e. Dom' t e -> e
unDom ContextEntry
dom then Hiding
NotHidden else Hiding
Hidden) ContextEntry
dom
      Telescope
tel  <- ListTel -> Telescope
telFromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Name -> ArgName
nameToArgName) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> ContextEntry
hideButXs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext
      forall a b. b -> a -> OutputConstraint' a b
OfType' Expr
h forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        -- Andreas, 2019-10-11: I actually prefer pi-types over ->.
        forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envPrintDomainFreePi :: Bool
envPrintDomainFreePi = Bool
True }) forall a b. (a -> b) -> a -> b
$ forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> Type
telePiVisible Telescope
tel Type
a0

     -- If some arguments are not variables.
     Maybe [Name]
Nothing -> do
      Args
cxtArgs  <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
      -- cleanupType relies on with arguments being named 'w',
      -- so we'd better rename any actual 'w's to avoid confusion.
      Telescope
tel  <- forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *).
Applicative f =>
(ArgName -> f ArgName) -> Telescope -> f Telescope
onNamesTel forall {a} {m :: * -> *}. (Eq a, IsString a, Monad m) => a -> m a
unW forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      let a :: Type
a = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
Applicative m =>
(ArgName -> m ArgName) -> Type -> m Type
onNames forall {a} {m :: * -> *}. (Eq a, IsString a, Monad m) => a -> m a
unW forall a b. (a -> b) -> a -> b
$ Type
a0
      [Arg (Term, EqualityView)]
vtys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ NamedArg Expr
a -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall e. ArgInfo -> e -> Arg e
Arg (forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Expr
a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> EqualityView
OtherType) forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Term, Type)
inferExpr forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Expr
a) [NamedArg Expr]
args
      -- Remember the arity of a
      TelV Telescope
atel Type
_ <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
      let arity :: Int
arity = forall a. Sized a => a -> Int
size Telescope
atel
          (Telescope
delta1, Telescope
delta2, Permutation
_, Type
a', [Arg (Term, EqualityView)]
vtys') = Telescope
-> Type
-> [Arg (Term, EqualityView)]
-> (Telescope, Telescope, Permutation, Type,
    [Arg (Term, EqualityView)])
splitTelForWith Telescope
tel Type
a [Arg (Term, EqualityView)]
vtys
      Expr
a <- forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envPrintDomainFreePi :: Bool
envPrintDomainFreePi = Bool
True }) forall a b. (a -> b) -> a -> b
$ do
        forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> [NamedArg Expr] -> Type -> TCMT IO Type
cleanupType Int
arity [NamedArg Expr]
args forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope
-> [Arg (Term, EqualityView)]
-> Telescope
-> Type
-> [(Int, (Term, Term))]
-> TCM (Type, Int)
withFunctionType Telescope
delta1 [Arg (Term, EqualityView)]
vtys' Telescope
delta2 Type
a' []
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.helper" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.vcat forall a b. (a -> b) -> a -> b
$
        let extractOtherType :: EqualityView -> Type
extractOtherType = \case { OtherType Type
a -> Type
a; EqualityView
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__ } in
        let ([Term]
vs, [Type]
as)   = forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EqualityView -> Type
extractOtherType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg (Term, EqualityView)]
vtys in
        let ([Term]
vs', [Type]
as') = forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EqualityView -> Type
extractOtherType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg) [Arg (Term, EqualityView)]
vtys' in
        [ TCMT IO Doc
"generating helper function"
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"tel    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel)
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"a      = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
a
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs     = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"as     = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Type]
as
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"delta1 = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta1)
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"delta2 = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta2)
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"a'     = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta2 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a')
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"as'    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Type]
as')
        , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TP.nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs'    = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs')
        ]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> a -> OutputConstraint' a b
OfType' Expr
h Expr
a
  where
    failure :: TCMT IO a
failure = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ ArgName
"Expected an argument of the form f e1 e2 .. en"
    ensureName :: ArgName -> ScopeM ()
ensureName ArgName
f = do
      Expr
ce <- Range -> ArgName -> TCM Expr
parseExpr Range
rng ArgName
f
      forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Name
isName Expr
ce) (\ Name
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$ do
         forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"interaction.helper" Int
10 forall a b. (a -> b) -> a -> b
$ ArgName
"ce = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Expr
ce
         forall {a}. TCMT IO a
failure
    isVar :: A.Expr -> Maybe A.Name
    isVar :: Expr -> Maybe Name
isVar = \case
      A.Var Name
x -> forall a. a -> Maybe a
Just Name
x
      Expr
_ -> forall a. Maybe a
Nothing
    cleanupType :: Int -> [NamedArg Expr] -> Type -> TCMT IO Type
cleanupType Int
arity [NamedArg Expr]
args Type
t = do
      -- Get the arity of t
      TelV Telescope
ttel 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 :: Int
n = forall a. Sized a => a -> Int
size Telescope
ttel forall a. Num a => a -> a -> a
- Int
arity
      -- It cannot be negative, otherwise we would have performed a
      -- negative number of with-abstractions.
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n forall a. Ord a => a -> a -> Bool
>= Int
0) forall a. HasCallStack => a
__IMPOSSIBLE__
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall s a. State s a -> s -> a
evalState (Type -> StateT [NamedArg Expr] Identity Type
renameVars forall a b. (a -> b) -> a -> b
$ forall {a}. (Eq a, Num a) => a -> Type -> Type
stripUnused Int
n Type
t) [NamedArg Expr]
args

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

    -- Strip the non-dependent abstractions from the first n abstractions.
    stripUnused :: a -> Type -> Type
stripUnused a
n (El Sort
s Term
v) = forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ a -> Term -> Term
strip a
n Term
v
    strip :: a -> Term -> Term
strip a
0 = forall a. a -> a
id
    strip a
n = \case
      I.Pi Dom Type
a Abs Type
b -> case a -> Type -> Type
stripUnused (a
nforall a. Num a => a -> a -> a
-a
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b of
        Abs Type
b | forall a. Abs a -> ArgName
absName Abs Type
b forall a. Eq a => a -> a -> Bool
== ArgName
"w"   -> Dom Type -> Abs Type -> Term
I.Pi Dom Type
a Abs Type
b
        NoAbs ArgName
_ Type
b              -> forall t a. Type'' t a -> a
unEl Type
b
        Abs ArgName
s Type
b | Int
0 forall a. Free a => Int -> a -> Bool
`freeIn` Type
b -> Dom Type -> Abs Type -> Term
I.Pi (forall a. LensHiding a => a -> a
hide Dom Type
a) (forall a. ArgName -> a -> Abs a
Abs ArgName
s Type
b)
                | Bool
otherwise    -> forall a. Subst a => Impossible -> a -> a
strengthen HasCallStack => Impossible
impossible (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 -> StateT [NamedArg Expr] Identity Type
renameVars = forall (m :: * -> *).
Applicative m =>
(ArgName -> m ArgName) -> Type -> m Type
onNames ArgName -> StateT [NamedArg Expr] Identity ArgName
renameVar

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

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

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

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

    betterName :: StateT [NamedArg Expr] Identity ArgName
betterName = do
      [NamedArg Expr]
xs <- forall s (m :: * -> *). MonadState s m => m s
get
      case [NamedArg Expr]
xs of
        []         -> forall a. HasCallStack => a
__IMPOSSIBLE__
        NamedArg Expr
arg : [NamedArg Expr]
args -> do
          forall s (m :: * -> *). MonadState s m => s -> m ()
put [NamedArg Expr]
args
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if
            | Arg ArgInfo
_ (Named Maybe NamedName
_ (A.Var Name
x)) <- NamedArg Expr
arg -> forall a. Pretty a => a -> ArgName
prettyShow forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete Name
x
            | Just ArgName
x <- forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf NamedArg Expr
arg         -> ArgName -> ArgName
argNameToString ArgName
x
            | Bool
otherwise                        -> ArgName
"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 = forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ do
  Closure Range
info <- MetaVariable -> Closure Range
getMetaInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii)
  forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
info forall a b. (a -> b) -> a -> b
$ do
    -- List of local variables.
    [ContextEntry]
cxt <- forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext
    let localVars :: [ContextEntry]
localVars = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Subst a => Int -> a -> a
raise [Int
1..] [ContextEntry]
cxt
    -- List of let-bindings.
    [(Name, Open (Term, Dom Type))]
letVars <- forall k a. Map k a -> [(k, a)]
Map.toAscList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> LetBindings
envLetBindings
    -- Reify the types and filter out bindings without a name.
    forall a. [a] -> [a] -> [a]
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b.
Monad m =>
[a] -> (a -> m (Maybe b)) -> m [b]
forMaybeM (forall a. [a] -> [a]
reverse [ContextEntry]
localVars) ContextEntry -> TCM (Maybe ResponseContextEntry)
mkVar
         forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a b.
Monad m =>
[a] -> (a -> m (Maybe b)) -> m [b]
forMaybeM [(Name, Open (Term, Dom Type))]
letVars (Name, Open (Term, Dom Type)) -> TCM (Maybe ResponseContextEntry)
mkLet

  where
    mkVar :: ContextEntry -> TCM (Maybe ResponseContextEntry)
    mkVar :: ContextEntry -> TCM (Maybe ResponseContextEntry)
mkVar Dom{ domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = (Name
name, Type
t) } = do
      if ArgInfo -> Name -> Bool
shouldHide ArgInfo
ai Name
name then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        let n :: Name
n = Name -> Name
nameConcrete Name
name
        Name
x  <- forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ Name
name
        let s :: NameInScope
s = forall a. LensInScope a => a -> NameInScope
C.isInScope Name
x
        Expr
ty <- forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Type
t
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name
-> Name
-> Arg Expr
-> TacticAttr
-> NameInScope
-> ResponseContextEntry
ResponseContextEntry Name
n Name
x (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Expr
ty) forall a. Maybe a
Nothing NameInScope
s

    mkLet :: (Name, Open (Term, Dom I.Type)) -> TCM (Maybe ResponseContextEntry)
    mkLet :: (Name, Open (Term, Dom Type)) -> TCM (Maybe ResponseContextEntry)
mkLet (Name
name, Open (Term, Dom Type)
lb) = do
      (Term
tm, !Dom Type
dom) <- forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open (Term, Dom Type)
lb
      if ArgInfo -> Name -> Bool
shouldHide (forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) Name
name then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        let n :: Name
n = Name -> Name
nameConcrete Name
name
        Name
x  <- forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ Name
name
        let s :: NameInScope
s = forall a. LensInScope a => a -> NameInScope
C.isInScope Name
x
        Arg Expr
ty <- forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Dom Type
dom
        Expr
v  <- forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Term
tm
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name
-> Name
-> Arg Expr
-> TacticAttr
-> NameInScope
-> ResponseContextEntry
ResponseContextEntry Name
n Name
x Arg Expr
ty (forall a. a -> Maybe a
Just Expr
v) NameInScope
s

    shouldHide :: ArgInfo -> A.Name -> Bool
    shouldHide :: ArgInfo -> Name -> Bool
shouldHide ArgInfo
ai Name
n = Bool -> Bool
not (forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai) Bool -> Bool -> 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
--   We wake up irrelevant variables just in case the user want to
--   invoke that command in an irrelevant context.
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
norm Expr
e =
    do  (Term
_,Type
t) <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
wakeIrrelevantVars forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Term, Type)
inferExpr Expr
e
        Type
v <- forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Type
t
        forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked Type
v



typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
ii Rewrite
norm Expr
e =
   do   MetaId
m <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
        Closure Range
mi <- MetaVariable -> Closure Range
getMetaInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
        forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
mi forall a b. (a -> b) -> a -> b
$
            Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
norm Expr
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 Names
introTactic Bool
pmLambda InteractionId
ii = do
  MetaId
mi <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  MetaVariable
mv <- forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
  forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) forall a b. (a -> b) -> a -> b
$ case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
    HasType MetaId
_ Comparison
_ Type
t -> do
        Type
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
piApplyM Type
t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
        -- Andreas, 2013-03-05 Issue 810: skip hidden domains in introduction
        -- of constructor.
        TelV Telescope
tel' Type
t <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) forall a. LensHiding a => a -> Bool
notVisible Type
t
        -- if we cannot introduce a constructor, we try a lambda
        let fallback :: TCM Names
fallback = do
              Bool
cubical <- forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
              TelV Telescope
tel Type
_ <- (if Bool
cubical then forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath else forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView) Type
t
              forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.intro" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.sep
                [ TCMT IO Doc
"introTactic/fallback"
                , TCMT IO Doc
"tel' = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel'
                , TCMT IO Doc
"tel  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
                ]
              case (Telescope
tel', Telescope
tel) of
                (Telescope
EmptyTel, Telescope
EmptyTel) -> forall (m :: * -> *) a. Monad m => a -> m a
return []
                (Telescope, Telescope)
_ -> ListTel -> TCM Names
introFun (forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel' forall a. [a] -> [a] -> [a]
++ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel)

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

    showUnambiguousConName :: ConHead -> f ArgName
showUnambiguousConName ConHead
v =
       Doc -> ArgName
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> Doc
pretty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) c. MonadAbsToCon m => AbsToCon c -> m c
runAbsToCon (AllowAmbiguousNames -> QName -> AbsToCon QName
lookupQName AllowAmbiguousNames
AmbiguousNothing forall a b. (a -> b) -> a -> b
$ ConHead -> QName
I.conName ConHead
v)

    showTCM :: PrettyTCM a => a -> TCM String
    showTCM :: forall a. PrettyTCM a => a -> TCM ArgName
showTCM a
v = Doc -> ArgName
render forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
v

    introFun :: ListTel -> TCM [String]
    introFun :: ListTel -> TCM Names
introFun ListTel
tel = forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.intro" Int
10 forall a b. (a -> b) -> a -> b
$ do TCMT IO Doc
"introFun" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (ListTel -> Telescope
telFromList ListTel
tel)
        Bool
imp <- forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
        let okHiding0 :: Hiding -> Bool
okHiding0 Hiding
h = Bool
imp Bool -> Bool -> Bool
|| Hiding
h 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
allHidden   = Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Hiding -> Bool
okHiding0 [Hiding]
hs)
            okHiding :: Hiding -> Bool
okHiding    = if Bool
allHidden then forall a b. a -> b -> a
const Bool
True else Hiding -> Bool
okHiding0
        Names
vars <- -- setShowImplicitArguments (imp || allHidden) $
                (if Bool
allHidden then forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments else forall a. a -> a
id) forall a b. (a -> b) -> a -> b
$
                  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. PrettyTCM a => a -> TCM ArgName
showTCM [ forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i :: Arg Term
                               | (Hiding
h, Int
i) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Hiding]
hs forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> [a]
downFrom Int
n
                               , Hiding -> Bool
okHiding Hiding
h
                               ]
        if Bool
pmLambda
           then forall (m :: * -> *) a. Monad m => a -> m a
return [ Names -> ArgName
unwords forall a b. (a -> b) -> a -> b
$ [ArgName
"λ", ArgName
"{"] forall a. [a] -> [a] -> [a]
++ Names
vars forall a. [a] -> [a] -> [a]
++ [ArgName
"→", ArgName
"?", ArgName
"}"] ]
           else forall (m :: * -> *) a. Monad m => a -> m a
return [ Names -> ArgName
unwords forall a b. (a -> b) -> a -> b
$ [ArgName
"λ"]      forall a. [a] -> [a] -> [a]
++ Names
vars forall a. [a] -> [a] -> [a]
++ [ArgName
"→", ArgName
"?"] ]
      where
        n :: Int
n = forall a. Sized a => a -> Int
size ListTel
tel
        hs :: [Hiding]
hs   = forall a b. (a -> b) -> [a] -> [b]
map forall a. LensHiding a => a -> Hiding
getHiding ListTel
tel
        tel' :: Telescope
tel' = ListTel -> Telescope
telFromList [ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {a} {b}. (Eq a, IsString a) => (a, b) -> (a, b)
makeName Dom (ArgName, Type)
b | Dom (ArgName, 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)

    introData :: I.Type -> TCM [String]
    introData :: Type -> TCM Names
introData Type
t = do
      let tel :: Telescope
tel  = ListTel -> Telescope
telFromList [forall a. a -> Dom a
defaultDom (ArgName
"_", Type
t)]
          pat :: [Arg (Named name DeBruijnPattern)]
pat  = [forall a. a -> Arg a
defaultArg forall a b. (a -> b) -> a -> b
$ forall a name. a -> Named name a
unnamed forall a b. (a -> b) -> a -> b
$ forall a. DeBruijn a => ArgName -> Int -> a
debruijnNamedVar ArgName
"c" Int
0]
      Either SplitError Covering
r <- Induction
-> Telescope
-> [NamedArg DeBruijnPattern]
-> TCM (Either SplitError Covering)
splitLast Induction
CoInductive Telescope
tel forall {name}. [Arg (Named name DeBruijnPattern)]
pat
      case Either SplitError Covering
r of
        Left SplitError
err -> forall (m :: * -> *) a. Monad m => a -> m a
return []
        Right Covering
cov ->
           forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {f :: * -> *}.
(MonadFresh NameId f, MonadInteractionPoints f,
 MonadStConcreteNames f, PureTCM f, IsString (f Doc), Null (f Doc),
 Semigroup (f Doc)) =>
ConHead -> f ArgName
showUnambiguousConName forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([NamedArg SplitPattern] -> [ConHead]
conName forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitClause -> [NamedArg SplitPattern]
scPats) forall a b. (a -> b) -> a -> b
$ Covering -> [SplitClause]
splitClauses Covering
cov

    introRec :: QName -> TCM [String]
    introRec :: QName -> TCM Names
introRec QName
d = do
      [Dom Name]
hfs <- forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m [Dom Name]
getRecordFieldNames QName
d
      [Name]
fs <- forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
            (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t e. Dom' t e -> e
unDom [Dom Name]
hfs)
            (forall (m :: * -> *) a. Monad m => a -> m a
return [ forall t e. Dom' t e -> e
unDom Dom Name
a | Dom Name
a <- [Dom Name]
hfs, forall a. LensHiding a => a -> Bool
visible Dom Name
a ])
      let e :: Expr
e = Range -> RecordAssignments -> Expr
C.Rec forall a. Range' a
noRange forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Name]
fs forall a b. (a -> b) -> a -> b
$ \ Name
f ->
            forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. Name -> a -> FieldAssignment' a
C.FieldAssignment Name
f forall a b. (a -> b) -> a -> b
$ Range -> Maybe Int -> Expr
C.QuestionMark forall a. Range' a
noRange forall a. Maybe a
Nothing
      forall (m :: * -> *) a. Monad m => a -> m a
return [ forall a. Pretty a => a -> ArgName
prettyShow Expr
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 = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode forall a b. (a -> b) -> a -> b
$ do
  let err :: TCMT IO a
err = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError ArgName
"The file has not been loaded yet."
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Maybe (ModuleName, TopLevelModuleName)) TCState
stCurrentModule) forall {a}. TCMT IO a
err forall a b. (a -> b) -> a -> b
$ \(ModuleName
current, TopLevelModuleName
topCurrent) -> do
    forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
topCurrent) forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ \ ModuleInfo
mi -> do
      let scope :: ScopeInfo
scope = Interface -> ScopeInfo
iInsideScope forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
mi
      Telescope
tel <- forall (m :: * -> *).
(Functor 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 :: [Name]
names = forall a b. (a -> b) -> [a] -> [b]
map LocalVar -> Name
localVar forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter ((BindingSource
LetBound forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalVar -> BindingSource
localBindingSource)
                               forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope forall o i. o -> Lens' i o -> i
^. Lens' [(Name, LocalVar)] ScopeInfo
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 Type]
types = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel
          gamma :: ListTel' A.Name
          gamma :: [ContextEntry]
gamma = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$
                    forall a b c. (a -> b -> c) -> [a] -> [b] -> Maybe [c]
zipWith' (\ Name
x Dom Type
dom -> (Name
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
dom) [Name]
names [Dom Type]
types
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.top" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.vcat
        [ TCMT IO Doc
"BasicOps.atTopLevel"
        , TCMT IO Doc
"  names = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA   [Name]
names)
        , TCMT IO Doc
"  types = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.sep (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Dom Type]
types)
        ]
      forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
M.withCurrentModule ModuleName
current forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
withScope_ ScopeInfo
scope forall a b. (a -> b) -> a -> b
$
          forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext [ContextEntry]
gamma forall a b. (a -> b) -> a -> b
$ do
            -- We're going inside the top-level module, so we have to set the
            -- checkpoint for it and all its submodules to the new checkpoint.
            CheckpointId
cp <- forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' CheckpointId TCEnv
eCurrentCheckpoint
            Lens' (Map ModuleName CheckpointId) TCState
stModuleCheckpoints forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const CheckpointId
cp)
            TCM a
m

-- | Parse a name.
parseName :: Range -> String -> TCM C.QName
parseName :: Range -> ArgName -> TCM QName
parseName Range
r ArgName
s = do
  Expr
e <- Range -> ArgName -> TCM Expr
parseExpr Range
r ArgName
s
  let failure :: TCM QName
failure = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ ArgName
"Not an identifier: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show Expr
e forall a. [a] -> [a] -> [a]
++ ArgName
"."
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCM QName
failure forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Expr -> Maybe QName
isQName Expr
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                    -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
  Expr
_ -> forall a. Maybe a
Nothing

isName :: C.Expr -> Maybe C.Name
isName :: Expr -> Maybe Name
isName = Expr -> Maybe QName
isQName forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
  C.QName Name
x -> forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
  QName
_ -> 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 -> ArgName -> TCM ([Name], Telescope, [(Name, Type)])
moduleContents Rewrite
norm Range
rng ArgName
s = forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
ModuleContents forall a b. (a -> b) -> a -> b
$ do
  if forall a. Null a => a -> Bool
null (ArgName -> ArgName
trim ArgName
s) then Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
getModuleContents Rewrite
norm forall a. Maybe a
Nothing else do
  Expr
e <- Range -> ArgName -> TCM Expr
parseExpr Range
rng ArgName
s
  case Expr -> Maybe QName
isQName Expr
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
      [AbstractModule]
ms :: [AbstractModule] <- forall a. InScope a => QName -> ScopeInfo -> [a]
scopeLookup QName
x forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
      if forall a. Null a => a -> Bool
null [AbstractModule]
ms then Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
getRecordContents Rewrite
norm Expr
e else Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
getModuleContents Rewrite
norm forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
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
  Expr
e <- forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
toAbstract Expr
ce
  (Term
_, Type
t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
  let notRecordType :: TCMT IO (QName, Args, Defn)
notRecordType = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
t
  (QName
q, Args
vs, Defn
defn) <- forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM TCMT IO (QName, Args, Defn)
notRecordType forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, Args, Defn))
isRecordType Type
t
  case Defn
defn of
    Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs, recTel :: Defn -> Telescope
recTel = Telescope
rtel } -> do
      let xs :: [Name]
xs   = forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
nameConcrete forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom QName]
fs
          tel :: Telescope
tel  = forall t. Apply t => t -> Args -> t
apply Telescope
rtel Args
vs
          doms :: [Dom Type]
doms = 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.
      forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.contents.record" Int
20 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.vcat
        [ TCMT IO Doc
"getRecordContents"
        , TCMT IO Doc
"  cxt  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
        , TCMT IO Doc
"  tel  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
        , TCMT IO Doc
"  doms = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Dom Type]
doms
        , TCMT IO Doc
"  doms'= " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Dom Type]
doms)
        ]
      [Type]
ts <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom Type]
doms
      forall (m :: * -> *) a. Monad m => a -> m a
return ([], Telescope
tel, forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs [Type]
ts)
    Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | 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
  Scope
modScope <- case Maybe QName
mm of
    Maybe QName
Nothing -> TCMT IO Scope
getCurrentScope
    Just QName
m  -> ModuleName -> TCMT IO Scope
getNamedScope forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractModule -> ModuleName
amodName forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> ScopeM AbstractModule
resolveModule QName
m
  let modules :: ThingsInScope AbstractModule
      modules :: ThingsInScope AbstractModule
modules = forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
      names :: ThingsInScope AbstractName
      names :: ThingsInScope AbstractName
names = forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
      xns :: [(Name, AbstractName)]
xns = [ (Name
x,AbstractName
n) | (Name
x, [AbstractName]
ns) <- forall k a. Map k a -> [(k, a)]
Map.toList ThingsInScope AbstractName
names, AbstractName
n <- [AbstractName]
ns ]
  [(Name, Type)]
types <- forall (m :: * -> *) a b.
Monad m =>
[a] -> (a -> m (Maybe b)) -> m [b]
forMaybeM [(Name, AbstractName)]
xns forall a b. (a -> b) -> a -> b
$ \(Name
x, AbstractName
n) -> do
    forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' (AbstractName -> QName
anameName AbstractName
n) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Right Definition
d -> do
        Type
t <- forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Definition -> Type
defType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef Definition
d)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Name
x, Type
t)
      Left{} -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall k a. Map k a -> [k]
Map.keys ThingsInScope AbstractModule
modules, forall a. Tele a
EmptyTel, [(Name, Type)]
types)


whyInScope :: FilePath -> String -> TCM WhyInScopeData
whyInScope :: ArgName -> ArgName -> TCM WhyInScopeData
whyInScope ArgName
cwd ArgName
s = do
  QName
x     <- Range -> ArgName -> TCM QName
parseName forall a. Range' a
noRange ArgName
s
  ScopeInfo
scope <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName
-> ArgName
-> Maybe LocalVar
-> [AbstractName]
-> [AbstractModule]
-> WhyInScopeData
WhyInScopeData
    QName
x
    ArgName
cwd
    (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup QName
x forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Name -> QName
C.QName) forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope forall o i. o -> Lens' i o -> i
^. Lens' [(Name, LocalVar)] ScopeInfo
scopeLocals)
    (forall a. InScope a => QName -> ScopeInfo -> [a]
scopeLookup QName
x ScopeInfo
scope)
    (forall a. InScope a => QName -> ScopeInfo -> [a]
scopeLookup QName
x ScopeInfo
scope)