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 Data.Traversable (traverse)
import Agda.Interaction.Options
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 qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Common
import Agda.Syntax.Translation.AbstractToConcrete
import Agda.Syntax.Concrete.Pretty
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.Syntax.Translation.InternalToAbstract (reify)
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.Irrelevance
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Quote
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Level
import Agda.TypeChecking.Rules.Builtin.Coinduction
import Agda.Utils.Fresh
import Agda.Utils.Tuple
import Agda.Utils.Permutation
import Agda.TypeChecking.Empty (isEmptyType)
import Agda.TypeChecking.Rules.Decl (checkSectionApplication)
import Agda.TypeChecking.Rules.Def (checkFunDef,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) $
case e of
A.Fun i a b -> do
a <- traverse isType_ a
b <- isType_ b
return $ El (sLub (getSort $ unArg a) (getSort b)) (Pi a (NoAbs "_" b))
A.Pi _ tel e -> do
checkTelescope_ tel $ \tel -> do
t <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
return $ telePi tel t
A.Set _ n -> do
n <- ifM typeInType (return 0) (return n)
return $ sort (mkType n)
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
n <- levelView =<< applyRelevanceToContext NonStrict
(checkExpr (namedThing l) (El (mkType 0) lvl))
return $ sort (Type n)
_ -> do
s <- workOnTypes $ newSortMeta
isType e s
isTypeEqualTo :: A.Expr -> Type -> TCM Type
isTypeEqualTo e t = case e of
A.ScopedExpr _ e -> isTypeEqualTo e t
A.Underscore i | A.metaNumber i == Nothing -> return t
e -> do
t' <- isType e (getSort t)
t' <$ leqType_ t t'
leqType_ :: Type -> Type -> TCM ()
leqType_ t t' = workOnTypes $ leqType t 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_ = checkTypedBindings PiNotLam
data LamOrPi = LamNotPi | PiNotLam deriving (Eq,Show)
checkTypedBindings :: LamOrPi -> A.TypedBindings -> (Telescope -> TCM a) -> TCM a
checkTypedBindings lamOrPi (A.TypedBindings i (Arg h rel b)) ret =
checkTypedBinding lamOrPi h rel b $ \bs ->
ret $ foldr (\(x,t) -> ExtendTel (Arg h rel t) . Abs x) EmptyTel bs
checkTypedBinding :: LamOrPi -> Hiding -> Relevance -> A.TypedBinding -> ([(String,Type)] -> TCM a) -> TCM a
checkTypedBinding lamOrPi h rel (A.TBind i xs e) ret = do
allowed <- optExperimentalIrrelevance <$> pragmaOptions
t <- modEnv lamOrPi allowed $ isType_ e
addCtxs xs (Arg h (modRel lamOrPi allowed rel) t) $ ret $ mkTel xs t
where
modEnv LamNotPi True = doWorkOnTypes
modEnv _ _ = id
modRel PiNotLam True = irrToNonStrict
modRel _ _ = id
mkTel [] t = []
mkTel (x:xs) t = (show $ nameConcrete x,t) : mkTel xs (raise 1 t)
checkTypedBinding lamOrPi h rel (A.TNoBind e) ret = do
t <- isType_ e
ret [("_",t)]
checkLambda :: Arg A.TypedBinding -> A.Expr -> Type -> TCM Term
checkLambda (Arg _ _ A.TNoBind{}) _ _ = __IMPOSSIBLE__
checkLambda (Arg h r (A.TBind _ xs typ)) body target = do
TelV tel btyp <- telViewUpTo (length xs) target
if size tel < size xs || length xs /= 1
then dontUseTargetType
else useTargetType tel btyp
where
dontUseTargetType = do
verboseS "tc.term.lambda" 5 $ tick "lambda-no-target-type"
argsT <- workOnTypes $ Arg h r <$> isType_ typ
t1 <- addCtxs xs argsT $ workOnTypes newTypeMeta_
let tel = telFromList $ mkTel xs argsT
pid <- newProblem_ $ leqType (telePi tel t1) target
v <- addCtxs xs argsT $ checkExpr body t1
blockTermOnProblem target (teleLam tel v) pid
useTargetType tel@(ExtendTel arg (Abs _ EmptyTel)) btyp = do
verboseS "tc.term.lambda" 5 $ tick "lambda-with-target-type"
unless (argHiding arg == h) $ typeError $ WrongHidingInLambda target
let r' = argRelevance arg
when (r == Irrelevant && r' /= r) $ typeError $ WrongIrrelevanceInLambda target
(pid, argT) <- newProblem $ isTypeEqualTo typ (unArg arg)
v <- addCtx x (Arg h r' argT) $ checkExpr body btyp
blockTermOnProblem target (Lam h $ Abs (show $ nameConcrete x) v) pid
where
[x] = xs
useTargetType _ _ = __IMPOSSIBLE__
mkTel [] t = []
mkTel (x : xs) t = ((,) s <$> t) : mkTel xs (raise 1 t)
where s = show $ nameConcrete x
checkLiteral :: Literal -> Type -> TCM Term
checkLiteral lit t = do
t' <- litType lit
blockTerm t $ Lit lit <$ leqType_ t' t
litType :: Literal -> TCM Type
litType l = case l of
LitInt _ _ -> el <$> primNat
LitFloat _ _ -> el <$> primFloat
LitChar _ _ -> el <$> primChar
LitString _ _ -> el <$> primString
LitQName _ _ -> el <$> primQName
where
el t = El (mkType 0) t
reduceCon :: 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 -> 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) -> k vs t1
Left t0 -> postponeTypeCheckingProblem e t (unblockedTester t0)
unScope (A.ScopedExpr scope e) = unScope e
unScope e = e
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)
]
reportSDoc "tc.term.expr.top.detailed" 80 $
text "Checking" <+> fsep [ prettyTCM e, text ":", text (show t) ]
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
_ | Pi (Arg h rel _) _ <- unEl t
, not (hiddenLambdaOrHole h e)
, h /= NotHidden -> do
x <- freshName r (argName t)
reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda"
checkExpr (A.Lam (A.ExprRange $ getRange e) (domainFree h rel x) e) t
where
r = case rStart $ getRange e of
Nothing -> noRange
Just pos -> posToRange pos pos
hiddenLambdaOrHole h (A.AbsurdLam _ h') | h == h' = True
hiddenLambdaOrHole h (A.ExtendedLam _ _ _ []) = False
hiddenLambdaOrHole h (A.ExtendedLam _ _ _ cls) = any hiddenLHS cls
hiddenLambdaOrHole h (A.Lam _ (A.DomainFree h' _ _) _) | h == h' = True
hiddenLambdaOrHole h (A.Lam _ (A.DomainFull (A.TypedBindings _ (Arg h' _ _))) _)
| h == h' = True
hiddenLambdaOrHole _ (A.QuestionMark _) = True
hiddenLambdaOrHole _ _ = False
hiddenLHS (A.Clause (A.LHS _ _ (a : _) _) _ _) = elem (argHiding a) [Hidden, Instance]
hiddenLHS _ = False
A.QuestionMark i -> checkMeta newQuestionMark t i
A.Underscore i -> checkMeta newValueMeta t i
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
n <- levelView =<< applyRelevanceToContext NonStrict
(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 $ sSuc $ Type 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.QuoteTerm _ <- unScope q ->
do (et, _) <- inferExpr (namedThing e)
q <- quoteTerm =<< normalise et
ty <- el primAgdaTerm
blockTerm t $ q <$ leqType_ ty t
| A.Unquote _ <- unScope q ->
do e1 <- checkExpr (namedThing e) =<< el primAgdaTerm
e2 <- unquote e1
checkTerm e2 t
A.Quote _ -> typeError $ GenericError "quote must be applied to a defined name"
A.QuoteTerm _ -> typeError $ GenericError "quoteTerm must be applied to a term"
A.Unquote _ -> typeError $ GenericError "unquote must be applied to a term"
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 unEl t' of
Pi (Arg h' _ a) _
| h == h' && not (null $ foldTerm metas a) ->
postponeTypeCheckingProblem e (ignoreBlocking t) $
null . foldTerm metas <$> instantiateFull a
| h == h' -> blockTerm t' $ do
isEmptyType a
top <- currentModule
let name = "absurd"
aux <- qualify top <$> freshName (getRange i) name
rel <- asks envRelevance
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 noCompiledRep
$ Function
{ funClauses =
[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
, funStatic = False
}
return (Def aux [])
| otherwise -> typeError $ WrongHidingInLambda t'
_ -> typeError $ ShouldBePi t'
where
metas (MetaV m _) = [m]
metas _ = []
A.ExtendedLam i di qname cs -> do
t <- reduceB =<< instantiateFull t
case t of
Blocked{} -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
NotBlocked (El _ MetaV{}) -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
NotBlocked t -> do
j <- currentMutualBlock
rel <- asks envRelevance
addConstant qname (Defn rel qname t (defaultDisplayForm qname) j noCompiledRep Axiom)
reportSDoc "tc.term.exlam" 50 $ text "extended lambda's implementation \"" <> prettyTCM qname <>
text "\" has type: " $$ prettyTCM t
abstract (A.defAbstract di) $ checkFunDef' t rel NotDelayed di qname cs
tel <- getContextTelescope
addExtLambdaTele qname (counthidden tel , countnothidden tel)
reduce $ (Def qname [] `apply` (mkArgs tel))
where
abstract ConcreteDef = inConcreteMode
abstract AbstractDef = inAbstractMode
mkArgs :: Telescope -> Args
mkArgs tel = map arg [n 1, n 2..0]
where
n = size tel
arg i = defaultArg (Var i [])
metas (MetaV m _) = [m]
metas _ = []
counthidden :: Telescope -> Int
counthidden t = length $ filter (\ (Arg h r a) -> h == Hidden ) $ teleArgs t
countnothidden :: Telescope -> Int
countnothidden t = length $ filter (\ (Arg h r a) -> h == NotHidden ) $ teleArgs t
A.Lam i (A.DomainFull (A.TypedBindings _ b)) e -> checkLambda b e t
A.Lam i (A.DomainFree h rel x) e0 -> checkExpr (A.Lam i (domainFree h rel x) e0) 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
let s = 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
s <- reduce $ getSort a' `sLub` getSort b'
blockTerm t $ Pi (Arg h r a') (NoAbs "_" 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 arg x e =
case [ a | a <- axs, unArg a == x ] of
[a] -> unnamed e <$ a
_ -> defaultArg $ unnamed e
let meta = A.Underscore $ A.MetaInfo (getRange e) scope Nothing
missingExplicits = [ (unArg a, [unnamed meta <$ a])
| a <- axs, argHiding a == NotHidden
, notElem (unArg a) (map fst fs) ]
es <- concat <$> orderFields r [] xs ([ (x, [arg x e]) | (x, e) <- fs ] ++
missingExplicits)
let tel = ftel `apply` vs
args <- checkArguments_ ExpandLast (getRange e)
es
tel
return $ Con con args
MetaV _ _ -> do
let fields = map fst fs
rs <- findPossibleRecords fields
case rs of
[] -> case fs of
[] -> typeError $ GenericError "There are no records in scope"
[(f, _)] -> typeError $ GenericError $ "There is no known record with the field " ++ show f
_ -> typeError $ GenericError $ "There is no known record with the fields " ++ unwords (map show fields)
[r] -> do
def <- getConstInfo r
vs <- newArgsMeta (defType def)
let target = piApply (defType def) vs
s = case unEl target of
Level l -> Type l
Sort s -> s
_ -> __IMPOSSIBLE__
inferred = El s $ Def r vs
v <- checkExpr e inferred
blockTerm t $ v <$ leqType_ t inferred
_:_:_ -> 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.RecUpdate ei recexpr fs -> do
case unEl t of
Def r vs -> do
rec <- checkExpr recexpr t
name <- freshNoName (getRange recexpr)
addLetBinding Relevant name rec t $ do
projs <- recFields <$> getRecordDef r
axs <- getRecordFieldNames r
scope <- getScope
let xs = map unArg axs
es <- orderFields r Nothing xs $ map (\(x, e) -> (x, Just e)) fs
let es' = zipWith (replaceFields name ei) projs es
checkExpr (A.Rec ei [ (x, e) | (x, Just e) <- zip xs es' ]) t
MetaV _ _ -> do
inferred <- inferExpr recexpr >>= reduce . snd
case unEl inferred of
MetaV _ _ -> postponeTypeCheckingProblem_ e t
_ -> do
v <- checkExpr e inferred
blockTerm t $ v <$ leqType_ t inferred
_ -> typeError $ ShouldBeRecordType t
where
replaceFields :: Name -> A.ExprInfo -> Arg A.QName -> Maybe A.Expr -> Maybe A.Expr
replaceFields n ei (Arg NotHidden _ p) Nothing = Just $ A.App ei (A.Def p) $ defaultArg (unnamed $ A.Var n)
replaceFields _ _ (Arg _ _ _) Nothing = Nothing
replaceFields _ _ _ (Just e) = Just $ e
A.DontCare e ->
checkExpr e t
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 <- quoteTerm (unEl t')
tmType <- agdaTermType
(v, ty) <- addLetBinding Relevant x quoted tmType (inferExpr e)
blockTerm t' $ v <$ leqType_ ty t'
A.ETel _ -> __IMPOSSIBLE__
_ | Application (A.Con (AmbQ 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 [])
cs -> typeError $ GenericError $
"Can't resolve overloaded constructors targeting the same datatype (" ++ show d ++
"): " ++ unwords (map show cs)
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 (A.Con (AmbQ [c])) args <- appView e ->
checkConstructorApplication e t c args
| Application hd args <- appView e ->
checkHeadApplication e t hd args
domainFree h rel x =
A.DomainFull $ A.TypedBindings r $ Arg h rel $ A.TBind r [x] $ A.Underscore info
where
r = getRange x
info = A.MetaInfo{ A.metaRange = r, A.metaScope = emptyScopeInfo, A.metaNumber = Nothing }
checkMeta :: (Type -> TCM Term) -> Type -> A.MetaInfo -> TCM Term
checkMeta newMeta t i = do
case A.metaNumber i of
Nothing -> do
setScope (A.metaScope i)
newMeta t
Just n -> do
let v = MetaV (MetaId n) []
t' <- jMetaType . mvJudgement <$> lookupMeta (MetaId n)
blockTerm t $ v <$ leqType t' t
inferMeta :: (Type -> TCM Term) -> A.MetaInfo -> TCM (Args -> Term, Type)
inferMeta newMeta i =
case A.metaNumber i of
Nothing -> do
setScope (A.metaScope i)
t <- workOnTypes $ newTypeMeta_
v <- newMeta t
return (apply v, t)
Just n -> do
let v = MetaV (MetaId n)
t' <- jMetaType . mvJudgement <$> lookupMeta (MetaId n)
return (v, t')
inferHead :: A.Expr -> TCM (Args -> Term, Type)
inferHead (A.Var x) = do
(u, a) <- getVarInfo x
when (unusableRelevance $ argRelevance a) $
typeError $ VariableIsIrrelevant x
return (apply u, unArg a)
inferHead (A.Def x) = do
proj <- isProjection x
case proj of
Nothing -> do
(u, a) <- inferDef Def x
return (apply u, a)
Just{} -> do
Just (r, n) <- funProjection . theDef <$> getConstInfo x
cxt <- size <$> freeVarsToApply x
m <- getDefFreeVars x
reportSDoc "tc.term.proj" 10 $ sep
[ text "building projection" <+> prettyTCM x
, nest 2 $ parens (text "ctx =" <+> text (show cxt))
, nest 2 $ parens (text "n =" <+> text (show n))
, nest 2 $ parens (text "m =" <+> text (show m)) ]
let hs | n == 0 = __IMPOSSIBLE__
| otherwise = genericReplicate (n 1) NotHidden
names = [ s ++ [c] | s <- "" : names, c <- ['a'..'z'] ]
eta = foldr (\(h, s) -> Lam h . NoAbs s) (Def x []) (zip hs names)
(u, a) <- inferDef (\f vs -> eta `apply` vs) x
return (apply u, a)
inferHead (A.Con (AmbQ [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 (A.Con _) = __IMPOSSIBLE__
inferHead (A.QuestionMark i) = inferMeta newQuestionMark i
inferHead (A.Underscore i) = inferMeta newValueMeta i
inferHead e = do (term, t) <- inferExpr e
return (apply term, t)
inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)
inferDef mkTerm x =
traceCall (InferDef (getRange x) x) $ do
d <- instantiateDef =<< getConstInfo x
let drel = defRelevance d
when (drel /= Relevant) $ do
rel <- asks envRelevance
reportSDoc "tc.irr" 50 $ vcat
[ text "declaration relevance =" <+> text (show drel)
, text "context relevance =" <+> text (show rel)
]
unless (drel `moreRelevant` rel) $ 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
| hiddenArg = fallback
| otherwise = do
cdef <- getConstInfo c
let Constructor{conData = d} = theDef cdef
case unEl t of
Def d' vs | d' == d -> do
def <- theDef <$> getConstInfo d
let npars = case def of
Datatype{ dataPars = n } -> Just n
Record{ recPars = n } -> Just n
_ -> Nothing
flip (maybe fallback) npars $ \n -> do
let ps = genericTake n vs
ctype = defType cdef
reportSDoc "tc.term.con" 20 $ vcat
[ text "special checking of constructor application of" <+> prettyTCM c
, nest 2 $ vcat [ text "ps =" <+> prettyTCM ps
, text "ctype =" <+> prettyTCM ctype ] ]
let ctype' = ctype `piApply` ps
reportSDoc "tc.term.con" 20 $ nest 2 $ text "ctype' =" <+> prettyTCM ctype'
checkArguments' ExpandLast (getRange c) args ctype' t org $ \us t' -> do
reportSDoc "tc.term.con" 20 $ nest 2 $ vcat
[ text "us =" <+> prettyTCM us
, text "t' =" <+> prettyTCM t' ]
blockTerm t $ Con c us <$ leqType_ t' t
_ -> fallback
where
fallback = checkHeadApplication org t (A.Con (AmbQ [c])) args
hiddenArg = case args of
Arg Hidden _ _ : _ -> True
_ -> False
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.Expr -> [NamedArg A.Expr] -> TCM Term
checkHeadApplication e t hd args = do
kit <- coinductionKit
case hd of
A.Con (AmbQ [c]) | Just c == (nameOfSharp <$> kit) -> do
defaultResult
A.Con (AmbQ [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 -> do
TelV eTel eType <- telView t
TelV fTel fType <- telViewUpTo (size eTel) t1
when (size eTel > size fTel) $
typeError $ UnequalTypes CmpLeq t1 t
reportSDoc "tc.term.con" 10 $ vcat
[ text "checking" <+>
prettyTCM fType <+> text "?<=" <+> prettyTCM eType
]
blockTerm t $ f vs <$ workOnTypes (do
addCtxTel eTel $ leqType fType eType
compareTel t t1 CmpLeq eTel fTel)
(A.Def 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 (killRange <$> currentModule) (freshName_ name)
e' <- Def c' <$> getContextArgs
i <- currentMutualBlock
tel <- getContextTelescope
rel <- asks envRelevance
addConstant c' (Defn rel c' t (defaultDisplayForm c') i noCompiledRep $ Axiom)
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 (A.Con (AmbQ [c])) 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 "."
]
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'
A.Con _ -> __IMPOSSIBLE__
_ -> defaultResult
where
defaultResult = do
(f, t0) <- inferHead hd
checkArguments' ExpandLast (getRange hd) args t0 t e $ \vs t1 ->
blockTerm t $ f vs <$ 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)
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 unEl t0' of
Pi (Arg Hidden rel a) _ | notHPi Hidden $ unEl t1' -> do
v <- lift $ applyRelevanceToContext rel $ newValueMeta a
let arg = Arg Hidden rel v
(vs, t0'') <- checkArguments exh r [] (piApply t0' [arg]) t1'
return (arg : vs, t0'')
Pi (Arg Instance rel a) _ | notHPi Instance $ unEl t1' -> do
lift $ reportSLn "tc.term.args.ifs" 15 $ "inserting implicit meta for type " ++ show a
v <- lift $ applyRelevanceToContext rel $ newIFSMeta a
let arg = Arg Instance rel v
(vs, t0'') <- checkArguments exh r [] (piApply t0' [arg]) t1'
return (arg : vs, t0'')
_ -> return ([], t0')
where
notHPi h (Pi (Arg h' _ _) _) | h == h' = 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 unEl t0' of
Pi (Arg h' rel a) _ |
h == h' && (h == NotHidden || sameName (nameOf e) (nameInPi $ unEl t0')) -> do
u <- lift $ applyRelevanceToContext rel $ checkExpr e' a
let arg = Arg h rel u
(us, t0'') <- checkArguments exh (fuseRange r e) args (piApply t0' [arg]) t1
return (nukeIfIrrelevant arg : us, t0'')
where nukeIfIrrelevant arg =
if argRelevance arg == Irrelevant then
arg { unArg = DontCare $ unArg arg }
else arg
Pi (Arg Instance rel a) _ -> insertIFSUnderscore rel a
Pi (Arg Hidden rel a) _ -> insertUnderscore rel
Pi (Arg NotHidden _ _) _ -> lift $ typeError $ WrongHidingInApplication t0'
_ -> lift $ typeError $ ShouldBePi t0'
where
insertIFSUnderscore rel a = do v <- lift $ applyRelevanceToContext rel $ newIFSMeta a
lift $ reportSLn "tc.term.args.ifs" 15 $ "inserting implicit meta (2) for type " ++ show a
let arg = Arg Instance rel v
(vs, t0'') <- checkArguments exh r args0 (piApply t0 [arg]) t1
return (arg : vs, t0'')
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 _ = __IMPOSSIBLE__
checkArguments_ :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Telescope -> TCM Args
checkArguments_ exh r args tel = do
z <- runErrorT $ checkArguments exh r args (telePi tel $ sort Prop) (sort Prop)
case z of
Right (args, _) -> return args
Left _ -> __IMPOSSIBLE__
inferExpr :: A.Expr -> TCM (Term, Type)
inferExpr e = do
t <- workOnTypes $ newTypeMeta_
v <- checkExpr e t
return (v,t)
checkTerm :: Term -> Type -> TCM Term
checkTerm tm ty = do atm <- reify tm
checkExpr atm ty
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 modapp rd rm) ret = do
fv <- getModuleFreeVars =<< currentModule
n <- size <$> getContext
let new = n fv
reportSLn "tc.term.let.apply" 10 $ "Applying " ++ show modapp ++ " 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 modapp rd rm
withAnonymousModule x new ret
checkLetBinding A.LetOpen{} ret = ret