{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Term where
import Prelude hiding ( null )
import Control.Monad ( (<=<), forM )
import Control.Monad.Except
import Control.Monad.Reader
import Data.Maybe
import Data.Either (partitionEithers, lefts)
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import Agda.Interaction.Options
import Agda.Interaction.Highlighting.Generate (disambiguateRecordFields)
import Agda.Syntax.Abstract (Binder, TypedBindingInfo (tbTacticAttr))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views as A
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Concrete (FieldAssignment'(..), nameFieldA)
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Scope.Base ( ThingsInScope, AbstractName
, emptyScopeInfo
, exportedNamesInScope)
import Agda.Syntax.Scope.Monad (getNamedScope)
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Generalize
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.IApplyConfluence
import Agda.TypeChecking.Level
import Agda.TypeChecking.Lock (requireGuarded)
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Quote
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.LHS
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Unquote
import Agda.TypeChecking.Warnings
import {-# SOURCE #-} Agda.TypeChecking.Empty ( ensureEmptyType )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Def (checkFunDef', useTerPragma)
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkSectionApplication)
import {-# SOURCE #-} Agda.TypeChecking.Rules.Application
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.Pretty ( prettyShow )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
isType :: A.Expr -> Sort -> TCM Type
isType :: Expr -> Sort' Term -> TCM Type
isType = Comparison -> Expr -> Sort' Term -> TCM Type
isType' Comparison
CmpLeq
isType' :: Comparison -> A.Expr -> Sort -> TCM Type
isType' :: Comparison -> Expr -> Sort' Term -> TCM Type
isType' Comparison
c Expr
e Sort' Term
s =
Call -> TCM Type -> TCM Type
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Sort' Term -> Call
IsTypeCall Comparison
c Expr
e Sort' Term
s) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ do
Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
c Expr
e (Sort' Term -> Type
sort Sort' Term
s)
Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s Term
v
isType_ :: A.Expr -> TCM Type
isType_ :: Expr -> TCM Type
isType_ Expr
e = Call -> TCM Type -> TCM Type
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
IsType_ Expr
e) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ do
ArgName -> Int -> (Type -> TCMT IO Doc) -> TCM Type -> TCM Type
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> (a -> TCMT IO Doc) -> m a -> m a
reportResult ArgName
"tc.term.istype" Int
15 (\Type
a -> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"isType_" 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
, 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
"returns" 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
a
]) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ do
let fallback :: TCM Type
fallback = Comparison -> Expr -> Sort' Term -> TCM Type
isType' Comparison
CmpEq Expr
e (Sort' Term -> TCM Type) -> TCMT IO (Sort' Term) -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do TCMT IO (Sort' Term) -> TCMT IO (Sort' Term)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCMT IO (Sort' Term) -> TCMT IO (Sort' Term))
-> TCMT IO (Sort' Term) -> TCMT IO (Sort' Term)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Sort' Term)
forall (m :: * -> *). MonadMetaSolver m => m (Sort' Term)
newSortMeta
SortKit{QName
IsFibrant -> QName
nameOfSet :: QName
nameOfProp :: QName
nameOfSSet :: QName
nameOfSetOmega :: IsFibrant -> QName
nameOfSet :: SortKit -> QName
nameOfProp :: SortKit -> QName
nameOfSSet :: SortKit -> QName
nameOfSetOmega :: SortKit -> IsFibrant -> QName
..} <- TCMT IO SortKit
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, HasOptions m) =>
m SortKit
sortKit
case Expr -> Expr
unScope Expr
e of
A.Fun ExprInfo
i (Arg ArgInfo
info Expr
t) Expr
b -> do
Dom Type
a <- ArgInfo -> Dom Type -> Dom Type
forall a. LensArgInfo a => ArgInfo -> a -> a
setArgInfo ArgInfo
info (Dom Type -> Dom Type) -> (Type -> Dom Type) -> Type -> Dom Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Dom Type
forall a. a -> Dom a
defaultDom (Type -> Dom Type) -> TCM Type -> TCMT IO (Dom Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> List1 ArgInfo -> Expr -> TCM Type
forall a.
(LensLock a, LensModality a) =>
List1 a -> Expr -> TCM Type
checkPiDomain (ArgInfo
info ArgInfo -> [ArgInfo] -> List1 ArgInfo
forall a. a -> [a] -> NonEmpty a
:| []) Expr
t
Type
b <- Expr -> TCM Type
isType_ Expr
b
Sort' Term
s <- Sort' Term -> Sort' Term -> TCMT IO (Sort' Term)
inferFunSort (Dom Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Dom Type
a) (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
b)
let t' :: Type
t' = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi Dom Type
a (Abs Type -> Term) -> Abs Type -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
NoAbs ArgName
forall a. Underscore a => a
underscore Type
b
Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t'
A.Pi ExprInfo
_ Telescope1
tel Expr
e -> do
(Type
t0, Type
t') <- Telescope -> (Telescope -> TCM (Type, Type)) -> TCM (Type, Type)
forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope (Telescope1 -> [Item Telescope1]
forall l. IsList l => l -> [Item l]
List1.toList Telescope1
tel) ((Telescope -> TCM (Type, Type)) -> TCM (Type, Type))
-> (Telescope -> TCM (Type, Type)) -> TCM (Type, Type)
forall a b. (a -> b) -> a -> b
$ \ Telescope
tel -> do
Type
t0 <- Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull (Type -> TCM Type) -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM Type
isType_ Expr
e
Telescope
tel <- Telescope -> TCMT IO Telescope
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Telescope
tel
(Type, Type) -> TCM (Type, Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t0, Telescope -> Type -> Type
telePi Telescope
tel Type
t0)
Type -> TCM ()
checkTelePiSort Type
t'
Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t'
A.Generalized Set QName
s Expr
e -> do
([Maybe QName]
_, Type
t') <- Set QName -> TCM Type -> TCM ([Maybe QName], Type)
generalizeType Set QName
s (TCM Type -> TCM ([Maybe QName], Type))
-> TCM Type -> TCM ([Maybe QName], Type)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
e
Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t'
A.Def' QName
x Suffix
suffix | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
nameOfSet -> case Suffix
suffix of
Suffix
NoSuffix -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkType Integer
0)
Suffix Integer
i -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkType Integer
i)
A.Def' QName
x Suffix
suffix | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
nameOfProp -> do
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
case Suffix
suffix of
Suffix
NoSuffix -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkProp Integer
0)
Suffix Integer
i -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkProp Integer
i)
A.Def' QName
x Suffix
suffix | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
nameOfSSet -> do
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel
case Suffix
suffix of
Suffix
NoSuffix -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkSSet Integer
0)
Suffix Integer
i -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (Integer -> Sort' Term
mkSSet Integer
i)
A.Def' QName
x Suffix
suffix | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant -> QName
nameOfSetOmega IsFibrant
IsFibrant -> case Suffix
suffix of
Suffix
NoSuffix -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (IsFibrant -> Integer -> Sort' Term
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
0)
Suffix Integer
i -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (IsFibrant -> Integer -> Sort' Term
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
i)
A.Def' QName
x Suffix
suffix | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== IsFibrant -> QName
nameOfSetOmega IsFibrant
IsStrict -> do
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel
case Suffix
suffix of
Suffix
NoSuffix -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (IsFibrant -> Integer -> Sort' Term
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsStrict Integer
0)
Suffix Integer
i -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Type
sort (IsFibrant -> Integer -> Sort' Term
forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsStrict Integer
i)
A.App AppInfo
i Expr
s NamedArg Expr
arg
| NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg,
A.Def QName
x <- Expr -> Expr
unScope Expr
s,
QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
nameOfSet -> do
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError
ArgName
"Use --universe-polymorphism to enable level arguments to Set"
Relevance -> TCM Type -> TCM Type
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
Sort' Term -> Type
sort (Sort' Term -> Type)
-> (Level' Term -> Sort' Term) -> Level' Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
Type (Level' Term -> Type) -> TCMT IO (Level' Term) -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg Expr -> TCMT IO (Level' Term)
checkLevel NamedArg Expr
arg
A.App AppInfo
i Expr
s NamedArg Expr
arg
| NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg,
A.Def QName
x <- Expr -> Expr
unScope Expr
s,
QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
nameOfProp -> do
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isPropEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionProp
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError
ArgName
"Use --universe-polymorphism to enable level arguments to Prop"
Relevance -> TCM Type -> TCM Type
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
Sort' Term -> Type
sort (Sort' Term -> Type)
-> (Level' Term -> Sort' Term) -> Level' Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
Prop (Level' Term -> Type) -> TCMT IO (Level' Term) -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg Expr -> TCMT IO (Level' Term)
checkLevel NamedArg Expr
arg
A.App AppInfo
i Expr
s NamedArg Expr
arg
| NamedArg Expr -> Bool
forall a. LensHiding a => a -> Bool
visible NamedArg Expr
arg,
A.Def QName
x <- Expr -> Expr
unScope Expr
s,
QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
nameOfSSet -> do
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
isTwoLevelEnabled (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
NeedOptionTwoLevel
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
hasUniversePolymorphism (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError
ArgName
"Use --universe-polymorphism to enable level arguments to SSet"
Relevance -> TCM Type -> TCM Type
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
NonStrict (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
Sort' Term -> Type
sort (Sort' Term -> Type)
-> (Level' Term -> Sort' Term) -> Level' Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Level' Term -> Sort' Term
forall t. Level' t -> Sort' t
SSet (Level' Term -> Type) -> TCMT IO (Level' Term) -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg Expr -> TCMT IO (Level' Term)
checkLevel NamedArg Expr
arg
A.QuestionMark MetaInfo
minfo InteractionId
ii -> TCMT IO (Maybe MetaId)
-> TCM Type -> (MetaId -> TCM Type) -> TCM Type
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (InteractionId -> TCMT IO (Maybe MetaId)
forall (m :: * -> *).
ReadTCState m =>
InteractionId -> m (Maybe MetaId)
lookupInteractionMeta InteractionId
ii) TCM Type
fallback ((MetaId -> TCM Type) -> TCM Type)
-> (MetaId -> TCM Type) -> TCM Type
forall a b. (a -> b) -> a -> b
$ \ MetaId
x -> do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip" 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
fsep
[ TCMT IO Doc
"Rechecking meta "
, MetaId -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => MetaId -> m Doc
prettyTCM MetaId
x
, ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
" for interaction point " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ InteractionId -> ArgName
forall a. Show a => a -> ArgName
show InteractionId
ii
]
MetaVariable
mv <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
x
let s0 :: Type
s0 = Judgement MetaId -> Type
forall a. Judgement a -> Type
jMetaType (Judgement MetaId -> Type)
-> (MetaVariable -> Judgement MetaId) -> MetaVariable -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> Judgement MetaId
mvJudgement (MetaVariable -> Type) -> MetaVariable -> Type
forall a b. (a -> b) -> a -> b
$ MetaVariable
mv
let n :: Int
n = [ContextEntry] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([ContextEntry] -> Int)
-> (MetaVariable -> [ContextEntry]) -> MetaVariable -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [ContextEntry]
envContext (TCEnv -> [ContextEntry])
-> (MetaVariable -> TCEnv) -> MetaVariable -> [ContextEntry]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Range -> TCEnv
forall a. Closure a -> TCEnv
clEnv (Closure Range -> TCEnv)
-> (MetaVariable -> Closure Range) -> MetaVariable -> TCEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInfo -> Closure Range
miClosRange (MetaInfo -> Closure Range)
-> (MetaVariable -> MetaInfo) -> MetaVariable -> Closure Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaVariable -> MetaInfo
mvInfo (MetaVariable -> Int) -> MetaVariable -> Int
forall a b. (a -> b) -> a -> b
$ MetaVariable
mv
([Arg Term]
vs, [Arg Term]
rest) <- Int -> [Arg Term] -> ([Arg Term], [Arg Term])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n ([Arg Term] -> ([Arg Term], [Arg Term]))
-> TCMT IO [Arg Term] -> TCMT IO ([Arg Term], [Arg Term])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [Arg Term]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip" 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
" s0 = " 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
s0
, TCMT IO Doc
" vs = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
vs
, TCMT IO Doc
" rest = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Arg Term] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Arg Term] -> m Doc
prettyTCM [Arg Term]
rest
]
if ([Arg Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
n) then TCM Type
fallback else do
Type
s1 <- Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCM Type) -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> [Arg Term] -> TCM Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type -> a -> m Type
forall (m :: * -> *).
(MonadReduce m, HasBuiltins m) =>
Type -> [Arg Term] -> m Type
piApplyM Type
s0 [Arg Term]
vs
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip" 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
" s1 = " 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
s1
]
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.ip" 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
vcat
[ TCMT IO Doc
" s1 = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Type -> ArgName
forall a. Show a => a -> ArgName
show Type
s1)
]
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
s1 of
Sort Sort' Term
s -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
vs
Term
_ -> TCM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
Expr
_ -> TCM Type
fallback
checkLevel :: NamedArg A.Expr -> TCM Level
checkLevel :: NamedArg Expr -> TCMT IO (Level' Term)
checkLevel NamedArg Expr
arg = do
Type
lvl <- TCM Type
forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
levelType
Term -> TCMT IO (Level' Term)
forall (m :: * -> *). PureTCM m => Term -> m (Level' Term)
levelView (Term -> TCMT IO (Level' Term))
-> TCM Term -> TCMT IO (Level' Term)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< NamedArg Expr -> Type -> TCM Term
checkNamedArg NamedArg Expr
arg Type
lvl
isTypeEqualTo :: A.Expr -> Type -> TCM Type
isTypeEqualTo :: Expr -> Type -> TCM Type
isTypeEqualTo Expr
e0 Type
t = Expr -> TCM Expr
scopedExpr Expr
e0 TCM Expr -> (Expr -> TCM Type) -> TCM Type
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
A.ScopedExpr{} -> TCM Type
forall a. HasCallStack => a
__IMPOSSIBLE__
A.Underscore MetaInfo
i | Maybe MetaId -> Bool
forall a. Maybe a -> Bool
isNothing (MetaInfo -> Maybe MetaId
A.metaNumber MetaInfo
i) -> Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
Expr
e -> TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ do
Type
t' <- Expr -> Sort' Term -> TCM Type
isType Expr
e (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
t)
Type
t' Type -> TCM () -> TCM Type
forall a b. a -> TCMT IO b -> TCMT IO a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
t Type
t'
leqType_ :: Type -> Type -> TCM ()
leqType_ :: Type -> Type -> TCM ()
leqType_ Type
t Type
t' = TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
t Type
t'
checkGeneralizeTelescope :: A.GeneralizeTelescope -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
checkGeneralizeTelescope :: forall a.
GeneralizeTelescope
-> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
checkGeneralizeTelescope (A.GeneralizeTel Map QName Name
vars Telescope
tel) [Maybe Name] -> Telescope -> TCM a
k =
Map QName Name
-> (forall a1. (Telescope -> TCM a1) -> TCM a1)
-> ([Maybe Name] -> Telescope -> TCM a)
-> TCM a
forall a.
Map QName Name
-> (forall a1. (Telescope -> TCM a1) -> TCM a1)
-> ([Maybe Name] -> Telescope -> TCM a)
-> TCM a
generalizeTelescope Map QName Name
vars (Telescope -> (Telescope -> TCM a1) -> TCM a1
forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope Telescope
tel) [Maybe Name] -> Telescope -> TCM a
k
checkTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope :: forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope = LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
LamNotPi
checkPiTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope :: forall a. Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope = LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
PiNotLam
data LamOrPi
= LamNotPi
| PiNotLam
deriving (LamOrPi -> LamOrPi -> Bool
(LamOrPi -> LamOrPi -> Bool)
-> (LamOrPi -> LamOrPi -> Bool) -> Eq LamOrPi
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LamOrPi -> LamOrPi -> Bool
== :: LamOrPi -> LamOrPi -> Bool
$c/= :: LamOrPi -> LamOrPi -> Bool
/= :: LamOrPi -> LamOrPi -> Bool
Eq, Int -> LamOrPi -> ArgName -> ArgName
[LamOrPi] -> ArgName -> ArgName
LamOrPi -> ArgName
(Int -> LamOrPi -> ArgName -> ArgName)
-> (LamOrPi -> ArgName)
-> ([LamOrPi] -> ArgName -> ArgName)
-> Show LamOrPi
forall a.
(Int -> a -> ArgName -> ArgName)
-> (a -> ArgName) -> ([a] -> ArgName -> ArgName) -> Show a
$cshowsPrec :: Int -> LamOrPi -> ArgName -> ArgName
showsPrec :: Int -> LamOrPi -> ArgName -> ArgName
$cshow :: LamOrPi -> ArgName
show :: LamOrPi -> ArgName
$cshowList :: [LamOrPi] -> ArgName -> ArgName
showList :: [LamOrPi] -> ArgName -> ArgName
Show)
checkTelescope' :: LamOrPi -> A.Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' :: forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
lamOrPi [] Telescope -> TCM a
ret = Telescope -> TCM a
ret Telescope
forall a. Tele a
EmptyTel
checkTelescope' LamOrPi
lamOrPi (TypedBinding
b : Telescope
tel) Telescope -> TCM a
ret =
LamOrPi -> TypedBinding -> (Telescope -> TCM a) -> TCM a
forall a. LamOrPi -> TypedBinding -> (Telescope -> TCM a) -> TCM a
checkTypedBindings LamOrPi
lamOrPi TypedBinding
b ((Telescope -> TCM a) -> TCM a) -> (Telescope -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Telescope
tel1 ->
LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
forall a. LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' LamOrPi
lamOrPi Telescope
tel ((Telescope -> TCM a) -> TCM a) -> (Telescope -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \Telescope
tel2 ->
Telescope -> TCM a
ret (Telescope -> TCM a) -> Telescope -> TCM a
forall a b. (a -> b) -> a -> b
$ Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
abstract Telescope
tel1 Telescope
tel2
checkDomain :: (LensLock a, LensModality a) => LamOrPi -> List1 a -> A.Expr -> TCM Type
checkDomain :: forall a.
(LensLock a, LensModality a) =>
LamOrPi -> List1 a -> Expr -> TCM Type
checkDomain LamOrPi
lamOrPi List1 a
xs Expr
e = do
let (Cohesion
c :| [Cohesion]
cs) = (a -> Cohesion) -> List1 a -> NonEmpty Cohesion
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion (Modality -> Cohesion) -> (a -> Modality) -> a -> Cohesion
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Modality
forall a. LensModality a => a -> Modality
getModality) List1 a
xs
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Cohesion -> Bool) -> [Cohesion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Cohesion
c Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
==) [Cohesion]
cs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
let (Quantity
q :| [Quantity]
qs) = (a -> Quantity) -> List1 a -> NonEmpty Quantity
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Modality -> Quantity) -> (a -> Modality) -> a -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Modality
forall a. LensModality a => a -> Modality
getModality) List1 a
xs
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Quantity -> Bool) -> [Quantity] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Quantity
q Quantity -> Quantity -> Bool
forall a. Eq a => a -> a -> Bool
==) [Quantity]
qs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Type
t <- Quantity -> TCM Type -> TCM Type
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext Quantity
q (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
Cohesion -> TCM Type -> TCM Type
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensCohesion m) =>
m -> tcm a -> tcm a
applyCohesionToContext Cohesion
c (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
LamOrPi -> TCM Type -> TCM Type
forall {m :: * -> *} {a}.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
LamOrPi -> m a -> m a
modEnv LamOrPi
lamOrPi (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
e
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((a -> Bool) -> List1 a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ a
x -> a -> Lock
forall a. LensLock a => a -> Lock
getLock a
x Lock -> Lock -> Bool
forall a. Eq a => a -> a -> Bool
== Lock
IsLock) List1 a
xs) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
ArgName -> TCM ()
requireGuarded ArgName
"which is needed for @tick/@lock attributes."
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Maybe QName -> Bool
forall a. Maybe a -> Bool
isJust (Maybe QName -> Bool) -> TCMT IO (Maybe QName) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ArgName -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe QName)
getName' ArgName
builtinLockUniv) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
Doc -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Doc
"Missing binding for primLockUniv primitive."
Sort' Term -> Sort' Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Sort' Term -> Sort' Term -> m ()
equalSort (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
t) Sort' Term
forall t. Sort' t
LockUniv
Type -> TCM Type
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
where
modEnv :: LamOrPi -> m a -> m a
modEnv LamOrPi
LamNotPi = m a -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes
modEnv LamOrPi
_ = m a -> m a
forall a. a -> a
id
checkPiDomain :: (LensLock a, LensModality a) => List1 a -> A.Expr -> TCM Type
checkPiDomain :: forall a.
(LensLock a, LensModality a) =>
List1 a -> Expr -> TCM Type
checkPiDomain = LamOrPi -> List1 a -> Expr -> TCM Type
forall a.
(LensLock a, LensModality a) =>
LamOrPi -> List1 a -> Expr -> TCM Type
checkDomain LamOrPi
PiNotLam
checkTypedBindings :: LamOrPi -> A.TypedBinding -> (Telescope -> TCM a) -> TCM a
checkTypedBindings :: forall a. LamOrPi -> TypedBinding -> (Telescope -> TCM a) -> TCM a
checkTypedBindings LamOrPi
lamOrPi (A.TBind Range
r TypedBindingInfo
tac List1 (NamedArg (Binder' BindName))
xps Expr
e) Telescope -> TCM a
ret = do
let xs :: NonEmpty (NamedArg Name)
xs = (NamedArg (Binder' BindName) -> NamedArg Name)
-> List1 (NamedArg (Binder' BindName)) -> NonEmpty (NamedArg Name)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Binder' BindName -> Name)
-> NamedArg (Binder' BindName) -> NamedArg Name
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg ((Binder' BindName -> Name)
-> NamedArg (Binder' BindName) -> NamedArg Name)
-> (Binder' BindName -> Name)
-> NamedArg (Binder' BindName)
-> NamedArg Name
forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind (BindName -> Name)
-> (Binder' BindName -> BindName) -> Binder' BindName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder' BindName -> BindName
forall a. Binder' a -> a
A.binderName) List1 (NamedArg (Binder' BindName))
xps
Maybe Term
tac <- (Expr -> TCM Term) -> Maybe Expr -> TCMT IO (Maybe Term)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (LamOrPi -> Expr -> TCM Term
checkTacticAttribute LamOrPi
lamOrPi) (TypedBindingInfo -> Maybe Expr
tbTacticAttr TypedBindingInfo
tac)
Maybe Term -> (Term -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Term
tac ((Term -> TCM ()) -> TCM ()) -> (Term -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ Term
t -> ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.tactic" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Checked tactic attribute:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t
Bool
experimental <- PragmaOptions -> Bool
optExperimentalIrrelevance (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
Type
t <- LamOrPi -> List1 (NamedArg (Binder' BindName)) -> Expr -> TCM Type
forall a.
(LensLock a, LensModality a) =>
LamOrPi -> List1 a -> Expr -> TCM Type
checkDomain LamOrPi
lamOrPi List1 (NamedArg (Binder' BindName))
xps Expr
e
[NamedArg (Binder' BindName)]
-> (List1 (NamedArg (Binder' BindName)) -> TCM ()) -> TCM ()
forall m a. Null m => [a] -> (List1 a -> m) -> m
List1.unlessNull ((NamedArg (Binder' BindName) -> Bool)
-> List1 (NamedArg (Binder' BindName))
-> [NamedArg (Binder' BindName)]
forall a. (a -> Bool) -> NonEmpty a -> [a]
List1.filter NamedArg (Binder' BindName) -> Bool
forall a. LensHiding a => a -> Bool
isInstance List1 (NamedArg (Binder' BindName))
xps) ((List1 (NamedArg (Binder' BindName)) -> TCM ()) -> TCM ())
-> (List1 (NamedArg (Binder' BindName)) -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ List1 (NamedArg (Binder' BindName))
ixs -> do
(Telescope
tel, OutputTypeName
target) <- Type -> TCM (Telescope, OutputTypeName)
getOutputTypeName Type
t
case OutputTypeName
target of
OutputTypeName{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
OutputTypeVar{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
OutputTypeVisiblePi{} -> Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> (Doc -> Warning) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Warning
InstanceArgWithExplicitArg (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypedBinding -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypedBinding -> m Doc
prettyTCM (Range
-> List1 (NamedArg (Binder' BindName)) -> Expr -> TypedBinding
A.mkTBind Range
r List1 (NamedArg (Binder' BindName))
ixs Expr
e)
OutputTypeNameNotYetKnown{} -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
OutputTypeName
NoOutputTypeName -> Warning -> TCM ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning (Warning -> TCM ()) -> (Doc -> Warning) -> Doc -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Warning
InstanceNoOutputTypeName (Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TypedBinding -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypedBinding -> m Doc
prettyTCM (Range
-> List1 (NamedArg (Binder' BindName)) -> Expr -> TypedBinding
A.mkTBind Range
r List1 (NamedArg (Binder' BindName))
ixs Expr
e)
let setTac :: Maybe t -> Tele (Dom' t e) -> Tele (Dom' t e)
setTac Maybe t
tac Tele (Dom' t e)
EmptyTel = Tele (Dom' t e)
forall a. Tele a
EmptyTel
setTac Maybe t
tac (ExtendTel Dom' t e
dom Abs (Tele (Dom' t e))
tel) = Dom' t e -> Abs (Tele (Dom' t e)) -> Tele (Dom' t e)
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' t e
dom{ domTactic :: Maybe t
domTactic = Maybe t
tac } (Abs (Tele (Dom' t e)) -> Tele (Dom' t e))
-> Abs (Tele (Dom' t e)) -> Tele (Dom' t e)
forall a b. (a -> b) -> a -> b
$ Maybe t -> Tele (Dom' t e) -> Tele (Dom' t e)
setTac (Int -> Maybe t -> Maybe t
forall a. Subst a => Int -> a -> a
raise Int
1 Maybe t
tac) (Tele (Dom' t e) -> Tele (Dom' t e))
-> Abs (Tele (Dom' t e)) -> Abs (Tele (Dom' t e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (Tele (Dom' t e))
tel
xs' :: NonEmpty (NamedArg Name)
xs' = (NamedArg Name -> NamedArg Name)
-> NonEmpty (NamedArg Name) -> NonEmpty (NamedArg Name)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LamOrPi -> Bool -> NamedArg Name -> NamedArg Name
forall {a}. LensRelevance a => LamOrPi -> Bool -> a -> a
modMod LamOrPi
lamOrPi Bool
experimental) NonEmpty (NamedArg Name)
xs
let tel :: Telescope
tel = Maybe Term -> Telescope -> Telescope
forall {t} {t} {e}.
Subst t =>
Maybe t -> Tele (Dom' t e) -> Tele (Dom' t e)
setTac Maybe Term
tac (Telescope -> Telescope) -> Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$ NonEmpty (NamedArg Name) -> Type -> Telescope
namedBindsToTel1 NonEmpty (NamedArg Name)
xs Type
t
(NonEmpty (NamedArg Name), Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(NonEmpty (NamedArg Name), Type) -> m a -> m a
addContext (NonEmpty (NamedArg Name)
xs', Type
t) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ List1 (NamedArg (Binder' BindName)) -> TCM a -> TCM a
forall a. List1 (NamedArg (Binder' BindName)) -> TCM a -> TCM a
addTypedPatterns List1 (NamedArg (Binder' BindName))
xps (Telescope -> TCM a
ret Telescope
tel)
where
modEnv :: LamOrPi -> m a -> m a
modEnv LamOrPi
LamNotPi = m a -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes
modEnv LamOrPi
_ = m a -> m a
forall a. a -> a
id
modMod :: LamOrPi -> Bool -> a -> a
modMod LamOrPi
PiNotLam Bool
xp = (if Bool
xp then (Relevance -> Relevance) -> a -> a
forall a. LensRelevance a => (Relevance -> Relevance) -> a -> a
mapRelevance Relevance -> Relevance
irrToNonStrict else a -> a
forall a. a -> a
id)
modMod LamOrPi
_ Bool
_ = a -> a
forall a. a -> a
id
checkTypedBindings LamOrPi
lamOrPi (A.TLet Range
_ List1 LetBinding
lbs) Telescope -> TCM a
ret = do
List1 LetBinding -> TCM a -> TCM a
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings List1 LetBinding
lbs (Telescope -> TCM a
ret Telescope
forall a. Tele a
EmptyTel)
addTypedPatterns :: List1 (NamedArg A.Binder) -> TCM a -> TCM a
addTypedPatterns :: forall a. List1 (NamedArg (Binder' BindName)) -> TCM a -> TCM a
addTypedPatterns List1 (NamedArg (Binder' BindName))
xps TCM a
ret = do
let ps :: [(Pattern, BindName)]
ps = (NamedArg (Binder' BindName) -> Maybe (Pattern, BindName))
-> List1 (NamedArg (Binder' BindName)) -> [(Pattern, BindName)]
forall a b. (a -> Maybe b) -> List1 a -> [b]
List1.mapMaybe (Binder' BindName -> Maybe (Pattern, BindName)
forall a. Binder' a -> Maybe (Pattern, a)
A.extractPattern (Binder' BindName -> Maybe (Pattern, BindName))
-> (NamedArg (Binder' BindName) -> Binder' BindName)
-> NamedArg (Binder' BindName)
-> Maybe (Pattern, BindName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Binder' BindName) -> Binder' BindName
forall a. NamedArg a -> a
namedArg) List1 (NamedArg (Binder' BindName))
xps
let lbs :: [LetBinding]
lbs = ((Pattern, BindName) -> LetBinding)
-> [(Pattern, BindName)] -> [LetBinding]
forall a b. (a -> b) -> [a] -> [b]
map (Pattern, BindName) -> LetBinding
letBinding [(Pattern, BindName)]
ps
[LetBinding] -> TCM a -> TCM a
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings [LetBinding]
lbs TCM a
ret
where
letBinding :: (A.Pattern, A.BindName) -> A.LetBinding
letBinding :: (Pattern, BindName) -> LetBinding
letBinding (Pattern
p, BindName
n) = LetInfo -> Pattern -> Expr -> LetBinding
A.LetPatBind (Range -> LetInfo
A.LetRange Range
r) Pattern
p (Name -> Expr
A.Var (Name -> Expr) -> Name -> Expr
forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind BindName
n)
where r :: Range
r = Pattern -> BindName -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Pattern
p BindName
n
checkTacticAttribute :: LamOrPi -> A.Expr -> TCM Term
checkTacticAttribute :: LamOrPi -> Expr -> TCM Term
checkTacticAttribute LamOrPi
LamNotPi Expr
e = Doc -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCM Term) -> TCMT IO Doc -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Doc
"The @tactic attribute is not allowed here"
checkTacticAttribute LamOrPi
PiNotLam Expr
e = do
Type
expectedType <- TCM Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
Expr -> Type -> TCM Term
checkExpr Expr
e Type
expectedType
checkPath :: A.TypedBinding -> A.Expr -> Type -> TCM Term
checkPath :: TypedBinding -> Expr -> Type -> TCM Term
checkPath b :: TypedBinding
b@(A.TBind Range
_r TypedBindingInfo
_tac (NamedArg (Binder' BindName)
xp :| []) Expr
typ) Expr
body Type
ty = do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" 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
hsep [ TCMT IO Doc
"checking path lambda", NamedArg (Binder' BindName) -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg (Binder' BindName)
xp ]
case (Binder' BindName -> Maybe (Pattern, BindName)
forall a. Binder' a -> Maybe (Pattern, a)
A.extractPattern (Binder' BindName -> Maybe (Pattern, BindName))
-> Binder' BindName -> Maybe (Pattern, BindName)
forall a b. (a -> b) -> a -> b
$ NamedArg (Binder' BindName) -> Binder' BindName
forall a. NamedArg a -> a
namedArg NamedArg (Binder' BindName)
xp) of
Just{} -> NamedArg (Binder' BindName) -> TCM Term -> TCM Term
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg (Binder' BindName)
xp (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError (ArgName -> TCM Term) -> ArgName -> TCM Term
forall a b. (a -> b) -> a -> b
$ ArgName
"Patterns are not allowed in Path-lambdas"
Maybe (Pattern, BindName)
Nothing -> do
let x :: NamedArg Name
x = (Binder' BindName -> Name)
-> NamedArg (Binder' BindName) -> NamedArg Name
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (BindName -> Name
A.unBind (BindName -> Name)
-> (Binder' BindName -> BindName) -> Binder' BindName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder' BindName -> BindName
forall a. Binder' a -> a
A.binderName) NamedArg (Binder' BindName)
xp
info :: ArgInfo
info = NamedArg Name -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Name
x
PathType Sort' Term
s QName
path Arg Term
level Arg Term
typ Arg Term
lhs Arg Term
rhs <- Type -> TCMT IO PathView
forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView Type
ty
Type
interval <- TCM Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType
Term
v <- ([NamedArg Name], Type) -> TCM Term -> TCM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
([NamedArg Name], Type) -> m a -> m a
addContext ([NamedArg Name
x], Type
interval) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
Expr -> Type -> TCM Term
checkExpr Expr
body (Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort' Term -> Sort' Term
forall a. Subst a => Int -> a -> a
raise Int
1 Sort' Term
s) (Int -> Term -> Term
forall a. Subst a => Int -> a -> a
raise Int
1 (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
typ) Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
0]))
Term
iZero <- TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
Term
iOne <- TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
let lhs' :: Term
lhs' = Int -> SubstArg Term -> Term -> Term
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
SubstArg Term
iZero Term
v
rhs' :: Term
rhs' = Int -> SubstArg Term -> Term -> Term
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
SubstArg Term
iOne Term
v
let t :: Term
t = ArgInfo -> Abs Term -> Term
Lam ArgInfo
info (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs (NamedArg Name -> ArgName
namedArgName NamedArg Name
x) Term
v
let btyp :: Term -> Type
btyp Term
i = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
typ Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall e. e -> Arg e
argN Term
i])
Lens' Range TCEnv -> (Range -> Range) -> TCM Term -> TCM Term
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC (Range -> f Range) -> TCEnv -> f TCEnv
Lens' Range TCEnv
eRange (Range -> Range -> Range
forall a b. a -> b -> a
const Range
forall a. Range' a
noRange) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TCM Term -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Int m,
MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
ty (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Term -> TCM Term
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Expr
body (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm (Term -> Type
btyp Term
iZero) Term
lhs' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
lhs)
Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm (Term -> Type
btyp Term
iOne) Term
rhs' (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
rhs)
Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
checkPath TypedBinding
b Expr
body Type
ty = TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
checkLambda :: Comparison -> A.TypedBinding -> A.Expr -> Type -> TCM Term
checkLambda :: Comparison -> TypedBinding -> Expr -> Type -> TCM Term
checkLambda Comparison
cmp (A.TLet Range
_ List1 LetBinding
lbs) Expr
body Type
target =
List1 LetBinding -> TCM Term -> TCM Term
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings List1 LetBinding
lbs (Expr -> Type -> TCM Term
checkExpr Expr
body Type
target)
checkLambda Comparison
cmp b :: TypedBinding
b@(A.TBind Range
r TypedBindingInfo
tac List1 (NamedArg (Binder' BindName))
xps0 Expr
typ) Expr
body Type
target = do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" 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
"checkLambda before insertion xs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> List1 (NamedArg (Binder' BindName)) -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg (Binder' BindName))
xps0
]
List1 (NamedArg (Binder' BindName))
xps <- List1 (NamedArg (Binder' BindName))
-> Type -> TCMT IO (List1 (NamedArg (Binder' BindName)))
forall (m :: * -> *).
(PureTCM m, MonadError TCErr m, MonadFresh NameId m,
MonadTrace m) =>
List1 (NamedArg (Binder' BindName))
-> Type -> m (List1 (NamedArg (Binder' BindName)))
insertImplicitBindersT1 List1 (NamedArg (Binder' BindName))
xps0 Type
target
Comparison
-> TypedBinding
-> List1 (NamedArg (Binder' BindName))
-> Expr
-> Expr
-> Type
-> TCM Term
checkLambda' Comparison
cmp (Range
-> TypedBindingInfo
-> List1 (NamedArg (Binder' BindName))
-> Expr
-> TypedBinding
A.TBind Range
r TypedBindingInfo
tac List1 (NamedArg (Binder' BindName))
xps Expr
typ) List1 (NamedArg (Binder' BindName))
xps Expr
typ Expr
body Type
target
checkLambda'
:: Comparison
-> A.TypedBinding
-> List1 (NamedArg Binder)
-> A.Expr
-> A.Expr
-> Type
-> TCM Term
checkLambda' :: Comparison
-> TypedBinding
-> List1 (NamedArg (Binder' BindName))
-> Expr
-> Expr
-> Type
-> TCM Term
checkLambda' Comparison
cmp TypedBinding
b List1 (NamedArg (Binder' BindName))
xps Expr
typ Expr
body Type
target = do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" 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
"checkLambda xs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> List1 (NamedArg (Binder' BindName)) -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA List1 (NamedArg (Binder' BindName))
xps
, TCMT IO Doc
"possiblePath =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Bool -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Bool -> m Doc
prettyTCM Bool
possiblePath
, TCMT IO Doc
"numbinds =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
numbinds
, TCMT IO Doc
"typ =" 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 :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> Expr
unScope Expr
typ)
]
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
60 (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
"info =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (ArgInfo -> ArgName) -> ArgInfo -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgInfo -> ArgName
forall a. Show a => a -> ArgName
show) ArgInfo
info
]
TelV Telescope
tel Type
btyp <- Int -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m (TelV Type)
telViewUpTo Int
numbinds Type
target
if Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
numbinds Bool -> Bool -> Bool
|| Int
numbinds Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1
then (if Bool
possiblePath then TCM Term
trySeeingIfPath else TCM Term
dontUseTargetType)
else Telescope -> Type -> TCM Term
useTargetType Telescope
tel Type
btyp
where
xs :: NonEmpty (NamedArg Name)
xs = (NamedArg (Binder' BindName) -> NamedArg Name)
-> List1 (NamedArg (Binder' BindName)) -> NonEmpty (NamedArg Name)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Binder' BindName -> Name)
-> NamedArg (Binder' BindName) -> NamedArg Name
forall a b. (a -> b) -> NamedArg a -> NamedArg b
updateNamedArg (BindName -> Name
A.unBind (BindName -> Name)
-> (Binder' BindName -> BindName) -> Binder' BindName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder' BindName -> BindName
forall a. Binder' a -> a
A.binderName)) List1 (NamedArg (Binder' BindName))
xps
numbinds :: Int
numbinds = List1 (NamedArg (Binder' BindName)) -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 (NamedArg (Binder' BindName))
xps
isUnderscore :: Expr -> Bool
isUnderscore = \case { A.Underscore{} -> Bool
True; Expr
_ -> Bool
False }
possiblePath :: Bool
possiblePath = Int
numbinds Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Expr -> Bool
isUnderscore (Expr -> Expr
unScope Expr
typ)
Bool -> Bool -> Bool
&& ArgInfo -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant ArgInfo
info Bool -> Bool -> Bool
&& ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
info
info :: ArgInfo
info = NamedArg Name -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo (NamedArg Name -> ArgInfo) -> NamedArg Name -> ArgInfo
forall a b. (a -> b) -> a -> b
$ NonEmpty (NamedArg Name) -> NamedArg Name
forall a. NonEmpty a -> a
List1.head NonEmpty (NamedArg Name)
xs
trySeeingIfPath :: TCM Term
trySeeingIfPath = do
Bool
cubical <- Maybe Cubical -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Cubical -> Bool)
-> (PragmaOptions -> Maybe Cubical) -> PragmaOptions -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PragmaOptions -> Maybe Cubical
optCubical (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.term.lambda" Int
60 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"trySeeingIfPath for " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ List1 (NamedArg (Binder' BindName)) -> ArgName
forall a. Show a => a -> ArgName
show List1 (NamedArg (Binder' BindName))
xps
let postpone' :: Blocker -> Type -> TCM Term
postpone' = if Bool
cubical then Blocker -> Type -> TCM Term
postpone else \ Blocker
_ Type
_ -> TCM Term
dontUseTargetType
Type
-> (Blocker -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
target Blocker -> Type -> TCM Term
postpone' ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
TCMT IO Bool -> TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PathView -> Bool
isPathType (PathView -> Bool) -> TCMT IO PathView -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO PathView
forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView Type
t) TCM Term
dontUseTargetType (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ if Bool
cubical
then TypedBinding -> Expr -> Type -> TCM Term
checkPath TypedBinding
b Expr
body Type
t
else ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError (ArgName -> TCM Term) -> ArgName -> TCM Term
forall a b. (a -> b) -> a -> b
$ [ArgName] -> ArgName
unwords
[ ArgName
"Option --cubical/--erased-cubical needed to build"
, ArgName
"a path with a lambda abstraction"
]
postpone :: Blocker -> Type -> TCM Term
postpone Blocker
blocker Type
tgt = (TypeCheckingProblem -> Blocker -> TCM Term)
-> Blocker -> TypeCheckingProblem -> TCM Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem Blocker
blocker (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$
Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp (ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
A.exprNoRange (TypedBinding -> LamBinding
A.DomainFull TypedBinding
b) Expr
body) Type
tgt
dontUseTargetType :: TCM Term
dontUseTargetType = do
ArgName -> Int -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> m () -> m ()
verboseS ArgName
"tc.term.lambda" Int
5 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM ()
forall (m :: * -> *). MonadStatistics m => ArgName -> m ()
tick ArgName
"lambda-no-target-type"
Type
argsT <- TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
typ
let tel :: Telescope
tel = NonEmpty (NamedArg Name) -> Type -> Telescope
namedBindsToTel1 NonEmpty (NamedArg Name)
xs Type
argsT
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.lambda" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"dontUseTargetType tel =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Telescope
tel
Term -> TCM ()
checkSizeLtSat (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
argsT
let postponeOnBlockedPattern :: TCM (Type, Term) -> TCM (Type, Term)
postponeOnBlockedPattern TCM (Type, Term)
m = TCM (Type, Term)
m TCM (Type, Term)
-> ((TCErr, Blocker) -> TCM (Type, Term)) -> TCM (Type, Term)
forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
`catchIlltypedPatternBlockedOnMeta` \(TCErr
err , Blocker
x) -> do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term" Int
50 (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 record pattern stuck on meta: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Blocker -> ArgName
forall a. Show a => a -> ArgName
show Blocker
x) ]
Type
t1 <- (NonEmpty (NamedArg Name), Type) -> TCM Type -> TCM Type
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(NonEmpty (NamedArg Name), Type) -> m a -> m a
addContext (NonEmpty (NamedArg Name)
xs, Type
argsT) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes TCM Type
newTypeMeta_
let e :: Expr
e = ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
A.exprNoRange (TypedBinding -> LamBinding
A.DomainFull TypedBinding
b) Expr
body
tgt' :: Type
tgt' = Telescope -> Type -> Type
telePi Telescope
tel Type
t1
Term
w <- TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
tgt') Blocker
x
(Type, Term) -> TCM (Type, Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tgt' , Term
w)
(Type
target0 , Term
w) <- TCM (Type, Term) -> TCM (Type, Term)
postponeOnBlockedPattern (TCM (Type, Term) -> TCM (Type, Term))
-> TCM (Type, Term) -> TCM (Type, Term)
forall a b. (a -> b) -> a -> b
$
(NonEmpty (NamedArg Name), Type)
-> TCM (Type, Term) -> TCM (Type, Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(NonEmpty (NamedArg Name), Type) -> m a -> m a
addContext (NonEmpty (NamedArg Name)
xs, Type
argsT) (TCM (Type, Term) -> TCM (Type, Term))
-> TCM (Type, Term) -> TCM (Type, Term)
forall a b. (a -> b) -> a -> b
$ List1 (NamedArg (Binder' BindName))
-> TCM (Type, Term) -> TCM (Type, Term)
forall a. List1 (NamedArg (Binder' BindName)) -> TCM a -> TCM a
addTypedPatterns List1 (NamedArg (Binder' BindName))
xps (TCM (Type, Term) -> TCM (Type, Term))
-> TCM (Type, Term) -> TCM (Type, Term)
forall a b. (a -> b) -> a -> b
$ do
Type
t1 <- TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes TCM Type
newTypeMeta_
Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
body Type
t1
(Type, Term) -> TCM (Type, Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope -> Type -> Type
telePi Telescope
tel Type
t1 , Telescope -> Term -> Term
teleLam Telescope
tel Term
v)
if ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
notVisible ArgInfo
info Bool -> Bool -> Bool
|| (NamedArg Name -> Bool) -> NonEmpty (NamedArg Name) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any NamedArg Name -> Bool
forall a. LensHiding a => a -> Bool
notVisible NonEmpty (NamedArg Name)
xs then do
ProblemId
pid <- TCM () -> TCMT IO ProblemId
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblem_ (TCM () -> TCMT IO ProblemId) -> TCM () -> TCMT IO ProblemId
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType Type
target0 Type
target
Type -> Term -> ProblemId -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Int m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
target Term
w ProblemId
pid
else do
Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
w Type
target0 Type
target
useTargetType :: Telescope -> Type -> TCM Term
useTargetType tel :: Telescope
tel@(ExtendTel Dom Type
dom (Abs ArgName
y Telescope
EmptyTel)) Type
btyp = do
ArgName -> Int -> TCM () -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> m () -> m ()
verboseS ArgName
"tc.term.lambda" Int
5 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCM ()
forall (m :: * -> *). MonadStatistics m => ArgName -> m ()
tick ArgName
"lambda-with-target-type"
ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.term.lambda" Int
30 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"useTargetType y = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ArgName
y
let (NamedArg Name
x :| []) = NonEmpty (NamedArg Name)
xs
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Dom Type -> ArgInfo -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Dom Type
dom ArgInfo
info) (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
$ Type -> TypeError
WrongHidingInLambda Type
target
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe (WithOrigin (Ranged ArgName)) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (WithOrigin (Ranged ArgName)) -> Bool)
-> Maybe (WithOrigin (Ranged ArgName)) -> Bool
forall a b. (a -> b) -> a -> b
$ NamedArg Name -> Maybe (NameOf (NamedArg Name))
forall a. LensNamed a => a -> Maybe (NameOf a)
getNameOf NamedArg Name
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Dom Type -> NamedArg Name -> Bool
forall a b.
(LensNamed a, LensNamed b, NameOf a ~ WithOrigin (Ranged ArgName),
NameOf b ~ WithOrigin (Ranged ArgName)) =>
a -> b -> Bool
namedSame Dom Type
dom NamedArg Name
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
NamedArg Name -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Name
x (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
$ TypeError
WrongHidingInLHS
ArgInfo
info <- Dom Type -> ArgInfo -> TCM ArgInfo
forall dom.
(LensAnnotation dom, LensModality dom) =>
dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck Dom Type
dom ArgInfo
info
let a :: Type
a = Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom
Term -> TCM ()
checkSizeLtSat (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
a
(ProblemId
pid, Type
argT) <- TCM Type -> TCMT IO (ProblemId, Type)
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m (ProblemId, a)
newProblem (TCM Type -> TCMT IO (ProblemId, Type))
-> TCM Type -> TCMT IO (ProblemId, Type)
forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TCM Type
isTypeEqualTo Expr
typ Type
a
Term
v <- Name -> ArgName -> Dom Type -> TCM Term -> TCM Term
forall a. Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext (NamedArg Name -> Name
forall a. NamedArg a -> a
namedArg NamedArg Name
x) ArgName
y (ArgInfo -> Type -> Dom Type
forall a. ArgInfo -> a -> Dom a
defaultArgDom ArgInfo
info Type
argT) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
List1 (NamedArg (Binder' BindName)) -> TCM Term -> TCM Term
forall a. List1 (NamedArg (Binder' BindName)) -> TCM a -> TCM a
addTypedPatterns List1 (NamedArg (Binder' BindName))
xps (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
body Type
btyp
Type -> Term -> ProblemId -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Int m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
target (ArgInfo -> Abs Term -> Term
Lam ArgInfo
info (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs (NamedArg Name -> ArgName
namedArgName NamedArg Name
x) Term
v) ProblemId
pid
useTargetType Telescope
_ Type
_ = TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
lambdaModalityCheck :: (LensAnnotation dom, LensModality dom) => dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck :: forall dom.
(LensAnnotation dom, LensModality dom) =>
dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck dom
dom = Annotation -> ArgInfo -> TCM ArgInfo
forall dom. LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo
lambdaAnnotationCheck (dom -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation dom
dom) (ArgInfo -> TCM ArgInfo)
-> (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck Modality
m (ArgInfo -> TCM ArgInfo)
-> (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck Modality
m (ArgInfo -> TCM ArgInfo)
-> (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Modality -> ArgInfo -> TCM ArgInfo
forall dom. LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck Modality
m
where m :: Modality
m = dom -> Modality
forall a. LensModality a => a -> Modality
getModality dom
dom
lambdaIrrelevanceCheck :: LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck :: forall dom. LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck dom
dom ArgInfo
info
| ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
== Relevance
defaultRelevance = ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$ Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance (dom -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance dom
dom) ArgInfo
info
| Bool
otherwise = do
let rPi :: Relevance
rPi = dom -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance dom
dom
let rLam :: Relevance
rLam = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Relevance -> Relevance -> Bool
sameRelevance Relevance
rPi Relevance
rLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongIrrelevanceInLambda
ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info
lambdaQuantityCheck :: LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck :: forall dom. LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck dom
dom ArgInfo
info
| ArgInfo -> Bool
forall a. LensQuantity a => a -> Bool
noUserQuantity ArgInfo
info = ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$ Quantity -> ArgInfo -> ArgInfo
forall a. LensQuantity a => Quantity -> a -> a
setQuantity (dom -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity dom
dom) ArgInfo
info
| Bool
otherwise = do
let qPi :: Quantity
qPi = dom -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity dom
dom
let qLam :: Quantity
qLam = ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
info
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Quantity
qPi Quantity -> Quantity -> Bool
`sameQuantity` Quantity
qLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongQuantityInLambda
ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info
lambdaAnnotationCheck :: LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo
lambdaAnnotationCheck :: forall dom. LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo
lambdaAnnotationCheck dom
dom ArgInfo
info
| ArgInfo -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation ArgInfo
info Annotation -> Annotation -> Bool
forall a. Eq a => a -> a -> Bool
== Annotation
defaultAnnotation = ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$ Annotation -> ArgInfo -> ArgInfo
forall a. LensAnnotation a => Annotation -> a -> a
setAnnotation (dom -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation dom
dom) ArgInfo
info
| Bool
otherwise = do
let aPi :: Annotation
aPi = dom -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation dom
dom
let aLam :: Annotation
aLam = ArgInfo -> Annotation
forall a. LensAnnotation a => a -> Annotation
getAnnotation ArgInfo
info
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Annotation
aPi Annotation -> Annotation -> Bool
forall a. Eq a => a -> a -> Bool
== Annotation
aLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
GenericError (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$ ArgName
"Wrong annotation in lambda"
ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info
lambdaCohesionCheck :: LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck :: forall dom. LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck dom
dom ArgInfo
info
| ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
== Cohesion
defaultCohesion = ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgInfo -> TCM ArgInfo) -> ArgInfo -> TCM ArgInfo
forall a b. (a -> b) -> a -> b
$ Cohesion -> ArgInfo -> ArgInfo
forall a. LensCohesion a => Cohesion -> a -> a
setCohesion (dom -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion dom
dom) ArgInfo
info
| Bool
otherwise = do
let cPi :: Cohesion
cPi = dom -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion dom
dom
let cLam :: Cohesion
cLam = ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
info
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Cohesion
cPi Cohesion -> Cohesion -> Bool
`sameCohesion` Cohesion
cLam) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError TypeError
WrongCohesionInLambda
ArgInfo -> TCM ArgInfo
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgInfo
info
lambdaAddContext :: Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext :: forall a. Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext Name
x ArgName
y Dom Type
dom
| Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x = (ArgName, Dom Type) -> TCMT IO a -> TCMT IO a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ArgName, Dom Type) -> m a -> m a
addContext (ArgName
y, Dom Type
dom)
| Bool
otherwise = (Name, Dom Type) -> TCMT IO a -> TCMT IO a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(Name, Dom Type) -> m a -> m a
addContext (Name
x, Dom Type
dom)
checkPostponedLambda :: Comparison -> Arg (List1 (WithHiding Name), Maybe Type) -> A.Expr -> Type -> TCM Term
checkPostponedLambda :: Comparison
-> Arg (List1 (WithHiding Name), Maybe Type)
-> Expr
-> Type
-> TCM Term
checkPostponedLambda Comparison
cmp args :: Arg (List1 (WithHiding Name), Maybe Type)
args@(Arg ArgInfo
info (WithHiding Hiding
h Name
x :| [WithHiding Name]
xs, Maybe Type
mt)) Expr
body Type
target = do
let postpone :: Blocker -> Type -> TCM Term
postpone Blocker
_ Type
t = TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison
-> Arg (List1 (WithHiding Name), Maybe Type)
-> Expr
-> Type
-> TypeCheckingProblem
CheckLambda Comparison
cmp Arg (List1 (WithHiding Name), Maybe Type)
args Expr
body Type
t
lamHiding :: Hiding
lamHiding = Hiding -> Hiding -> Hiding
forall a. Monoid a => a -> a -> a
mappend Hiding
h (Hiding -> Hiding) -> Hiding -> Hiding
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info
Hiding
-> Type
-> (Blocker -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas Hiding
lamHiding Type
target Blocker -> Type -> TCM Term
postpone ((Type -> TCM Term) -> TCM Term) -> (Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ t :: Type
t@(El Sort' Term
_ (Pi Dom Type
dom Abs Type
b)) -> do
ArgInfo
info' <- Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
lamHiding (ArgInfo -> ArgInfo) -> TCM ArgInfo -> TCM ArgInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dom Type -> ArgInfo -> TCM ArgInfo
forall dom.
(LensAnnotation dom, LensModality dom) =>
dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck Dom Type
dom ArgInfo
info
Maybe ProblemId
mpid <- Maybe Type
-> TCMT IO (Maybe ProblemId)
-> (Type -> TCMT IO (Maybe ProblemId))
-> TCMT IO (Maybe ProblemId)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Type
mt (Maybe ProblemId -> TCMT IO (Maybe ProblemId)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ProblemId
forall a. Maybe a
Nothing) ((Type -> TCMT IO (Maybe ProblemId)) -> TCMT IO (Maybe ProblemId))
-> (Type -> TCMT IO (Maybe ProblemId)) -> TCMT IO (Maybe ProblemId)
forall a b. (a -> b) -> a -> b
$ \ Type
ascribedType -> ProblemId -> Maybe ProblemId
forall a. a -> Maybe a
Just (ProblemId -> Maybe ProblemId)
-> TCMT IO ProblemId -> TCMT IO (Maybe ProblemId)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
TCM () -> TCMT IO ProblemId
forall (m :: * -> *) a.
(MonadFresh ProblemId m, MonadConstraint m) =>
m a -> m ProblemId
newProblem_ (TCM () -> TCMT IO ProblemId) -> TCM () -> TCMT IO ProblemId
forall a b. (a -> b) -> a -> b
$ Type -> Type -> TCM ()
forall (m :: * -> *). MonadConversion m => Type -> Type -> m ()
leqType (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
dom) Type
ascribedType
let dom' :: Dom Type
dom' = Relevance -> Dom Type -> Dom Type
forall a. LensRelevance a => Relevance -> a -> a
setRelevance (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info') (Dom Type -> Dom Type)
-> (Dom Type -> Dom Type) -> Dom Type -> Dom Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hiding -> Dom Type -> Dom Type
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
lamHiding (Dom Type -> Dom Type) -> Dom Type -> Dom Type
forall a b. (a -> b) -> a -> b
$
Dom Type -> (Type -> Dom Type) -> Maybe Type -> Dom Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Dom Type
dom (Dom Type
dom Dom Type -> Type -> Dom Type
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$>) Maybe Type
mt
Term
v <- Name -> ArgName -> Dom Type -> TCM Term -> TCM Term
forall a. Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext Name
x (Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b) Dom Type
dom' (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
Comparison
-> Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term
checkPostponedLambda0 Comparison
cmp (ArgInfo
-> ([WithHiding Name], Maybe Type)
-> Arg ([WithHiding Name], Maybe Type)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info ([WithHiding Name]
xs, Maybe Type
mt)) Expr
body (Type -> TCM Term) -> Type -> TCM Term
forall a b. (a -> b) -> a -> b
$ Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b
let v' :: Term
v' = ArgInfo -> Abs Term -> Term
Lam ArgInfo
info' (Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs (Name -> ArgName
nameToArgName Name
x) Term
v
TCM Term -> (ProblemId -> TCM Term) -> Maybe ProblemId -> TCM Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v') (Type -> Term -> ProblemId -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadFresh Int m) =>
Type -> Term -> ProblemId -> m Term
blockTermOnProblem Type
t Term
v') Maybe ProblemId
mpid
checkPostponedLambda0 :: Comparison -> Arg ([WithHiding Name], Maybe Type) -> A.Expr -> Type -> TCM Term
checkPostponedLambda0 :: Comparison
-> Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term
checkPostponedLambda0 Comparison
cmp (Arg ArgInfo
_ ([] , Maybe Type
_ )) Expr
body Type
target =
Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
body Type
target
checkPostponedLambda0 Comparison
cmp (Arg ArgInfo
info (WithHiding Name
x : [WithHiding Name]
xs, Maybe Type
mt)) Expr
body Type
target =
Comparison
-> Arg (List1 (WithHiding Name), Maybe Type)
-> Expr
-> Type
-> TCM Term
checkPostponedLambda Comparison
cmp (ArgInfo
-> (List1 (WithHiding Name), Maybe Type)
-> Arg (List1 (WithHiding Name), Maybe Type)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (WithHiding Name
x WithHiding Name -> [WithHiding Name] -> List1 (WithHiding Name)
forall a. a -> [a] -> NonEmpty a
:| [WithHiding Name]
xs, Maybe Type
mt)) Expr
body Type
target
insertHiddenLambdas
:: Hiding
-> Type
-> (Blocker -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas :: Hiding
-> Type
-> (Blocker -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas Hiding
h Type
target Blocker -> Type -> TCM Term
postpone Type -> TCM Term
ret = do
Type
-> (Blocker -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
target Blocker -> Type -> TCM Term
postpone ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
Pi Dom Type
dom Abs Type
b -> do
let h' :: Hiding
h' = Dom Type -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding Dom Type
dom
if Hiding -> Hiding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h Hiding
h' then Type -> TCM Term
ret Type
t else do
if Hiding -> Bool
forall a. LensHiding a => a -> Bool
visible Hiding
h' then TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
WrongHidingInLambda Type
target else do
let x :: ArgName
x = Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b
ArgInfo -> Abs Term -> Term
Lam (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
forall a b. (a -> b) -> a -> b
$ Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom Type
dom) (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
Abs ArgName
x (Term -> Term) -> TCM Term -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
(ArgName, Dom Type) -> TCM Term -> TCM Term
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
(ArgName, Dom Type) -> m a -> m a
addContext (ArgName
x, Dom Type
dom) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Hiding
-> Type
-> (Blocker -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas Hiding
h (Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b) Blocker -> Type -> TCM Term
postpone Type -> TCM Term
ret
Term
_ -> TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> (Doc -> TypeError) -> Doc -> TCM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM Term) -> TCMT IO Doc -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
TCMT IO Doc
"Expected " 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
target TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" to be a function type"
checkAbsurdLambda :: Comparison -> A.ExprInfo -> Hiding -> A.Expr -> Type -> TCM Term
checkAbsurdLambda :: Comparison -> ExprInfo -> Hiding -> Expr -> Type -> TCM Term
checkAbsurdLambda Comparison
cmp ExprInfo
i Hiding
h Expr
e Type
t = (TCEnv -> TCEnv) -> TCM Term -> TCM Term
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (Lens' Quantity TCEnv -> LensSet Quantity TCEnv
forall i o. Lens' i o -> LensSet i o
set (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' Quantity TCEnv
eQuantity Quantity
topQuantity) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
Type
t <- Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
Type
-> (Blocker -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
blocker Type
t' -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t') Blocker
blocker) ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t' -> do
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t' of
Pi dom :: Dom Type
dom@(Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info', unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b
| Bool -> Bool
not (Hiding -> ArgInfo -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding Hiding
h ArgInfo
info') -> TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
WrongHidingInLambda Type
t'
| Bool
otherwise -> Type -> TCM Term -> TCM Term
forall (m :: * -> *).
(MonadMetaSolver m, MonadConstraint m, MonadFresh Int m,
MonadFresh ProblemId m) =>
Type -> m Term -> m Term
blockTerm Type
t' (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
Range -> Type -> TCM ()
ensureEmptyType (ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i) Type
a
ModuleName
top <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
QName
aux <- ModuleName -> Name -> QName
qualify ModuleName
top (Name -> QName) -> TCMT IO Name -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Range, ArgName) -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
forall (m :: * -> *).
MonadFresh NameId m =>
(Range, ArgName) -> m Name
freshName_ (ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
i, ArgName
absurdLambdaName)
Modality
mod <- (TCEnv -> Modality) -> TCMT IO Modality
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Modality
forall a. LensModality a => a -> Modality
getModality
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.absurd" 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
"Adding absurd function" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Modality -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Modality -> m Doc
prettyTCM Modality
mod) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
aux
, 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
"of 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
t'
]
Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
QName -> Definition -> TCM ()
addConstant QName
aux (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$
(\ Defn
d -> (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn (Modality -> ArgInfo -> ArgInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
info') QName
aux Type
t' Language
lang Defn
d)
{ defPolarity :: [Polarity]
defPolarity = [Polarity
Nonvariant]
, defArgOccurrences :: [Occurrence]
defArgOccurrences = [Occurrence
Unused] })
(Defn -> Definition) -> Defn -> Definition
forall a b. (a -> b) -> a -> b
$ FunctionData -> Defn
FunctionDefn FunctionData
emptyFunctionData
{ _funClauses :: [Clause]
_funClauses =
[ Clause
{ clauseLHSRange :: Range
clauseLHSRange = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
, clauseFullRange :: Range
clauseFullRange = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
, clauseTel :: Telescope
clauseTel = ListTel -> Telescope
telFromList [(Type -> (ArgName, Type)) -> Dom Type -> Dom' Term (ArgName, Type)
forall a b. (a -> b) -> Dom' Term a -> Dom' Term b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ArgName
absurdPatternName,) Dom Type
dom]
, namedClausePats :: NAPs
namedClausePats = [ArgInfo -> Named_ DeBruijnPattern -> Arg (Named_ DeBruijnPattern)
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' (Named_ DeBruijnPattern -> Arg (Named_ DeBruijnPattern))
-> Named_ DeBruijnPattern -> Arg (Named_ DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ Maybe (WithOrigin (Ranged ArgName))
-> DeBruijnPattern -> Named_ DeBruijnPattern
forall name a. Maybe name -> a -> Named name a
Named (WithOrigin (Ranged ArgName) -> Maybe (WithOrigin (Ranged ArgName))
forall a. a -> Maybe a
Just (WithOrigin (Ranged ArgName)
-> Maybe (WithOrigin (Ranged ArgName)))
-> WithOrigin (Ranged ArgName)
-> Maybe (WithOrigin (Ranged ArgName))
forall a b. (a -> b) -> a -> b
$ Origin -> Ranged ArgName -> WithOrigin (Ranged ArgName)
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
Inserted (Ranged ArgName -> WithOrigin (Ranged ArgName))
-> Ranged ArgName -> WithOrigin (Ranged ArgName)
forall a b. (a -> b) -> a -> b
$ ArgName -> Ranged ArgName
forall a. a -> Ranged a
unranged (ArgName -> Ranged ArgName) -> ArgName -> Ranged ArgName
forall a b. (a -> b) -> a -> b
$ Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b) (DeBruijnPattern -> Named_ DeBruijnPattern)
-> DeBruijnPattern -> Named_ DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ Int -> DeBruijnPattern
absurdP Int
0]
, 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 (Arg Type -> Maybe (Arg Type)) -> Arg Type -> Maybe (Arg Type)
forall a b. (a -> b) -> a -> b
$ Modality -> Arg Type -> Arg Type
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod (Arg Type -> Arg Type) -> Arg Type -> Arg Type
forall a b. (a -> b) -> a -> b
$ Type -> Arg Type
forall e. e -> Arg e
defaultArg (Type -> Arg Type) -> Type -> Arg Type
forall a b. (a -> b) -> a -> b
$ Abs Type -> Type
forall a. Subst a => Abs a -> a
absBody Abs Type
b
, clauseCatchall :: Bool
clauseCatchall = Bool
True
, clauseExact :: Maybe Bool
clauseExact = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
, 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
True
, clauseEllipsis :: ExpandedEllipsis
clauseEllipsis = ExpandedEllipsis
NoEllipsis
, clauseWhereModule :: Maybe ModuleName
clauseWhereModule = Maybe ModuleName
forall a. Maybe a
Nothing
}
]
, _funCompiled :: Maybe CompiledClauses
_funCompiled = CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just (CompiledClauses -> Maybe CompiledClauses)
-> CompiledClauses -> Maybe CompiledClauses
forall a b. (a -> b) -> a -> b
$ [Arg ArgName] -> CompiledClauses
forall a. [Arg ArgName] -> CompiledClauses' a
Fail [ArgInfo -> ArgName -> Arg ArgName
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info' ArgName
"()"]
, _funSplitTree :: Maybe SplitTree
_funSplitTree = SplitTree -> Maybe SplitTree
forall a. a -> Maybe a
Just (SplitTree -> Maybe SplitTree) -> SplitTree -> Maybe SplitTree
forall a b. (a -> b) -> a -> b
$ Int -> SplitTree
forall a. Int -> SplitTree' a
SplittingDone Int
0
, _funMutual :: Maybe [QName]
_funMutual = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just []
, _funTerminates :: Maybe Bool
_funTerminates = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
, _funExtLam :: Maybe ExtLamInfo
_funExtLam = ExtLamInfo -> Maybe ExtLamInfo
forall a. a -> Maybe a
Just (ExtLamInfo -> Maybe ExtLamInfo) -> ExtLamInfo -> Maybe ExtLamInfo
forall a b. (a -> b) -> a -> b
$ ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
top Bool
True Maybe System
forall a. Null a => a
empty
}
QName -> Elims -> Term
Def QName
aux (Elims -> Term) -> (Telescope -> Elims) -> Telescope -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ([Arg Term] -> Elims)
-> (Telescope -> [Arg Term]) -> Telescope -> Elims
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Telescope -> [Arg Term]
forall a t. DeBruijn a => Tele (Dom t) -> [Arg a]
teleArgs (Telescope -> Term) -> TCMT IO Telescope -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
Term
_ -> TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBePi Type
t'
checkExtendedLambda ::
Comparison -> A.ExprInfo -> A.DefInfo -> Erased -> QName ->
List1 A.Clause -> A.Expr -> Type -> TCM Term
checkExtendedLambda :: Comparison
-> ExprInfo
-> DefInfo
-> Erased
-> QName
-> List1 Clause
-> Expr
-> Type
-> TCM Term
checkExtendedLambda Comparison
cmp ExprInfo
i DefInfo
di Erased
erased QName
qname List1 Clause
cs Expr
e Type
t = do
Modality
mod <- (TCEnv -> Modality) -> TCMT IO Modality
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Modality
forall a. LensModality a => a -> Modality
getModality
if Erased -> Bool
isErased Erased
erased Bool -> Bool -> Bool
&& Bool -> Bool
not (Modality -> Bool
forall a. LensQuantity a => a -> Bool
hasQuantity0 Modality
mod) then
ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError (ArgName -> TCM Term) -> ArgName -> TCM Term
forall a b. (a -> b) -> a -> b
$ [ArgName] -> ArgName
unwords
[ ArgName
"Erased pattern-matching lambdas may only be used in erased"
, ArgName
"contexts"
]
else (TCEnv -> TCEnv) -> TCM Term -> TCM Term
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (Lens' Quantity TCEnv -> LensSet Quantity TCEnv
forall i o. Lens' i o -> LensSet i o
set (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' Quantity TCEnv
eQuantity LensSet Quantity TCEnv -> LensSet Quantity TCEnv
forall a b. (a -> b) -> a -> b
$ Erased -> Quantity
asQuantity Erased
erased) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
DefaultToInfty -> TCM ()
solveSizeConstraints DefaultToInfty
DontDefaultToInfty
ModuleName
lamMod <- TCMT IO ModuleName -> TCMT IO ModuleName
forall a. TCM a -> TCM a
inFreshModuleIfFreeParams TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
Type
t <- Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
Type
-> (Blocker -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
m Type
t' -> TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t') ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
MutualId
j <- TCM MutualId
currentOrFreshMutualBlock
Modality
mod <- (TCEnv -> Modality) -> TCMT IO Modality
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Modality
forall a. LensModality a => a -> Modality
getModality
let info :: ArgInfo
info = Modality -> ArgInfo -> ArgInfo
forall a. LensModality a => Modality -> a -> a
setModality Modality
mod ArgInfo
defaultArgInfo
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.exlam" 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
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep
[ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ IsAbstract -> ArgName
forall a. Show a => a -> ArgName
show (IsAbstract -> ArgName) -> IsAbstract -> ArgName
forall a b. (a -> b) -> a -> b
$ DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
A.defAbstract DefInfo
di
, TCMT IO Doc
"extended lambda's implementation"
, TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
doubleQuotes (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 :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
qname
, TCMT IO Doc
"has type:"
]
, Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
]
[Arg Term]
args <- TCMT IO [Arg Term]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
IsAbstract -> TCM Term -> TCM Term
forall {m :: * -> *} {a}. MonadTCEnv m => IsAbstract -> m a -> m a
abstract (DefInfo -> IsAbstract
forall t. DefInfo' t -> IsAbstract
A.defAbstract DefInfo
di) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
QName -> Definition -> TCM ()
addConstant QName
qname (Definition -> TCM ()) -> TCMT IO Definition -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
Language
lang <- TCMT IO Language
forall (m :: * -> *). HasOptions m => m Language
getLanguage
Definition -> TCMT IO Definition
useTerPragma (Definition -> TCMT IO Definition)
-> Definition -> TCMT IO Definition
forall a b. (a -> b) -> a -> b
$
(ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
info QName
qname Type
t Language
lang Defn
emptyFunction)
{ defMutual :: MutualId
defMutual = MutualId
j }
Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> DefInfo
-> QName
-> [Clause]
-> TCM ()
checkFunDef' Type
t ArgInfo
info Delayed
NotDelayed (ExtLamInfo -> Maybe ExtLamInfo
forall a. a -> Maybe a
Just (ExtLamInfo -> Maybe ExtLamInfo) -> ExtLamInfo -> Maybe ExtLamInfo
forall a b. (a -> b) -> a -> b
$ ModuleName -> Bool -> Maybe System -> ExtLamInfo
ExtLamInfo ModuleName
lamMod Bool
False Maybe System
forall a. Null a => a
empty) Maybe QName
forall a. Maybe a
Nothing DefInfo
di QName
qname ([Clause] -> TCM ()) -> [Clause] -> TCM ()
forall a b. (a -> b) -> a -> b
$
List1 Clause -> [Item (List1 Clause)]
forall l. IsList l => l -> [Item l]
List1.toList List1 Clause
cs
TCMT IO (Maybe MutualId) -> TCM () -> TCM ()
forall (m :: * -> *) a. Monad m => m (Maybe a) -> m () -> m ()
whenNothingM ((TCEnv -> Maybe MutualId) -> TCMT IO (Maybe MutualId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe MutualId
envMutualBlock) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
QName -> TCM ()
checkIApplyConfluence_ QName
qname
Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
qname (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
args
where
abstract :: IsAbstract -> m a -> m a
abstract IsAbstract
ConcreteDef = m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode
abstract IsAbstract
AbstractDef = m a -> m a
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inAbstractMode
catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
catchIlltypedPatternBlockedOnMeta :: forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
catchIlltypedPatternBlockedOnMeta TCM a
m (TCErr, Blocker) -> TCM a
handle = do
TCState
st <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
TCM a
m TCM a -> (TCErr -> TCM a) -> TCM a
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err -> do
let reraise :: MonadError TCErr m => m a
reraise :: forall (m :: * -> *) a. MonadError TCErr m => m a
reraise = TCErr -> m a
forall a. TCErr -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
Blocker
blocker <- TCMT IO Blocker
-> (Blocker -> TCMT IO Blocker) -> Maybe Blocker -> TCMT IO Blocker
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TCMT IO Blocker
forall (m :: * -> *) a. MonadError TCErr m => m a
reraise Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Blocker -> TCMT IO Blocker)
-> Maybe Blocker -> TCMT IO Blocker
forall a b. (a -> b) -> a -> b
$ case TCErr
err of
TypeError CallStack
_ TCState
s Closure TypeError
cl -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cl of
SortOfSplitVarError Maybe Blocker
b Doc
_ -> Maybe Blocker
b
SplitError (UnificationStuck Maybe Blocker
b QName
c Telescope
tel [Arg Term]
us [Arg Term]
vs [UnificationFailure]
_) -> Maybe Blocker
b
SplitError (BlockedType Blocker
b Closure Type
aClosure) -> Blocker -> Maybe Blocker
forall a. a -> Maybe a
Just Blocker
b
CannotEliminateWithPattern Maybe Blocker
b NamedArg Pattern
p Type
a -> Maybe Blocker
b
TypeError
_ -> Maybe Blocker
forall a. Maybe a
Nothing
TCErr
_ -> Maybe Blocker
forall a. Maybe a
Nothing
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.postpone" 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 definition blocked 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 a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Blocker -> m Doc
prettyTCM Blocker
blocker ]
TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st
Blocker
blocker <- ((MetaId -> TCMT IO Blocker) -> Blocker -> TCMT IO Blocker
forall (m :: * -> *).
Monad m =>
(MetaId -> m Blocker) -> Blocker -> m Blocker
`onBlockingMetasM` Blocker
blocker) ((MetaId -> TCMT IO Blocker) -> TCMT IO Blocker)
-> (MetaId -> TCMT IO Blocker) -> TCMT IO Blocker
forall a b. (a -> b) -> a -> b
$ \ MetaId
x ->
MetaId -> TCMT IO (Maybe (Either RemoteMetaVariable MetaVariable))
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
x TCMT IO (Maybe (Either RemoteMetaVariable MetaVariable))
-> (Maybe (Either RemoteMetaVariable MetaVariable)
-> TCMT IO Blocker)
-> TCMT IO Blocker
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ case
Maybe (Either RemoteMetaVariable MetaVariable)
Nothing -> Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
neverUnblock
Just Left{} -> Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock
Just (Right MetaVariable
m)
| InstV{} <- MetaVariable -> MetaInstantiation
mvInstantiation MetaVariable
m -> Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocker
alwaysUnblock
| Bool
otherwise -> Blocker -> TCMT IO Blocker
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Blocker -> TCMT IO Blocker) -> Blocker -> TCMT IO Blocker
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
x
if Blocker
blocker Blocker -> [Blocker] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Blocker
neverUnblock, Blocker
alwaysUnblock] then TCM a
forall (m :: * -> *) a. MonadError TCErr m => m a
reraise else (TCErr, Blocker) -> TCM a
handle (TCErr
err, Blocker
blocker)
expandModuleAssigns
:: [Either A.Assign A.ModuleName]
-> [C.Name]
-> TCM A.Assigns
expandModuleAssigns :: [Either (FieldAssignment' Expr) ModuleName]
-> [Name] -> TCM Assigns
expandModuleAssigns [Either (FieldAssignment' Expr) ModuleName]
mfs [Name]
xs = do
let (Assigns
fs , [ModuleName]
ms) = [Either (FieldAssignment' Expr) ModuleName]
-> (Assigns, [ModuleName])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (FieldAssignment' Expr) ModuleName]
mfs
[Maybe (FieldAssignment' Expr)]
fs' <- [Name]
-> (Name -> TCMT IO (Maybe (FieldAssignment' Expr)))
-> TCMT IO [Maybe (FieldAssignment' Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Name]
xs [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ (FieldAssignment' Expr -> Name) -> Assigns -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Lens' Name (FieldAssignment' Expr) -> FieldAssignment' Expr -> Name
forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
view (Name -> f Name)
-> FieldAssignment' Expr -> f (FieldAssignment' Expr)
forall a (f :: * -> *).
Functor f =>
(Name -> f Name) -> FieldAssignment' a -> f (FieldAssignment' a)
Lens' Name (FieldAssignment' Expr)
nameFieldA) Assigns
fs) ((Name -> TCMT IO (Maybe (FieldAssignment' Expr)))
-> TCMT IO [Maybe (FieldAssignment' Expr)])
-> (Name -> TCMT IO (Maybe (FieldAssignment' Expr)))
-> TCMT IO [Maybe (FieldAssignment' Expr)]
forall a b. (a -> b) -> a -> b
$ \ Name
f -> do
[Maybe (ModuleName, FieldAssignment' Expr)]
pms <- [ModuleName]
-> (ModuleName
-> TCMT IO (Maybe (ModuleName, FieldAssignment' Expr)))
-> TCMT IO [Maybe (ModuleName, FieldAssignment' Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ModuleName]
ms ((ModuleName
-> TCMT IO (Maybe (ModuleName, FieldAssignment' Expr)))
-> TCMT IO [Maybe (ModuleName, FieldAssignment' Expr)])
-> (ModuleName
-> TCMT IO (Maybe (ModuleName, FieldAssignment' Expr)))
-> TCMT IO [Maybe (ModuleName, FieldAssignment' Expr)]
forall a b. (a -> b) -> a -> b
$ \ ModuleName
m -> do
Scope
modScope <- ModuleName -> ScopeM Scope
getNamedScope ModuleName
m
let names :: ThingsInScope AbstractName
names :: ThingsInScope AbstractName
names = Scope -> ThingsInScope AbstractName
forall a. InScope a => Scope -> ThingsInScope a
exportedNamesInScope Scope
modScope
Maybe (ModuleName, FieldAssignment' Expr)
-> TCMT IO (Maybe (ModuleName, FieldAssignment' Expr))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (ModuleName, FieldAssignment' Expr)
-> TCMT IO (Maybe (ModuleName, FieldAssignment' Expr)))
-> Maybe (ModuleName, FieldAssignment' Expr)
-> TCMT IO (Maybe (ModuleName, FieldAssignment' Expr))
forall a b. (a -> b) -> a -> b
$
case Name -> ThingsInScope AbstractName -> Maybe [AbstractName]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
f ThingsInScope AbstractName
names of
Just [AbstractName
n] -> (ModuleName, FieldAssignment' Expr)
-> Maybe (ModuleName, FieldAssignment' Expr)
forall a. a -> Maybe a
Just (ModuleName
m, Name -> Expr -> FieldAssignment' Expr
forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
f (Expr -> FieldAssignment' Expr) -> Expr -> FieldAssignment' Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. KillRange a => KillRangeT a
killRange (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ AbstractName -> Expr
forall a. NameToExpr a => a -> Expr
A.nameToExpr AbstractName
n)
Maybe [AbstractName]
_ -> Maybe (ModuleName, FieldAssignment' Expr)
forall a. Maybe a
Nothing
case [Maybe (ModuleName, FieldAssignment' Expr)]
-> [(ModuleName, FieldAssignment' Expr)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (ModuleName, FieldAssignment' Expr)]
pms of
[] -> Maybe (FieldAssignment' Expr)
-> TCMT IO (Maybe (FieldAssignment' Expr))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (FieldAssignment' Expr)
forall a. Maybe a
Nothing
[(ModuleName
_, FieldAssignment' Expr
fa)] -> Maybe (FieldAssignment' Expr)
-> TCMT IO (Maybe (FieldAssignment' Expr))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FieldAssignment' Expr -> Maybe (FieldAssignment' Expr)
forall a. a -> Maybe a
Just FieldAssignment' Expr
fa)
[(ModuleName, FieldAssignment' Expr)]
mfas -> TypeError -> TCMT IO (Maybe (FieldAssignment' Expr))
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO (Maybe (FieldAssignment' Expr)))
-> (Doc -> TypeError)
-> Doc
-> TCMT IO (Maybe (FieldAssignment' Expr))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO (Maybe (FieldAssignment' Expr)))
-> TCMT IO Doc -> TCMT IO (Maybe (FieldAssignment' Expr))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
[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
"Ambiguity: the field" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Name -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
f
TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"appears in the following modules: " TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. a -> [a] -> [a]
: ((ModuleName, FieldAssignment' Expr) -> TCMT IO Doc)
-> [(ModuleName, FieldAssignment' Expr)] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM (ModuleName -> TCMT IO Doc)
-> ((ModuleName, FieldAssignment' Expr) -> ModuleName)
-> (ModuleName, FieldAssignment' Expr)
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, FieldAssignment' Expr) -> ModuleName
forall a b. (a, b) -> a
fst) [(ModuleName, FieldAssignment' Expr)]
mfas
Assigns -> TCM Assigns
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Assigns
fs Assigns -> Assigns -> Assigns
forall a. [a] -> [a] -> [a]
++ [Maybe (FieldAssignment' Expr)] -> Assigns
forall a. [Maybe a] -> [a]
catMaybes [Maybe (FieldAssignment' Expr)]
fs')
checkRecordExpression
:: Comparison
-> A.RecordAssigns
-> A.Expr
-> Type
-> TCM Term
checkRecordExpression :: Comparison
-> [Either (FieldAssignment' Expr) ModuleName]
-> Expr
-> Type
-> TCM Term
checkRecordExpression Comparison
cmp [Either (FieldAssignment' Expr) ModuleName]
mfs Expr
e Type
t = do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" 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 record expression"
, Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
]
Type
-> (Blocker -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
_ Type
t -> Type -> TCM Term
guessRecordType Type
t) ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t -> do
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t of
Def QName
r Elims
es -> do
let ~(Just [Arg Term]
vs) = Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
" r = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
r
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" xs = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> do
ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> TCMT IO ArgName -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Name] -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow ([Name] -> ArgName)
-> ([Dom' Term Name] -> [Name]) -> [Dom' Term Name] -> ArgName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Dom' Term Name -> Name) -> [Dom' Term Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term Name -> Name
forall t e. Dom' t e -> e
unDom ([Dom' Term Name] -> ArgName)
-> TCMT IO [Dom' Term Name] -> TCMT IO ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO [Dom' Term Name]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m [Dom' Term Name]
getRecordFieldNames QName
r
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" ftel= " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> do
Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO Telescope
getRecordFieldTypes QName
r
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" con = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> do
ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> TCMT IO ArgName -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConHead -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (ConHead -> ArgName) -> TCMT IO ConHead -> TCMT IO ArgName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO ConHead
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m ConHead
getRecordConstructor QName
r
Defn
def <- QName -> TCMT IO Defn
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m Defn
getRecordDef QName
r
let
cxs :: [Arg Name]
cxs = (Dom' Term Name -> Arg Name) -> [Dom' Term Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term Name] -> [Arg Name]) -> [Dom' Term Name] -> [Arg Name]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom' Term Name]
recordFieldNames Defn
def
xs :: [Name]
xs = (Arg Name -> Name) -> [Arg Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Arg Name -> Name
forall e. Arg e -> e
unArg [Arg Name]
cxs
con :: ConHead
con = KillRangeT ConHead
forall a. KillRange a => KillRangeT a
killRange KillRangeT ConHead -> KillRangeT ConHead
forall a b. (a -> b) -> a -> b
$ Defn -> ConHead
recConHead Defn
def
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" 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
" xs = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Doc
forall a. Pretty a => a -> Doc
P.pretty [Name]
xs)
, TCMT IO Doc
" ftel= " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Defn -> Telescope
recTel Defn
def)
, TCMT IO Doc
" con = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead -> Doc
forall a. Pretty a => a -> Doc
P.pretty ConHead
con)
]
Quantity
constructorQ <- Definition -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Definition -> Quantity) -> TCMT IO Definition -> TCMT IO Quantity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
con)
Quantity
currentQ <- Lens' Quantity TCEnv -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC (Quantity -> f Quantity) -> TCEnv -> f TCEnv
Lens' Quantity TCEnv
eQuantity
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Quantity
constructorQ Quantity -> Quantity -> Bool
`moreQuantity` Quantity
currentQ) (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
$ ArgName -> TypeError
GenericError (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$
ArgName
"A record expression corresponding to an erased record " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++
ArgName
"constructor must only be used in erased settings"
[Name] -> [QName] -> TCM ()
disambiguateRecordFields ((FieldAssignment' Expr -> Name) -> Assigns -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FieldAssignment' Expr -> Name
forall a. FieldAssignment' a -> Name
_nameFieldA (Assigns -> [Name]) -> Assigns -> [Name]
forall a b. (a -> b) -> a -> b
$ [Either (FieldAssignment' Expr) ModuleName] -> Assigns
forall a b. [Either a b] -> [a]
lefts [Either (FieldAssignment' Expr) ModuleName]
mfs) ((Dom QName -> QName) -> [Dom QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> QName
forall t e. Dom' t e -> e
unDom ([Dom QName] -> [QName]) -> [Dom QName] -> [QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom QName]
recFields Defn
def)
Assigns
fs <- [Either (FieldAssignment' Expr) ModuleName]
-> [Name] -> TCM Assigns
expandModuleAssigns [Either (FieldAssignment' Expr) ModuleName]
mfs ((Arg Name -> Name) -> [Arg Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Arg Name -> Name
forall e. Arg e -> e
unArg [Arg Name]
cxs)
ScopeInfo
scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
let re :: Range
re = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
meta :: Name -> Expr
meta Name
x = MetaInfo -> Expr
A.Underscore (MetaInfo -> Expr) -> MetaInfo -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> ScopeInfo -> Maybe MetaId -> ArgName -> MetaInfo
A.MetaInfo Range
re ScopeInfo
scope Maybe MetaId
forall a. Maybe a
Nothing (Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow Name
x)
[NamedArg Expr]
es <- QName
-> (Name -> Expr) -> Assigns -> [Arg Name] -> TCM [NamedArg Expr]
forall a.
HasRange a =>
QName
-> (Name -> a)
-> [FieldAssignment' a]
-> [Arg Name]
-> TCM [NamedArg a]
insertMissingFieldsWarn QName
r Name -> Expr
meta Assigns
fs [Arg Name]
cxs
[Arg Term]
args <- Comparison
-> ExpandHidden
-> Range
-> [NamedArg Expr]
-> Telescope
-> TCM (Elims, Telescope)
checkArguments_ Comparison
cmp ExpandHidden
ExpandLast Range
re [NamedArg Expr]
es (Defn -> Telescope
recTel Defn
def Telescope -> [Arg Term] -> Telescope
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
vs) TCM (Elims, Telescope)
-> ((Elims, Telescope) -> TCMT IO [Arg Term]) -> TCMT IO [Arg Term]
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
(Elims
elims, Telescope
remainingTel) | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
remainingTel
, Just [Arg Term]
args <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
elims -> [Arg Term] -> TCMT IO [Arg Term]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Arg Term]
args
(Elims, Telescope)
_ -> TCMT IO [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"finished record expression"
Term -> TCM Term
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCM Term) -> Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConORec ((Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply [Arg Term]
args)
Term
_ -> TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
t
where
guessRecordType :: Type -> TCM Term
guessRecordType Type
t = do
let fields :: [Name]
fields = [ Name
x | Left (FieldAssignment Name
x Expr
_) <- [Either (FieldAssignment' Expr) ModuleName]
mfs ]
[QName]
rs <- [Name] -> TCM [QName]
findPossibleRecords [Name]
fields
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Possible records for" 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 -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"are" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [QName] -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [QName]
rs
case [QName]
rs of
[] -> case [Name]
fields of
[] -> ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"There are no records in scope"
[Name
f] -> ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError (ArgName -> TCM Term) -> ArgName -> TCM Term
forall a b. (a -> b) -> a -> b
$ ArgName
"There is no known record with the field " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow Name
f
[Name]
_ -> ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError (ArgName -> TCM Term) -> ArgName -> TCM Term
forall a b. (a -> b) -> a -> b
$ ArgName
"There is no known record with the fields " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [ArgName] -> ArgName
unwords ((Name -> ArgName) -> [Name] -> [ArgName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow [Name]
fields)
[QName
r] -> do
Definition
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
r
[Arg Term]
ps <- QName -> TCMT IO [Arg Term]
forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
MonadTCEnv m, MonadDebug m) =>
QName -> m [Arg Term]
freeVarsToApply QName
r
let rt :: Type
rt = Definition -> Type
defType Definition
def
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.rec" Int
30 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Type of unique record" 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
rt
[Arg Term]
vs <- Type -> TCMT IO [Arg Term]
forall (m :: * -> *). MonadMetaSolver m => Type -> m [Arg Term]
newArgsMeta Type
rt
Type
target <- Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> [Arg Term] -> Type
piApply Type
rt [Arg Term]
vs
Sort' Term
s <- case Type -> Term
forall t a. Type'' t a -> a
unEl Type
target of
Sort Sort' Term
s -> Sort' Term -> TCMT IO (Sort' Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Sort' Term
s
Term
v -> do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"impossible" 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
"The impossible happened when checking record expression against meta"
, TCMT IO Doc
"Candidate record type r = " 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
r
, TCMT IO Doc
"Type of r = " 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
rt
, TCMT IO Doc
"Ends in (should be sort)= " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
, ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
" Raw = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Term -> ArgName
forall a. Show a => a -> ArgName
show Term
v
]
TCMT IO (Sort' Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
let inferred :: Type
inferred = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
r (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ([Arg Term]
ps [Arg Term] -> [Arg Term] -> [Arg Term]
forall a. [a] -> [a] -> [a]
++ [Arg Term]
vs)
Term
v <- Expr -> Type -> TCM Term
checkExpr Expr
e Type
inferred
Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
inferred Type
t
QName
_:QName
_:[QName]
_ -> do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.rec" 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
"Postponing type checking of"
, 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
$ Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e 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 Type
t
]
TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t
checkRecordUpdate
:: Comparison
-> A.ExprInfo
-> A.Expr
-> A.Assigns
-> A.Expr
-> Type
-> TCM Term
checkRecordUpdate :: Comparison
-> ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term
checkRecordUpdate Comparison
cmp ExprInfo
ei Expr
recexpr Assigns
fs Expr
eupd Type
t = do
Type
-> (Blocker -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
t (\ Blocker
_ Type
_ -> TCM Term
tryInfer) ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
t' -> do
TCMT IO (Maybe (QName, [Arg Term], Defn))
-> TCM Term -> ((QName, [Arg Term], Defn) -> TCM Term) -> TCM Term
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Type -> TCMT IO (Maybe (QName, [Arg Term], Defn))
forall (m :: * -> *).
PureTCM m =>
Type -> m (Maybe (QName, [Arg Term], Defn))
isRecordType Type
t') TCM Term
should (((QName, [Arg Term], Defn) -> TCM Term) -> TCM Term)
-> ((QName, [Arg Term], Defn) -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ (QName
r, [Arg Term]
_pars, Defn
defn) -> do
Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
recexpr Type
t'
Name
name <- Range -> TCMT IO Name
forall (m :: * -> *). MonadFresh NameId m => Range -> m Name
freshNoName (Range -> TCMT IO Name) -> Range -> TCMT IO Name
forall a b. (a -> b) -> a -> b
$ Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
recexpr
ArgInfo -> Name -> Term -> Type -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding ArgInfo
defaultArgInfo Name
name Term
v Type
t' (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
let projs :: [Arg QName]
projs = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ Defn -> [Dom QName]
recFields Defn
defn
[Name] -> [QName] -> TCM ()
disambiguateRecordFields ((FieldAssignment' Expr -> Name) -> Assigns -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FieldAssignment' Expr -> Name
forall a. FieldAssignment' a -> Name
_nameFieldA Assigns
fs) ((Arg QName -> QName) -> [Arg QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Arg QName -> QName
forall e. Arg e -> e
unArg [Arg QName]
projs)
let fs' :: [(Name, Maybe Expr)]
fs' = (FieldAssignment' Expr -> (Name, Maybe Expr))
-> Assigns -> [(Name, Maybe Expr)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (FieldAssignment Name
x Expr
e) -> (Name
x, Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e)) Assigns
fs
[Arg Name]
axs <- (Dom' Term Name -> Arg Name) -> [Dom' Term Name] -> [Arg Name]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term Name -> Arg Name
forall t a. Dom' t a -> Arg a
argFromDom ([Dom' Term Name] -> [Arg Name])
-> TCMT IO [Dom' Term Name] -> TCMT IO [Arg Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO [Dom' Term Name]
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m [Dom' Term Name]
getRecordFieldNames QName
r
[Maybe Expr]
es <- QName
-> (Arg Name -> Maybe Expr)
-> [Arg Name]
-> [(Name, Maybe Expr)]
-> TCM [Maybe Expr]
forall a.
HasRange a =>
QName -> (Arg Name -> a) -> [Arg Name] -> [(Name, a)] -> TCM [a]
orderFieldsWarn QName
r (Maybe Expr -> Arg Name -> Maybe Expr
forall a b. a -> b -> a
const Maybe Expr
forall a. Maybe a
Nothing) [Arg Name]
axs [(Name, Maybe Expr)]
fs'
let es' :: [Maybe Expr]
es' = (Arg QName -> Maybe Expr -> Maybe Expr)
-> [Arg QName] -> [Maybe Expr] -> [Maybe Expr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> ExprInfo -> Arg QName -> Maybe Expr -> Maybe Expr
replaceFields Name
name ExprInfo
ei) [Arg QName]
projs [Maybe Expr]
es
let erec :: Expr
erec = ExprInfo -> [Either (FieldAssignment' Expr) ModuleName] -> Expr
A.Rec ExprInfo
ei [ FieldAssignment' Expr -> Either (FieldAssignment' Expr) ModuleName
forall a b. a -> Either a b
Left (Name -> Expr -> FieldAssignment' Expr
forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
x Expr
e) | (Arg ArgInfo
_ Name
x, Just Expr
e) <- [Arg Name] -> [Maybe Expr] -> [(Arg Name, Maybe Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Arg Name]
axs [Maybe Expr]
es' ]
Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
erec Type
t
where
replaceFields :: Name -> A.ExprInfo -> Arg A.QName -> Maybe A.Expr -> Maybe A.Expr
replaceFields :: Name -> ExprInfo -> Arg QName -> Maybe Expr -> Maybe Expr
replaceFields Name
name ExprInfo
ei (Arg ArgInfo
ai QName
p) Maybe Expr
Nothing | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai = Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$
AppInfo -> Expr -> NamedArg Expr -> Expr
A.App
(Range -> AppInfo
A.defaultAppInfo (Range -> AppInfo) -> Range -> AppInfo
forall a b. (a -> b) -> a -> b
$ ExprInfo -> Range
forall a. HasRange a => a -> Range
getRange ExprInfo
ei)
(ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjSystem (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous QName
p)
(Expr -> NamedArg Expr
forall a. a -> NamedArg a
defaultNamedArg (Expr -> NamedArg Expr) -> Expr -> NamedArg Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
A.Var Name
name)
replaceFields Name
_ ExprInfo
_ Arg QName
_ Maybe Expr
me = Maybe Expr
me
tryInfer :: TCM Term
tryInfer = do
(Term
_, Type
trec) <- Expr -> TCM (Term, Type)
inferExpr Expr
recexpr
Type
-> (Blocker -> Type -> TCM Term)
-> (NotBlocked -> Type -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Type
trec (\ Blocker
_ Type
_ -> TCM Term
postpone) ((NotBlocked -> Type -> TCM Term) -> TCM Term)
-> (NotBlocked -> Type -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Type
_ -> do
Term
v <- Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
eupd Type
trec
Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
trec Type
t
postpone :: TCM Term
postpone = TypeCheckingProblem -> TCM Term
postponeTypeCheckingProblem_ (TypeCheckingProblem -> TCM Term)
-> TypeCheckingProblem -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
eupd Type
t
should :: TCM Term
should = TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeRecordType Type
t
checkLiteral :: Literal -> Type -> TCM Term
checkLiteral :: Literal -> Type -> TCM Term
checkLiteral Literal
lit Type
t = do
Type
t' <- Literal -> TCM Type
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType Literal
lit
Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
CmpEq (Literal -> Term
Lit Literal
lit) Type
t' Type
t
scopedExpr :: A.Expr -> TCM A.Expr
scopedExpr :: Expr -> TCM Expr
scopedExpr (A.ScopedExpr ScopeInfo
scope Expr
e) = ScopeInfo -> TCM ()
setScope ScopeInfo
scope TCM () -> TCM Expr -> TCM Expr
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> TCM Expr
scopedExpr Expr
e
scopedExpr Expr
e = Expr -> TCM Expr
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
checkExpr :: A.Expr -> Type -> TCM Term
checkExpr :: Expr -> Type -> TCM Term
checkExpr = Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
CmpLeq
checkExpr'
:: Comparison
-> A.Expr
-> Type
-> TCM Term
checkExpr' :: Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t =
ArgName -> Int -> ArgName -> TCM Term -> TCM Term
forall a. ArgName -> Int -> ArgName -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> ArgName -> m a -> m a
verboseBracket ArgName
"tc.term.expr.top" Int
5 ArgName
"checkExpr" (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
ArgName -> Int -> (Term -> TCMT IO Doc) -> TCM Term -> TCM Term
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> (a -> TCMT IO Doc) -> m a -> m a
reportResult ArgName
"tc.term.expr.top" Int
15 (\ Term
v -> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"checkExpr" 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 [ Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e, TCMT IO 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
" returns" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v ]) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
Call -> TCM Term -> TCM Term
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
cmp Expr
e Type
t) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TCM Term -> TCM Term
forall a. TCM a -> TCM a
localScope (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TCM Term -> TCM Term
forall a. TCM a -> TCM a
doExpandLast (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
forall (m :: * -> *). PureTCM m => Term -> m Term
unfoldInlined (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.top" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Checking" 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
sep
[ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e, TCMT IO 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
"at " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (Range -> ArgName) -> Range -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Range -> TCMT IO Doc) -> TCMT IO Range -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Range
forall (m :: * -> *). MonadTCEnv m => m Range
getCurrentRange)
]
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.top.detailed" Int
80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"Checking" 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 [ Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
e, TCMT IO Doc
":", ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Type -> ArgName
forall a. Show a => a -> ArgName
show Type
t) ]
Type
tReduced <- Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
t
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.expr.top" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
tReduced
Expr
e <- Expr -> TCM Expr
scopedExpr Expr
e
TCM Term -> TCM Term
irrelevantIfProp <- (BlockT (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
forall (m :: * -> *) a.
Monad m =>
BlockT m a -> m (Either Blocker a)
runBlocked (BlockT (TCMT IO) Bool -> TCMT IO (Either Blocker Bool))
-> BlockT (TCMT IO) Bool -> TCMT IO (Either Blocker Bool)
forall a b. (a -> b) -> a -> b
$ Type -> BlockT (TCMT IO) Bool
forall a (m :: * -> *).
(LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) =>
a -> m Bool
isPropM Type
t) TCMT IO (Either Blocker Bool)
-> (Either Blocker Bool -> TCMT IO (TCM Term -> TCM Term))
-> TCMT IO (TCM Term -> TCM Term)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Right Bool
True -> do
let mod :: Modality
mod = Modality
defaultModality { modRelevance :: Relevance
modRelevance = Relevance
Irrelevant }
(TCM Term -> TCM Term) -> TCMT IO (TCM Term -> TCM Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TCM Term -> TCM Term) -> TCMT IO (TCM Term -> TCM Term))
-> (TCM Term -> TCM Term) -> TCMT IO (TCM Term -> TCM Term)
forall a b. (a -> b) -> a -> b
$ (Term -> Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> Term
dontCare (TCM Term -> TCM Term)
-> (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> TCM Term -> TCM Term
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext Modality
mod
Either Blocker Bool
_ -> (TCM Term -> TCM Term) -> TCMT IO (TCM Term -> TCM Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return TCM Term -> TCM Term
forall a. a -> a
id
TCM Term -> TCM Term
irrelevantIfProp (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TCM Term -> TCM Term
tryInsertHiddenLambda Expr
e Type
tReduced (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ case Expr
e of
A.ScopedExpr ScopeInfo
scope Expr
e -> TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
A.QuestionMark MetaInfo
i InteractionId
ii -> (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> InteractionId -> TCM Term
checkQuestionMark (RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta' RunMetaOccursCheck
RunMetaOccursCheck) Comparison
cmp Type
t MetaInfo
i InteractionId
ii
A.Underscore MetaInfo
i -> Comparison -> Type -> MetaInfo -> TCM Term
checkUnderscore Comparison
cmp Type
t MetaInfo
i
A.WithApp ExprInfo
_ Expr
e [Expr]
es -> TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
NotImplemented ArgName
"type checking of with application"
e0 :: Expr
e0@(A.App AppInfo
i Expr
q (Arg ArgInfo
ai Named_ Expr
e))
| A.Quote ExprInfo
_ <- Expr -> Expr
unScope Expr
q, ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai -> do
QName
x <- Expr -> TCMT IO QName
forall (m :: * -> *).
(MonadTCError m, MonadAbsToCon m) =>
Expr -> m QName
quotedName (Expr -> TCMT IO QName) -> Expr -> TCMT IO QName
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e
Type
ty <- TCM Type
qNameType
Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp (QName -> Term
quoteName QName
x) Type
ty Type
t
| A.QuoteTerm ExprInfo
_ <- Expr -> Expr
unScope Expr
q -> do
(Term
et, Type
_) <- Expr -> TCM (Term, Type)
inferExpr (Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e)
Comparison -> Term -> Type -> TCM Term
doQuoteTerm Comparison
cmp Term
et Type
t
A.Quote{} -> ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"quote must be applied to a defined name"
A.QuoteTerm{} -> ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"quoteTerm must be applied to a term"
A.Unquote{} -> ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"unquote must be applied to a term"
A.AbsurdLam ExprInfo
i Hiding
h -> Comparison -> ExprInfo -> Hiding -> Expr -> Type -> TCM Term
checkAbsurdLambda Comparison
cmp ExprInfo
i Hiding
h Expr
e Type
t
A.ExtendedLam ExprInfo
i DefInfo
di Erased
erased QName
qname List1 Clause
cs ->
Comparison
-> ExprInfo
-> DefInfo
-> Erased
-> QName
-> List1 Clause
-> Expr
-> Type
-> TCM Term
checkExtendedLambda Comparison
cmp ExprInfo
i DefInfo
di Erased
erased QName
qname List1 Clause
cs Expr
e Type
t
A.Lam ExprInfo
i (A.DomainFull TypedBinding
b) Expr
e -> Comparison -> TypedBinding -> Expr -> Type -> TCM Term
checkLambda Comparison
cmp TypedBinding
b Expr
e Type
t
A.Lam ExprInfo
i (A.DomainFree Maybe Expr
_ NamedArg (Binder' BindName)
x) Expr
e0
| Maybe (WithOrigin (Ranged ArgName)) -> Bool
forall a. Maybe a -> Bool
isNothing (Named (WithOrigin (Ranged ArgName)) (Binder' BindName)
-> Maybe (WithOrigin (Ranged ArgName))
forall name a. Named name a -> Maybe name
nameOf (Named (WithOrigin (Ranged ArgName)) (Binder' BindName)
-> Maybe (WithOrigin (Ranged ArgName)))
-> Named (WithOrigin (Ranged ArgName)) (Binder' BindName)
-> Maybe (WithOrigin (Ranged ArgName))
forall a b. (a -> b) -> a -> b
$ NamedArg (Binder' BindName)
-> Named (WithOrigin (Ranged ArgName)) (Binder' BindName)
forall e. Arg e -> e
unArg NamedArg (Binder' BindName)
x) Bool -> Bool -> Bool
&& Maybe Pattern -> Bool
forall a. Maybe a -> Bool
isNothing (Binder' BindName -> Maybe Pattern
forall a. Binder' a -> Maybe Pattern
A.binderPattern (Binder' BindName -> Maybe Pattern)
-> Binder' BindName -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ NamedArg (Binder' BindName) -> Binder' BindName
forall a. NamedArg a -> a
namedArg NamedArg (Binder' BindName)
x) ->
Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp (ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i (ArgInfo -> Binder' Name -> LamBinding
domainFree (NamedArg (Binder' BindName) -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg (Binder' BindName)
x) (Binder' Name -> LamBinding) -> Binder' Name -> LamBinding
forall a b. (a -> b) -> a -> b
$ BindName -> Name
A.unBind (BindName -> Name) -> Binder' BindName -> Binder' Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamedArg (Binder' BindName) -> Binder' BindName
forall a. NamedArg a -> a
namedArg NamedArg (Binder' BindName)
x) Expr
e0) Type
t
| Bool
otherwise -> TypeError -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM Term) -> TypeError -> TCM Term
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
NotImplemented ArgName
"named arguments in lambdas"
A.Lit ExprInfo
_ Literal
lit -> Literal -> Type -> TCM Term
checkLiteral Literal
lit Type
t
A.Let ExprInfo
i List1 LetBinding
ds Expr
e -> List1 LetBinding -> TCM Term -> TCM Term
forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings List1 LetBinding
ds (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t
e :: Expr
e@A.Pi{} -> do
Type
t' <- Expr -> TCM Type
isType_ Expr
e
let s :: Sort' Term
s = Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
t'
v :: Term
v = Type -> Term
forall t a. Type'' t a -> a
unEl Type
t'
Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v (Sort' Term -> Type
sort Sort' Term
s) Type
t
A.Generalized Set QName
s Expr
e -> do
([Maybe QName]
_, Type
t') <- Set QName -> TCM Type -> TCM ([Maybe QName], Type)
generalizeType Set QName
s (TCM Type -> TCM ([Maybe QName], Type))
-> TCM Type -> TCM ([Maybe QName], Type)
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
e
let s :: Sort' Term
s = Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
t'
v :: Term
v = Type -> Term
forall t a. Type'' t a -> a
unEl Type
t'
Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v (Sort' Term -> Type
sort Sort' Term
s) Type
t
e :: Expr
e@A.Fun{} -> do
Type
t' <- Expr -> TCM Type
isType_ Expr
e
let s :: Sort' Term
s = Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
t'
v :: Term
v = Type -> Term
forall t a. Type'' t a -> a
unEl Type
t'
Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v (Sort' Term -> Type
sort Sort' Term
s) Type
t
A.Rec ExprInfo
_ [Either (FieldAssignment' Expr) ModuleName]
fs -> Comparison
-> [Either (FieldAssignment' Expr) ModuleName]
-> Expr
-> Type
-> TCM Term
checkRecordExpression Comparison
cmp [Either (FieldAssignment' Expr) ModuleName]
fs Expr
e Type
t
A.RecUpdate ExprInfo
ei Expr
recexpr Assigns
fs -> Comparison
-> ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term
checkRecordUpdate Comparison
cmp ExprInfo
ei Expr
recexpr Assigns
fs Expr
e Type
t
A.DontCare Expr
e ->
TCMT IO Bool -> TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Relevance
Irrelevant Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
==) (Relevance -> Bool) -> TCMT IO Relevance -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Relevance) -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance)
(Term -> Term
dontCare (Term -> Term) -> TCM Term -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Relevance -> TCM Term -> TCM Term
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
Irrelevant (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t)
(ArgName -> TCM Term
forall (tcm :: * -> *) a.
(HasCallStack, MonadTCM tcm) =>
ArgName -> tcm a
internalError ArgName
"DontCare may only appear in irrelevant contexts")
A.Dot{} -> ArgName -> TCM Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
ArgName -> m a
genericError ArgName
"Invalid dotted expression"
Expr
_ | Application Expr
hd [NamedArg Expr]
args <- Expr -> AppView' Expr
appView Expr
e -> Comparison -> Expr -> [NamedArg Expr] -> Expr -> Type -> TCM Term
checkApplication Comparison
cmp Expr
hd [NamedArg Expr]
args Expr
e Type
t
TCM Term -> ((TCErr, Blocker) -> TCM Term) -> TCM Term
forall a. TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
`catchIlltypedPatternBlockedOnMeta` \ (TCErr
err, Blocker
x) -> do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term" Int
50 (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 pattern got stuck on meta: " 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
x ]
TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Expr -> Type -> TypeCheckingProblem
CheckExpr Comparison
cmp Expr
e Type
t) Blocker
x
where
tryInsertHiddenLambda
:: A.Expr
-> Type
-> TCM Term
-> TCM Term
tryInsertHiddenLambda :: Expr -> Type -> TCM Term -> TCM Term
tryInsertHiddenLambda Expr
e Type
tReduced TCM Term
fallback
| Pi (Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
a}) Abs Type
b <- Type -> Term
forall t a. Type'' t a -> a
unEl Type
tReduced
, let h :: Hiding
h = ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info
, Hiding -> Bool
forall a. LensHiding a => a -> Bool
notVisible Hiding
h
, Bool -> Bool
not (Hiding -> Expr -> Bool
forall {a}. LensHiding a => a -> Expr -> Bool
hiddenLambdaOrHole Hiding
h Expr
e)
= do
let proceed :: TCM Term
proceed = ArgInfo -> ArgName -> TCM Term
doInsert (Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
setOrigin Origin
Inserted ArgInfo
info) (ArgName -> TCM Term) -> ArgName -> TCM Term
forall a b. (a -> b) -> a -> b
$ Abs Type -> ArgName
forall a. Abs a -> ArgName
absName Abs Type
b
ExpandHidden
expandHidden <- (TCEnv -> ExpandHidden) -> TCMT IO ExpandHidden
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> ExpandHidden
envExpandLast
if Bool
definitelyIntroduction then TCM Term
proceed else
if ExpandHidden
expandHidden ExpandHidden -> ExpandHidden -> Bool
forall a. Eq a => a -> a -> Bool
== ExpandHidden
ReallyDontExpandLast then TCM Term
fallback else do
Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Type
a TCM Type
-> (Type -> TCMT IO (Maybe BoundedSize))
-> TCMT IO (Maybe BoundedSize)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> TCMT IO (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> m (Maybe BoundedSize)
isSizeType TCMT IO (Maybe BoundedSize)
-> (Maybe BoundedSize -> TCM Term) -> TCM Term
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Just (BoundedLt Term
u) -> Term
-> (Blocker -> Term -> TCM Term)
-> (NotBlocked -> Term -> TCM Term)
-> TCM Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
u (\ Blocker
_ Term
_ -> TCM Term
fallback) ((NotBlocked -> Term -> TCM Term) -> TCM Term)
-> (NotBlocked -> Term -> TCM Term) -> TCM Term
forall a b. (a -> b) -> a -> b
$ \ NotBlocked
_ Term
v -> do
TCMT IO Bool -> TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Term -> TCMT IO Bool
checkSizeNeverZero Term
v) TCM Term
proceed TCM Term
fallback
TCM Term -> (TCErr -> TCM Term) -> TCM Term
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> TCM Term
fallback
Maybe BoundedSize
_ -> TCM Term
proceed
| Bool
otherwise = TCM Term
fallback
where
re :: Range
re = Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e
rx :: Range
rx = Maybe (Position' SrcFile)
-> Range -> (Position' SrcFile -> Range) -> Range
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
rStart Range
re) Range
forall a. Range' a
noRange ((Position' SrcFile -> Range) -> Range)
-> (Position' SrcFile -> Range) -> Range
forall a b. (a -> b) -> a -> b
$ \ Position' SrcFile
pos -> Position' SrcFile -> Position' SrcFile -> Range
forall a. Position' a -> Position' a -> Range' a
posToRange Position' SrcFile
pos Position' SrcFile
pos
doInsert :: ArgInfo -> ArgName -> TCM Term
doInsert ArgInfo
info ArgName
y = do
Name
x <- Name -> Name
forall a. LensInScope a => a -> a
C.setNotInScope (Name -> Name) -> TCMT IO Name -> TCMT IO Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range -> ArgName -> TCMT IO Name
forall (m :: * -> *).
MonadFresh NameId m =>
Range -> ArgName -> m Name
freshName Range
rx ArgName
y
ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.term.expr.impl" Int
15 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"Inserting implicit lambda"
Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp (ExprInfo -> LamBinding -> Expr -> Expr
A.Lam (Range -> ExprInfo
A.ExprRange Range
re) (ArgInfo -> Binder' Name -> LamBinding
domainFree ArgInfo
info (Binder' Name -> LamBinding) -> Binder' Name -> LamBinding
forall a b. (a -> b) -> a -> b
$ Name -> Binder' Name
forall a. a -> Binder' a
A.mkBinder Name
x) Expr
e) Type
tReduced
hiddenLambdaOrHole :: a -> Expr -> Bool
hiddenLambdaOrHole a
h = \case
A.AbsurdLam ExprInfo
_ Hiding
h' -> a -> Hiding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding a
h Hiding
h'
A.ExtendedLam ExprInfo
_ DefInfo
_ Erased
_ QName
_ List1 Clause
cls -> (Clause -> Bool) -> List1 Clause -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Clause -> Bool
hiddenLHS List1 Clause
cls
A.Lam ExprInfo
_ LamBinding
bind Expr
_ -> a -> LamBinding -> Bool
forall a b. (LensHiding a, LensHiding b) => a -> b -> Bool
sameHiding a
h LamBinding
bind
A.QuestionMark{} -> Bool
True
Expr
_ -> Bool
False
hiddenLHS :: Clause -> Bool
hiddenLHS (A.Clause (A.LHS LHSInfo
_ (A.LHSHead QName
_ (NamedArg Pattern
a : [NamedArg Pattern]
_))) [ProblemEq]
_ RHS
_ WhereDeclarations
_ Bool
_) = NamedArg Pattern -> Bool
forall a. LensHiding a => a -> Bool
notVisible NamedArg Pattern
a
hiddenLHS Clause
_ = Bool
False
definitelyIntroduction :: Bool
definitelyIntroduction = case Expr
e of
A.Lam{} -> Bool
True
A.AbsurdLam{} -> Bool
True
A.Lit{} -> Bool
True
A.Pi{} -> Bool
True
A.Fun{} -> Bool
True
A.Rec{} -> Bool
True
A.RecUpdate{} -> Bool
True
A.ScopedExpr{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
Expr
_ -> Bool
False
doQuoteTerm :: Comparison -> Term -> Type -> TCM Term
doQuoteTerm :: Comparison -> Term -> Type -> TCM Term
doQuoteTerm Comparison
cmp Term
et Type
t = do
Term
et' <- Term -> TCM Term
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract (Term -> TCM Term) -> TCM Term -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCM Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
et
case Term -> [MetaId]
forall a. AllMetas a => a -> [MetaId]
allMetasList Term
et' of
[] -> do
Term
q <- Term -> TCM Term
quoteTerm Term
et'
Type
ty <- TCM Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm
Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
q Type
ty Type
t
[MetaId]
metas -> TypeCheckingProblem -> Blocker -> TCM Term
postponeTypeCheckingProblem (Comparison -> Term -> Type -> TypeCheckingProblem
DoQuoteTerm Comparison
cmp Term
et Type
t) (Blocker -> TCM Term) -> Blocker -> TCM Term
forall a b. (a -> b) -> a -> b
$ Set MetaId -> Blocker
unblockOnAllMetas (Set MetaId -> Blocker) -> Set MetaId -> Blocker
forall a b. (a -> b) -> a -> b
$ [MetaId] -> Set MetaId
forall a. Ord a => [a] -> Set a
Set.fromList [MetaId]
metas
unquoteM :: A.Expr -> Term -> Type -> TCM ()
unquoteM :: Expr -> Term -> Type -> TCM ()
unquoteM Expr
tacA Term
hole Type
holeType = do
Term
tac <- Quantity -> TCM Term -> TCM Term
forall (tcm :: * -> *) q a.
(MonadTCEnv tcm, LensQuantity q) =>
q -> tcm a -> tcm a
applyQuantityToContext Quantity
zeroQuantity (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$
Expr -> Type -> TCM Term
checkExpr Expr
tacA (Type -> TCM Term) -> TCM Type -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCM Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Term -> TCM Type
forall (m :: * -> *). Functor m => m Term -> m Type
el (TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Term -> TCM Term -> TCM Term
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit))
TCM () -> TCM ()
forall a. TCM a -> TCM a
inFreshModuleIfFreeParams (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Type -> TCM ()
unquoteTactic Term
tac Term
hole Type
holeType
unquoteTactic :: Term -> Term -> Type -> TCM ()
unquoteTactic :: Term -> Term -> Type -> TCM ()
unquoteTactic Term
tac Term
hole Type
goal = do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.tactic" Int
40 (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
"Running tactic" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
tac
, 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
"on" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
hole 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 Type
goal ]
Either UnquoteError (Term, [QName])
ok <- UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
forall a. UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
runUnquoteM (UnquoteM Term -> TCM (Either UnquoteError (Term, [QName])))
-> UnquoteM Term -> TCM (Either UnquoteError (Term, [QName]))
forall a b. (a -> b) -> a -> b
$ Term -> Term -> UnquoteM Term
unquoteTCM Term
tac Term
hole
case Either UnquoteError (Term, [QName])
ok of
Left (BlockedOnMeta TCState
oldState Blocker
blocker) -> do
TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
let stripFreshMeta :: MetaId -> f Blocker
stripFreshMeta MetaId
x = Blocker
-> (MetaVariable -> Blocker) -> Maybe MetaVariable -> Blocker
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Blocker
neverUnblock (Blocker -> MetaVariable -> Blocker
forall a b. a -> b -> a
const (Blocker -> MetaVariable -> Blocker)
-> Blocker -> MetaVariable -> Blocker
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
x) (Maybe MetaVariable -> Blocker)
-> f (Maybe MetaVariable) -> f Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> f (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
x
Blocker
blocker' <- (MetaId -> TCMT IO Blocker) -> Blocker -> TCMT IO Blocker
forall (m :: * -> *).
Monad m =>
(MetaId -> m Blocker) -> Blocker -> m Blocker
onBlockingMetasM MetaId -> TCMT IO Blocker
forall {f :: * -> *}. ReadTCState f => MetaId -> f Blocker
stripFreshMeta Blocker
blocker
Range
r <- case Set MetaId -> [MetaId]
forall a. Set a -> [a]
Set.toList (Set MetaId -> [MetaId]) -> Set MetaId -> [MetaId]
forall a b. (a -> b) -> a -> b
$ Blocker -> Set MetaId
allBlockingMetas Blocker
blocker' of
MetaId
x : [MetaId]
_ -> Maybe MetaVariable -> Range
forall a. HasRange a => a -> Range
getRange (Maybe MetaVariable -> Range)
-> TCMT IO (Maybe MetaVariable) -> TCMT IO Range
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO (Maybe MetaVariable)
forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe MetaVariable)
lookupLocalMeta' MetaId
x
[] -> Range -> TCMT IO Range
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Range
forall a. Range' a
noRange
Range -> TCM () -> TCM ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Blocker -> Constraint -> TCM ()
forall (m :: * -> *).
MonadConstraint m =>
Blocker -> Constraint -> m ()
addConstraint Blocker
blocker' (Term -> Term -> Type -> Constraint
UnquoteTactic Term
tac Term
hole Type
goal)
Left UnquoteError
err -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ UnquoteError -> TypeError
UnquoteFailed UnquoteError
err
Right (Term, [QName])
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkQuestionMark
:: (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison
-> Type
-> A.MetaInfo
-> InteractionId
-> TCM Term
checkQuestionMark :: (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> InteractionId -> TCM Term
checkQuestionMark Comparison -> Type -> TCM (MetaId, Term)
new Comparison
cmp Type
t0 MetaInfo
i InteractionId
ii = do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.interaction" 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
sep
[ TCMT IO Doc
"Found interaction point"
, ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (IsAbstract -> ArgName) -> IsAbstract -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsAbstract -> ArgName
forall a. Show a => a -> ArgName
show (IsAbstract -> TCMT IO Doc) -> TCMT IO IsAbstract -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> IsAbstract) -> TCMT IO IsAbstract
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (TCEnv -> Lens' IsAbstract TCEnv -> IsAbstract
forall o i. o -> Lens' i o -> i
^. (IsAbstract -> f IsAbstract) -> TCEnv -> f TCEnv
forall a. LensIsAbstract a => Lens' IsAbstract a
Lens' IsAbstract TCEnv
lensIsAbstract)
, InteractionId -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty InteractionId
ii
, TCMT IO Doc
":"
, Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t0
]
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.interaction" Int
60 (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
"Raw:"
, ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Type -> ArgName
forall a. Show a => a -> ArgName
show Type
t0)
]
(Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> TCM Term
checkMeta ((Comparison -> Type -> TCM (MetaId, Term))
-> InteractionId -> Comparison -> Type -> TCM (MetaId, Term)
newQuestionMark' Comparison -> Type -> TCM (MetaId, Term)
new InteractionId
ii) Comparison
cmp Type
t0 MetaInfo
i
checkUnderscore :: Comparison -> Type -> A.MetaInfo -> TCM Term
checkUnderscore :: Comparison -> Type -> MetaInfo -> TCM Term
checkUnderscore = (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> TCM Term
checkMeta (RunMetaOccursCheck -> Comparison -> Type -> TCM (MetaId, Term)
forall (m :: * -> *).
MonadMetaSolver m =>
RunMetaOccursCheck -> Comparison -> Type -> m (MetaId, Term)
newValueMeta RunMetaOccursCheck
RunMetaOccursCheck)
checkMeta :: (Comparison -> Type -> TCM (MetaId, Term)) -> Comparison -> Type -> A.MetaInfo -> TCM Term
checkMeta :: (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> TCM Term
checkMeta Comparison -> Type -> TCM (MetaId, Term)
newMeta Comparison
cmp Type
t MetaInfo
i = (Term, Type) -> Term
forall a b. (a, b) -> a
fst ((Term, Type) -> Term) -> TCM (Term, Type) -> TCM Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Comparison -> Type -> TCM (MetaId, Term))
-> Maybe (Comparison, Type) -> MetaInfo -> TCM (Term, Type)
checkOrInferMeta Comparison -> Type -> TCM (MetaId, Term)
newMeta ((Comparison, Type) -> Maybe (Comparison, Type)
forall a. a -> Maybe a
Just (Comparison
cmp , Type
t)) MetaInfo
i
inferMeta :: (Comparison -> Type -> TCM (MetaId, Term)) -> A.MetaInfo -> TCM (Elims -> Term, Type)
inferMeta :: (Comparison -> Type -> TCM (MetaId, Term))
-> MetaInfo -> TCM (Elims -> Term, Type)
inferMeta Comparison -> Type -> TCM (MetaId, Term)
newMeta MetaInfo
i = (Term -> Elims -> Term) -> (Term, Type) -> (Elims -> Term, Type)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst Term -> Elims -> Term
forall t. Apply t => t -> Elims -> t
applyE ((Term, Type) -> (Elims -> Term, Type))
-> TCM (Term, Type) -> TCM (Elims -> Term, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Comparison -> Type -> TCM (MetaId, Term))
-> Maybe (Comparison, Type) -> MetaInfo -> TCM (Term, Type)
checkOrInferMeta Comparison -> Type -> TCM (MetaId, Term)
newMeta Maybe (Comparison, Type)
forall a. Maybe a
Nothing MetaInfo
i
checkOrInferMeta
:: (Comparison -> Type -> TCM (MetaId, Term))
-> Maybe (Comparison , Type)
-> A.MetaInfo
-> TCM (Term, Type)
checkOrInferMeta :: (Comparison -> Type -> TCM (MetaId, Term))
-> Maybe (Comparison, Type) -> MetaInfo -> TCM (Term, Type)
checkOrInferMeta Comparison -> Type -> TCM (MetaId, Term)
newMeta Maybe (Comparison, Type)
mt MetaInfo
i = do
case MetaInfo -> Maybe MetaId
A.metaNumber MetaInfo
i of
Maybe MetaId
Nothing -> do
ScopeInfo -> TCM ()
setScope (MetaInfo -> ScopeInfo
A.metaScope MetaInfo
i)
(Comparison
cmp , Type
t) <- TCMT IO (Comparison, Type)
-> ((Comparison, Type) -> TCMT IO (Comparison, Type))
-> Maybe (Comparison, Type)
-> TCMT IO (Comparison, Type)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Comparison
CmpEq,) (Type -> (Comparison, Type))
-> TCM Type -> TCMT IO (Comparison, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes TCM Type
newTypeMeta_) (Comparison, Type) -> TCMT IO (Comparison, Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Comparison, Type)
mt
(MetaId
x, Term
v) <- Comparison -> Type -> TCM (MetaId, Term)
newMeta Comparison
cmp Type
t
MetaId -> ArgName -> TCM ()
forall (m :: * -> *).
MonadMetaSolver m =>
MetaId -> ArgName -> m ()
setMetaNameSuggestion MetaId
x (MetaInfo -> ArgName
A.metaNameSuggestion MetaInfo
i)
(Term, Type) -> TCM (Term, Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)
Just MetaId
x -> do
let v :: Term
v = MetaId -> Elims -> Term
MetaV MetaId
x []
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
TCMT IO Doc
"checking existing meta " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
Type
t' <- MetaId -> TCM Type
forall (m :: * -> *). ReadTCState m => MetaId -> m Type
metaType MetaId
x
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.meta.check" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"of 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
t'
case Maybe (Comparison, Type)
mt of
Maybe (Comparison, Type)
Nothing -> (Term, Type) -> TCM (Term, Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t')
Just (Comparison
cmp , Type
t) -> (,Type
t) (Term -> (Term, Type)) -> TCM Term -> TCM (Term, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Comparison -> Term -> Type -> Type -> TCM Term
forall (m :: * -> *).
(MonadConversion m, MonadTCM m) =>
Comparison -> Term -> Type -> Type -> m Term
coerce Comparison
cmp Term
v Type
t' Type
t
domainFree :: ArgInfo -> A.Binder' A.Name -> A.LamBinding
domainFree :: ArgInfo -> Binder' Name -> LamBinding
domainFree ArgInfo
info Binder' Name
x =
TypedBinding -> LamBinding
A.DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. (a -> b) -> a -> b
$ Range
-> List1 (NamedArg (Binder' BindName)) -> Expr -> TypedBinding
A.mkTBind Range
r (NamedArg (Binder' BindName) -> List1 (NamedArg (Binder' BindName))
forall el coll. Singleton el coll => el -> coll
singleton (NamedArg (Binder' BindName)
-> List1 (NamedArg (Binder' BindName)))
-> NamedArg (Binder' BindName)
-> List1 (NamedArg (Binder' BindName))
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Binder' BindName -> NamedArg (Binder' BindName)
forall a. ArgInfo -> a -> NamedArg a
unnamedArg ArgInfo
info (Binder' BindName -> NamedArg (Binder' BindName))
-> Binder' BindName -> NamedArg (Binder' BindName)
forall a b. (a -> b) -> a -> b
$ (Name -> BindName) -> Binder' Name -> Binder' BindName
forall a b. (a -> b) -> Binder' a -> Binder' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> BindName
A.mkBindName Binder' Name
x)
(Expr -> TypedBinding) -> Expr -> TypedBinding
forall a b. (a -> b) -> a -> b
$ MetaInfo -> Expr
A.Underscore MetaInfo
underscoreInfo
where
r :: Range
r = Binder' Name -> Range
forall a. HasRange a => a -> Range
getRange Binder' Name
x
underscoreInfo :: MetaInfo
underscoreInfo = A.MetaInfo
{ metaRange :: Range
A.metaRange = Range
r
, metaScope :: ScopeInfo
A.metaScope = ScopeInfo
emptyScopeInfo
, metaNumber :: Maybe MetaId
A.metaNumber = Maybe MetaId
forall a. Maybe a
Nothing
, metaNameSuggestion :: ArgName
A.metaNameSuggestion = Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Name -> ArgName) -> Name -> ArgName
forall a b. (a -> b) -> a -> b
$ Name -> Name
A.nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ Binder' Name -> Name
forall a. Binder' a -> a
A.binderName Binder' Name
x
}
checkKnownArguments
:: [NamedArg A.Expr]
-> Args
-> Type
-> TCM (Args, Type)
checkKnownArguments :: [NamedArg Expr] -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArguments [] [Arg Term]
vs Type
t = ([Arg Term], Type) -> TCM ([Arg Term], Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term]
vs, Type
t)
checkKnownArguments (NamedArg Expr
arg : [NamedArg Expr]
args) [Arg Term]
vs Type
t = do
([Arg Term]
vs', Type
t') <- NamedArg Expr -> TCM ([Arg Term], Type) -> TCM ([Arg Term], Type)
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange NamedArg Expr
arg (TCM ([Arg Term], Type) -> TCM ([Arg Term], Type))
-> TCM ([Arg Term], Type) -> TCM ([Arg Term], Type)
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArgument NamedArg Expr
arg [Arg Term]
vs Type
t
[NamedArg Expr] -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArguments [NamedArg Expr]
args [Arg Term]
vs' Type
t'
checkKnownArgument
:: NamedArg A.Expr
-> Args
-> Type
-> TCM (Args, Type)
checkKnownArgument :: NamedArg Expr -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArgument NamedArg Expr
arg [] Type
_ = Doc -> TCM ([Arg Term], Type)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCM ([Arg Term], Type))
-> TCMT IO Doc -> TCM ([Arg Term], Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
TCMT IO Doc
"Invalid projection parameter " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> NamedArg Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Expr
arg
checkKnownArgument NamedArg Expr
arg (Arg ArgInfo
_ Term
v : [Arg Term]
vs) Type
t = do
(dom :: Dom Type
dom@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = Type
a }, Abs Type
b) <- Type -> TCMT IO (Dom Type, Abs Type)
forall (m :: * -> *).
MonadReduce m =>
Type -> m (Dom Type, Abs Type)
mustBePi Type
t
if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> Dom Type -> Maybe Bool
forall arg dom.
(LensNamed arg, NameOf arg ~ WithOrigin (Ranged ArgName),
LensHiding arg, LensNamed dom,
NameOf dom ~ WithOrigin (Ranged ArgName), LensHiding dom) =>
arg -> dom -> Maybe Bool
fittingNamedArg NamedArg Expr
arg Dom Type
dom
then NamedArg Expr -> [Arg Term] -> Type -> TCM ([Arg Term], Type)
checkKnownArgument NamedArg Expr
arg [Arg Term]
vs (Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
v)
else do
Term
u <- NamedArg Expr -> Type -> TCM Term
checkNamedArg NamedArg Expr
arg Type
a
Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
u Term
v
([Arg Term], Type) -> TCM ([Arg Term], Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Arg Term]
vs, Abs Type
b Abs Type -> SubstArg Type -> Type
forall a. Subst a => Abs a -> SubstArg a -> a
`absApp` Term
SubstArg Type
v)
checkNamedArg :: NamedArg A.Expr -> Type -> TCM Term
checkNamedArg :: NamedArg Expr -> Type -> TCM Term
checkNamedArg arg :: NamedArg Expr
arg@(Arg ArgInfo
info Named_ Expr
e0) Type
t0 = do
let e :: Expr
e = Named_ Expr -> Expr
forall name a. Named name a -> a
namedThing Named_ Expr
e0
let x :: ArgName
x = ArgName -> Named_ Expr -> ArgName
forall a.
(LensNamed a, NameOf a ~ WithOrigin (Ranged ArgName)) =>
ArgName -> a -> ArgName
bareNameWithDefault ArgName
"" Named_ Expr
e0
Call -> TCM Term -> TCM Term
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
CmpLeq Expr
e Type
t0) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.args.named" Int
15 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
TCMT IO Doc
"Checking named arg" 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
sep
[ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep [ NamedArg Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
prettyTCM NamedArg Expr
arg, TCMT IO Doc
":", Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t0 ]
]
ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.term.args.named" Int
75 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
" arg = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ NamedArg Expr -> ArgName
forall a. Show a => a -> ArgName
show (NamedArg Expr -> NamedArg Expr
forall a. ExprLike a => a -> a
deepUnscope NamedArg Expr
arg)
let checkU :: MetaInfo -> TCM Term
checkU = (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> TCM Term
checkMeta (ArgInfo -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m) =>
ArgInfo -> ArgName -> Comparison -> Type -> m (MetaId, Term)
newMetaArg (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
info) ArgName
x) Comparison
CmpLeq Type
t0
let checkQ :: MetaInfo -> InteractionId -> TCM Term
checkQ = (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison -> Type -> MetaInfo -> InteractionId -> TCM Term
checkQuestionMark (ArgInfo -> ArgName -> Comparison -> Type -> TCM (MetaId, Term)
newInteractionMetaArg (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
info) ArgName
x) Comparison
CmpLeq Type
t0
if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isHole Expr
e then Expr -> Type -> TCM Term
checkExpr Expr
e Type
t0 else TCM Term -> TCM Term
forall a. TCM a -> TCM a
localScope (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
Expr -> TCM Expr
scopedExpr Expr
e TCM Expr -> (Expr -> TCM Term) -> TCM Term
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
A.Underscore MetaInfo
i -> MetaInfo -> TCM Term
checkU MetaInfo
i
A.QuestionMark MetaInfo
i InteractionId
ii -> MetaInfo -> InteractionId -> TCM Term
checkQ MetaInfo
i InteractionId
ii
Expr
_ -> TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
where
isHole :: Expr -> Bool
isHole A.Underscore{} = Bool
True
isHole A.QuestionMark{} = Bool
True
isHole (A.ScopedExpr ScopeInfo
_ Expr
e) = Expr -> Bool
isHole Expr
e
isHole Expr
_ = Bool
False
inferExpr :: A.Expr -> TCM (Term, Type)
inferExpr :: Expr -> TCM (Term, Type)
inferExpr = ExpandHidden -> Expr -> TCM (Term, Type)
inferExpr' ExpandHidden
DontExpandLast
inferExpr' :: ExpandHidden -> A.Expr -> TCM (Term, Type)
inferExpr' :: ExpandHidden -> Expr -> TCM (Term, Type)
inferExpr' ExpandHidden
exh Expr
e = Call -> TCM (Term, Type) -> TCM (Term, Type)
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
InferExpr Expr
e) (TCM (Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ do
let Application Expr
hd [NamedArg Expr]
args = Expr -> AppView' Expr
appView Expr
e
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.infer" 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
"inferExpr': appView of " 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 :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
, TCMT IO Doc
" hd = " 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 :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
hd
, TCMT IO Doc
" args = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg Expr] -> TCMT IO Doc
forall a ce (m :: * -> *).
(ToConcrete a, ConOfAbs a ~ [ce], Pretty ce, MonadAbsToCon m) =>
a -> m Doc
prettyAs [NamedArg Expr]
args
]
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.infer" Int
60 (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
[ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
" hd (raw) = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Expr -> ArgName
forall a. Show a => a -> ArgName
show Expr
hd
]
ExpandHidden -> Expr -> [NamedArg Expr] -> Expr -> TCM (Term, Type)
inferApplication ExpandHidden
exh Expr
hd [NamedArg Expr]
args Expr
e
defOrVar :: A.Expr -> Bool
defOrVar :: Expr -> Bool
defOrVar A.Var{} = Bool
True
defOrVar A.Def'{} = Bool
True
defOrVar A.Proj{} = Bool
True
defOrVar (A.ScopedExpr ScopeInfo
_ Expr
e) = Expr -> Bool
defOrVar Expr
e
defOrVar Expr
_ = Bool
False
checkDontExpandLast :: Comparison -> A.Expr -> Type -> TCM Term
checkDontExpandLast :: Comparison -> Expr -> Type -> TCM Term
checkDontExpandLast Comparison
cmp Expr
e Type
t = case Expr
e of
Expr
_ | Application Expr
hd [NamedArg Expr]
args <- Expr -> AppView' Expr
appView Expr
e, Expr -> Bool
defOrVar Expr
hd ->
Call -> TCM Term -> TCM Term
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Comparison -> Expr -> Type -> Call
CheckExprCall Comparison
cmp Expr
e Type
t) (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TCM Term -> TCM Term
forall a. TCM a -> TCM a
localScope (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ TCM Term -> TCM Term
forall a. TCM a -> TCM a
dontExpandLast (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
Comparison -> Expr -> [NamedArg Expr] -> Expr -> Type -> TCM Term
checkApplication Comparison
cmp Expr
hd [NamedArg Expr]
args Expr
e Type
t
Expr
_ -> Comparison -> Expr -> Type -> TCM Term
checkExpr' Comparison
cmp Expr
e Type
t
isModuleFreeVar :: Int -> TCM Bool
isModuleFreeVar :: Int -> TCMT IO Bool
isModuleFreeVar Int
i = do
[Arg Term]
params <- ModuleName -> TCMT IO [Arg Term]
forall (m :: * -> *).
(Functor m, Applicative m, HasOptions m, MonadTCEnv m,
ReadTCState m, MonadDebug m) =>
ModuleName -> m [Arg Term]
moduleParamsToApply (ModuleName -> TCMT IO [Arg Term])
-> TCMT IO ModuleName -> TCMT IO [Arg Term]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Bool) -> [Arg Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Elims -> Term
Var Int
i []) (Term -> Bool) -> (Arg Term -> Term) -> Arg Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
unArg) [Arg Term]
params
inferExprForWith :: Arg A.Expr -> TCM (Term, Type)
inferExprForWith :: Arg Expr -> TCM (Term, Type)
inferExprForWith (Arg ArgInfo
info Expr
e) = ArgName -> Int -> ArgName -> TCM (Term, Type) -> TCM (Term, Type)
forall a. ArgName -> Int -> ArgName -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadDebug m =>
ArgName -> Int -> ArgName -> m a -> m a
verboseBracket ArgName
"tc.with.infer" Int
20 ArgName
"inferExprForWith" (TCM (Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$
Relevance -> TCM (Term, Type) -> TCM (Term, Type)
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext (ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
info) (TCM (Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.with.infer" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"inferExprforWith " 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
ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"tc.with.infer" Int
80 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"inferExprforWith " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Expr -> ArgName
forall a. Show a => a -> ArgName
show (Expr -> Expr
forall a. ExprLike a => a -> a
deepUnscope Expr
e)
Call -> TCM (Term, Type) -> TCM (Term, Type)
forall a. Call -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a. MonadTrace m => Call -> m a -> m a
traceCall (Expr -> Call
InferExpr Expr
e) (TCM (Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ do
(Term
v, Type
t) <- (Term, Type) -> TCM (Term, Type)
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull ((Term, Type) -> TCM (Term, Type))
-> TCM (Term, Type) -> TCM (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM (Term, Type)
inferExpr Expr
e
Term
v0 <- Term -> TCM Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
v
case Term
v0 of
Var Int
i [] -> TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Int -> TCMT IO Bool
isModuleFreeVar Int
i) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.with.infer" Int
80 (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
[ ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> ArgName -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ ArgName
"with expression is variable " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Int -> ArgName
forall a. Show a => a -> ArgName
show Int
i
, TCMT IO Doc
"current modules = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (ModuleName -> ArgName) -> ModuleName -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> ArgName
forall a. Show a => a -> ArgName
show (ModuleName -> TCMT IO Doc) -> TCMT IO ModuleName -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
, TCMT IO Doc
"current module free vars = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> (Int -> ArgName) -> Int -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ArgName
forall a. Show a => a -> ArgName
show (Int -> TCMT IO Doc) -> TCMT IO Int -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Int
getCurrentModuleFreeVars
, TCMT IO Doc
"context size = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc) -> (Int -> ArgName) -> Int -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ArgName
forall a. Show a => a -> ArgName
show (Int -> TCMT IO Doc) -> TCMT IO Int -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
, TCMT IO Doc
"current context = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope
]
TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ Expr -> Term -> TypeError
WithOnFreeVariable Expr
e Term
v0
Term
_ -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
TelV Telescope
tel Type
t0 <- Int -> (Dom Type -> Bool) -> Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> (Dom Type -> Bool) -> Type -> m (TelV Type)
telViewUpTo' (-Int
1) (Bool -> Bool
not (Bool -> Bool) -> (Dom Type -> Bool) -> Dom Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom Type -> Bool
forall a. LensHiding a => a -> Bool
visible) Type
t
case Type -> Term
forall t a. Type'' t a -> a
unEl Type
t0 of
Def QName
d Elims
vs -> do
Maybe DataOrRecord
res <- QName -> TCM (Maybe DataOrRecord)
isDataOrRecordType QName
d
case Maybe DataOrRecord
res of
Maybe DataOrRecord
Nothing -> (Term, Type) -> TCM (Term, Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)
Just{} -> do
([Arg Term]
args, Type
t1) <- Int -> (Hiding -> Bool) -> Type -> TCM ([Arg Term], Type)
forall (m :: * -> *).
(PureTCM m, MonadMetaSolver m, MonadTCM m) =>
Int -> (Hiding -> Bool) -> Type -> m ([Arg Term], Type)
implicitArgs (-Int
1) Hiding -> Bool
forall a. LensHiding a => a -> Bool
notVisible Type
t
(Term, Type) -> TCM (Term, Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term]
args, Type
t1)
Term
_ -> (Term, Type) -> TCM (Term, Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
v, Type
t)
checkLetBindings :: Foldable t => t A.LetBinding -> TCM a -> TCM a
checkLetBindings :: forall (t :: * -> *) a.
Foldable t =>
t LetBinding -> TCM a -> TCM a
checkLetBindings = (LetBinding -> (TCM a -> TCM a) -> TCM a -> TCM a)
-> (TCM a -> TCM a) -> t LetBinding -> TCM a -> TCM a
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((TCM a -> TCM a) -> (TCM a -> TCM a) -> TCM a -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ((TCM a -> TCM a) -> (TCM a -> TCM a) -> TCM a -> TCM a)
-> (LetBinding -> TCM a -> TCM a)
-> LetBinding
-> (TCM a -> TCM a)
-> TCM a
-> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LetBinding -> TCM a -> TCM a
forall a. LetBinding -> TCM a -> TCM a
checkLetBinding) TCM a -> TCM a
forall a. a -> a
id
checkLetBinding :: A.LetBinding -> TCM a -> TCM a
checkLetBinding :: forall a. LetBinding -> TCM a -> TCM a
checkLetBinding b :: LetBinding
b@(A.LetBind LetInfo
i ArgInfo
info BindName
x Expr
t Expr
e) TCM a
ret =
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 (LetBinding -> Call
CheckLetBinding LetBinding
b) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
let check :: Comparison -> Expr -> Type -> TCM Term
check | ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
info Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
Inserted = Comparison -> Expr -> Type -> TCM Term
checkDontExpandLast
| Bool
otherwise = Comparison -> Expr -> Type -> TCM Term
checkExpr'
Type
t <- TCM Type -> TCM Type
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ Expr
t
Term
v <- ArgInfo -> TCM Term -> TCM Term
forall (tcm :: * -> *) m a.
(MonadTCEnv tcm, LensModality m) =>
m -> tcm a -> tcm a
applyModalityToContext ArgInfo
info (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ Comparison -> Expr -> Type -> TCM Term
check Comparison
CmpLeq Expr
e Type
t
ArgInfo -> Name -> Term -> Type -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding ArgInfo
info (BindName -> Name
A.unBind BindName
x) Term
v Type
t TCM a
ret
checkLetBinding b :: LetBinding
b@(A.LetPatBind LetInfo
i Pattern
p Expr
e) TCM a
ret =
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 (LetBinding -> Call
CheckLetBinding LetBinding
b) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
Pattern
p <- Pattern -> TCM Pattern
forall a. ExpandPatternSynonyms a => a -> TCM a
expandPatternSynonyms Pattern
p
(Term
v, Type
t) <- ExpandHidden -> Expr -> TCM (Term, Type)
inferExpr' ExpandHidden
ExpandLast Expr
e
let
t0 :: Type
t0 = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Type -> Sort' Term
forall a. LensSort a => a -> Sort' Term
getSort Type
t) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Dom Type -> Abs Type -> Term
Pi (Type -> Dom Type
forall a. a -> Dom a
defaultDom Type
t) (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
NoAbs ArgName
forall a. Underscore a => a
underscore Type
HasCallStack => Type
__DUMMY_TYPE__)
p0 :: NamedArg Pattern
p0 = ArgInfo
-> Named (WithOrigin (Ranged ArgName)) Pattern -> NamedArg Pattern
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
defaultArgInfo (Maybe (WithOrigin (Ranged ArgName))
-> Pattern -> Named (WithOrigin (Ranged ArgName)) Pattern
forall name a. Maybe name -> a -> Named name a
Named Maybe (WithOrigin (Ranged ArgName))
forall a. Maybe a
Nothing Pattern
p)
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" 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
"let-binding pattern p at 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] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ TCMT IO Doc
"p (A) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Pattern -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p
, 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
"cxtRel=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Relevance -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Relevance -> TCMT IO Doc) -> TCMT IO Relevance -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Relevance) -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance
, TCMT IO Doc
"cxtQnt=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Quantity -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Quantity -> TCMT IO Doc) -> TCMT IO Quantity -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Quantity) -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity
]
]
Int
fvs <- TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
Call
-> Maybe QName
-> [NamedArg Pattern]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
forall a.
Call
-> Maybe QName
-> [NamedArg Pattern]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide (Pattern -> Telescope -> Type -> Call
CheckPattern Pattern
p Telescope
forall a. Tele a
EmptyTel Type
t) Maybe QName
forall a. Maybe a
Nothing [NamedArg Pattern
p0] Type
t0 Maybe Substitution
forall a. Maybe a
Nothing [] ((LHSResult -> TCM a) -> TCM a) -> (LHSResult -> TCM a) -> TCM a
forall a b. (a -> b) -> a -> b
$ \ (LHSResult Int
_ Telescope
delta0 NAPs
ps Bool
_ Arg Type
_t Substitution
_ [AsBinding]
asb IntSet
_ Bool
_) -> [AsBinding] -> TCM a -> TCM a
forall a. [AsBinding] -> TCM a -> TCM a
bindAsPatterns [AsBinding]
asb (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
let p :: DeBruijnPattern
p = case Int -> NAPs -> NAPs
forall a. Int -> [a] -> [a]
drop Int
fvs NAPs
ps of [Arg (Named_ DeBruijnPattern)
p] -> Arg (Named_ DeBruijnPattern) -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg Arg (Named_ DeBruijnPattern)
p; NAPs
_ -> DeBruijnPattern
forall a. HasCallStack => a
__IMPOSSIBLE__
delta :: Telescope
delta = ListTel -> Telescope
telFromList (ListTel -> Telescope) -> ListTel -> Telescope
forall a b. (a -> b) -> a -> b
$ Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
drop Int
fvs (ListTel -> ListTel) -> ListTel -> ListTel
forall a b. (a -> b) -> a -> b
$ Telescope -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Telescope
delta0
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
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
"p (I) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM DeBruijnPattern
p
, TCMT IO Doc
"delta =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
delta
, TCMT IO Doc
"cxtRel=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Relevance -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Relevance -> TCMT IO Doc) -> TCMT IO Relevance -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Relevance) -> TCMT IO Relevance
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance
, TCMT IO Doc
"cxtQnt=" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> do Quantity -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Quantity -> TCMT IO Doc) -> TCMT IO Quantity -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TCEnv -> Quantity) -> TCMT IO Quantity
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity
]
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
80 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
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
"p (I) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName -> TCMT IO Doc)
-> (DeBruijnPattern -> ArgName) -> DeBruijnPattern -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijnPattern -> ArgName
forall a. Show a => a -> ArgName
show) DeBruijnPattern
p
]
[Term -> Term]
fs <- DeBruijnPattern -> TCM [Term -> Term]
recordPatternToProjections DeBruijnPattern
p
[ContextEntry]
cxt0 <- TCMT IO [ContextEntry]
forall (m :: * -> *). MonadTCEnv m => m [ContextEntry]
getContext
let ([ContextEntry]
binds, [ContextEntry]
cxt) = Int -> [ContextEntry] -> ([ContextEntry], [ContextEntry])
forall a. Int -> [a] -> ([a], [a])
splitAt (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
delta) [ContextEntry]
cxt0
toDrop :: Int
toDrop = [ContextEntry] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ContextEntry]
binds
sigma :: [Term]
sigma = ((Term -> Term) -> Term) -> [Term -> Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term
v) [Term -> Term]
fs
sub :: Substitution
sub = [Term] -> Substitution
forall a. DeBruijn a => [a] -> Substitution' a
parallelS ([Term] -> [Term]
forall a. [a] -> [a]
reverse [Term]
sigma)
Substitution
-> ([ContextEntry] -> [ContextEntry]) -> TCM a -> TCM a
forall a.
Substitution
-> ([ContextEntry] -> [ContextEntry]) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadAddContext m =>
Substitution -> ([ContextEntry] -> [ContextEntry]) -> m a -> m a
updateContext Substitution
sub (Int -> [ContextEntry] -> [ContextEntry]
forall a. Int -> [a] -> [a]
drop Int
toDrop) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ do
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
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
"delta =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
delta
, TCMT IO Doc
"binds =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [ContextEntry] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [ContextEntry] -> m Doc
prettyTCM [ContextEntry]
binds
]
let fdelta :: [Dom Type]
fdelta = Telescope -> [Dom Type]
forall a. TermSubst a => Tele (Dom a) -> [Dom a]
flattenTel Telescope
delta
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.pattern" Int
20 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
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
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
"fdelta =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Telescope -> TCMT IO Doc -> TCMT IO Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
delta ([Dom Type] -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => [Dom Type] -> m Doc
prettyTCM [Dom Type]
fdelta)
]
let tsl :: [Dom Type]
tsl = Substitution' (SubstArg [Dom Type]) -> [Dom Type] -> [Dom Type]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution
Substitution' (SubstArg [Dom Type])
sub [Dom Type]
fdelta
let ts :: [Type]
ts = (Dom Type -> Type) -> [Dom Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Dom Type -> Type
forall t e. Dom' t e -> e
unDom [Dom Type]
tsl
let infos :: [ArgInfo]
infos = (Dom Type -> ArgInfo) -> [Dom Type] -> [ArgInfo]
forall a b. (a -> b) -> [a] -> [b]
map Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo [Dom Type]
tsl
let xs :: [Name]
xs = (ContextEntry -> Name) -> [ContextEntry] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Name
forall a b. (a, b) -> a
fst ((Name, Type) -> Name)
-> (ContextEntry -> (Name, Type)) -> ContextEntry -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContextEntry -> (Name, Type)
forall t e. Dom' t e -> e
unDom) ([ContextEntry] -> [ContextEntry]
forall a. [a] -> [a]
reverse [ContextEntry]
binds)
((ArgInfo, Name, Term, Type) -> TCM a -> TCM a)
-> TCM a -> [(ArgInfo, Name, Term, Type)] -> TCM a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((ArgInfo -> Name -> Term -> Type -> TCM a -> TCM a)
-> (ArgInfo, Name, Term, Type) -> TCM a -> TCM a
forall a b c d e. (a -> b -> c -> d -> e) -> (a, b, c, d) -> e
uncurry4 ArgInfo -> Name -> Term -> Type -> TCM a -> TCM a
forall (m :: * -> *) a.
MonadAddContext m =>
ArgInfo -> Name -> Term -> Type -> m a -> m a
addLetBinding) TCM a
ret ([(ArgInfo, Name, Term, Type)] -> TCM a)
-> [(ArgInfo, Name, Term, Type)] -> TCM a
forall a b. (a -> b) -> a -> b
$ [ArgInfo]
-> [Name] -> [Term] -> [Type] -> [(ArgInfo, Name, Term, Type)]
forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
List.zip4 [ArgInfo]
infos [Name]
xs [Term]
sigma [Type]
ts
checkLetBinding (A.LetApply ModuleInfo
i ModuleName
x ModuleApplication
modapp ScopeCopyInfo
copyInfo ImportDirective
_adir) TCM a
ret = do
Int
fv <- TCMT IO Int
getCurrentModuleFreeVars
Int
n <- TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
let new :: Int
new = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
fv
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.apply" Int
10 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Applying" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleName -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ModuleName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ModuleApplication -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA ModuleApplication
modapp TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (TCMT IO Doc
"with" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Int -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Show a) => a -> m Doc
pshow Int
new TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"free variables")
ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"tc.term.let.apply" 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
"context =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Telescope -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM (Telescope -> TCMT IO Doc) -> TCMT IO Telescope -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Telescope
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Telescope
getContextTelescope)
, TCMT IO Doc
"module =" 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 -> TCMT IO Doc) -> TCMT IO ModuleName -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule)
, TCMT IO Doc
"fv =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (Int -> ArgName
forall a. Show a => a -> ArgName
show Int
fv)
]
ModuleInfo
-> ModuleName -> ModuleApplication -> ScopeCopyInfo -> TCM ()
checkSectionApplication ModuleInfo
i ModuleName
x ModuleApplication
modapp ScopeCopyInfo
copyInfo
ModuleName -> Int -> TCM a -> TCM a
forall a. ModuleName -> Int -> TCM a -> TCM a
withAnonymousModule ModuleName
x Int
new TCM a
ret
checkLetBinding A.LetOpen{} TCM a
ret = TCM a
ret
checkLetBinding (A.LetDeclaredVariable BindName
_) TCM a
ret = TCM a
ret