module Agda.TypeChecking.Rules.Term where
import Control.Applicative
import Control.Arrow ((***), (&&&))
import Control.Monad.Trans
import Control.Monad.Reader
import Control.Monad.Error
import Data.Maybe
import Data.List hiding (sort)
import qualified Agda.Utils.IO.Locale as LocIO
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Views
import Agda.Syntax.Scope.Base (emptyScopeInfo)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Free
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Quote
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Rules.Builtin.Coinduction
import Agda.Utils.Fresh
import Agda.Utils.Tuple
import Agda.Utils.Permutation
import Agda.TypeChecking.Empty (isEmptyTypeC)
import Agda.TypeChecking.Rules.Decl (checkSectionApplication)
import Agda.TypeChecking.Rules.Def (checkFunDef)
import Agda.Utils.Monad
import Agda.Utils.Size
#include "../../undefined.h"
import Agda.Utils.Impossible
isType :: A.Expr -> Sort -> TCM Type
isType e s =
traceCall (IsTypeCall e s) $ do
v <- checkExpr e (sort s)
return $ El s v
isType_ :: A.Expr -> TCM Type
isType_ e =
traceCall (IsType_ e) $ do
s <- newSortMeta
isType e s
forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)
forcePi h name (El s t) =
do t' <- reduce t
case t' of
Pi _ _ -> return (El s t', [])
Fun _ _ -> return (El s t', [])
_ -> do
sa <- newSortMeta
sb <- newSortMeta
let s' = sLub sa sb
a <- newTypeMeta sa
x <- freshName_ name
let arg = Arg h Relevant a
b <- addCtx x arg $ newTypeMeta sb
let ty = El s' $ Pi arg (Abs (show x) b)
cs <- equalType (El s t') ty
ty' <- reduce ty
return (ty', cs)
checkTelescope :: A.Telescope -> Sort -> (Telescope -> TCM a) -> TCM a
checkTelescope [] s ret = ret EmptyTel
checkTelescope (b : tel) s ret =
checkTypedBindings b s $ \tel1 ->
checkTelescope tel s $ \tel2 ->
ret $ abstract tel1 tel2
checkTypedBindings :: A.TypedBindings -> Sort -> (Telescope -> TCM a) -> TCM a
checkTypedBindings (A.TypedBindings i (Arg h rel bs)) s ret =
thread (checkTypedBinding h s) bs $ \bss ->
ret $ foldr (\(x,t) -> ExtendTel (Arg h rel t) . Abs x) EmptyTel (concat bss)
checkTypedBinding :: Hiding -> Sort -> A.TypedBinding -> ([(String,Type)] -> TCM a) -> TCM a
checkTypedBinding h s (A.TBind i xs e) ret = do
t <- isType e s
addCtxs xs (Arg h Relevant t) $ ret $ mkTel xs t
where
mkTel [] t = []
mkTel (x:xs) t = (show $ nameConcrete x,t) : mkTel xs (raise 1 t)
checkTypedBinding h s (A.TNoBind e) ret = do
t <- isType e s
ret [("_",t)]
checkTelescope_ :: A.Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope_ [] ret = ret EmptyTel
checkTelescope_ (b : tel) ret =
checkTypedBindings_ b $ \tel1 ->
checkTelescope_ tel $ \tel2 ->
ret $ abstract tel1 tel2
checkTypedBindings_ :: A.TypedBindings -> (Telescope -> TCM a) -> TCM a
checkTypedBindings_ (A.TypedBindings i (Arg h rel bs)) ret =
thread (checkTypedBinding_ h) bs $ \bss ->
ret $ foldr (\(x,t) -> ExtendTel (Arg h rel t) . Abs x) EmptyTel (concat bss)
checkTypedBinding_ :: Hiding -> A.TypedBinding -> ([(String,Type)] -> TCM a) -> TCM a
checkTypedBinding_ h (A.TBind i xs e) ret = do
t <- isType_ e
addCtxs xs (Arg h Relevant t) $ ret $ mkTel xs t
where
mkTel [] t = []
mkTel (x:xs) t = (show $ nameConcrete x,t) : mkTel xs (raise 1 t)
checkTypedBinding_ h (A.TNoBind e) ret = do
t <- isType_ e
ret [("_",t)]
checkLiteral :: Literal -> Type -> TCM Term
checkLiteral lit t = do
t' <- litType lit
v <- blockTerm t (Lit lit) $ leqType t' t
return v
litType :: Literal -> TCM Type
litType l = case l of
LitLevel _ _ -> el <$> primLevel
LitInt _ _ -> el <$> primNat
LitFloat _ _ -> el <$> primFloat
LitChar _ _ -> el <$> primChar
LitString _ _ -> el <$> primString
LitQName _ _ -> el <$> primQName
where
el t = El (mkType 0) t
reduceCon :: MonadTCM tcm => QName -> tcm QName
reduceCon c = do
Con c [] <- constructorForm =<< reduce (Con c [])
return c
checkArguments' ::
ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type -> A.Expr ->
(Args -> Type -> Constraints -> TCM Term) -> TCM Term
checkArguments' exph r args t0 t e k = do
z <- runErrorT $ checkArguments exph r args t0 t
case z of
Right (vs, t1, cs) -> k vs t1 cs
Left t0 -> postponeTypeCheckingProblem e t (unblockedTester t0)
checkExpr :: A.Expr -> Type -> TCM Term
checkExpr e t =
verboseBracket "tc.term.expr.top" 5 "checkExpr" $
traceCall (CheckExpr e t) $ localScope $ do
reportSDoc "tc.term.expr.top" 15 $
text "Checking" <+> sep
[ fsep [ prettyTCM e, text ":", prettyTCM t ]
, nest 2 $ text "at " <+> (text . show =<< getCurrentRange)
]
t <- reduce t
reportSDoc "tc.term.expr.top" 15 $
text " --> " <+> prettyTCM t
let scopedExpr (A.ScopedExpr scope e) = setScope scope >> scopedExpr e
scopedExpr e = return e
unScope (A.ScopedExpr scope e) = unScope e
unScope e = e
e <- scopedExpr e
case e of
_ | not (hiddenLambdaOrHole e)
, FunV (Arg Hidden _ _) _ <- funView (unEl t) -> do
x <- freshName r (argName t)
reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda"
checkExpr (A.Lam (A.ExprRange $ getRange e) (A.DomainFree Hidden x) e) t
where
r = case rStart $ getRange e of
Nothing -> noRange
Just pos -> posToRange pos pos
hiddenLambdaOrHole (A.AbsurdLam _ Hidden) = True
hiddenLambdaOrHole (A.Lam _ (A.DomainFree Hidden _) _) = True
hiddenLambdaOrHole (A.Lam _ (A.DomainFull (A.TypedBindings _ (Arg Hidden _ _))) _) = True
hiddenLambdaOrHole (A.QuestionMark _) = True
hiddenLambdaOrHole _ = False
_ | Application (HeadCon cs@(_:_:_)) args <- appView e -> do
reportSLn "tc.check.term" 40 $ "Ambiguous constructor: " ++ show cs
let getData Constructor{conData = d} = d
getData _ = __IMPOSSIBLE__
reportSLn "tc.check.term" 40 $ " ranges before: " ++ show (getRange cs)
cs <- zip cs . zipWith setRange (map getRange cs) <$> mapM reduceCon cs
reportSLn "tc.check.term" 40 $ " ranges after: " ++ show (getRange cs)
reportSLn "tc.check.term" 40 $ " reduced: " ++ show cs
dcs <- mapM (\(c0, c1) -> (getData /\ const c0) . theDef <$> getConstInfo c1) cs
let badCon t = typeError $ DoesNotConstructAnElementOf
(fst $ head cs) t
let getCon = do
TelV _ t1 <- telView t
t1 <- reduceB $ unEl t1
reportSDoc "tc.check.term.con" 40 $ nest 2 $
text "target type: " <+> prettyTCM t1
case t1 of
NotBlocked (Def d _) -> do
let dataOrRec = case [ c | (d', c) <- dcs, d == d' ] of
c:_ -> do
reportSLn "tc.check.term" 40 $ " decided on: " ++ show c
return (Just c)
[] -> badCon (Def d [])
defn <- theDef <$> getConstInfo d
case defn of
Datatype{} -> dataOrRec
Record{} -> dataOrRec
_ -> badCon (ignoreBlocking t1)
NotBlocked (MetaV _ _) -> return Nothing
Blocked{} -> return Nothing
_ -> badCon (ignoreBlocking t1)
let unblock = isJust <$> getCon
mc <- getCon
case mc of
Just c -> checkConstructorApplication e t c args
Nothing -> postponeTypeCheckingProblem e t unblock
| Application (HeadCon [c]) args <- appView e ->
checkConstructorApplication e t c args
| Application hd args <- appView e ->
checkHeadApplication e t hd args
A.WithApp _ e es -> typeError $ NotImplemented "type checking of with application"
A.App i s (Arg NotHidden r l)
| A.Set _ 0 <- unScope s ->
ifM (not <$> hasUniversePolymorphism)
(typeError $ GenericError "Use --universe-polymorphism to enable level arguments to Set")
$ do
lvl <- primLevel
suc <- do s <- primLevelSuc
return $ \x -> s `apply` [defaultArg x]
n <- checkExpr (namedThing l) (El (mkType 0) lvl)
reportSDoc "tc.univ.poly" 10 $
text "checking Set " <+> prettyTCM n <+> text "against" <+> prettyTCM t
blockTerm t (Sort $ Type n) $ leqType (sort $ Type $ suc n) t
A.App i q (Arg NotHidden r e)
| A.Quote _ <- unScope q -> do
let quoted (A.Def x) = return x
quoted (A.Con (AmbQ [x])) = return x
quoted (A.Con (AmbQ xs)) = typeError $ GenericError $ "quote: Ambigous name: " ++ show xs
quoted (A.ScopedExpr _ e) = quoted e
quoted _ = typeError $ GenericError $ "quote: not a defined name"
x <- quoted (namedThing e)
ty <- qNameType
blockTerm t (quoteName x) $ leqType ty t
A.Quote _ -> typeError $ GenericError "quote must be applied to a defined name"
A.App i e arg -> do
(v0, t0) <- inferExpr e
checkArguments' ExpandLast (getRange e) [arg] t0 t e $ \vs t1 cs ->
blockTerm t (apply v0 vs) $ (cs ++) <$> leqType t1 t
A.AbsurdLam i h -> do
t <- reduceB =<< instantiateFull t
case t of
Blocked{} -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
NotBlocked (El _ MetaV{}) -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
NotBlocked t' -> case funView $ unEl t' of
FunV (Arg h' _ a) _
| h == h' && not (null $ foldTerm metas a) ->
postponeTypeCheckingProblem e (ignoreBlocking t) $
null . foldTerm metas <$> instantiateFull a
| h == h' -> do
cs' <- isEmptyTypeC a
top <- currentModule
let name = "absurd"
aux <- qualify top <$> freshName (getRange i) name
rel <- irrelevant <$> asks envIrrelevant
reportSDoc "tc.term.absurd" 10 $ vcat
[ text "Adding absurd function" <+> prettyTCM rel <> prettyTCM aux
, nest 2 $ text "of type" <+> prettyTCM t'
]
addConstant aux $ Defn rel aux t' (defaultDisplayForm aux) 0
$ Function
{ funClauses =
[Clauses Nothing
(Clause { clauseRange = getRange e
, clauseTel = EmptyTel
, clausePerm = Perm 0 []
, clausePats = [Arg h Relevant $ VarP "()"]
, clauseBody = NoBody
})
]
, funCompiled = Fail
, funDelayed = NotDelayed
, funInv = NotInjective
, funAbstr = ConcreteDef
, funPolarity = [Covariant]
, funArgOccurrences = [Unused]
, funProjection = Nothing
}
blockTerm t' (Def aux []) $ return cs'
| otherwise -> typeError $ WrongHidingInLambda t'
_ -> typeError $ ShouldBePi t'
where
metas (MetaV m _) = [m]
metas _ = []
A.Lam i (A.DomainFull b) e -> do
(v, cs) <- checkTypedBindings_ b $ \tel -> do
t1 <- newTypeMeta_
cs <- escapeContext (size tel) $ leqType (telePi tel t1) t
v <- checkExpr e t1
return (teleLam tel v, cs)
blockTerm t v (return cs)
A.Lam i (A.DomainFree h x) e0 -> do
t <- reduceB t
case t of
Blocked{} -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
NotBlocked (El _ MetaV{}) -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
NotBlocked t' -> case funView $ unEl t' of
FunV arg0@(Arg h' r a) _
| h == h' -> do
v <- addCtx x arg0 $ do
let arg = Arg h r (Var 0 [])
tb = raise 1 t' `piApply` [arg]
v <- checkExpr e0 tb
return $ Lam h $ Abs (show x) v
return v
| otherwise ->
typeError $ WrongHidingInLambda t'
_ -> typeError $ ShouldBePi t'
A.QuestionMark i -> do
setScope (A.metaScope i)
newQuestionMark t
A.Underscore i -> do
setScope (A.metaScope i)
newValueMeta t
A.Lit lit -> checkLiteral lit t
A.Let i ds e -> checkLetBindings ds $ checkExpr e t
A.Pi _ tel e -> do
t' <- checkTelescope_ tel $ \tel -> do
t <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
return $ telePi_ tel t
s <- return $ getSort t'
when (s == Inf) $ reportSDoc "tc.term.sort" 20 $
vcat [ text ("reduced to omega:")
, nest 2 $ text "t =" <+> prettyTCM t'
, nest 2 $ text "cxt =" <+> (prettyTCM =<< getContextTelescope)
]
blockTerm t (unEl t') $ leqType (sort s) t
A.Fun _ (Arg h r a) b -> do
a' <- isType_ a
b' <- isType_ b
let s = getSort a' `sLub` getSort b'
blockTerm t (Fun (Arg h r a') b') $ leqType (sort s) t
A.Set _ n -> do
n <- ifM typeInType (return 0) (return n)
blockTerm t (Sort (mkType n)) $ leqType (sort $ mkType $ n + 1) t
A.Prop _ -> do
typeError $ GenericError "Prop is no longer supported"
A.Rec _ fs -> do
t <- reduce t
case unEl t of
Def r vs -> do
axs <- getRecordFieldNames r
let xs = map unArg axs
ftel <- getRecordFieldTypes r
con <- getRecordConstructor r
scope <- getScope
let meta = A.Underscore $ A.MetaInfo (getRange e) scope Nothing
es <- orderFields r meta xs fs
let tel = ftel `apply` vs
(args, cs) <- checkArguments_ ExpandLast (getRange e)
(zipWith (\ax e -> fmap (const (unnamed e)) ax) axs es)
tel
blockTerm t (Con con args) $ return cs
MetaV _ _ -> do
reportSDoc "tc.term.expr.rec" 10 $ sep
[ text "Postponing type checking of"
, nest 2 $ prettyA e <+> text ":" <+> prettyTCM t
]
postponeTypeCheckingProblem_ e t
_ -> typeError $ ShouldBeRecordType t
A.Var _ -> __IMPOSSIBLE__
A.Def _ -> __IMPOSSIBLE__
A.Con _ -> __IMPOSSIBLE__
A.ETel _ -> __IMPOSSIBLE__
A.DontCare ->
return DontCare
A.ScopedExpr scope e -> setScope scope >> checkExpr e t
e0@(A.QuoteGoal _ x e) -> do
t' <- etaContract =<< normalise t
let metas = foldTerm (\v -> case v of
MetaV m _ -> [m]
_ -> []
) t'
case metas of
_:_ -> postponeTypeCheckingProblem e0 t' $ and <$> mapM isInstantiatedMeta metas
[] -> do
quoted <- quoteType t'
tmType <- agdaTermType
(v,ty) <- addLetBinding Relevant x quoted tmType (inferExpr e)
blockTerm t' v $ leqType ty t'
inferHead :: Head -> TCM (Args -> Term, Type)
inferHead (HeadVar x) = do
(u, a) <- getVarInfo x
when (argRelevance a == Irrelevant) $
typeError $ VariableIsIrrelevant x
return (apply u, unArg a)
inferHead (HeadDef x) = do
(u, a) <- inferDef Def x
return (apply u, a)
inferHead (HeadCon [c]) = do
(u, a) <- inferDef (\c _ -> Con c []) c
Constructor{conPars = n} <- theDef <$> (instantiateDef =<< getConstInfo c)
verboseS "tc.term.con" 7 $ do
liftIO $ LocIO.putStrLn $ unwords [show c, "has", show n, "parameters."]
return (apply u . genericDrop n, a)
inferHead (HeadCon _) = __IMPOSSIBLE__
inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)
inferDef mkTerm x =
traceCall (InferDef (getRange x) x) $ do
d <- instantiateDef =<< getConstInfo x
when (defRelevance d == Irrelevant) $ do
irr <- asks envIrrelevant
unless irr $ typeError $ DefinitionIsIrrelevant x
vs <- freeVarsToApply x
verboseS "tc.term.def" 10 $ do
ds <- mapM prettyTCM vs
dx <- prettyTCM x
dt <- prettyTCM $ defType d
liftIO $ LocIO.putStrLn $ "inferred def " ++ unwords (show dx : map show ds) ++ " : " ++ show dt
return (mkTerm x vs, defType d)
checkConstructorApplication :: A.Expr -> Type -> QName -> [NamedArg A.Expr] -> TCM Term
checkConstructorApplication org t c args = do
checkHead t args
where
checkHead t args = checkHeadApplication org t (HeadCon [c]) args
splitArgs [] args = ([], args)
splitArgs ps [] =
(map (const dummyUnderscore) ps, args)
splitArgs ps args@(Arg NotHidden _ _ : _) =
(map (const dummyUnderscore) ps, args)
splitArgs (p:ps) (arg : args)
| elem mname [Nothing, Just p] =
(arg :) *** id $ splitArgs ps args
| otherwise =
(dummyUnderscore :) *** id $ splitArgs ps (arg:args)
where
mname = nameOf (unArg arg)
dummyUnderscore = Arg Hidden Relevant (unnamed $ A.Underscore $ A.MetaInfo noRange emptyScopeInfo Nothing)
checkHeadApplication :: A.Expr -> Type -> A.Head -> [NamedArg A.Expr] -> TCM Term
checkHeadApplication e t hd args = do
replacing <- envReplace <$> ask
kit <- coinductionKit
if not replacing
then local (\e -> e { envReplace = True }) defaultResult
else case hd of
HeadCon [c] -> do
(f, t0) <- inferHead hd
reportSDoc "tc.term.con" 5 $ vcat
[ text "checkHeadApplication inferred" <+>
prettyTCM c <+> text ":" <+> prettyTCM t0
]
checkArguments' ExpandLast (getRange hd) args t0 t e $ \vs t1 cs -> do
TelV eTel eType <- telView t
TelV fTel fType <- telViewUpTo (size eTel) t1
blockTerm t (f vs) $ (cs ++) <$> do
when (size eTel > size fTel) $
compareTel CmpLeq eTel fTel >> return ()
reportSDoc "tc.term.con" 10 $ vcat
[ text "checking" <+>
prettyTCM fType <+> text "?<=" <+> prettyTCM eType
]
cs1 <- addCtxTel eTel $ leqType fType eType
cs2 <- compareTel CmpLeq eTel fTel
return $ cs1 ++ cs2
HeadDef c | Just c == (nameOfSharp <$> kit) -> do
lets <- envLetBindings <$> ask
unless (Map.null lets) $
typeError $ NotImplemented
"coinductive constructor in the scope of a let-bound variable"
i <- fresh :: TCM Integer
let name = filter (/= '_') (show $ A.qnameName c) ++ "-" ++ show i
c' <- liftM2 qualify currentModule (freshName_ name)
e' <- Def c' <$> getContextArgs
i <- currentMutualBlock
tel <- getContextTelescope
rel <- irrelevant <$> asks envIrrelevant
addConstant c' (Defn rel c' t (defaultDisplayForm c') i $ Axiom Nothing Nothing)
ctx <- getContext
let info = A.mkDefInfo (A.nameConcrete $ A.qnameName c') defaultFixity'
PublicAccess ConcreteDef noRange
pats = map (fmap $ \(n, _) -> Named Nothing (A.VarP n)) $
reverse ctx
clause = A.Clause (A.LHS (A.LHSRange noRange) c' pats [])
(A.RHS $ unAppView (A.Application hd args))
[]
reportSDoc "tc.term.expr.coind" 15 $ vcat $
[ text "The coinductive constructor application"
, nest 2 $ prettyTCM e
, text "was translated into the application"
, nest 2 $ prettyTCM e'
, text "and the function"
, nest 2 $ prettyTCM rel <> prettyTCM c' <+> text ":"
, nest 4 $ prettyTCM (telePi tel t)
, nest 2 $ prettyA clause <> text "."
]
local (\e -> e { envReplace = False }) $
escapeContext (size ctx) $ checkFunDef Delayed info c' [clause]
reportSDoc "tc.term.expr.coind" 15 $ do
def <- theDef <$> getConstInfo c'
text "The definition is" <+> text (show $ funDelayed def) <>
text "."
return e'
HeadCon _ -> __IMPOSSIBLE__
HeadVar {} -> defaultResult
HeadDef {} -> defaultResult
where
defaultResult = do
(f, t0) <- inferHead hd
checkArguments' ExpandLast (getRange hd) args t0 t e $ \vs t1 cs ->
blockTerm t (f vs) $ (cs ++) <$> leqType t1 t
data ExpandHidden = ExpandLast | DontExpandLast
instance Error Type where
strMsg _ = __IMPOSSIBLE__
noMsg = __IMPOSSIBLE__
traceCallE :: Error e => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM r
traceCallE call m = do
z <- lift $ traceCall call' $ runErrorT m
case z of
Right e -> return e
Left err -> throwError err
where
call' Nothing = call Nothing
call' (Just (Left _)) = call Nothing
call' (Just (Right x)) = call (Just x)
checkArguments :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type ->
ErrorT Type TCM (Args, Type, Constraints)
checkArguments DontExpandLast _ [] t0 t1 = return ([], t0, [])
checkArguments exh r [] t0 t1 =
traceCallE (CheckArguments r [] t0 t1) $ do
t0' <- lift $ reduce t0
t1' <- lift $ reduce t1
case funView $ unEl t0' of
FunV (Arg Hidden rel a) _ | notHPi $ unEl t1' -> do
v <- lift $ applyRelevanceToContext rel $ newValueMeta a
let arg = Arg Hidden rel v
(vs, t0'',cs) <- checkArguments exh r [] (piApply t0' [arg]) t1'
return (arg : vs, t0'',cs)
_ -> return ([], t0', [])
where
notHPi (Pi (Arg Hidden _ _) _) = False
notHPi (Fun (Arg Hidden _ _) _) = False
notHPi _ = True
checkArguments exh r args0@(Arg h _ e : args) t0 t1 =
traceCallE (CheckArguments r args0 t0 t1) $ do
t0b <- lift $ reduceB t0
case t0b of
Blocked{} -> throwError $ ignoreBlocking t0b
NotBlocked (El _ MetaV{}) -> throwError $ ignoreBlocking t0b
NotBlocked t0' -> do
e' <- return $ namedThing e
case (h, funView $ unEl t0') of
(NotHidden, FunV (Arg Hidden rel a) _) -> insertUnderscore rel
(Hidden, FunV (Arg Hidden rel a) _)
| not $ sameName (nameOf e) (nameInPi $ unEl t0') -> insertUnderscore rel
(_, FunV (Arg h' rel a) _) | h == h' -> do
u <- lift $ applyRelevanceToContext rel $ checkExpr e' a
let arg = Arg h rel u
(us, t0'', cs') <- checkArguments exh (fuseRange r e) args (piApply t0' [arg]) t1
return (nukeIfIrrelevant arg : us, t0'', cs')
where nukeIfIrrelevant arg =
if argRelevance arg == Irrelevant then
arg { unArg = DontCare }
else arg
(Hidden, FunV (Arg NotHidden _ _) _) ->
lift $ typeError $ WrongHidingInApplication t0'
_ -> lift $ typeError $ ShouldBePi t0'
where
insertUnderscore rel = do
scope <- lift $ getScope
let m = A.Underscore $ A.MetaInfo
{ A.metaRange = r
, A.metaScope = scope
, A.metaNumber = Nothing
}
checkArguments exh r (Arg Hidden rel (unnamed m) : args0) t0 t1
name (Named _ (A.Var x)) = show x
name (Named (Just x) _) = x
name _ = "x"
sameName Nothing _ = True
sameName n1 n2 = n1 == n2
nameInPi (Pi _ b) = Just $ absName b
nameInPi (Fun _ _) = Nothing
nameInPi _ = __IMPOSSIBLE__
checkArguments_ :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Telescope -> TCM (Args, Constraints)
checkArguments_ exh r args tel = do
z <- runErrorT $ checkArguments exh r args (telePi tel $ sort Prop) (sort Prop)
case z of
Right (args, _, cs) -> return (args, cs)
Left _ -> __IMPOSSIBLE__
inferExpr :: A.Expr -> TCM (Term, Type)
inferExpr e = do
t <- newTypeMeta_
v <- checkExpr e t
return (v,t)
checkLetBindings :: [A.LetBinding] -> TCM a -> TCM a
checkLetBindings = foldr (.) id . map checkLetBinding
checkLetBinding :: A.LetBinding -> TCM a -> TCM a
checkLetBinding b@(A.LetBind i rel x t e) ret =
traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
t <- isType_ t
v <- applyRelevanceToContext rel $ checkExpr e t
addLetBinding rel x v t ret
checkLetBinding (A.LetApply i x tel m args rd rm) ret = do
fv <- getModuleFreeVars =<< currentModule
n <- size <$> getContext
let new = n fv
reportSLn "tc.term.let.apply" 10 $ "Applying " ++ show m ++ " with " ++ show new ++ " free variables"
reportSDoc "tc.term.let.apply" 20 $ vcat
[ text "context =" <+> (prettyTCM =<< getContextTelescope)
, text "module =" <+> (prettyTCM =<< currentModule)
, text "fv =" <+> (text $ show fv)
]
checkSectionApplication i x tel m args rd rm
withAnonymousModule x new ret
checkLetBinding A.LetOpen{} ret = ret