{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE NondecreasingIndentation #-}

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

module Agda.Interaction.BasicOps where

import Prelude hiding (null)

import Control.Arrow (first)
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Identity

import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.List as List
import Data.Maybe
import Data.Monoid
import Data.Function (on)

import Agda.Interaction.Base
import Agda.Interaction.Options
import {-# SOURCE #-} Agda.Interaction.Imports (MaybeWarnings'(..), getMaybeWarnings)
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.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Errors ( stringTCErr )
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.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.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Permutation
import Agda.Utils.Size

import Agda.Utils.Impossible

-- | Parses an expression.

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

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

giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM ()
-- When translator from internal to abstract is given, this function might return
-- the expression returned by the type checker.
giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCMT IO ()
giveExpr UseForce
force Maybe InteractionId
mii MetaId
mi Expr
e = do
    MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi
    -- In the context (incl. signature) of the meta variable,
    -- type check expression and assign meta
    Closure Range -> TCMT IO () -> TCMT IO ()
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
      let t :: Type
t = case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
                IsSort{}    -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__
                HasType MetaId
_ Comparison
_ Type
t -> Type
t
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.give" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TCM Doc
"give: meta type =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Type -> TCM Doc
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 <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
      Type
t' <- Type
t Type -> Args -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute (VerboseLevel -> Permutation -> Permutation
takeP (Args -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Args
ctx) (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) Args
ctx
      Call -> TCMT IO () -> TCMT IO ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
CmpLeq Expr
e Type
t') (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
        String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.give" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
          AbstractMode
a <- (TCEnv -> AbstractMode) -> TCMT IO AbstractMode
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> AbstractMode
envAbstractMode
          [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TP.hsep
            [ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TP.text (String
"give(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ AbstractMode -> String
forall a. Show a => a -> String
show AbstractMode
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"): instantiated meta type =")
            , Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t'
            ]
        Term
v <- Expr -> Type -> TCM Term
checkExpr Expr
e Type
t'
        case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of

          InstV [Arg String]
xs Term
v' -> TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((Relevance
Irrelevant Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
==) (Relevance -> Bool) -> TCMT IO Relevance -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Relevance) -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
            String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.give" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TP.sep
              [ TCM Doc
"meta was already set to value v' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v'
                TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> TCM Doc
" with free variables " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return ([Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Arg String -> Doc) -> [Arg String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg String -> Doc
forall a. Pretty a => a -> Doc
pretty [Arg String]
xs)
              , TCM Doc
"now comparing it to given value v = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
              , TCM Doc
"in context " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Args -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
ctx)
              ]
            -- The number of free variables should be at least the size of the context
            -- (Ideally, if we implemented contextual type theory, it should be the same.)
            Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Arg String] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Arg String]
xs VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
ctx) TCMT IO ()
forall a. HasCallStack => a
__IMPOSSIBLE__
            -- if there are more free variables than the context has
            -- we need to abstract over the additional ones (xs2)
            let ([Arg String]
_xs1, [Arg String]
xs2) = VerboseLevel -> [Arg String] -> ([Arg String], [Arg String])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt (Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
ctx) [Arg String]
xs
            Term
v' <- Term -> TCM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ (Arg String -> Term -> Term) -> Term -> [Arg String] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Arg String -> Term -> Term
mkLam Term
v' [Arg String]
xs2
            String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.give" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TP.sep
              [ TCM Doc
"in meta context, v' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v'
              ]
            Type -> Term -> Term -> TCMT IO ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t' Term
v Term
v'  -- Note: v' now lives in context of meta

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

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

-- | After a give, redo termination etc. checks for function which was complemented.
redoChecks :: Maybe InteractionId -> TCM ()
redoChecks :: Maybe InteractionId -> TCMT IO ()
redoChecks Maybe InteractionId
Nothing = () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
redoChecks (Just InteractionId
ii) = do
  String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"interaction.give" VerboseLevel
20 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    String
"give: redoing termination check for function surrounding " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
  InteractionPoint
ip <- InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
  case InteractionPoint -> IPClause
ipClause InteractionPoint
ip of
    IPClause
IPNoClause -> () -> TCMT IO ()
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 <- (TCEnv -> TCEnv) -> TCMT IO Result -> TCMT IO Result
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envMutualBlock :: Maybe MutualId
envMutualBlock = MutualId -> Maybe MutualId
forall a. a -> Maybe a
Just MutualId
mb }) (TCMT IO Result -> TCMT IO Result)
-> TCMT IO Result -> TCMT IO Result
forall a b. (a -> b) -> a -> b
$ [QName] -> TCMT IO Result
termMutual []
      Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Result -> Bool
forall a. Null a => a -> Bool
null Result
terErrs) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCMT IO ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
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 = TCM Expr -> TCM Expr
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ do
  -- if Range is given, update the range of the interaction meta
  MetaId
