module Agda.TypeChecking.Rules.Term where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Arrow ((&&&), (***), first, second)
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Control.Monad.State (get, put)
import Control.Monad.Reader
import Data.Maybe
import Data.Either (partitionEithers)
import Data.Monoid (mappend)
import Data.List hiding (sort, null)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Traversable (sequenceA)
import Data.Void
import Agda.Interaction.Options
import Agda.Interaction.Highlighting.Generate (storeDisambiguatedName)
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, exprFieldA)
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.Syntax.Literal
import qualified Agda.Syntax.Reflected as R
import Agda.Syntax.Scope.Base ( ThingsInScope, AbstractName
, emptyScopeInfo
, exportedNamesInScope)
import Agda.Syntax.Scope.Monad (getNamedScope)
import Agda.Syntax.Translation.InternalToAbstract (reify)
import Agda.Syntax.Translation.ReflectedToAbstract (toAbstract_)
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Free (isBinderUsed)
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.InstanceArguments
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
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.Unquote
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.LHS
import Agda.TypeChecking.Empty (isEmptyType)
import Agda.TypeChecking.Rules.Decl (checkSectionApplication)
import Agda.TypeChecking.Rules.Def (checkFunDef, checkFunDef', useTerPragma)
import Agda.Utils.Except
( Error(noMsg, strMsg)
, ExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List (groupOn)
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Tuple
#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) $ sharedType =<< do
let fallback = isType e =<< do workOnTypes $ newSortMeta
case unScope e of
A.Fun i (Arg info t) b -> do
a <- Dom info <$> isType_ t
b <- isType_ b
s <- ptsRule a b
let t' = El s $ Pi a $ NoAbs underscore b
noFunctionsIntoSize b t'
return t'
A.Pi _ tel e | null tel -> isType_ e
A.Pi _ tel e -> do
(t0, t') <- checkPiTelescope tel $ \ tel -> do
t0 <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
return (t0, telePi tel t0)
noFunctionsIntoSize t0 t'
return t'
A.Set _ n -> do
return $ sort (mkType n)
A.App i s arg
| getHiding arg == NotHidden,
A.Set _ 0 <- unScope s ->
ifNotM hasUniversePolymorphism
(typeError $ GenericError "Use --universe-polymorphism to enable level arguments to Set")
$ do
lvl <- levelType
n <- levelView =<< do
applyRelevanceToContext NonStrict $
checkNamedArg arg lvl
return $ sort (Type n)
A.QuestionMark minfo ii -> caseMaybeM (lookupInteractionMeta ii) fallback $ \ x -> do
reportSDoc "tc.ip" 20 $ fsep
[ text "Rechecking meta "
, prettyTCM x
, text $ " for interaction point " ++ show ii
]
mv <- lookupMeta x
let s0 = jMetaType . mvJudgement $ mv
let n = length . envContext . clEnv . miClosRange . mvInfo $ mv
(vs, rest) <- splitAt n <$> getContextArgs
reportSDoc "tc.ip" 20 $ vcat
[ text " s0 = " <+> prettyTCM s0
, text " vs = " <+> prettyTCM vs
, text " rest = " <+> prettyTCM rest
]
if (length vs /= n) then fallback else do
s1 <- piApplyM s0 vs
case ignoreSharing $ unEl s1 of
Sort s -> return $ El s $ MetaV x $ map Apply vs
_ -> __IMPOSSIBLE__
_ -> fallback
ptsRule :: (LensSort a, LensSort b) => a -> b -> TCM Sort
ptsRule a b = pts <$> reduce (getSort a) <*> reduce (getSort b)
noFunctionsIntoSize :: Type -> Type -> TCM ()
noFunctionsIntoSize t tBlame = do
reportSDoc "tc.fun" 20 $ do
let El s (Pi dom b) = ignoreSharing <$> tBlame
sep [ text "created function type " <+> prettyTCM tBlame
, text "with pts rule" <+> prettyTCM (getSort dom, getSort b, s)
]
s <- reduce $ getSort t
when (s == SizeUniv) $ do
typeError $ FunctionTypeInSizeUniv $ unEl tBlame
isTypeEqualTo :: A.Expr -> Type -> TCM Type
isTypeEqualTo e0 t = scopedExpr e0 >>= \case
A.ScopedExpr{} -> __IMPOSSIBLE__
A.Underscore i | A.metaNumber i == Nothing -> return t
e -> workOnTypes $ 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 = checkTelescope' LamNotPi
checkPiTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a
checkPiTelescope = checkTelescope' PiNotLam
data LamOrPi
= LamNotPi
| PiNotLam
deriving (Eq, Show)
checkTelescope' :: LamOrPi -> A.Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope' lamOrPi [] ret = ret EmptyTel
checkTelescope' lamOrPi (b : tel) ret =
checkTypedBindings lamOrPi b $ \tel1 ->
checkTelescope' lamOrPi tel $ \tel2 ->
ret $ abstract tel1 tel2
checkTypedBindings :: LamOrPi -> A.TypedBindings -> (Telescope -> TCM a) -> TCM a
checkTypedBindings lamOrPi (A.TypedBindings i (Arg info b)) ret =
checkTypedBinding lamOrPi info b $ \ bs ->
ret $ telFromList bs
checkTypedBinding :: LamOrPi -> ArgInfo -> A.TypedBinding -> (ListTel -> TCM a) -> TCM a
checkTypedBinding lamOrPi info (A.TBind i xs e) ret = do
experimental <- optExperimentalIrrelevance <$> pragmaOptions
t <- modEnv lamOrPi $ isType_ e
let info' = mapRelevance (modRel lamOrPi experimental) info
addContext' (xs, Dom info' t) $
ret $ bindsWithHidingToTel xs (Dom info t)
where
modEnv LamNotPi = workOnTypes
modEnv _ = id
modRel PiNotLam xp = if xp then irrToNonStrict else nonStrictToRel
modRel _ _ = id
checkTypedBinding lamOrPi info (A.TLet _ lbs) ret = do
checkLetBindings lbs (ret [])
checkLambda :: Arg A.TypedBinding -> A.Expr -> Type -> TCM Term
checkLambda (Arg _ (A.TLet _ lbs)) body target =
checkLetBindings lbs (checkExpr body target)
checkLambda (Arg info (A.TBind _ xs typ)) body target = do
reportSLn "tc.term.lambda" 60 $ "checkLambda xs = " ++ show xs
let numbinds = length xs
TelV tel btyp <- telViewUpTo numbinds target
if size tel < numbinds || numbinds /= 1
then dontUseTargetType
else useTargetType tel btyp
where
dontUseTargetType = do
verboseS "tc.term.lambda" 5 $ tick "lambda-no-target-type"
argsT <- workOnTypes $ Dom info <$> isType_ typ
checkSizeLtSat $ unEl $ unDom argsT
let tel = telFromList $ bindsWithHidingToTel xs argsT
reportSLn "tc.term.lambda" 60 $ "dontUseTargetType tel = " ++ show tel
t1 <- addContext (xs, argsT) $ workOnTypes newTypeMeta_
if notVisible info || any notVisible xs then do
pid <- newProblem_ $ leqType (telePi tel t1) target
v <- addContext' (xs, argsT) $ checkExpr body t1
blockTermOnProblem target (teleLam tel v) pid
else do
v <- addContext' (xs, argsT) $ checkExpr body t1
coerce (teleLam tel v) (telePi tel t1) target
useTargetType tel@(ExtendTel arg (Abs y EmptyTel)) btyp = do
verboseS "tc.term.lambda" 5 $ tick "lambda-with-target-type"
reportSLn "tc.term.lambda" 60 $ "useTargetType y = " ++ show y
info <- return $ mapHiding (mappend h) info
unless (getHiding arg == getHiding info) $ typeError $ WrongHidingInLambda target
let r = getRelevance info
r' = getRelevance arg
when (r == Irrelevant && r' /= r) $ typeError $ WrongIrrelevanceInLambda target
let a = unDom arg
checkSizeLtSat $ unEl a
(pid, argT) <- newProblem $ isTypeEqualTo typ a
v <- add (notInScopeName y) (Dom (setRelevance r' info) argT) $ checkExpr body btyp
blockTermOnProblem target (Lam info $ Abs (nameToArgName x) v) pid
where
[WithHiding h x] = xs
add y dom | isNoName x = addContext' (y, dom)
| otherwise = addContext' (x, dom)
useTargetType _ _ = __IMPOSSIBLE__
checkPostponedLambda :: Arg ([WithHiding Name], Maybe Type) -> A.Expr -> Type -> TCM Term
checkPostponedLambda args@(Arg _ ([] , _ )) body target = do
checkExpr body target
checkPostponedLambda args@(Arg info (WithHiding h x : xs, mt)) body target = do
let postpone _ t = postponeTypeCheckingProblem_ $ CheckLambda args body t
lamHiding = mappend h $ getHiding info
insertHiddenLambdas lamHiding target postpone $ \ t@(El _ (Pi dom b)) -> do
let r = getRelevance info
r' = getRelevance dom
info' = setHiding lamHiding $ setRelevance r' info
when (r == Irrelevant && r' /= r) $
typeError $ WrongIrrelevanceInLambda target
mpid <- caseMaybe mt (return Nothing) $ \ ascribedType -> Just <$> do
newProblem_ $ leqType (unDom dom) ascribedType
let add dom | isNoName x = addContext (absName b, dom)
| otherwise = addContext (x, dom)
v <- add (maybe dom (dom $>) mt) $
checkPostponedLambda (Arg info (xs, mt)) body $ absBody b
let v' = Lam info' $ Abs (nameToArgName x) v
maybe (return v') (blockTermOnProblem t v') mpid
insertHiddenLambdas
:: Hiding
-> Type
-> (MetaId -> Type -> TCM Term)
-> (Type -> TCM Term)
-> TCM Term
insertHiddenLambdas h target postpone ret = do
ifBlockedType target postpone $ \ t0 -> do
let t = ignoreSharing <$> t0
case unEl t of
Pi dom b -> do
let h' = getHiding dom
if h == h' then ret t else do
if visible h' then typeError $ WrongHidingInLambda target else do
let x = absName b
Lam (domInfo dom) . Abs x <$> do
addContext' (x, dom) $ insertHiddenLambdas h (absBody b) postpone ret
_ -> typeError . GenericDocError =<< do
text "Expected " <+> prettyTCM target <+> text " to be a function type"
checkAbsurdLambda :: A.ExprInfo -> Hiding -> A.Expr -> Type -> TCM Term
checkAbsurdLambda i h e t = do
t <- instantiateFull t
ifBlockedType t (\ m t' -> postponeTypeCheckingProblem_ $ CheckExpr e t') $ \ t' -> do
case ignoreSharing $ unEl t' of
Pi dom@(Dom info' a) b
| h /= getHiding info' -> typeError $ WrongHidingInLambda t'
| not (null $ allMetas a) ->
postponeTypeCheckingProblem (CheckExpr e t') $
null . allMetas <$> instantiateFull a
| otherwise -> blockTerm t' $ do
isEmptyType (getRange i) a
top <- currentModule
aux <- qualify top <$> freshName_ (getRange i, absurdLambdaName)
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 $
(\ d -> (defaultDefn (setRelevance rel info') aux t' d)
{ defPolarity = [Nonvariant]
, defArgOccurrences = [Unused] })
$ emptyFunction
{ funClauses =
[Clause
{ clauseRange = getRange e
, clauseTel = telFromList [fmap ("()",) dom]
, namedClausePats = [Arg info' $ Named (Just $ unranged $ absName b) $ debruijnNamedVar "()" 0]
, clauseBody = Nothing
, clauseType = Just $ setRelevance rel $ defaultArg $ absBody b
, clauseCatchall = False
}
]
, funCompiled = Just Fail
, funTerminates = Just True
}
tel <- getContextTelescope
return $ Def aux $ map Apply $ teleArgs tel
_ -> typeError $ ShouldBePi t'
checkExtendedLambda :: A.ExprInfo -> A.DefInfo -> QName -> [A.Clause] ->
A.Expr -> Type -> TCM Term
checkExtendedLambda i di qname cs e t = do
solveSizeConstraints DontDefaultToInfty
t <- instantiateFull t
ifBlockedType t (\ m t' -> postponeTypeCheckingProblem_ $ CheckExpr e t') $ \ t -> do
j <- currentOrFreshMutualBlock
rel <- asks envRelevance
let info = setRelevance rel defaultArgInfo
st <- get
addConstant qname =<< do
useTerPragma $
(defaultDefn info qname t emptyFunction) { defMutual = j }
reportSDoc "tc.term.exlam" 20 $
text (show $ A.defAbstract di) <+>
text "extended lambda's implementation \"" <> prettyTCM qname <>
text "\" has type: " $$ prettyTCM t
args <- getContextArgs
freevars <- getCurrentModuleFreeVars
let argsNoParam = genericDrop freevars args
let (hid, notHid) = partition notVisible argsNoParam
reportSDoc "tc.term.exlam" 30 $ vcat $
[ text "dropped args: " <+> prettyTCM (take freevars args)
, text "hidden args: " <+> prettyTCM hid
, text "visible args: " <+> prettyTCM notHid
]
mx <- catchIlltypedPatternBlockedOnMeta $ abstract (A.defAbstract di) $
checkFunDef' t info NotDelayed (Just $ ExtLamInfo (length hid) (length notHid)) Nothing di qname cs
case mx of
Nothing -> return $ Def qname $ map Apply args
Just (err, x) -> do
put st
mm <- Map.lookup x <$> getMetaStore
case mvInstantiation <$> mm of
Nothing -> do
throwError err
Just InstV{} -> __IMPOSSIBLE__
Just{} -> do
postponeTypeCheckingProblem (CheckExpr e t) $ isInstantiatedMeta x
where
abstract ConcreteDef = inConcreteMode
abstract AbstractDef = inAbstractMode
catchIlltypedPatternBlockedOnMeta :: TCM () -> TCM (Maybe (TCErr, MetaId))
catchIlltypedPatternBlockedOnMeta m = (Nothing <$ do disableDestructiveUpdate m)
`catchError` \ err -> do
let reraise = throwError err
case err of
TypeError s cl@Closure{ clValue = IlltypedPattern p a } -> do
mx <- localState $ do
put s
enterClosure cl $ \ _ -> do
ifBlockedType a (\ x _ -> return $ Just x) $ \ _ -> return Nothing
caseMaybe mx reraise $ \ x -> return $ Just (err, x)
_ -> reraise
expandModuleAssigns :: [Either A.Assign A.ModuleName] -> [C.Name] -> TCM A.Assigns
expandModuleAssigns mfs exs = do
let (fs , ms) = partitionEithers mfs
exs' = exs \\ map (view nameFieldA) fs
fs' <- forM exs' $ \ f -> do
pms <- forM ms $ \ m -> do
modScope <- getNamedScope m
let names :: ThingsInScope AbstractName
names = exportedNamesInScope modScope
return $
case Map.lookup f names of
Just [n] -> Just (m, FieldAssignment f (A.nameExpr n))
_ -> Nothing
case catMaybes pms of
[] -> return Nothing
[(_, fa)] -> return (Just fa)
mfas -> typeError $ GenericError $ "Ambiguity: the field " ++ show f ++ " appears in the following modules " ++ show (map fst mfas)
return (fs ++ catMaybes fs')
checkRecordExpression :: A.RecordAssigns -> A.Expr -> Type -> TCM Term
checkRecordExpression mfs e t = do
reportSDoc "tc.term.rec" 10 $ sep
[ text "checking record expression"
, prettyA e
]
ifBlockedType t (\ _ t -> guessRecordType t) $ \ t -> do
case ignoreSharing $ unEl t of
Def r es -> do
let ~(Just vs) = allApplyElims es
reportSDoc "tc.term.rec" 20 $ text $ " r = " ++ show r
reportSDoc "tc.term.rec" 30 $ text " xs = " <> do
text =<< show . map unArg <$> getRecordFieldNames r
reportSDoc "tc.term.rec" 30 $ text " ftel= " <> do
prettyTCM =<< getRecordFieldTypes r
reportSDoc "tc.term.rec" 30 $ text " con = " <> do
text =<< show <$> getRecordConstructor r
def <- getRecordDef r
let
axs = recordFieldNames def
exs = filter notHidden axs
xs = map unArg axs
con = killRange $ recConHead def
reportSDoc "tc.term.rec" 20 $ vcat
[ text $ " xs = " ++ show xs
, text " ftel= " <> prettyTCM (recTel def)
, text $ " con = " ++ show con
]
fs <- expandModuleAssigns mfs (map unArg exs)
scope <- getScope
let re = getRange e
meta x = A.Underscore $ A.MetaInfo re scope Nothing (show x)
es <- insertMissingFields r meta fs axs
args <- checkArguments_ ExpandLast re es (recTel def `apply` vs) >>= \case
(args, remainingTel) | null remainingTel -> return args
_ -> __IMPOSSIBLE__
reportSDoc "tc.term.rec" 20 $ text $ "finished record expression"
return $ Con con ConORec args
_ -> typeError $ ShouldBeRecordType t
where
guessRecordType t = do
let fields = [ x | Left (FieldAssignment x _) <- mfs ]
rs <- findPossibleRecords fields
case rs of
[] -> case fields 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
let rt = defType def
vs <- newArgsMeta rt
target <- reduce $ piApply rt vs
s <- case ignoreSharing $ unEl target of
Level l -> return $ Type l
Sort s -> return s
v -> do
reportSDoc "impossible" 10 $ vcat
[ text "The impossible happened when checking record expression against meta"
, text "Candidate record type r = " <+> prettyTCM r
, text "Type of r = " <+> prettyTCM rt
, text "Ends in (should be sort)= " <+> prettyTCM v
, text $ " Raw = " ++ show v
]
__IMPOSSIBLE__
let inferred = El s $ Def r $ map Apply vs
v <- checkExpr e inferred
coerce v inferred t
_:_:_ -> do
reportSDoc "tc.term.expr.rec" 10 $ sep
[ text "Postponing type checking of"
, nest 2 $ prettyA e <+> text ":" <+> prettyTCM t
]
postponeTypeCheckingProblem_ $ CheckExpr e t
checkRecordUpdate :: A.ExprInfo -> A.Expr -> A.Assigns -> A.Expr -> Type -> TCM Term
checkRecordUpdate ei recexpr fs e t = do
case ignoreSharing $ unEl t of
Def r vs -> do
v <- checkExpr recexpr t
name <- freshNoName (getRange recexpr)
addLetBinding defaultArgInfo name v t $ do
projs <- recFields <$> getRecordDef r
axs <- getRecordFieldNames r
scope <- getScope
let xs = map unArg axs
es <- orderFields r Nothing xs $ map (\ (FieldAssignment x e) -> (x, Just e)) fs
let es' = zipWith (replaceFields name ei) projs es
checkExpr (A.Rec ei [ Left (FieldAssignment x e) | (x, Just e) <- zip xs es' ]) t
MetaV _ _ -> do
inferred <- inferExpr recexpr >>= reduce . snd
case ignoreSharing $ unEl inferred of
MetaV _ _ -> postponeTypeCheckingProblem_ $ CheckExpr e t
_ -> do
v <- checkExpr e inferred
coerce v inferred t
_ -> typeError $ ShouldBeRecordType t
where
replaceFields :: Name -> A.ExprInfo -> Arg A.QName -> Maybe A.Expr -> Maybe A.Expr
replaceFields n ei a@(Arg _ p) Nothing | notHidden a =
Just $ A.App ei (A.Def p) $ defaultNamedArg $ A.Var n
replaceFields _ _ (Arg _ _) Nothing = Nothing
replaceFields _ _ _ (Just e) = Just $ e
checkLiteral :: Literal -> Type -> TCM Term
checkLiteral lit t = do
t' <- litType lit
coerce (Lit lit) t' t
checkArguments' ::
ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type ->
(Args -> Type -> TCM Term) -> TCM Term
checkArguments' exph r args t0 t k = do
z <- runExceptT $ checkArguments exph r args t0 t
case z of
Right (vs, t1) -> k vs t1
Left (us, es, t0) -> do
reportSDoc "tc.term.expr.args" 80 $
sep [ text "postponed checking arguments"
, nest 4 $ prettyList (map (prettyA . namedThing . unArg) args)
, nest 2 $ text "against"
, nest 4 $ prettyTCM t0 ] $$
sep [ text "progress:"
, nest 2 $ text "checked" <+> prettyList (map prettyTCM us)
, nest 2 $ text "remaining" <+> sep [ prettyList (map (prettyA . namedThing . unArg) es)
, nest 2 $ text ":" <+> prettyTCM t0 ] ]
postponeTypeCheckingProblem_ (CheckArgs exph r es t0 t $ \vs t -> k (us ++ vs) t)
scopedExpr :: A.Expr -> TCM A.Expr
scopedExpr (A.ScopedExpr scope e) = setScope scope >> scopedExpr e
scopedExpr e = return e
checkExpr :: A.Expr -> Type -> TCM Term
checkExpr e t0 =
verboseBracket "tc.term.expr.top" 5 "checkExpr" $
traceCall (CheckExprCall e t0) $ localScope $ doExpandLast $ shared =<< do
reportSDoc "tc.term.expr.top" 15 $
text "Checking" <+> sep
[ fsep [ prettyTCM e, text ":", prettyTCM t0 ]
, nest 2 $ text "at " <+> (text . show =<< getCurrentRange)
]
reportSDoc "tc.term.expr.top.detailed" 80 $
text "Checking" <+> fsep [ prettyTCM e, text ":", text (show t0) ]
t <- reduce t0
reportSDoc "tc.term.expr.top" 15 $
text " --> " <+> prettyTCM t
e <- scopedExpr e
case e of
A.ScopedExpr scope e -> __IMPOSSIBLE__
_ | Pi (Dom info _) b <- ignoreSharing $ unEl t
, let h = getHiding info
, notVisible h
, not (hiddenLambdaOrHole h e)
-> do
x <- unshadowName <=< freshName rx $ notInScopeName $ absName b
reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda"
checkExpr (A.Lam (A.ExprRange re) (domainFree info x) e) t
where
re = getRange e
rx = caseMaybe (rStart re) noRange $ \ pos -> posToRange pos pos
hiddenLambdaOrHole h e = case e of
A.AbsurdLam _ h' -> h == h'
A.ExtendedLam _ _ _ cls -> any hiddenLHS cls
A.Lam _ bind _ -> h == getHiding bind
A.QuestionMark{} -> True
_ -> False
hiddenLHS (A.Clause (A.LHS _ (A.LHSHead _ (a : _)) _) _ _ _ _) = notVisible a
hiddenLHS _ = False
A.QuestionMark i ii -> checkQuestionMark (newValueMeta' DontRunMetaOccursCheck) t0 i ii
A.Underscore i -> checkUnderscore t0 i
A.WithApp _ e es -> typeError $ NotImplemented "type checking of with application"
A.App i s arg@(Arg ai l)
| A.Set _ 0 <- unScope s, visible ai ->
ifNotM hasUniversePolymorphism
(typeError $ GenericError "Use --universe-polymorphism to enable level arguments to Set")
$ do
lvl <- levelType
n <- levelView =<< do
applyRelevanceToContext NonStrict $
checkNamedArg arg lvl
reportSDoc "tc.univ.poly" 10 $
text "checking Set " <+> prettyTCM n <+>
text "against" <+> prettyTCM t
coerce (Sort $ Type n) (sort $ sSuc $ Type n) t
e0@(A.App i q (Arg ai e))
| A.Quote _ <- unScope q, visible ai -> do
let quoted (A.Def x) = return x
quoted (A.Macro x) = return x
quoted (A.Proj o (AmbQ [x])) = return x
quoted (A.Proj o (AmbQ xs)) = typeError $ GenericError $ "quote: Ambigous name: " ++ show xs
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
coerce (quoteName x) ty t
| A.QuoteTerm _ <- unScope q ->
do (et, _) <- inferExpr (namedThing e)
et' <- etaContract =<< instantiateFull et
let metas = allMetas et'
case metas of
_:_ -> postponeTypeCheckingProblem (CheckExpr e0 t) $ andM $ map isInstantiatedMeta metas
[] -> do
q <- quoteTerm et'
ty <- el primAgdaTerm
coerce q ty 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 -> checkAbsurdLambda i h e t
A.ExtendedLam i di qname cs -> checkExtendedLambda i di qname cs e t
A.Lam i (A.DomainFull (A.TypedBindings _ b)) e -> checkLambda b e t
A.Lam i (A.DomainFree info x) e0 -> checkExpr (A.Lam i (domainFree info x) e0) t
A.Lit lit -> checkLiteral lit t
A.Let i ds e -> checkLetBindings ds $ checkExpr e t
A.Pi _ tel e | null tel -> checkExpr e t
A.Pi _ tel e -> do
(t0, t') <- checkPiTelescope tel $ \ tel -> do
t0 <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
return (t0, telePi tel t0)
noFunctionsIntoSize t0 t'
let s = getSort t'
v = unEl 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)
]
coerce v (sort s) t
A.Fun _ (Arg info a) b -> do
a' <- isType_ a
b' <- isType_ b
s <- ptsRule a' b'
let v = Pi (Dom info a') (NoAbs underscore b')
noFunctionsIntoSize b' $ El s v
coerce v (sort s) t
A.Set _ n -> do
coerce (Sort $ mkType n) (sort $ mkType $ n + 1) t
A.Prop _ -> do
typeError $ GenericError "Prop is no longer supported"
A.Rec _ fs -> checkRecordExpression fs e t
A.RecUpdate ei recexpr fs -> checkRecordUpdate ei recexpr fs e t
A.DontCare e ->
ifM ((Irrelevant ==) <$> asks envRelevance)
(dontCare <$> do applyRelevanceToContext Irrelevant $ checkExpr e t)
(internalError "DontCare may only appear in irrelevant contexts")
e0@(A.QuoteGoal _ x e) -> do
qg <- quoteGoal t
case qg of
Left metas -> postponeTypeCheckingProblem (CheckExpr e0 t) $ andM $ map isInstantiatedMeta metas
Right quoted -> do
tmType <- agdaTermType
(v, ty) <- addLetBinding defaultArgInfo x quoted tmType (inferExpr e)
coerce v ty t
e0@(A.QuoteContext _) -> do
qc <- quoteContext
case qc of
Left metas -> postponeTypeCheckingProblem (CheckExpr e0 t) $ andM $ map isInstantiatedMeta metas
Right quotedContext -> do
ctxType <- el $ list $ primArg <@> (unEl <$> agdaTypeType)
coerce quotedContext ctxType t
e0@(A.Tactic i e xs ys) -> do
qc <- quoteContext
qg <- quoteGoal t
let postpone metas = postponeTypeCheckingProblem (CheckExpr e0 t) $ andM $ map isInstantiatedMeta metas
case (qc, qg) of
(Left metas1, Left metas2) -> postpone $ metas1 ++ metas2
(Left metas , Right _ ) -> postpone $ metas
(Right _ , Left metas ) -> postpone $ metas
(Right quotedCtx, Right quotedGoal) -> do
quotedCtx <- defaultNamedArg <$> reify quotedCtx
quotedGoal <- defaultNamedArg <$> reify quotedGoal
let tac = foldl (A.App i) (A.App i (A.App i e quotedCtx) quotedGoal) xs
result = foldl (A.App i) (A.Unquote i) (defaultNamedArg tac : ys)
checkExpr result t
A.ETel _ -> __IMPOSSIBLE__
A.Dot{} -> typeError $ GenericError $ "Invalid dotted expression"
_ | Application hd args <- appView e -> checkApplication hd args e t
quoteGoal :: Type -> TCM (Either [MetaId] Term)
quoteGoal t = do
t' <- etaContract =<< instantiateFull t
let metas = allMetas t'
case metas of
_:_ -> return $ Left metas
[] -> do
quotedGoal <- quoteTerm (unEl t')
return $ Right quotedGoal
quoteContext :: TCM (Either [MetaId] Term)
quoteContext = do
contextTypes <- map (fmap snd) <$> getContext
contextTypes <- etaContract =<< instantiateFull contextTypes
let metas = allMetas contextTypes
case metas of
_:_ -> return $ Left metas
[] -> do
quotedContext <- buildList <*> mapM quoteDom contextTypes
return $ Right quotedContext
unquoteM :: A.Expr -> Term -> Type -> TCM Term -> TCM Term
unquoteM tac hole holeType k = do
tac <- checkExpr tac =<< (el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit))
inFreshModuleIfFreeParams $ unquoteTactic tac hole holeType k
unquoteTactic :: Term -> Term -> Type -> TCM Term -> TCM Term
unquoteTactic tac hole goal k = do
ok <- runUnquoteM $ unquoteTCM tac hole
case ok of
Left (BlockedOnMeta oldState x) -> do
put oldState
mi <- Map.lookup x <$> getMetaStore
(r, unblock) <- case mi of
Nothing -> do
otherMetas <- allMetas <$> instantiateFull goal
case otherMetas of
[] -> return (noRange, return False)
x:_ -> return (noRange, isInstantiatedMeta x)
Just mi -> return (getRange mi, isInstantiatedMeta x)
setCurrentRange r $
postponeTypeCheckingProblem (UnquoteTactic tac hole goal) unblock
Left err -> typeError $ UnquoteFailed err
Right _ -> k
inferProjApp :: A.Expr -> ProjOrigin -> [QName] -> A.Args -> TCM (Term, Type)
inferProjApp e o ds args0 = inferOrCheckProjApp e o ds args0 Nothing
checkProjApp :: A.Expr -> ProjOrigin -> [QName] -> A.Args -> Type -> TCM Term
checkProjApp e o ds args0 t = do
(v, ti) <- inferOrCheckProjApp e o ds args0 (Just t)
coerce v ti t
inferOrCheckProjApp
:: A.Expr
-> ProjOrigin
-> [QName]
-> A.Args
-> Maybe Type
-> TCM (Term, Type)
inferOrCheckProjApp e o ds args mt = do
reportSDoc "tc.proj.amb" 20 $ vcat
[ text "checking ambiguous projection"
, text $ " ds = " ++ show ds
, text " args = " <+> sep (map prettyTCM args)
, text " t = " <+> caseMaybe mt (text "Nothing") prettyTCM
]
let refuse :: String -> TCM (Term, Type)
refuse reason = typeError $ GenericError $
"Cannot resolve overloaded projection "
++ show (A.nameConcrete $ A.qnameName $ head ds)
++ " because " ++ reason
refuseNotApplied = refuse "it is not applied to a visible argument"
refuseNoMatching = refuse "no matching candidate found"
refuseNotRecordType = refuse "principal argument is not of record type"
postpone m = do
tc <- caseMaybe mt newTypeMeta_ return
v <- postponeTypeCheckingProblem (CheckExpr e tc) $ isInstantiatedMeta m
return (v, tc)
case filter (visible . getHiding . snd) $ zip [0..] args of
[] -> caseMaybe mt refuseNotApplied $ \ t -> do
TelV _ptel core <- telViewUpTo' (1) (not . visible) t
ifBlockedType core (\ m _ -> postpone m) $ \ core -> do
ifNotPiType core (\ _ -> refuseNotApplied) $ \ dom _b -> do
ifBlockedType (unDom dom) (\ m _ -> postpone m) $ \ ta -> do
caseMaybeM (isRecordType ta) refuseNotRecordType $ \ (_q, _pars, defn) -> do
case defn of
Record { recFields = fs } -> do
case catMaybes $ for fs $ \ (Arg _ f) -> find (f ==) ds of
[] -> refuseNoMatching
[d] -> do
storeDisambiguatedName d
(,t) <$> checkHeadApplication e t (A.Proj o $ AmbQ [d]) args
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
((k, arg) : _) -> do
(v0, ta) <- inferExpr $ namedArg arg
reportSDoc "tc.proj.amb" 25 $ vcat
[ text " principal arg " <+> prettyTCM arg
, text " has type " <+> prettyTCM ta
]
(vargs, ta) <- implicitArgs (1) (not . visible) ta
let v = v0 `apply` vargs
ifBlockedType ta (\ m _ -> postpone m) $ \ ta -> do
caseMaybeM (isRecordType ta) refuseNotRecordType $ \ (q, _pars0, _) -> do
let try d = do
reportSDoc "tc.proj.amb" 30 $ vcat
[ text $ "trying projection " ++ show d
, text " td = " <+> caseMaybeM (getDefType d ta) (text "Nothing") prettyTCM
]
Projection{ projProper = proper, projOrig = orig } <- MaybeT $ isProjection d
guard proper
(dom, u, tb) <- MaybeT (projectTyped v ta o d `catchError` \ _ -> return Nothing)
reportSDoc "tc.proj.amb" 30 $ vcat
[ text " dom = " <+> prettyTCM dom
, text " u = " <+> prettyTCM u
, text " tb = " <+> prettyTCM tb
]
(q', pars, _) <- MaybeT $ isRecordType $ unDom dom
reportSDoc "tc.proj.amb" 30 $ vcat
[ text " q = " <+> prettyTCM q
, text " q' = " <+> prettyTCM q'
]
guard (q == q')
tfull <- lift $ defType <$> getConstInfo d
TelV tel _ <- lift $ telViewUpTo' (1) (not . visible) tfull
reportSDoc "tc.proj.amb" 30 $ vcat
[ text $ " size tel = " ++ show (size tel)
, text $ " size pars = " ++ show (size pars)
]
return (orig, (d, (pars, (dom, u, tb))))
cands <- groupOn fst . catMaybes <$> mapM (runMaybeT . try) ds
case cands of
[] -> refuseNoMatching
[[]] -> refuseNoMatching
(_:_:_) -> refuse $ "several matching candidates found: "
++ show (map (fst . snd) $ concat cands)
[ (_orig, (d, (pars, (_dom,u,tb)))) : _ ] -> do
storeDisambiguatedName d
tfull <- typeOfConst d
(_,_) <- checkKnownArguments (take k args) pars tfull
let tc = fromMaybe typeDontCare mt
let r = getRange e
z <- runExceptT $ checkArguments ExpandLast r (drop (k+1) args) tb tc
case z of
Right (us, trest) -> return (u `apply` us, trest)
Left (us1, es2, trest1) -> do
tc <- caseMaybe mt newTypeMeta_ return
v <- postponeTypeCheckingProblem_ $
CheckArgs ExpandLast r es2 trest1 tc $ \ us2 trest ->
coerce (u `apply` us1 `apply` us2) trest tc
return (v, tc)
checkApplication :: A.Expr -> A.Args -> A.Expr -> Type -> TCM Term
checkApplication hd args e t = do
reportSDoc "tc.check.app" 20 $ vcat
[ text "checkApplication"
, nest 2 $ text "hd = " <+> prettyA hd
, nest 2 $ text "args = " <+> sep (map prettyA args)
, nest 2 $ text "e = " <+> prettyA e
, nest 2 $ text "t = " <+> prettyTCM t
]
reportSDoc "tc.check.app" 70 $ vcat
[ text "checkApplication (raw)"
, nest 2 $ text $ "hd = " ++ show hd
, nest 2 $ text $ "args = " ++ show (deepUnscope args)
, nest 2 $ text $ "e = " ++ show (deepUnscope e)
, nest 2 $ text $ "t = " ++ show t
]
case unScope hd of
A.Proj _ (AmbQ []) -> __IMPOSSIBLE__
A.Proj _ (AmbQ [_]) -> checkHeadApplication e t hd args
A.Proj o (AmbQ ds@(_:_:_)) -> checkProjApp e o ds args t
A.Con (AmbQ cs@(_:_:_)) -> 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)
cons <- mapM getConForm cs
reportSLn "tc.check.term" 40 $ " reduced: " ++ show cons
dcs <- zipWithM (\ c con -> (, setConName c con) . getData . theDef <$> getConInfo con) cs cons
let badCon t = typeError $ DoesNotConstructAnElementOf (head cs) t
let getCon :: TCM (Maybe ConHead)
getCon = do
TelV tel t1 <- telView t
addContext tel $ do
reportSDoc "tc.check.term.con" 40 $ nest 2 $
text "target type: " <+> prettyTCM t1
ifBlockedType t1 (\ m t -> return Nothing) $ \ t' ->
caseMaybeM (isDataOrRecord $ unEl t') (badCon t') $ \ d ->
case [ c | (d', c) <- dcs, d == d' ] of
[c] -> do
reportSLn "tc.check.term" 40 $ " decided on: " ++ show c
storeDisambiguatedName $ conName c
return $ Just c
[] -> badCon $ t' $> Def d []
cs -> typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d $ map conName cs
let unblock = isJust <$> getCon
mc <- getCon
case mc of
Just c -> checkConstructorApplication e t c args
Nothing -> postponeTypeCheckingProblem (CheckExpr e t) unblock
A.Con (AmbQ [c]) -> do
con <- getOrigConHead c
checkConstructorApplication e t con args
A.PatternSyn n -> do
(ns, p) <- lookupPatternSyn n
p <- setRange (getRange n) . killRange <$> expandPatternSynonyms (vacuous p)
let meta r = A.Underscore $ A.emptyMetaInfo{ A.metaRange = r }
case A.insertImplicitPatSynArgs meta (getRange n) ns args of
Nothing -> typeError $ BadArgumentsToPatternSynonym n
Just (s, ns) -> do
let p' = A.patternToExpr p
e' = A.lambdaLiftExpr (map unArg ns) (A.substExpr s p')
checkExpr e' t
A.Macro x -> do
TelV tel _ <- telView =<< normalise . defType =<< instantiateDef =<< getConstInfo x
tTerm <- primAgdaTerm
tName <- primQName
let argTel = init $ telToList tel
mkArg :: Type -> NamedArg A.Expr -> NamedArg A.Expr
mkArg t a | unEl t == tTerm =
(fmap . fmap)
(A.App (A.ExprRange (getRange a)) (A.QuoteTerm A.exprNoRange) . defaultNamedArg) a
mkArg t a | unEl t == tName =
(fmap . fmap)
(A.App (A.ExprRange (getRange a)) (A.Quote A.exprNoRange) . defaultNamedArg) a
mkArg t a | otherwise = a
makeArgs :: [Dom (String, Type)] -> [NamedArg A.Expr] -> ([NamedArg A.Expr], [NamedArg A.Expr])
makeArgs [] args = ([], args)
makeArgs _ [] = ([], [])
makeArgs tel@(d : _) (arg : args) =
case insertImplicit arg (map (fmap fst . argFromDom) tel) of
ImpInsert is -> makeArgs (drop (length is) tel) (arg : args)
BadImplicits -> (arg : args, [])
NoSuchName{} -> (arg : args, [])
NoInsertNeeded -> first (mkArg (snd $ unDom d) arg :) $ makeArgs (tail tel) args
(macroArgs, otherArgs) = makeArgs argTel args
unq = A.App (A.ExprRange $ fuseRange x args) (A.Unquote A.exprNoRange) . defaultNamedArg
desugared = A.app (unq $ unAppView $ Application (A.Def x) $ macroArgs) otherArgs
checkExpr desugared t
A.Unquote _
| [arg] <- args -> do
(_, hole) <- newValueMeta RunMetaOccursCheck t
unquoteM (namedArg arg) hole t $ return hole
| arg : args <- args -> do
tel <- metaTel args
target <- addContext tel newTypeMeta_
let holeType = telePi_ tel target
(vs, EmptyTel) <- checkArguments_ ExpandLast (getRange args) args tel
let rho = reverse (map unArg vs) ++# IdS
equalType (applySubst rho target) t
(_, hole) <- newValueMeta RunMetaOccursCheck holeType
unquoteM (namedArg arg) hole holeType $ return $ apply hole vs
where
metaTel :: [Arg a] -> TCM Telescope
metaTel [] = pure EmptyTel
metaTel (arg : args) = do
a <- newTypeMeta_
let dom = a <$ domFromArg arg
ExtendTel dom . Abs "x" <$> addContext ("x", dom) (metaTel args)
_ -> checkHeadApplication e t hd args
checkQuestionMark :: (Type -> TCM (MetaId, Term)) -> Type -> A.MetaInfo -> InteractionId -> TCM Term
checkQuestionMark new t0 i ii = do
reportSDoc "tc.interaction" 20 $ sep
[ text "Found interaction point"
, text (show ii)
, text ":"
, prettyTCM t0
]
reportSDoc "tc.interaction" 60 $ sep
[ text "Raw:"
, text (show t0)
]
checkMeta (newQuestionMark' new ii) t0 i
checkUnderscore :: Type -> A.MetaInfo -> TCM Term
checkUnderscore = checkMeta (newValueMeta RunMetaOccursCheck)
checkMeta :: (Type -> TCM (MetaId, Term)) -> Type -> A.MetaInfo -> TCM Term
checkMeta newMeta t i = fst <$> checkOrInferMeta newMeta (Just t) i
inferMeta :: (Type -> TCM (MetaId, Term)) -> A.MetaInfo -> TCM (Args -> Term, Type)
inferMeta newMeta i = mapFst apply <$> checkOrInferMeta newMeta Nothing i
checkOrInferMeta :: (Type -> TCM (MetaId, Term)) -> Maybe Type -> A.MetaInfo -> TCM (Term, Type)
checkOrInferMeta newMeta mt i = do
case A.metaNumber i of
Nothing -> do
setScope (A.metaScope i)
t <- maybe (workOnTypes $ newTypeMeta_) return mt
(x, v) <- newMeta t
setMetaNameSuggestion x (A.metaNameSuggestion i)
return (v, t)
Just x -> do
let v = MetaV x []
t' <- jMetaType . mvJudgement <$> lookupMeta x
case mt of
Nothing -> return (v, t')
Just t -> (,t) <$> coerce v t' t
domainFree :: ArgInfo -> A.Name -> A.LamBinding
domainFree info x =
A.DomainFull $ A.TypedBindings r $ Arg info $ A.TBind r [pure x] $ A.Underscore underscoreInfo
where
r = getRange x
underscoreInfo = A.MetaInfo
{ A.metaRange = r
, A.metaScope = emptyScopeInfo
, A.metaNumber = Nothing
, A.metaNameSuggestion = show $ A.nameConcrete x
}
inferHeadDef :: ProjOrigin -> QName -> TCM (Args -> Term, Type)
inferHeadDef o x = do
proj <- isProjection x
let app =
case proj of
Nothing -> \ args -> Def x $ map Apply args
Just p -> \ args -> projDropParsApply p o args
mapFst apply <$> inferDef app x
inferHead :: A.Expr -> TCM (Args -> Term, Type)
inferHead e = do
case e of
(A.Var x) -> do
(u, a) <- getVarInfo x
reportSDoc "tc.term.var" 20 $ hsep
[ text "variable" , text (show x)
, text "(" , text (show u) , text ")"
, text "has type:" , text (show a)
]
when (unusableRelevance $ getRelevance a) $
typeError $ VariableIsIrrelevant x
return (apply u, unDom a)
(A.Def x) -> inferHeadDef ProjPrefix x
(A.Proj o (AmbQ [d])) -> inferHeadDef o d
(A.Proj{}) -> __IMPOSSIBLE__
(A.Con (AmbQ [c])) -> do
con <- getOrigConHead c
(u, a) <- inferDef (\ _ -> Con con ConOCon []) c
Constructor{conPars = n} <- theDef <$> (instantiateDef =<< getConstInfo c)
reportSLn "tc.term.con" 7 $ unwords [show c, "has", show n, "parameters."]
return (apply u . genericDrop n, a)
(A.Con _) -> __IMPOSSIBLE__
(A.QuestionMark i ii) -> inferMeta (newQuestionMark ii) i
(A.Underscore i) -> inferMeta (newValueMeta RunMetaOccursCheck) i
e -> do
(term, t) <- inferExpr e
return (apply term, t)
inferDef :: (Args -> Term) -> QName -> TCM (Term, Type)
inferDef mkTerm x =
traceCall (InferDef 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
reportSDoc "tc.term.def" 10 $ do
text "inferred def " <+> prettyTCM x <+> hsep (map prettyTCM vs)
let t = defType d
reportSDoc "tc.term.def" 10 $ nest 2 $ text " : " <+> prettyTCM t
let v = mkTerm vs
reportSDoc "tc.term.def" 10 $ nest 2 $ text " --> " <+> prettyTCM v
return (v, t)
checkConstructorApplication :: A.Expr -> Type -> ConHead -> [NamedArg A.Expr] -> TCM Term
checkConstructorApplication org t c args = do
reportSDoc "tc.term.con" 50 $ vcat
[ text "entering checkConstructorApplication"
, nest 2 $ vcat
[ text "org =" <+> prettyTCM org
, text "t =" <+> prettyTCM t
, text "c =" <+> prettyTCM c
, text "args =" <+> prettyTCM args
] ]
let paramsGiven = checkForParams args
if paramsGiven then fallback else do
reportSDoc "tc.term.con" 50 $ text "checkConstructorApplication: no parameters explicitly supplied, continuing..."
cdef <- getConInfo c
let Constructor{conData = d, conPars = npars} = theDef cdef
reportSDoc "tc.term.con" 50 $ nest 2 $ text "d =" <+> prettyTCM d
t0 <- reduce (Def d [])
case (ignoreSharing t0, ignoreSharing $ unEl t) of
(Def d0 _, Def d' es) -> do
let ~(Just vs) = allApplyElims es
reportSDoc "tc.term.con" 50 $ nest 2 $ text "d0 =" <+> prettyTCM d0
reportSDoc "tc.term.con" 50 $ nest 2 $ text "d' =" <+> prettyTCM d'
reportSDoc "tc.term.con" 50 $ nest 2 $ text "vs =" <+> prettyTCM vs
if d' /= d0 then fallback else do
npars' <- getNumberOfParameters d'
caseMaybe (sequenceA $ List2 (Just npars, npars')) fallback $ \ (List2 (n, n')) -> do
reportSDoc "tc.term.con" 50 $ nest 2 $ text $ "n = " ++ show n
reportSDoc "tc.term.con" 50 $ nest 2 $ text $ "n' = " ++ show n'
when (n > n')
__IMPOSSIBLE__
let ps = genericTake n $ genericDrop (n' 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'
let TelV ptel _ = telView'UpTo n ctype
let pnames = map (fmap fst) $ telToList ptel
args' = dropArgs pnames args
expandLast <- asks envExpandLast
checkArguments' expandLast (getRange c) args' ctype' t $ \us t' -> do
reportSDoc "tc.term.con" 20 $ nest 2 $ vcat
[ text "us =" <+> prettyTCM us
, text "t' =" <+> prettyTCM t' ]
coerce (Con c ConOCon us) t' t
_ -> do
reportSDoc "tc.term.con" 50 $ nest 2 $ text "we are not at a datatype, falling back"
fallback
where
fallback = checkHeadApplication org t (A.Con (AmbQ [conName c])) args
checkForParams args =
let (hargs, rest) = span (not . visible) args
notUnderscore A.Underscore{} = False
notUnderscore _ = True
in any notUnderscore $ map (unScope . namedArg) hargs
dropArgs [] args = args
dropArgs ps [] = args
dropArgs ps args@(arg : args')
| Just p <- name,
Just ps' <- namedPar p ps = dropArgs ps' args'
| Nothing <- name,
Just ps' <- unnamedPar h ps = dropArgs ps' args'
| otherwise = args
where
name = fmap rangedThing . nameOf $ unArg arg
h = getHiding arg
namedPar x = dropPar ((x ==) . unDom)
unnamedPar h = dropPar ((h ==) . getHiding)
dropPar this (p : ps) | this p = Just ps
| otherwise = dropPar this ps
dropPar _ [] = 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
]
expandLast <- asks envExpandLast
checkArguments' expandLast (getRange hd) args t0 t $ \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 $ addContext eTel $ vcat
[ text "checking" <+>
prettyTCM fType <+> text "?<=" <+> prettyTCM eType
]
blockTerm t $ f vs <$ workOnTypes (do
addContext eTel $ leqType fType eType
compareTel t t1 CmpLeq eTel fTel)
(A.Def c) | Just c == (nameOfSharp <$> kit) -> do
arg <- case args of
[a] | getHiding a == NotHidden -> return $ namedArg a
_ -> typeError $ GenericError $ show c ++ " must be applied to exactly one argument."
i <- fresh :: TCM Int
let name = filter (/= '_') (show $ A.nameConcrete $ A.qnameName c) ++ "-" ++ show i
kit <- coinductionKit'
let flat = nameOfFlat kit
inf = nameOfInf kit
forcedType <- do
lvl <- levelType
(_, l) <- newValueMeta RunMetaOccursCheck lvl
lv <- levelView l
(_, a) <- newValueMeta RunMetaOccursCheck (sort $ Type lv)
return $ El (Type lv) $ Def inf [Apply $ setHiding Hidden $ defaultArg l, Apply $ defaultArg a]
wrapper <- inFreshModuleIfFreeParams $ do
c' <- setRange (getRange c) <$>
liftM2 qualify (killRange <$> currentModule)
(freshName_ name)
rel <- asks envRelevance
abs <- aModeToDef <$> asks envAbstractMode
let info = A.mkDefInfo (A.nameConcrete $ A.qnameName c') noFixity'
PublicAccess abs noRange
core = A.LHSProj { A.lhsDestructor = AmbQ [flat]
, A.lhsFocus = defaultNamedArg $ A.LHSHead c' []
, A.lhsPatsRight = [] }
clause = A.Clause (A.LHS (A.LHSRange noRange) core []) []
(A.RHS arg Nothing)
[] False
i <- currentOrFreshMutualBlock
addConstant c' =<< do
let ai = setRelevance rel defaultArgInfo
useTerPragma $
(defaultDefn ai c' forcedType emptyFunction)
{ defMutual = i }
checkFunDef NotDelayed info c' [clause]
reportSDoc "tc.term.expr.coind" 15 $ do
def <- theDef <$> getConstInfo c'
vcat $
[ text "The coinductive wrapper"
, nest 2 $ prettyTCM rel <> prettyTCM c' <+> text ":"
, nest 4 $ prettyTCM t
, nest 2 $ prettyA clause
, text "The definition is" <+> text (show $ funDelayed def) <>
text "."
]
return c'
e' <- Def wrapper . map Apply <$> getContextArgs
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'
]
blockTerm t $ e' <$ workOnTypes (leqType forcedType t)
A.Con _ -> __IMPOSSIBLE__
_ -> defaultResult
where
defaultResult = do
(f, t0) <- inferHead hd
expandLast <- asks envExpandLast
checkArguments' expandLast (getRange hd) args t0 t $ \vs t1 -> do
coerce (f vs) t1 t
traceCallE ::
#if !MIN_VERSION_transformers(0,4,1)
Error e =>
#endif
Call -> ExceptT e TCM r -> ExceptT e TCM r
traceCallE call m = do
z <- lift $ traceCall call $ runExceptT m
case z of
Right e -> return e
Left err -> throwError err
checkKnownArguments
:: [NamedArg A.Expr]
-> Args
-> Type
-> TCM (Args, Type)
checkKnownArguments [] vs t = return (vs, t)
checkKnownArguments (arg : args) vs t = do
(vs', t') <- traceCall (SetRange $ getRange arg) $ checkKnownArgument arg vs t
checkKnownArguments args vs' t'
checkKnownArgument
:: NamedArg A.Expr
-> Args
-> Type
-> TCM (Args, Type)
checkKnownArgument arg [] _ = genericDocError =<< do
text "Invalid projection parameter " <+> prettyA arg
checkKnownArgument arg@(Arg info e) (Arg _infov v : vs) t = do
(Dom info' a, b) <- mustBePi t
if not (getHiding info == getHiding info'
&& (notHidden info || maybe True ((absName b ==) . rangedThing) (nameOf e)))
then checkKnownArgument arg vs (b `absApp` v)
else do
u <- checkNamedArg arg a
equalTerm a u v
return (vs, b `absApp` v)
checkNamedArg :: NamedArg A.Expr -> Type -> TCM Term
checkNamedArg arg@(Arg info e0) t0 = do
let e = namedThing e0
let x = maybe "" rangedThing $ nameOf e0
traceCall (CheckExprCall e t0) $ do
reportSDoc "tc.term.args.named" 15 $ do
text "Checking named arg" <+> sep
[ fsep [ prettyTCM arg, text ":", prettyTCM t0 ]
]
reportSLn "tc.term.args.named" 75 $ " arg = " ++ show (deepUnscope arg)
let checkU = checkMeta (newMetaArg info x) t0
let checkQ = checkQuestionMark (newInteractionMetaArg info x) t0
if not $ isHole e then checkExpr e t0 else localScope $ do
scopedExpr e >>= \case
A.Underscore i -> checkU i
A.QuestionMark i ii -> checkQ i ii
_ -> __IMPOSSIBLE__
where
isHole A.Underscore{} = True
isHole A.QuestionMark{} = True
isHole (A.ScopedExpr _ e) = isHole e
isHole _ = False
checkArguments :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type ->
ExceptT (Args, [NamedArg A.Expr], Type) TCM (Args, Type)
checkArguments DontExpandLast _ [] t0 t1 = return ([], t0)
checkArguments exh r [] t0 t1 =
traceCallE (CheckArguments r [] t0 t1) $ lift $ do
t1' <- unEl <$> reduce t1
implicitArgs (1) (expand t1') t0
where
expand (Pi (Dom info _) _) Hidden = getHiding info /= Hidden &&
exh == ExpandLast
expand _ Hidden = exh == ExpandLast
expand (Pi (Dom info _) _) Instance = getHiding info /= Instance
expand _ Instance = True
expand _ NotHidden = False
checkArguments exh r args0@(arg@(Arg info e) : args) t0 t1 =
traceCallE (CheckArguments r args0 t0 t1) $ do
lift $ reportSDoc "tc.term.args" 30 $ sep
[ text "checkArguments"
, nest 2 $ vcat
[ text "e =" <+> prettyA e
, text "t0 =" <+> prettyTCM t0
, text "t1 =" <+> prettyTCM t1
]
]
let hx = getHiding info
mx = fmap rangedThing $ nameOf e
expand NotHidden y = False
expand hy y = hy /= hx || maybe False (y /=) mx
(nargs, t) <- lift $ implicitNamedArgs (1) expand t0
let (mxs, us) = unzip $ map (\ (Arg ai (Named mx u)) -> (mx, Arg ai u)) nargs
xs = catMaybes mxs
ifBlockedType t (\ m t -> throwError (us, args0, t)) $ \ t0' -> do
let shouldBePi
| notHidden info = lift $ typeError $ ShouldBePi t0'
| null xs = lift $ typeError $ ShouldBePi t0'
| otherwise = lift $ typeError $ WrongNamedArgument arg
let wrongPi
| null xs = lift $ typeError $ WrongHidingInApplication t0'
| otherwise = lift $ typeError $ WrongNamedArgument arg
case ignoreSharing $ unEl t0' of
Pi (Dom info' a) b
| getHiding info == getHiding info'
&& (notHidden info || maybe True ((absName b ==) . rangedThing) (nameOf e)) -> do
u <- lift $ applyRelevanceToContext (getRelevance info') $ do
let e' = e { nameOf = maybe (Just $ unranged $ absName b) Just (nameOf e) }
checkNamedArg (Arg info' e') a
addCheckedArgs us (Arg info' u) $
checkArguments exh (fuseRange r e) args (absApp b u) t1
| otherwise -> do
reportSDoc "error" 10 $ nest 2 $ vcat
[ text $ "info = " ++ show info
, text $ "info' = " ++ show info'
, text $ "absName b = " ++ show (absName b)
, text $ "nameOf e = " ++ show (nameOf e)
]
wrongPi
_ -> shouldBePi
where
addCheckedArgs us u rec =
(mapFst ((us ++) . (u :)) <$> rec)
`catchError` \(vs, es, t) ->
throwError (us ++ u : vs, es, t)
checkArguments_
:: ExpandHidden
-> Range
-> [NamedArg A.Expr]
-> Telescope
-> TCM (Args, Telescope)
checkArguments_ exh r args tel = do
z <- runExceptT $
checkArguments exh r args (telePi tel typeDontCare) typeDontCare
case z of
Right (args, t) -> do
let TelV tel' _ = telView' t
return (args, tel')
Left _ -> __IMPOSSIBLE__
inferExpr :: A.Expr -> TCM (Term, Type)
inferExpr = inferExpr' DontExpandLast
inferExpr' :: ExpandHidden -> A.Expr -> TCM (Term, Type)
inferExpr' exh e = case e of
_ | Application hd args <- appView e, defOrVar hd -> traceCall (InferExpr e) $ do
case hd of
A.Proj o (AmbQ ds@(_:_:_)) -> inferProjApp e o ds args
_ -> do
(f, t0) <- inferHead hd
res <- runExceptT $ checkArguments exh (getRange hd) args t0 (sort Prop)
case res of
Right (vs, t1) -> return (f vs, t1)
Left t1 -> fallback
_ -> fallback
where
fallback = do
t <- workOnTypes $ newTypeMeta_
v <- checkExpr e t
return (v,t)
defOrVar :: A.Expr -> Bool
defOrVar A.Var{} = True
defOrVar A.Def{} = True
defOrVar A.Proj{} = True
defOrVar (A.ScopedExpr _ e) = defOrVar e
defOrVar _ = False
checkDontExpandLast :: A.Expr -> Type -> TCM Term
checkDontExpandLast e t = case e of
_ | Application hd args <- appView e, defOrVar hd ->
traceCall (CheckExprCall e t) $ localScope $ dontExpandLast $ shared =<< do
checkApplication hd args e t
_ -> checkExpr e t
isModuleFreeVar :: Int -> TCM Bool
isModuleFreeVar i = do
params <- moduleParamsToApply =<< currentModule
return $ any ((== Var i []) . unArg) params
inferExprForWith :: A.Expr -> TCM (Term, Type)
inferExprForWith e = do
reportSDoc "tc.with.infer" 20 $ text "inferExprforWith " <+> prettyTCM e
reportSLn "tc.with.infer" 80 $ "inferExprforWith " ++ show (deepUnscope e)
traceCall (InferExpr e) $ do
(v, t) <- instantiateFull =<< inferExpr e
v0 <- reduce v
case ignoreSharing v0 of
Var i [] -> whenM (isModuleFreeVar i) $ do
reportSDoc "tc.with.infer" 80 $ vcat
[ text $ "with expression is variable " ++ show i
, text "current modules = " <+> do text . show =<< currentModule
, text "current module free vars = " <+> do text . show =<< getCurrentModuleFreeVars
, text "context size = " <+> do text . show =<< getContextSize
, text "current context = " <+> do prettyTCM =<< getContextTelescope
]
typeError $ WithOnFreeVariable e v0
_ -> return ()
TelV tel t0 <- telViewUpTo' (1) ((NotHidden /=) . getHiding) t
case ignoreSharing $ unEl t0 of
Def d vs -> do
res <- isDataOrRecordType d
case res of
Nothing -> return (v, t)
Just{} -> do
(args, t1) <- implicitArgs (1) (NotHidden /=) t
return (v `apply` args, t1)
_ -> 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 info x t e) ret =
traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
t <- isType_ t
v <- applyRelevanceToContext (getRelevance info) $ checkDontExpandLast e t
addLetBinding info x v t ret
checkLetBinding b@(A.LetPatBind i p e) ret =
traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
p <- expandPatternSynonyms p
(v, t) <- inferExpr' ExpandLast e
let
t0 = El (getSort t) $ Pi (Dom defaultArgInfo t) (NoAbs underscore typeDontCare)
p0 = Arg defaultArgInfo (Named Nothing p)
reportSDoc "tc.term.let.pattern" 10 $ vcat
[ text "let-binding pattern p at type t"
, nest 2 $ vcat
[ text "p (A) =" <+> text (show p)
, text "t =" <+> prettyTCM t
]
]
fvs <- getContextSize
checkLeftHandSide (CheckPattern p EmptyTel t) Nothing [p0] t0 Nothing $ \ (LHSResult _ delta0 ps _t _ asb) -> bindAsPatterns asb $ do
let p = case drop fvs ps of [p] -> namedArg p; _ -> __IMPOSSIBLE__
delta = telFromList $ drop fvs $ telToList delta0
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ text "p (I) =" <+> text (show p)
, text "delta =" <+> text (show delta)
]
fs <- recordPatternToProjections p
cxt0 <- getContext
let (binds, cxt) = splitAt (size delta) cxt0
toDrop = length binds
sigma = zipWith ($) fs (repeat v)
sub = parallelS (reverse sigma)
subLetBind (OpenThing cxt va) = OpenThing (drop toDrop cxt) (applySubst sub va)
escapeContext toDrop $ updateModuleParameters sub
$ locally eLetBindings (fmap subLetBind) $ do
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ text "delta =" <+> prettyTCM delta
, text "binds =" <+> text (show binds)
]
let fdelta = flattenTel delta
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ text "fdelta =" <+> text (show fdelta)
]
let tsl = applySubst sub fdelta
let ts = map unDom tsl
let infos = map domInfo tsl
let xs = map (fst . unDom) (reverse binds)
foldr (uncurry4 addLetBinding) ret $ zip4 infos xs sigma ts
checkLetBinding (A.LetApply i x modapp copyInfo _adir) ret = do
fv <- getCurrentModuleFreeVars
n <- getContextSize
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 copyInfo
withAnonymousModule x new ret
checkLetBinding A.LetOpen{} ret = ret
checkLetBinding (A.LetDeclaredVariable _) ret = ret