{-# LANGUAGE NondecreasingIndentation #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.Interaction.BasicOps where
import Prelude hiding (null)
import Control.Arrow ( first )
import Control.Monad ( (<=<), (>=>), forM, filterM, guard )
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Identity
import Control.Monad.Trans.Maybe
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import qualified Data.Map.Strict as MapS
import qualified Data.Set as Set
import qualified Data.List as List
import Data.Maybe
import Data.Monoid
import Data.Function (on)
import Data.Text (Text)
import qualified Data.Text as T
import Agda.Interaction.Base
import Agda.Interaction.Output
import Agda.Interaction.Options
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 ( getAllWarnings, stringTCErr, Verbalize(..) )
import Agda.TypeChecking.Monad as M hiding (MetaInfo)
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.MetaVars.Mention
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.With
import Agda.TypeChecking.Coverage
import Agda.TypeChecking.Coverage.Match ( SplitPattern )
import Agda.TypeChecking.Records
import Agda.TypeChecking.Pretty ( PrettyTCM, prettyTCM )
import Agda.TypeChecking.Pretty.Constraint (prettyRangeConstraint)
import Agda.TypeChecking.IApplyConfluence
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.ProjectionLike (reduceProjectionLike)
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.Function (applyWhen)
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty as P
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.String
import Agda.Utils.WithDefault ( WithDefault'(Value) )
import Agda.Utils.Impossible
parseExpr :: Range -> String -> TCM C.Expr
parseExpr :: Range -> ArgName -> TCM Expr
parseExpr Range
rng ArgName
s = do
(C.ExprWhere e wh, attrs) <-
PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes)
forall a. PM a -> TCM a
runPM (PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes))
-> PM (ExprWhere, Attributes) -> TCM (ExprWhere, Attributes)
forall a b. (a -> b) -> a -> b
$ Parser ExprWhere
-> Position -> ArgName -> PM (ExprWhere, Attributes)
forall a. Parser a -> Position -> ArgName -> PM (a, Attributes)
parsePosString Parser ExprWhere
exprWhereParser Position
pos ArgName
s
checkAttributes attrs
unless (null wh) $ typeError $ GenericError $
"where clauses are not supported in holes"
return e
where pos :: Position
pos = Position -> Maybe Position -> Position
forall a. a -> Maybe a -> a
fromMaybe (Maybe RangeFile -> Position
startPos Maybe RangeFile
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 -> ArgName -> TCM Expr
parseExprIn InteractionId
ii Range
rng ArgName
s = do
mId <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
updateMetaVarRange mId rng
mi <- getMetaInfo <$> lookupLocalMeta mId
e <- parseExpr rng s
withMetaInfo mi $
concreteToAbstract (clScope mi) e
giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term
giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term
giveExpr UseForce
force Maybe InteractionId
mii MetaId
mi Expr
e = do
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
let t = case MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv of
IsSort{} -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__
HasType MetaId
_ Comparison
_ Type
t -> Type
t
reportSDoc "interaction.give" 20 $
"give: meta type =" TP.<+> prettyTCM t
ctx <- getContextArgs
t' <- t `piApplyM` permute (takeP (length ctx) $ mvPermutation mv) ctx
traceCall (CheckExprCall CmpLeq e t') $ do
reportSDoc "interaction.give" 20 $ do
a <- asksTC envAbstractMode
TP.hsep
[ TP.text ("give(" ++ show a ++ "): instantiated meta type =")
, prettyTCM t'
]
v <- locallyTC eMutualBlock (const Nothing) $
checkExpr e t'
reportSDoc "interaction.give" 40 $ "give: checked expression:" TP.<+> pure (pretty v)
case mvInstantiation mv of
InstV{} -> TCMT IO Bool -> ScopeM () -> ScopeM ()
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
<$> Lens' TCEnv Relevance -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Relevance -> f Relevance) -> TCEnv -> f TCEnv
Lens' TCEnv Relevance
eRelevance) (ScopeM () -> ScopeM ()) -> ScopeM () -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ do
v' <- Term -> TCM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
mi (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
ctx
reportSDoc "interaction.give" 20 $ TP.sep
[ "meta was already set to value v' = " TP.<+> prettyTCM v'
, "now comparing it to given value v = " TP.<+> prettyTCM v
, "in context " TP.<+> inTopContext (prettyTCM ctx)
]
equalTerm t' v v'
MetaInstantiation
_ -> do
ArgName -> Int -> ArgName -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"interaction.give" Int
20 ArgName
"give: meta unassigned, assigning..."
args <- TCMT IO Args
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Args
getContextArgs
nowSolvingConstraints $ assign DirEq mi args v (AsTermsOf t')
reportSDoc "interaction.give" 20 $ "give: meta variable updated!"
unless (force == WithForce) $ redoChecks mii
wakeupConstraints mi
solveSizeConstraints DontDefaultToInfty
cubical <- isJust <$> cubicalOption
unless (cubical || force == WithForce) $ do
reportSDoc "interaction.give" 20 $ "give: double checking"
vfull <- instantiateFull v
checkInternal vfull CmpLeq t'
return v
redoChecks :: Maybe InteractionId -> TCM ()
redoChecks :: Maybe InteractionId -> ScopeM ()
redoChecks Maybe InteractionId
Nothing = () -> ScopeM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
redoChecks (Just InteractionId
ii) = do
ArgName -> Int -> ArgName -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"interaction.give" Int
20 (ArgName -> ScopeM ()) -> ArgName -> ScopeM ()
forall a b. (a -> b) -> a -> b
$
ArgName
"give: redoing termination check for function surrounding " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ InteractionId -> ArgName
forall a. Show a => a -> ArgName
show InteractionId
ii
ip <- InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
case ipClause ip of
IPClause
IPNoClause -> () -> ScopeM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
IPClause{ipcQName :: IPClause -> QName
ipcQName = QName
f} -> do
mb <- QName -> TCM MutualId
mutualBlockOf QName
f
terErrs <- localTC (\ TCEnv
e -> TCEnv
e { envMutualBlock = Just mb }) $ termMutual []
unless (null terErrs) $ warning $ TerminationIssue terErrs
give
:: UseForce
-> InteractionId
-> Maybe Range
-> Expr
-> TCM Expr
give :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give UseForce
force InteractionId
ii Maybe Range
mr Expr
e = TCM Expr -> TCM Expr
forall a. TCM a -> TCM a
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
mi <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
whenJust mr $ updateMetaVarRange mi
reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e
reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e
_ <- withInteractionId ii $ do
setMetaOccursCheck mi DontRunMetaOccursCheck
giveExpr force (Just ii) mi e
`catchError` \ case
PatternErr{} -> TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> (Doc -> TypeError) -> Doc -> TCM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM Term) -> TCMT IO Doc -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
InteractionId -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Failed to give" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e
TCErr
err -> TCErr -> TCM Term
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
removeInteractionPoint ii
return e
elaborate_give
:: Rewrite
-> UseForce
-> InteractionId
-> Maybe Range
-> Expr
-> TCM Expr
elaborate_give :: Rewrite
-> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
elaborate_give Rewrite
norm UseForce
force InteractionId
ii Maybe Range
mr Expr
e = InteractionId -> TCM Expr -> TCM Expr
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ do
mi <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
whenJust mr $ updateMetaVarRange mi
reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e
reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e
v <- withInteractionId ii $ do
setMetaOccursCheck mi DontRunMetaOccursCheck
locallyTC eCurrentlyElaborating (const True) $
giveExpr force (Just ii) mi e
`catchError` \ case
PatternErr{} -> TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> (Doc -> TypeError) -> Doc -> TCM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM Term) -> TCMT IO Doc -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
InteractionId -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Failed to give" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e
TCErr
err -> TCErr -> TCM Term
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
mv <- lookupLocalMeta mi
nv <- reduceProjectionLike =<< normalForm norm v
reportSDoc "interaction.give" 40 $ "nv = " TP.<+> pure (pretty v)
locallyTC ePrintMetasBare (const True) $ reify nv
refine
:: UseForce
-> InteractionId
-> Maybe Range
-> Expr
-> TCM Expr
refine :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
refine UseForce
force InteractionId
ii Maybe Range
mr Expr
e = do
mi <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
mv <- lookupLocalMeta mi
let range = Range -> Maybe Range -> Range
forall a. a -> Maybe a -> a
fromMaybe (MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange MetaVariable
mv) Maybe Range
mr
scope = MetaVariable -> ScopeInfo
M.getMetaScope MetaVariable
mv
reportSDoc "interaction.refine" 10 $
"refining with expression" TP.<+> prettyTCM e
reportSDoc "interaction.refine" 50 $
TP.text $ show $ deepUnscope e
tryRefine 10 range scope e
where
tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine :: Int -> Range -> ScopeInfo -> Expr -> TCM Expr
tryRefine Int
nrOfMetas Range
r ScopeInfo
scope = Int -> Maybe TCErr -> Expr -> TCM Expr
try Int
nrOfMetas Maybe TCErr
forall a. Maybe a
Nothing
where
try :: Int -> Maybe TCErr -> Expr -> TCM Expr
try :: Int -> Maybe TCErr -> Expr -> TCM Expr
try Int
0 Maybe TCErr
err Expr
e = TCErr -> TCM Expr
forall a. TCErr -> TCMT IO a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCErr -> TCM Expr) -> (ArgName -> TCErr) -> ArgName -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> TCErr
stringTCErr (ArgName -> TCM Expr) -> ArgName -> TCM Expr
forall a b. (a -> b) -> a -> b
$ case Maybe TCErr
err of
Just (TypeError CallStack
_ TCState
_ Closure TypeError
cl) | UnequalTerms Comparison
_ I.Pi{} Term
_ CompareAs
_ <- Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cl ->
ArgName
"Cannot refine functions with 10 or more arguments"
Maybe TCErr
_ ->
ArgName
"Cannot refine"
try Int
n Maybe TCErr
_ Expr
e = UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give UseForce
force InteractionId
ii (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) Expr
e TCM Expr -> (TCErr -> TCM Expr) -> TCM Expr
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
err -> Int -> Maybe TCErr -> Expr -> TCM Expr
try (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (TCErr -> Maybe TCErr
forall a. a -> Maybe a
Just TCErr
err) (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM Expr
appMeta Expr
e
appMeta :: Expr -> TCM Expr
appMeta :: Expr -> TCM Expr
appMeta Expr
e = do
let rng :: Range
rng = Range -> Range
rightMargin Range
r
ii <- Bool -> Range -> Maybe Int -> TCMT IO InteractionId
forall (m :: * -> *).
MonadInteractionPoints m =>
Bool -> Range -> Maybe Int -> m InteractionId
registerInteractionPoint Bool
False Range
rng Maybe Int
forall a. Maybe a
Nothing
let info = Info.MetaInfo
{ metaRange :: Range
Info.metaRange = Range
rng
, metaScope :: ScopeInfo
Info.metaScope = Lens' ScopeInfo [Precedence] -> LensSet ScopeInfo [Precedence]
forall o i. Lens' o i -> LensSet o i
set ([Precedence] -> f [Precedence]) -> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo [Precedence]
scopePrecedence [Precedence
argumentCtx_] ScopeInfo
scope
, metaNumber :: Maybe MetaId
metaNumber = Maybe MetaId
forall a. Maybe a
Nothing
, metaNameSuggestion :: ArgName
metaNameSuggestion = ArgName
""
, metaKind :: MetaKind
metaKind = MetaKind
Info.UnificationMeta
}
metaVar = MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
info InteractionId
ii
count Name
x a
e = Sum a -> a
forall a. Sum a -> a
getSum (Sum a -> a) -> Sum a -> a
forall a b. (a -> b) -> a -> b
$ (Expr -> Sum a) -> a -> Sum a
forall m. FoldExprFn m a
forall a m. ExprLike a => FoldExprFn m a
foldExpr Expr -> Sum a
isX a
e
where isX :: Expr -> Sum a
isX (A.Var Name
y) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = a -> Sum a
forall a. a -> Sum a
Sum a
1
isX Expr
_ = Sum a
forall a. Monoid a => a
mempty
lamView (A.Lam ExprInfo
_ (DomainFree TacticAttribute
_ NamedArg Binder
x) Expr
e) = (Binder, Expr) -> Maybe (Binder, Expr)
forall a. a -> Maybe a
Just (NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x, Expr
e)
lamView (A.Lam ExprInfo
i (DomainFull (TBind Range
r TypedBindingInfo
t (NamedArg Binder
x :| [NamedArg Binder]
xs) Expr
a)) Expr
e) =
[NamedArg Binder]
-> Maybe (Binder, Expr)
-> (NonEmpty (NamedArg Binder) -> Maybe (Binder, Expr))
-> Maybe (Binder, Expr)
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [NamedArg Binder]
xs ((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)) ((NonEmpty (NamedArg Binder) -> Maybe (Binder, Expr))
-> Maybe (Binder, Expr))
-> (NonEmpty (NamedArg Binder) -> Maybe (Binder, Expr))
-> Maybe (Binder, Expr)
forall a b. (a -> b) -> a -> b
$ \ NonEmpty (NamedArg Binder)
xs ->
(Binder, Expr) -> Maybe (Binder, Expr)
forall a. a -> Maybe a
Just (NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
x, ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (TypedBinding -> LamBinding
DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. (a -> b) -> a -> b
$ Range
-> TypedBindingInfo
-> NonEmpty (NamedArg Binder)
-> Expr
-> TypedBinding
TBind Range
r TypedBindingInfo
t NonEmpty (NamedArg Binder)
xs Expr
a) Expr
e)
lamView Expr
_ = Maybe (Binder, Expr)
forall a. Maybe a
Nothing
smartApp AppInfo
i Expr
e NamedArg Expr
arg =
case ((Binder, Expr) -> (BindName, Expr))
-> Maybe (Binder, Expr) -> Maybe (BindName, Expr)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Binder -> BindName) -> (Binder, Expr) -> (BindName, Expr)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Binder -> BindName
forall a. Binder' a -> a
A.binderName) (Expr -> Maybe (Binder, Expr)
lamView (Expr -> Maybe (Binder, Expr)) -> Expr -> Maybe (Binder, Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
unScope Expr
e) of
Just (A.BindName{unBind :: BindName -> Name
unBind = Name
x}, Expr
e) | Name -> Expr -> Integer
forall {a} {a}. (Num a, ExprLike a) => Name -> a -> a
count Name
x Expr
e Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2 -> (Expr -> Expr) -> Expr -> Expr
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
subX Expr
e
where subX :: Expr -> Expr
subX (A.Var Name
y) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg Expr
arg
subX Expr
e = Expr
e
Maybe (BindName, Expr)
_ -> AppInfo -> Expr -> NamedArg Expr -> Expr
App AppInfo
i Expr
e NamedArg Expr
arg
return $ smartApp (defaultAppInfo r) e $ defaultNamedArg metaVar
evalInCurrent :: ComputeMode -> Expr -> TCM Expr
evalInCurrent :: ComputeMode -> Expr -> TCM Expr
evalInCurrent ComputeMode
cmode Expr
e = do
(v, _t) <- Expr -> TCM (Term, Type)
inferExpr Expr
e
vb <- reduceB v
reportSDoc "interaction.eval" 30 $ "evaluated to" TP.<+> TP.pretty vb
v <- pure $ ignoreBlocking vb
reify =<< if cmode == HeadCompute then pure v else normalise v
evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
evalInMeta :: InteractionId -> ComputeMode -> Expr -> TCM Expr
evalInMeta InteractionId
ii ComputeMode
cmode Expr
e =
do m <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
mi <- getMetaInfo <$> lookupLocalMeta m
withMetaInfo mi $
evalInCurrent cmode e
normalForm :: (Reduce t, Simplify t, Instantiate t, Normalise t) => Rewrite -> t -> TCM t
normalForm :: forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm = \case
Rewrite
AsIs -> t -> TCM t
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate
Rewrite
Instantiated -> t -> TCM t
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate
Rewrite
HeadNormal -> t -> TCM t
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce
Rewrite
Simplified -> t -> TCM t
forall a (m :: * -> *). (Simplify a, MonadReduce m) => a -> m a
simplify
Rewrite
Normalised -> t -> TCM t
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise
computeIgnoreAbstract :: ComputeMode -> Bool
computeIgnoreAbstract :: ComputeMode -> Bool
computeIgnoreAbstract ComputeMode
DefaultCompute = Bool
False
computeIgnoreAbstract ComputeMode
HeadCompute = Bool
False
computeIgnoreAbstract ComputeMode
IgnoreAbstract = Bool
True
computeIgnoreAbstract ComputeMode
UseShowInstance = Bool
False
computeWrapInput :: ComputeMode -> String -> String
computeWrapInput :: ComputeMode -> ArgName -> ArgName
computeWrapInput ComputeMode
UseShowInstance ArgName
s = ArgName
"show (" ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
s ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
")"
computeWrapInput ComputeMode
_ ArgName
s = ArgName
s
showComputed :: ComputeMode -> Expr -> TCM Doc
showComputed :: ComputeMode -> Expr -> TCMT IO Doc
showComputed ComputeMode
UseShowInstance Expr
e =
case Expr
e of
A.Lit ExprInfo
_ (LitString Text
s) -> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ArgName -> Doc
forall a. ArgName -> Doc a
text (ArgName -> Doc) -> ArgName -> Doc
forall a b. (a -> b) -> a -> b
$ Text -> ArgName
T.unpack Text
s)
Expr
_ -> (Doc
"Expected applying `show` to the given value to produce a string literal, but got:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
$$) (Doc -> Doc) -> TCMT IO Doc -> TCMT IO Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
showComputed ComputeMode
_ Expr
e = Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
outputFormId :: OutputForm a b -> b
outputFormId :: forall a b. OutputForm a b -> b
outputFormId (OutputForm Range
_ [ProblemId]
_ Blocker
_ OutputConstraint_boot TCErr a b
o) = OutputConstraint_boot TCErr a b -> b
forall {tcErr} {a} {b}. OutputConstraint_boot tcErr a b -> b
out OutputConstraint_boot TCErr a b
o
where
out :: OutputConstraint_boot tcErr a b -> b
out = \case
OfType b
i a
_ -> b
i
CmpInType Comparison
_ a
_ b
i b
_ -> b
i
CmpElim [Polarity]
_ a
_ (b
i:[b]
_) [b]
_ -> b
i
CmpElim [Polarity]
_ a
_ [] [b]
_ -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
JustType b
i -> b
i
CmpLevels Comparison
_ b
i b
_ -> b
i
CmpTypes Comparison
_ b
i b
_ -> b
i
CmpTeles Comparison
_ b
i b
_ -> b
i
JustSort b
i -> b
i
CmpSorts Comparison
_ b
i b
_ -> b
i
Assign b
i a
_ -> b
i
TypedAssign b
i a
_ a
_ -> b
i
PostponedCheckArgs b
i [a]
_ a
_ a
_ -> b
i
IsEmptyType a
_ -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
SizeLtSat{} -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
FindInstanceOF b
_ a
_ [(a, a, a)]
_ -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
ResolveInstanceOF QName
_ -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
PTSInstance b
i b
_ -> b
i
PostponedCheckFunDef{} -> b
forall a. HasCallStack => a
__IMPOSSIBLE__
DataSort QName
_ b
i -> b
i
CheckLock b
i b
_ -> b
i
UsableAtMod Modality
_ b
i -> b
i
instance Reify ProblemConstraint where
type ReifiesTo ProblemConstraint = Closure (OutputForm Expr Expr)
reify :: forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify (PConstr Set ProblemId
pids Blocker
unblock Closure Constraint
cl) = Closure Constraint
-> (Constraint -> m (OutputForm Expr Expr))
-> m (Closure (OutputForm Expr Expr))
forall (m :: * -> *) a b.
(MonadTCEnv m, ReadTCState m) =>
Closure a -> (a -> m b) -> m (Closure b)
withClosure Closure Constraint
cl ((Constraint -> m (OutputForm Expr Expr))
-> m (Closure (OutputForm Expr Expr)))
-> (Constraint -> m (OutputForm Expr Expr))
-> m (Closure (OutputForm Expr Expr))
forall a b. (a -> b) -> a -> b
$ \ Constraint
c ->
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr Expr Expr
-> OutputForm Expr Expr
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm (Constraint -> Range
forall a. HasRange a => a -> Range
getRange Constraint
c) (Set ProblemId -> [ProblemId]
forall a. Set a -> [a]
Set.toList Set ProblemId
pids) Blocker
unblock (OutputConstraint_boot TCErr Expr Expr -> OutputForm Expr Expr)
-> m (OutputConstraint_boot TCErr Expr Expr)
-> m (OutputForm Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Constraint -> m (ReifiesTo Constraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Constraint -> m (ReifiesTo Constraint)
reify Constraint
c
reifyElimToExpr :: MonadReify m => I.Elim -> m Expr
reifyElimToExpr :: forall (m :: * -> *). MonadReify m => Elim' Term -> m Expr
reifyElimToExpr = \case
I.IApply Term
_ Term
_ Term
v -> Text -> Arg Expr -> Expr
appl Text
"iapply" (Arg Expr -> Expr) -> m (Arg Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> m (ReifiesTo (Arg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Term -> m (ReifiesTo (Arg Term))
reify (Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term
v)
I.Apply Arg Term
v -> Text -> Arg Expr -> Expr
appl Text
"apply" (Arg Expr -> Expr) -> m (Arg Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> m (ReifiesTo (Arg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Term -> m (ReifiesTo (Arg Term))
reify Arg Term
v
I.Proj ProjOrigin
_o QName
f -> Text -> Arg Expr -> Expr
appl Text
"proj" (Arg Expr -> Expr) -> m (Arg Expr) -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> m (ReifiesTo (Arg Term))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
Arg Term -> m (ReifiesTo (Arg Term))
reify ((Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
I.Def QName
f []) :: Arg Term)
where
appl :: Text -> Arg Expr -> Expr
appl :: Text -> Arg Expr -> Expr
appl Text
s Arg Expr
v = AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Literal -> Expr
A.Lit ExprInfo
forall a. Null a => a
empty (Text -> Literal
LitString Text
s)) (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ (Expr -> Named_ Expr) -> Arg Expr -> NamedArg Expr
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Named_ Expr
forall a name. a -> Named name a
unnamed Arg Expr
v
instance Reify Constraint where
type ReifiesTo Constraint = OutputConstraint Expr Expr
reify :: forall (m :: * -> *).
MonadReify m =>
Constraint -> m (ReifiesTo Constraint)
reify (ValueCmp Comparison
cmp (AsTermsOf Type
t) Term
u Term
v) = Comparison
-> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
CmpInType Comparison
cmp (Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
u m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
reify (ValueCmp Comparison
cmp CompareAs
AsSizes Term
u Term
v) = Comparison
-> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
CmpInType Comparison
cmp (Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType) m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
u m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
reify (ValueCmp Comparison
cmp CompareAs
AsTypes Term
u Term
v) = Comparison -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpTypes Comparison
cmp (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
u m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
reify (ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v) = Comparison
-> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
CmpInType Comparison
cmp (Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
ty) m (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Term -> Term
lam_o Term
u) m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Term -> Term
lam_o Term
v)
where
lam_o :: Term -> Term
lam_o = ArgInfo -> Abs Term -> Term
I.Lam (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
. ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
NoAbs ArgName
"_"
ty :: m Type
ty = Names -> NamesT m Type -> m Type
forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (NamesT m Type -> m Type) -> NamesT m Type -> m Type
forall a b. (a -> b) -> a -> b
$ do
p <- Term -> NamesT m (NamesT m Term)
forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open Term
p
t <- open t
pPi' "o" p (\ NamesT m Term
o -> NamesT m Type
t)
reify (ElimCmp [Polarity]
cmp [IsForced]
_ Type
t Term
v Elims
es1 Elims
es2) =
[Polarity]
-> Expr
-> [Expr]
-> [Expr]
-> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
[Polarity] -> a -> [b] -> [b] -> OutputConstraint_boot tcErr a b
CmpElim [Polarity]
cmp (Expr -> [Expr] -> [Expr] -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m ([Expr] -> [Expr] -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t m ([Expr] -> [Expr] -> OutputConstraint_boot TCErr Expr Expr)
-> m [Expr] -> m ([Expr] -> OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Elim' Term -> m Expr) -> Elims -> m [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> m Expr
forall (m :: * -> *). MonadReify m => Elim' Term -> m Expr
reifyElimToExpr Elims
es1
m ([Expr] -> OutputConstraint_boot TCErr Expr Expr)
-> m [Expr] -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Elim' Term -> m Expr) -> Elims -> m [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim' Term -> m Expr
forall (m :: * -> *). MonadReify m => Elim' Term -> m Expr
reifyElimToExpr Elims
es2
reify (LevelCmp Comparison
cmp Level
t Level
t') = Comparison -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpLevels Comparison
cmp (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
reify Level
t m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Level -> m (ReifiesTo Level)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Level -> m (ReifiesTo Level)
reify Level
t'
reify (SortCmp Comparison
cmp Sort
s Sort
s') = Comparison -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpSorts Comparison
cmp (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s'
reify (UnquoteTactic Term
tac Term
_ Type
goal) = do
tac <- AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Expr
A.Unquote ExprInfo
exprNoRange) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
tac
OfType tac <$> reify goal
reify (UnBlock MetaId
m) = do
mi <- MetaId -> m MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
m
m' <- reify (MetaV m [])
case mi of
BlockedConst Term
t -> do
e <- Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
t
return $ Assign m' e
PostponedTypeCheckingProblem Closure TypeCheckingProblem
cl -> Closure TypeCheckingProblem
-> (TypeCheckingProblem
-> m (OutputConstraint_boot TCErr Expr Expr))
-> m (OutputConstraint_boot TCErr Expr Expr)
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure Closure TypeCheckingProblem
cl ((TypeCheckingProblem -> m (OutputConstraint_boot TCErr Expr Expr))
-> m (OutputConstraint_boot TCErr Expr Expr))
-> (TypeCheckingProblem
-> m (OutputConstraint_boot TCErr Expr Expr))
-> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. (a -> b) -> a -> b
$ \case
CheckExpr Comparison
cmp Expr
e Type
a -> do
a <- Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
a
return $ TypedAssign m' e a
CheckLambda Comparison
cmp (Arg ArgInfo
ai (List1 (WithHiding Name)
xs, Maybe Type
mt)) Expr
body Type
target -> do
domType <- m Expr -> (Type -> m Expr) -> Maybe Type -> m Expr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Expr -> m Expr
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall a. Underscore a => a
underscore) Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Maybe Type
mt
target <- reify target
let mkN (WithHiding Hiding
h Name
x) = Hiding -> NamedArg Binder -> NamedArg Binder
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
h (NamedArg Binder -> NamedArg Binder)
-> NamedArg Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Binder -> NamedArg Binder
forall a. a -> NamedArg a
defaultNamedArg (Binder -> NamedArg Binder) -> Binder -> NamedArg Binder
forall a b. (a -> b) -> a -> b
$ Name -> Binder
A.mkBinder_ Name
x
bs = Range -> NonEmpty (NamedArg Binder) -> Expr -> TypedBinding
mkTBind Range
forall a. Range' a
noRange ((WithHiding Name -> NamedArg Binder)
-> List1 (WithHiding Name) -> NonEmpty (NamedArg Binder)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WithHiding Name -> NamedArg Binder
mkN List1 (WithHiding Name)
xs) Expr
domType
e = ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
Info.exprNoRange (TypedBinding -> LamBinding
DomainFull TypedBinding
bs) Expr
body
return $ TypedAssign m' e target
CheckArgs Comparison
_ ExpandHidden
_ Range
_ [NamedArg Expr]
args Type
t0 Type
t1 ArgsCheckState CheckedTarget -> TCM Term
_ -> do
t0 <- Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t0
t1 <- reify t1
return $ PostponedCheckArgs m' (map (namedThing . unArg) args) t0 t1
CheckProjAppToKnownPrincipalArg Comparison
cmp Expr
e ProjOrigin
_ List1 QName
_ [NamedArg Expr]
_ Type
t Int
_ Term
_ Type
_ PrincipalArgTypeMetas
_ -> Expr -> Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. b -> a -> a -> OutputConstraint_boot tcErr a b
TypedAssign Expr
m' Expr
e (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t
DoQuoteTerm Comparison
cmp Term
v Type
t -> do
tm <- AppInfo -> Expr -> NamedArg Expr -> Expr
A.App AppInfo
defaultAppInfo_ (ExprInfo -> Expr
A.QuoteTerm ExprInfo
exprNoRange) (NamedArg Expr -> Expr) -> (Expr -> NamedArg Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
v
OfType tm <$> reify t
OpenMeta{} -> m (OutputConstraint_boot TCErr Expr Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
InstV{} -> m (OutputConstraint_boot TCErr Expr Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
reify (FindInstance MetaId
m Maybe [Candidate]
mcands) = Expr
-> Expr
-> [(Expr, Expr, Expr)]
-> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b.
b -> a -> [(a, a, a)] -> OutputConstraint_boot tcErr a b
FindInstanceOF
(Expr
-> Expr
-> [(Expr, Expr, Expr)]
-> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m (Expr
-> [(Expr, Expr, Expr)] -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (MetaId -> Elims -> Term
MetaV MetaId
m [])
m (Expr
-> [(Expr, Expr, Expr)] -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr
-> m ([(Expr, Expr, Expr)]
-> OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> m Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
getMetaType MetaId
m)
m ([(Expr, Expr, Expr)] -> OutputConstraint_boot TCErr Expr Expr)
-> m [(Expr, Expr, Expr)]
-> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Candidate]
-> (Candidate -> m (Expr, Expr, Expr)) -> m [(Expr, Expr, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Candidate] -> Maybe [Candidate] -> [Candidate]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Candidate]
mcands) (\ (Candidate CandidateKind
q Term
tm Type
ty OverlapMode
_) -> do
(,,) (Expr -> Expr -> Expr -> (Expr, Expr, Expr))
-> m Expr -> m (Expr -> Expr -> (Expr, Expr, Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
tm m (Expr -> Expr -> (Expr, Expr, Expr))
-> m Expr -> m (Expr -> (Expr, Expr, Expr))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
tm m (Expr -> (Expr, Expr, Expr)) -> m Expr -> m (Expr, Expr, Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
ty)
reify (ResolveInstanceHead QName
q) = ReifiesTo Constraint -> m (ReifiesTo Constraint)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ReifiesTo Constraint -> m (ReifiesTo Constraint))
-> ReifiesTo Constraint -> m (ReifiesTo Constraint)
forall a b. (a -> b) -> a -> b
$ QName -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. QName -> OutputConstraint_boot tcErr a b
ResolveInstanceOF QName
q
reify (IsEmpty Range
r Type
a) = Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. a -> OutputConstraint_boot tcErr a b
IsEmptyType (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
a
reify (CheckSizeLtSat Term
a) = Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. a -> OutputConstraint_boot tcErr a b
SizeLtSat (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
a
reify (CheckFunDef DefInfo
i QName
q [Clause]
cs TCErr
err) = do
a <- Type -> m Expr
Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (Type -> m Expr) -> m Type -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Definition -> Type
defType (Definition -> Type) -> m Definition -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
return $ PostponedCheckFunDef q a err
reify (HasBiggerSort Sort
a) = Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
OfType (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
a m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify (Sort -> Sort
forall t. Sort' t -> Sort' t
UnivSort Sort
a)
reify (HasPTSRule Dom Type
a Abs Sort
b) = do
(a,(x,b)) <- (Type, Abs Sort) -> m (ReifiesTo (Type, Abs Sort))
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
(Type, Abs Sort) -> m (ReifiesTo (Type, Abs Sort))
reify (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a,Abs Sort
b)
return $ PTSInstance a b
reify (CheckDataSort QName
q Sort
s) = QName -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. QName -> b -> OutputConstraint_boot tcErr a b
DataSort QName
q (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> m (ReifiesTo Sort)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Sort -> m (ReifiesTo Sort)
reify Sort
s
reify (CheckLockedVars Term
t Type
_ Arg Term
lk Type
_) = Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. b -> b -> OutputConstraint_boot tcErr a b
CheckLock (Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (Expr -> OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
t m (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
lk)
reify (CheckMetaInst MetaId
m) = do
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 :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
OfType <$> reify (MetaV m []) <*> reify t
reify (CheckType Type
t) = Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. b -> OutputConstraint_boot tcErr a b
JustType (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> m (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify Type
t
reify (UsableAtModality WhyCheckModality
_ Maybe Sort
_ Modality
mod Term
t) = Modality -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. Modality -> b -> OutputConstraint_boot tcErr a b
UsableAtMod Modality
mod (Expr -> OutputConstraint_boot TCErr Expr Expr)
-> m Expr -> m (OutputConstraint_boot TCErr Expr Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m (ReifiesTo Term)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Term -> m (ReifiesTo Term)
reify Term
t
{-# SPECIALIZE reify :: Constraint -> TCM (ReifiesTo Constraint) #-}
instance (Pretty a, Pretty b) => PrettyTCM (OutputForm a b) where
prettyTCM :: forall (m :: * -> *). MonadPretty m => OutputForm a b -> m Doc
prettyTCM (OutputForm Range
r [ProblemId]
pids Blocker
unblock OutputConstraint_boot TCErr a b
c) =
Range -> [ProblemId] -> Blocker -> Doc -> m Doc
forall (m :: * -> *) (f :: * -> *).
(MonadPretty m, Foldable f, Null (f ProblemId)) =>
Range -> f ProblemId -> Blocker -> Doc -> m Doc
prettyRangeConstraint Range
r [ProblemId]
pids Blocker
unblock (OutputConstraint_boot TCErr a b -> Doc
forall a. Pretty a => a -> Doc
pretty OutputConstraint_boot TCErr a b
c)
{-# SPECIALIZE prettyTCM :: (Pretty a, Pretty b) => (OutputForm a b) -> TCM Doc #-}
instance (Pretty a, Pretty b) => Pretty (OutputForm a b) where
pretty :: OutputForm a b -> Doc
pretty (OutputForm Range
r [ProblemId]
pids Blocker
unblock OutputConstraint_boot TCErr a b
c) =
OutputConstraint_boot TCErr a b -> Doc
forall a. Pretty a => a -> Doc
pretty OutputConstraint_boot TCErr a b
c Doc -> Doc -> Doc
<?>
[Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Range -> Doc
forall {a} {a}. Pretty a => a -> Doc a
prange Range
r, Doc -> Doc
parensNonEmpty ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [Blocker -> Doc
blockedOn Blocker
unblock, [ProblemId] -> Doc
forall {a}. Pretty a => [a] -> Doc
prPids [ProblemId]
pids]) ]
where
prPids :: [a] -> Doc
prPids [] = Doc
forall a. Null a => a
empty
prPids [a
pid] = Doc
"belongs to problem" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
pid
prPids [a]
pids = Doc
"belongs to problems" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep (Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
"," ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty [a]
pids)
comma :: Doc
comma | [ProblemId] -> Bool
forall a. Null a => a -> Bool
null [ProblemId]
pids = Doc
forall a. Null a => a
empty
| Bool
otherwise = Doc
","
blockedOn :: Blocker -> Doc
blockedOn (UnblockOnAll Set Blocker
bs) | Set Blocker -> Bool
forall a. Set a -> Bool
Set.null Set Blocker
bs = Doc
forall a. Null a => a
empty
blockedOn (UnblockOnAny Set Blocker
bs) | Set Blocker -> Bool
forall a. Set a -> Bool
Set.null Set Blocker
bs = Doc
"stuck" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
comma
blockedOn Blocker
u = Doc
"blocked on" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (Blocker -> Doc
forall a. Pretty a => a -> Doc
pretty Blocker
u Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
P.<> Doc
comma)
prange :: a -> Doc a
prange a
r | ArgName -> Bool
forall a. Null a => a -> Bool
null ArgName
s = Doc a
forall a. Null a => a
empty
| Bool
otherwise = ArgName -> Doc a
forall a. ArgName -> Doc a
text (ArgName -> Doc a) -> ArgName -> Doc a
forall a b. (a -> b) -> a -> b
$ ArgName
" [ at " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
s ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" ]"
where s :: ArgName
s = a -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow a
r
instance (Pretty a, Pretty b) => Pretty (OutputConstraint a b) where
pretty :: OutputConstraint a b -> Doc
pretty OutputConstraint a b
oc =
case OutputConstraint a b
oc of
OfType b
e a
t -> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e Doc -> a -> Doc
forall {a}. Pretty a => Doc -> a -> Doc
.: a
t
JustType b
e -> Doc
"Type" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e
JustSort b
e -> Doc
"Sort" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e
CmpInType Comparison
cmp a
t b
e b
e' -> Comparison -> b -> b -> Doc
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc
pcmp Comparison
cmp b
e b
e' Doc -> a -> Doc
forall {a}. Pretty a => Doc -> a -> Doc
.: a
t
CmpElim [Polarity]
cmp a
t [b]
e [b]
e' -> [Polarity] -> [b] -> [b] -> Doc
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc
pcmp [Polarity]
cmp [b]
e [b]
e' Doc -> a -> Doc
forall {a}. Pretty a => Doc -> a -> Doc
.: a
t
CmpTypes Comparison
cmp b
t b
t' -> Comparison -> b -> b -> Doc
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc
pcmp Comparison
cmp b
t b
t'
CmpLevels Comparison
cmp b
t b
t' -> Comparison -> b -> b -> Doc
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc
pcmp Comparison
cmp b
t b
t'
CmpTeles Comparison
cmp b
t b
t' -> Comparison -> b -> b -> Doc
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc
pcmp Comparison
cmp b
t b
t'
CmpSorts Comparison
cmp b
s b
s' -> Comparison -> b -> b -> Doc
forall {a} {a} {a}.
(Pretty a, Pretty a, Pretty a) =>
a -> a -> a -> Doc
pcmp Comparison
cmp b
s b
s'
Assign b
m a
e -> Doc -> Doc -> Doc -> Doc
bin (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
m) Doc
":=" (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e)
TypedAssign b
m a
e a
a -> Doc -> Doc -> Doc -> Doc
bin (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
m) Doc
":=" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc -> Doc -> Doc
bin (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
e) Doc
":?" (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a)
PostponedCheckArgs b
m [a]
es a
t0 a
t1 ->
Doc -> Doc -> Doc -> Doc
bin (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
m) Doc
":=" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc -> Doc
parens (Doc
"_" Doc -> a -> Doc
forall {a}. Pretty a => Doc -> a -> Doc
.: a
t0) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
paren (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Pretty a => a -> Doc
pretty) [a]
es)) Doc -> a -> Doc
forall {a}. Pretty a => Doc -> a -> Doc
.: a
t1
where paren :: Doc -> Doc
paren Doc
d = Bool -> Doc -> Doc
mparens ((Char -> Bool) -> ArgName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Char -> ArgName -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
' ', Char
'\n']) (ArgName -> Bool) -> ArgName -> Bool
forall a b. (a -> b) -> a -> b
$ Doc -> ArgName
forall a. Show a => a -> ArgName
show Doc
d) Doc
d
IsEmptyType a
a -> Doc
"Is empty:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
SizeLtSat a
a -> Doc
"Not empty type of sizes:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a
FindInstanceOF b
s a
t [(a, a, a)]
cs -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Doc
"Resolve instance argument" Doc -> Doc -> Doc
<?> (b -> Doc
forall a. Pretty a => a -> Doc
pretty b
s Doc -> a -> Doc
forall {a}. Pretty a => Doc -> a -> Doc
.: a
t)
, Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Candidate:"
, Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ Doc -> Doc -> Doc -> Doc
bin (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
q) Doc
"=" (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
v) Doc -> a -> Doc
forall {a}. Pretty a => Doc -> a -> Doc
.: a
t | (a
q, a
v, a
t) <- [(a, a, a)]
cs ] ]
ResolveInstanceOF QName
q ->
Doc
"Resolve output type of instance" Doc -> Doc -> Doc
<?> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q
PTSInstance b
a b
b -> Doc
"PTS instance for" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> (b, b) -> Doc
forall a. Pretty a => a -> Doc
pretty (b
a, b
b)
PostponedCheckFunDef QName
q a
a TCErr
_err ->
[Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ Doc
"Check definition of" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
q Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
":" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a ]
DataSort QName
q b
s -> Doc
"Sort" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
s Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"allows data/record definitions"
CheckLock b
t b
lk -> Doc
"Check lock" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
lk Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"allows" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
t
UsableAtMod Modality
mod b
t -> Doc
"Is usable at" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> ArgName -> Doc
forall a. ArgName -> Doc a
text (Modality -> ArgName
forall a. Verbalize a => a -> ArgName
verbalize Modality
mod) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"modality:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
t
where
bin :: Doc -> Doc -> Doc -> Doc
bin Doc
a Doc
op Doc
b = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [Doc
a, Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
op Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
b]
pcmp :: a -> a -> a -> Doc
pcmp a
cmp a
a a
b = Doc -> Doc -> Doc -> Doc
bin (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a) (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
cmp) (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
b)
Doc
val .: :: Doc -> a -> Doc
.: a
ty = Doc -> Doc -> Doc -> Doc
bin Doc
val Doc
":" (a -> Doc
forall a. Pretty a => a -> Doc
pretty a
ty)
instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b) where
type ConOfAbs (OutputForm a b) = OutputForm (ConOfAbs a) (ConOfAbs b)
toConcrete :: OutputForm a b -> AbsToCon (ConOfAbs (OutputForm a b))
toConcrete (OutputForm Range
r [ProblemId]
pid Blocker
u OutputConstraint_boot TCErr a b
c) = Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
-> OutputForm_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range
r [ProblemId]
pid Blocker
u (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
-> OutputForm_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (OutputForm_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OutputConstraint_boot TCErr a b
-> AbsToCon (ConOfAbs (OutputConstraint_boot TCErr a b))
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete OutputConstraint_boot TCErr a b
c
instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b) where
type ConOfAbs (OutputConstraint a b) = OutputConstraint (ConOfAbs a) (ConOfAbs b)
toConcrete :: OutputConstraint a b -> AbsToCon (ConOfAbs (OutputConstraint a b))
toConcrete (OfType b
e a
t) = ConOfAbs b
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
OfType (ConOfAbs b
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
e AbsToCon
(ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
t
toConcrete (JustType b
e) = ConOfAbs b -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> OutputConstraint_boot tcErr a b
JustType (ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
e
toConcrete (JustSort b
e) = ConOfAbs b -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> OutputConstraint_boot tcErr a b
JustSort (ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
e
toConcrete (CmpInType Comparison
cmp a
t b
e b
e') =
Comparison
-> ConOfAbs a
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> a -> b -> b -> OutputConstraint_boot tcErr a b
CmpInType Comparison
cmp (ConOfAbs a
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon
(ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
t AbsToCon
(ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e
AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e'
toConcrete (CmpElim [Polarity]
cmp a
t [b]
e [b]
e') =
[Polarity]
-> ConOfAbs a
-> [ConOfAbs b]
-> [ConOfAbs b]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
[Polarity] -> a -> [b] -> [b] -> OutputConstraint_boot tcErr a b
CmpElim [Polarity]
cmp (ConOfAbs a
-> [ConOfAbs b]
-> [ConOfAbs b]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon
([ConOfAbs b]
-> [ConOfAbs b]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
t AbsToCon
([ConOfAbs b]
-> [ConOfAbs b]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon [ConOfAbs b]
-> AbsToCon
([ConOfAbs b]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> [b] -> AbsToCon (ConOfAbs [b])
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx [b]
e AbsToCon
([ConOfAbs b]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon [ConOfAbs b]
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> [b] -> AbsToCon (ConOfAbs [b])
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx [b]
e'
toConcrete (CmpTypes Comparison
cmp b
e b
e') = Comparison
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpTypes Comparison
cmp (ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e
AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e'
toConcrete (CmpLevels Comparison
cmp b
e b
e') = Comparison
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpLevels Comparison
cmp (ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e
AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e'
toConcrete (CmpTeles Comparison
cmp b
e b
e') = Comparison
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpTeles Comparison
cmp (ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
e AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
e'
toConcrete (CmpSorts Comparison
cmp b
e b
e') = Comparison
-> ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
Comparison -> b -> b -> OutputConstraint_boot tcErr a b
CmpSorts Comparison
cmp (ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e
AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx b
e'
toConcrete (Assign b
m a
e) = AbsToCon (ConOfAbs (OutputConstraint a b))
-> AbsToCon (ConOfAbs (OutputConstraint a b))
forall a. AbsToCon a -> AbsToCon a
noTakenNames (AbsToCon (ConOfAbs (OutputConstraint a b))
-> AbsToCon (ConOfAbs (OutputConstraint a b)))
-> AbsToCon (ConOfAbs (OutputConstraint a b))
-> AbsToCon (ConOfAbs (OutputConstraint a b))
forall a b. (a -> b) -> a -> b
$ ConOfAbs b
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
Assign (ConOfAbs b
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
m AbsToCon
(ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
e
toConcrete (TypedAssign b
m a
e a
a) = ConOfAbs b
-> ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> a -> a -> OutputConstraint_boot tcErr a b
TypedAssign (ConOfAbs b
-> ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
m AbsToCon
(ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon
(ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
e
AbsToCon
(ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
a
toConcrete (PostponedCheckArgs b
m [a]
args a
t0 a
t1) =
ConOfAbs b
-> [ConOfAbs a]
-> ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
b -> [a] -> a -> a -> OutputConstraint_boot tcErr a b
PostponedCheckArgs (ConOfAbs b
-> [ConOfAbs a]
-> ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
([ConOfAbs a]
-> ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
m AbsToCon
([ConOfAbs a]
-> ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon [ConOfAbs a]
-> AbsToCon
(ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [a] -> AbsToCon (ConOfAbs [a])
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete [a]
args AbsToCon
(ConOfAbs a
-> ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon
(ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
t0 AbsToCon
(ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
t1
toConcrete (IsEmptyType a
a) = ConOfAbs a -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. a -> OutputConstraint_boot tcErr a b
IsEmptyType (ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
a
toConcrete (SizeLtSat a
a) = ConOfAbs a -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. a -> OutputConstraint_boot tcErr a b
SizeLtSat (ConOfAbs a
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
a
toConcrete (FindInstanceOF b
s a
t [(a, a, a)]
cs) =
ConOfAbs b
-> ConOfAbs a
-> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
b -> a -> [(a, a, a)] -> OutputConstraint_boot tcErr a b
FindInstanceOF (ConOfAbs b
-> ConOfAbs a
-> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs a
-> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
s AbsToCon
(ConOfAbs a
-> [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon
([(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
t
AbsToCon
([(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((a, a, a) -> AbsToCon (ConOfAbs a, ConOfAbs a, ConOfAbs a))
-> [(a, a, a)] -> AbsToCon [(ConOfAbs a, ConOfAbs a, ConOfAbs a)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(a
q,a
tm,a
ty) -> (,,) (ConOfAbs a
-> ConOfAbs a
-> ConOfAbs a
-> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
-> AbsToCon (ConOfAbs a)
-> AbsToCon
(ConOfAbs a -> ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
q AbsToCon
(ConOfAbs a -> ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
-> AbsToCon (ConOfAbs a)
-> AbsToCon (ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
tm AbsToCon (ConOfAbs a -> (ConOfAbs a, ConOfAbs a, ConOfAbs a))
-> AbsToCon (ConOfAbs a)
-> AbsToCon (ConOfAbs a, ConOfAbs a, ConOfAbs a)
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
ty) [(a, a, a)]
cs
toConcrete (ResolveInstanceOF QName
q) = ConOfAbs (OutputConstraint a b)
-> AbsToCon (ConOfAbs (OutputConstraint a b))
forall a. a -> AbsToCon a
forall (m :: * -> *) a. Monad m => a -> m a
return (ConOfAbs (OutputConstraint a b)
-> AbsToCon (ConOfAbs (OutputConstraint a b)))
-> ConOfAbs (OutputConstraint a b)
-> AbsToCon (ConOfAbs (OutputConstraint a b))
forall a b. (a -> b) -> a -> b
$ QName -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. QName -> OutputConstraint_boot tcErr a b
ResolveInstanceOF QName
q
toConcrete (PTSInstance b
a b
b) = ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> b -> OutputConstraint_boot tcErr a b
PTSInstance (ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
a AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
b
toConcrete (DataSort QName
a b
b) = QName
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. QName -> b -> OutputConstraint_boot tcErr a b
DataSort QName
a (ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
b
toConcrete (CheckLock b
a b
b) = ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. b -> b -> OutputConstraint_boot tcErr a b
CheckLock (ConOfAbs b
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
a AbsToCon
(ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
b
toConcrete (PostponedCheckFunDef QName
q a
a TCErr
err) = QName
-> ConOfAbs a
-> TCErr
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b.
QName -> a -> tcErr -> OutputConstraint_boot tcErr a b
PostponedCheckFunDef QName
q (ConOfAbs a
-> TCErr -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon
(TCErr -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete a
a AbsToCon
(TCErr -> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon TCErr
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TCErr -> AbsToCon TCErr
forall a. a -> AbsToCon a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TCErr
err
toConcrete (UsableAtMod Modality
a b
b) = Modality
-> ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b)
forall tcErr a b. Modality -> b -> OutputConstraint_boot tcErr a b
UsableAtMod Modality
a (ConOfAbs b
-> OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon (OutputConstraint_boot TCErr (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
b
instance (Pretty a, Pretty b) => Pretty (OutputConstraint' a b) where
pretty :: OutputConstraint' a b -> Doc
pretty (OfType' b
e a
t) = b -> Doc
forall a. Pretty a => a -> Doc
pretty b
e Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
":" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
t
instance (ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b) where
type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)
toConcrete :: OutputConstraint' a b
-> AbsToCon (ConOfAbs (OutputConstraint' a b))
toConcrete (OfType' b
e a
t) = ConOfAbs b
-> ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b)
forall a b. b -> a -> OutputConstraint' a b
OfType' (ConOfAbs b
-> ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs b)
-> AbsToCon
(ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b -> AbsToCon (ConOfAbs b)
forall a. ToConcrete a => a -> AbsToCon (ConOfAbs a)
toConcrete b
e AbsToCon
(ConOfAbs a -> OutputConstraint' (ConOfAbs a) (ConOfAbs b))
-> AbsToCon (ConOfAbs a)
-> AbsToCon (OutputConstraint' (ConOfAbs a) (ConOfAbs b))
forall a b. AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx a
t
instance Reify a => Reify (IPBoundary' a) where
type ReifiesTo (IPBoundary' a) = IPBoundary' (ReifiesTo a)
reify :: forall (m :: * -> *).
MonadReify m =>
IPBoundary' a -> m (ReifiesTo (IPBoundary' a))
reify = (a -> m (ReifiesTo a))
-> IPBoundary' a -> m (IPBoundary' (ReifiesTo a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> IPBoundary' a -> f (IPBoundary' b)
traverse a -> m (ReifiesTo a)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => a -> m (ReifiesTo a)
reify
instance ToConcrete a => ToConcrete (IPBoundary' a) where
type ConOfAbs (IPBoundary' a) = IPBoundary' (ConOfAbs a)
toConcrete :: IPBoundary' a -> AbsToCon (ConOfAbs (IPBoundary' a))
toConcrete = (a -> AbsToCon (ConOfAbs a))
-> IPBoundary' a -> AbsToCon (IPBoundary' (ConOfAbs a))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> IPBoundary' a -> f (IPBoundary' b)
traverse (Precedence -> a -> AbsToCon (ConOfAbs a)
forall a. ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a)
toConcreteCtx Precedence
TopCtx)
instance Pretty c => Pretty (IPFace' c) where
pretty :: IPFace' c -> Doc
pretty (IPFace' [(c, c)]
eqs c
val) = do
let
xs :: [Doc]
xs = ((c, c) -> Doc) -> [(c, c)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (c
l,c
r) -> c -> Doc
forall a. Pretty a => a -> Doc
pretty c
l Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"=" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> c -> Doc
forall a. Pretty a => a -> Doc
pretty c
r) [(c, c)]
eqs
[Doc] -> Doc
forall {a}. Pretty a => [a] -> Doc
prettyList_ [Doc]
xs Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"⊢" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> c -> Doc
forall a. Pretty a => a -> Doc
pretty c
val
prettyConstraints :: [Closure Constraint] -> TCM [OutputForm C.Expr C.Expr]
prettyConstraints :: [Closure Constraint] -> TCM [OutputForm Expr Expr]
prettyConstraints [Closure Constraint]
cs = do
[Closure Constraint]
-> (Closure Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Closure Constraint]
cs ((Closure Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr])
-> (Closure Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ \ Closure Constraint
c -> do
cl <- ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify (Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
forall a. Set a
Set.empty Blocker
alwaysUnblock Closure Constraint
c)
enterClosure cl abstractToConcrete_
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 a. a -> TCMT IO a
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 :: forall a. OutputConstraint Expr a -> a
namedMetaOf (OfType a
i Expr
_) = a
i
namedMetaOf (JustType a
i) = a
i
namedMetaOf (JustSort a
i) = a
i
namedMetaOf (Assign a
i Expr
_) = a
i
namedMetaOf OutputConstraint_boot TCErr Expr a
_ = a
forall a. HasCallStack => a
__IMPOSSIBLE__
getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm C.Expr C.Expr]
getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm Expr Expr]
getConstraintsMentioning Rewrite
norm MetaId
m = (ProblemConstraint -> 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 b
p
= Lens' TCState Bool -> (Bool -> Bool) -> m b -> m b
forall a b. Lens' TCState a -> (a -> a) -> m b -> m b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stInstantiateBlocking (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
True) (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$
b -> m b
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull b
p
nay :: MaybeT TCM Elims
nay :: MaybeT (TCMT IO) Elims
nay = TCM (Maybe Elims) -> MaybeT (TCMT IO) Elims
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCM (Maybe Elims) -> MaybeT (TCMT IO) Elims)
-> TCM (Maybe Elims) -> MaybeT (TCMT IO) Elims
forall a b. (a -> b) -> a -> b
$ Maybe Elims -> TCM (Maybe Elims)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Elims
forall a. Maybe a
Nothing
hasHeadMeta :: Constraint -> Maybe Elims
hasHeadMeta Constraint
c =
case Constraint
c of
ValueCmp Comparison
_ CompareAs
_ Term
u Term
v -> Term -> Maybe Elims
isMeta Term
u Maybe Elims -> Maybe Elims -> Maybe Elims
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Maybe Elims
isMeta Term
v
ValueCmpOnFace Comparison
cmp Term
p Type
t Term
u Term
v -> Term -> Maybe Elims
isMeta Term
u Maybe Elims -> Maybe Elims -> Maybe Elims
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Maybe Elims
isMeta Term
v
ElimCmp [Polarity]
cmp [IsForced]
fs Type
t Term
v Elims
as Elims
bs -> Maybe Elims
forall a. Maybe a
Nothing
LevelCmp Comparison
cmp Level
u Level
v -> Maybe Elims
forall a. Maybe a
Nothing
SortCmp Comparison
cmp Sort
a Sort
b -> Maybe Elims
forall a. Maybe a
Nothing
UnBlock{} -> Maybe Elims
forall a. Maybe a
Nothing
FindInstance{} -> Maybe Elims
forall a. Maybe a
Nothing
ResolveInstanceHead{} -> Maybe Elims
forall a. Maybe a
Nothing
IsEmpty Range
r Type
t -> Term -> Maybe Elims
isMeta (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t)
CheckSizeLtSat Term
t -> Term -> Maybe Elims
isMeta Term
t
CheckFunDef{} -> Maybe Elims
forall a. Maybe a
Nothing
HasBiggerSort Sort
a -> Maybe Elims
forall a. Maybe a
Nothing
HasPTSRule Dom Type
a Abs Sort
b -> Maybe Elims
forall a. Maybe a
Nothing
UnquoteTactic{} -> Maybe Elims
forall a. Maybe a
Nothing
CheckDataSort QName
_ Sort
s -> Sort -> Maybe Elims
isMetaS Sort
s
CheckMetaInst{} -> Maybe Elims
forall a. Maybe a
Nothing
CheckType Type
t -> Term -> Maybe Elims
isMeta (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t)
CheckLockedVars Term
t Type
_ Arg Term
_ Type
_ -> Term -> Maybe Elims
isMeta Term
t
UsableAtModality WhyCheckModality
_ Maybe Sort
ms Modality
_ Term
t -> Maybe Sort -> Maybe Elims -> (Sort -> Maybe Elims) -> Maybe Elims
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Sort
ms (Term -> Maybe Elims
isMeta Term
t) ((Sort -> Maybe Elims) -> Maybe Elims)
-> (Sort -> Maybe Elims) -> Maybe Elims
forall a b. (a -> b) -> a -> b
$ \ Sort
s -> Sort -> Maybe Elims
isMetaS Sort
s Maybe Elims -> Maybe Elims -> Maybe Elims
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Term -> Maybe Elims
isMeta Term
t
isMeta :: Term -> Maybe Elims
isMeta :: Term -> Maybe Elims
isMeta (MetaV MetaId
m' Elims
es_m) | MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m' = Elims -> Maybe Elims
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elims
es_m
isMeta Term
_ = Maybe Elims
forall a. Maybe a
Nothing
isMetaS :: I.Sort -> Maybe Elims
isMetaS :: Sort -> Maybe Elims
isMetaS (MetaS MetaId
m' Elims
es_m)
| MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m' = Elims -> Maybe Elims
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Elims
es_m
isMetaS Sort
_ = Maybe Elims
forall a. Maybe a
Nothing
getConstrs :: (ProblemConstraint -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getConstrs ProblemConstraint -> TCM ProblemConstraint
g ProblemConstraint -> Bool
f = TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr])
-> TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ do
cs <- Constraints -> Constraints
stripConstraintPids (Constraints -> Constraints)
-> (Constraints -> Constraints) -> Constraints -> Constraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Bool) -> Constraints -> Constraints
forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
f (Constraints -> Constraints)
-> TCMT IO Constraints -> TCMT IO Constraints
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ProblemConstraint -> TCM ProblemConstraint)
-> Constraints -> TCMT IO Constraints
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ProblemConstraint -> 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)
cs <- caseMaybeM (traverse lookupInteractionPoint =<< isInteractionMeta m) (pure cs) $ \InteractionPoint
ip -> do
let
boundary :: Set (IntMap Bool)
boundary = Map (IntMap Bool) Term -> Set (IntMap Bool)
forall k a. Map k a -> Set k
MapS.keysSet (IPBoundary' Term -> Map (IntMap Bool) Term
forall t. IPBoundary' t -> Map (IntMap Bool) t
getBoundary (InteractionPoint -> IPBoundary' Term
ipBoundary InteractionPoint
ip))
isRedundant :: Constraint -> TCMT IO Bool
isRedundant Constraint
c = case Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims (Elims -> Maybe Args) -> Maybe Elims -> Maybe Args
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Constraint -> Maybe Elims
hasHeadMeta Constraint
c of
Just Args
apps -> TCMT
IO (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
-> TCMT IO Bool
-> ((MetaVariable, IntMap Bool, SubstCand, Substitution)
-> TCMT IO Bool)
-> TCMT IO Bool
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (MetaId
-> Args
-> TCMT
IO (Maybe (MetaVariable, IntMap Bool, SubstCand, Substitution))
isFaceConstraint MetaId
m Args
apps) (Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) (((MetaVariable, IntMap Bool, SubstCand, Substitution)
-> TCMT IO Bool)
-> TCMT IO Bool)
-> ((MetaVariable, IntMap Bool, SubstCand, Substitution)
-> TCMT IO Bool)
-> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ \(MetaVariable
_, IntMap Bool
endps, SubstCand
_, Substitution
_) ->
Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ IntMap Bool -> Set (IntMap Bool) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member IntMap Bool
endps Set (IntMap Bool)
boundary
Maybe Args
Nothing -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
(ProblemConstraint -> TCMT IO Bool)
-> Constraints -> TCMT IO Constraints
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM ((Closure Constraint
-> (Constraint -> TCMT IO Bool) -> TCMT IO Bool)
-> (Constraint -> TCMT IO Bool)
-> Closure Constraint
-> TCMT IO Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Closure Constraint -> (Constraint -> TCMT IO Bool) -> TCMT IO Bool
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure ((Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (TCMT IO Bool -> TCMT IO Bool)
-> (Constraint -> TCMT IO Bool) -> Constraint -> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> TCMT IO Bool
isRedundant) (Closure Constraint -> TCMT IO Bool)
-> (ProblemConstraint -> Closure Constraint)
-> ProblemConstraint
-> TCMT IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Closure Constraint
theConstraint) Constraints
cs
reportSDoc "tc.constr.mentioning" 20 $ "getConstraintsMentioning"
forM cs $ \(PConstr Set ProblemId
s Blocker
ub Closure Constraint
c) -> do
ArgName -> Int -> TCMT IO Doc -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.constr.mentioning" Int
20 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"constraint: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Closure Constraint -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Closure Constraint -> m Doc
prettyTCM Closure Constraint
c
c <- Rewrite -> Closure Constraint -> TCM (Closure Constraint)
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm Closure Constraint
c
let hm = Constraint -> Maybe Elims
hasHeadMeta (Closure Constraint -> Constraint
forall a. Closure a -> a
clValue Closure Constraint
c)
reportSDoc "tc.constr.mentioning" 20 $ "constraint: " TP.<+> prettyTCM c
reportSDoc "tc.constr.mentioning" 20 $ "hasHeadMeta: " TP.<+> prettyTCM hm
case allApplyElims =<< hm of
Just Args
as_m -> do
MetaId
-> Args
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall a.
MetaId
-> Args
-> Closure Constraint
-> ([(Term, Term)] -> Constraint -> TCM a)
-> TCM a
unifyElimsMeta MetaId
m Args
as_m Closure Constraint
c (([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr))
-> ([(Term, Term)] -> Constraint -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall a b. (a -> b) -> a -> b
$ \ [(Term, Term)]
eqs Constraint
c -> do
(Closure (OutputForm Expr Expr)
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr))
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> Closure (OutputForm Expr Expr)
-> TCMT IO (OutputForm Expr Expr)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Closure (OutputForm Expr Expr)
-> (OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall (m :: * -> *) c a b.
(MonadTCEnv m, ReadTCState m, LensClosure c a) =>
c -> (a -> m b) -> m b
enterClosure OutputForm Expr Expr -> TCMT IO (OutputForm Expr Expr)
OutputForm Expr Expr -> TCMT IO (ConOfAbs (OutputForm Expr Expr))
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ (Closure (OutputForm Expr Expr) -> TCMT IO (OutputForm Expr Expr))
-> TCMT IO (Closure (OutputForm Expr Expr))
-> TCMT IO (OutputForm Expr Expr)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr))
ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify (ProblemConstraint -> TCMT IO (Closure (OutputForm Expr Expr)))
-> (Closure Constraint -> ProblemConstraint)
-> Closure Constraint
-> TCMT IO (Closure (OutputForm Expr Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
s Blocker
ub (Closure Constraint -> TCMT IO (Closure (OutputForm Expr Expr)))
-> TCM (Closure Constraint)
-> TCMT IO (Closure (OutputForm Expr Expr))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Constraint -> TCM (Closure Constraint)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure Constraint
c
Maybe Args
_ -> do
cl <- ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify (ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint))
-> ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall a b. (a -> b) -> a -> b
$ Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr Set ProblemId
s Blocker
ub Closure Constraint
c
enterClosure cl abstractToConcrete_
stripConstraintPids :: Constraints -> Constraints
stripConstraintPids :: Constraints -> Constraints
stripConstraintPids Constraints
cs = (ProblemConstraint -> ProblemConstraint -> Ordering)
-> Constraints -> Constraints
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Bool -> Bool -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Bool -> Bool -> Ordering)
-> (ProblemConstraint -> Bool)
-> ProblemConstraint
-> ProblemConstraint
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ProblemConstraint -> Bool
isBlocked) (Constraints -> Constraints) -> Constraints -> Constraints
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> ProblemConstraint)
-> Constraints -> Constraints
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> ProblemConstraint
stripPids Constraints
cs
where
isBlocked :: ProblemConstraint -> Bool
isBlocked = Bool -> Bool
not (Bool -> Bool)
-> (ProblemConstraint -> Bool) -> ProblemConstraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set ProblemId -> Bool
forall a. Null a => a -> Bool
null (Set ProblemId -> Bool)
-> (ProblemConstraint -> Set ProblemId)
-> ProblemConstraint
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Blocker -> Set ProblemId
allBlockingProblems (Blocker -> Set ProblemId)
-> (ProblemConstraint -> Blocker)
-> ProblemConstraint
-> Set ProblemId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker
interestingPids :: Set ProblemId
interestingPids = [Set ProblemId] -> Set ProblemId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set ProblemId] -> Set ProblemId)
-> [Set ProblemId] -> Set ProblemId
forall a b. (a -> b) -> a -> b
$ (ProblemConstraint -> Set ProblemId)
-> Constraints -> [Set ProblemId]
forall a b. (a -> b) -> [a] -> [b]
map (Blocker -> Set ProblemId
allBlockingProblems (Blocker -> Set ProblemId)
-> (ProblemConstraint -> Blocker)
-> ProblemConstraint
-> Set ProblemId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemConstraint -> Blocker
constraintUnblocker) Constraints
cs
stripPids :: ProblemConstraint -> ProblemConstraint
stripPids (PConstr Set ProblemId
pids Blocker
unblock Closure Constraint
c) = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set ProblemId
pids Set ProblemId
interestingPids) Blocker
unblock Closure Constraint
c
{-# SPECIALIZE interactionIdToMetaId :: InteractionId -> TCM MetaId #-}
interactionIdToMetaId :: ReadTCState m => InteractionId -> m MetaId
interactionIdToMetaId :: forall (m :: * -> *). ReadTCState m => InteractionId -> m MetaId
interactionIdToMetaId InteractionId
i = do
h <- m ModuleNameHash
forall (m :: * -> *). ReadTCState m => m ModuleNameHash
currentModuleNameHash
return MetaId
{ metaId = fromIntegral i
, metaModule = h
}
getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm C.Expr C.Expr]
getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint)
-> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
getConstraints' ProblemConstraint -> TCM ProblemConstraint
g ProblemConstraint -> Bool
f = TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr])
-> TCM [OutputForm Expr Expr] -> TCM [OutputForm Expr Expr]
forall a b. (a -> b) -> a -> b
$ do
cs <- Constraints -> Constraints
stripConstraintPids (Constraints -> Constraints)
-> (Constraints -> Constraints) -> Constraints -> Constraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProblemConstraint -> Bool) -> Constraints -> Constraints
forall a. (a -> Bool) -> [a] -> [a]
filter ProblemConstraint -> Bool
f (Constraints -> Constraints)
-> TCMT IO Constraints -> TCMT IO Constraints
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ProblemConstraint -> TCM ProblemConstraint)
-> Constraints -> TCMT IO Constraints
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ProblemConstraint -> 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)
cs <- forM cs $ \ProblemConstraint
c -> do
cl <- ProblemConstraint -> TCMT IO (ReifiesTo ProblemConstraint)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *).
MonadReify m =>
ProblemConstraint -> m (ReifiesTo ProblemConstraint)
reify ProblemConstraint
c
enterClosure cl abstractToConcrete_
ss <- mapM toOutputForm =<< getSolvedInteractionPoints True AsIs
return $ ss ++ cs
where
toOutputForm :: (InteractionId, MetaId, Expr) -> m (OutputForm Expr Expr)
toOutputForm (InteractionId
ii, MetaId
mi, Expr
e) = do
mv <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> m MetaVariable -> m (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
withMetaInfo mv $ do
mi <- interactionIdToMetaId ii
let m = MetaInfo -> InteractionId -> Expr
QuestionMark MetaInfo
emptyMetaInfo{ metaNumber = Just mi } InteractionId
ii
let oform = Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr Expr Expr
-> OutputForm Expr Expr
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock (OutputConstraint_boot TCErr Expr Expr -> OutputForm Expr Expr)
-> OutputConstraint_boot TCErr Expr Expr -> OutputForm Expr Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> OutputConstraint_boot TCErr Expr Expr
forall tcErr a b. b -> a -> OutputConstraint_boot tcErr a b
Assign Expr
m Expr
e :: OutputForm Expr Expr
abstractToConcrete_ oform
getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' C.Expr]
getIPBoundary :: Rewrite -> InteractionId -> TCM [IPFace' Expr]
getIPBoundary Rewrite
norm InteractionId
ii = InteractionId -> TCM [IPFace' Expr] -> TCM [IPFace' Expr]
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM [IPFace' Expr] -> TCM [IPFace' Expr])
-> TCM [IPFace' Expr] -> TCM [IPFace' Expr]
forall a b. (a -> b) -> a -> b
$ do
ip <- InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
io <- primIOne
iz <- primIZero
lookupInteractionMeta ii >>= \case
Just MetaId
mi -> do
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
let t = Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv
telv@(TelV tel a) <- telView t
reportSDoc "tc.ip.boundary" 30 $ TP.vcat
[ "reifying interaction point boundary"
, "tel: " TP.<+> prettyTCM tel
, "meta: " TP.<+> prettyTCM mi
]
reportSDoc "tc.ip.boundary" 30 $ "boundary: " TP.<+> pure (pretty (getBoundary (ipBoundary ip)))
withInteractionId ii $ do
as <- getContextArgs
let
c = Expr -> TCM Expr
Expr -> TCMT IO (ConOfAbs Expr)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ (Expr -> TCM Expr) -> (Term -> TCM Expr) -> Term -> TCM Expr
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> TCM Expr
Term -> TCMT IO (ReifiesTo Term)
forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked (Term -> TCM Expr) -> (Term -> TCM Term) -> Term -> TCM Expr
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Rewrite -> Term -> TCM Term
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm
go (IntMap Bool
im, Term
rhs) = do
ArgName -> Int -> TCMT IO Doc -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip.boundary" Int
30 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.vcat
[ TCMT IO Doc
"reifying constraint for face" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> IntMap Bool -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
TP.pretty IntMap Bool
im
]
ArgName -> Int -> TCMT IO Doc -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip.boundary" Int
30 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"term " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
TP.prettyTCM Term
rhs
rhs <- Term -> TCM Expr
c (Term
rhs Term -> Args -> Term
forall t. Apply t => t -> Args -> t
`apply` Args
as)
eqns <- forM (IntMap.toList im) $ \(Int
a, Bool
b) -> do
a <- Term -> TCM Expr
c (Int -> Elims -> Term
I.Var Int
a [])
(,) a <$> c (if b then io else iz)
pure $ IPFace' eqns rhs
traverse go $ MapS.toList (getBoundary (ipBoundary ip))
Maybe MetaId
Nothing -> [IPFace' Expr] -> TCM [IPFace' Expr]
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' C.Expr])
typeAndFacesInMeta :: InteractionId -> Rewrite -> Expr -> TCM (Expr, [IPFace' Expr])
typeAndFacesInMeta InteractionId
ii Rewrite
norm Expr
expr = InteractionId
-> TCM (Expr, [IPFace' Expr]) -> TCM (Expr, [IPFace' Expr])
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM (Expr, [IPFace' Expr]) -> TCM (Expr, [IPFace' Expr]))
-> TCM (Expr, [IPFace' Expr]) -> TCM (Expr, [IPFace' Expr])
forall a b. (a -> b) -> a -> b
$ do
(ex, ty) <- Expr -> TCM (Term, Type)
inferExpr Expr
expr
ty <- normalForm norm ty
ip <- lookupInteractionPoint ii
io <- primIOne
iz <- primIZero
let
go IntMap Bool
im = do
let
c :: Term -> TCM Expr
c = Expr -> TCM Expr
Expr -> TCMT IO (ConOfAbs Expr)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ (Expr -> TCM Expr) -> (Term -> TCM Expr) -> Term -> TCM Expr
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Term -> TCM Expr
Term -> TCMT IO (ReifiesTo Term)
forall i. Reify i => i -> TCM (ReifiesTo i)
reifyUnblocked (Term -> TCM Expr) -> (Term -> TCM Term) -> Term -> TCM Expr
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Rewrite -> Term -> TCM Term
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm
fa :: [(Int, Bool)]
fa = IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Bool
im
face :: (Int, Bool) -> Substitution
face (Int
i, Bool
m) = Int -> Term -> Substitution
forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
i (Term -> Substitution) -> Term -> Substitution
forall a b. (a -> b) -> a -> b
$ if Bool
m then Term
io else Term
iz
sub :: Substitution
sub = ((Int, Bool) -> Substitution -> Substitution)
-> Substitution -> [(Int, Bool)] -> Substitution
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Int, Bool)
f Substitution
s -> Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
composeS ((Int, Bool) -> Substitution
face (Int, Bool)
f) Substitution
s) Substitution
forall a. Substitution' a
idS [(Int, Bool)]
fa
eqns <- [(Int, Bool)]
-> ((Int, Bool) -> TCMT IO (Expr, Expr)) -> TCMT IO [(Expr, Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, Bool)]
fa (((Int, Bool) -> TCMT IO (Expr, Expr)) -> TCMT IO [(Expr, Expr)])
-> ((Int, Bool) -> TCMT IO (Expr, Expr)) -> TCMT IO [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$ \(Int
a, Bool
b) -> do
a <- Term -> TCM Expr
c (Int -> Elims -> Term
I.Var Int
a [])
(,) a <$> c (if b then io else iz)
fmap (IPFace' eqns) . c =<< simplify (applySubst sub ex)
faces <- traverse go $ MapS.keys (getBoundary (ipBoundary ip))
ty <- reifyUnblocked ty
pure (ty, faces)
getGoals :: TCM Goals
getGoals :: TCM Goals
getGoals = Rewrite -> Rewrite -> TCM Goals
getGoals' Rewrite
AsIs Rewrite
Simplified
getGoals'
:: Rewrite
-> Rewrite
-> TCM Goals
getGoals' :: Rewrite -> Rewrite -> TCM Goals
getGoals' Rewrite
normVisible Rewrite
normHidden = do
visibleMetas <- Rewrite -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
typesOfVisibleMetas Rewrite
normVisible
hiddenMetas <- typesOfHiddenMetas normHidden
return (visibleMetas, hiddenMetas)
showGoals :: Goals -> TCM String
showGoals :: Goals -> TCM ArgName
showGoals ([OutputConstraint_boot TCErr Expr InteractionId]
ims, [OutputConstraint Expr NamedMeta]
hms) = do
di <- [OutputConstraint_boot TCErr Expr InteractionId]
-> (OutputConstraint_boot TCErr Expr InteractionId -> TCMT IO Doc)
-> TCMT IO [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [OutputConstraint_boot TCErr Expr InteractionId]
ims ((OutputConstraint_boot TCErr Expr InteractionId -> TCMT IO Doc)
-> TCMT IO [Doc])
-> (OutputConstraint_boot TCErr Expr InteractionId -> TCMT IO Doc)
-> TCMT IO [Doc]
forall a b. (a -> b) -> a -> b
$ \ OutputConstraint_boot TCErr Expr InteractionId
i ->
InteractionId -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (OutputForm Expr InteractionId -> InteractionId
forall a b. OutputForm a b -> b
outputFormId (OutputForm Expr InteractionId -> InteractionId)
-> OutputForm Expr InteractionId -> InteractionId
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot TCErr Expr InteractionId
-> OutputForm Expr InteractionId
forall tcErr a b.
Range
-> [ProblemId]
-> Blocker
-> OutputConstraint_boot tcErr a b
-> OutputForm_boot tcErr a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
alwaysUnblock OutputConstraint_boot TCErr Expr InteractionId
i) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
OutputConstraint_boot TCErr Expr InteractionId -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint_boot TCErr Expr InteractionId
i
dh <- mapM showA' hms
return $ unlines $ map show di ++ dh
where
showA' :: OutputConstraint A.Expr NamedMeta -> TCM String
showA' :: OutputConstraint Expr NamedMeta -> TCM ArgName
showA' OutputConstraint Expr NamedMeta
m = do
let i :: MetaId
i = NamedMeta -> MetaId
nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
forall a b. (a -> b) -> a -> b
$ OutputConstraint Expr NamedMeta -> NamedMeta
forall a. OutputConstraint Expr a -> a
namedMetaOf OutputConstraint Expr NamedMeta
m
r <- MetaId -> TCMT IO Range
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Range
getMetaRange MetaId
i
d <- withMetaId i (prettyATop m)
return $ show d ++ " [ at " ++ prettyShow r ++ " ]"
getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
getWarningsAndNonFatalErrors = do
mws <- WhichWarnings -> TCMT IO [TCWarning]
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadWarning m, MonadTCM m) =>
WhichWarnings -> m [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
let 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]
mws
return $ case notMetaWarnings of
ws :: [TCWarning]
ws@(TCWarning
_:[TCWarning]
_) -> [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings [TCWarning]
ws
[TCWarning]
_ -> WarningsAndNonFatalErrors
emptyWarningsAndNonFatalErrors
getResponseContext
:: Rewrite
-> InteractionId
-> TCM [ResponseContextEntry]
getResponseContext :: Rewrite -> InteractionId -> TCM [ResponseContextEntry]
getResponseContext Rewrite
norm 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 Bool
all Rewrite
norm = [[(InteractionId, MetaId, Expr)]]
-> [(InteractionId, MetaId, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(InteractionId, MetaId, Expr)]]
-> [(InteractionId, MetaId, Expr)])
-> TCMT IO [[(InteractionId, MetaId, Expr)]]
-> TCMT IO [(InteractionId, MetaId, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
((InteractionId, MetaId)
-> TCMT IO [(InteractionId, MetaId, Expr)])
-> [(InteractionId, MetaId)]
-> TCMT IO [[(InteractionId, MetaId, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (InteractionId, MetaId) -> TCMT IO [(InteractionId, MetaId, Expr)]
solution ([(InteractionId, MetaId)]
-> TCMT IO [[(InteractionId, MetaId, Expr)]])
-> TCMT IO [(InteractionId, MetaId)]
-> TCMT IO [[(InteractionId, MetaId, Expr)]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [(InteractionId, MetaId)]
forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas
where
solution :: (InteractionId, MetaId) -> TCMT IO [(InteractionId, MetaId, Expr)]
solution (InteractionId
i, MetaId
m) = do
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
withMetaInfo (getMetaInfo mv) $ do
args <- getContextArgs
scope <- getScope
let sol Term
v = do
v <- Term -> TCM Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
v
let isMeta = case Term
v of MetaV{} -> Bool
True; Term
_ -> Bool
False
if isMeta && not all then return [] else do
e <- blankNotInScope =<< reify =<< normalForm norm v
return [(i, m, ScopedExpr scope e)]
unsol = [a] -> TCMT IO [a]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
case mvInstantiation mv of
InstV{} -> Term -> TCMT IO [(InteractionId, MetaId, Expr)]
sol (MetaId -> Elims -> Term
MetaV MetaId
m (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply Args
args)
OpenMeta{} -> TCMT IO [(InteractionId, MetaId, Expr)]
forall {a}. TCMT IO [a]
unsol
BlockedConst{} -> TCMT IO [(InteractionId, MetaId, Expr)]
forall {a}. TCMT IO [a]
unsol
PostponedTypeCheckingProblem{} -> TCMT IO [(InteractionId, MetaId, Expr)]
forall {a}. TCMT IO [a]
unsol
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI Rewrite
norm MetaId
mi =
do mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
mi
withMetaInfo (getMetaInfo mv) $
rewriteJudg mv (mvJudgement mv)
where
rewriteJudg :: MetaVariable -> Judgement MetaId ->
TCM (OutputConstraint Expr NamedMeta)
rewriteJudg :: MetaVariable
-> Judgement MetaId -> TCM (OutputConstraint Expr NamedMeta)
rewriteJudg MetaVariable
mv (HasType MetaId
i Comparison
cmp Type
t) = do
ms <- MetaId -> TCM ArgName
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m ArgName
getMetaNameSuggestion MetaId
i
vs <- getContextArgs
t <- t `piApplyM` permute (takeP (size vs) $ mvPermutation mv) vs
t <- normalForm norm t
let x = ArgName -> MetaId -> NamedMeta
NamedMeta ArgName
ms MetaId
i
reportSDoc "interactive.meta" 10 $ TP.vcat
[ TP.text $ unwords ["permuting", show i, "with", show $ mvPermutation mv]
, TP.nest 2 $ TP.vcat
[ "len =" TP.<+> TP.text (show $ length vs)
, "args =" TP.<+> prettyTCM vs
, "t =" TP.<+> prettyTCM t
, "x =" TP.<+> TP.pretty x
]
]
reportSDoc "interactive.meta.scope" 20 $ TP.text $ show $ getMetaScope mv
OfType x <$> reifyUnblocked t
rewriteJudg MetaVariable
mv (IsSort MetaId
i Type
t) = do
ms <- MetaId -> TCM ArgName
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m ArgName
getMetaNameSuggestion MetaId
i
return $ JustSort $ NamedMeta ms i
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta :: Rewrite
-> InteractionId
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
typeOfMeta Rewrite
norm InteractionId
ii = Rewrite
-> (InteractionId, MetaId)
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
typeOfMeta' Rewrite
norm ((InteractionId, MetaId)
-> TCM (OutputConstraint_boot TCErr Expr InteractionId))
-> (MetaId -> (InteractionId, MetaId))
-> MetaId
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionId
ii,) (MetaId -> TCM (OutputConstraint_boot TCErr Expr InteractionId))
-> TCMT IO MetaId
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(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_boot TCErr Expr InteractionId)
typeOfMeta' Rewrite
norm (InteractionId
ii, MetaId
mi) = (NamedMeta -> InteractionId)
-> OutputConstraint Expr NamedMeta
-> OutputConstraint_boot TCErr Expr InteractionId
forall a b.
(a -> b)
-> OutputConstraint_boot TCErr Expr a
-> OutputConstraint_boot TCErr Expr b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\NamedMeta
_ -> InteractionId
ii) (OutputConstraint Expr NamedMeta
-> OutputConstraint_boot TCErr Expr InteractionId)
-> TCM (OutputConstraint Expr NamedMeta)
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMetaMI Rewrite
norm MetaId
mi
typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint_boot TCErr Expr InteractionId]
typesOfVisibleMetas Rewrite
norm =
TCM [OutputConstraint_boot TCErr Expr InteractionId]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [OutputConstraint_boot TCErr Expr InteractionId]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId])
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
forall a b. (a -> b) -> a -> b
$ ((InteractionId, MetaId)
-> TCM (OutputConstraint_boot TCErr Expr InteractionId))
-> [(InteractionId, MetaId)]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Rewrite
-> (InteractionId, MetaId)
-> TCM (OutputConstraint_boot TCErr Expr InteractionId)
typeOfMeta' Rewrite
norm) ([(InteractionId, MetaId)]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId])
-> TCMT IO [(InteractionId, MetaId)]
-> TCM [OutputConstraint_boot TCErr Expr InteractionId]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [(InteractionId, MetaId)]
forall (m :: * -> *). ReadTCState m => m [(InteractionId, MetaId)]
getInteractionIdsAndMetas
typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas Rewrite
norm = TCM [OutputConstraint Expr NamedMeta]
-> TCM [OutputConstraint Expr NamedMeta]
forall a. TCM a -> TCM a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [OutputConstraint Expr NamedMeta]
-> TCM [OutputConstraint Expr NamedMeta])
-> TCM [OutputConstraint Expr NamedMeta]
-> TCM [OutputConstraint Expr NamedMeta]
forall a b. (a -> b) -> a -> b
$ do
is <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
store <- MapS.filterWithKey (implicit is) <$> useR stOpenMetaStore
mapM (typeOfMetaMI norm) $ MapS.keys store
where
implicit :: t a -> a -> MetaVariable -> Bool
implicit t a
is a
x MetaVariable
m | Maybe MetaId -> Bool
forall a. Maybe a -> Bool
isJust (MetaVariable -> Maybe MetaId
mvTwin MetaVariable
m) = Bool
False
implicit t a
is a
x MetaVariable
m =
case MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
m of
M.InstV{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
M.OpenMeta MetaKind
_ -> a
x a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t a
is
M.BlockedConst{} -> Bool
False
M.PostponedTypeCheckingProblem{} -> Bool
False
metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr)
metaHelperType :: Rewrite
-> InteractionId
-> Range
-> ArgName
-> TCM (OutputConstraint' Expr Expr)
metaHelperType Rewrite
norm InteractionId
ii Range
rng ArgName
s = case ArgName -> Names
words ArgName
s of
[] -> TCM (OutputConstraint' Expr Expr)
forall {a}. TCMT IO a
failure
ArgName
f : Names
_ -> InteractionId
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m 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
ArgName -> ScopeM ()
ensureName ArgName
f
A.Application h 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 -> ArgName -> TCM Expr
parseExprIn InteractionId
ii Range
rng (ArgName
"let " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
f ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
" = _ in " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
s)
inCxt <- hasElem <$> getContextNames
cxtArgs <- getContextArgs
enclosingFunctionName <- ipcQName . envClause <$> getEnv
a0 <- (`piApply` cxtArgs) <$> (getMetaType =<< lookupInteractionId ii)
freeVars <- getCurrentModuleFreeVars
contextForAbstracting <- drop freeVars . reverse <$> getContext
let runInPrintingEnvironment = (TCEnv -> TCEnv) -> TCM Expr -> TCM Expr
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
e -> TCEnv
e { envPrintDomainFreePi = True, envPrintMetasBare = True })
(TCM Expr -> TCM Expr)
-> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Impossible -> Int -> TCM Expr -> TCM Expr
forall (m :: * -> *) a.
MonadAddContext m =>
Impossible -> Int -> m a -> m a
escapeContext Impossible
HasCallStack => Impossible
impossible ([ContextEntry] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ContextEntry]
contextForAbstracting)
(TCM Expr -> TCM Expr)
-> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM Expr -> TCM Expr
forall (m :: * -> *) a. ReadTCState m => m a -> m a
withoutPrintingGeneralization
(TCM Expr -> TCM Expr)
-> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
dontFoldLetBindings
case mapM (isVar . namedArg) args >>= \ [Name]
xs -> [Name]
xs [Name] -> Maybe () -> Maybe [Name]
forall a b. a -> Maybe b -> Maybe a
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 [Name]
xs -> do
let inXs :: Name -> Bool
inXs = [Name] -> Name -> Bool
forall a. Ord a => [a] -> a -> Bool
hasElem [Name]
xs
let hideButXs :: ContextEntry -> ContextEntry
hideButXs ContextEntry
dom = Hiding -> ContextEntry -> ContextEntry
forall a. LensHiding a => Hiding -> a -> a
setHiding (if Name -> Bool
inXs (Name -> Bool) -> Name -> Bool
forall a b. (a -> b) -> a -> b
$ (Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name) -> (Name, Type) -> Name
forall a b. (a -> b) -> a -> b
$ ContextEntry -> (Name, Type)
forall t e. Dom' t e -> e
unDom ContextEntry
dom then Hiding
NotHidden else Hiding
Hidden) ContextEntry
dom
let tel :: Telescope
tel = ListTel -> Telescope
telFromList (ListTel -> Telescope)
-> ([ContextEntry] -> ListTel) -> [ContextEntry] -> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ContextEntry -> Dom (ArgName, Type)) -> [ContextEntry] -> ListTel
forall a b. (a -> b) -> [a] -> [b]
map (((Name, Type) -> (ArgName, Type))
-> ContextEntry -> Dom (ArgName, Type)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name -> ArgName) -> (Name, Type) -> (ArgName, Type)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Name -> ArgName
nameToArgName) (ContextEntry -> Dom (ArgName, Type))
-> (ContextEntry -> ContextEntry)
-> ContextEntry
-> Dom (ArgName, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> ContextEntry
hideButXs) ([ContextEntry] -> Telescope) -> [ContextEntry] -> Telescope
forall a b. (a -> b) -> a -> b
$ [ContextEntry]
contextForAbstracting
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
TCM Expr -> TCM Expr
runInPrintingEnvironment (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ Type -> TCM (ReifiesTo Type)
forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
forall (m :: * -> *). MonadReify m => Type -> m (ReifiesTo Type)
reify (Type -> TCM (ReifiesTo Type)) -> Type -> TCM (ReifiesTo Type)
forall a b. (a -> b) -> a -> b
$ Telescope -> Type -> Type
telePiVisible Telescope
tel Type
a0
Maybe [Name]
Nothing -> do
let tel :: Telescope
tel = Identity Telescope -> Telescope
forall a. Identity a -> a
runIdentity (Identity Telescope -> Telescope)
-> ([ContextEntry] -> Identity Telescope)
-> [ContextEntry]
-> Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgName -> Identity ArgName) -> Telescope -> Identity Telescope
forall (f :: * -> *).
Applicative f =>
(ArgName -> f ArgName) -> Telescope -> f Telescope
onNamesTel ArgName -> Identity ArgName
forall {a} {m :: * -> *}. (Eq a, IsString a, Monad m) => a -> m a
unW (Telescope -> Identity Telescope)
-> ([ContextEntry] -> Telescope)
-> [ContextEntry]
-> Identity Telescope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> ArgName) -> [ContextEntry] -> Telescope
forall a. (a -> ArgName) -> ListTel' a -> Telescope
telFromList' Name -> ArgName
nameToArgName ([ContextEntry] -> Telescope) -> [ContextEntry] -> Telescope
forall a b. (a -> b) -> a -> b
$ [ContextEntry]
contextForAbstracting
let a :: Type
a = Identity Type -> Type
forall a. Identity a -> a
runIdentity (Identity Type -> Type) -> (Type -> Identity Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgName -> Identity ArgName) -> Type -> Identity Type
forall (m :: * -> *).
Applicative m =>
(ArgName -> m ArgName) -> Type -> m Type
onNames ArgName -> Identity ArgName
forall {a} {m :: * -> *}. (Eq a, IsString a, Monad m) => a -> m a
unW (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
a0
vtys <- (NamedArg Expr -> TCMT IO (Arg (Term, EqualityView)))
-> [NamedArg Expr] -> TCMT IO [Arg (Term, EqualityView)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ NamedArg Expr
a -> ((Term, Type) -> Arg (Term, EqualityView))
-> TCM (Term, Type) -> TCMT IO (Arg (Term, EqualityView))
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgInfo -> (Term, EqualityView) -> Arg (Term, EqualityView)
forall e. ArgInfo -> e -> Arg e
Arg (NamedArg Expr -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Expr
a) ((Term, EqualityView) -> Arg (Term, EqualityView))
-> ((Term, Type) -> (Term, EqualityView))
-> (Term, Type)
-> Arg (Term, EqualityView)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> EqualityView) -> (Term, Type) -> (Term, EqualityView)
forall a b. (a -> b) -> (Term, a) -> (Term, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> EqualityView
OtherType) (TCM (Term, Type) -> TCMT IO (Arg (Term, EqualityView)))
-> TCM (Term, Type) -> TCMT IO (Arg (Term, EqualityView))
forall a b. (a -> b) -> a -> b
$ Expr -> TCM (Term, Type)
inferExpr (Expr -> TCM (Term, Type)) -> Expr -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Expr
forall a. NamedArg a -> a
namedArg NamedArg Expr
a) [NamedArg Expr]
args
TelV atel _ <- telView a
let arity = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
atel
(delta1, delta2, _, a', vtys') = splitTelForWith tel a vtys
a <- runInPrintingEnvironment $ do
reify =<< cleanupType arity args =<< normalForm norm =<< fst <$> withFunctionType delta1 vtys' delta2 a' []
reportSDoc "interaction.helper" 10 $ TP.vcat $
let extractOtherType = \case { OtherType Type
a -> Type
a; EqualityView
_ -> Type
forall a. HasCallStack => a
__IMPOSSIBLE__ } in
let (vs, as) = unzipWith (fmap extractOtherType . unArg) vtys in
let (vs', as') = unzipWith (fmap extractOtherType . unArg) vtys' in
[ "generating helper function"
, TP.nest 2 $ "tel = " TP.<+> inTopContext (prettyTCM tel)
, TP.nest 2 $ "a = " TP.<+> prettyTCM a
, TP.nest 2 $ "vs = " TP.<+> prettyTCM vs
, TP.nest 2 $ "as = " TP.<+> prettyTCM as
, TP.nest 2 $ "delta1 = " TP.<+> inTopContext (prettyTCM delta1)
, TP.nest 2 $ "delta2 = " TP.<+> inTopContext (addContext delta1 $ prettyTCM delta2)
, TP.nest 2 $ "a' = " TP.<+> inTopContext (addContext delta1 $ addContext delta2 $ prettyTCM a')
, TP.nest 2 $ "as' = " TP.<+> inTopContext (addContext delta1 $ prettyTCM as')
, TP.nest 2 $ "vs' = " TP.<+> inTopContext (addContext delta1 $ prettyTCM vs')
]
return $ OfType' h a
where
failure :: TCMT IO a
failure = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$ ArgName
"Expected an argument of the form f e1 e2 .. en"
ensureName :: ArgName -> ScopeM ()
ensureName ArgName
f = do
ce <- Range -> ArgName -> TCM Expr
parseExpr Range
rng ArgName
f
flip (caseMaybe $ isName ce) (\ Name
_ -> () -> ScopeM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) $ do
reportSLn "interaction.helper" 10 $ "ce = " ++ show ce
failure
isVar :: A.Expr -> Maybe A.Name
isVar :: Expr -> Maybe Name
isVar = \case
A.Var Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
Expr
_ -> Maybe Name
forall a. Maybe a
Nothing
cleanupType :: Int -> [NamedArg Expr] -> Type -> TCMT IO Type
cleanupType Int
arity [NamedArg Expr]
args Type
t = do
TelV ttel _ <- Type -> TCMT IO TelView
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m TelView
telView Type
t
let n = Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
ttel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
arity
unless (n >= 0) __IMPOSSIBLE__
return $ evalState (renameVars $ stripUnused n t) args
getBody :: Expr -> Expr
getBody (A.Let ExprInfo
_ List1 LetBinding
_ Expr
e) = Expr
e
getBody Expr
_ = Expr
forall a. HasCallStack => a
__IMPOSSIBLE__
stripUnused :: a -> Type -> Type
stripUnused a
n (El Sort
s Term
v) = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ a -> Term -> Term
strip a
n Term
v
strip :: a -> Term -> Term
strip a
0 = Term -> Term
forall a. a -> a
id
strip a
n = \case
I.Pi Dom Type
a Abs Type
b -> case a -> Type -> Type
stripUnused (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) (Type -> Type) -> Abs Type -> Abs Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs Type
b of
Abs Type
b | Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== ArgName
"w" -> Dom Type -> Abs Type -> Term
I.Pi Dom Type
a Abs Type
b
NoAbs ArgName
_ Type
b -> Type -> Term
forall t a. Type'' t a -> a
unEl Type
b
Abs ArgName
s Type
b | Int
0 Int -> Type -> Bool
forall a. Free a => Int -> 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) (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
Abs ArgName
s Type
b)
| Bool
otherwise -> Impossible -> Term -> Term
forall a. Subst a => Impossible -> a -> a
strengthen Impossible
HasCallStack => Impossible
impossible (Type -> Term
forall t a. Type'' t a -> a
unEl Type
b)
Term
v -> Term
v
renameVars :: Type -> State [NamedArg Expr] Type
renameVars = (ArgName -> StateT [NamedArg Expr] Identity ArgName)
-> Type -> State [NamedArg Expr] Type
forall (m :: * -> *).
Applicative m =>
(ArgName -> m ArgName) -> Type -> m Type
onNames ArgName -> StateT [NamedArg Expr] Identity ArgName
renameVar
onNames :: Applicative m => (String -> m String) -> I.Type -> m I.Type
onNames :: forall (m :: * -> *).
Applicative m =>
(ArgName -> m ArgName) -> Type -> m Type
onNames ArgName -> m ArgName
f (El Sort
s Term
v) = 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
<$> (ArgName -> m ArgName) -> Term -> m Term
forall {f :: * -> *}.
Applicative f =>
(ArgName -> f ArgName) -> Term -> f Term
onNamesTm ArgName -> m ArgName
f Term
v
onNamesTel :: Applicative f => (String -> f String) -> I.Telescope -> f I.Telescope
onNamesTel :: forall (f :: * -> *).
Applicative f =>
(ArgName -> f ArgName) -> Telescope -> f Telescope
onNamesTel ArgName -> f ArgName
f Telescope
I.EmptyTel = Telescope -> f Telescope
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Telescope
forall a. Tele a
I.EmptyTel
onNamesTel ArgName -> f ArgName
f (I.ExtendTel Dom Type
a Abs Telescope
b) = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
I.ExtendTel (Dom Type -> Abs Telescope -> Telescope)
-> f (Dom Type) -> f (Abs Telescope -> Telescope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> f Type) -> Dom Type -> f (Dom Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' Term a -> f (Dom' Term b)
traverse ((ArgName -> f ArgName) -> Type -> f Type
forall (m :: * -> *).
Applicative m =>
(ArgName -> m ArgName) -> Type -> m Type
onNames ArgName -> f ArgName
f) Dom Type
a f (Abs Telescope -> Telescope) -> f (Abs Telescope) -> f Telescope
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ArgName -> f ArgName)
-> ((ArgName -> f ArgName) -> Telescope -> f Telescope)
-> Abs Telescope
-> f (Abs Telescope)
forall {f :: * -> *} {t} {a}.
Applicative f =>
(ArgName -> f ArgName)
-> ((ArgName -> f ArgName) -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs ArgName -> f ArgName
f (ArgName -> f ArgName) -> Telescope -> f Telescope
forall (f :: * -> *).
Applicative f =>
(ArgName -> f ArgName) -> Telescope -> f Telescope
onNamesTel Abs Telescope
b
onNamesTm :: (ArgName -> f ArgName) -> Term -> f Term
onNamesTm ArgName -> f ArgName
f = \case
I.Var Int
x Elims
es -> Int -> Elims -> Term
I.Var Int
x (Elims -> Term) -> f Elims -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ArgName -> f ArgName) -> Elims -> f Elims
onNamesElims ArgName -> f ArgName
f Elims
es
I.Def QName
q Elims
es -> QName -> Elims -> Term
I.Def QName
q (Elims -> Term) -> f Elims -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ArgName -> f ArgName) -> Elims -> f Elims
onNamesElims ArgName -> f ArgName
f Elims
es
I.Con ConHead
c ConInfo
ci Elims
args -> ConHead -> ConInfo -> Elims -> Term
I.Con ConHead
c ConInfo
ci (Elims -> Term) -> f Elims -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ArgName -> f ArgName) -> Elims -> f Elims
onNamesArgs ArgName -> f ArgName
f Elims
args
I.Lam ArgInfo
i Abs Term
b -> ArgInfo -> Abs Term -> Term
I.Lam ArgInfo
i (Abs Term -> Term) -> f (Abs Term) -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ArgName -> f ArgName)
-> ((ArgName -> f ArgName) -> Term -> f Term)
-> Abs Term
-> f (Abs Term)
forall {f :: * -> *} {t} {a}.
Applicative f =>
(ArgName -> f ArgName)
-> ((ArgName -> f ArgName) -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs ArgName -> f ArgName
f (ArgName -> f ArgName) -> Term -> f Term
onNamesTm Abs Term
b
I.Pi Dom Type
a Abs Type
b -> Dom Type -> Abs Type -> Term
I.Pi (Dom Type -> Abs Type -> Term)
-> f (Dom Type) -> f (Abs Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> f Type) -> Dom Type -> f (Dom Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Dom' Term a -> f (Dom' Term b)
traverse ((ArgName -> f ArgName) -> Type -> f Type
forall (m :: * -> *).
Applicative m =>
(ArgName -> m ArgName) -> Type -> m Type
onNames ArgName -> f ArgName
f) Dom Type
a f (Abs Type -> Term) -> f (Abs Type) -> f Term
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ArgName -> f ArgName)
-> ((ArgName -> f ArgName) -> Type -> f Type)
-> Abs Type
-> f (Abs Type)
forall {f :: * -> *} {t} {a}.
Applicative f =>
(ArgName -> f ArgName)
-> ((ArgName -> f ArgName) -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs ArgName -> f ArgName
f (ArgName -> f ArgName) -> Type -> f Type
forall (m :: * -> *).
Applicative m =>
(ArgName -> m ArgName) -> Type -> m Type
onNames Abs Type
b
I.DontCare Term
v -> Term -> Term
I.DontCare (Term -> Term) -> f Term -> f Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ArgName -> f ArgName) -> Term -> f Term
onNamesTm ArgName -> f ArgName
f Term
v
v :: Term
v@I.Lit{} -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
v :: Term
v@I.Sort{} -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
v :: Term
v@I.Level{} -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
v :: Term
v@I.MetaV{} -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
v :: Term
v@I.Dummy{} -> Term -> f Term
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
onNamesElims :: (ArgName -> f ArgName) -> Elims -> f Elims
onNamesElims ArgName -> f ArgName
f = (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Elim' Term -> f (Elim' Term)) -> Elims -> f Elims)
-> (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
forall a b. (a -> b) -> a -> b
$ (Term -> f Term) -> Elim' Term -> f (Elim' Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse ((Term -> f Term) -> Elim' Term -> f (Elim' Term))
-> (Term -> f Term) -> Elim' Term -> f (Elim' Term)
forall a b. (a -> b) -> a -> b
$ (ArgName -> f ArgName) -> Term -> f Term
onNamesTm ArgName -> f ArgName
f
onNamesArgs :: (ArgName -> f ArgName) -> Elims -> f Elims
onNamesArgs ArgName -> f ArgName
f = (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Elim' Term -> f (Elim' Term)) -> Elims -> f Elims)
-> (Elim' Term -> f (Elim' Term)) -> Elims -> f Elims
forall a b. (a -> b) -> a -> b
$ (Term -> f Term) -> Elim' Term -> f (Elim' Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Elim' a -> f (Elim' b)
traverse ((Term -> f Term) -> Elim' Term -> f (Elim' Term))
-> (Term -> f Term) -> Elim' Term -> f (Elim' Term)
forall a b. (a -> b) -> a -> b
$ (ArgName -> f ArgName) -> Term -> f Term
onNamesTm ArgName -> f ArgName
f
onNamesAbs :: (ArgName -> f ArgName)
-> ((ArgName -> f ArgName) -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs ArgName -> f ArgName
f = (ArgName -> f ArgName)
-> (ArgName -> f ArgName)
-> ((ArgName -> f ArgName) -> t -> f a)
-> Abs t
-> f (Abs a)
forall {f :: * -> *} {t} {t} {a}.
Applicative f =>
t
-> (ArgName -> f ArgName) -> (t -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs' ArgName -> f ArgName
f (ArgName -> ArgName
stringToArgName (ArgName -> ArgName)
-> (ArgName -> f ArgName) -> ArgName -> f ArgName
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> ArgName -> f ArgName
f (ArgName -> f ArgName)
-> (ArgName -> ArgName) -> ArgName -> f ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> ArgName
argNameToString)
onNamesAbs' :: t
-> (ArgName -> f ArgName) -> (t -> t -> f a) -> Abs t -> f (Abs a)
onNamesAbs' t
f ArgName -> f ArgName
f' t -> t -> f a
nd (Abs ArgName
s t
x) = ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
Abs (ArgName -> a -> Abs a) -> f ArgName -> f (a -> Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> f ArgName
f' ArgName
s f (a -> Abs a) -> f a -> f (Abs a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> t -> f a
nd t
f t
x
onNamesAbs' t
f ArgName -> f ArgName
f' t -> t -> f a
nd (NoAbs ArgName
s t
x) = ArgName -> a -> Abs a
forall a. ArgName -> a -> Abs a
NoAbs (ArgName -> a -> Abs a) -> f ArgName -> f (a -> Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> f ArgName
f' ArgName
s f (a -> Abs a) -> f a -> f (Abs a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> t -> t -> f a
nd t
f t
x
unW :: a -> m a
unW a
"w" = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
".w"
unW a
s = a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
s
renameVar :: ArgName -> StateT [NamedArg Expr] Identity ArgName
renameVar ArgName
"w" = StateT [NamedArg Expr] Identity ArgName
betterName
renameVar ArgName
s = ArgName -> StateT [NamedArg Expr] Identity ArgName
forall a. a -> StateT [NamedArg Expr] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ArgName
s
betterName :: StateT [NamedArg Expr] Identity ArgName
betterName = do
xs <- StateT [NamedArg Expr] Identity [NamedArg Expr]
forall s (m :: * -> *). MonadState s m => m s
get
case xs of
[] -> StateT [NamedArg Expr] Identity ArgName
forall a. HasCallStack => a
__IMPOSSIBLE__
NamedArg Expr
arg : [NamedArg Expr]
args -> do
[NamedArg Expr] -> StateT [NamedArg Expr] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [NamedArg Expr]
args
ArgName -> StateT [NamedArg Expr] Identity ArgName
forall a. a -> StateT [NamedArg Expr] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgName -> StateT [NamedArg Expr] Identity ArgName)
-> ArgName -> StateT [NamedArg Expr] Identity ArgName
forall a b. (a -> b) -> a -> b
$ if
| Arg ArgInfo
_ (Named Maybe NamedName
_ (A.Var Name
x)) <- NamedArg Expr
arg -> Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Name -> ArgName) -> Name -> ArgName
forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete Name
x
| Just ArgName
x <- NamedArg Expr -> Maybe ArgName
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
bareNameOf NamedArg Expr
arg -> ArgName -> ArgName
argNameToString ArgName
x
| Bool
otherwise -> ArgName
"w"
contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry]
contextOfMeta InteractionId
ii Rewrite
norm = InteractionId
-> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM [ResponseContextEntry] -> TCM [ResponseContextEntry])
-> TCM [ResponseContextEntry] -> TCM [ResponseContextEntry]
forall a b. (a -> b) -> a -> b
$ do
info <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> TCMT IO MetaVariable -> TCMT IO (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta (MetaId -> TCMT IO MetaVariable)
-> TCMT IO MetaId -> TCMT IO MetaVariable
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii)
withMetaInfo info $ do
cxt <- getContext
let localVars = (Int -> ContextEntry -> ContextEntry)
-> [Int] -> [ContextEntry] -> [ContextEntry]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> ContextEntry -> ContextEntry
forall a. Subst a => Int -> a -> a
raise [Int
1..] [ContextEntry]
cxt
letVars <- Map.toAscList <$> asksTC envLetBindings
(++) <$> forMaybeM (reverse localVars) mkVar
<*> forMaybeM letVars mkLet
where
mkVar :: ContextEntry -> TCM (Maybe ResponseContextEntry)
mkVar :: ContextEntry -> TCMT IO (Maybe ResponseContextEntry)
mkVar Dom{ domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
ai, unDom :: forall t e. Dom' t e -> e
unDom = (Name
name, Type
t) } = do
if ArgInfo -> Name -> Bool
shouldHide ArgInfo
ai Name
name then Maybe ResponseContextEntry -> TCMT IO (Maybe ResponseContextEntry)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ResponseContextEntry
forall a. Maybe a
Nothing else ResponseContextEntry -> Maybe ResponseContextEntry
forall a. a -> Maybe a
Just (ResponseContextEntry -> Maybe ResponseContextEntry)
-> TCMT IO ResponseContextEntry
-> TCMT IO (Maybe ResponseContextEntry)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
let n :: Name
n = Name -> Name
nameConcrete Name
name
x <- Name -> TCMT IO (ConOfAbs Name)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
a -> m (ConOfAbs a)
abstractToConcrete_ Name
name
let s = Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
C.isInScope Name
x
ty <- reifyUnblocked =<< normalForm norm t
return $ ResponseContextEntry n x (Arg ai ty) Nothing s
mkLet :: (Name, Open M.LetBinding) -> TCM (Maybe ResponseContextEntry)
mkLet :: (Name, Open LetBinding) -> TCMT IO (Maybe ResponseContextEntry)
mkLet (Name
name, Open LetBinding
lb) = do
LetBinding _ tm !dom <- Open LetBinding -> TCMT IO LetBinding
forall a (m :: * -> *).
(TermSubst a, MonadTCEnv m) =>
Open a -> m a
getOpen Open LetBinding
lb
if shouldHide (domInfo dom) name then return Nothing else Just <$> do
let n = Name -> Name
nameConcrete Name
name
x <- abstractToConcrete_ name
let s = Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
C.isInScope Name
x
ty <- reifyUnblocked =<< normalForm norm dom
v <- removeLetBindingsFrom name $ reifyUnblocked =<< normalForm norm tm
return $ ResponseContextEntry n x ty (Just v) s
shouldHide :: ArgInfo -> A.Name -> Bool
shouldHide :: ArgInfo -> Name -> Bool
shouldHide ArgInfo
ai Name
n = Bool -> Bool
not (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai) Bool -> Bool -> Bool
&& (Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
n Bool -> Bool -> Bool
|| Name -> Bool
nameIsRecordName Name
n)
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
norm Expr
e =
do (_,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
v <- normalForm norm t
reifyUnblocked v
typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
ii Rewrite
norm Expr
e =
do m <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
mi <- getMetaInfo <$> lookupLocalMeta m
withMetaInfo mi $
typeInCurrent norm e
introTactic :: Bool -> InteractionId -> TCM [String]
introTactic :: Bool -> InteractionId -> TCMT IO Names
introTactic Bool
pmLambda InteractionId
ii = do
mi <- InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii
mv <- lookupLocalMeta mi
withMetaInfo (getMetaInfo mv) $ case mvJudgement mv of
HasType MetaId
_ Comparison
_ Type
t -> do
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, HasBuiltins m) =>
Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> Args -> 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' t <- telViewUpTo' (-1) notVisible t
let fallback = do
cubical <- Maybe Cubical -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Cubical -> Bool) -> TCMT IO (Maybe Cubical) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
TelV tel _ <- (if cubical then telViewPath else telView) t
reportSDoc "interaction.intro" 20 $ TP.sep
[ "introTactic/fallback"
, "tel' = " TP.<+> prettyTCM tel'
, "tel = " TP.<+> prettyTCM tel
]
case (tel', tel) of
(Telescope
EmptyTel, Telescope
EmptyTel) -> Names -> TCMT IO Names
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
(Telescope, Telescope)
_ -> ListTel -> TCMT IO Names
introFun (Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel' ListTel -> ListTel -> ListTel
forall a. [a] -> [a] -> [a]
++ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
tel)
case unEl t of
I.Def QName
d Elims
_ -> do
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d
case theDef def of
Datatype{} -> Telescope -> TCMT IO Names -> TCMT IO Names
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel' (TCMT IO Names -> TCMT IO Names) -> TCMT IO Names -> TCMT IO Names
forall a b. (a -> b) -> a -> b
$ AllowAmbiguousNames -> Type -> TCMT IO Names
introData AllowAmbiguousNames
AmbiguousNothing 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
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
$ AllowAmbiguousNames -> Type -> TCMT IO Names
introData AllowAmbiguousNames
AmbiguousConProjs Type
t
| Bool
otherwise -> Telescope -> TCMT IO Names -> TCMT IO Names
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel' (TCMT IO Names -> TCMT IO Names) -> TCMT IO Names -> TCMT IO Names
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Names
introRec QName
d
Defn
_ -> TCMT IO Names
fallback
Term
_ -> TCMT IO Names
fallback
TCMT IO Names -> (TCErr -> TCMT IO Names) -> TCMT IO Names
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> Names -> TCMT IO Names
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
Judgement MetaId
_ -> TCMT IO Names
forall a. HasCallStack => a
__IMPOSSIBLE__
where
conName :: [NamedArg SplitPattern] -> [I.ConHead]
conName :: [NamedArg SplitPattern] -> [ConHead]
conName [NamedArg SplitPattern
p] = [ ConHead
c | I.ConP ConHead
c ConPatternInfo
_ [NamedArg SplitPattern]
_ <- [NamedArg SplitPattern -> SplitPattern
forall a. NamedArg a -> a
namedArg NamedArg SplitPattern
p] ]
conName [NamedArg SplitPattern]
_ = [ConHead]
forall a. HasCallStack => a
__IMPOSSIBLE__
showUnambiguousConName :: AllowAmbiguousNames -> ConHead -> f ArgName
showUnambiguousConName AllowAmbiguousNames
amb ConHead
v =
Doc -> ArgName
forall a. Doc a -> ArgName
render (Doc -> ArgName) -> (QName -> Doc) -> QName -> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Doc
forall a. Pretty a => a -> Doc
pretty (QName -> ArgName) -> f QName -> f ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsToCon QName -> f QName
forall (m :: * -> *) c. MonadAbsToCon m => AbsToCon c -> m c
runAbsToCon (AllowAmbiguousNames -> QName -> AbsToCon QName
lookupQName AllowAmbiguousNames
amb (QName -> AbsToCon QName) -> QName -> AbsToCon QName
forall a b. (a -> b) -> a -> b
$ ConHead -> QName
I.conName ConHead
v)
showTCM :: PrettyTCM a => a -> TCM String
showTCM :: forall a. PrettyTCM a => a -> TCM ArgName
showTCM a
v = Doc -> ArgName
forall a. Doc a -> ArgName
render (Doc -> ArgName) -> TCMT IO Doc -> TCM ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
v
introFun :: ListTel -> TCM [String]
introFun :: ListTel -> TCMT IO Names
introFun ListTel
tel = Telescope -> TCMT IO Names -> TCMT IO Names
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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
ArgName -> Int -> TCMT IO Doc -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.intro" Int
10 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ do TCMT IO Doc
"introFun" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (ListTel -> Telescope
telFromList ListTel
tel)
imp <- TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
let okHiding0 Hiding
h = Bool
imp Bool -> Bool -> Bool
|| Hiding
h Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== Hiding
NotHidden
allHidden = Bool -> Bool
not ((Hiding -> Bool) -> [Hiding] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Hiding -> Bool
okHiding0 [Hiding]
hs)
okHiding = if Bool
allHidden then Bool -> Hiding -> Bool
forall a b. a -> b -> a
const Bool
True else Hiding -> Bool
okHiding0
vars <-
applyWhen allHidden withShowAllArguments $
mapM showTCM [ setHiding h $ defaultArg $ var i :: Arg Term
| (h, i) <- zip hs $ downFrom n
, okHiding h
]
if pmLambda
then return [ unwords $ ["λ", "{"] ++ vars ++ ["→", "?", "}"] ]
else return [ unwords $ ["λ"] ++ vars ++ ["→", "?"] ]
where
n :: Int
n = ListTel -> Int
forall a. Sized a => a -> Int
size ListTel
tel
hs :: [Hiding]
hs = (Dom (ArgName, Type) -> Hiding) -> ListTel -> [Hiding]
forall a b. (a -> b) -> [a] -> [b]
map Dom (ArgName, Type) -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ListTel
tel
tel' :: Telescope
tel' = ListTel -> Telescope
telFromList [ ((ArgName, Type) -> (ArgName, Type))
-> Dom (ArgName, Type) -> Dom (ArgName, Type)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName, Type) -> (ArgName, Type)
forall {a} {b}. (Eq a, IsString a) => (a, b) -> (a, b)
makeName Dom (ArgName, Type)
b | Dom (ArgName, Type)
b <- ListTel
tel ]
makeName :: (a, b) -> (a, b)
makeName (a
"_", b
t) = (a
"x", b
t)
makeName (a
x, b
t) = (a
x, b
t)
introData :: AllowAmbiguousNames -> I.Type -> TCM [String]
introData :: AllowAmbiguousNames -> Type -> TCMT IO Names
introData AllowAmbiguousNames
amb Type
t = do
let tel :: Telescope
tel = ListTel -> Telescope
telFromList [(ArgName, Type) -> Dom (ArgName, Type)
forall a. a -> Dom a
defaultDom (ArgName
"_", 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
$ ArgName -> Int -> DeBruijnPattern
forall a. DeBruijn a => ArgName -> Int -> a
debruijnNamedVar ArgName
"c" Int
0]
cubical <- Maybe Cubical -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Cubical -> Bool) -> TCMT IO (Maybe Cubical) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
r <- (if cubical then id else
locallyTCState (stPragmaOptions . lensOptWithoutK) (const (Value False)))
$ splitLast CoInductive tel pat
case r of
Left SplitError
err -> Names -> TCMT IO Names
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
Right Covering
cov ->
(ConHead -> TCM ArgName) -> [ConHead] -> TCMT IO Names
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (AllowAmbiguousNames -> ConHead -> TCM ArgName
forall {f :: * -> *}.
(MonadFresh NameId f, MonadInteractionPoints f,
MonadStConcreteNames f, PureTCM f, IsString (f Doc), Null (f Doc),
Semigroup (f Doc)) =>
AllowAmbiguousNames -> ConHead -> f ArgName
showUnambiguousConName AllowAmbiguousNames
amb) ([ConHead] -> TCMT IO Names) -> [ConHead] -> TCMT IO Names
forall a b. (a -> b) -> a -> b
$ (SplitClause -> [ConHead]) -> [SplitClause] -> [ConHead]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([NamedArg SplitPattern] -> [ConHead]
conName ([NamedArg SplitPattern] -> [ConHead])
-> (SplitClause -> [NamedArg SplitPattern])
-> SplitClause
-> [ConHead]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitClause -> [NamedArg SplitPattern]
scPats) ([SplitClause] -> [ConHead]) -> [SplitClause] -> [ConHead]
forall a b. (a -> b) -> a -> b
$ Covering -> [SplitClause]
splitClauses Covering
cov
introRec :: QName -> TCM [String]
introRec :: QName -> TCMT IO Names
introRec QName
d = do
hfs <- QName -> TCMT IO [Dom Name]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m [Dom Name]
getRecordFieldNames QName
d
fs <- ifM showImplicitArguments
(return $ map unDom hfs)
(return [ unDom a | a <- hfs, visible a ])
let e = Range -> RecordAssignments -> Expr
C.Rec Range
forall a. Range' a
noRange (RecordAssignments -> Expr) -> RecordAssignments -> Expr
forall a b. (a -> b) -> a -> b
$ [Name] -> (Name -> RecordAssignment) -> RecordAssignments
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Name]
fs ((Name -> RecordAssignment) -> RecordAssignments)
-> (Name -> RecordAssignment) -> RecordAssignments
forall a b. (a -> b) -> a -> b
$ \ Name
f ->
FieldAssignment -> RecordAssignment
forall a b. a -> Either a b
Left (FieldAssignment -> RecordAssignment)
-> FieldAssignment -> RecordAssignment
forall a b. (a -> b) -> a -> b
$ Name -> Expr -> FieldAssignment
forall a. Name -> a -> FieldAssignment' a
C.FieldAssignment Name
f (Expr -> FieldAssignment) -> Expr -> FieldAssignment
forall a b. (a -> b) -> a -> b
$ Range -> Maybe Int -> Expr
C.QuestionMark Range
forall a. Range' a
noRange Maybe Int
forall a. Maybe a
Nothing
return [ prettyShow e ]
atTopLevel :: TCM a -> TCM a
atTopLevel :: forall a. TCM a -> TCM a
atTopLevel TCM a
m = TCM a -> TCM a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
let err :: TCMT IO a
err = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError ArgName
"The file has not been loaded yet."
TCMT IO (Maybe (ModuleName, TopLevelModuleName))
-> TCM a -> ((ModuleName, TopLevelModuleName) -> TCM a) -> TCM a
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
-> TCMT IO (Maybe (ModuleName, TopLevelModuleName))
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (Maybe (ModuleName, TopLevelModuleName)
-> f (Maybe (ModuleName, TopLevelModuleName)))
-> TCState -> f TCState
Lens' TCState (Maybe (ModuleName, TopLevelModuleName))
stCurrentModule) TCM a
forall {a}. TCMT IO a
err (((ModuleName, TopLevelModuleName) -> TCM a) -> TCM a)
-> ((ModuleName, TopLevelModuleName) -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \(ModuleName
current, TopLevelModuleName
topCurrent) -> do
TCMT IO (Maybe ModuleInfo)
-> TCM a -> (ModuleInfo -> TCM a) -> TCM a
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
topCurrent) TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__ ((ModuleInfo -> TCM a) -> TCM a) -> (ModuleInfo -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ ModuleInfo
mi -> do
let scope :: ScopeInfo
scope = Interface -> ScopeInfo
iInsideScope (Interface -> ScopeInfo) -> Interface -> ScopeInfo
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
mi
tel <- ModuleName -> TCMT IO Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
current
let names :: [A.Name]
names = (LocalVar -> Name) -> [LocalVar] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map LocalVar -> Name
localVar ([LocalVar] -> [Name]) -> [LocalVar] -> [Name]
forall a b. (a -> b) -> a -> b
$ (LocalVar -> Bool) -> [LocalVar] -> [LocalVar]
forall a. (a -> Bool) -> [a] -> [a]
filter ((BindingSource
LetBound BindingSource -> BindingSource -> Bool
forall a. Eq a => a -> a -> Bool
/=) (BindingSource -> Bool)
-> (LocalVar -> BindingSource) -> LocalVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocalVar -> BindingSource
localBindingSource)
([LocalVar] -> [LocalVar]) -> [LocalVar] -> [LocalVar]
forall a b. (a -> b) -> a -> b
$ ((Name, LocalVar) -> LocalVar) -> [(Name, LocalVar)] -> [LocalVar]
forall a b. (a -> b) -> [a] -> [b]
map (Name, LocalVar) -> LocalVar
forall a b. (a, b) -> b
snd ([(Name, LocalVar)] -> [LocalVar])
-> [(Name, LocalVar)] -> [LocalVar]
forall a b. (a -> b) -> a -> b
$ [(Name, LocalVar)] -> [(Name, LocalVar)]
forall a. [a] -> [a]
reverse ([(Name, LocalVar)] -> [(Name, LocalVar)])
-> [(Name, LocalVar)] -> [(Name, LocalVar)]
forall a b. (a -> b) -> a -> b
$ ScopeInfo
scope ScopeInfo
-> Lens' ScopeInfo [(Name, LocalVar)] -> [(Name, LocalVar)]
forall o i. o -> Lens' o i -> i
^. ([(Name, LocalVar)] -> f [(Name, LocalVar)])
-> ScopeInfo -> f ScopeInfo
Lens' ScopeInfo [(Name, LocalVar)]
scopeLocals
let types :: [Dom I.Type]
types = (Dom (ArgName, Type) -> Dom Type) -> ListTel -> [Dom Type]
forall a b. (a -> b) -> [a] -> [b]
map ((ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type) -> Dom (ArgName, 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 (ArgName, t)]
telToList Telescope
tel
gamma :: ListTel' A.Name
gamma = [ContextEntry] -> Maybe [ContextEntry] -> [ContextEntry]
forall a. a -> Maybe a -> a
fromMaybe [ContextEntry]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [ContextEntry] -> [ContextEntry])
-> Maybe [ContextEntry] -> [ContextEntry]
forall a b. (a -> b) -> a -> b
$
(Name -> Dom Type -> ContextEntry)
-> [Name] -> [Dom Type] -> Maybe [ContextEntry]
forall a b c. (a -> b -> c) -> [a] -> [b] -> Maybe [c]
zipWith' (\ Name
x Dom Type
dom -> (Name
x,) (Type -> (Name, Type)) -> Dom Type -> ContextEntry
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type
dom) [Name]
names [Dom Type]
types
reportSDoc "interaction.top" 20 $ TP.vcat
[ "BasicOps.atTopLevel"
, " names = " TP.<+> TP.sep (map prettyA names)
, " types = " TP.<+> TP.sep (map prettyTCM types)
]
M.withCurrentModule current $
withScope_ scope $
addContext gamma $ do
cp <- viewTC eCurrentCheckpoint
stModuleCheckpoints `modifyTCLens` fmap (const cp)
m
parseName :: Range -> String -> TCM C.QName
parseName :: Range -> ArgName -> TCM QName
parseName Range
r ArgName
s = do
e <- Range -> ArgName -> TCM Expr
parseExpr Range
r ArgName
s
let failure = TypeError -> TCM QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM QName) -> TypeError -> TCM QName
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$ ArgName
"Not an identifier: " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Expr -> ArgName
forall a. Show a => a -> ArgName
show Expr
e ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
"."
maybe failure return $ isQName e
isQName :: C.Expr -> Maybe C.QName
isQName :: Expr -> Maybe QName
isQName = \case
C.Ident QName
x -> QName -> Maybe QName
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
Expr
_ -> Maybe QName
forall a. Maybe a
Nothing
isName :: C.Expr -> Maybe C.Name
isName :: Expr -> Maybe Name
isName = Expr -> Maybe QName
isQName (Expr -> Maybe QName)
-> (QName -> Maybe Name) -> Expr -> Maybe Name
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
C.QName Name
x -> Name -> Maybe Name
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
x
QName
_ -> Maybe Name
forall a. Maybe a
Nothing
moduleContents
:: Rewrite
-> Range
-> String
-> TCM ([C.Name], I.Telescope, [(C.Name, I.Type)])
moduleContents :: Rewrite
-> Range -> ArgName -> TCM ([Name], Telescope, [(Name, Type)])
moduleContents Rewrite
norm Range
rng ArgName
s = Call
-> TCM ([Name], Telescope, [(Name, Type)])
-> TCM ([Name], Telescope, [(Name, Type)])
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall Call
ModuleContents (TCM ([Name], Telescope, [(Name, Type)])
-> TCM ([Name], Telescope, [(Name, Type)]))
-> TCM ([Name], Telescope, [(Name, Type)])
-> TCM ([Name], Telescope, [(Name, Type)])
forall a b. (a -> b) -> a -> b
$ do
if ArgName -> Bool
forall a. Null a => a -> Bool
null (ArgName -> ArgName
trim ArgName
s) then Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
getModuleContents Rewrite
norm Maybe QName
forall a. Maybe a
Nothing else do
e <- Range -> ArgName -> TCM Expr
parseExpr Range
rng ArgName
s
case isQName e of
Maybe QName
Nothing -> Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
getRecordContents Rewrite
norm Expr
e
Just QName
x -> do
ms :: [AbstractModule] <- QName -> ScopeInfo -> [AbstractModule]
forall a. InScope a => QName -> ScopeInfo -> [a]
scopeLookup QName
x (ScopeInfo -> [AbstractModule])
-> TCMT IO ScopeInfo -> TCMT IO [AbstractModule]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
if null ms then getRecordContents norm e else getModuleContents norm $ Just x
getRecordContents
:: Rewrite
-> C.Expr
-> TCM ([C.Name], I.Telescope, [(C.Name, I.Type)])
getRecordContents :: Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
getRecordContents Rewrite
norm Expr
ce = do
(_, t) <- Expr -> TCM (Term, Type)
inferExpr (Expr -> TCM (Term, Type)) -> TCM Expr -> TCM (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> ScopeM (AbsOfCon Expr)
forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
toAbstract Expr
ce
isRecordType t >>= \case
Maybe (QName, Args, RecordData)
Nothing -> TypeError -> TCM ([Name], Telescope, [(Name, Type)])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ([Name], Telescope, [(Name, Type)]))
-> TypeError -> TCM ([Name], Telescope, [(Name, Type)])
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
t
Just (QName
q, Args
vs, RecordData{ _recFields :: RecordData -> [Dom QName]
_recFields = [Dom QName]
fs, _recTel :: RecordData -> Telescope
_recTel = Telescope
rtel }) -> do
let xs :: [Name]
xs = (Dom QName -> Name) -> [Dom QName] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name
nameConcrete (Name -> Name) -> (Dom QName -> Name) -> Dom QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
qnameName (QName -> Name) -> (Dom QName -> QName) -> Dom QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom QName -> QName
forall t e. Dom' t e -> e
unDom) [Dom QName]
fs
tel :: Telescope
tel = Telescope -> Args -> Telescope
forall t. Apply t => t -> Args -> t
apply Telescope
rtel Args
vs
doms :: [Dom Type]
doms = Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
tel
ArgName -> Int -> TCMT IO Doc -> ScopeM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"interaction.contents.record" Int
20 (TCMT IO Doc -> ScopeM ()) -> TCMT IO Doc -> ScopeM ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TP.vcat
[ TCMT IO Doc
"getRecordContents"
, TCMT IO Doc
" cxt = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> (Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO 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)
, TCMT IO Doc
" tel = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel
, TCMT IO Doc
" doms = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> [Dom Type] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Dom Type] -> m Doc
prettyTCM [Dom Type]
doms
, TCMT IO Doc
" doms'= " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TP.<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel ([Dom Type] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Dom Type] -> m Doc
prettyTCM [Dom Type]
doms)
]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Rewrite -> Type -> TCMT IO Type
forall t.
(Reduce t, Simplify t, Instantiate 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
return ([], tel, zip xs ts)
getModuleContents
:: Rewrite
-> Maybe C.QName
-> TCM ([C.Name], I.Telescope, [(C.Name, I.Type)])
getModuleContents :: Rewrite -> Maybe QName -> TCM ([Name], Telescope, [(Name, Type)])
getModuleContents Rewrite
norm Maybe QName
mm = do
modScope <- case Maybe QName
mm of
Maybe QName
Nothing -> TCMT IO Scope
getCurrentScope
Just QName
m -> ModuleName -> TCMT IO Scope
getNamedScope (ModuleName -> TCMT IO Scope)
-> (AbstractModule -> ModuleName)
-> AbstractModule
-> TCMT IO Scope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractModule -> ModuleName
amodName (AbstractModule -> TCMT IO Scope)
-> TCMT IO AbstractModule -> TCMT IO Scope
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO AbstractModule
resolveModule QName
m
let modules :: ThingsInScope AbstractModule
modules = Scope -> ThingsInScope AbstractModule
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
names :: ThingsInScope AbstractName
names = Scope -> ThingsInScope AbstractName
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
xns = [ (Name
x,AbstractName
n) | (Name
x, List1 AbstractName
ns) <- ThingsInScope AbstractName -> [(Name, List1 AbstractName)]
forall k a. Map k a -> [(k, a)]
Map.toList ThingsInScope AbstractName
names, AbstractName
n <- List1 AbstractName -> [Item (List1 AbstractName)]
forall l. IsList l => l -> [Item l]
List1.toList List1 AbstractName
ns ]
types <- forMaybeM xns $ \(Name
x, AbstractName
n) -> do
QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' (AbstractName -> QName
anameName AbstractName
n) TCMT IO (Either SigError Definition)
-> (Either SigError Definition -> TCMT IO (Maybe (Name, Type)))
-> TCMT IO (Maybe (Name, Type))
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Right Definition
d -> do
t <- Rewrite -> Type -> TCMT IO Type
forall t.
(Reduce t, Simplify t, Instantiate 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)
return $ Just (x, t)
Left{} -> Maybe (Name, Type) -> TCMT IO (Maybe (Name, Type))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Name, Type)
forall a. Maybe a
Nothing
return (Map.keys modules, EmptyTel, types)
whyInScope :: FilePath -> String -> TCM WhyInScopeData
whyInScope :: ArgName -> ArgName -> TCM WhyInScopeData
whyInScope ArgName
cwd ArgName
s = do
x <- Range -> ArgName -> TCM QName
parseName Range
forall a. Range' a
noRange ArgName
s
scope <- getScope
return $ WhyInScopeData
x
cwd
(lookup x $ map (first C.QName) $ scope ^. scopeLocals)
(scopeLookup x scope)
(scopeLookup x scope)