{-# 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
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
parseExpr :: Range -> String -> TCM C.Expr
parseExpr :: Range -> String -> TCM Expr
parseExpr rng :: Range
rng s :: String
s = do
C.ExprWhere e :: Expr
e wh :: 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
$
"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 ii :: InteractionId
ii rng :: Range
rng s :: 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
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 ()
giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCMT IO ()
giveExpr force :: UseForce
force mii :: Maybe InteractionId
mii mi :: MetaId
mi e :: Expr
e = do
MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi
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 _ _ t :: Type
t -> Type
t
String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "interaction.give" 20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
"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
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 "interaction.give" 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 ("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]
++ "): 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 xs :: [Arg String]
xs v' :: 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 "interaction.give" 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
[ "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.<+> " 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)
, "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
, "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)
]
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__
let (_xs1 :: [Arg String]
_xs1, xs2 :: [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 "interaction.give" 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
[ "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'
_ -> do
String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn "interaction.give" 20 "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 "interaction.give" 20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "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
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
String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "interaction.give" 20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "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'
redoChecks :: Maybe InteractionId -> TCM ()
redoChecks :: Maybe InteractionId -> TCMT IO ()
redoChecks Nothing = () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
redoChecks (Just ii :: InteractionId
ii) = do
String -> VerboseLevel -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn "interaction.give" 20 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
"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
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 (\ e :: 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
give
:: UseForce
-> InteractionId
-> Maybe Range
-> Expr
-> TCM Expr
give :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give force :: UseForce
force ii :: InteractionId
ii mr :: Maybe Range
mr e :: 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
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 "interaction.give" 10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "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 "interaction.give" 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
do MetaId -> RunMetaOccursCheck -> TCMT IO ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> RunMetaOccursCheck -> m ()
setMetaOccursCheck MetaId
mi RunMetaOccursCheck
DontRunMetaOccursCheck
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
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
$ "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
err :: 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
refine
:: UseForce
-> InteractionId
-> Maybe Range
-> Expr
-> TCM Expr
refine :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
refine force :: UseForce
force ii :: InteractionId
ii mr :: Maybe Range
mr e :: 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 "interaction.refine" 10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
"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 "interaction.refine" 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
VerboseLevel -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine 10 Range
range ScopeInfo
scope Expr
e
where
tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine :: VerboseLevel -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine nrOfMetas :: VerboseLevel
nrOfMetas r :: Range
r scope :: ScopeInfo
scope e :: Expr
e = VerboseLevel -> Expr -> TCM Expr
try VerboseLevel
nrOfMetas Expr
e
where
try :: Int -> Expr -> TCM Expr
try :: VerboseLevel -> Expr -> TCM Expr
try 0 e :: 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 "Cannot refine"
try n :: VerboseLevel
n e :: 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` (\_ -> VerboseLevel -> Expr -> TCM Expr
try (VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 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)
appMeta :: Expr -> TCM Expr
appMeta :: Expr -> TCM Expr
appMeta e :: Expr
e = do
let rng :: Range
rng = Range -> Range
rightMargin Range
r
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
, metaNumber :: Maybe MetaId
metaNumber = Maybe MetaId
forall a. Maybe a
Nothing
, metaNameSuggestion :: String
metaNameSuggestion = ""
}
metaVar :: Expr
metaVar = MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
info InteractionId
ii
count :: Name -> a -> a
count x :: Name
x e :: 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 y :: 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 1
isX _ = Sum a
forall a. Monoid a => a
mempty
lamView :: Expr -> Maybe (Binder, Expr)
lamView (A.Lam _ (DomainFree _ x :: NamedArg Binder
x) e :: 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 i :: ExprInfo
i (DomainFull (TBind r :: Range
r t :: TacticAttr
t (x :: NamedArg Binder
x : xs :: [NamedArg Binder]
xs) a :: Expr
a)) e :: 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 _ = Maybe (Binder, Expr)
forall a. Maybe a
Nothing
smartApp :: AppInfo -> Expr -> NamedArg Expr -> Expr
smartApp i :: AppInfo
i e :: Expr
e arg :: 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}, e :: 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
< 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 y :: 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 e :: Expr
e = Expr
e
_ -> 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
evalInCurrent :: Expr -> TCM Expr
evalInCurrent :: Expr -> TCM Expr
evalInCurrent e :: Expr
e =
do (v :: Term
v, t :: Type
t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
Term
v' <- 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 ii :: InteractionId
ii e :: 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
normalForm :: (Reduce t, Simplify t, Normalise t) => Rewrite -> t -> TCM t
normalForm :: Rewrite -> t -> TCM t
normalForm AsIs t :: t
t = t -> TCM t
forall (m :: * -> *) a. Monad m => a -> m a
return t
t
normalForm Instantiated t :: t
t = t -> TCM t
forall (m :: * -> *) a. Monad m => a -> m a
return t
t
normalForm HeadNormal t :: t
t = t -> TCM t
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce t
t
normalForm Simplified t :: t
t = t -> TCM t
forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify t
t
normalForm Normalised t :: t
t = t -> TCM t
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise t
t
computeIgnoreAbstract :: ComputeMode -> Bool
computeIgnoreAbstract :: ComputeMode -> Bool
computeIgnoreAbstract DefaultCompute = Bool
False
computeIgnoreAbstract IgnoreAbstract = Bool
True
computeIgnoreAbstract UseShowInstance = Bool
True
computeWrapInput :: ComputeMode -> String -> String
computeWrapInput :: ComputeMode -> String -> String
computeWrapInput UseShowInstance s :: String
s = "show (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
computeWrapInput _ s :: String
s = String
s
showComputed :: ComputeMode -> Expr -> TCM Doc
showComputed :: ComputeMode -> Expr -> TCM Doc
showComputed UseShowInstance e :: Expr
e =
case Expr
e of
A.Lit (LitString _ s :: String
s) -> Doc -> TCM Doc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Doc
text String
s)
_ -> ("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 _ e :: Expr
e = Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
outputFormId :: OutputForm a b -> b
outputFormId :: OutputForm a b -> b
outputFormId (OutputForm _ _ o :: 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 o :: OutputConstraint a p
o = case OutputConstraint a p
o of
OfType i :: p
i _ -> p
i
CmpInType _ _ i :: p
i _ -> p
i
CmpElim _ _ (i :: p
i:_) _ -> p
i
CmpElim _ _ [] _ -> p
forall a. HasCallStack => a
__IMPOSSIBLE__
JustType i :: p
i -> p
i
CmpLevels _ i :: p
i _ -> p
i
CmpTypes _ i :: p
i _ -> p
i
CmpTeles _ i :: p
i _ -> p
i
JustSort i :: p
i -> p
i
CmpSorts _ i :: p
i _ -> p
i
Guard o :: OutputConstraint a p
o _ -> OutputConstraint a p -> p
out OutputConstraint a p
o
Assign i :: p
i _ -> p
i
TypedAssign i :: p
i _ _ -> p
i
PostponedCheckArgs i :: p
i _ _ _ -> p
i
IsEmptyType _ -> p
forall a. HasCallStack => a
__IMPOSSIBLE__
SizeLtSat{} -> p
forall a. HasCallStack => a
__IMPOSSIBLE__
FindInstanceOF _ _ _ -> p
forall a. HasCallStack => a
__IMPOSSIBLE__
PTSInstance i :: p
i _ -> 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 pids :: Set ProblemId
pids cl :: 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
$ \ c :: 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 e :: Elim
e = case Elim
e of
I.IApply _ _ v :: Term
v -> String -> Arg Expr -> Expr
appl "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)
I.Apply v :: Arg Term
v -> String -> Arg Expr -> Expr
appl "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 _o :: ProjOrigin
_o f :: QName
f -> String -> Arg Expr -> Expr
appl "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 s :: String
s v :: 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 cmp :: Comparison
cmp (AsTermsOf t :: Type
t) u :: Term
u v :: 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 cmp :: Comparison
cmp AsSizes u :: Term
u v :: 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 cmp :: Comparison
cmp AsTypes u :: Term
u v :: 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 cmp :: Comparison
cmp p :: Term
p t :: Type
t u :: Term
u v :: 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 "_"
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' "o" NamesT m Term
p (\ o :: NamesT m Term
o -> NamesT m Type
t)
reify (ElimCmp cmp :: [Polarity]
cmp _ t :: Type
t v :: Term
v es1 :: Elims
es1 es2 :: 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 cmp :: Comparison
cmp t :: Level
t 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 a :: Type
a b :: Type
b cmp :: Comparison
cmp t :: Telescope
t 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 cmp :: Comparison
cmp s :: Sort
s 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 c :: Constraint
c pid :: 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 _ tac :: Term
tac _ goal :: 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 m :: 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 t :: 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 cl :: Closure TypeCheckingProblem
cl _ -> 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 cmp :: Comparison
cmp e :: Expr
e a :: 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 cmp :: Comparison
cmp (Arg ai :: ArgInfo
ai (xs :: [WithHiding Name]
xs, mt :: Maybe Type
mt)) body :: Expr
body target :: 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 h :: Hiding
h x :: 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 _ _ args :: [NamedArg Expr]
args t0 :: Type
t0 t1 :: Type
t1 _ -> 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 cmp :: Comparison
cmp e :: Expr
e _ _ _ t :: Type
t _ _ _ -> 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 cmp :: Comparison
cmp v :: Term
v t :: 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 m :: MetaId
m _b :: Maybe MetaId
_b mcands :: 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 tm :: Term
tm ty :: Type
ty _) -> 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 r :: Range
r a :: 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 a :: 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 d :: Delayed
d i :: DefInfo
i q :: QName
q cs :: [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 a :: 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 a :: Dom Type
a b :: Abs Sort
b) = do
(a :: Expr
a,(x :: Name
x,b :: 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 m :: 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 r :: Range
r pids :: [ProblemId]
pids c :: 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 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 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 [pid :: a
pid] = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "problem" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
pid
prPids pids :: [a]
pids = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "problems" Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate "," ([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 r :: 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
$ " [ at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " ]"
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 oc :: OutputConstraint a b
oc =
case OutputConstraint a b
oc of
OfType e :: b
e t :: 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 e :: b
e -> "Type" Doc -> Doc -> Doc
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e
JustSort e :: b
e -> "Sort" Doc -> Doc -> Doc
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e
CmpInType cmp :: Comparison
cmp t :: a
t e :: b
e 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 cmp :: [Polarity]
cmp t :: a
t e :: [b]
e 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 cmp :: Comparison
cmp t :: b
t 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 cmp :: Comparison
cmp t :: b
t 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 cmp :: Comparison
cmp t :: b
t 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 cmp :: Comparison
cmp s :: b
s 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 o :: OutputConstraint a b
o pid :: ProblemId
pid -> OutputConstraint a b -> Doc
forall a. Pretty a => a -> Doc
pretty OutputConstraint a b
o Doc -> Doc -> Doc
<?> Doc -> Doc
parens ("blocked by problem" Doc -> Doc -> Doc
<+> ProblemId -> Doc
forall a. Pretty a => a -> Doc
pretty ProblemId
pid)
Assign m :: b
m e :: a
e -> Doc -> Doc -> Doc -> Doc
bin (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
m) ":=" (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e)
TypedAssign m :: b
m e :: a
e a :: a
a -> Doc -> Doc -> Doc -> Doc
bin (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
m) ":=" (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) ":?" (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a)
PostponedCheckArgs m :: b
m es :: [a]
es t0 :: a
t0 t1 :: a
t1 ->
Doc -> Doc -> Doc -> Doc
bin (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
m) ":=" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc -> Doc
parens ("_" 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 d :: 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` [' ', '\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
a -> "Is empty:" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
SizeLtSat a :: a
a -> "Not empty type of sizes:" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
FindInstanceOF s :: b
s t :: a
t cs :: [(a, a)]
cs -> [Doc] -> Doc
vcat
[ "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 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ "Candidate:"
, VerboseLevel -> Doc -> Doc
nest 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 | (v :: a
v, t :: a
t) <- [(a, a)]
cs ] ]
PTSInstance a :: b
a b :: b
b -> "PTS instance for" Doc -> Doc -> Doc
<+> (b, b) -> Doc
forall a. Pretty a => a -> Doc
pretty (b
a, b
b)
PostponedCheckFunDef q :: QName
q a :: a
a -> "Check definition of" Doc -> Doc -> Doc
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> Doc
<+> ":" Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
where
bin :: Doc -> Doc -> Doc -> Doc
bin a :: Doc
a op :: Doc
op b :: Doc
b = [Doc] -> Doc
sep [Doc
a, VerboseLevel -> Doc -> Doc
nest 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 cmp :: a
cmp a :: a
a b :: 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)
val :: Doc
val .: :: Doc -> a -> Doc
.: ty :: a
ty = Doc -> Doc -> Doc -> Doc
bin Doc
val ":" (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 r :: Range
r pid :: [ProblemId]
pid c :: 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 e :: b
e t :: 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 e :: 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 e :: 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 cmp :: Comparison
cmp t :: a
t e :: b
e 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 cmp :: [Polarity]
cmp t :: a
t e :: [b]
e 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 cmp :: Comparison
cmp e :: b
e 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 cmp :: Comparison
cmp e :: b
e 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 cmp :: Comparison
cmp e :: b
e 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 cmp :: Comparison
cmp e :: b
e 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 o :: OutputConstraint a b
o pid :: 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 m :: b
m e :: 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 m :: b
m e :: a
e a :: 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 m :: b
m args :: [a]
args t0 :: a
t0 t1 :: 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
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
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 s :: b
s t :: a
t cs :: [(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 (\(tm :: a
tm,ty :: 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 a :: b
a b :: 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 q :: QName
q a :: 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' e :: b
e t :: a
t) = b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e 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' e :: b
e t :: 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 eqs :: [(c, c)]
eqs val :: c
val meta :: c
meta over :: Overapplied
over) = do
let
xs :: [Doc]
xs = ((c, c) -> Doc) -> [(c, c)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (l :: c
l,r :: c
r) -> c -> Doc
forall a. Pretty a => a -> Doc
pretty c
l 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 -> "=" Doc -> Doc -> Doc
<+> c -> Doc
forall a. Pretty a => a -> Doc
pretty c
meta
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
<+> 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 cs :: [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
$ \ c :: 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 i :: a
i _) = a
i
namedMetaOf (JustType i :: a
i) = a
i
namedMetaOf (JustSort i :: a
i) = a
i
namedMetaOf (Assign i :: a
i _) = a
i
namedMetaOf _ = a
forall a. HasCallStack => a
__IMPOSSIBLE__
getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm C.Expr C.Expr]
getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm Expr Expr]
getConstraintsMentioning norm :: Rewrite
norm m :: 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)
where
instantiateBlockingFull :: b -> m b
instantiateBlockingFull p :: 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
hasHeadMeta :: Constraint -> Maybe Elims
hasHeadMeta c :: Constraint
c =
case Constraint
c of
ValueCmp _ _ u :: Term
u v :: 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 cmp :: Comparison
cmp p :: Term
p t :: Type
t u :: Term
u v :: 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
ElimCmp cmp :: [Polarity]
cmp fs :: [IsForced]
fs t :: Type
t v :: Term
v as :: Elims
as bs :: Elims
bs -> Maybe Elims
forall a. Maybe a
Nothing
LevelCmp cmp :: Comparison
cmp u :: Level
u v :: Level
v -> Maybe Elims
forall a. Maybe a
Nothing
TelCmp a :: Type
a b :: Type
b cmp :: Comparison
cmp tela :: Telescope
tela telb :: Telescope
telb -> Maybe Elims
forall a. Maybe a
Nothing
SortCmp cmp :: Comparison
cmp a :: Sort
a b :: Sort
b -> Maybe Elims
forall a. Maybe a
Nothing
Guarded c :: Constraint
c pid :: 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 r :: Range
r t :: Type
t -> Term -> Maybe Elims
isMeta (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t)
CheckSizeLtSat t :: Term
t -> Term -> Maybe Elims
isMeta Term
t
CheckFunDef{} -> Maybe Elims
forall a. Maybe a
Nothing
HasBiggerSort a :: Sort
a -> Maybe Elims
forall a. Maybe a
Nothing
HasPTSRule a :: Dom Type
a b :: 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 m' :: MetaId
m' es_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 _ = Maybe Elims
forall a. Maybe a
Nothing
getConstrs :: (ProblemConstraint -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> tcm [OutputForm Expr Expr]
getConstrs g :: ProblemConstraint -> TCM ProblemConstraint
g f :: 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 "constr.ment" 20 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "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 s :: Set ProblemId
s c :: 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 as_m :: Args
as_m -> do
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
$ \ eqs :: [(Term, Term)]
eqs c :: 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
_ -> 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_
stripConstraintPids :: Constraints -> Constraints
stripConstraintPids :: Constraints -> Constraints
stripConstraintPids cs :: 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 pids :: Set ProblemId
pids c :: 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 c :: Constraint
c pid :: ProblemId
pid) = ProblemId
pid ProblemId -> [ProblemId] -> [ProblemId]
forall a. a -> [a] -> [a]
: Constraint -> [ProblemId]
blocking Constraint
c
blocking _ = []
getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm C.Expr C.Expr]
getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getConstraints' g :: ProblemConstraint -> TCM ProblemConstraint
g f :: 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
$ \c :: 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
[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 (ii :: InteractionId
ii, mi :: MetaId
mi, e :: 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 norm :: Rewrite
norm ii :: 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
$ \ cl :: 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
$ \ 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
IPNoClause -> [IPBoundary' Expr] -> TCM [IPBoundary' Expr]
forall (m :: * -> *) a. Monad m => a -> m a
return []
getGoals :: TCM Goals
getGoals :: TCM Goals
getGoals = do
[OutputConstraint Expr InteractionId]
visibleMetas <- Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas Rewrite
AsIs
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)
showGoals :: Goals -> TCM String
showGoals :: Goals -> TCM String
showGoals (ims :: [OutputConstraint Expr InteractionId]
ims, hms :: [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
$ \ i :: 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' m :: 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]
++ " [ 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]
++ " ]"
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] -> WarningsAndNonFatalErrors
classifyWarnings [TCWarning]
ws
_ -> WarningsAndNonFatalErrors
emptyWarningsAndNonFatalErrors
getResponseContext
:: Rewrite
-> InteractionId
-> TCM [ResponseContextEntry]
getResponseContext :: Rewrite -> InteractionId -> TCM [ResponseContextEntry]
getResponseContext norm :: Rewrite
norm ii :: InteractionId
ii = InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta InteractionId
ii Rewrite
norm
getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints :: Bool -> Rewrite -> TCMT IO [(InteractionId, MetaId, Expr)]
getSolvedInteractionPoints all :: Bool
all norm :: 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 (i :: a
i, m :: 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 v :: Term
v = do
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; _ -> 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 norm :: Rewrite
norm mi :: 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 mv :: MetaVariable
mv (HasType i :: MetaId
i cmp :: Comparison
cmp t :: Type
t) = do
String
ms <- MetaId -> TCM String
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m String
getMetaNameSuggestion MetaId
i
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 "interactive.meta" 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 ["permuting", MetaId -> String
forall a. Show a => a -> String
show MetaId
i, "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 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
[ "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)
, "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
, "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
, "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 "interactive.meta.scope" 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
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 mv :: MetaVariable
mv (IsSort i :: MetaId
i t :: 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 norm :: Rewrite
norm ii :: 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' norm :: Rewrite
norm (ii :: InteractionId
ii, mi :: MetaId
mi) = (NamedMeta -> InteractionId)
-> OutputConstraint Expr NamedMeta
-> OutputConstraint Expr InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\_ -> 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 norm :: 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 norm :: 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 is :: t a
is x :: a
x m :: MetaVariable
m | Maybe MetaId -> Bool
forall a. Maybe a -> Bool
isJust (MetaVariable -> Maybe MetaId
mvTwin MetaVariable
m) = Bool
False
openAndImplicit is :: t a
is x :: a
x m :: MetaVariable
m =
case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
m of
M.InstV{} -> Bool
False
M.Open -> a
x a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t a
is
M.OpenInstance -> a
x a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t a
is
M.BlockedConst{} -> Bool
False
M.PostponedTypeCheckingProblem{} -> Bool
False
metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr)
metaHelperType :: Rewrite
-> InteractionId
-> Range
-> String
-> TCM (OutputConstraint' Expr Expr)
metaHelperType norm :: Rewrite
norm ii :: InteractionId
ii rng :: Range
rng s :: String
s = case String -> Names
words String
s of
[] -> TCM (OutputConstraint' Expr Expr)
forall a. TCMT IO a
failure
f :: String
f : _ -> 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 h :: Expr
h args :: [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 ("let " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = _ 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
>>= \ xs :: [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
Just xs :: [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 :: 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
(TCEnv -> TCEnv) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\e :: 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
Nothing -> do
Args
cxtArgs <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
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 (\ a :: 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
TelV atel :: Telescope
atel _ <- 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
(delta1 :: Telescope
delta1, delta2 :: Telescope
delta2, _, a' :: Type
a', vtys' :: [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 (\e :: 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 "interaction.helper" 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 a :: Type
a -> Type
a; _ -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__ } in
let (vs :: [Term]
vs, as :: [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 (vs' :: [Term]
vs', as' :: [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
[ "generating helper function"
, VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TP.nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "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
$ "Expected an argument of the form f e1 e2 .. en"
ensureName :: String -> TCMT IO ()
ensureName f :: 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) (\ _ -> () -> 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 "interaction.helper" 10 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ "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 x :: Name
x) -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
C.RawApp _ [C.Ident (C.QName x :: Name
x)] -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
_ -> Maybe Name
forall a. Maybe a
Nothing
isVar :: A.Expr -> Maybe A.Name
isVar :: Expr -> Maybe Name
isVar = \case
A.Var x :: Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
_ -> Maybe Name
forall a. Maybe a
Nothing
cleanupType :: VerboseLevel -> [NamedArg Expr] -> Type -> m Type
cleanupType arity :: VerboseLevel
arity args :: [NamedArg Expr]
args t :: Type
t = do
TelV ttel :: Telescope
ttel _ <- Type -> m (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
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
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
>= 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 _ _ e :: Expr
e) = Expr
e
getBody _ = Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
stripUnused :: a -> Type -> Type
stripUnused n :: a
n (El s :: Sort
s v :: 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 0 v :: Term
v = Term
v
strip n :: a
n v :: Term
v = case Term
v of
I.Pi a :: Dom Type
a b :: Abs Type
b -> case a -> Type -> Type
stripUnused (a
na -> a -> a
forall a. Num 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
b :: 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
== "w" -> Dom Type -> Abs Type -> Term
I.Pi Dom Type
a Abs Type
b
NoAbs _ b :: Type
b -> Type -> Term
forall t a. Type'' t a -> a
unEl Type
b
Abs s :: String
s b :: Type
b | 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
v
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 => (String -> m String) -> Type -> m Type
onNames :: (String -> m String) -> Type -> m Type
onNames f :: String -> m String
f (El s :: Sort
s v :: 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 => (String -> f String) -> I.Telescope -> f I.Telescope
onNamesTel :: (String -> f String) -> Telescope -> f Telescope
onNamesTel f :: String -> f String
f I.EmptyTel = Telescope -> f Telescope
forall (f :: * -> *) a. Applicative f => a -> f a
pure Telescope
forall a. Tele a
I.EmptyTel
onNamesTel f :: String -> f String
f (I.ExtendTel a :: Dom Type
a b :: 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 f :: String -> f String
f v :: Term
v = case Term
v of
I.Var x :: VerboseLevel
x es :: 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 q :: QName
q es :: 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 c :: ConHead
c ci :: ConInfo
ci args :: 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 i :: ArgInfo
i b :: 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 a :: Dom Type
a b :: 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 v :: 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 f :: 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 f :: 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 f :: 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' f :: t
f f' :: String -> f String
f' nd :: t -> t -> f a
nd (Abs s :: String
s x :: 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' f :: t
f f' :: String -> f String
f' nd :: t -> t -> f a
nd (NoAbs s :: String
s x :: 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 "w" = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ".w"
unW s :: a
s = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
s
renameVar :: String -> StateT [NamedArg Expr] Identity String
renameVar "w" = StateT [NamedArg Expr] Identity String
betterName
renameVar s :: 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__
arg :: NamedArg Expr
arg : args :: [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 _ (Named _ (A.Var x :: 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 x :: 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 -> "w"
contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta ii :: InteractionId
ii norm :: 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
[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 [1..] [Dom' Term (Name, Type)]
cxt
[(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
[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
name, t :: 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
name, lb :: Open (Term, Dom Type)
lb) = do
(tm :: 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 ai :: ArgInfo
ai n :: 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)
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent norm :: Rewrite
norm e :: Expr
e =
do (_,t :: 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 ii :: InteractionId
ii norm :: Rewrite
norm e :: 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 i :: InteractionId
i ret :: 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 m :: MetaId
m ret :: 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
introTactic :: Bool -> InteractionId -> TCM [String]
introTactic :: Bool -> InteractionId -> TCMT IO Names
introTactic pmLambda :: Bool
pmLambda ii :: 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 _ _ t :: 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
TelV tel' :: Telescope
tel' t :: 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' (-1) Dom Type -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
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 tel :: Telescope
tel _ <- (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 "interaction.intro" 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
[ "introTactic/fallback"
, "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'
, "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
(EmptyTel, EmptyTel) -> Names -> TCMT IO Names
forall (m :: * -> *) a. Monad m => a -> m a
return []
_ -> 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 d :: QName
d _ -> 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
_ -> TCMT IO Names
fallback
_ -> 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` \_ -> Names -> TCMT IO Names
forall (m :: * -> *) a. Monad m => a -> m a
return []
_ -> TCMT IO Names
forall a. HasCallStack => a
__IMPOSSIBLE__
where
conName :: [NamedArg SplitPattern] -> [I.ConHead]
conName :: [NamedArg SplitPattern] -> [ConHead]
conName [p :: NamedArg SplitPattern
p] = [ ConHead
c | I.ConP c :: ConHead
c _ _ <- [NamedArg SplitPattern -> SplitPattern
forall a. NamedArg a -> a
namedArg NamedArg SplitPattern
p] ]
conName _ = [ConHead]
forall a. HasCallStack => a
__IMPOSSIBLE__
showTCM :: PrettyTCM a => a -> TCM String
showTCM :: a -> TCM String
showTCM v :: 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 tel :: 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 "interaction.intro" 10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do "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 h :: Hiding
h = Bool
imp Bool -> Bool -> Bool
|| Hiding
h Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
NotHidden
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 <-
(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
| (h :: Hiding
h, i :: 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
$ ["λ", "{"] Names -> Names -> Names
forall a. [a] -> [a] -> [a]
++ Names
vars Names -> Names -> Names
forall a. [a] -> [a] -> [a]
++ ["→", "?", "}"] ]
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
$ ["λ"] Names -> Names -> Names
forall a. [a] -> [a] -> [a]
++ Names
vars Names -> Names -> Names
forall a. [a] -> [a] -> [a]
++ ["→", "?"] ]
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 ("_", t :: b
t) = ("x", b
t)
makeName (x :: a
x, t :: b
t) = (a
x, b
t)
introData :: I.Type -> TCM [String]
introData :: Type -> TCMT IO Names
introData t :: Type
t = do
let tel :: Telescope
tel = ListTel -> Telescope
telFromList [(String, Type) -> Dom' Term (String, Type)
forall a. a -> Dom a
defaultDom ("_", 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 "c" 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 err :: SplitError
err -> Names -> TCMT IO Names
forall (m :: * -> *) a. Monad m => a -> m a
return []
Right cov :: 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 d :: 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
$ \ f :: 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 ]
atTopLevel :: TCM a -> TCM a
atTopLevel :: TCM a -> TCM a
atTopLevel m :: 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 "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
$ \ current :: 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
$ \ mi :: 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
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
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' (\ x :: Name
x dom :: 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 "interaction.top" 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
[ "BasicOps.atTopLevel"
, " 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)
, " 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
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
parseName :: Range -> String -> TCM C.QName
parseName :: Range -> String -> TCM QName
parseName r :: Range
r s :: String
s = do
Expr
m <- Range -> String -> TCM Expr
parseExpr Range
r String
s
case Expr
m of
C.Ident m :: QName
m -> QName -> TCM QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
C.RawApp _ [C.Ident m :: QName
m] -> QName -> TCM QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
_ -> 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
$ "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]
++ "."
isQName :: C.Expr -> Maybe C.QName
isQName :: Expr -> Maybe QName
isQName m :: Expr
m = do
case Expr
m of
C.Ident m :: QName
m -> QName -> Maybe QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
C.RawApp _ [C.Ident m :: QName
m] -> QName -> Maybe QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
m
_ -> Maybe QName
forall a. Maybe a
Nothing
moduleContents
:: Rewrite
-> Range
-> String
-> TCM ([C.Name], I.Telescope, [(C.Name, Type)])
moduleContents :: Rewrite
-> Range -> String -> TCM ([Name], Telescope, [(Name, Type)])
moduleContents norm :: Rewrite
norm rng :: Range
rng s :: 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
Nothing -> Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
getRecordContents Rewrite
norm Expr
e
Just x :: 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
getRecordContents
:: Rewrite
-> C.Expr
-> TCM ([C.Name], I.Telescope, [(C.Name, Type)])
getRecordContents :: Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
getRecordContents norm :: Rewrite
norm ce :: Expr
ce = do
Expr
e <- Expr -> TCM Expr
forall concrete abstract.
ToAbstract concrete abstract =>
concrete -> ScopeM abstract
toAbstract Expr
ce
(_, t :: 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
(q :: QName
q, vs :: Args
vs, defn :: 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
String -> VerboseLevel -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc "interaction.contents.record" 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
[ "getRecordContents"
, " 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)
, " 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
, " 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
, " 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)
_ -> TCM ([Name], Telescope, [(Name, Type)])
forall a. HasCallStack => a
__IMPOSSIBLE__
getModuleContents
:: Rewrite
-> C.QName
-> TCM ([C.Name], I.Telescope, [(C.Name, Type)])
getModuleContents :: Rewrite -> QName -> TCM ([Name], Telescope, [(Name, Type)])
getModuleContents norm :: Rewrite
norm m :: 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) | (x :: Name
x, ns :: [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
$ \(x :: Name
x, n :: 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 s :: 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 )