mi  <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  Maybe Range -> (Range -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Range
mr ((Range -> TCMT IO ()) -> TCMT IO ())
-> (Range -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ MetaId -> Range -> TCMT IO ()
forall (m :: * -> *). MonadMetaSolver m => MetaId -> Range -> m ()
updateMetaVarRange MetaId
mi
  String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.give" VerboseLevel
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"giving expression" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
  String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.give" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TP.text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Expr -> String
forall a. Show a => a -> String
show (Expr -> String) -> Expr -> String
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope Expr
e
  -- Try to give mi := e
  do MetaId -> RunMetaOccursCheck -> TCMT IO ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck MetaId
mi RunMetaOccursCheck
DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.
     UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCMT IO ()
giveExpr UseForce
force (InteractionId -> Maybe InteractionId
forall a. a -> Maybe a
Just InteractionId
ii) MetaId
mi Expr
e
    TCMT IO () -> (TCErr -> TCMT IO ()) -> TCMT IO ()
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ case
      -- Turn PatternErr into proper error:
      TCErr
PatternErr -> TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ())
-> (Doc -> TypeError) -> Doc -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
        InteractionId -> TCM Doc -> TCM Doc
forall a. InteractionId -> TCM a -> TCM a
withInteractionId InteractionId
ii (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Failed to give" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
      TCErr
err -> TCErr -> TCMT IO ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
  InteractionId -> TCMT IO ()
forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> m ()
removeInteractionPoint InteractionId
ii
  Expr -> TCM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e


-- | 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 <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi
  let range :: Range
range = Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe (MetaVariable -> Range
forall t. HasRange t => t -> Range
getRange MetaVariable
mv) Maybe Range
mr
      scope :: ScopeInfo
scope = MetaVariable -> ScopeInfo
M.getMetaScope MetaVariable
mv
  String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.refine" VerboseLevel
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    TCM Doc
"refining with expression" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e
  String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.refine" VerboseLevel
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TP.text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Expr -> String
forall a. Show a => a -> String
show (Expr -> String) -> Expr -> String
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope Expr
e
  -- We try to append up to 10 meta variables
  VerboseLevel -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine VerboseLevel
10 Range
range ScopeInfo
scope Expr
e
  where
    tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
    tryRefine :: VerboseLevel -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine VerboseLevel
nrOfMetas Range
r ScopeInfo
scope Expr
e = VerboseLevel -> Expr -> TCM Expr
try VerboseLevel
nrOfMetas Expr
e
      where
        try :: Int -> Expr -> TCM Expr
        try :: VerboseLevel -> Expr -> TCM Expr
try VerboseLevel
0 Expr
e = TCErr -> TCM Expr
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> TCM Expr) -> TCErr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ String -> TCErr
stringTCErr String
"Cannot refine"
        try VerboseLevel
n Expr
e = UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give UseForce
force InteractionId
ii (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) Expr
e TCM Expr -> (TCErr -> TCM Expr) -> TCM Expr
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` (\TCErr
_ -> VerboseLevel -> Expr -> TCM Expr
try (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1) (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM Expr
appMeta Expr
e)

        -- Apply A.Expr to a new meta
        appMeta :: Expr -> TCM Expr
        appMeta :: Expr -> TCM Expr
appMeta Expr
e = do
          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 <- Bool -> Range -> Maybe VerboseLevel -> TCMT IO InteractionId
forall (m :: * -> *).
MonadInteractionPoints m =>
Bool -> Range -> Maybe VerboseLevel -> m InteractionId
registerInteractionPoint Bool
False Range
rng Maybe VerboseLevel
forall a. Maybe a
Nothing
          let info :: MetaInfo
info = MetaInfo :: Range -> ScopeInfo -> Maybe MetaId -> String -> MetaInfo
Info.MetaInfo
                { metaRange :: Range
Info.metaRange = Range
rng
                , metaScope :: ScopeInfo
Info.metaScope = Lens' [Precedence] ScopeInfo -> LensSet [Precedence] ScopeInfo
forall i o. Lens' i o -> LensSet i o
set Lens' [Precedence] 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 = Maybe MetaId
forall a. Maybe a
Nothing -- in order to print just as ?, not ?n
                , metaNameSuggestion :: String
metaNameSuggestion = String
""
                }
              metaVar :: Expr
metaVar = MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
info InteractionId
ii

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

              lamView :: Expr -> Maybe (Binder, Expr)
lamView (A.Lam ExprInfo
_ (DomainFree TacticAttr
_ NamedArg Binder
x) Expr
e) = (Binder, Expr) -> Maybe (Binder, Expr)
forall a. a -> Maybe a
Just (NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x, Expr
e)
              lamView (A.Lam ExprInfo
i (DomainFull (TBind Range
r TacticAttr
t (NamedArg Binder
x : [NamedArg Binder]
xs) Expr
a)) Expr
e)
                | [NamedArg Binder] -> Bool
forall a. Null a => a -> Bool
null [NamedArg Binder]
xs   = (Binder, Expr) -> Maybe (Binder, Expr)
forall a. a -> Maybe a
Just (NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x, Expr
e)
                | Bool
otherwise = (Binder, Expr) -> Maybe (Binder, Expr)
forall a. a -> Maybe a
Just (NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x, ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (TypedBinding -> LamBinding
DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. (a -> b) -> a -> b
$ Range -> TacticAttr -> [NamedArg Binder] -> Expr -> TypedBinding
TBind Range
r TacticAttr
t [NamedArg Binder]
xs Expr
a) Expr
e)
              lamView Expr
_ = Maybe (Binder, Expr)
forall a. Maybe a
Nothing

              -- reduce beta-redexes where the argument is used at most once
              smartApp :: AppInfo -> Expr -> NamedArg Expr -> Expr
smartApp AppInfo
i Expr
e NamedArg Expr
arg =
                case ((Binder, Expr) -> (BindName, Expr))
-> Maybe (Binder, Expr) -> Maybe (BindName, Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Binder -> BindName) -> (Binder, Expr) -> (BindName, Expr)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Binder -> BindName
forall a. Binder' a -> a
A.binderName) (Expr -> Maybe (Binder, Expr)
lamView (Expr -> Maybe (Binder, Expr)) -> Expr -> Maybe (Binder, Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
unScope Expr
e) of
                  Just (A.BindName{unBind :: BindName -> Name
unBind = Name
x}, Expr
e) | Name -> Expr -> Integer
forall a a. (ExprLike a, Num a) => Name -> a -> a
count Name
x Expr
e Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2 -> (Expr -> Expr) -> Expr -> Expr
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
subX Expr
e
                    where subX :: Expr -> Expr
subX (A.Var Name
y) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg Expr
arg
                          subX Expr
e = Expr
e
                  Maybe (BindName, Expr)
_ -> AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
i Expr
e NamedArg Expr
arg
          Expr -> TCM Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> TCM Expr) -> Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ AppInfo -> Expr -> NamedArg Expr -> Expr
smartApp (Range -> AppInfo
defaultAppInfo Range
r) Expr
e (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> NamedArg Expr
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 :: Expr -> TCM Expr
evalInCurrent :: Expr -> TCM Expr
evalInCurrent Expr
e =
    do  (Term
v, Type
t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
        Term
v' <- {- etaContract =<< -} Term -> TCM Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v
        Term -> TCM Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
v'


evalInMeta :: InteractionId -> Expr -> TCM Expr
evalInMeta :: InteractionId -> Expr -> TCM Expr
evalInMeta InteractionId
ii Expr
e =
   do   MetaId
m <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
        Closure Range
mi <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> TCMT IO MetaVariable -> TCMT IO (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
        Closure Range -> TCM Expr -> TCM Expr
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo Closure Range
mi (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$
            Expr -> TCM Expr
evalInCurrent Expr
e

-- | Modifier for interactive commands,
--   specifying the amount of normalization in the output.
--
normalForm :: (Reduce t, Simplify t, Normalise t) => Rewrite -> t -> TCM t
normalForm :: Rewrite -> t -> TCM t
normalForm Rewrite
AsIs         t
t = t -> TCM t
forall (m :: * -> *) a. Monad m => a -> m a
return t
t
normalForm Rewrite
Instantiated t
t = t -> TCM t
forall (m :: * -> *) a. Monad m => a -> m a
return t
t   -- reify does instantiation
normalForm Rewrite
HeadNormal   t
t = {- etaContract =<< -} t -> TCM t
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce t
t
normalForm Rewrite
Simplified   t
t = {- etaContract =<< -} t -> TCM t
forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify t
t
normalForm Rewrite
Normalised   t
t = {- etaContract =<< -} t -> TCM t
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise t
t

-- | 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
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 -> String -> String
computeWrapInput ComputeMode
UseShowInstance String
s = String
"show (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
computeWrapInput ComputeMode
_               String
s = String
s

showComputed :: ComputeMode -> Expr -> TCM Doc
showComputed :: ComputeMode -> Expr -> TCM Doc
showComputed ComputeMode
UseShowInstance Expr
e =
  case Expr
e of
    A.Lit (LitString Range
_ String
s) -> Doc -> TCM Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
s)
    Expr
_                     -> (Doc
"Not a string:" Doc -> Doc -> Doc
$$) (Doc -> Doc) -> TCM Doc -> TCM Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
showComputed ComputeMode
_ Expr
e = Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, 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 :: OutputForm a b -> b
outputFormId (OutputForm Range
_ [ProblemId]
_ OutputConstraint a b
o) = OutputConstraint a b -> b
forall a p. OutputConstraint a p -> p
out OutputConstraint a b
o
  where
    out :: OutputConstraint a p -> p
out OutputConstraint a p
o = case OutputConstraint a p
o of
      OfType p
i a
_                 -> p
i
      CmpInType Comparison
_ a
_ p
i p
_          -> p
i
      CmpElim [Polarity]
_ a
_ (p
i:[p]
_) [p]
_        -> p
i
      CmpElim [Polarity]
_ a
_ [] [p]
_           -> p
forall a. HasCallStack => a
__IMPOSSIBLE__
      JustType p
i                 -> p
i
      CmpLevels Comparison
_ p
i p
_            -> p
i
      CmpTypes Comparison
_ p
i p
_             -> p
i
      CmpTeles Comparison
_ p
i p
_             -> p
i
      JustSort p
i                 -> p
i
      CmpSorts Comparison
_ p
i p
_             -> p
i
      Guard OutputConstraint a p
o ProblemId
_                  -> OutputConstraint a p -> p
out OutputConstraint a p
o
      Assign p
i a
_                 -> p
i
      TypedAssign p
i a
_ a
_          -> p
i
      PostponedCheckArgs p
i [a]
_ a
_ a
_ -> p
i
      IsEmptyType a
_              -> p
forall a. HasCallStack => a
__IMPOSSIBLE__   -- Should never be used on IsEmpty constraints
      SizeLtSat{}                -> p
forall a. HasCallStack => a
__IMPOSSIBLE__
      FindInstanceOF p
_ a
_ [(a, a)]
_        -> p
forall a. HasCallStack => a
__IMPOSSIBLE__
      PTSInstance p
i p
_            -> p
i
      PostponedCheckFunDef{}     -> p
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

instance Reify Constraint (OutputConstraint Expr Expr) where
    reify :: Constraint -> m (OutputConstraint Expr Expr)
reify (ValueCmp Comparison
cmp (AsTermsOf Type
t) Term
u Term
v) = Comparison -> Expr -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. Comparison -> a -> b -> b -> OutputConstraint a b
CmpInType Comparison
cmp (Expr -> Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
t m (Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
u m (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
v
    reify (ValueCmp Comparison
cmp CompareAs
AsSizes Term
u Term
v) = Comparison -> Expr -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. Comparison -> a -> b -> b -> OutputConstraint a b
CmpInType Comparison
cmp (Expr -> Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType) m (Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
u m (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
v
    reify (ValueCmp Comparison
cmp CompareAs
AsTypes Term
u Term
v) = Comparison -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. Comparison -> b -> b -> OutputConstraint a b
CmpTypes Comparison
cmp (Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
u m (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
v
    reify (ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v) = Comparison -> Expr -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. Comparison -> a -> b -> b -> OutputConstraint a b
CmpInType Comparison
cmp (Expr -> Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
ty) m (Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Term -> Term
lam_o Term
u) m (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Term -> Term
lam_o Term
v)
      where
        lam_o :: Term -> Term
lam_o = ArgInfo -> Abs Term -> Term
I.Lam (Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo) (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
NoAbs String
"_"
        ty :: m Type
ty = Names -> NamesT m Type -> m Type
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT m Type -> m Type) -> NamesT m Type -> m Type
forall a b. (a -> b) -> a -> b
$ do
          NamesT m Term
p <- Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) t a.
(MonadFail m, Subst t a) =>
a -> NamesT m (NamesT m a)
open Term
p
          NamesT m Type
t <- Type -> NamesT m (NamesT m Type)
forall (m :: * -> *) t a.
(MonadFail m, Subst t a) =>
a -> NamesT m (NamesT m a)
open Type
t
          String
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
String
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' String
"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) =
      [Polarity]
-> Expr -> [Expr] -> [Expr] -> OutputConstraint Expr Expr
forall a b. [Polarity] -> a -> [b] -> [b] -> OutputConstraint a b
CmpElim [Polarity]
cmp (Expr -> [Expr] -> [Expr] -> OutputConstraint Expr Expr)
-> m Expr -> m ([Expr] -> [Expr] -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
t m ([Expr] -> [Expr] -> OutputConstraint Expr Expr)
-> m [Expr] -> m ([Expr] -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Elim -> m Expr) -> Elims -> m [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Elim -> m Expr
forall (m :: * -> *). MonadReify m => Elim -> m Expr
reifyElimToExpr Elims
es1
                              m ([Expr] -> OutputConstraint Expr Expr)
-> m [Expr] -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Elim -> m Expr) -> Elims -> m [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Elim -> m Expr
forall (m :: * -> *). MonadReify m => Elim -> m Expr
reifyElimToExpr Elims
es2
    reify (LevelCmp Comparison
cmp Level
t Level
t')    = Comparison -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. Comparison -> b -> b -> OutputConstraint a b
CmpLevels Comparison
cmp (Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Level
t m (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Level -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Level
t'
    reify (TelCmp Type
a Type
b Comparison
cmp Telescope
t Telescope
t')  = Comparison -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. Comparison -> b -> b -> OutputConstraint a b
CmpTeles Comparison
cmp (Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Telescope -> Expr
ETel (Telescope -> Expr) -> m Telescope -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m Telescope
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Telescope
t) m (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Telescope -> Expr
ETel (Telescope -> Expr) -> m Telescope -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope -> m Telescope
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Telescope
t')
    reify (SortCmp Comparison
cmp Sort
s Sort
s')     = Comparison -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. Comparison -> b -> b -> OutputConstraint a b
CmpSorts Comparison
cmp (Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Sort
s m (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Sort
s'
    reify (Guarded Constraint
c ProblemId
pid) = do
        OutputConstraint Expr Expr
o  <- Constraint -> m (OutputConstraint Expr Expr)
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Constraint
c
        OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr))
-> OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall a b. (a -> b) -> a -> b
$ OutputConstraint Expr Expr
-> ProblemId -> OutputConstraint Expr Expr
forall a b.
OutputConstraint a b -> ProblemId -> OutputConstraint a b
Guard OutputConstraint Expr Expr
o ProblemId
pid
    reify (UnquoteTactic Maybe MetaId
_ Term
tac Term
_ Type
goal) = do
        Expr
tac <- AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Expr
A.Unquote ExprInfo
exprNoRange) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
tac
        Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> a -> OutputConstraint a b
OfType Expr
tac (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
goal
    reify (UnBlock MetaId
m) = do
        MetaInstantiation
mi <- MetaVariable -> MetaInstantiation
mvInstantiation (MetaVariable -> MetaInstantiation)
-> m MetaVariable -> m MetaInstantiation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
        Expr
m' <- Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (MetaId -> Elims -> Term
MetaV MetaId
m [])
        case MetaInstantiation
mi of
          BlockedConst Term
t -> do
            Expr
e  <- Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
t
            OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr))
-> OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> a -> OutputConstraint a b
Assign Expr
m' Expr
e
          PostponedTypeCheckingProblem Closure TypeCheckingProblem
cl TCMT IO Bool
_ -> Closure TypeCheckingProblem
-> (TypeCheckingProblem -> m (OutputConstraint Expr Expr))
-> m (OutputConstraint Expr Expr)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl ((TypeCheckingProblem -> m (OutputConstraint Expr Expr))
 -> m (OutputConstraint Expr Expr))
-> (TypeCheckingProblem -> m (OutputConstraint Expr Expr))
-> m (OutputConstraint Expr Expr)
forall a b. (a -> b) -> a -> b
$ \case
            CheckExpr Comparison
cmp Expr
e Type
a -> do
                Expr
a  <- Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
a
                OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr))
-> OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> a -> a -> OutputConstraint a b
TypedAssign Expr
m' Expr
e Expr
a
            CheckLambda Comparison
cmp (Arg ArgInfo
ai ([WithHiding Name]
xs, Maybe Type
mt)) Expr
body Type
target -> do
              Expr
domType <- m Expr -> (Type -> m Expr) -> Maybe Type -> m Expr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Expr -> m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall a. Underscore a => a
underscore) Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Maybe Type
mt
              Expr
target  <- Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
target
              let mkN :: WithHiding Name -> NamedArg Binder
mkN (WithHiding Hiding
h Name
x) = Hiding -> NamedArg Binder -> NamedArg Binder
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h (NamedArg Binder -> NamedArg Binder)
-> NamedArg Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Binder -> NamedArg Binder
forall a. a -> NamedArg a
defaultNamedArg (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
x
                  bs :: TypedBinding
bs = Range -> [NamedArg Binder] -> Expr -> TypedBinding
mkTBind Range
forall a. Range' a
noRange ((WithHiding Name -> NamedArg Binder)
-> [WithHiding Name] -> [NamedArg Binder]
forall a b. (a -> b) -> [a] -> [b]
map WithHiding Name -> NamedArg Binder
mkN [WithHiding Name]
xs) Expr
domType
                  e :: Expr
e  = ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
Info.exprNoRange (TypedBinding -> LamBinding
DomainFull TypedBinding
bs) Expr
body
              OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr))
-> OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> a -> a -> OutputConstraint a b
TypedAssign Expr
m' Expr
e Expr
target
            CheckArgs ExpandHidden
_ Range
_ [NamedArg Expr]
args Type
t0 Type
t1 [Maybe Range] -> Elims -> Type -> CheckedTarget -> TCM Term
_ -> do
              Expr
t0 <- Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
t0
              Expr
t1 <- Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
t1
              OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr))
-> OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr] -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> [a] -> a -> a -> OutputConstraint a b
PostponedCheckArgs Expr
m' ((NamedArg Expr -> Expr) -> [NamedArg Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Named NamedName Expr -> Expr
forall name a. Named name a -> a
namedThing (Named NamedName Expr -> Expr)
-> (NamedArg Expr -> Named NamedName Expr) -> NamedArg Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> Named NamedName Expr
forall e. Arg e -> e
unArg) [NamedArg Expr]
args) Expr
t0 Expr
t1
            CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
_ NonEmpty QName
_ [NamedArg Expr]
_ Type
t VerboseLevel
_ Term
_ Type
_ -> Expr -> Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> a -> a -> OutputConstraint a b
TypedAssign Expr
m' Expr
e (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
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) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
v
              Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> a -> OutputConstraint a b
OfType Expr
tm (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
t
          Open{}  -> m (OutputConstraint Expr Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
          OpenInstance{}  -> m (OutputConstraint Expr Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
          InstV{} -> m (OutputConstraint Expr Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
    reify (FindInstance MetaId
m Maybe MetaId
_b Maybe [Candidate]
mcands) = Expr -> Expr -> [(Expr, Expr)] -> OutputConstraint Expr Expr
forall a b. b -> a -> [(a, a)] -> OutputConstraint a b
FindInstanceOF
      (Expr -> Expr -> [(Expr, Expr)] -> OutputConstraint Expr Expr)
-> m Expr
-> m (Expr -> [(Expr, Expr)] -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Term -> m Expr) -> Term -> m Expr
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
m [])
      m (Expr -> [(Expr, Expr)] -> OutputConstraint Expr Expr)
-> m Expr -> m ([(Expr, Expr)] -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType MetaId
m)
      m ([(Expr, Expr)] -> OutputConstraint Expr Expr)
-> m [(Expr, Expr)] -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Candidate] -> (Candidate -> m (Expr, Expr)) -> m [(Expr, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Candidate] -> Maybe [Candidate] -> [Candidate]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Candidate]
mcands) ((Candidate -> m (Expr, Expr)) -> m [(Expr, Expr)])
-> (Candidate -> m (Expr, Expr)) -> m [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$ \ (Candidate Term
tm Type
ty Bool
_) -> do
            (,) (Expr -> Expr -> (Expr, Expr))
-> m Expr -> m (Expr -> (Expr, Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
tm m (Expr -> (Expr, Expr)) -> m Expr -> m (Expr, Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
ty)
    reify (IsEmpty Range
r Type
a) = Expr -> OutputConstraint Expr Expr
forall a b. a -> OutputConstraint a b
IsEmptyType (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
a
    reify (CheckSizeLtSat Term
a) = Expr -> OutputConstraint Expr Expr
forall a b. a -> OutputConstraint a b
SizeLtSat  (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Term
a
    reify (CheckFunDef Delayed
d DefInfo
i QName
q [Clause]
cs) = do
      Expr
a <- Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr))
-> OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall a b. (a -> b) -> a -> b
$ QName -> Expr -> OutputConstraint Expr Expr
forall a b. QName -> a -> OutputConstraint a b
PostponedCheckFunDef QName
q Expr
a
    reify (HasBiggerSort Sort
a) = Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> a -> OutputConstraint a b
OfType (Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Sort
a m (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort Sort
a)
    reify (HasPTSRule Dom Type
a Abs Sort
b) = do
      (Expr
a,(Name
x,Expr
b)) <- (Type, Abs Sort) -> m (Expr, (Name, Expr))
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a,Abs Sort
b)
      OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr))
-> OutputConstraint Expr Expr -> m (OutputConstraint Expr Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> b -> OutputConstraint a b
PTSInstance Expr
a Expr
b
    reify (CheckMetaInst MetaId
m) = do
      Type
t <- Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type)
-> (MetaVariable -> Judgement MetaId) -> MetaVariable -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement (MetaVariable -> Type) -> m MetaVariable -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
      Expr -> Expr -> OutputConstraint Expr Expr
forall a b. b -> a -> OutputConstraint a b
OfType (Expr -> Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (MetaId -> Elims -> Term
MetaV MetaId
m []) m (Expr -> OutputConstraint Expr Expr)
-> m Expr -> m (OutputConstraint Expr Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify Type
t


instance (Pretty a, Pretty b) => Pretty (OutputForm a b) where
  pretty :: OutputForm a b -> Doc
pretty (OutputForm Range
r [ProblemId]
pids OutputConstraint a b
c) = [Doc] -> Doc
sep [OutputConstraint a b -> Doc
forall a. Pretty a => a -> Doc
pretty OutputConstraint a b
c, VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Range -> Doc
forall a. Pretty a => a -> Doc
prange Range
r, VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [ProblemId] -> Doc
forall a. Pretty a => [a] -> Doc
prPids [ProblemId]
pids]
    where
      prPids :: [a] -> Doc
prPids []    = Doc
forall a. Null a => a
empty
      prPids [a
pid] = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"problem" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
pid
      prPids [a]
pids  = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"problems" Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
"," ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty [a]
pids)
      prange :: a -> Doc
prange a
r | String -> Bool
forall a. Null a => a -> Bool
null String
s = Doc
forall a. Null a => a
empty
               | Bool
otherwise = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
" [ at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ]"
        where s :: String
s = a -> String
forall a. Pretty a => a -> String
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           -> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e Doc -> a -> Doc
forall a. Pretty a => Doc -> a -> Doc
.: a
t
      JustType b
e           -> Doc
"Type" Doc -> Doc -> Doc
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e
      JustSort b
e           -> Doc
"Sort" Doc -> Doc -> Doc
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e
      CmpInType Comparison
cmp a
t b
e b
e' -> Comparison -> b -> b -> Doc
forall a a a. (Pretty a, Pretty a, Pretty a) => a -> a -> a -> Doc
pcmp Comparison
cmp b
e b
e' Doc -> a -> Doc
forall a. Pretty a => Doc -> a -> Doc
.: a
t
      CmpElim [Polarity]
cmp a
t [b]
e [b]
e'   -> [Polarity] -> [b] -> [b] -> Doc
forall a a a. (Pretty a, Pretty a, Pretty a) => a -> a -> a -> Doc
pcmp [Polarity]
cmp [b]
e [b]
e' Doc -> a -> Doc
forall a. Pretty a => Doc -> a -> Doc
.: a
t
      CmpTypes  Comparison
cmp b
t b
t'   -> Comparison -> b -> b -> Doc
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'   -> Comparison -> b -> b -> Doc
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'   -> Comparison -> b -> b -> Doc
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'    -> Comparison -> b -> b -> Doc
forall a a a. (Pretty a, Pretty a, Pretty a) => a -> a -> a -> Doc
pcmp Comparison
cmp b
s b
s'
      Guard OutputConstraint a b
o ProblemId
pid          -> OutputConstraint a b -> Doc
forall a. Pretty a => a -> Doc
pretty OutputConstraint a b
o Doc -> Doc -> Doc
<?> Doc -> Doc
parens (Doc
"blocked by problem" Doc -> Doc -> Doc
<+> ProblemId -> Doc
forall a. Pretty a => a -> Doc
pretty ProblemId
pid)
      Assign b
m a
e           -> Doc -> Doc -> Doc -> Doc
bin (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
m) Doc
":=" (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e)
      TypedAssign b
m a
e a
a    -> Doc -> Doc -> Doc -> Doc
bin (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
m) Doc
":=" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc -> Doc -> Doc
bin (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e) Doc
":?" (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a)
      PostponedCheckArgs b
m [a]
es a
t0 a
t1 ->
        Doc -> Doc -> Doc -> Doc
bin (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
m) Doc
":=" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc -> Doc
parens (Doc
"_" Doc -> a -> Doc
forall a. Pretty a => Doc -> a -> Doc
.: a
t0) Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
paren (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Pretty a => a -> Doc
pretty) [a]
es)) Doc -> a -> Doc
forall a. Pretty a => Doc -> a -> Doc
.: a
t1
        where paren :: Doc -> Doc
paren Doc
d = Bool -> Doc -> Doc
mparens ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
' ', Char
'\n']) (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
d) Doc
d
      IsEmptyType a
a        -> Doc
"Is empty:" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
      SizeLtSat a
a          -> Doc
"Not empty type of sizes:" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
      FindInstanceOF b
s a
t [(a, a)]
cs -> [Doc] -> Doc
vcat
        [ Doc
"Resolve instance argument" Doc -> Doc -> Doc
<?> (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
s Doc -> a -> Doc
forall a. Pretty a => Doc -> a -> Doc
.: a
t)
        , VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Candidate:"
        , VerboseLevel -> Doc -> Doc
nest VerboseLevel
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
v Doc -> a -> Doc
forall a. Pretty a => Doc -> a -> Doc
.: a
t | (a
v, a
t) <- [(a, a)]
cs ] ]
      PTSInstance b
a b
b      -> Doc
"PTS instance for" Doc -> Doc -> Doc
<+> (b, b) -> Doc
forall a. Pretty a => a -> Doc
pretty (b
a, b
b)
      PostponedCheckFunDef QName
q a
a -> Doc
"Check definition of" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
    where
      bin :: Doc -> Doc -> Doc -> Doc
bin Doc
a Doc
op Doc
b = [Doc] -> Doc
sep [Doc
a, VerboseLevel -> Doc -> Doc
nest VerboseLevel
2 (Doc -> Doc) -> Doc -> Doc
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 (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a) (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
cmp) (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
b)
      Doc
val .: :: Doc -> a -> Doc
.: a
ty = Doc -> Doc -> Doc -> Doc
bin Doc
val Doc
":" (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
ty)


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

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

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

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

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

instance ToConcrete a c => ToConcrete (IPBoundary' a) (IPBoundary' c) where
  toConcrete :: IPBoundary' a -> AbsToCon (IPBoundary' c)
toConcrete = (a -> AbsToCon c) -> IPBoundary' a -> AbsToCon (IPBoundary' c)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Precedence -> a -> AbsToCon c
forall a c. ToConcrete a c => Precedence -> a -> AbsToCon c
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 = ((c, c) -> Doc) -> [(c, c)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (c
l,c
r) -> c -> Doc
forall a. Pretty a => a -> Doc
pretty c
l Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+> c -> 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
<+> c -> Doc
forall a. Pretty a => a -> Doc
pretty c
meta
              Overapplied
NotOverapplied -> Doc
forall a. Monoid a => a
mempty
    [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
prettyList_ [Doc]
xs Doc -> Doc -> Doc
<+> Doc
"⊢" Doc -> Doc -> Doc
<+> c -> 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
  [Closure Constraint]
-> (Closure Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Closure Constraint]
cs ((Closure Constraint -> TCMT IO (OutputForm Expr Expr))
 -> TCM [OutputForm Expr Expr])
-> (Closure Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ \ Closure Constraint
c -> do
            Closure (OutputForm Expr Expr)
cl <- ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr))
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Set ProblemId -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
forall a. Set a
Set.empty Closure Constraint
c)
            Closure (OutputForm Expr Expr)
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure (OutputForm Expr Expr)
cl OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr)
forall a c (m :: * -> *).
(ToConcrete a c, MonadAbsToCon m) =>
a -> m c
abstractToConcrete_

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

namedMetaOf :: OutputConstraint A.Expr a -> a
namedMetaOf :: 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
_ = 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]
forall (tcm :: * -> *).
MonadTCM tcm =>
(ProblemConstraint -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> tcm [OutputForm Expr Expr]
getConstrs ProblemConstraint -> TCM ProblemConstraint
forall (m :: * -> *) b.
(InstantiateFull b, MonadReduce m) =>
b -> m b
instantiateBlockingFull (MetaId -> ProblemConstraint -> Bool
forall t. MentionsMeta t => MetaId -> t -> Bool
mentionsMeta MetaId
m)
  -- could be optimized by not doing a full instantiation up front, with a more clever mentionsMeta.
  where
    instantiateBlockingFull :: b -> m b
instantiateBlockingFull b
p
      = Lens' Bool TCState -> (Bool -> Bool) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' a TCState -> (a -> a) -> m b -> m b
locallyTCState Lens' Bool TCState
stInstantiateBlocking (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$
          b -> m b
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull b
p

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

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

    getConstrs :: (ProblemConstraint -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> tcm [OutputForm Expr Expr]
getConstrs ProblemConstraint -> TCM ProblemConstraint
g ProblemConstraint -> Bool
f = TCM [OutputForm Expr Expr] -> tcm [OutputForm Expr Expr]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [OutputForm Expr Expr] -> tcm [OutputForm Expr Expr])
-> TCM [OutputForm Expr Expr] -> tcm [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ do
      Constraints
cs <- Constraints -> Constraints
stripConstraintPids (Constraints -> Constraints)
-> (Constraints -> Constraints) -> Constraints -> Constraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Bool) -> Constraints -> Constraints
forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
f (Constraints -> Constraints)
-> TCMT IO Constraints -> TCMT IO Constraints
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ProblemConstraint -> TCM ProblemConstraint)
-> Constraints -> TCMT IO Constraints
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ProblemConstraint -> TCM ProblemConstraint
g (Constraints -> TCMT IO Constraints)
-> TCMT IO Constraints -> TCMT IO Constraints
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
M.getAllConstraints)
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"constr.ment" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"getConstraintsMentioning"
      Constraints
-> (ProblemConstraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Constraints
cs ((ProblemConstraint -> TCMT IO (OutputForm Expr Expr))
 -> TCM [OutputForm Expr Expr])
-> (ProblemConstraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ \(PConstr Set ProblemId
s Closure Constraint
c) -> do
        Closure Constraint
c <- Rewrite -> Closure Constraint -> TCM (Closure Constraint)
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Closure Constraint
c
        case Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims (Elims -> Maybe Args) -> Maybe Elims -> Maybe Args
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Constraint -> Maybe Elims
hasHeadMeta (Closure Constraint -> Constraint
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.
            MetaId
-> Args
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall a.
MetaId
-> Args
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCM a)
-> TCM a
unifyElimsMeta MetaId
m Args
as_m Closure Constraint
c (([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
 -> TCMT IO (OutputForm Expr Expr))
-> ([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall a b. (a -> b) -> a -> b
$ \ [(Term, Term)]
eqs Constraint
c -> do
              (Closure (OutputForm Expr Expr)
 -> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
 -> TCMT IO (OutputForm Expr Expr))
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> Closure (OutputForm Expr Expr)
-> TCMT IO (OutputForm Expr Expr)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Closure (OutputForm Expr Expr)
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr)
forall a c (m :: * -> *).
(ToConcrete a c, MonadAbsToCon m) =>
a -> m c
abstractToConcrete_ (Closure (OutputForm Expr Expr) -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (Closure (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr))
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr)))
-> (Closure Constraint -> ProblemConstraint)
-> Closure Constraint
-> TCMT IO (Closure (OutputForm Expr Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ProblemId -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
s (Closure Constraint -> TCMT IO (Closure (OutputForm Expr Expr)))
-> TCM (Closure Constraint)
-> TCMT IO (Closure (OutputForm Expr Expr))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Constraint -> TCM (Closure Constraint)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Constraint
c
          Maybe Args
_ -> do
            Closure (OutputForm Expr Expr)
cl <- ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr))
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr)))
-> ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr))
forall a b. (a -> b) -> a -> b
$ Set ProblemId -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
s Closure Constraint
c
            Closure (OutputForm Expr Expr)
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure (OutputForm Expr Expr)
cl OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr)
forall a c (m :: * -> *).
(ToConcrete a c, MonadAbsToCon m) =>
a -> m c
abstractToConcrete_

-- Copied from Agda.TypeChecking.Pretty.Warning.prettyConstraints
stripConstraintPids :: Constraints -> Constraints
stripConstraintPids :: Constraints -> Constraints
stripConstraintPids Constraints
cs = (ProblemConstraint -> ProblemConstraint -> Ordering)
-> Constraints -> Constraints
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Bool -> Bool -> Ordering)
-> (ProblemConstraint -> Bool)
-> ProblemConstraint
-> ProblemConstraint
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ProblemConstraint -> Bool
isBlocked) (Constraints -> Constraints) -> Constraints -> Constraints
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> ProblemConstraint)
-> Constraints -> Constraints
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> ProblemConstraint
stripPids Constraints
cs
  where
    isBlocked :: ProblemConstraint -> Bool
isBlocked = Bool -> Bool
not (Bool -> Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ProblemId] -> Bool
forall a. Null a => a -> Bool
null ([ProblemId] -> Bool)
-> (ProblemConstraint -> [ProblemId]) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> [ProblemId]
blocking (Constraint -> [ProblemId])
-> (ProblemConstraint -> Constraint)
-> ProblemConstraint
-> [ProblemId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint
    interestingPids :: Set ProblemId
interestingPids = [ProblemId] -> Set ProblemId
forall a. Ord a => [a] -> Set a
Set.fromList ([ProblemId] -> Set ProblemId) -> [ProblemId] -> Set ProblemId
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> [ProblemId]) -> Constraints -> [ProblemId]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Constraint -> [ProblemId]
blocking (Constraint -> [ProblemId])
-> (ProblemConstraint -> Constraint)
-> ProblemConstraint
-> [ProblemId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (Closure Constraint -> Constraint)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> Constraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) Constraints
cs
    stripPids :: ProblemConstraint -> ProblemConstraint
stripPids (PConstr Set ProblemId
pids Closure Constraint
c) = Set ProblemId -> Closure Constraint -> ProblemConstraint
PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set ProblemId
pids Set ProblemId
interestingPids) Closure Constraint
c
    blocking :: Constraint -> [ProblemId]
blocking (Guarded Constraint
c ProblemId
pid) = ProblemId
pid ProblemId -> [ProblemId] -> [ProblemId]
forall a. a -> [a] -> [a]
: Constraint -> [ProblemId]
blocking Constraint
c
    blocking Constraint
_               = []

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 = TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr])
-> TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ do
    Constraints
cs <- Constraints -> Constraints
stripConstraintPids (Constraints -> Constraints)
-> (Constraints -> Constraints) -> Constraints -> Constraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Bool) -> Constraints -> Constraints
forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
f (Constraints -> Constraints)
-> TCMT IO Constraints -> TCMT IO Constraints
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ProblemConstraint -> TCM ProblemConstraint)
-> Constraints -> TCMT IO Constraints
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ProblemConstraint -> TCM ProblemConstraint
g (Constraints -> TCMT IO Constraints)
-> TCMT IO Constraints -> TCMT IO Constraints
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
M.getAllConstraints)
    [OutputForm Expr Expr]
cs <- Constraints
-> (ProblemConstraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Constraints
cs ((ProblemConstraint -> TCMT IO (OutputForm Expr Expr))
 -> TCM [OutputForm Expr Expr])
-> (ProblemConstraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ \ProblemConstraint
c -> do
            Closure (OutputForm Expr Expr)
cl <- ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr))
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify ProblemConstraint
c
            Closure (OutputForm Expr Expr)
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure (OutputForm Expr Expr)
cl OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr)
forall a c (m :: * -> *).
(ToConcrete a c, MonadAbsToCon m) =>
a -> m c
abstractToConcrete_
    [OutputForm Expr Expr]
ss <- ((InteractionId, MetaId, Expr) -> TCMT IO (OutputForm Expr Expr))
-> [(InteractionId, MetaId, Expr)] -> TCM [OutputForm Expr Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InteractionId, MetaId, Expr) -> TCMT IO (OutputForm Expr Expr)
forall a c.
ToConcrete a c =>
(InteractionId, MetaId, a) -> TCMT IO (OutputForm c Expr)
toOutputForm ([(InteractionId, MetaId, Expr)] -> TCM [OutputForm Expr Expr])
-> TCMT IO [(InteractionId, MetaId, Expr)]
-> TCM [OutputForm Expr Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Bool -> Rewrite -> TCMT IO [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints Bool
True Rewrite
AsIs -- get all
    [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall (m :: * -> *) a. Monad m => a -> m a
return ([OutputForm Expr Expr] -> TCM [OutputForm Expr Expr])
-> [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ [OutputForm Expr Expr]
ss [OutputForm Expr Expr]
-> [OutputForm Expr Expr] -> [OutputForm Expr Expr]
forall a. [a] -> [a] -> [a]
++ [OutputForm Expr Expr]
cs
  where
    toOutputForm :: (InteractionId, MetaId, a) -> TCMT IO (OutputForm c Expr)
toOutputForm (InteractionId
ii, MetaId
mi, a
e) = do
      Closure Range
mv <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> TCMT IO MetaVariable -> TCMT IO (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi
      Closure Range
-> TCMT IO (OutputForm c Expr) -> TCMT IO (OutputForm c Expr)
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo Closure Range
mv (TCMT IO (OutputForm c Expr) -> TCMT IO (OutputForm c Expr))
-> TCMT IO (OutputForm c Expr) -> TCMT IO (OutputForm c Expr)
forall a b. (a -> b) -> a -> b
$ do
        let m :: Expr
m = MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
emptyMetaInfo{ metaNumber :: Maybe MetaId
metaNumber = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just (MetaId -> Maybe MetaId) -> MetaId -> Maybe MetaId
forall a b. (a -> b) -> a -> b
$ InteractionId -> MetaId
forall a b. (Integral a, Num b) => a -> b
fromIntegral InteractionId
ii } InteractionId
ii
        OutputForm a Expr -> TCMT IO (OutputForm c Expr)
forall a c (m :: * -> *).
(ToConcrete a c, MonadAbsToCon m) =>
a -> m c
abstractToConcrete_ (OutputForm a Expr -> TCMT IO (OutputForm c Expr))
-> OutputForm a Expr -> TCMT IO (OutputForm c Expr)
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId] -> OutputConstraint a Expr -> OutputForm a Expr
forall a b.
Range -> [ProblemId] -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] (OutputConstraint a Expr -> OutputForm a Expr)
-> OutputConstraint a Expr -> OutputForm a Expr
forall a b. (a -> b) -> a -> b
$ Expr -> a -> OutputConstraint a Expr
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 <- InteractionId -> TCMT IO InteractionPoint
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]
ipcBoundary = [Closure IPBoundary]
cs } -> do
          [Closure IPBoundary]
-> (Closure IPBoundary -> TCMT IO (IPBoundary' Expr))
-> TCM [IPBoundary' Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Closure IPBoundary]
cs ((Closure IPBoundary -> TCMT IO (IPBoundary' Expr))
 -> TCM [IPBoundary' Expr])
-> (Closure IPBoundary -> TCMT IO (IPBoundary' Expr))
-> TCM [IPBoundary' Expr]
forall a b. (a -> b) -> a -> b
$ \ Closure IPBoundary
cl -> Closure IPBoundary
-> (IPBoundary -> TCMT IO (IPBoundary' Expr))
-> TCMT IO (IPBoundary' Expr)
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure IPBoundary
cl ((IPBoundary -> TCMT IO (IPBoundary' Expr))
 -> TCMT IO (IPBoundary' Expr))
-> (IPBoundary -> TCMT IO (IPBoundary' Expr))
-> TCMT IO (IPBoundary' Expr)
forall a b. (a -> b) -> a -> b
$ \ IPBoundary
b ->
            IPBoundary' Expr -> TCMT IO (IPBoundary' Expr)
forall a c (m :: * -> *).
(ToConcrete a c, MonadAbsToCon m) =>
a -> m c
abstractToConcrete_ (IPBoundary' Expr -> TCMT IO (IPBoundary' Expr))
-> TCMT IO (IPBoundary' Expr) -> TCMT IO (IPBoundary' Expr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IPBoundary -> TCMT IO (IPBoundary' Expr)
forall i a. Reify i a => i -> TCM a
reifyUnblocked (IPBoundary -> TCMT IO (IPBoundary' Expr))
-> TCMT IO IPBoundary -> TCMT IO (IPBoundary' Expr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite -> IPBoundary -> TCMT IO IPBoundary
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm IPBoundary
b
        IPClause
IPNoClause -> [IPBoundary' Expr] -> TCM [IPBoundary' Expr]
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Goals and Warnings

getGoals :: TCM Goals
getGoals :: TCM Goals
getGoals = do
  -- visible metas (as-is)
  [OutputConstraint Expr InteractionId]
visibleMetas <- Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas Rewrite
AsIs
  -- hidden metas (unsolved implicit arguments simplified)
  Bool
unsolvedNotOK <- Bool -> Bool
not (Bool -> Bool) -> (PragmaOptions -> Bool) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Bool
optAllowUnsolved (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  [OutputConstraint Expr NamedMeta]
hiddenMetas <- (Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
unsolvedNotOK [()]
-> [OutputConstraint Expr NamedMeta]
-> [OutputConstraint Expr NamedMeta]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>) ([OutputConstraint Expr NamedMeta]
 -> [OutputConstraint Expr NamedMeta])
-> TCMT IO [OutputConstraint Expr NamedMeta]
-> TCMT IO [OutputConstraint Expr NamedMeta]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rewrite -> TCMT IO [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas Rewrite
Simplified
  Goals -> TCM Goals
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 String
showGoals ([OutputConstraint Expr InteractionId]
ims, [OutputConstraint Expr NamedMeta]
hms) = do
  [Doc]
di <- [OutputConstraint Expr InteractionId]
-> (OutputConstraint Expr InteractionId -> TCM Doc)
-> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [OutputConstraint Expr InteractionId]
ims ((OutputConstraint Expr InteractionId -> TCM Doc) -> TCMT IO [Doc])
-> (OutputConstraint Expr InteractionId -> TCM Doc)
-> TCMT IO [Doc]
forall a b. (a -> b) -> a -> b
$ \ OutputConstraint Expr InteractionId
i ->
    InteractionId -> TCM Doc -> TCM Doc
forall a. InteractionId -> TCM a -> TCM a
withInteractionId (OutputForm Expr InteractionId -> InteractionId
forall a b. OutputForm a b -> b
outputFormId (OutputForm Expr InteractionId -> InteractionId)
-> OutputForm Expr InteractionId -> InteractionId
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId]
-> OutputConstraint Expr InteractionId
-> OutputForm Expr InteractionId
forall a b.
Range -> [ProblemId] -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] OutputConstraint Expr InteractionId
i) (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$
      OutputConstraint Expr InteractionId -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr InteractionId
i
  Names
dh <- (OutputConstraint Expr NamedMeta -> TCM String)
-> [OutputConstraint Expr NamedMeta] -> TCMT IO Names
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM OutputConstraint Expr NamedMeta -> TCM String
showA' [OutputConstraint Expr NamedMeta]
hms
  String -> TCM String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCM String) -> String -> TCM String
forall a b. (a -> b) -> a -> b
$ Names -> String
unlines (Names -> String) -> Names -> String
forall a b. (a -> b) -> a -> b
$ (Doc -> String) -> [Doc] -> Names
forall a b. (a -> b) -> [a] -> [b]
map Doc -> String
forall a. Show a => a -> String
show [Doc]
di Names -> Names -> Names
forall a. [a] -> [a] -> [a]
++ Names
dh
  where
    showA' :: OutputConstraint A.Expr NamedMeta -> TCM String
    showA' :: OutputConstraint Expr NamedMeta -> TCM String
showA' OutputConstraint Expr NamedMeta
m = do
      let i :: MetaId
i = NamedMeta -> MetaId
nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
forall a b. (a -> b) -> a -> b
$ OutputConstraint Expr NamedMeta -> NamedMeta
forall a. OutputConstraint Expr a -> a
namedMetaOf OutputConstraint Expr NamedMeta
m
      Range
r <- MetaId -> TCMT IO Range
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
i
      Doc
d <- MetaId -> TCM Doc -> TCM Doc
forall a. MetaId -> TCM a -> TCM a
withMetaId MetaId
i (OutputConstraint Expr NamedMeta -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr NamedMeta
m)
      String -> TCM String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCM String) -> String -> TCM String
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show Doc
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  [ at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Show a => a -> String
show Range
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ]"

getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
getWarningsAndNonFatalErrors = do
  MaybeWarnings
mws <- WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings WhichWarnings
AllWarnings
  let notMetaWarnings :: MaybeWarnings
notMetaWarnings = (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Bool
isMetaTCWarning) ([TCWarning] -> [TCWarning]) -> MaybeWarnings -> MaybeWarnings
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeWarnings
mws
  WarningsAndNonFatalErrors -> TCM WarningsAndNonFatalErrors
forall (m :: * -> *) a. Monad m => a -> m a
return (WarningsAndNonFatalErrors -> TCM WarningsAndNonFatalErrors)
-> WarningsAndNonFatalErrors -> TCM WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ case MaybeWarnings
notMetaWarnings of
    SomeWarnings ws :: [TCWarning]
ws@(TCWarning
_:[TCWarning]
_) -> [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings [TCWarning]
ws
    MaybeWarnings
_ -> 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 -> TCMT IO [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints Bool
all Rewrite
norm = [[(InteractionId, MetaId, Expr)]]
-> [(InteractionId, MetaId, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(InteractionId, MetaId, Expr)]]
 -> [(InteractionId, MetaId, Expr)])
-> TCMT IO [[(InteractionId, MetaId, Expr)]]
-> TCMT IO [(InteractionId, MetaId, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
  ((InteractionId, MetaId)
 -> TCMT IO [(InteractionId, MetaId, Expr)])
-> [(InteractionId, MetaId)]
-> TCMT IO [[(InteractionId, MetaId, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InteractionId, MetaId) -> TCMT IO [(InteractionId, MetaId, Expr)]
forall a. (a, MetaId) -> TCMT IO [(a, MetaId, Expr)]
solution ([(InteractionId, MetaId)]
 -> TCMT IO [[(InteractionId, MetaId, Expr)]])
-> TCMT IO [(InteractionId, MetaId)]
-> TCMT IO [[(InteractionId, MetaId, Expr)]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [(InteractionId, MetaId)]
forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas
  where
    solution :: (a, MetaId) -> TCMT IO [(a, MetaId, Expr)]
solution (a
i, MetaId
m) = do
      MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
      Closure Range
-> TCMT IO [(a, MetaId, Expr)] -> TCMT IO [(a, MetaId, Expr)]
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCMT IO [(a, MetaId, Expr)] -> TCMT IO [(a, MetaId, Expr)])
-> TCMT IO [(a, MetaId, Expr)] -> TCMT IO [(a, MetaId, Expr)]
forall a b. (a -> b) -> a -> b
$ do
        Args
args  <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
        ScopeInfo
scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
        let sol :: Term -> TCMT IO [(a, MetaId, Expr)]
sol Term
v = do
              -- Andreas, 2014-02-17 exclude metas solved by metas
              Term
v <- Term -> TCM Term
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 [(a, MetaId, Expr)] -> TCMT IO [(a, MetaId, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
                Expr
e <- Expr -> TCM Expr
forall (m :: * -> *) a. (MonadTCEnv m, BlankVars a) => a -> m a
blankNotInScope (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCM Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Term -> TCM Expr) -> TCM Term -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite -> Term -> TCM Term
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Term
v
                [(a, MetaId, Expr)] -> TCMT IO [(a, MetaId, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(a
i, MetaId
m, ScopeInfo -> Expr -> Expr
ScopedExpr ScopeInfo
scope Expr
e)]
            unsol :: TCMT IO [a]
unsol = [a] -> TCMT IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
        case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
mv of
          InstV{}                        -> Term -> TCMT IO [(a, MetaId, Expr)]
sol (MetaId -> Elims -> Term
MetaV MetaId
m (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Args
args)
          Open{}                         -> TCMT IO [(a, MetaId, Expr)]
forall a. TCMT IO [a]
unsol
          OpenInstance{}                 -> TCMT IO [(a, MetaId, Expr)]
forall a. TCMT IO [a]
unsol
          BlockedConst{}                 -> TCMT IO [(a, MetaId, Expr)]
forall a. TCMT IO [a]
unsol
          PostponedTypeCheckingProblem{} -> TCMT IO [(a, MetaId, Expr)]
forall a. TCMT IO [a]
unsol

typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI Rewrite
norm MetaId
mi =
     do MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi
        Closure Range
-> TCM (OutputConstraint Expr NamedMeta)
-> TCM (OutputConstraint Expr NamedMeta)
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCM (OutputConstraint Expr NamedMeta)
 -> TCM (OutputConstraint Expr NamedMeta))
-> TCM (OutputConstraint Expr NamedMeta)
-> TCM (OutputConstraint Expr NamedMeta)
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
      String
ms <- MetaId -> TCM String
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m String
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 <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
      Type
t <- Type
t Type -> Args -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` Permutation -> Args -> Args
forall a. Permutation -> [a] -> [a]
permute (VerboseLevel -> Permutation -> Permutation
takeP (Args -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Args
vs) (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) Args
vs
      Type
t <- Rewrite -> Type -> TCMT IO Type
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Type
t
      let x :: NamedMeta
x = String -> MetaId -> NamedMeta
NamedMeta String
ms MetaId
i
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interactive.meta" VerboseLevel
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TP.vcat
        [ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TP.text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Names -> String
unwords [String
"permuting", MetaId -> String
forall a. Show a => a -> String
show MetaId
i, String
"with", Permutation -> String
forall a. Show a => a -> String
show (Permutation -> String) -> Permutation -> String
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv]
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TP.vcat
          [ TCM Doc
"len  =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TP.text (VerboseLevel -> String
forall a. Show a => a -> String
show (VerboseLevel -> String) -> VerboseLevel -> String
forall a b. (a -> b) -> a -> b
$ Args -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length Args
vs)
          , TCM Doc
"args =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Args -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Args
vs
          , TCM Doc
"t    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
          , TCM Doc
"x    =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> NamedMeta -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
TP.pretty NamedMeta
x
          ]
        ]
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interactive.meta.scope" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TP.text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ ScopeInfo -> String
forall a. Show a => a -> String
show (ScopeInfo -> String) -> ScopeInfo -> String
forall a b. (a -> b) -> a -> b
$ MetaVariable -> ScopeInfo
getMetaScope MetaVariable
mv
      -- Andreas, 2016-01-19, issue #1783: need piApplyM instead of just piApply
      NamedMeta -> Expr -> OutputConstraint Expr NamedMeta
forall a b. b -> a -> OutputConstraint a b
OfType NamedMeta
x (Expr -> OutputConstraint Expr NamedMeta)
-> TCM Expr -> TCM (OutputConstraint Expr NamedMeta)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM Expr
forall i a. Reify i a => i -> TCM a
reifyUnblocked Type
t
    rewriteJudg MetaVariable
mv (IsSort MetaId
i Type
t) = do
      String
ms <- MetaId -> TCM String
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m String
getMetaNameSuggestion MetaId
i
      OutputConstraint Expr NamedMeta
-> TCM (OutputConstraint Expr NamedMeta)
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConstraint Expr NamedMeta
 -> TCM (OutputConstraint Expr NamedMeta))
