{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Def where
import Prelude hiding ( null )
import Control.Monad ( forM, forM_ )
import Control.Monad.Except ( MonadError(..) )
import Data.Bifunctor
import Data.Function (on)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Semigroup (Semigroup((<>)))
import Agda.Interaction.Options
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Concrete.Pretty as C
import Agda.Syntax.Position
import Agda.Syntax.Abstract.Pattern as A
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import Agda.Syntax.Internal.MetaVars (allMetasList)
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Info hiding (defAbstract)
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Warnings ( warning )
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Inlining
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Patterns.Abstract (expandPatternSynonyms)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.With
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Telescope.Path
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.Rewriting.Confluence
import Agda.TypeChecking.CompiledClause (CompiledClauses'(..), hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.RecordPatterns ( recordRHSToCopatterns )
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Rules.LHS ( checkLeftHandSide, LHSResult(..), bindAsPatterns )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl ( checkDecls )
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.Utils.Permutation
import Agda.Syntax.Common.Pretty ( prettyShow )
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.Singleton
import Agda.Utils.Size
import qualified Agda.Utils.SmallSet as SmallSet
import Agda.Utils.Update
import Agda.Utils.Impossible
checkFunDef :: A.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef :: DefInfo -> QName -> [Clause' LHS] -> TCM ()
checkFunDef DefInfo
i QName
name [Clause' LHS]
cs = do
(Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
name ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Blocked_ -> Blocked_) -> Definition -> Definition
updateDefBlocked ((Blocked_ -> Blocked_) -> Definition -> Definition)
-> (Blocked_ -> Blocked_) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Blocked_ -> Blocked_
forall a b. a -> b -> a
const (Blocked_ -> Blocked_ -> Blocked_)
-> Blocked_ -> Blocked_ -> Blocked_
forall a b. (a -> b) -> a -> b
$
NotBlocked' Term -> () -> Blocked_
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked (QName -> NotBlocked' Term
forall t. QName -> NotBlocked' t
MissingClauses QName
name) ()
def <- Definition -> TCMT IO Definition
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef (Definition -> TCMT IO Definition)
-> TCMT IO Definition -> TCMT IO Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
let t = Definition -> Type
defType Definition
def
let info = Definition -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo Definition
def
setHardCompileTimeModeIfErased' info $ do
case isAlias cs t of
Just (Expr
e, Maybe Expr
mc, MetaId
x)
| DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
Info.defAbstract DefInfo
i IsAbstract -> IsAbstract -> Bool
forall a. Eq a => a -> a -> Bool
== IsAbstract
ConcreteDef, DefInfo -> IsOpaque
forall t. DefInfo' t -> IsOpaque
Info.defOpaque DefInfo
i IsOpaque -> IsOpaque -> Bool
forall a. Eq a => a -> a -> Bool
== IsOpaque
TransparentDef ->
Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> [Clause' LHS] -> Bool -> Call
CheckFunDefCall (DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i) QName
name [Clause' LHS]
cs Bool
True) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaId -> TCMT IO Bool
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m Bool
isFrozen MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
xs <- Type -> [MetaId]
forall a. AllMetas a => a -> [MetaId]
allMetasList (Type -> [MetaId])
-> (MetaVariable -> Type) -> MetaVariable -> [MetaId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> [MetaId])
-> TCMT IO MetaVariable -> TCMT IO [MetaId]
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
x
mapM_ unfreezeMeta (x : xs)
Type -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM ()
checkAlias Type
t ArgInfo
info DefInfo
i QName
name Expr
e Maybe Expr
mc
| Bool
otherwise -> do
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (MetaInstantiation -> Bool
isOpenMeta (MetaInstantiation -> Bool)
-> TCMT IO MetaInstantiation -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO MetaInstantiation
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m MetaInstantiation
lookupMetaInstantiation MetaId
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
DefInfo -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange DefInfo
i (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> IsOpaque -> Warning
MissingTypeSignatureForOpaque QName
name (DefInfo -> IsOpaque
forall t. DefInfo' t -> IsOpaque
Info.defOpaque DefInfo
i)
Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> [Clause' LHS]
-> TCM ()
checkFunDef' Type
t ArgInfo
info Maybe ExtLamInfo
forall a. Maybe a
Nothing Maybe QName
forall a. Maybe a
Nothing DefInfo
i QName
name [Clause' LHS]
cs
Maybe (Expr, Maybe Expr, MetaId)
_ -> Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> [Clause' LHS]
-> TCM ()
checkFunDef' Type
t ArgInfo
info Maybe ExtLamInfo
forall a. Maybe a
Nothing Maybe QName
forall a. Maybe a
Nothing DefInfo
i QName
name [Clause' LHS]
cs
let ismacro = Defn -> Bool
isMacro (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Bool) -> Definition -> Bool
forall a b. (a -> b) -> a -> b
$ Definition
def
when (ismacro || Info.defMacro i == MacroDef) $ checkMacroType t
TCM () -> ((TCErr, Blocker) -> TCM ()) -> TCM ()
forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
`catchIlltypedPatternBlockedOnMeta` \ (TCErr
err, Blocker
blocker) -> do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"checking function definition got stuck on: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Blocker -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Blocker
blocker ]
(Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
name ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ (Blocked_ -> Blocked_) -> Definition -> Definition
updateDefBlocked ((Blocked_ -> Blocked_) -> Definition -> Definition)
-> (Blocked_ -> Blocked_) -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Blocked_ -> Blocked_ -> Blocked_
forall a b. a -> b -> a
const (Blocked_ -> Blocked_ -> Blocked_)
-> Blocked_ -> Blocked_ -> Blocked_
forall a b. (a -> b) -> a -> b
$ Blocker -> () -> Blocked_
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
blocker ()
Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
blocker (Constraint -> TCM ()) -> Constraint -> TCM ()
forall a b. (a -> b) -> a -> b
$ DefInfo -> QName -> [Clause' LHS] -> TCErr -> Constraint
CheckFunDef DefInfo
i QName
name [Clause' LHS]
cs TCErr
err
checkMacroType :: Type -> TCM ()
checkMacroType :: Type -> TCM ()
checkMacroType Type
t = do
TelV tel tr <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView Type
t
let telList = Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
tel
resType = Tele (Dom Type) -> Type -> Type
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract ([Dom ([Char], Type)] -> Tele (Dom Type)
telFromList (Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
forall a. Int -> [a] -> [a]
drop ([Dom ([Char], Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dom ([Char], Type)]
telList Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Dom ([Char], Type)]
telList)) Type
tr
expectedType <- el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)
equalType resType expectedType
`catchError` \ TCErr
_ -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
MacroResultTypeMismatch Type
expectedType
isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, Maybe C.Expr, MetaId)
isAlias :: [Clause' LHS] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
isAlias [Clause' LHS]
cs Type
t =
case [Clause' LHS] -> Maybe (Expr, Maybe Expr)
trivialClause [Clause' LHS]
cs of
Just (Expr
e, Maybe Expr
mc) | Just MetaId
x <- Term -> Maybe MetaId
isMeta (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t) -> (Expr, Maybe Expr, MetaId) -> Maybe (Expr, Maybe Expr, MetaId)
forall a. a -> Maybe a
Just (Expr
e, Maybe Expr
mc, MetaId
x)
Maybe (Expr, Maybe Expr)
_ -> Maybe (Expr, Maybe Expr, MetaId)
forall a. Maybe a
Nothing
where
isMeta :: Term -> Maybe MetaId
isMeta (MetaV MetaId
x Elims
_) = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
x
isMeta Term
_ = Maybe MetaId
forall a. Maybe a
Nothing
trivialClause :: [Clause' LHS] -> Maybe (Expr, Maybe Expr)
trivialClause [A.Clause (A.LHS LHSInfo
i (A.LHSHead QName
f [])) [ProblemEq]
_ (A.RHS Expr
e Maybe Expr
mc) WhereDeclarations
wh Bool
_]
| WhereDeclarations -> Bool
forall a. Null a => a -> Bool
null WhereDeclarations
wh = (Expr, Maybe Expr) -> Maybe (Expr, Maybe Expr)
forall a. a -> Maybe a
Just (Expr
e, Maybe Expr
mc)
trivialClause [Clause' LHS]
_ = Maybe (Expr, Maybe Expr)
forall a. Maybe a
Nothing
checkAlias :: Type -> ArgInfo -> A.DefInfo -> QName -> A.Expr -> Maybe C.Expr -> TCM ()
checkAlias :: Type -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM ()
checkAlias Type
t ArgInfo
ai DefInfo
i QName
name Expr
e Maybe Expr
mc =
let clause :: SpineClause
clause = A.Clause { clauseLHS :: SpineLHS
clauseLHS = LHSInfo -> QName -> [NamedArg (Pattern' Expr)] -> SpineLHS
A.SpineLHS (Range -> ExpandedEllipsis -> LHSInfo
LHSInfo (DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i) ExpandedEllipsis
NoEllipsis) QName
name []
, clauseStrippedPats :: [ProblemEq]
clauseStrippedPats = []
, clauseRHS :: RHS
clauseRHS = Expr -> Maybe Expr -> RHS
A.RHS Expr
e Maybe Expr
mc
, clauseWhereDecls :: WhereDeclarations
clauseWhereDecls = WhereDeclarations
A.noWhereDecls
, clauseCatchall :: Bool
clauseCatchall = Bool
False } in
QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCM ()
-> TCM ()
forall a.
QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCM a
-> TCM a
atClause QName
name Int
0 Type
t Maybe Substitution
forall a. Maybe a
Nothing SpineClause
clause (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def.alias" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"checkAlias" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
name) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
colon TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
, [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
name) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
equals TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e
]
v <- ArgInfo -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r) =>
r -> tcm a -> tcm a
applyModalityToContextFunBody ArgInfo
ai (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCMT IO Term
checkDontExpandLast Comparison
CmpLeq Expr
e Type
t
reportSDoc "tc.def.alias" 20 $ "checkAlias: finished checking"
solveSizeConstraints DontDefaultToInfty
v <- instantiateFull v
let bodyMod = case ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai of
Relevance
Irrelevant -> Term -> Term
dontCare
Relevance
_ -> Term -> Term
forall a. a -> a
id
fun <- emptyFunctionData
addConstant' name ai name t $ FunctionDefn $
set funMacro_ (Info.defMacro i == MacroDef) $
set funAbstr_ (Info.defAbstract i) $
fun { _funClauses = [ Clause
{ clauseLHSRange = getRange i
, clauseFullRange = getRange i
, clauseTel = EmptyTel
, namedClausePats = []
, clauseBody = Just $ bodyMod v
, clauseType = Just $ Arg ai t
, clauseCatchall = False
, clauseExact = Just True
, clauseRecursive = Nothing
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
, clauseWhereModule = Nothing
} ]
, _funCompiled = Just $ Done [] $ bodyMod v
, _funSplitTree = Just $ SplittingDone 0
, _funOpaque = Info.defOpaque i
}
case Info.defInstance i of
InstanceDef KwRange
_r -> QName -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange QName
name (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Type -> TCM ()
addTypedInstance QName
name Type
t
IsInstance
NotInstanceDef -> () -> TCM ()
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
reportSDoc "tc.def.alias" 20 $ "checkAlias: leaving"
checkFunDef' :: Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> A.DefInfo
-> QName
-> [A.Clause]
-> TCM ()
checkFunDef' :: Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> [Clause' LHS]
-> TCM ()
checkFunDef' Type
t ArgInfo
ai Maybe ExtLamInfo
extlam Maybe QName
with DefInfo
i QName
name [Clause' LHS]
cs =
Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> Maybe (Substitution, Map Name LetBinding)
-> [Clause' LHS]
-> TCM ()
checkFunDefS Type
t ArgInfo
ai Maybe ExtLamInfo
extlam Maybe QName
with DefInfo
i QName
name Maybe (Substitution, Map Name LetBinding)
forall a. Maybe a
Nothing [Clause' LHS]
cs
checkFunDefS :: Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> A.DefInfo
-> QName
-> Maybe (Substitution, Map Name LetBinding)
-> [A.Clause]
-> TCM ()
checkFunDefS :: Type
-> ArgInfo
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> Maybe (Substitution, Map Name LetBinding)
-> [Clause' LHS]
-> TCM ()
checkFunDefS Type
t ArgInfo
ai Maybe ExtLamInfo
extlam Maybe QName
with DefInfo
i QName
name Maybe (Substitution, Map Name LetBinding)
withSubAndLets [Clause' LHS]
cs = do
Call -> TCM () -> TCM ()
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Range -> QName -> [Clause' LHS] -> Bool -> Call
CheckFunDefCall (DefInfo -> Range
forall a. HasRange a => a -> Range
getRange DefInfo
i) QName
name [Clause' LHS]
cs Bool
True) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def.fun" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
sep [ TCMT IO Doc
"checking body of" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
name
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
":" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"full type:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> TCMT IO Doc)
-> (Definition -> Type) -> Definition -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> TCMT IO Doc) -> TCMT IO Definition -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name)
]
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.def.fun" Int
70 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"clauses:" TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (Clause' LHS -> TCMT IO Doc) -> [Clause' LHS] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc)
-> (Clause' LHS -> TCMT IO Doc) -> Clause' LHS -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (Clause' LHS -> [Char]) -> Clause' LHS -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' LHS -> [Char]
forall a. Show a => a -> [Char]
show (Clause' LHS -> [Char])
-> (Clause' LHS -> Clause' LHS) -> Clause' LHS -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause' LHS -> Clause' LHS
forall a. ExprLike a => a -> a
A.deepUnscope) [Clause' LHS]
cs
cs <- [SpineClause] -> TCMT IO [SpineClause]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([SpineClause] -> TCMT IO [SpineClause])
-> [SpineClause] -> TCMT IO [SpineClause]
forall a b. (a -> b) -> a -> b
$ (Clause' LHS -> SpineClause) -> [Clause' LHS] -> [SpineClause]
forall a b. (a -> b) -> [a] -> [b]
map Clause' LHS -> SpineClause
forall a b. LHSToSpine a b => a -> b
A.lhsToSpine [Clause' LHS]
cs
reportSDoc "tc.def.fun" 70 $
sep $ "spine clauses:" : map (nest 2 . text . show . A.deepUnscope) cs
cs <- traceCall NoHighlighting $ do
forM (zip cs [0..]) $ \ (SpineClause
c, Int
clauseNo) -> do
QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a.
QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCM a
-> TCM a
atClause QName
name Int
clauseNo Type
t ((Substitution, Map Name LetBinding) -> Substitution
forall a b. (a, b) -> a
fst ((Substitution, Map Name LetBinding) -> Substitution)
-> Maybe (Substitution, Map Name LetBinding) -> Maybe Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Substitution, Map Name LetBinding)
withSubAndLets) SpineClause
c (TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ do
(c,b) <- ArgInfo
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall (tcm :: * -> *) r a.
(MonadTCM tcm, LensModality r) =>
r -> tcm a -> tcm a
applyModalityToContextFunBody ArgInfo
ai (TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ do
Type
-> Maybe (Substitution, Map Name LetBinding)
-> SpineClause
-> TCMT IO (Clause, ClausesPostChecks)
checkClause Type
t Maybe (Substitution, Map Name LetBinding)
withSubAndLets SpineClause
c
whenNothing extlam $ solveSizeConstraints DontDefaultToInfty
inTopContext $ addClauses name [c]
return (c,b)
(cs, CPC isOneIxs) <- return $ (second mconcat . unzip) cs
let isSystem = Bool -> Bool
not (Bool -> Bool) -> (IntSet -> Bool) -> IntSet -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Bool
forall a. Null a => a -> Bool
null (IntSet -> Bool) -> IntSet -> Bool
forall a b. (a -> b) -> a -> b
$ IntSet
isOneIxs
canBeSystem <- do
let pss = (Clause -> [NamedArg DeBruijnPattern])
-> [Clause] -> [[NamedArg DeBruijnPattern]]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> [NamedArg DeBruijnPattern]
namedClausePats [Clause]
cs
allowed = \case
VarP{} -> Bool
True
ConP ConHead
_ ConPatternInfo
cpi [] | ConPatternInfo -> Bool
conPFallThrough ConPatternInfo
cpi -> Bool
True
DotP{} -> Bool
True
Pattern' x
_ -> Bool
False
return $! all (allowed . namedArg) (concat pss)
when isSystem $ unless canBeSystem $
typeError $ GenericError "no pattern matching or path copatterns in systems!"
reportSDoc "tc.def.fun" 70 $ inTopContext $ do
sep $ "checked clauses:" : map (nest 2 . text . show) cs
modifyFunClauses name (const [])
reportSDoc "tc.cc" 25 $ inTopContext $ do
sep [ "clauses before injectivity test"
, nest 2 $ prettyTCM $ map (QNamed name) cs
]
reportSDoc "tc.cc" 60 $ inTopContext $ do
sep [ "raw clauses: "
, nest 2 $ sep $ map (text . show . QNamed name) cs
]
applyCohesionToContext ai $ do
(cs,sys) <- if not isSystem then return (cs, empty) else do
fullType <- flip abstract t <$> getContextTelescope
sys <- inTopContext $ checkSystemCoverage name (IntSet.toList isOneIxs) fullType cs
tel <- getContextTelescope
let c = Clause
{ clauseFullRange :: Range
clauseFullRange = Range
forall a. Range' a
noRange
, clauseLHSRange :: Range
clauseLHSRange = Range
forall a. Range' a
noRange
, clauseTel :: Tele (Dom Type)
clauseTel = Tele (Dom Type)
tel
, namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = Tele (Dom Type) -> [NamedArg DeBruijnPattern]
forall a t. DeBruijn a => Tele (Dom t) -> [NamedArg a]
teleNamedArgs Tele (Dom Type)
tel
, clauseBody :: Maybe Term
clauseBody = Maybe Term
forall a. Maybe a
Nothing
, clauseType :: Maybe (Arg Type)
clauseType = Arg Type -> Maybe (Arg Type)
forall a. a -> Maybe a
Just (Type -> Arg Type
forall a. a -> Arg a
defaultArg Type
t)
, clauseCatchall :: Bool
clauseCatchall = Bool
False
, clauseExact :: Maybe Bool
clauseExact = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
, clauseRecursive :: Maybe Bool
clauseRecursive = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
, clauseUnreachable :: Maybe Bool
clauseUnreachable = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
}
return (cs ++ [c], pure sys)
cs <- instantiateFull cs
cs <- concat <$> do
forM cs $ \ Clause
cl -> do
(cls, nonExactSplit) <- ChangeT (TCMT IO) [Clause] -> TCMT IO ([Clause], Bool)
forall (m :: * -> *) a. Functor m => ChangeT m a -> m (a, Bool)
runChangeT (ChangeT (TCMT IO) [Clause] -> TCMT IO ([Clause], Bool))
-> ChangeT (TCMT IO) [Clause] -> TCMT IO ([Clause], Bool)
forall a b. (a -> b) -> a -> b
$ Clause -> ChangeT (TCMT IO) [Clause]
forall (m :: * -> *).
(MonadChange m, PureTCM m) =>
Clause -> m [Clause]
recordRHSToCopatterns Clause
cl
when nonExactSplit do
warning $ InlineNoExactSplit name cl
return cls
reportSLn "tc.inj.def" 20 $ "checkFunDef': checking injectivity..."
inv <- Bench.billTo [Bench.Injectivity] $
checkInjectivity name cs
reportSDoc "tc.cc" 15 $ inTopContext $ do
sep [ "clauses before compilation"
, nest 2 $ sep $ map (prettyTCM . QNamed name) cs
]
reportSDoc "tc.cc.raw" 65 $ do
sep [ "clauses before compilation"
, nest 2 $ sep $ map (text . show) cs
]
inTopContext $ addClauses name cs
reportSDoc "tc.cc.type" 60 $ " type : " <+> (text . prettyShow) t
reportSDoc "tc.cc.type" 60 $ " context: " <+> (text . prettyShow =<< getContextTelescope)
fullType <- flip telePi t <$> getContextTelescope
reportSLn "tc.cc.type" 80 $ show fullType
(mst, _recordExpressionBecameCopatternLHS, cc) <- Bench.billTo [Bench.Coverage] $
unsafeInTopContext $ compileClauses (if isSystem then Nothing else (Just (name, fullType)))
cs
cs <- defClauses <$> getConstInfo name
reportSDoc "tc.cc" 60 $ inTopContext $ do
sep [ "compiled clauses of" <+> prettyTCM name
, nest 2 $ pretty cc
]
ismacro <- isMacro . theDef <$> getConstInfo name
covering <- funCovering . theDef <$> getConstInfo name
inTopContext $ addConstant name =<< do
reportSDoc "tc.def.fun.clauses" 15 $ inTopContext $ do
vcat [ "final clauses for" <+> prettyTCM name <+> ":"
, nest 2 $ vcat $ map (prettyTCM . QNamed name) cs
]
fun <- emptyFunctionData
defn <- autoInline $ FunctionDefn $
set funMacro_ (ismacro || Info.defMacro i == MacroDef) $
set funAbstr_ (Info.defAbstract i) $
fun
{ _funClauses = cs
, _funCompiled = Just cc
, _funSplitTree = mst
, _funInv = inv
, _funOpaque = Info.defOpaque i
, _funExtLam = (\ ExtLamInfo
e -> ExtLamInfo
e { extLamSys = sys }) <$> extlam
, _funWith = with
, _funCovering = covering
}
lang <- getLanguage
useTerPragma $
updateDefCopatternLHS (const $ hasProjectionPatterns cc) $
(defaultDefn ai name fullType lang defn)
reportSDoc "tc.def.fun" 10 $ do
sep [ "added " <+> prettyTCM name <+> ":"
, nest 2 $ prettyTCM . defType =<< getConstInfo name
]
whenJustM (optConfluenceCheck <$> pragmaOptions) $ \ConfluenceCheck
confChk -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
ConfluenceCheck -> QName -> TCM ()
checkConfluenceOfClauses ConfluenceCheck
confChk QName
name
useTerPragma :: Definition -> TCM Definition
useTerPragma :: Definition -> TCMT IO Definition
useTerPragma def :: Definition
def@Defn{ defName :: Definition -> QName
defName = QName
name, theDef :: Definition -> Defn
theDef = fun :: Defn
fun@Function{}} = do
tc <- Lens' TCEnv (TerminationCheck ()) -> TCMT IO (TerminationCheck ())
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (TerminationCheck () -> f (TerminationCheck ()))
-> TCEnv -> f TCEnv
Lens' TCEnv (TerminationCheck ())
eTerminationCheck
let terminates = case TerminationCheck ()
tc of
TerminationCheck ()
NonTerminating -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
TerminationCheck ()
Terminating -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
TerminationCheck ()
_ -> Maybe Bool
forall a. Maybe a
Nothing
reportS "tc.fundef" 30 $
[ "funTerminates of " ++ prettyShow name ++ " set to " ++ show terminates
, " tc = " ++ show tc
]
return $ def { theDef = fun { funTerminates = terminates }}
useTerPragma Definition
def = Definition -> TCMT IO Definition
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Definition
def
mapLHSCores :: (A.LHSCore -> A.LHSCore) -> (A.RHS -> A.RHS)
mapLHSCores :: (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f = \case
A.WithRHS QName
aux [WithExpr]
es List1 (Clause' LHS)
cs -> QName -> [WithExpr] -> List1 (Clause' LHS) -> RHS
A.WithRHS QName
aux [WithExpr]
es (List1 (Clause' LHS) -> RHS) -> List1 (Clause' LHS) -> RHS
forall a b. (a -> b) -> a -> b
$ List1 (Clause' LHS)
-> (Clause' LHS -> Clause' LHS) -> List1 (Clause' LHS)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for List1 (Clause' LHS)
cs ((Clause' LHS -> Clause' LHS) -> List1 (Clause' LHS))
-> (Clause' LHS -> Clause' LHS) -> List1 (Clause' LHS)
forall a b. (a -> b) -> a -> b
$
\ (A.Clause (A.LHS LHSInfo
info LHSCore' Expr
core) [ProblemEq]
spats RHS
rhs WhereDeclarations
ds Bool
catchall) ->
LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' LHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
info (LHSCore' Expr -> LHSCore' Expr
f LHSCore' Expr
core)) [ProblemEq]
spats ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f RHS
rhs) WhereDeclarations
ds Bool
catchall
A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh -> [RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores LHSCore' Expr -> LHSCore' Expr
f RHS
rhs) WhereDeclarations
wh
rhs :: RHS
rhs@RHS
A.AbsurdRHS -> RHS
rhs
rhs :: RHS
rhs@A.RHS{} -> RHS
rhs
insertNames :: [Arg (Maybe A.BindName)] -> A.RHS -> A.RHS
insertNames :: [Arg (Maybe BindName)] -> RHS -> RHS
insertNames = (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores ((LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS)
-> ([Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr)
-> [Arg (Maybe BindName)]
-> RHS
-> RHS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr
insertInspects
insertInspects :: [Arg (Maybe A.BindName)] -> A.LHSCore -> A.LHSCore
insertInspects :: [Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr
insertInspects [Arg (Maybe BindName)]
ps = \case
A.LHSWith LHSCore' Expr
core [Arg (Pattern' Expr)]
wps [] ->
let ps' :: [Arg (Maybe (Arg (Pattern' Expr)))]
ps' = (Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr))))
-> [Arg (Maybe BindName)] -> [Arg (Maybe (Arg (Pattern' Expr)))]
forall a b. (a -> b) -> [a] -> [b]
map ((Maybe BindName -> Maybe (Arg (Pattern' Expr)))
-> Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr)))
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Maybe BindName -> Maybe (Arg (Pattern' Expr)))
-> Arg (Maybe BindName) -> Arg (Maybe (Arg (Pattern' Expr))))
-> (Maybe BindName -> Maybe (Arg (Pattern' Expr)))
-> Arg (Maybe BindName)
-> Arg (Maybe (Arg (Pattern' Expr)))
forall a b. (a -> b) -> a -> b
$ (BindName -> Arg (Pattern' Expr))
-> Maybe BindName -> Maybe (Arg (Pattern' Expr))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BindName -> Arg (Pattern' Expr)
patOfName) [Arg (Maybe BindName)]
ps in
LHSCore' Expr
-> [Arg (Pattern' Expr)]
-> [NamedArg (Pattern' Expr)]
-> LHSCore' Expr
forall e.
LHSCore' e
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSWith LHSCore' Expr
core ([Arg (Maybe (Arg (Pattern' Expr)))]
-> [Arg (Pattern' Expr)] -> [Arg (Pattern' Expr)]
forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
insertIn [Arg (Maybe (Arg (Pattern' Expr)))]
ps' [Arg (Pattern' Expr)]
wps) []
LHSCore' Expr
lhs -> LHSCore' Expr
lhs
where
patOfName :: A.BindName -> Arg A.Pattern
patOfName :: BindName -> Arg (Pattern' Expr)
patOfName = Pattern' Expr -> Arg (Pattern' Expr)
forall a. a -> Arg a
defaultArg (Pattern' Expr -> Arg (Pattern' Expr))
-> (BindName -> Pattern' Expr) -> BindName -> Arg (Pattern' Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindName -> Pattern' Expr
forall e. BindName -> Pattern' e
A.VarP
insertIn :: [Arg (Maybe (Arg a))]
-> [Arg a] -> [Arg a]
insertIn :: forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
insertIn [] [Arg a]
wps = [Arg a]
wps
insertIn (Arg ArgInfo
info Maybe (Arg a)
nm : [Arg (Maybe (Arg a))]
ps) (Arg a
w : [Arg a]
wps) | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info =
Arg a
w Arg a -> [Arg a] -> [Arg a]
forall a. a -> [a] -> [a]
: ([Arg a] -> (Arg a -> [Arg a]) -> Maybe (Arg a) -> [Arg a]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Arg a -> [Arg a]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Arg a)
nm) [Arg a] -> [Arg a] -> [Arg a]
forall a. [a] -> [a] -> [a]
++ [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
insertIn [Arg (Maybe (Arg a))]
ps [Arg a]
wps
insertIn (Arg ArgInfo
info Maybe (Arg a)
nm : [Arg (Maybe (Arg a))]
ps) [Arg a]
wps | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info =
([Arg a] -> (Arg a -> [Arg a]) -> Maybe (Arg a) -> [Arg a]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Arg a -> [Arg a]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Arg a)
nm) [Arg a] -> [Arg a] -> [Arg a]
forall a. [a] -> [a] -> [a]
++ [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
forall a. [Arg (Maybe (Arg a))] -> [Arg a] -> [Arg a]
insertIn [Arg (Maybe (Arg a))]
ps [Arg a]
wps
insertIn [Arg (Maybe (Arg a))]
_ [Arg a]
_ = [Arg a]
forall a. HasCallStack => a
__IMPOSSIBLE__
insertPatterns :: [Arg A.Pattern] -> A.RHS -> A.RHS
insertPatterns :: [Arg (Pattern' Expr)] -> RHS -> RHS
insertPatterns [Arg (Pattern' Expr)]
pats = (LHSCore' Expr -> LHSCore' Expr) -> RHS -> RHS
mapLHSCores ([Arg (Pattern' Expr)] -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore [Arg (Pattern' Expr)]
pats)
insertPatternsLHSCore :: [Arg A.Pattern] -> A.LHSCore -> A.LHSCore
insertPatternsLHSCore :: [Arg (Pattern' Expr)] -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore [Arg (Pattern' Expr)]
pats = \case
A.LHSWith LHSCore' Expr
core [Arg (Pattern' Expr)]
wps [] -> LHSCore' Expr
-> [Arg (Pattern' Expr)]
-> [NamedArg (Pattern' Expr)]
-> LHSCore' Expr
forall e.
LHSCore' e
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSWith LHSCore' Expr
core ([Arg (Pattern' Expr)]
pats [Arg (Pattern' Expr)]
-> [Arg (Pattern' Expr)] -> [Arg (Pattern' Expr)]
forall a. [a] -> [a] -> [a]
++ [Arg (Pattern' Expr)]
wps) []
LHSCore' Expr
core -> LHSCore' Expr
-> [Arg (Pattern' Expr)]
-> [NamedArg (Pattern' Expr)]
-> LHSCore' Expr
forall e.
LHSCore' e
-> [Arg (Pattern' e)] -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSWith LHSCore' Expr
core [Arg (Pattern' Expr)]
pats []
data WithFunctionProblem
= NoWithFunction
| WithFunction
{ WithFunctionProblem -> QName
wfParentName :: QName
, WithFunctionProblem -> QName
wfName :: QName
, WithFunctionProblem -> Type
wfParentType :: Type
, WithFunctionProblem -> Tele (Dom Type)
wfParentTel :: Telescope
, WithFunctionProblem -> Tele (Dom Type)
wfBeforeTel :: Telescope
, WithFunctionProblem -> Tele (Dom Type)
wfAfterTel :: Telescope
, WithFunctionProblem -> [Arg (Term, EqualityView)]
wfExprs :: [Arg (Term, EqualityView)]
, WithFunctionProblem -> Type
wfRHSType :: Type
, WithFunctionProblem -> [NamedArg DeBruijnPattern]
wfParentPats :: [NamedArg DeBruijnPattern]
, WithFunctionProblem -> Int
wfParentParams :: Nat
, WithFunctionProblem -> Permutation
wfPermSplit :: Permutation
, WithFunctionProblem -> Permutation
wfPermParent :: Permutation
, WithFunctionProblem -> Permutation
wfPermFinal :: Permutation
, WithFunctionProblem -> List1 (Clause' LHS)
wfClauses :: List1 A.Clause
, WithFunctionProblem -> Substitution
wfCallSubst :: Substitution
, WithFunctionProblem -> Map Name LetBinding
wfLetBindings :: Map Name LetBinding
}
checkSystemCoverage
:: QName
-> [Int]
-> Type
-> [Clause]
-> TCM System
checkSystemCoverage :: QName -> [Int] -> Type -> [Clause] -> TCMT IO System
checkSystemCoverage QName
f [Int
n] Type
t [Clause]
cs = do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.sys.cover" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ((Int, Int) -> [Char]
forall a. Show a => a -> [Char]
show (Int
n , [Clause] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
cs)) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
TelV gamma t <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
n Type
t
addContext gamma $ do
TelV (ExtendTel a _) _ <- telViewUpTo 1 t
a <- reduce $ unEl $ unDom a
case a of
Def QName
q [Apply Arg Term
phi] -> do
[iz,io] <- (BuiltinId -> TCMT IO (Maybe QName))
-> [BuiltinId] -> TCMT IO [Maybe QName]
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 BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' [BuiltinId
builtinIZero, BuiltinId
builtinIOne]
ineg <- primINeg
imin <- primIMin
imax <- primIMax
i0 <- primIZero
i1 <- primIOne
let
isDir (ConP ConHead
q ConPatternInfo
_ []) | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
iz = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
isDir (ConP ConHead
q ConPatternInfo
_ []) | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
io = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
isDir DeBruijnPattern
_ = Maybe Bool
forall a. Maybe a
Nothing
collectDirs :: [Int] -> [DeBruijnPattern] -> [(Int,Bool)]
collectDirs [] [] = []
collectDirs (Int
i : [Int]
is) (DeBruijnPattern
p : [DeBruijnPattern]
ps) | Just Bool
d <- DeBruijnPattern -> Maybe Bool
isDir DeBruijnPattern
p = (Int
i,Bool
d) (Int, Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. a -> [a] -> [a]
: [Int] -> [DeBruijnPattern] -> [(Int, Bool)]
collectDirs [Int]
is [DeBruijnPattern]
ps
| Bool
otherwise = [Int] -> [DeBruijnPattern] -> [(Int, Bool)]
collectDirs [Int]
is [DeBruijnPattern]
ps
collectDirs [Int]
_ [DeBruijnPattern]
_ = [(Int, Bool)]
forall a. HasCallStack => a
__IMPOSSIBLE__
dir :: (Int,Bool) -> Term
dir (Int
i,Bool
False) = Term
ineg Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i]
dir (Int
i,Bool
True) = Int -> Term
var Int
i
andI, orI :: [Term] -> Term
andI [] = Term
i1
andI [Term
t] = Term
t
andI (Term
t:[Term]
ts) = (\ Term
x -> Term
imin Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argN Term
t, Term -> Arg Term
forall a. a -> Arg a
argN Term
x]) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Term
andI [Term]
ts
orI [] = Term
i0
orI [Term
t] = Term
t
orI (Term
t:[Term]
ts) = Term
imax Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argN Term
t, Term -> Arg Term
forall a. a -> Arg a
argN ([Term] -> Term
orI [Term]
ts)]
let
pats = (Clause -> [DeBruijnPattern]) -> [Clause] -> [[DeBruijnPattern]]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [DeBruijnPattern] -> [DeBruijnPattern]
forall a. Int -> [a] -> [a]
take Int
n ([DeBruijnPattern] -> [DeBruijnPattern])
-> (Clause -> [DeBruijnPattern]) -> Clause -> [DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map (Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> (NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> DeBruijnPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> Named NamedName DeBruijnPattern
forall e. Arg e -> e
unArg) ([NamedArg DeBruijnPattern] -> [DeBruijnPattern])
-> (Clause -> [NamedArg DeBruijnPattern])
-> Clause
-> [DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [NamedArg DeBruijnPattern]
namedClausePats) [Clause]
cs
alphas :: [[(Int,Bool)]]
alphas = ([DeBruijnPattern] -> [(Int, Bool)])
-> [[DeBruijnPattern]] -> [[(Int, Bool)]]
forall a b. (a -> b) -> [a] -> [b]
map ([Int] -> [DeBruijnPattern] -> [(Int, Bool)]
collectDirs (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n)) [[DeBruijnPattern]]
pats
phis :: [Term]
phis = ([(Int, Bool)] -> Term) -> [[(Int, Bool)]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ([Term] -> Term
andI ([Term] -> Term)
-> ([(Int, Bool)] -> [Term]) -> [(Int, Bool)] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Int, Bool) -> Term) -> [(Int, Bool)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Bool) -> Term
dir)) [[(Int, Bool)]]
alphas
psi = [Term] -> Term
orI ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ [Term]
phis
pcs = [Term] -> [Clause] -> [(Term, Clause)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Term]
phis [Clause]
cs
reportSDoc "tc.sys.cover" 20 $ fsep $ map prettyTCM pats
interval <- primIntervalType
reportSDoc "tc.sys.cover" 10 $ "equalTerm " <+> prettyTCM (unArg phi) <+> prettyTCM psi
equalTerm interval (unArg phi) psi
forM_ (initWithDefault __IMPOSSIBLE__ $
initWithDefault __IMPOSSIBLE__ $ List.tails pcs) $ \ ((Term
phi1,Clause
cl1):[(Term, Clause)]
pcs') -> do
[(Term, Clause)] -> ((Term, Clause) -> TCMT IO [()]) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Term, Clause)]
pcs' (((Term, Clause) -> TCMT IO [()]) -> TCM ())
-> ((Term, Clause) -> TCMT IO [()]) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (Term
phi2,Clause
cl2) -> do
phi12 <- Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
imin Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
argN Term
phi1, Term -> Arg Term
forall a. a -> Arg a
argN Term
phi2])
forallFaceMaps phi12 (\ IntMap Bool
_ Blocker
_ -> Term -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__) $ \IntMap Bool
_ Substitution
sigma -> do
let args :: [Arg Term]
args = Substitution
Substitution' (SubstArg [Arg Term])
sigma Substitution' (SubstArg [Arg Term]) -> [Arg Term] -> [Arg Term]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Tele (Dom Type) -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs Tele (Dom Type)
gamma
t' :: Type
t' = Substitution
Substitution' (SubstArg Type)
sigma Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Type
t
fromReduced :: Reduced (Blocked' t yes) yes -> yes
fromReduced (YesReduction Simplification
_ yes
x) = yes
x
fromReduced (NoReduction Blocked' t yes
x) = Blocked' t yes -> yes
forall t a. Blocked' t a -> a
ignoreBlocking Blocked' t yes
x
body :: Clause -> TCMT IO Term
body Clause
cl = do
let extra :: Int
extra = [NamedArg DeBruijnPattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
drop Int
n ([NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl)
TelV delta _ <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
extra Type
t'
fmap (abstract delta) $ addContext delta $ do
fmap fromReduced $ runReduceM $
appDef' f (Def f []) [cl] [] (map notReduced $ raise (size delta) args ++ teleArgs delta)
v1 <- Clause -> TCMT IO Term
body Clause
cl1
v2 <- body cl2
equalTerm t' v1 v2
sys <- forM (zip alphas cs) $ \ ([(Int, Bool)]
alpha,Clause
cl) -> do
let
delta :: Tele (Dom Type)
delta = Clause -> Tele (Dom Type)
clauseTel Clause
cl
Just Term
b = Clause -> Maybe Term
clauseBody Clause
cl
ps :: [NamedArg DeBruijnPattern]
ps = Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl
extra :: Int
extra = [NamedArg DeBruijnPattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Int -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Int -> [a] -> [a]
drop (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
gamma Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [NamedArg DeBruijnPattern]
ps)
takeLast :: Int -> [a] -> [a]
takeLast Int
n [a]
xs = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) [a]
xs
weak :: [Int] -> Substitution' a
weak [] = Substitution' a
forall a. Substitution' a
idS
weak (Int
i:[Int]
is) = [Int] -> Substitution' a
weak [Int]
is Substitution' a -> Substitution' a -> Substitution' a
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Int -> Substitution' a -> Substitution' a
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
i (Int -> Substitution' a
forall a. Int -> Substitution' a
raiseS Int
1)
tel :: Tele (Dom Type)
tel = [Dom ([Char], Type)] -> Tele (Dom Type)
telFromList (Int -> [Dom ([Char], Type)] -> [Dom ([Char], Type)]
forall a. Int -> [a] -> [a]
takeLast Int
extra (Tele (Dom Type) -> [Dom ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
delta))
u :: Term
u = Tele (Dom Type) -> Term -> Term
forall t. Abstract t => Tele (Dom Type) -> t -> t
abstract Tele (Dom Type)
tel (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
extra ([Int] -> Substitution
forall {a}.
(SubstArg a ~ a, Subst a, DeBruijn a) =>
[Int] -> Substitution' a
weak ([Int] -> Substitution) -> [Int] -> Substitution
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. Ord a => [a] -> [a]
List.sort ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Bool) -> Int) -> [(Int, Bool)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Bool) -> Int
forall a b. (a, b) -> a
fst [(Int, Bool)]
alpha) Substitution' (SubstArg Term) -> Term -> Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
b)
([(Term, Bool)], Term) -> TCMT IO ([(Term, Bool)], Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Int, Bool) -> (Term, Bool)) -> [(Int, Bool)] -> [(Term, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Term) -> (Int, Bool) -> (Term, Bool)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Int -> Term
var) [(Int, Bool)]
alpha,Term
u)
reportSDoc "tc.sys.cover.sys" 20 $ fsep $ prettyTCM gamma : map prettyTCM sys
reportSDoc "tc.sys.cover.sys" 40 $ fsep $ (text . show) gamma : map (text . show) sys
return (System gamma sys)
Term
_ -> TCMT IO System
forall a. HasCallStack => a
__IMPOSSIBLE__
checkSystemCoverage QName
_ [Int]
_ Type
t [Clause]
cs = TCMT IO System
forall a. HasCallStack => a
__IMPOSSIBLE__
data ClausesPostChecks = CPC
{ ClausesPostChecks -> IntSet
cpcPartialSplits :: IntSet
}
instance Semigroup ClausesPostChecks where
CPC IntSet
xs <> :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks
<> CPC IntSet
xs' = IntSet -> ClausesPostChecks
CPC (IntSet -> IntSet -> IntSet
IntSet.union IntSet
xs IntSet
xs')
instance Monoid ClausesPostChecks where
mempty :: ClausesPostChecks
mempty = IntSet -> ClausesPostChecks
CPC IntSet
forall a. Null a => a
empty
mappend :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks
mappend = ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks
forall a. Semigroup a => a -> a -> a
(<>)
checkClauseLHS :: Type -> Maybe Substitution -> A.SpineClause -> (LHSResult -> TCM a) -> TCM a
checkClauseLHS :: forall a.
Type
-> Maybe Substitution
-> SpineClause
-> (LHSResult -> TCM a)
-> TCM a
checkClauseLHS Type
t Maybe Substitution
withSub c :: SpineClause
c@(A.Clause lhs :: SpineLHS
lhs@(A.SpineLHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps) [ProblemEq]
strippedPats RHS
rhs0 WhereDeclarations
wh Bool
catchall) LHSResult -> TCM a
ret = do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checking clause" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ SpineClause -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA SpineClause
c
[NamedArg (Pattern' Expr)]
-> ([NamedArg (Pattern' Expr)] -> TCM ()) -> TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ([NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
trailingWithPatterns [NamedArg (Pattern' Expr)]
aps) (([NamedArg (Pattern' Expr)] -> TCM ()) -> TCM ())
-> ([NamedArg (Pattern' Expr)] -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ [NamedArg (Pattern' Expr)]
withPats -> do
TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [Pattern' Expr] -> TypeError
UnexpectedWithPatterns ([Pattern' Expr] -> TypeError) -> [Pattern' Expr] -> TypeError
forall a b. (a -> b) -> a -> b
$ (NamedArg (Pattern' Expr) -> Pattern' Expr)
-> [NamedArg (Pattern' Expr)] -> [Pattern' Expr]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg (Pattern' Expr) -> Pattern' Expr
forall a. NamedArg a -> a
namedArg [NamedArg (Pattern' Expr)]
withPats
Call -> TCM a -> TCM a
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Type -> SpineClause -> Call
CheckClause Type
t SpineClause
c) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
aps <- [NamedArg (Pattern' Expr)] -> TCM [NamedArg (Pattern' Expr)]
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms [NamedArg (Pattern' Expr)]
aps
unless (null strippedPats) $ reportSDoc "tc.lhs.top" 50 $
"strippedPats:" <+> vcat [ prettyA p <+> "=" <+> prettyTCM v <+> ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ]
closed_t <- flip abstract t <$> getContextTelescope
checkLeftHandSide (CheckLHS lhs) (getRange lhs) (Just x) aps t withSub strippedPats ret
checkClause
:: Type
-> Maybe (Substitution, Map Name LetBinding)
-> A.SpineClause
-> TCM (Clause, ClausesPostChecks)
checkClause :: Type
-> Maybe (Substitution, Map Name LetBinding)
-> SpineClause
-> TCMT IO (Clause, ClausesPostChecks)
checkClause Type
t Maybe (Substitution, Map Name LetBinding)
withSubAndLets c :: SpineClause
c@(A.Clause lhs :: SpineLHS
lhs@(A.SpineLHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps) [ProblemEq]
strippedPats RHS
rhs0 WhereDeclarations
wh Bool
catchall) = do
let withSub :: Maybe Substitution
withSub = (Substitution, Map Name LetBinding) -> Substitution
forall a b. (a, b) -> a
fst ((Substitution, Map Name LetBinding) -> Substitution)
-> Maybe (Substitution, Map Name LetBinding) -> Maybe Substitution
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Substitution, Map Name LetBinding)
withSubAndLets
cxtNames <- [Name] -> [Name]
forall a. [a] -> [a]
reverse ([Name] -> [Name])
-> ([Dom' Term (Name, Type)] -> [Name])
-> [Dom' Term (Name, Type)]
-> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom' Term (Name, Type) -> Name)
-> [Dom' Term (Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
unDom) ([Dom' Term (Name, Type)] -> [Name])
-> TCMT IO [Dom' Term (Name, Type)] -> TCMT IO [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Dom' Term (Name, Type)]
forall (m :: * -> *). MonadTCEnv m => m [Dom' Term (Name, Type)]
getContext
checkClauseLHS t withSub c $ \ lhsResult :: LHSResult
lhsResult@(LHSResult Int
npars Tele (Dom Type)
delta [NamedArg DeBruijnPattern]
ps Bool
absurdPat Arg Type
trhs Substitution
patSubst [AsBinding]
asb IntSet
psplit Bool
ixsplit) -> do
let installInheritedLets :: TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
installInheritedLets TCMT IO (Clause, ClausesPostChecks)
k
| Just (Substitution
withSub, Map Name LetBinding
lets) <- Maybe (Substitution, Map Name LetBinding)
withSubAndLets = do
lets' <- (LetBinding -> TCMT IO (Open LetBinding))
-> Map Name LetBinding -> TCMT IO (Map Name (Open LetBinding))
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) -> Map Name a -> f (Map Name b)
traverse LetBinding -> TCMT IO (Open LetBinding)
forall (m :: * -> *) a.
(ReadTCState m, MonadTCEnv m) =>
a -> m (Open a)
makeOpen (Map Name LetBinding -> TCMT IO (Map Name (Open LetBinding)))
-> Map Name LetBinding -> TCMT IO (Map Name (Open LetBinding))
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg (Map Name LetBinding))
-> Map Name LetBinding -> Map Name LetBinding
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Substitution
patSubst Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Substitution
withSub) Map Name LetBinding
lets
locallyTC eLetBindings (lets' <>) k
| Bool
otherwise = TCMT IO (Clause, ClausesPostChecks)
k
TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
installInheritedLets (TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks))
-> TCMT IO (Clause, ClausesPostChecks)
-> TCMT IO (Clause, ClausesPostChecks)
forall a b. (a -> b) -> a -> b
$ do
t' <- case Maybe Substitution
withSub of
Just{} -> Type -> TCMT IO Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
Maybe Substitution
Nothing -> do
theta <- ModuleName -> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection (QName -> ModuleName
qnameModule QName
x)
return $ abstract theta t
let rhs = RHS -> RHS
updateRHS RHS
rhs0
updateRHS rhs :: RHS
rhs@A.RHS{} = RHS
rhs
updateRHS rhs :: RHS
rhs@A.AbsurdRHS{} = RHS
rhs
updateRHS (A.WithRHS QName
q [WithExpr]
es List1 (Clause' LHS)
cs) = QName -> [WithExpr] -> List1 (Clause' LHS) -> RHS
A.WithRHS QName
q [WithExpr]
es (List1 (Clause' LHS) -> RHS) -> List1 (Clause' LHS) -> RHS
forall a b. (a -> b) -> a -> b
$ (Clause' LHS -> Clause' LHS)
-> List1 (Clause' LHS) -> List1 (Clause' LHS)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Clause' LHS -> Clause' LHS
updateClause List1 (Clause' LHS)
cs
updateRHS (A.RewriteRHS [RewriteEqn]
qes [ProblemEq]
spats RHS
rhs WhereDeclarations
wh) =
[RewriteEqn] -> [ProblemEq] -> RHS -> WhereDeclarations -> RHS
A.RewriteRHS [RewriteEqn]
qes (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [ProblemEq])
patSubst [ProblemEq]
spats) (RHS -> RHS
updateRHS RHS
rhs) WhereDeclarations
wh
updateClause (A.Clause LHS
f [ProblemEq]
spats RHS
rhs WhereDeclarations
wh Bool
ca) =
LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' LHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
f (Substitution' (SubstArg [ProblemEq]) -> [ProblemEq] -> [ProblemEq]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [ProblemEq])
patSubst [ProblemEq]
spats) (RHS -> RHS
updateRHS RHS
rhs) WhereDeclarations
wh Bool
ca
(body, with) <- bindAsPatterns asb $ checkWhere wh $ checkRHS i x aps t' lhsResult rhs
wbody <- unsafeInTopContext $ Bench.billTo [Bench.Typing, Bench.With] $ checkWithFunction cxtNames with
body <- return $ body `mplus` wbody
whenM (optDoubleCheck <$> pragmaOptions) $ case body of
Just Term
v -> do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.lhs.top" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
vcat
[ TCMT IO Doc
"double checking rhs"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" : " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs))
]
TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadMetaSolver m, MonadTCState m) =>
m a -> m a
withFrozenMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Comparison -> TypeOf Term -> TCM ()
forall a (m :: * -> *).
(CheckInternal a, MonadCheckInternal m) =>
a -> Comparison -> TypeOf a -> m ()
forall (m :: * -> *).
MonadCheckInternal m =>
Term -> Comparison -> TypeOf Term -> m ()
checkInternal Term
v Comparison
CmpLeq (TypeOf Term -> TCM ()) -> TypeOf Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs
Maybe Term
Nothing -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
reportSDoc "tc.lhs.top" 10 $ vcat
[ "Clause before translation:"
, nest 2 $ vcat
[ "delta =" <+> do escapeContext impossible (size delta) $ prettyTCM delta
, "ps =" <+> do P.fsep <$> prettyTCMPatterns ps
, "body =" <+> maybe "_|_" prettyTCM body
, "type =" <+> prettyTCM t
]
]
reportSDoc "tc.lhs.top" 60 $ escapeContext impossible (size delta) $ vcat
[ "Clause before translation (raw):"
, nest 2 $ vcat
[ "ps =" <+> text (show ps)
, "body =" <+> text (show body)
, "type =" <+> text (show t)
]
]
rel <- viewTC eRelevance
let bodyMod Maybe Term
body = case Relevance
rel of
Relevance
Irrelevant -> Term -> Term
dontCare (Term -> Term) -> Maybe Term -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Term
body
Relevance
_ -> Maybe Term
body
let catchall' = Bool
catchall Bool -> Bool -> Bool
|| Maybe Term -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Term
body
let exact = if Maybe Term -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Term
body then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False else Maybe Bool
forall a. Maybe a
Nothing
return $ (, CPC psplit)
Clause { clauseLHSRange = getRange i
, clauseFullRange = getRange c
, clauseTel = killRange delta
, namedClausePats = ps
, clauseBody = bodyMod body
, clauseType = Just trhs
, clauseCatchall = catchall'
, clauseExact = exact
, clauseRecursive = Nothing
, clauseUnreachable = Nothing
, clauseEllipsis = lhsEllipsis i
, clauseWhereModule = A.whereModule wh
}
getReflPattern :: TCM A.Pattern
getReflPattern :: TCM (Pattern' Expr)
getReflPattern = do
Con reflCon _ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl
reflInfo <- fmap (setOrigin Inserted) <$> getReflArgInfo reflCon
let patInfo = ConInfo -> PatInfo -> ConPatLazy -> ConPatInfo
ConPatInfo ConInfo
ConOCon PatInfo
patNoRange ConPatLazy
ConPatEager
let reflArg = Maybe (NamedArg (Pattern' Expr)) -> [NamedArg (Pattern' Expr)]
forall a. Maybe a -> [a]
maybeToList (Maybe (NamedArg (Pattern' Expr)) -> [NamedArg (Pattern' Expr)])
-> Maybe (NamedArg (Pattern' Expr)) -> [NamedArg (Pattern' Expr)]
forall a b. (a -> b) -> a -> b
$ (ArgInfo -> NamedArg (Pattern' Expr))
-> Maybe ArgInfo -> Maybe (NamedArg (Pattern' Expr))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ ArgInfo
ai -> ArgInfo
-> Named NamedName (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Named NamedName (Pattern' Expr) -> NamedArg (Pattern' Expr))
-> Named NamedName (Pattern' Expr) -> NamedArg (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ Pattern' Expr -> Named NamedName (Pattern' Expr)
forall a name. a -> Named name a
unnamed (Pattern' Expr -> Named NamedName (Pattern' Expr))
-> Pattern' Expr -> Named NamedName (Pattern' Expr)
forall a b. (a -> b) -> a -> b
$ PatInfo -> Pattern' Expr
forall e. PatInfo -> Pattern' e
A.WildP PatInfo
patNoRange) Maybe ArgInfo
reflInfo
pure $ A.ConP patInfo (unambiguous $ conName reflCon) reflArg
checkRHS
:: LHSInfo
-> QName
-> [NamedArg A.Pattern]
-> Type
-> LHSResult
-> A.RHS
-> TCM (Maybe Term, WithFunctionProblem)
checkRHS :: LHSInfo
-> QName
-> [NamedArg (Pattern' Expr)]
-> Type
-> LHSResult
-> RHS
-> TCM (Maybe Term, WithFunctionProblem)
checkRHS LHSInfo
i QName
x [NamedArg (Pattern' Expr)]
aps Type
t lhsResult :: LHSResult
lhsResult@(LHSResult Int
_ Tele (Dom Type)
delta [NamedArg DeBruijnPattern]
ps Bool
absurdPat Arg Type
trhs Substitution
_ [AsBinding]
_asb IntSet
_ Bool
_) RHS
rhs0 =
RHS -> TCM (Maybe Term, WithFunctionProblem)
handleRHS RHS
rhs0 where
handleRHS :: A.RHS -> TCM (Maybe Term, WithFunctionProblem)
handleRHS :: RHS -> TCM (Maybe Term, WithFunctionProblem)
handleRHS RHS
rhs = case RHS
rhs of
A.RHS Expr
e Maybe Expr
_ -> Expr -> TCM (Maybe Term, WithFunctionProblem)
ordinaryRHS Expr
e
RHS
A.AbsurdRHS -> TCM (Maybe Term, WithFunctionProblem)
noRHS
A.RewriteRHS [RewriteEqn]
eqs [ProblemEq]
ps RHS
rhs WhereDeclarations
wh -> [RewriteEqn]
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnsRHS [RewriteEqn]
eqs [ProblemEq]
ps RHS
rhs WhereDeclarations
wh
A.WithRHS QName
aux [WithExpr]
es List1 (Clause' LHS)
cs -> QName
-> [WithExpr]
-> List1 (Clause' LHS)
-> TCM (Maybe Term, WithFunctionProblem)
withRHS QName
aux [WithExpr]
es List1 (Clause' LHS)
cs
ordinaryRHS :: A.Expr -> TCM (Maybe Term, WithFunctionProblem)
ordinaryRHS :: Expr -> TCM (Maybe Term, WithFunctionProblem)
ordinaryRHS Expr
e = Account (BenchPhase (TCMT IO))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.CheckRHS] (TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ do
mv <- if Bool
absurdPat
then do
ps <- [NamedArg DeBruijnPattern] -> TCMT IO [NamedArg DeBruijnPattern]
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull [NamedArg DeBruijnPattern]
ps
Nothing <$ setCurrentRange e (warning $ AbsurdPatternRequiresNoRHS ps)
else Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> TCMT IO Term -> TCMT IO (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Type -> TCMT IO Term
checkExpr Expr
e (Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
trhs)
return (mv, NoWithFunction)
noRHS :: TCM (Maybe Term, WithFunctionProblem)
noRHS :: TCM (Maybe Term, WithFunctionProblem)
noRHS = do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
absurdPat (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ [NamedArg (Pattern' Expr)] -> TypeError
NoRHSRequiresAbsurdPattern [NamedArg (Pattern' Expr)]
aps
(Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term
forall a. Maybe a
Nothing, WithFunctionProblem
NoWithFunction)
withRHS ::
QName
-> [A.WithExpr]
-> List1 A.Clause
-> TCM (Maybe Term, WithFunctionProblem)
withRHS :: QName
-> [WithExpr]
-> List1 (Clause' LHS)
-> TCM (Maybe Term, WithFunctionProblem)
withRHS QName
aux [WithExpr]
es List1 (Clause' LHS)
cs = do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
vcat
[ TCMT IO Doc
"TC.Rules.Def.checkclause reached A.WithRHS"
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA QName
aux TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: (WithExpr -> TCMT IO Doc) -> [WithExpr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (TCMT IO Doc -> TCMT IO Doc)
-> (WithExpr -> TCMT IO Doc) -> WithExpr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Arg Expr -> TCMT IO Doc)
-> (WithExpr -> Arg Expr) -> WithExpr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithExpr -> Arg Expr
forall name a. Named name a -> a
namedThing) [WithExpr]
es
]
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
nfv <- TCM Int
getCurrentModuleFreeVars
m <- currentModule
sep [ "with function module:" <+>
prettyList (map prettyTCM $ mnameToList m)
, text $ "free variables: " ++ show nfv
]
vtys <- [WithExpr]
-> (WithExpr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO [Arg (Term, EqualityView)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [WithExpr]
es ((WithExpr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO [Arg (Term, EqualityView)])
-> (WithExpr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO [Arg (Term, EqualityView)]
forall a b. (a -> b) -> a -> b
$ \ (Named Maybe BindName
nm Arg Expr
we) -> do
(e, ty) <- Arg Expr -> TCM (Term, Type)
inferExprForWith Arg Expr
we
pure $ (<$ we) . (e,) $ case nm of
Maybe BindName
Nothing -> Type -> EqualityView
OtherType Type
ty
Just{} -> Type -> EqualityView
IdiomType Type
ty
let names = (WithExpr -> Arg (Maybe BindName))
-> [WithExpr] -> [Arg (Maybe BindName)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Named Maybe BindName
nm Arg Expr
e) -> Maybe BindName
nm Maybe BindName -> Arg Expr -> Arg (Maybe BindName)
forall a b. a -> Arg b -> Arg a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Arg Expr
e) [WithExpr]
es
cs <- forM cs $ \ c :: Clause' LHS
c@(A.Clause (A.LHS LHSInfo
i LHSCore' Expr
core) [ProblemEq]
eqs RHS
rhs WhereDeclarations
wh Bool
b) -> do
let rhs' :: RHS
rhs' = [Arg (Maybe BindName)] -> RHS -> RHS
insertNames [Arg (Maybe BindName)]
names RHS
rhs
let core' :: LHSCore' Expr
core' = [Arg (Maybe BindName)] -> LHSCore' Expr -> LHSCore' Expr
insertInspects [Arg (Maybe BindName)]
names LHSCore' Expr
core
Clause' LHS -> TCMT IO (Clause' LHS)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Clause' LHS -> TCMT IO (Clause' LHS))
-> Clause' LHS -> TCMT IO (Clause' LHS)
forall a b. (a -> b) -> a -> b
$ LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' LHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
i LHSCore' Expr
core') [ProblemEq]
eqs RHS
rhs' WhereDeclarations
wh Bool
b
solveSizeConstraints DefaultToInfty
checkWithRHS x aux t lhsResult vtys cs
rewriteEqnsRHS
:: [A.RewriteEqn]
-> [A.ProblemEq]
-> A.RHS
-> A.WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnsRHS :: [RewriteEqn]
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnsRHS [] [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh = WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. WhereDeclarations -> TCM a -> TCM a
checkWhere WhereDeclarations
wh (TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ RHS -> TCM (Maybe Term, WithFunctionProblem)
handleRHS RHS
rhs
rewriteEqnsRHS (RewriteEqn
r:[RewriteEqn]
rs) [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh = case RewriteEqn
r of
Rewrite ((QName
qname, Expr
eq) :| [(QName, Expr)]
qes) ->
QName
-> Expr -> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnRHS QName
qname Expr
eq ([RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem))
-> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$
[(QName, Expr)]
-> [RewriteEqn]
-> (NonEmpty (QName, Expr) -> [RewriteEqn])
-> [RewriteEqn]
forall a b. [a] -> b -> (List1 a -> b) -> b
List1.ifNull [(QName, Expr)]
qes [RewriteEqn]
rs ((NonEmpty (QName, Expr) -> [RewriteEqn]) -> [RewriteEqn])
-> (NonEmpty (QName, Expr) -> [RewriteEqn]) -> [RewriteEqn]
forall a b. (a -> b) -> a -> b
$ \ NonEmpty (QName, Expr)
qes -> NonEmpty (QName, Expr) -> RewriteEqn
forall qn nm p e. List1 (qn, e) -> RewriteEqn' qn nm p e
Rewrite NonEmpty (QName, Expr)
qes RewriteEqn -> [RewriteEqn] -> [RewriteEqn]
forall a. a -> [a] -> [a]
: [RewriteEqn]
rs
Invert QName
qname List1 (Named BindName (Pattern' Expr, Expr))
pes -> QName
-> [Named BindName (Pattern' Expr, Expr)]
-> [RewriteEqn]
-> TCM (Maybe Term, WithFunctionProblem)
invertEqnRHS QName
qname (List1 (Named BindName (Pattern' Expr, Expr))
-> [Item (List1 (Named BindName (Pattern' Expr, Expr)))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Named BindName (Pattern' Expr, Expr))
pes) [RewriteEqn]
rs
LeftLet List1 (Pattern' Expr, Expr)
pes -> [(Pattern' Expr, Expr)]
-> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
usingEqnRHS (List1 (Pattern' Expr, Expr) -> [Item (List1 (Pattern' Expr, Expr))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Pattern' Expr, Expr)
pes) [RewriteEqn]
rs
where
usingEqnRHS :: [(A.Pattern, A.Expr)] -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
usingEqnRHS :: [(Pattern' Expr, Expr)]
-> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
usingEqnRHS [(Pattern' Expr, Expr)]
pes [RewriteEqn]
rs = do
let letBindings :: [LetBinding]
letBindings = [(Pattern' Expr, Expr)]
-> ((Pattern' Expr, Expr) -> LetBinding) -> [LetBinding]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for ([(Pattern' Expr, Expr)] -> [Item [(Pattern' Expr, Expr)]]
forall l. IsList l => l -> [Item l]
List1.toList [(Pattern' Expr, Expr)]
pes) (((Pattern' Expr, Expr) -> LetBinding) -> [LetBinding])
-> ((Pattern' Expr, Expr) -> LetBinding) -> [LetBinding]
forall a b. (a -> b) -> a -> b
$ \(Pattern' Expr
p, Expr
e) -> LetInfo -> Pattern' Expr -> Expr -> LetBinding
A.LetPatBind (Range -> LetInfo
LetRange (Range -> LetInfo) -> Range -> LetInfo
forall a b. (a -> b) -> a -> b
$ Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e) Pattern' Expr
p Expr
e
[LetBinding]
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings [LetBinding]
letBindings (TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ [RewriteEqn]
-> [ProblemEq]
-> RHS
-> WhereDeclarations
-> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnsRHS [RewriteEqn]
rs [ProblemEq]
strippedPats RHS
rhs WhereDeclarations
wh
invertEqnRHS :: QName -> [Named A.BindName (A.Pattern,A.Expr)] -> [A.RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
invertEqnRHS :: QName
-> [Named BindName (Pattern' Expr, Expr)]
-> [RewriteEqn]
-> TCM (Maybe Term, WithFunctionProblem)
invertEqnRHS QName
qname [Named BindName (Pattern' Expr, Expr)]
pes [RewriteEqn]
rs = do
let ([Named BindName (Pattern' Expr)]
npats, [Named BindName Expr]
es) = (Named BindName (Pattern' Expr, Expr)
-> (Named BindName (Pattern' Expr), Named BindName Expr))
-> [Named BindName (Pattern' Expr, Expr)]
-> ([Named BindName (Pattern' Expr)], [Named BindName Expr])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith (\ (Named Maybe BindName
nm (Pattern' Expr
p , Expr
e)) -> (Maybe BindName -> Pattern' Expr -> Named BindName (Pattern' Expr)
forall name a. Maybe name -> a -> Named name a
Named Maybe BindName
nm Pattern' Expr
p, Maybe BindName -> Expr -> Named BindName Expr
forall name a. Maybe name -> a -> Named name a
Named Maybe BindName
nm Expr
e)) [Named BindName (Pattern' Expr, Expr)]
pes
vtys <- [Named BindName Expr]
-> (Named BindName Expr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO [Arg (Term, EqualityView)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Named BindName Expr]
es ((Named BindName Expr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO [Arg (Term, EqualityView)])
-> (Named BindName Expr -> TCMT IO (Arg (Term, EqualityView)))
-> TCMT IO [Arg (Term, EqualityView)]
forall a b. (a -> b) -> a -> b
$ \ (Named Maybe BindName
nm Expr
we) -> do
(e, ty) <- Arg Expr -> TCM (Term, Type)
inferExprForWith (Expr -> Arg Expr
forall a. a -> Arg a
defaultArg Expr
we)
pure $ defaultArg . (e,) $ case nm of
Maybe BindName
Nothing -> Type -> EqualityView
OtherType Type
ty
Just{} -> Type -> EqualityView
IdiomType Type
ty
let pats = ([Pattern' Expr] -> [Arg (Pattern' Expr)])
-> [[Pattern' Expr]] -> [Arg (Pattern' Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Pattern' Expr -> Arg (Pattern' Expr))
-> [Pattern' Expr] -> [Arg (Pattern' Expr)]
forall a b. (a -> b) -> [a] -> [b]
map Pattern' Expr -> Arg (Pattern' Expr)
forall a. a -> Arg a
defaultArg) ([[Pattern' Expr]] -> [Arg (Pattern' Expr)])
-> [[Pattern' Expr]] -> [Arg (Pattern' Expr)]
forall a b. (a -> b) -> a -> b
$
[Named BindName (Pattern' Expr)]
-> (Named BindName (Pattern' Expr) -> [Pattern' Expr])
-> [[Pattern' Expr]]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Named BindName (Pattern' Expr)]
npats ((Named BindName (Pattern' Expr) -> [Pattern' Expr])
-> [[Pattern' Expr]])
-> (Named BindName (Pattern' Expr) -> [Pattern' Expr])
-> [[Pattern' Expr]]
forall a b. (a -> b) -> a -> b
$ \ (Named Maybe BindName
nm Pattern' Expr
p) -> case Maybe BindName
nm of
Maybe BindName
Nothing -> [Pattern' Expr
p]
Just BindName
n -> [Pattern' Expr
p, BindName -> Pattern' Expr
forall e. BindName -> Pattern' e
A.VarP BindName
n]
solveSizeConstraints DefaultToInfty
let rhs' = [Arg (Pattern' Expr)] -> RHS -> RHS
insertPatterns [Arg (Pattern' Expr)]
pats RHS
rhs
(rhs'', outerWhere)
| null rs = (rhs', wh)
| otherwise = (A.RewriteRHS rs strippedPats rhs' wh, A.noWhereDecls)
cl = LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' LHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
i (LHSCore' Expr -> LHS) -> LHSCore' Expr -> LHS
forall a b. (a -> b) -> a -> b
$ [Arg (Pattern' Expr)] -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore [Arg (Pattern' Expr)]
pats (LHSCore' Expr -> LHSCore' Expr) -> LHSCore' Expr -> LHSCore' Expr
forall a b. (a -> b) -> a -> b
$ QName -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSHead QName
x ([NamedArg (Pattern' Expr)] -> LHSCore' Expr)
-> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall a b. (a -> b) -> a -> b
$ [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
forall a. KillRange a => KillRangeT a
killRange [NamedArg (Pattern' Expr)]
aps)
[ProblemEq]
strippedPats RHS
rhs'' WhereDeclarations
outerWhere Bool
False
reportSDoc "tc.invert" 60 $ vcat
[ text "invert"
, " rhs' = " <> (text . show) rhs'
]
checkWithRHS x qname t lhsResult vtys $ singleton cl
rewriteEqnRHS
:: QName
-> A.Expr
-> [A.RewriteEqn]
-> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnRHS :: QName
-> Expr -> [RewriteEqn] -> TCM (Maybe Term, WithFunctionProblem)
rewriteEqnRHS QName
qname Expr
eq [RewriteEqn]
rs = do
st <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
let recurse = do
st' <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
let sameIP = InteractionPoints -> InteractionPoints -> Bool
forall a. Eq a => a -> a -> Bool
(==) (InteractionPoints -> InteractionPoints -> Bool)
-> (TCState -> InteractionPoints) -> TCState -> TCState -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (TCState -> Lens' TCState InteractionPoints -> InteractionPoints
forall o i. o -> Lens' o i -> i
^. (InteractionPoints -> f InteractionPoints) -> TCState -> f TCState
Lens' TCState InteractionPoints
stInteractionPoints)
when (sameIP st st') $ putTC st
handleRHS $ A.RewriteRHS rs strippedPats rhs wh
(proof, eqt) <- inferExpr eq
solveAwakeConstraints
solveSizeConstraints DefaultToInfty
t' <- reduce =<< instantiateFull eqt
(eqt,rewriteType,rewriteFrom,rewriteTo) <- equalityView t' >>= \case
eqt :: EqualityView
eqt@(EqualityType Sort
_s QName
_eq [Arg Term]
_params (Arg ArgInfo
_ Term
dom) Arg Term
a Arg Term
b) -> do
s <- Term -> TCMT IO Sort
forall (m :: * -> *).
(PureTCM m, MonadBlock m, MonadConstraint m) =>
Term -> m Sort
sortOf Term
dom
return (eqt, El s dom, unArg a, unArg b)
OtherType{} -> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (EqualityView, Type, Term, Term))
-> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
CannotRewriteByNonEquation Type
t'
IdiomType{} -> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (EqualityView, Type, Term, Term))
-> TypeError -> TCMT IO (EqualityView, Type, Term, Term)
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
CannotRewriteByNonEquation Type
t'
reflPat <- getReflPattern
let isReflexive = TCM () -> TCMT IO Bool
forall (m :: * -> *).
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m () -> m Bool
tryConversion (TCM () -> TCMT IO Bool) -> TCM () -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
dontAssignMetas (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
rewriteType Term
rewriteFrom Term
rewriteTo
(pats', withExpr, withType) <- do
ifM isReflexive
(return ([ reflPat ] , proof, OtherType t'))
(return ([ A.WildP patNoRange, reflPat ], proof, eqt))
let pats = Pattern' Expr -> Arg (Pattern' Expr)
forall a. a -> Arg a
defaultArg (Pattern' Expr -> Arg (Pattern' Expr))
-> [Pattern' Expr] -> [Arg (Pattern' Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pattern' Expr]
pats'
let rhs' = [Arg (Pattern' Expr)] -> RHS -> RHS
insertPatterns [Arg (Pattern' Expr)]
pats RHS
rhs
(rhs'', outerWhere)
| null rs = (rhs', wh)
| otherwise = (A.RewriteRHS rs strippedPats rhs' wh, A.noWhereDecls)
cl = LHS
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' LHS
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause (LHSInfo -> LHSCore' Expr -> LHS
A.LHS LHSInfo
i (LHSCore' Expr -> LHS) -> LHSCore' Expr -> LHS
forall a b. (a -> b) -> a -> b
$ [Arg (Pattern' Expr)] -> LHSCore' Expr -> LHSCore' Expr
insertPatternsLHSCore [Arg (Pattern' Expr)]
pats (LHSCore' Expr -> LHSCore' Expr) -> LHSCore' Expr -> LHSCore' Expr
forall a b. (a -> b) -> a -> b
$ QName -> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall e. QName -> [NamedArg (Pattern' e)] -> LHSCore' e
A.LHSHead QName
x ([NamedArg (Pattern' Expr)] -> LHSCore' Expr)
-> [NamedArg (Pattern' Expr)] -> LHSCore' Expr
forall a b. (a -> b) -> a -> b
$ [NamedArg (Pattern' Expr)] -> [NamedArg (Pattern' Expr)]
forall a. KillRange a => KillRangeT a
killRange [NamedArg (Pattern' Expr)]
aps)
[ProblemEq]
strippedPats RHS
rhs'' WhereDeclarations
outerWhere Bool
False
reportSDoc "tc.rewrite" 60 $ vcat
[ text "rewrite"
, " rhs' = " <> (text . show) rhs'
]
checkWithRHS x qname t lhsResult [defaultArg (withExpr, withType)] $ singleton cl
checkWithRHS
:: QName
-> QName
-> Type
-> LHSResult
-> [Arg (Term, EqualityView)]
-> List1 A.Clause
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS :: QName
-> QName
-> Type
-> LHSResult
-> [Arg (Term, EqualityView)]
-> List1 (Clause' LHS)
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS QName
x QName
aux Type
t (LHSResult Int
npars Tele (Dom Type)
delta [NamedArg DeBruijnPattern]
ps Bool
_absurdPat Arg Type
trhs Substitution
_ [AsBinding]
_asb IntSet
_ Bool
_) [Arg (Term, EqualityView)]
vtys0 List1 (Clause' LHS)
cs =
[Char]
-> Int
-> [Char]
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a. [Char] -> Int -> [Char] -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
[Char] -> Int -> [Char] -> m a -> m a
verboseBracket [Char]
"tc.with.top" Int
25 [Char]
"checkWithRHS" (TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ do
Account (BenchPhase (TCMT IO))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase (TCMT IO)
Phase
Bench.Typing, BenchPhase (TCMT IO)
Phase
Bench.With] (TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem))
-> TCM (Maybe Term, WithFunctionProblem)
-> TCM (Maybe Term, WithFunctionProblem)
forall a b. (a -> b) -> a -> b
$ do
withArgs <- [Arg (Term, EqualityView)] -> TCM [Arg Term]
withArguments [Arg (Term, EqualityView)]
vtys0
let perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm [NamedArg DeBruijnPattern]
ps
reportSDoc "tc.with.top" 30 $ vcat $
let (vs, as) = unzipWith unArg vtys0 in
[ "vs (before normalization) =" <+> prettyTCM vs
, "as (before normalization) =" <+> prettyTCM as
]
reportSDoc "tc.with.top" 45 $ vcat $
let (vs, as) = unzipWith unArg vtys0 in
[ "vs (before norm., raw) =" <+> pretty vs
]
vtys0 <- normalise vtys0
reportSDoc "tc.with.top" 25 $ escapeContext impossible (size delta) $ vcat
[ "delta =" <+> prettyTCM delta
]
reportSDoc "tc.with.top" 25 $ vcat $
let (vs, as) = unzipWith unArg vtys0 in
[ "vs =" <+> prettyTCM vs
, "as =" <+> prettyTCM as
, "perm =" <+> text (show perm)
]
let (delta1, delta2, perm', t', vtys) = splitTelForWith delta (unArg trhs) vtys0
let finalPerm = Permutation -> Permutation -> Permutation
composeP Permutation
perm' Permutation
perm
reportSLn "tc.with.top" 75 $ "delta = " ++ show delta
reportSDoc "tc.with.top" 25 $ escapeContext impossible (size delta) $ vcat
[ "delta1 =" <+> prettyTCM delta1
, "delta2 =" <+> addContext delta1 (prettyTCM delta2)
]
reportSDoc "tc.with.top" 25 $ vcat
[ "perm' =" <+> text (show perm')
, "fPerm =" <+> text (show finalPerm)
]
us <- getContextTerms
let n = [Term] -> Int
forall a. Sized a => a -> Int
size [Term]
us
m = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta
(us0, us1') = splitAt (n - m) us
(us1, us2) = splitAt (size delta1) $ permute perm' us1'
argsS = [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> Substitution) -> [Term] -> Substitution
forall a b. (a -> b) -> a -> b
$ [Term] -> [Term]
forall a. [a] -> [a]
reverse ([Term] -> [Term]) -> [Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Term]
us0 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
us1 [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg [Arg Term]
withArgs [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
us2
v = Maybe a
forall a. Maybe a
Nothing
addConstant aux =<< do
lang <- getLanguage
useTerPragma =<<
defaultDefn defaultArgInfo aux __DUMMY_TYPE__ lang <$>
emptyFunction
reportSDoc "tc.with.top" 20 $ vcat $
let (vs, as) = unzipWith unArg vtys in
[ " with arguments" <+> do escapeContext impossible (size delta) $ addContext delta1 $ prettyList (map prettyTCM vs)
, " types" <+> do escapeContext impossible (size delta) $ addContext delta1 $ prettyList (map prettyTCM as)
, " context" <+> (prettyTCM =<< getContextTelescope)
, " delta" <+> do escapeContext impossible (size delta) $ prettyTCM delta
, " delta1" <+> do escapeContext impossible (size delta) $ prettyTCM delta1
, " delta2" <+> do escapeContext impossible (size delta) $ addContext delta1 $ prettyTCM delta2
]
lets <- Map.filter ((== UserWritten) . letOrigin) <$> (traverse getOpen =<< viewTC eLetBindings)
return (v, WithFunction x aux t delta delta1 delta2 vtys t' ps npars perm' perm finalPerm cs argsS lets)
checkWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term)
checkWithFunction :: [Name] -> WithFunctionProblem -> TCMT IO (Maybe Term)
checkWithFunction [Name]
_ WithFunctionProblem
NoWithFunction = Maybe Term -> TCMT IO (Maybe Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing
checkWithFunction [Name]
cxtNames (WithFunction QName
f QName
aux Type
t Tele (Dom Type)
delta Tele (Dom Type)
delta1 Tele (Dom Type)
delta2 [Arg (Term, EqualityView)]
vtys Type
b [NamedArg DeBruijnPattern]
qs Int
npars Permutation
perm' Permutation
perm Permutation
finalPerm List1 (Clause' LHS)
cs Substitution
argsS Map Name LetBinding
lets) = do
let
withSub :: Substitution
withSub :: Substitution
withSub = let as :: [EqualityView]
as = (Arg (Term, EqualityView) -> EqualityView)
-> [Arg (Term, EqualityView)] -> [EqualityView]
forall a b. (a -> b) -> [a] -> [b]
map ((Term, EqualityView) -> EqualityView
forall a b. (a, b) -> b
snd ((Term, EqualityView) -> EqualityView)
-> (Arg (Term, EqualityView) -> (Term, EqualityView))
-> Arg (Term, EqualityView)
-> EqualityView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg) [Arg (Term, EqualityView)]
vtys in
Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
liftS (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
delta2) (Int -> Substitution -> Substitution
forall a. Int -> Substitution' a -> Substitution' a
wkS ([EqualityView] -> Int
countWithArgs [EqualityView]
as) Substitution
forall a. Substitution' a
idS)
Substitution -> Substitution -> Substitution
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS` Impossible -> Permutation -> Substitution
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm')
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
vcat
[ TCMT IO Doc
"checkWithFunction"
, Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
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
vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
let ([Term]
vs, [EqualityView]
as) = (Arg (Term, EqualityView) -> (Term, EqualityView))
-> [Arg (Term, EqualityView)] -> ([Term], [EqualityView])
forall a b c. (a -> (b, c)) -> [a] -> ([b], [c])
unzipWith Arg (Term, EqualityView) -> (Term, EqualityView)
forall e. Arg e -> e
unArg [Arg (Term, EqualityView)]
vtys in
[ TCMT IO Doc
"delta1 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
delta1
, TCMT IO Doc
"delta2 =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta1 (Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM Tele (Dom Type)
delta2)
, TCMT IO Doc
"t =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
, TCMT IO Doc
"as =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta1 ([EqualityView] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [EqualityView] -> m Doc
prettyTCM [EqualityView]
as)
, TCMT IO Doc
"vs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Term] -> m Doc
prettyTCM [Term]
vs
, TCMT IO Doc
"b =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta1 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
b
, TCMT IO Doc
"qs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext Tele (Dom Type)
delta (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [NamedArg DeBruijnPattern] -> TCMT IO Doc
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList [NamedArg DeBruijnPattern]
qs
, TCMT IO Doc
"perm' =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
perm')
, TCMT IO Doc
"perm =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
perm)
, TCMT IO Doc
"fperm =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Permutation -> [Char]
forall a. Show a => a -> [Char]
show Permutation
finalPerm)
, TCMT IO Doc
"withSub=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Substitution -> [Char]
forall a. Show a => a -> [Char]
show Substitution
withSub)
]
]
let reds :: SmallSet AllowedReduction
reds = [AllowedReduction] -> SmallSet AllowedReduction
forall a. SmallSetElement a => [a] -> SmallSet a
SmallSet.fromList [AllowedReduction
ProjectionReductions]
delta1 <- (SmallSet AllowedReduction -> SmallSet AllowedReduction)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
forall (m :: * -> *) a.
MonadTCEnv m =>
(SmallSet AllowedReduction -> SmallSet AllowedReduction)
-> m a -> m a
modifyAllowedReductions (SmallSet AllowedReduction
-> SmallSet AllowedReduction -> SmallSet AllowedReduction
forall a b. a -> b -> a
const SmallSet AllowedReduction
reds) (TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type)))
-> TCMT IO (Tele (Dom Type)) -> TCMT IO (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> TCMT IO (Tele (Dom Type))
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Tele (Dom Type)
delta1
(withFunType, n) <- do
let ps = Impossible -> Permutation -> Substitution' DeBruijnPattern
forall a.
DeBruijn a =>
Impossible -> Permutation -> Substitution' a
renaming Impossible
HasCallStack => Impossible
impossible (Permutation -> Permutation
reverseP Permutation
perm') Substitution' (SubstArg [NamedArg DeBruijnPattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` [NamedArg DeBruijnPattern]
qs
reportSDoc "tc.with.bndry" 40 $ addContext delta1 $ addContext delta2
$ text "ps =" <+> pretty ps
let vs = [NamedArg DeBruijnPattern] -> [Int]
forall p. IApplyVars p => p -> [Int]
iApplyVars [NamedArg DeBruijnPattern]
ps
bndry <- if null vs then return [] else do
iz <- primIZero
io <- primIOne
let tm = QName -> Elims -> Term
Def QName
f ([NamedArg DeBruijnPattern] -> Elims
patternsToElims [NamedArg DeBruijnPattern]
ps)
return [(i,(inplaceS i iz `applySubst` tm, inplaceS i io `applySubst` tm)) | i <- vs]
reportSDoc "tc.with.bndry" 40 $ addContext delta1 $ addContext delta2
$ text "bndry =" <+> pretty bndry
withFunctionType delta1 vtys delta2 b bndry
reportSDoc "tc.with.type" 10 $ sep [ "with-function type:", nest 2 $ prettyTCM withFunType ]
reportSDoc "tc.with.type" 50 $ sep [ "with-function type:", nest 2 $ pretty withFunType ]
call_in_parent <- do
(TelV tel _,bs) <- telViewUpToPathBoundaryP (n + size delta) withFunType
return $ argsS `applySubst` Def aux (teleElims tel bs)
reportSDoc "tc.with.top" 20 $ addContext delta $ "with function call" <+> prettyTCM call_in_parent
setCurrentRange cs $
traceCall NoHighlighting $
traceCall (CheckWithFunctionType withFunType) $
noConstraints $ checkType withFunType
df <- inTopContext $ makeOpen =<< withDisplayForm f aux delta1 delta2 n qs perm' perm
reportSLn "tc.with.top" 20 "created with display form"
case dget df of
Display Int
n Elims
ts DisplayTerm
dt ->
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.with.top" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Display" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (Elim -> TCMT IO Doc) -> Elims -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM Elims
ts
, DisplayTerm -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DisplayTerm -> m Doc
prettyTCM DisplayTerm
dt
]
addConstant aux =<< do
lang <- getLanguage
fun <- emptyFunction
useTerPragma $
(defaultDefn defaultArgInfo aux withFunType lang fun)
{ defDisplay = [df] }
reportSDoc "tc.with.top" 10 $ sep
[ "added with function" <+> (prettyTCM aux) <+> "of type"
, nest 2 $ prettyTCM withFunType
, nest 2 $ "-|" <+> (prettyTCM =<< getContextTelescope)
]
reportSDoc "tc.with.top" 70 $ vcat
[ nest 2 $ text $ "raw with func. type = " ++ show withFunType
]
cs <- return $ fmap (A.lhsToSpine) cs
cs <- buildWithFunction cxtNames f aux t delta qs npars withSub finalPerm (size delta1) n cs
cs <- return $ fmap (A.spineToLhs) cs
abstr <- defAbstract <$> ignoreAbstractMode (getConstInfo f)
let info = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
Info.mkDefInfo (Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
aux) Fixity'
noFixity' Access
PublicAccess IsAbstract
abstr (List1 (Clause' LHS) -> Range
forall a. HasRange a => a -> Range
getRange List1 (Clause' LHS)
cs)
ai <- defArgInfo <$> getConstInfo f
checkFunDefS withFunType ai Nothing (Just f) info aux (Just (withSub, lets)) $ List1.toList cs
return $ Just $ call_in_parent
checkWhere
:: A.WhereDeclarations
-> TCM a
-> TCM a
checkWhere :: forall a. WhereDeclarations -> TCM a -> TCM a
checkWhere wh :: WhereDeclarations
wh@(A.WhereDecls Maybe ModuleName
whmod Bool
whNamed Maybe Declaration
ds) TCM a
ret = do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
whNamed) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Maybe ModuleName -> TCM ()
forall {m :: * -> *}.
(MonadTrace m, HasOptions m, MonadDebug m, MonadError TCErr m) =>
Maybe ModuleName -> m ()
ensureNoNamedWhereInRefinedContext Maybe ModuleName
whmod
Maybe Declaration -> TCM a
loop Maybe Declaration
ds
where
loop :: Maybe Declaration -> TCM a
loop = \case
Maybe Declaration
Nothing -> TCM a
ret
Just (A.Section Range
_ Erased
e ModuleName
m GeneralizeTelescope
tel [Declaration]
ds) -> Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
forall a.
Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
newSection Erased
e ModuleName
m GeneralizeTelescope
tel (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
(TCEnv -> TCEnv) -> TCM a -> TCM a
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 { envCheckingWhere = True }) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
[Declaration] -> TCM ()
checkDecls [Declaration]
ds
TCM a
ret
Maybe Declaration
_ -> TCM a
forall a. HasCallStack => a
__IMPOSSIBLE__
ensureNoNamedWhereInRefinedContext :: Maybe ModuleName -> m ()
ensureNoNamedWhereInRefinedContext Maybe ModuleName
Nothing = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
ensureNoNamedWhereInRefinedContext (Just ModuleName
m) = Call -> m () -> m ()
forall a. Call -> m a -> m a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (ModuleName -> Call
CheckNamedWhere ModuleName
m) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
args <- (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term]) -> m [Arg Term] -> m [Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModuleName -> m [Arg Term]
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply (ModuleName -> m [Arg Term]) -> m ModuleName -> m [Arg Term]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
unless (isWeakening args) $ do
names <- map (argNameToString . fst . unDom) . telToList <$>
(lookupSection =<< currentModule)
typeError $ NamedWhereModuleInRefinedContext args names
where
isWeakening :: [Term] -> Bool
isWeakening [] = Bool
True
isWeakening (Var Int
i [] : [Term]
args) = Int -> [Term] -> Bool
isWk (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Term]
args
where
isWk :: Int -> [Term] -> Bool
isWk Int
i [] = Bool
True
isWk Int
i (Var Int
j [] : [Term]
args) = Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& Int -> [Term] -> Bool
isWk (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Term]
args
isWk Int
_ [Term]
_ = Bool
False
isWeakening [Term]
_ = Bool
False
newSection ::
Erased -> ModuleName -> A.GeneralizeTelescope -> TCM a -> TCM a
newSection :: forall a.
Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
newSection Erased
e ModuleName
m gtel :: GeneralizeTelescope
gtel@(A.GeneralizeTel Map QName Name
_ Telescope
tel) TCM a
cont = do
Erased -> TCM ()
warnForPlentyInHardCompileTimeMode Erased
e
Erased -> TCM a -> TCM a
forall a. Erased -> TCM a -> TCM a
setHardCompileTimeModeIfErased Erased
e (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.section" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"checking section" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Erased -> Doc -> Doc
C.prettyErased Erased
e (Doc -> Doc) -> TCMT IO Doc -> TCMT IO Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
[TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((TypedBinding -> TCMT IO Doc) -> Telescope -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map TypedBinding -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Telescope
tel)
Maybe ModuleName
-> GeneralizeTelescope
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a)
-> TCM a
forall a.
Maybe ModuleName
-> GeneralizeTelescope
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a)
-> TCM a
checkGeneralizeTelescope (ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just ModuleName
m) GeneralizeTelescope
gtel (([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a)
-> ([Maybe Name] -> Tele (Dom Type) -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ [Maybe Name]
_ Tele (Dom Type)
tel' -> do
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.section" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"adding section:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel'))
ModuleName -> TCM ()
addSection ModuleName
m
[Char] -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.section" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
4 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"actual tele:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Tele (Dom Type) -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Tele (Dom Type) -> m Doc
prettyTCM (Tele (Dom Type) -> TCMT IO Doc)
-> TCMT IO (Tele (Dom Type)) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ModuleName -> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection ModuleName
m
ModuleName -> TCM a -> TCM a
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule ModuleName
m TCM a
cont
atClause :: QName -> Int -> Type -> Maybe Substitution -> A.SpineClause -> TCM a -> TCM a
atClause :: forall a.
QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCM a
-> TCM a
atClause QName
name Int
i Type
t Maybe Substitution
sub SpineClause
cl TCM a
ret = do
clo <- () -> TCMT IO (Closure ())
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m) =>
a -> m (Closure a)
buildClosure ()
localTC (\ TCEnv
e -> TCEnv
e { envClause = IPClause name i t sub cl clo }) ret