{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Application
( checkArguments
, checkArguments_
, checkApplication
, inferApplication
) where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), null )
#else
import Prelude hiding ( null )
#endif
import Control.Arrow (first, second)
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import Control.Monad.Reader
import Data.Maybe
import qualified Data.List as List
import Data.Either (partitionEithers)
import Data.Traversable (sequenceA)
import Data.Void
import qualified Data.IntSet as IntSet
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.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Free
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.Def
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Either
import Agda.Utils.Except
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.NonemptyList
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Size
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
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 _ p | Just _ <- getUnambiguous p -> checkHeadApplication e t hd args
A.Proj o p -> checkProjApp e o (unAmbQ p) args t
A.Con ambC | Just c <- getUnambiguous ambC -> do
con <- fromRightM (sigError __IMPOSSIBLE_VERBOSE__ (typeError $ AbstractConstructorNotInScope c)) $
getOrigConHead c
checkConstructorApplication e t con args
A.Con (AmbQ cs0) -> disambiguateConstructor cs0 t >>= \ case
Left unblock -> postponeTypeCheckingProblem (CheckExpr e t) unblock
Right c -> checkConstructorApplication e t c args
A.PatternSyn n -> do
(ns, p) <- lookupPatternSyn n
p <- return $ setRange (getRange n) $ killRange $ 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.defaultAppInfo (getRange a)) (A.QuoteTerm A.exprNoRange) . defaultNamedArg) a
mkArg t a | unEl t == tName =
(fmap . fmap)
(A.App (A.defaultAppInfo (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.defaultAppInfo $ 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
(Just vs, EmptyTel) <- mapFst allApplyElims <$> 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)
_ -> do
v <- checkHeadApplication e t hd args
reportSDoc "tc.term.app" 30 $ vcat
[ text "checkApplication: checkHeadApplication returned"
, nest 2 $ text "v = " <+> prettyTCM v
]
return v
inferApplication :: ExpandHidden -> A.Expr -> A.Args -> A.Expr -> TCM (Term, Type)
inferApplication exh hd args e | not (defOrVar hd) = do
t <- workOnTypes $ newTypeMeta_
v <- checkExpr e t
return (v, t)
inferApplication exh hd args e =
case unScope hd of
A.Proj o p | isAmbiguous p -> inferProjApp e o (unAmbQ p) args
_ -> do
(f, t0) <- inferHead hd
let r = getRange hd
res <- runExceptT $ checkArgumentsE exh (getRange hd) args t0 Nothing
case res of
Right (vs, t1, _) -> (,t1) <$> unfoldInlined (f vs)
Left problem -> do
t <- workOnTypes $ newTypeMeta_
v <- postponeArgs problem exh r args t $ \ vs _ _ -> unfoldInlined (f vs)
return (v, t)
inferHeadDef :: ProjOrigin -> QName -> TCM (Elims -> 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 applyE <$> inferDef app x
inferHead :: A.Expr -> TCM (Elims -> Term, Type)
inferHead e = do
case e of
A.Var x -> do
(u, a) <- getVarInfo x
reportSDoc "tc.term.var" 20 $ hsep
[ text "variable" , prettyTCM x
, text "(" , text (show u) , text ")"
, text "has type:" , prettyTCM a
]
when (unusableRelevance $ getRelevance a) $
typeError $ VariableIsIrrelevant x
return (applyE u, unDom a)
A.Def x -> inferHeadDef ProjPrefix x
A.Proj o ambP | Just d <- getUnambiguous ambP -> inferHeadDef o d
A.Proj{} -> __IMPOSSIBLE__
A.Con ambC | Just c <- getUnambiguous ambC -> do
con <- fromRightM (sigError __IMPOSSIBLE_VERBOSE__ (typeError $ AbstractConstructorNotInScope c)) $
getOrigConHead c
(u, a) <- inferDef (\ _ -> Con con ConOCon []) c
Constructor{conPars = n} <- theDef <$> (instantiateDef =<< getConstInfo c)
reportSLn "tc.term.con" 7 $ unwords [prettyShow c, "has", show n, "parameters."]
return (applyE u . drop 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 (applyE term, t)
inferDef :: (Args -> Term) -> QName -> TCM (Term, Type)
inferDef mkTerm x =
traceCall (InferDef x) $ do
d <- instantiateDef =<< getConstInfo x
checkRelevance x (defRelevance d)
vs <- freeVarsToApply x
let t = defType d
v = mkTerm vs
debug vs t v
return (v, t)
where
debug vs t v = do
reportSDoc "tc.term.def" 60 $
text "freeVarsToApply to def " <+> hsep (map (text . show) vs)
reportSDoc "tc.term.def" 10 $ vcat
[ text "inferred def " <+> prettyTCM x <+> hsep (map prettyTCM vs)
, nest 2 $ text ":" <+> prettyTCM t
, nest 2 $ text "-->" <+> prettyTCM v ]
checkRelevance :: QName -> Relevance -> TCM ()
checkRelevance _ Relevant = return ()
checkRelevance x drel = 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
checkHeadApplication :: A.Expr -> Type -> A.Expr -> [NamedArg A.Expr] -> TCM Term
checkHeadApplication e t hd args = do
sharp <- fmap nameOfSharp <$> coinductionKit
case hd of
A.Def c | Just c == sharp -> checkSharpApplication e t c args
_ -> defaultResult
where
defaultResult = defaultResult' Nothing
defaultResult' mk = do
(f, t0) <- inferHead hd
expandLast <- asks envExpandLast
checkArguments expandLast (getRange hd) args t0 t $ \ vs t1 checkedTarget -> do
let check = do
k <- mk
as <- allApplyElims vs
pure $ k as t1
v <- unfoldInlined (f vs)
maybe id (\ ck m -> blockTerm t $ ck >> m) check $ coerce' checkedTarget v t1 t
traceCallE :: 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
coerce' :: CheckedTarget -> Term -> Type -> Type -> TCM Term
coerce' NotCheckedTarget v inferred expected = coerce v inferred expected
coerce' (CheckedTarget Nothing) v _ _ = return v
coerce' (CheckedTarget (Just pid)) v _ expected = blockTermOnProblem expected v pid
checkArgumentsE :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Maybe Type ->
ExceptT (Elims, [NamedArg A.Expr], Type) TCM (Elims, Type, CheckedTarget)
checkArgumentsE = checkArgumentsE' NotCheckedTarget
checkArgumentsE' :: CheckedTarget -> ExpandHidden -> Range -> [NamedArg A.Expr] -> Type ->
Maybe Type -> ExceptT (Elims, [NamedArg A.Expr], Type) TCM (Elims, Type, CheckedTarget)
checkArgumentsE' chk DontExpandLast _ [] t0 _ = return ([], t0, chk)
checkArgumentsE' chk ExpandLast r [] t0 mt1 =
traceCallE (CheckArguments r [] t0 mt1) $ lift $ do
mt1' <- traverse (unEl <.> reduce) mt1
(us, t) <- implicitArgs (-1) (expand mt1') t0
return (map Apply us, t, chk)
where
expand (Just (Pi dom _)) Hidden = not (hidden dom)
expand _ Hidden = True
expand (Just (Pi dom _)) Instance{} = not (isInstance dom)
expand _ Instance{} = True
expand _ NotHidden = False
checkArgumentsE' chk exh r args0@(arg@(Arg info e) : args) t0 mt1 =
traceCallE (CheckArguments r args0 t0 mt1) $ do
lift $ reportSDoc "tc.term.args" 30 $ sep
[ text "checkArgumentsE"
, nest 2 $ vcat
[ text "e =" <+> prettyA e
, text "t0 =" <+> prettyTCM t0
, text "t1 =" <+> maybe (text "Nothing") prettyTCM mt1
]
]
let hx = getHiding info
mx = fmap rangedThing $ nameOf e
expand NotHidden y = False
expand hy y = not (sameHiding hy hx) || maybe False (y /=) mx
(nargs, t) <- lift $ implicitNamedArgs (-1) expand t0
let (mxs, us) = unzip $ map (\ (Arg ai (Named mx u)) -> (mx, Apply $ Arg ai u)) nargs
xs = catMaybes mxs
t <- lift $ forcePiUsingInjectivity t
ifBlockedType t (\ m t -> throwError (us, args0, t)) $ \ _ t0' -> do
let shouldBePi
| visible 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
chk' <- lift $
case (chk, mt1) of
(NotCheckedTarget, Just t1) | all visible args0 -> do
let n = length args0
TelV tel tgt <- telViewUpTo n t0'
let dep = any (< n) $ IntSet.toList $ freeVars tgt
vis = all visible (telToList tel)
isRigid (El _ (Pi dom _)) = return $ visible dom
isRigid (El _ (Def d _)) = theDef <$> getConstInfo d >>= return . \ case
Axiom{} -> True
AbstractDefn{} -> True
Function{funClauses = cs} -> null cs
Datatype{} -> True
Record{} -> True
Constructor{} -> __IMPOSSIBLE__
Primitive{} -> False
isRigid _ = return False
rigid <- isRigid tgt
if | dep -> return chk
| not rigid -> return chk
| not vis -> return chk
| otherwise -> do
let tgt1 = applySubst (strengthenS __IMPOSSIBLE__ $ size tel) tgt
reportSDoc "tc.term.args.target" 30 $ vcat
[ text "Checking target types first"
, nest 2 $ text "inferred =" <+> prettyTCM tgt1
, nest 2 $ text "expected =" <+> prettyTCM t1 ]
traceCall (CheckTargetType (fuseRange r args0) tgt1 t1) $
CheckedTarget <$> ifNoConstraints_ (leqType tgt1 t1)
(return Nothing) (return . Just)
_ -> return chk
case unEl t0' of
Pi (Dom{domInfo = info', unDom = a}) b
| sameHiding info info'
&& (visible 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 (Apply $ Arg info' u) $
checkArgumentsE' chk' exh (fuseRange r e) args (absApp b u) mt1
| otherwise -> do
reportSDoc "error" 10 $ nest 2 $ vcat
[ text $ "info = " ++ show info
, text $ "info' = " ++ show info'
, text $ "absName b = " ++ absName b
, text $ "nameOf e = " ++ show (nameOf e)
]
wrongPi
_ -> shouldBePi
where
addCheckedArgs us u rec = do
(vs, t, chk) <- rec
return (us ++ u : vs, t, chk)
`catchError` \ (vs, es, t) ->
throwError (us ++ u : vs, es, t)
checkArguments_
:: ExpandHidden
-> Range
-> [NamedArg A.Expr]
-> Telescope
-> TCM (Elims, Telescope)
checkArguments_ exh r args tel = do
z <- runExceptT $
checkArgumentsE exh r args (telePi tel typeDontCare) Nothing
case z of
Right (args, t, _) -> do
let TelV tel' _ = telView' t
return (args, tel')
Left _ -> __IMPOSSIBLE__
checkArguments ::
ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type ->
(Elims -> Type -> CheckedTarget -> TCM Term) -> TCM Term
checkArguments exph r args t0 t k = do
z <- runExceptT $ checkArgumentsE exph r args t0 (Just t)
case z of
Right (vs, t1, pid) -> k vs t1 pid
Left problem -> postponeArgs problem exph r args t k
postponeArgs :: (Elims, [NamedArg A.Expr], Type) -> ExpandHidden -> Range -> [NamedArg A.Expr] -> Type ->
(Elims -> Type -> CheckedTarget -> TCM Term) -> TCM Term
postponeArgs (us, es, t0) exph r args t k = 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 pid -> k (us ++ vs) t pid)
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 (t0, 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 = take n $ drop (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 $ \ es t' targetCheck -> do
let us = fromMaybe __IMPOSSIBLE__ (allApplyElims es)
reportSDoc "tc.term.con" 20 $ nest 2 $ vcat
[ text "us =" <+> prettyTCM us
, text "t' =" <+> prettyTCM t' ]
coerce' targetCheck (Con c ConOCon (map Apply 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 (unambiguous $ 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 (sameHiding h)
dropPar this (p : ps) | this p = Just ps
| otherwise = dropPar this ps
dropPar _ [] = Nothing
disambiguateConstructor :: NonemptyList QName -> Type -> TCM (Either (TCM Bool) ConHead)
disambiguateConstructor cs0 t = do
reportSLn "tc.check.term" 40 $ "Ambiguous constructor: " ++ prettyShow cs0
let getData Constructor{conData = d} = d
getData _ = __IMPOSSIBLE__
reportSLn "tc.check.term" 40 $ " ranges before: " ++ show (getRange cs0)
(cs, cons) <- unzip . snd . partitionEithers <$> do
forM (toList cs0) $ \ c -> mapRight (c,) <$> getConForm c
reportSLn "tc.check.term" 40 $ " reduced: " ++ prettyShow cons
case cons of
[] -> typeError $ AbstractConstructorNotInScope $ headNe cs0
[con] -> do
let c = setConName (fromMaybe __IMPOSSIBLE__ $ headMaybe cs) con
reportSLn "tc.check.term" 40 $ " only one non-abstract constructor: " ++ prettyShow c
storeDisambiguatedName $ conName c
return (Right c)
_ -> do
dcs <- zipWithM (\ c con -> (, setConName c con) . getData . theDef <$> getConInfo con) cs cons
let badCon t = typeError $ flip DoesNotConstructAnElementOf t $
fromMaybe __IMPOSSIBLE__ $ headMaybe cs
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: " ++ prettyShow c
storeDisambiguatedName $ conName c
return $ Just c
[] -> badCon $ t' $> Def d []
cs -> typeError $ CantResolveOverloadedConstructorsTargetingSameDatatype d $ map conName cs
getCon >>= \ case
Nothing -> return $ Left $ isJust <$> getCon
Just c -> return $ Right c
inferProjApp :: A.Expr -> ProjOrigin -> NonemptyList QName -> A.Args -> TCM (Term, Type)
inferProjApp e o ds args0 = do
(v, t, _) <- inferOrCheckProjApp e o ds args0 Nothing
return (v, t)
checkProjApp :: A.Expr -> ProjOrigin -> NonemptyList QName -> A.Args -> Type -> TCM Term
checkProjApp e o ds args0 t = do
(v, ti, targetCheck) <- inferOrCheckProjApp e o ds args0 (Just t)
coerce' targetCheck v ti t
inferOrCheckProjApp
:: A.Expr
-> ProjOrigin
-> NonemptyList QName
-> A.Args
-> Maybe Type
-> TCM (Term, Type, CheckedTarget)
inferOrCheckProjApp e o ds args mt = do
reportSDoc "tc.proj.amb" 20 $ vcat
[ text "checking ambiguous projection"
, text $ " ds = " ++ prettyShow ds
, text " args = " <+> sep (map prettyTCM args)
, text " t = " <+> caseMaybe mt (text "Nothing") prettyTCM
]
let refuse :: String -> TCM a
refuse reason = typeError $ GenericError $
"Cannot resolve overloaded projection "
++ prettyShow (A.nameConcrete $ A.qnameName $ headNe 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, NotCheckedTarget)
case filter (visible . 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) -> List.find (f ==) (toList ds) of
[] -> refuseNoMatching
[d] -> do
storeDisambiguatedName d
(, t, CheckedTarget Nothing) <$>
checkHeadApplication e t (A.Proj o $ unambiguous 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 " ++ prettyShow d
, text " td = " <+> caseMaybeM (getDefType d ta) (text "Nothing") prettyTCM
]
isP <- isProjection d
reportSDoc "tc.proj.amb" 40 $ vcat $
[ text $ " isProjection = " ++ caseMaybe isP "no" (const "yes")
] ++ caseMaybe isP [] (\ Projection{ projProper = proper, projOrig = orig } ->
[ text $ " proper = " ++ show proper
, text $ " orig = " ++ prettyShow orig
])
let orig = caseMaybe isP d projOrig
(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) (toList ds)
case cands of
[] -> refuseNoMatching
[[]] -> refuseNoMatching
(_:_:_) -> refuse $ "several matching candidates found: "
++ prettyShow (map (fst . snd) $ concat cands)
[ (_orig, (d, (pars, (_dom,u,tb)))) : _ ] -> do
storeDisambiguatedName d
tfull <- typeOfConst d
(_,_) <- checkKnownArguments (take k args) pars tfull
let r = getRange e
args' = drop (k + 1) args
z <- runExceptT $ checkArgumentsE ExpandLast r args' tb mt
case z of
Right (us, trest, targetCheck) -> return (u `applyE` us, trest, targetCheck)
Left problem -> do
tc <- caseMaybe mt newTypeMeta_ return
v <- postponeArgs problem ExpandLast r args' tc $ \ us trest targetCheck ->
coerce' targetCheck (u `applyE` us) trest tc
return (v, tc, NotCheckedTarget)
checkSharpApplication :: A.Expr -> Type -> QName -> [NamedArg A.Expr] -> TCM Term
checkSharpApplication e t c args = do
arg <- case args of
[a] | visible a -> return $ namedArg a
_ -> typeError $ GenericError $ prettyShow c ++ " must be applied to exactly one argument."
i <- fresh :: TCM Int
let name = filter (/= '_') (prettyShow $ 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 = unambiguous flat
, A.lhsFocus = defaultNamedArg $ A.LHSHead c' []
, A.lhsPats = [] }
clause = A.Clause (A.LHS empty core) []
(A.RHS arg Nothing)
A.noWhereDecls 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)