-> OutputConstraint Expr NamedMeta
-> TCM (OutputConstraint Expr NamedMeta)
forall a b. (a -> b) -> a -> b
$ NamedMeta -> OutputConstraint Expr NamedMeta
forall a b. b -> OutputConstraint a b
JustSort (NamedMeta -> OutputConstraint Expr NamedMeta)
-> NamedMeta -> OutputConstraint Expr NamedMeta
forall a b. (a -> b) -> a -> b
$ String -> MetaId -> NamedMeta
NamedMeta String
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 ((InteractionId, MetaId)
 -> TCM (OutputConstraint Expr InteractionId))
-> (MetaId -> (InteractionId, MetaId))
-> MetaId
-> TCM (OutputConstraint Expr InteractionId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionId
ii,) (MetaId -> TCM (OutputConstraint Expr InteractionId))
-> TCMT IO MetaId -> TCM (OutputConstraint Expr InteractionId)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> TCMT IO MetaId
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) = (NamedMeta -> InteractionId)
-> OutputConstraint Expr NamedMeta
-> OutputConstraint Expr InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\NamedMeta
_ -> InteractionId
ii) (OutputConstraint Expr NamedMeta
 -> OutputConstraint Expr InteractionId)
-> TCM (OutputConstraint Expr NamedMeta)
-> TCM (OutputConstraint Expr InteractionId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI Rewrite
norm MetaId
mi

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

typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas :: Rewrite -> TCMT IO [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas Rewrite
norm = TCMT IO [OutputConstraint Expr NamedMeta]
-> TCMT IO [OutputConstraint Expr NamedMeta]
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO [OutputConstraint Expr NamedMeta]
 -> TCMT IO [OutputConstraint Expr NamedMeta])
-> TCMT IO [OutputConstraint Expr NamedMeta]
-> TCMT IO [OutputConstraint Expr NamedMeta]
forall a b. (a -> b) -> a -> b
$ do
  [MetaId]
is    <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
  IntMap MetaVariable
store <- (VerboseLevel -> MetaVariable -> Bool)
-> IntMap MetaVariable -> IntMap MetaVariable
forall a. (VerboseLevel -> a -> Bool) -> IntMap a -> IntMap a
IntMap.filterWithKey ([MetaId] -> MetaId -> MetaVariable -> Bool
forall (t :: * -> *) a.
(Foldable t, Eq a) =>
t a -> a -> MetaVariable -> Bool
openAndImplicit [MetaId]
is (MetaId -> MetaVariable -> Bool)
-> (VerboseLevel -> MetaId) -> VerboseLevel -> MetaVariable -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> MetaId
MetaId) (IntMap MetaVariable -> IntMap MetaVariable)
-> TCMT IO (IntMap MetaVariable) -> TCMT IO (IntMap MetaVariable)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (IntMap MetaVariable)
forall (m :: * -> *). ReadTCState m => m (IntMap MetaVariable)
getMetaStore
  (VerboseLevel -> TCM (OutputConstraint Expr NamedMeta))
-> [VerboseLevel] -> TCMT IO [OutputConstraint Expr NamedMeta]
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 (MetaId -> TCM (OutputConstraint Expr NamedMeta))
-> (VerboseLevel -> MetaId)
-> VerboseLevel
-> TCM (OutputConstraint Expr NamedMeta)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> MetaId
MetaId) ([VerboseLevel] -> TCMT IO [OutputConstraint Expr NamedMeta])
-> [VerboseLevel] -> TCMT IO [OutputConstraint Expr NamedMeta]
forall a b. (a -> b) -> a -> b
$ IntMap MetaVariable -> [VerboseLevel]
forall a. IntMap a -> [VerboseLevel]
IntMap.keys IntMap MetaVariable
store
  where
  openAndImplicit :: t a -> a -> MetaVariable -> Bool
openAndImplicit t a
is a
x MetaVariable
m | Maybe MetaId -> Bool
forall a. Maybe a -> Bool
isJust (MetaVariable -> Maybe MetaId
mvTwin MetaVariable
m) = Bool
False
  openAndImplicit t a
is a
x MetaVariable
m =
    case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
m of
      M.InstV{} -> Bool
False
      MetaInstantiation
M.Open    -> a
x a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t a
is
      MetaInstantiation
M.OpenInstance -> a
x a -> t a -> Bool
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
-> String
-> TCM (OutputConstraint' Expr Expr)
metaHelperType Rewrite
norm InteractionId
ii Range
rng String
s = case String -> Names
words String
s of
  []    -> TCM (OutputConstraint' Expr Expr)
forall a. TCMT IO a
failure
  String
f : Names
_ -> InteractionId
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall a. InteractionId -> TCM a -> TCM a
withInteractionId InteractionId
ii (TCM (OutputConstraint' Expr Expr)
 -> TCM (OutputConstraint' Expr Expr))
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall a b. (a -> b) -> a -> b
$ do
    String -> TCMT IO ()
ensureName String
f
    A.Application Expr
h [NamedArg Expr]
args <- Expr -> AppView' Expr
A.appView (Expr -> AppView' Expr) -> (Expr -> Expr) -> Expr -> AppView' Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
getBody (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope (Expr -> AppView' Expr) -> TCM Expr -> TCMT IO (AppView' Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> Range -> String -> TCM Expr
parseExprIn InteractionId
ii Range
rng (String
"let " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = _ in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)
    Name -> Bool
inCxt   <- [Name] -> Name -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem ([Name] -> Name -> Bool)
-> TCMT IO [Name] -> TCMT IO (Name -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Name]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Name]
getContextNames
    Args
cxtArgs <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
    Type
a0      <- (Type -> Args -> Type
`piApply` Args
cxtArgs) (Type -> Type) -> TCMT IO Type -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MetaId -> TCMT IO Type
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Type
getMetaType (MetaId -> TCMT IO Type) -> TCMT IO MetaId -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii)
    case (NamedArg Expr -> Maybe Name) -> [NamedArg Expr] -> Maybe [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Expr -> Maybe Name
isVar (Expr -> Maybe Name)
-> (NamedArg Expr -> Expr) -> NamedArg Expr -> Maybe Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg) [NamedArg Expr]
args Maybe [Name] -> ([Name] -> Maybe [Name]) -> Maybe [Name]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ [Name]
xs -> [Name]
xs [Name] -> Maybe () -> Maybe [Name]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ((Name -> Bool) -> [Name] -> Bool
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 = [Name] -> Name -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [Name]
xs
      let hideButXs :: Dom' t (Name, b) -> Dom' t (Name, b)
hideButXs Dom' t (Name, b)
dom = Hiding -> Dom' t (Name, b) -> Dom' t (Name, b)
forall a. LensHiding a => Hiding -> a -> a
setHiding (if Name -> Bool
inXs (Name -> Bool) -> Name -> Bool
forall a b. (a -> b) -> a -> b
$ (Name, b) -> Name
forall a b. (a, b) -> a
fst ((Name, b) -> Name) -> (Name, b) -> Name
forall a b. (a -> b) -> a -> b
$ Dom' t (Name, b) -> (Name, b)
forall t e. Dom' t e -> e
unDom Dom' t (Name, b)
dom then Hiding
NotHidden else Hiding
Hidden) Dom' t (Name, b)
dom
      Telescope
tel  <- ListTel -> Telescope
telFromList (ListTel -> Telescope)
-> ([Dom' Term (Name, Type)] -> ListTel)
-> [Dom' Term (Name, Type)]
-> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom' Term (Name, Type) -> Dom' Term (String, Type))
-> [Dom' Term (Name, Type)] -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map (((Name, Type) -> (String, Type))
-> Dom' Term (Name, Type) -> Dom' Term (String, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> String) -> (Name, Type) -> (String, Type)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Name -> String
nameToArgName) (Dom' Term (Name, Type) -> Dom' Term (String, Type))
-> (Dom' Term (Name, Type) -> Dom' Term (Name, Type))
-> Dom' Term (Name, Type)
-> Dom' Term (String, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> Dom' Term (Name, Type)
forall t b. Dom' t (Name, b) -> Dom' t (Name, b)
hideButXs) ([Dom' Term (Name, Type)] -> ListTel)
-> ([Dom' Term (Name, Type)] -> [Dom' Term (Name, Type)])
-> [Dom' Term (Name, Type)]
-> ListTel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Dom' Term (Name, Type)] -> [Dom' Term (Name, Type)]
forall a. [a] -> [a]
reverse ([Dom' Term (Name, Type)] -> Telescope)
-> TCMT IO [Dom' Term (Name, Type)] -> TCMT IO Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Dom' Term (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
getContext
      Expr -> Expr -> OutputConstraint' Expr Expr
forall a b. b -> a -> OutputConstraint' a b
OfType' Expr
h (Expr -> OutputConstraint' Expr Expr)
-> TCM Expr -> TCM (OutputConstraint' Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        -- Andreas, 2019-10-11: I actually prefer pi-types over ->.
        (TCEnv -> TCEnv) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envPrintDomainFreePi :: Bool
envPrintDomainFreePi = Bool
True }) (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ Type -> TCM Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Type -> TCM Expr) -> Type -> TCM Expr
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  <- TCMT IO Args
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  <- Identity Telescope -> Telescope
forall a. Identity a -> a
runIdentity (Identity Telescope -> Telescope)
-> (Telescope -> Identity Telescope) -> Telescope -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Identity String) -> Telescope -> Identity Telescope
forall (f :: * -> *).
Applicative f =>
(String -> f String) -> Telescope -> f Telescope
onNamesTel String -> Identity String
forall a (m :: * -> *). (Eq a, IsString a, Monad m) => a -> m a
unW (Telescope -> Telescope) -> TCMT IO Telescope -> TCMT IO Telescope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
      let a :: Type
a = Identity Type -> Type
forall a. Identity a -> a
runIdentity (Identity Type -> Type) -> (Type -> Identity Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Identity String) -> Type -> Identity Type
forall (m :: * -> *).
Applicative m =>
(String -> m String) -> Type -> m Type
onNames String -> Identity String
forall a (m :: * -> *). (Eq a, IsString a, Monad m) => a -> m a
unW (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
a0
      [WithHiding (Term, EqualityView)]
vtys <- (NamedArg Expr -> TCMT IO (WithHiding (Term, EqualityView)))
-> [NamedArg Expr] -> TCMT IO [WithHiding (Term, EqualityView)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ NamedArg Expr
a -> ((Term, Type) -> WithHiding (Term, EqualityView))
-> TCM (Term, Type) -> TCMT IO (WithHiding (Term, EqualityView))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Hiding -> (Term, EqualityView) -> WithHiding (Term, EqualityView)
forall a. Hiding -> a -> WithHiding a
WithHiding (NamedArg Expr -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding NamedArg Expr
a) ((Term, EqualityView) -> WithHiding (Term, EqualityView))
-> ((Term, Type) -> (Term, EqualityView))
-> (Term, Type)
-> WithHiding (Term, EqualityView)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> EqualityView) -> (Term, Type) -> (Term, EqualityView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> EqualityView
OtherType) (TCM (Term, Type) -> TCMT IO (WithHiding (Term, EqualityView)))
-> TCM (Term, Type) -> TCMT IO (WithHiding (Term, EqualityView))
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Term, Type)
inferExpr (Expr -> TCM (Term, Type)) -> Expr -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg Expr
a) [NamedArg Expr]
args
      -- Remember the arity of a
      TelV Telescope
atel Type
_ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
a
      let arity :: VerboseLevel
arity = Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
atel
          (Telescope
delta1, Telescope
delta2, Permutation
_, Type
a', [WithHiding (Term, EqualityView)]
vtys') = Telescope
-> Type
-> [WithHiding (Term, EqualityView)]
-> (Telescope, Telescope, Permutation, Type,
    [WithHiding (Term, EqualityView)])
splitTelForWith Telescope
tel Type
a [WithHiding (Term, EqualityView)]
vtys
      Expr
a <- (TCEnv -> TCEnv) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envPrintDomainFreePi :: Bool
envPrintDomainFreePi = Bool
True }) (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ do
        Type -> TCM Expr
forall i a (m :: * -> *). (Reify i a, MonadReify m) => i -> m a
reify (Type -> TCM Expr) -> TCMT IO Type -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< VerboseLevel -> [NamedArg Expr] -> Type -> TCMT IO Type
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
VerboseLevel -> [NamedArg Expr] -> Type -> m Type
cleanupType VerboseLevel
arity [NamedArg Expr]
args (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite -> Type -> TCMT IO Type
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Type, VerboseLevel) -> Type
forall a b. (a, b) -> a
fst ((Type, VerboseLevel) -> Type)
-> TCMT IO (Type, VerboseLevel) -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Telescope
-> [WithHiding (Term, EqualityView)]
-> Telescope
-> Type
-> TCMT IO (Type, VerboseLevel)
withFunctionType Telescope
delta1 [WithHiding (Term, EqualityView)]
vtys' Telescope
delta2 Type
a'
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.helper" VerboseLevel
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TP.vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
        let extractOtherType :: EqualityView -> Type
extractOtherType = \case { OtherType Type
a -> Type
a; EqualityView
_ -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__ } in
        let ([Term]
vs, [Type]
as)   = (WithHiding (Term, EqualityView) -> (Term, Type))
-> [WithHiding (Term, EqualityView)] -> ([Term], [Type])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith ((EqualityView -> Type) -> (Term, EqualityView) -> (Term, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EqualityView -> Type
extractOtherType ((Term, EqualityView) -> (Term, Type))
-> (WithHiding (Term, EqualityView) -> (Term, EqualityView))
-> WithHiding (Term, EqualityView)
-> (Term, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithHiding (Term, EqualityView) -> (Term, EqualityView)
forall a. WithHiding a -> a
whThing) [WithHiding (Term, EqualityView)]
vtys in
        let ([Term]
vs', [Type]
as') = (WithHiding (Term, EqualityView) -> (Term, Type))
-> [WithHiding (Term, EqualityView)] -> ([Term], [Type])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith ((EqualityView -> Type) -> (Term, EqualityView) -> (Term, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap EqualityView -> Type
extractOtherType ((Term, EqualityView) -> (Term, Type))
-> (WithHiding (Term, EqualityView) -> (Term, EqualityView))
-> WithHiding (Term, EqualityView)
-> (Term, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithHiding (Term, EqualityView) -> (Term, EqualityView)
forall a. WithHiding a -> a
whThing) [WithHiding (Term, EqualityView)]
vtys' in
        [ TCM Doc
"generating helper function"
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"tel    = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel)
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"a      = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Expr -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
a
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"vs     = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> [Term] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"as     = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> [Type] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Type]
as
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"delta1 = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta1)
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"delta2 = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
delta2)
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"a'     = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
a')
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"as'    = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Type] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Type]
as')
        , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc
"vs'    = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
delta1 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Term] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Term]
vs')
        ]
      OutputConstraint' Expr Expr -> TCM (OutputConstraint' Expr Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (OutputConstraint' Expr Expr -> TCM (OutputConstraint' Expr Expr))
-> OutputConstraint' Expr Expr -> TCM (OutputConstraint' Expr Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> OutputConstraint' Expr Expr
forall a b. b -> a -> OutputConstraint' a b
OfType' Expr
h Expr
a
  where
    failure :: TCMT IO a
failure = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ String
"Expected an argument of the form f e1 e2 .. en"
    ensureName :: String -> TCMT IO ()
ensureName String
f = do
      Expr
ce <- Range -> String -> TCM Expr
parseExpr Range
rng String
f
      (TCMT IO () -> (Name -> TCMT IO ()) -> TCMT IO ())
-> (Name -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe Name -> TCMT IO () -> (Name -> TCMT IO ()) -> TCMT IO ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Maybe Name -> TCMT IO () -> (Name -> TCMT IO ()) -> TCMT IO ())
-> Maybe Name -> TCMT IO () -> (Name -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Name
isName Expr
ce) (\ Name
_ -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
         String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"interaction.helper" VerboseLevel
10 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"ce = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
ce
         TCMT IO ()
forall a. TCMT IO a
failure
    isName :: C.Expr -> Maybe C.Name
    isName :: Expr -> Maybe Name
isName = \case
      C.Ident (C.QName Name
x)              -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
      C.RawApp Range
_ [C.Ident (C.QName Name
x)] -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
      Expr
_ -> Maybe Name
forall a. Maybe a
Nothing
    isVar :: A.Expr -> Maybe A.Name
    isVar :: Expr -> Maybe Name
isVar = \case
      A.Var Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
      Expr
_ -> Maybe Name
forall a. Maybe a
Nothing
    cleanupType :: VerboseLevel -> [NamedArg Expr] -> Type -> m Type
cleanupType VerboseLevel
arity [NamedArg Expr]
args Type
t = do
      -- Get the arity of t
      TelV Telescope
ttel Type
_ <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
      -- Compute the number of pi-types subject to stripping.
      let n :: VerboseLevel
n = Telescope -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size Telescope
ttel VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
arity
      -- It cannot be negative, otherwise we would have performed a
      -- negative number of with-abstractions.
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
>= VerboseLevel
0) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ State [NamedArg Expr] Type -> [NamedArg Expr] -> Type
forall s a. State s a -> s -> a
evalState (Type -> State [NamedArg Expr] Type
renameVars (Type -> State [NamedArg Expr] Type)
-> Type -> State [NamedArg Expr] Type
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Type -> Type
forall a. (Num a, Eq a) => a -> Type -> Type
stripUnused VerboseLevel
n Type
t) [NamedArg Expr]
args

    getBody :: Expr -> Expr
getBody (A.Let ExprInfo
_ [LetBinding]
_ Expr
e)      = Expr
e
    getBody Expr
_                  = 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) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ a -> Term -> Term
strip a
n Term
v
    strip :: a -> Term -> Term
strip a
0 Term
v = Term
v
    strip a
n Term
v = case Term
v of
      I.Pi Dom Type
a Abs Type
b -> case a -> Type -> Type
stripUnused (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) (Type -> Type) -> Abs Type -> Abs Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b of
        Abs Type
b | Abs Type -> String
forall a. Abs a -> String
absName Abs Type
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"w"   -> Dom Type -> Abs Type -> Term
I.Pi Dom Type
a Abs Type
b
        NoAbs String
_ Type
b              -> Type -> Term
forall t a. Type'' t a -> a
unEl Type
b
        Abs String
s Type
b | VerboseLevel
0 VerboseLevel -> Type -> Bool
forall a. Free a => VerboseLevel -> a -> Bool
`freeIn` Type
b -> Dom Type -> Abs Type -> Term
I.Pi (Dom Type -> Dom Type
forall a. LensHiding a => a -> a
hide Dom Type
a) (String -> Type -> Abs Type
forall a. String -> a -> Abs a
Abs String
s Type
b)
                | Bool
otherwise    -> Empty -> Term -> Term
forall t a. Subst t a => Empty -> a -> a
strengthen Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ (Type -> Term
forall t a. Type'' t a -> a
unEl Type
b)
      Term
_ -> Term
v  -- todo: handle if goal type is a Pi

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

    -- onNames :: Applicative m => (ArgName -> m ArgName) -> Type -> m Type
    onNames :: Applicative m => (String -> m String) -> Type -> m Type
    onNames :: (String -> m String) -> Type -> m Type
onNames String -> m String
f (El Sort
s Term
v) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> m String) -> Term -> m Term
forall (f :: * -> *).
Applicative f =>
(String -> f String) -> Term -> f Term
onNamesTm String -> m String
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 :: (String -> f String) -> Telescope -> f Telescope
onNamesTel String -> f String
f Telescope
I.EmptyTel = Telescope -> f Telescope
forall (f :: * -> *) a. Applicative f => a -> f a
pure Telescope
forall a. Tele a
I.EmptyTel
    onNamesTel String -> f String
f (I.ExtendTel Dom Type
a Abs Telescope
b) = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
I.ExtendTel (Dom Type -> Abs Telescope -> Telescope)
-> f (Dom Type) -> f (Abs Telescope -> Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> f Type) -> Dom Type -> f (Dom Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((String -> f String) -> Type -> f Type
forall (m :: * -> *).
Applicative m =>
(String -> m String) -> Type -> m Type
onNames String -> f String
f) Dom Type
a f (Abs Telescope -> Telescope) -> f (Abs Telescope) -> f Telescope
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> f String)
-> ((String -> f String) -> Telescope -> f Telescope)
-> Abs Telescope
-> f (Abs Telescope)
forall (f :: * -> *) t a.
Applicative f =>
(String -> f String)
-> ((String -> f String) -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs String -> f String
f (String -> f String) -> Telescope -> f Telescope
forall (f :: * -> *).
Applicative f =>
(String -> f String) -> Telescope -> f Telescope
onNamesTel Abs Telescope
b

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

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

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

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


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

contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta InteractionId
ii Rewrite
norm = InteractionId
-> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
forall a. InteractionId -> TCM a -> TCM a
withInteractionId InteractionId
ii (TCM [ResponseContextEntry] -> TCM [ResponseContextEntry])
-> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
forall a b. (a -> b) -> a -> b
$ do
  Closure Range
info <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> TCMT IO MetaVariable -> TCMT IO (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta (MetaId -> TCMT IO MetaVariable)
-> TCMT IO MetaId -> TCMT IO MetaVariable
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii)
  Closure Range
-> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo Closure Range
info (TCM [ResponseContextEntry] -> TCM [ResponseContextEntry])
-> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
forall a b. (a -> b) -> a -> b
$ do
    -- List of local variables.
    [Dom' Term (Name, Type)]
cxt <- TCMT IO [Dom' Term (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
getContext
    let n :: VerboseLevel
n         = [Dom' Term (Name, Type)] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Dom' Term (Name, Type)]
cxt
        localVars :: [Dom' Term (Name, Type)]
localVars = (VerboseLevel -> Dom' Term (Name, Type) -> Dom' Term (Name, Type))
-> [VerboseLevel]
-> [Dom' Term (Name, Type)]
-> [Dom' Term (Name, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VerboseLevel -> Dom' Term (Name, Type) -> Dom' Term (Name, Type)
forall t a. Subst t a => VerboseLevel -> a -> a
raise [VerboseLevel
1..] [Dom' Term (Name, Type)]
cxt
    -- List of let-bindings.
    [(Name, Open (Term, Dom Type))]
letVars <- Map Name (Open (Term, Dom Type)) -> [(Name, Open (Term, Dom Type))]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map Name (Open (Term, Dom Type))
 -> [(Name, Open (Term, Dom Type))])
-> TCMT IO (Map Name (Open (Term, Dom Type)))
-> TCMT IO [(Name, Open (Term, Dom Type))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Map Name (Open (Term, Dom Type)))
-> TCMT IO (Map Name (Open (Term, Dom Type)))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Map Name (Open (Term, Dom Type))
envLetBindings
    -- Reify the types and filter out bindings without a name.
    [ResponseContextEntry]
-> [ResponseContextEntry] -> [ResponseContextEntry]
forall a. [a] -> [a] -> [a]
(++) ([ResponseContextEntry]
 -> [ResponseContextEntry] -> [ResponseContextEntry])
-> TCM [ResponseContextEntry]
-> TCMT IO ([ResponseContextEntry] -> [ResponseContextEntry])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Dom' Term (Name, Type)]
-> (Dom' Term (Name, Type) -> TCMT IO (Maybe ResponseContextEntry))
-> TCM [ResponseContextEntry]
forall (m :: * -> *) a b.
Monad m =>
[a] -> (a -> m (Maybe b)) -> m [b]
forMaybeM ([Dom' Term (Name, Type)] -> [Dom' Term (Name, Type)]
forall a. [a] -> [a]
reverse [Dom' Term (Name, Type)]
localVars) Dom' Term (Name, Type) -> TCMT IO (Maybe ResponseContextEntry)
mkVar
         TCMT IO ([ResponseContextEntry] -> [ResponseContextEntry])
-> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [(Name, Open (Term, Dom Type))]
-> ((Name, Open (Term, Dom Type))
    -> TCMT IO (Maybe ResponseContextEntry))
-> TCM [ResponseContextEntry]
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))
-> TCMT IO (Maybe ResponseContextEntry)
mkLet

  where
    mkVar :: Dom (Name, Type) -> TCM (Maybe ResponseContextEntry)
    mkVar :: Dom' Term (Name, Type) -> TCMT IO (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 Maybe ResponseContextEntry -> TCMT IO (Maybe ResponseContextEntry)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ResponseContextEntry
forall a. Maybe a
Nothing else ResponseContextEntry -> Maybe ResponseContextEntry
forall a. a -> Maybe a
Just (ResponseContextEntry -> Maybe ResponseContextEntry)
-> TCMT IO ResponseContextEntry
-> TCMT IO (Maybe ResponseContextEntry)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        let n :: Name
n = Name -> Name
nameConcrete Name
name
        Name
x  <- Name -> TCMT IO Name
forall a c (m :: * -> *).
(ToConcrete a c, MonadAbsToCon m) =>
a -> m c
abstractToConcrete_ Name
name
        let s :: NameInScope
s = Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
C.isInScope Name
x
        Expr
ty <- Type -> TCM Expr
forall i a. Reify i a => i -> TCM a
reifyUnblocked (Type -> TCM Expr) -> TCMT IO Type -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite -> Type -> TCMT IO Type
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Type
t
        ResponseContextEntry -> TCMT IO ResponseContextEntry
forall (m :: * -> *) a. Monad m => a -> m a
return (ResponseContextEntry -> TCMT IO ResponseContextEntry)
-> ResponseContextEntry -> TCMT IO ResponseContextEntry
forall a b. (a -> b) -> a -> b
$ Name
-> Name
-> Arg Expr
-> TacticAttr
-> NameInScope
-> ResponseContextEntry
ResponseContextEntry Name
n Name
x (ArgInfo -> Expr -> Arg Expr
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai Expr
ty) TacticAttr
forall a. Maybe a
Nothing NameInScope
s

    mkLet :: (Name, Open (Term, Dom Type)) -> TCM (Maybe ResponseContextEntry)
    mkLet :: (Name, Open (Term, Dom Type))
-> TCMT IO (Maybe ResponseContextEntry)
mkLet (Name
name, Open (Term, Dom Type)
lb) = do
      (Term
tm, !Dom Type
dom) <- Open (Term, Dom Type) -> TCMT IO (Term, Dom Type)
forall a (m :: * -> *).
(Subst Term a, MonadTCEnv m) =>
Open a -> m a
getOpen Open (Term, Dom Type)
lb
      if ArgInfo -> Name -> Bool
shouldHide (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) Name
name then Maybe ResponseContextEntry -> TCMT IO (Maybe ResponseContextEntry)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ResponseContextEntry
forall a. Maybe a
Nothing else ResponseContextEntry -> Maybe ResponseContextEntry
forall a. a -> Maybe a
Just (ResponseContextEntry -> Maybe ResponseContextEntry)
-> TCMT IO ResponseContextEntry
-> TCMT IO (Maybe ResponseContextEntry)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
        let n :: Name
n = Name -> Name
nameConcrete Name
name
        Name
x  <- Name -> TCMT IO Name
forall a c (m :: * -> *).
(ToConcrete a c, MonadAbsToCon m) =>
a -> m c
abstractToConcrete_ Name
name
        let s :: NameInScope
s = Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
C.isInScope Name
x
        Arg Expr
ty <- Dom Type -> TCM (Arg Expr)
forall i a. Reify i a => i -> TCM a
reifyUnblocked (Dom Type -> TCM (Arg Expr))
-> TCMT IO (Dom Type) -> TCM (Arg Expr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite -> Dom Type -> TCMT IO (Dom Type)
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Dom Type
dom
        Expr
v  <- Term -> TCM Expr
forall i a. Reify i a => i -> TCM a
reifyUnblocked (Term -> TCM Expr) -> TCM Term -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite -> Term -> TCM Term
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Term
tm
        ResponseContextEntry -> TCMT IO ResponseContextEntry
forall (m :: * -> *) a. Monad m => a -> m a
return (ResponseContextEntry -> TCMT IO ResponseContextEntry)
-> ResponseContextEntry -> TCMT IO ResponseContextEntry
forall a b. (a -> b) -> a -> b
$ Name
-> Name
-> Arg Expr
-> TacticAttr
-> NameInScope
-> ResponseContextEntry
ResponseContextEntry Name
n Name
x Arg Expr
ty (Expr -> TacticAttr
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 (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai) Bool -> Bool -> Bool
&& (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
n Bool -> Bool -> Bool
|| Name -> Bool
nameIsRecordName Name
n)

-- | Returns the type of the expression in the current environment
--   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) <- TCM (Term, Type) -> TCM (Term, Type)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
wakeIrrelevantVars (TCM (Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Term, Type)
inferExpr Expr
e
        Type
v <- Rewrite -> Type -> TCMT IO Type
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Type
t
        Type -> TCM Expr
forall i a. Reify i a => i -> TCM a
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 <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
        Closure Range
mi <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> TCMT IO MetaVariable -> TCMT IO (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
        Closure Range -> TCM Expr -> TCM Expr
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo Closure Range
mi (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$
            Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
norm Expr
e

withInteractionId :: InteractionId -> TCM a -> TCM a
withInteractionId :: InteractionId -> TCM a -> TCM a
withInteractionId InteractionId
i TCM a
ret = do
  MetaId
m <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
  MetaId -> TCM a -> TCM a
forall a. MetaId -> TCM a -> TCM a
withMetaId MetaId
m TCM a
ret

withMetaId :: MetaId -> TCM a -> TCM a
withMetaId :: MetaId -> TCM a -> TCM a
withMetaId MetaId
m TCM a
ret = do
  MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
  MetaVariable -> TCM a -> TCM a
forall a. MetaVariable -> TCM a -> TCM a
withMetaInfo' MetaVariable
mv TCM a
ret

-- | 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 -> TCMT IO Names
introTactic Bool
pmLambda InteractionId
ii = do
  MetaId
mi <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
  MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi
  Closure Range -> TCMT IO Names -> TCMT IO Names
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCMT IO Names -> TCMT IO Names) -> TCMT IO Names -> TCMT IO Names
forall a b. (a -> b) -> a -> b
$ case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
    HasType MetaId
_ Comparison
_ Type
t -> do
        Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> Args -> TCMT IO Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
piApplyM Type
t (Args -> TCMT IO Type) -> TCMT IO Args -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Args
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 <- VerboseLevel -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
VerboseLevel -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-VerboseLevel
1) Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
        -- if we cannot introduce a constructor, we try a lambda
        let fallback :: TCMT IO Names
fallback = do
              Bool
cubical <- PragmaOptions -> Bool
optCubical (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
              TelV Telescope
tel Type
_ <- (if Bool
cubical then Type -> TCMT IO (TelV Type)
telViewPath else Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView) Type
t
              String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.intro" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TP.sep
                [ TCM Doc
"introTactic/fallback"
                , TCM Doc
"tel' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel'
                , TCM Doc
"tel  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
                ]
              case (Telescope
tel', Telescope
tel) of
                (Telescope
EmptyTel, Telescope
EmptyTel) -> Names -> TCMT IO Names
forall (m :: * -> *) a. Monad m => a -> m a
return []
                (Telescope, Telescope)
_ -> ListTel -> TCMT IO Names
introFun (Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel' ListTel -> ListTel -> ListTel
forall a. [a] -> [a] -> [a]
++ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel)

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

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

    introFun :: ListTel -> TCM [String]
    introFun :: ListTel -> TCMT IO Names
introFun ListTel
tel = Telescope -> TCMT IO Names -> TCMT IO Names
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel' (TCMT IO Names -> TCMT IO Names) -> TCMT IO Names -> TCMT IO Names
forall a b. (a -> b) -> a -> b
$ do
        String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.intro" VerboseLevel
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do TCM Doc
"introFun" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (ListTel -> Telescope
telFromList ListTel
tel)
        Bool
imp <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
        let okHiding0 :: Hiding -> Bool
okHiding0 Hiding
h = Bool
imp Bool -> Bool -> Bool
|| Hiding
h Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
NotHidden
            -- if none of the vars were displayed, we would get a parse error
            -- thus, we switch to displaying all
            allHidden :: Bool
allHidden   = [Hiding] -> Bool
forall a. Null a => a -> Bool
null ((Hiding -> Bool) -> [Hiding] -> [Hiding]
forall a. (a -> Bool) -> [a] -> [a]
filter Hiding -> Bool
okHiding0 [Hiding]
hs)
            okHiding :: Hiding -> Bool
okHiding    = if Bool
allHidden then Bool -> Hiding -> Bool
forall a b. a -> b -> a
const Bool
True else Hiding -> Bool
okHiding0
        Names
vars <- -- setShowImplicitArguments (imp || allHidden) $
                (if Bool
allHidden then TCMT IO Names -> TCMT IO Names
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withShowAllArguments else TCMT IO Names -> TCMT IO Names
forall a. a -> a
id) (TCMT IO Names -> TCMT IO Names) -> TCMT IO Names -> TCMT IO Names
forall a b. (a -> b) -> a -> b
$
                  (Arg Term -> TCM String) -> Args -> TCMT IO Names
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Arg Term -> TCM String
forall a. PrettyTCM a => a -> TCM String
showTCM [ Hiding -> Arg Term -> Arg Term
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h (Arg Term -> Arg Term) -> Arg Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Term
var VerboseLevel
i :: Arg Term
                               | (Hiding
h, VerboseLevel
i) <- [Hiding] -> [VerboseLevel] -> [(Hiding, VerboseLevel)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Hiding]
hs ([VerboseLevel] -> [(Hiding, VerboseLevel)])
-> [VerboseLevel] -> [(Hiding, VerboseLevel)]
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
n
                               , Hiding -> Bool
okHiding Hiding
h
                               ]
        if Bool
pmLambda
           then Names -> TCMT IO Names
forall (m :: * -> *) a. Monad m => a -> m a
return [ Names -> String
unwords (Names -> String) -> Names -> String
forall a b. (a -> b) -> a -> b
$ [String
"λ", String
"{"] Names -> Names -> Names
forall a. [a] -> [a] -> [a]
++ Names
vars Names -> Names -> Names
forall a. [a] -> [a] -> [a]
++ [String
"→", String
"?", String
"}"] ]
           else Names -> TCMT IO Names
forall (m :: * -> *) a. Monad m => a -> m a
return [ Names -> String
unwords (Names -> String) -> Names -> String
forall a b. (a -> b) -> a -> b
$ [String
"λ"]      Names -> Names -> Names
forall a. [a] -> [a] -> [a]
++ Names
vars Names -> Names -> Names
forall a. [a] -> [a] -> [a]
++ [String
"→", String
"?"] ]
      where
        n :: VerboseLevel
n = ListTel -> VerboseLevel
forall a. Sized a => a -> VerboseLevel
size ListTel
tel
        hs :: [Hiding]
hs   = (Dom' Term (String, Type) -> Hiding) -> ListTel -> [Hiding]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (String, Type) -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ListTel
tel
        tel' :: Telescope
tel' = ListTel -> Telescope
telFromList [ ((String, Type) -> (String, Type))
-> Dom' Term (String, Type) -> Dom' Term (String, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String, Type) -> (String, Type)
forall a b. (Eq a, IsString a) => (a, b) -> (a, b)
makeName Dom' Term (String, Type)
b | Dom' Term (String, 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 -> TCMT IO Names
introData Type
t = do
      let tel :: Telescope
tel  = ListTel -> Telescope
telFromList [(String, Type) -> Dom' Term (String, Type)
forall a. a -> Dom a
defaultDom (String
"_", Type
t)]
          pat :: [Arg (Named name DeBruijnPattern)]
pat  = [Named name DeBruijnPattern -> Arg (Named name DeBruijnPattern)
forall a. a -> Arg a
defaultArg (Named name DeBruijnPattern -> Arg (Named name DeBruijnPattern))
-> Named name DeBruijnPattern -> Arg (Named name DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ DeBruijnPattern -> Named name DeBruijnPattern
forall a name. a -> Named name a
unnamed (DeBruijnPattern -> Named name DeBruijnPattern)
-> DeBruijnPattern -> Named name DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ String -> VerboseLevel -> DeBruijnPattern
forall a. DeBruijn a => String -> VerboseLevel -> a
debruijnNamedVar String
"c" VerboseLevel
0]
      Either SplitError Covering
r <- Induction
-> Telescope
-> [NamedArg DeBruijnPattern]
-> TCM (Either SplitError Covering)
splitLast Induction
CoInductive Telescope
tel [NamedArg DeBruijnPattern]
forall name. [Arg (Named name DeBruijnPattern)]
pat
      case Either SplitError Covering
r of
        Left SplitError
err -> Names -> TCMT IO Names
forall (m :: * -> *) a. Monad m => a -> m a
return []
        Right Covering
cov -> (ConHead -> TCM String) -> [ConHead] -> TCMT IO Names
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ConHead -> TCM String
forall a. PrettyTCM a => a -> TCM String
showTCM ([ConHead] -> TCMT IO Names) -> [ConHead] -> TCMT IO Names
forall a b. (a -> b) -> a -> b
$ (SplitClause -> [ConHead]) -> [SplitClause] -> [ConHead]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([NamedArg SplitPattern] -> [ConHead]
conName ([NamedArg SplitPattern] -> [ConHead])
-> (SplitClause -> [NamedArg SplitPattern])
-> SplitClause
-> [ConHead]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitClause -> [NamedArg SplitPattern]
scPats) ([SplitClause] -> [ConHead]) -> [SplitClause] -> [ConHead]
forall a b. (a -> b) -> a -> b
$ Covering -> [SplitClause]
splitClauses Covering
cov

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

-- | Parse a name.
parseName :: Range -> String -> TCM C.QName
parseName :: Range -> String -> TCM QName
parseName Range
r String
s = do
  Expr
m <- Range -> String -> TCM Expr
parseExpr Range
r String
s
  case Expr
m of
    C.Ident QName
m              -> QName -> TCM QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
    C.RawApp Range
_ [C.Ident QName
m] -> QName -> TCM QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
    Expr
_                      -> TypeError -> TCM QName
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM QName) -> TypeError -> TCM QName
forall a b. (a -> b) -> a -> b
$
      String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ String
"Not an identifier: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."

-- | Check whether an expression is a (qualified) identifier.
isQName :: C.Expr -> Maybe C.QName
isQName :: Expr -> Maybe QName
isQName Expr
m = do
  case Expr
m of
    C.Ident QName
m              -> QName -> Maybe QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
    C.RawApp Range
_ [C.Ident QName
m] -> QName -> Maybe QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
    Expr
_ -> Maybe 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, Type)])
     -- ^ Module names,
     --   context extension needed to print types,
     --   names paired up with corresponding types.

moduleContents :: Rewrite
-> Range -> String -> TCM ([Name], Telescope, [(Name, Type)])
moduleContents Rewrite
norm Range
rng String
s = Call
-> TCM ([Name], Telescope, [(Name, Type)])
-> TCM ([Name], Telescope, [(Name, Type)])
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall Call
ModuleContents (TCM ([Name], Telescope, [(Name, Type)])
 -> TCM ([Name], Telescope, [(Name, Type)]))
-> TCM ([Name], Telescope, [(Name, Type)])
-> TCM ([Name], Telescope, [(Name, Type)])
forall a b. (a -> b) -> a -> b
$ do
  Expr
e <- Range -> String -> TCM Expr
parseExpr Range
rng String
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] <- QName -> ScopeInfo -> [AbstractModule]
forall a. InScope a => QName -> ScopeInfo -> [a]
scopeLookup QName
x (ScopeInfo -> [AbstractModule])
-> TCMT IO ScopeInfo -> TCMT IO [AbstractModule]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
      if [AbstractModule] -> Bool
forall a. Null a => a -> Bool
null [AbstractModule]
ms then Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
getRecordContents Rewrite
norm Expr
e else Rewrite -> QName -> TCM ([Name], Telescope, [(Name, Type)])
getModuleContents Rewrite
norm 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, 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 <- Expr -> TCM Expr
forall concrete abstract.
ToAbstract concrete abstract =>
concrete -> ScopeM abstract
toAbstract Expr
ce
  (Term
_, Type
t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
  let notRecordType :: TCMT IO a
notRecordType = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
t
  (QName
q, Args
vs, Defn
defn) <- TCMT IO (QName, Args, Defn)
-> TCMT IO (Maybe (QName, Args, Defn))
-> TCMT IO (QName, Args, Defn)
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM TCMT IO (QName, Args, Defn)
forall a. TCMT IO a
notRecordType (TCMT IO (Maybe (QName, Args, Defn))
 -> TCMT IO (QName, Args, Defn))
-> TCMT IO (Maybe (QName, Args, Defn))
-> TCMT IO (QName, Args, Defn)
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (Maybe (QName, Args, Defn))
forall (m :: * -> *).
(MonadReduce m, HasConstInfo m, HasBuiltins 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   = (Dom QName -> Name) -> [Dom QName] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
nameConcrete (Name -> Name) -> (Dom QName -> Name) -> Dom QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName (QName -> Name) -> (Dom QName -> QName) -> Dom QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom QName -> QName
forall t e. Dom' t e -> e
unDom) [Dom QName]
fs
          tel :: Telescope
tel  = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
rtel Args
vs
          doms :: [Dom Type]
doms = Telescope -> [Dom Type]
forall a. Subst Term a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel
      -- Andreas, 2019-04-10, issue #3687: use flattenTel
      -- to bring types into correct scope.
      String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"interaction.contents.record" VerboseLevel
20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TP.vcat
        [ TCM Doc
"getRecordContents"
        , TCM Doc
"  cxt  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> (Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Telescope -> TCM Doc) -> TCMT IO Telescope -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
        , TCM Doc
"  tel  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Telescope -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Telescope
tel
        , TCM Doc
"  doms = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> [Dom Type] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Dom Type]
doms
        , TCM Doc
"  doms'= " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> (Telescope -> TCM Doc -> TCM Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Dom Type] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Dom Type]
doms)
        ]
      [Type]
ts <- (Dom Type -> TCMT IO Type) -> [Dom Type] -> TCMT IO [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Rewrite -> Type -> TCMT IO Type
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm (Type -> TCMT IO Type)
-> (Dom Type -> Type) -> Dom Type -> TCMT IO Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Type
forall t e. Dom' t e -> e
unDom) [Dom Type]
doms
      ([Name], Telescope, [(Name, Type)])
-> TCM ([Name], Telescope, [(Name, Type)])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Telescope
tel, [Name] -> [Type] -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs [Type]
ts)
    Defn
_ -> TCM ([Name], Telescope, [(Name, Type)])
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Returns the contents of the given module.

getModuleContents
  :: Rewrite  -- ^ Amount of normalization in types.
  -> C.QName  -- ^ Module name.
  -> TCM ([C.Name], I.Telescope, [(C.Name, Type)])
              -- ^ Module names,
              --   context extension,
              --   names paired up with corresponding types.
getModuleContents :: Rewrite -> QName -> TCM ([Name], Telescope, [(Name, Type)])
getModuleContents Rewrite
norm QName
m = do
  Scope
modScope <- ModuleName -> ScopeM Scope
getNamedScope (ModuleName -> ScopeM Scope)
-> (AbstractModule -> ModuleName) -> AbstractModule -> ScopeM Scope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractModule -> ModuleName
amodName (AbstractModule -> ScopeM Scope)
-> TCMT IO AbstractModule -> ScopeM Scope
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO AbstractModule
resolveModule QName
m
  let modules :: ThingsInScope AbstractModule
      modules :: ThingsInScope AbstractModule
modules = Scope -> ThingsInScope AbstractModule
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
      names :: ThingsInScope AbstractName
      names :: ThingsInScope AbstractName
names = Scope -> ThingsInScope AbstractName
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
      xns :: [(Name, AbstractName)]
xns = [ (Name
x,AbstractName
n) | (Name
x, [AbstractName]
ns) <- ThingsInScope AbstractName -> [(Name, [AbstractName])]
forall k a. Map k a -> [(k, a)]
Map.toList ThingsInScope AbstractName
names, AbstractName
n <- [AbstractName]
ns ]
  [(Name, Type)]
types <- [(Name, AbstractName)]
-> ((Name, AbstractName) -> TCMT IO (Name, Type))
-> TCMT IO [(Name, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, AbstractName)]
xns (((Name, AbstractName) -> TCMT IO (Name, Type))
 -> TCMT IO [(Name, Type)])
-> ((Name, AbstractName) -> TCMT IO (Name, Type))
-> TCMT IO [(Name, Type)]
forall a b. (a -> b) -> a -> b
$ \(Name
x, AbstractName
n) -> do
    Definition
d <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (QName -> TCMT IO Definition) -> QName -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
n
    Type
t <- Rewrite -> Type -> TCMT IO Type
forall t.
(Reduce t, Simplify t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm (Type -> TCMT IO Type) -> TCMT IO Type -> TCMT IO Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Definition -> Type
defType (Definition -> Type) -> TCMT IO Definition -> TCMT IO Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Definition -> TCMT IO Definition
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef Definition
d)
    (Name, Type) -> TCMT IO (Name, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x, Type
t)
  ([Name], Telescope, [(Name, Type)])
-> TCM ([Name], Telescope, [(Name, Type)])
forall (m :: * -> *) a. Monad m => a -> m a
return (ThingsInScope AbstractModule -> [Name]
forall k a. Map k a -> [k]
Map.keys ThingsInScope AbstractModule
modules, Telescope
forall a. Tele a
EmptyTel, [(Name, Type)]
types)


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