{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Term where
import Prelude hiding ( null )
import Control.Monad.Reader
import Data.Maybe
import Data.Either (partitionEithers, lefts)
import Data.Monoid (mappend)
import qualified Data.List as List
import qualified Data.Map as Map
import Agda.Interaction.Options
import Agda.Interaction.Highlighting.Generate (disambiguateRecordFields)
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views as A
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Concrete (FieldAssignment'(..), nameFieldA)
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.MetaVars
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Scope.Base ( ThingsInScope, AbstractName
, emptyScopeInfo
, exportedNamesInScope)
import Agda.Syntax.Scope.Monad (getNamedScope)
import Agda.Syntax.Translation.InternalToAbstract (reify)
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Coverage.SplitTree
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Generalize
import Agda.TypeChecking.Implicit
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.IApplyConfluence
import Agda.TypeChecking.Level
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Quote
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rules.LHS
import Agda.TypeChecking.SizedTypes
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.Sort
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Unquote
import Agda.TypeChecking.Warnings
import {-# SOURCE #-} Agda.TypeChecking.Empty ( ensureEmptyType )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Def (checkFunDef', useTerPragma)
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkSectionApplication)
import {-# SOURCE #-} Agda.TypeChecking.Rules.Application
import Agda.Utils.Except
(MonadError(catchError, throwError))
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty ( prettyShow )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Tuple
import Agda.Utils.Impossible
isType :: A.Expr -> Sort -> TCM Type
isType = isType' CmpLeq
isType' :: Comparison -> A.Expr -> Sort -> TCM Type
isType' c e s =
traceCall (IsTypeCall c e s) $ do
v <- checkExpr' c e (sort s)
return $ El s v
isType_ :: A.Expr -> TCM Type
isType_ e = traceCall (IsType_ e) $ do
let fallback = isType' CmpEq e =<< do workOnTypes $ newSortMeta
case unScope e of
A.Fun i (Arg info t) b -> do
a <- setArgInfo info . defaultDom <$> isType_ t
b <- isType_ b
s <- inferFunSort a (getSort 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)
checkTelePiSort t'
noFunctionsIntoSize t0 t'
return t'
A.Set _ n -> do
return $ sort (mkType n)
A.Prop _ n -> do
unlessM isPropEnabled $ typeError NeedOptionProp
return $ sort (mkProp n)
A.App i s arg
| visible arg,
A.Set _ 0 <- unScope s -> do
unlessM hasUniversePolymorphism $ genericError
"Use --universe-polymorphism to enable level arguments to Set"
applyRelevanceToContext NonStrict $
sort . Type <$> checkLevel arg
A.App i s arg
| visible arg,
A.Prop _ 0 <- unScope s -> do
unlessM isPropEnabled $ typeError NeedOptionProp
unlessM hasUniversePolymorphism $ genericError
"Use --universe-polymorphism to enable level arguments to Prop"
applyRelevanceToContext NonStrict $
sort . Prop <$> checkLevel arg
A.QuestionMark minfo ii -> caseMaybeM (lookupInteractionMeta ii) fallback $ \ x -> do
reportSDoc "tc.ip" 20 $ fsep
[ "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
[ " s0 = " <+> prettyTCM s0
, " vs = " <+> prettyTCM vs
, " rest = " <+> prettyTCM rest
]
if (length vs /= n) then fallback else do
s1 <- reduce =<< piApplyM s0 vs
reportSDoc "tc.ip" 20 $ vcat
[ " s1 = " <+> prettyTCM s1
]
reportSDoc "tc.ip" 70 $ vcat
[ " s1 = " <+> text (show s1)
]
case unEl s1 of
Sort s -> return $ El s $ MetaV x $ map Apply vs
_ -> __IMPOSSIBLE__
_ -> fallback
checkLevel :: NamedArg A.Expr -> TCM Level
checkLevel arg = do
lvl <- levelType
levelView =<< checkNamedArg arg lvl
noFunctionsIntoSize :: Type -> Type -> TCM ()
noFunctionsIntoSize t tBlame = do
reportSDoc "tc.fun" 20 $ do
let El s (Pi dom b) = tBlame
sep [ "created function type " <+> prettyTCM tBlame
, "with pts rule (" <+> prettyTCM (getSort dom) <+>
"," <+> underAbstraction_ b (prettyTCM . getSort) <+>
"," <+> prettyTCM 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'
checkGeneralizeTelescope :: A.GeneralizeTelescope -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
checkGeneralizeTelescope (A.GeneralizeTel vars tel) k =
generalizeTelescope vars (checkTelescope tel) k
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.TypedBinding -> (Telescope -> TCM a) -> TCM a
checkTypedBindings lamOrPi (A.TBind r tac xps e) ret = do
let xs = map (updateNamedArg $ A.unBind . A.binderName) xps
tac <- traverse (checkTacticAttribute lamOrPi) tac
whenJust tac $ \ t -> reportSDoc "tc.term.tactic" 30 $ "Checked tactic attribute:" <?> prettyTCM t
experimental <- optExperimentalIrrelevance <$> pragmaOptions
let cs = map getCohesion xps
c = headWithDefault __IMPOSSIBLE__ cs
unless (all (c ==) cs) $ __IMPOSSIBLE__
t <- applyCohesionToContext c $ modEnv lamOrPi $ isType_ e
unlessNull (filter isInstance xps) $ \ixs -> do
(tel, target) <- getOutputTypeName t
case target of
OutputTypeName{} -> return ()
OutputTypeVar{} -> return ()
OutputTypeVisiblePi{} -> warning . InstanceArgWithExplicitArg =<< prettyTCM (A.mkTBind r ixs e)
OutputTypeNameNotYetKnown{} -> return ()
NoOutputTypeName -> warning . InstanceNoOutputTypeName =<< prettyTCM (A.mkTBind r ixs e)
let setTac tac EmptyTel = EmptyTel
setTac tac (ExtendTel dom tel) = ExtendTel dom{ domTactic = tac } $ setTac (raise 1 tac) <$> tel
xs' = map (modMod lamOrPi experimental) xs
let tel = setTac tac $ namedBindsToTel xs t
addContext (xs', t) $ addTypedPatterns xps (ret tel)
where
modEnv LamNotPi = workOnTypes
modEnv _ = id
modMod PiNotLam xp = (if xp then mapRelevance irrToNonStrict else id)
. (setQuantity topQuantity)
modMod _ _ = id
checkTypedBindings lamOrPi (A.TLet _ lbs) ret = do
checkLetBindings lbs (ret EmptyTel)
addTypedPatterns :: [NamedArg A.Binder] -> TCM a -> TCM a
addTypedPatterns xps ret = do
let ps = mapMaybe (A.extractPattern . namedArg) xps
let lbs = fmap letBinding ps
checkLetBindings lbs ret
where
letBinding :: (A.Pattern, A.BindName) -> A.LetBinding
letBinding (p, n) = A.LetPatBind (A.LetRange r) p (A.Var $ A.unBind n)
where r = fuseRange p n
checkTacticAttribute :: LamOrPi -> A.Expr -> TCM Term
checkTacticAttribute LamNotPi e = genericDocError =<< "The @tactic attribute is not allowed here"
checkTacticAttribute PiNotLam e = do
expectedType <- el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)
checkExpr e expectedType
ifPath :: Type -> TCM a -> TCM a -> TCM a
ifPath ty fallback work = do
pv <- pathView ty
if isPathType pv then work else fallback
checkPath :: A.TypedBinding -> A.Expr -> Type -> TCM Term
checkPath b@(A.TBind _ _ [x'] typ) body ty = do
let x = updateNamedArg (A.unBind . A.binderName) x'
info = getArgInfo x
PathType s path level typ lhs rhs <- pathView ty
interval <- elInf primInterval
v <- addContext ([x], interval) $
checkExpr body (El (raise 1 s) (raise 1 (unArg typ) `apply` [argN $ var 0]))
iZero <- primIZero
iOne <- primIOne
let lhs' = subst 0 iZero v
rhs' = subst 0 iOne v
let t = Lam info $ Abs (namedArgName x) v
let btyp i = El s (unArg typ `apply` [argN i])
locallyTC eRange (const noRange) $ blockTerm ty $ traceCall (SetRange $ getRange body) $ do
equalTerm (btyp iZero) lhs' (unArg lhs)
equalTerm (btyp iOne) rhs' (unArg rhs)
return t
checkPath b body ty = __IMPOSSIBLE__
checkLambda :: Comparison -> A.TypedBinding -> A.Expr -> Type -> TCM Term
checkLambda cmp (A.TLet _ lbs) body target =
checkLetBindings lbs (checkExpr body target)
checkLambda cmp b@(A.TBind _ _ xps typ) body target = do
reportSDoc "tc.term.lambda" 60 $ vcat
[ "checkLambda xs = " <+> prettyA xps
, "possiblePath = " <+> text (show (possiblePath, numbinds, unScope typ, info))
]
TelV tel btyp <- telViewUpTo numbinds target
if size tel < numbinds || numbinds /= 1
then (if possiblePath then trySeeingIfPath else dontUseTargetType)
else useTargetType tel btyp
where
xs = map (updateNamedArg (A.unBind . A.binderName)) xps
numbinds = length xps
isUnderscore e = case e of { A.Underscore{} -> True; _ -> False }
possiblePath = numbinds == 1 && isUnderscore (unScope typ)
&& isRelevant info && visible info
info = getArgInfo (headWithDefault __IMPOSSIBLE__ xs)
trySeeingIfPath = do
cubical <- optCubical <$> pragmaOptions
reportSLn "tc.term.lambda" 60 $ "trySeeingIfPath for " ++ show xps
let postpone' = if cubical then postpone else \ _ _ -> dontUseTargetType
ifBlocked target postpone' $ \ _ t -> do
ifPath t dontUseTargetType $ if cubical
then checkPath b body t
else genericError "Option --cubical needed to build a path with a lambda abstraction"
postpone m tgt = postponeTypeCheckingProblem_ $
CheckExpr cmp (A.Lam A.exprNoRange (A.DomainFull b) body) tgt
dontUseTargetType = do
verboseS "tc.term.lambda" 5 $ tick "lambda-no-target-type"
argsT <- workOnTypes $ isType_ typ
let tel = namedBindsToTel xs argsT
reportSDoc "tc.term.lambda" 60 $ "dontUseTargetType tel =" <+> pretty tel
checkSizeLtSat $ unEl argsT
let postponeOnBlockedPattern m = m `catchIlltypedPatternBlockedOnMeta` \(err , x) -> do
reportSDoc "tc.term" 50 $ vcat $
[ "checking record pattern stuck on meta: " <+> text (show x) ]
t1 <- addContext (xs, argsT) $ workOnTypes newTypeMeta_
let e = A.Lam A.exprNoRange (A.DomainFull b) body
tgt' = telePi tel t1
w <- postponeTypeCheckingProblem (CheckExpr cmp e tgt') $ isInstantiatedMeta x
return (tgt' , w)
(target0 , w) <- postponeOnBlockedPattern $
addContext (xs, argsT) $ addTypedPatterns xps $ do
t1 <- workOnTypes newTypeMeta_
v <- checkExpr' cmp body t1
return (telePi tel t1 , teleLam tel v)
if notVisible info || any notVisible xs then do
pid <- newProblem_ $ leqType target0 target
blockTermOnProblem target w pid
else do
coerce cmp w target0 target
useTargetType tel@(ExtendTel dom (Abs y EmptyTel)) btyp = do
verboseS "tc.term.lambda" 5 $ tick "lambda-with-target-type"
reportSLn "tc.term.lambda" 60 $ "useTargetType y = " ++ y
let [x] = xs
unless (sameHiding dom info) $ typeError $ WrongHidingInLambda target
info <- lambdaModalityCheck dom info
let a = unDom dom
checkSizeLtSat $ unEl a
(pid, argT) <- newProblem $ isTypeEqualTo typ a
v <- lambdaAddContext (namedArg x) y (defaultArgDom info argT) $
addTypedPatterns xps $ checkExpr' cmp body btyp
blockTermOnProblem target (Lam info $ Abs (namedArgName x) v) pid
useTargetType _ _ = __IMPOSSIBLE__
lambdaModalityCheck :: LensModality dom => dom -> ArgInfo -> TCM ArgInfo
lambdaModalityCheck dom = lambdaCohesionCheck m <=< lambdaQuantityCheck m <=< lambdaIrrelevanceCheck m
where m = getModality dom
lambdaIrrelevanceCheck :: LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
lambdaIrrelevanceCheck dom info
| getRelevance info == defaultRelevance = return $ setRelevance (getRelevance dom) info
| otherwise = do
let rPi = getRelevance dom
let rLam = getRelevance info
unless (moreRelevant rPi rLam) $ do
unless (rLam == NonStrict) __IMPOSSIBLE__
unless (rPi == Irrelevant) __IMPOSSIBLE__
typeError WrongIrrelevanceInLambda
return info
lambdaQuantityCheck :: LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
lambdaQuantityCheck dom info
| noUserQuantity info = return $ setQuantity (getQuantity dom) info
| otherwise = do
let qPi = getQuantity dom
let qLam = getQuantity info
unless (qPi `moreQuantity` qLam) $ do
typeError WrongQuantityInLambda
return info
lambdaCohesionCheck :: LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
lambdaCohesionCheck dom info
| getCohesion info == defaultCohesion = return $ setCohesion (getCohesion dom) info
| otherwise = do
let cPi = getCohesion dom
let cLam = getCohesion info
unless (cPi `sameCohesion` cLam) $ do
typeError WrongCohesionInLambda
return info
lambdaAddContext :: Name -> ArgName -> Dom Type -> TCM a -> TCM a
lambdaAddContext x y dom
| isNoName x = addContext (y, dom)
| otherwise = addContext (x, dom)
checkPostponedLambda :: Comparison -> Arg ([WithHiding Name], Maybe Type) -> A.Expr -> Type -> TCM Term
checkPostponedLambda cmp args@(Arg _ ([] , _ )) body target = do
checkExpr' cmp body target
checkPostponedLambda cmp args@(Arg info (WithHiding h x : xs, mt)) body target = do
let postpone _ t = postponeTypeCheckingProblem_ $ CheckLambda cmp args body t
lamHiding = mappend h $ getHiding info
insertHiddenLambdas lamHiding target postpone $ \ t@(El _ (Pi dom b)) -> do
info' <- setHiding lamHiding <$> lambdaModalityCheck dom info
mpid <- caseMaybe mt (return Nothing) $ \ ascribedType -> Just <$> do
newProblem_ $ leqType (unDom dom) ascribedType
let dom' = setRelevance (getRelevance info') . setHiding lamHiding $
maybe dom (dom $>) mt
v <- lambdaAddContext x (absName b) dom' $
checkPostponedLambda cmp (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
ifBlocked target postpone $ \ _ t -> do
case unEl t of
Pi dom b -> do
let h' = getHiding dom
if sameHiding h h' then ret t else do
if visible h' then typeError $ WrongHidingInLambda target else do
let x = absName b
Lam (setOrigin Inserted $ domInfo dom) . Abs x <$> do
addContext (x, dom) $ insertHiddenLambdas h (absBody b) postpone ret
_ -> typeError . GenericDocError =<< do
"Expected " <+> prettyTCM target <+> " to be a function type"
checkAbsurdLambda :: Comparison -> A.ExprInfo -> Hiding -> A.Expr -> Type -> TCM Term
checkAbsurdLambda cmp i h e t = localTC (set eQuantity topQuantity) $ do
t <- instantiateFull t
ifBlocked t (\ m t' -> postponeTypeCheckingProblem_ $ CheckExpr cmp e t') $ \ _ t' -> do
case unEl t' of
Pi dom@(Dom{domInfo = info', unDom = a}) b
| not (sameHiding h info') -> typeError $ WrongHidingInLambda t'
| not (noMetas a) ->
postponeTypeCheckingProblem (CheckExpr cmp e t') $
noMetas <$> instantiateFull a
| otherwise -> blockTerm t' $ do
ensureEmptyType (getRange i) a
top <- currentModule
aux <- qualify top <$> freshName_ (getRange i, absurdLambdaName)
mod <- asksTC getModality
reportSDoc "tc.term.absurd" 10 $ vcat
[ ("Adding absurd function" <+> prettyTCM mod) <> prettyTCM aux
, nest 2 $ "of type" <+> prettyTCM t'
]
addConstant aux $
(\ d -> (defaultDefn (setModality mod info') aux t' d)
{ defPolarity = [Nonvariant]
, defArgOccurrences = [Unused] })
$ emptyFunction
{ funClauses =
[ Clause
{ clauseLHSRange = getRange e
, clauseFullRange = getRange e
, clauseTel = telFromList [fmap (absurdPatternName,) dom]
, namedClausePats = [Arg info' $ Named (Just $ WithOrigin Inserted $ unranged $ absName b) $ absurdP 0]
, clauseBody = Nothing
, clauseType = Just $ setModality mod $ defaultArg $ absBody b
, clauseCatchall = False
, clauseUnreachable = Just True
, clauseEllipsis = NoEllipsis
}
]
, funCompiled = Just Fail
, funSplitTree = Just $ SplittingDone 0
, funMutual = Just []
, funTerminates = Just True
}
tel <- getContextTelescope
return $ Def aux $ map Apply $ teleArgs tel
_ -> typeError $ ShouldBePi t'
checkExtendedLambda :: Comparison -> A.ExprInfo -> A.DefInfo -> QName -> [A.Clause] ->
A.Expr -> Type -> TCM Term
checkExtendedLambda cmp i di qname cs e t = localTC (set eQuantity topQuantity) $ do
solveSizeConstraints DontDefaultToInfty
lamMod <- inFreshModuleIfFreeParams currentModule
t <- instantiateFull t
ifBlocked t (\ m t' -> postponeTypeCheckingProblem_ $ CheckExpr cmp e t') $ \ _ t -> do
j <- currentOrFreshMutualBlock
mod <- asksTC getModality
let info = setModality mod defaultArgInfo
reportSDoc "tc.term.exlam" 20 $
(text (show $ A.defAbstract di) <+>
"extended lambda's implementation \"") <> prettyTCM qname <>
"\" has type: " $$ prettyTCM t
args <- getContextArgs
(abstract (A.defAbstract di) $ do
addConstant qname =<< do
useTerPragma $
(defaultDefn info qname t emptyFunction) { defMutual = j }
checkFunDef' t info NotDelayed (Just $ ExtLamInfo lamMod Nothing) Nothing di qname cs
whenNothingM (asksTC envMutualBlock) $
checkIApplyConfluence_ qname
return $ Def qname $ map Apply args)
where
abstract ConcreteDef = inConcreteMode
abstract AbstractDef = inAbstractMode
catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, MetaId) -> TCM a) -> TCM a
catchIlltypedPatternBlockedOnMeta m handle = do
st <- getTC
m `catchError` \ err -> do
let reraise = throwError err
x <- maybe reraise return =<< do
case err of
TypeError s cl -> localTCState $ do
putTC s
enterClosure cl $ \case
IlltypedPattern p a -> isBlocked a
SplitError (UnificationStuck c tel us vs _) -> do
problem <- reduce =<< instantiateFull (flattenTel tel, us, vs)
return $ firstMeta problem
SplitError (NotADatatype aClosure) ->
enterClosure aClosure $ \ a -> isBlocked a
CannotEliminateWithPattern p a -> isBlocked a
_ -> return Nothing
_ -> return Nothing
reportSDoc "tc.postpone" 20 $ vcat $
[ "checking definition blocked on meta: " <+> prettyTCM x ]
putTC st
lookupMeta' x >>= \case
Nothing -> reraise
Just m | InstV{} <- mvInstantiation m -> reraise
Just m | Frozen <- mvFrozen m -> isInteractionMeta x >>= \case
Nothing -> reraise
Just{} -> handle (err, x)
Just{} -> handle (err, x)
expandModuleAssigns
:: [Either A.Assign A.ModuleName]
-> [C.Name]
-> TCM A.Assigns
expandModuleAssigns mfs xs = do
let (fs , ms) = partitionEithers mfs
fs' <- forM (xs List.\\ map (view nameFieldA) fs) $ \ 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 $ killRange $ A.nameToExpr n)
_ -> Nothing
case catMaybes pms of
[] -> return Nothing
[(_, fa)] -> return (Just fa)
mfas -> typeError . GenericDocError =<< do
vcat $
[ "Ambiguity: the field" <+> prettyTCM f
<+> "appears in the following modules: " ]
++ map (prettyTCM . fst) mfas
return (fs ++ catMaybes fs')
checkRecordExpression
:: Comparison
-> A.RecordAssigns
-> A.Expr
-> Type
-> TCM Term
checkRecordExpression cmp mfs e t = do
reportSDoc "tc.term.rec" 10 $ sep
[ "checking record expression"
, prettyA e
]
ifBlocked t (\ _ t -> guessRecordType t) $ \ _ t -> do
case unEl t of
Def r es -> do
let ~(Just vs) = allApplyElims es
reportSDoc "tc.term.rec" 20 $ text $ " r = " ++ prettyShow r
reportSDoc "tc.term.rec" 30 $ " xs = " <> do
text =<< prettyShow . map unDom <$> getRecordFieldNames r
reportSDoc "tc.term.rec" 30 $ " ftel= " <> do
prettyTCM =<< getRecordFieldTypes r
reportSDoc "tc.term.rec" 30 $ " con = " <> do
text =<< prettyShow <$> getRecordConstructor r
def <- getRecordDef r
let
cxs = map argFromDom $ recordFieldNames def
xs = map unArg cxs
con = killRange $ recConHead def
reportSDoc "tc.term.rec" 20 $ vcat
[ " xs = " <> return (P.pretty xs)
, " ftel= " <> prettyTCM (recTel def)
, " con = " <> return (P.pretty con)
]
disambiguateRecordFields (map _nameFieldA $ lefts mfs) (map unDom $ recFields def)
fs <- expandModuleAssigns mfs (map unArg cxs)
scope <- getScope
let re = getRange e
meta x = A.Underscore $ A.MetaInfo re scope Nothing (prettyShow x)
es <- insertMissingFields r meta fs cxs
args <- checkArguments_ ExpandLast re es (recTel def `apply` vs) >>= \case
(elims, remainingTel) | null remainingTel
, Just args <- allApplyElims elims -> return args
_ -> __IMPOSSIBLE__
reportSDoc "tc.term.rec" 20 $ text $ "finished record expression"
return $ Con con ConORec (map Apply args)
_ -> typeError $ ShouldBeRecordType t
where
guessRecordType t = do
let fields = [ x | Left (FieldAssignment x _) <- mfs ]
rs <- findPossibleRecords fields
case rs of
[] -> case fields of
[] -> genericError "There are no records in scope"
[f] -> genericError $ "There is no known record with the field " ++ prettyShow f
_ -> genericError $ "There is no known record with the fields " ++ unwords (map prettyShow fields)
[r] -> do
def <- getConstInfo r
let rt = defType def
vs <- newArgsMeta rt
target <- reduce $ piApply rt vs
s <- case unEl target of
Sort s -> return s
v -> do
reportSDoc "impossible" 10 $ vcat
[ "The impossible happened when checking record expression against meta"
, "Candidate record type r = " <+> prettyTCM r
, "Type of r = " <+> prettyTCM rt
, "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 cmp v inferred t
_:_:_ -> do
reportSDoc "tc.term.expr.rec" 10 $ sep
[ "Postponing type checking of"
, nest 2 $ prettyA e <+> ":" <+> prettyTCM t
]
postponeTypeCheckingProblem_ $ CheckExpr cmp e t
checkRecordUpdate
:: Comparison
-> A.ExprInfo
-> A.Expr
-> A.Assigns
-> A.Expr
-> Type
-> TCM Term
checkRecordUpdate cmp ei recexpr fs e t = do
case unEl t of
Def r vs -> do
v <- checkExpr' cmp recexpr t
name <- freshNoName (getRange recexpr)
addLetBinding defaultArgInfo name v t $ do
projs <- map argFromDom . recFields <$> getRecordDef r
disambiguateRecordFields (map _nameFieldA fs) (map unArg projs)
axs <- map argFromDom <$> getRecordFieldNames r
let xs = map unArg axs
es <- orderFields r (\ _ -> Nothing) axs $ map (\ (FieldAssignment x e) -> (x, Just e)) fs
let es' = zipWith (replaceFields name ei) projs es
checkExpr' cmp (A.Rec ei [ Left (FieldAssignment x e) | (x, Just e) <- zip xs es' ]) t
MetaV _ _ -> do
inferred <- inferExpr recexpr >>= reduce . snd
case unEl inferred of
MetaV _ _ -> postponeTypeCheckingProblem_ $ CheckExpr cmp e t
_ -> do
v <- checkExpr' cmp e inferred
coerce cmp 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 | visible a =
Just $ A.App (A.defaultAppInfo $ getRange 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 CmpEq (Lit lit) t' 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 = checkExpr' CmpLeq
checkExpr'
:: Comparison
-> A.Expr
-> Type
-> TCM Term
checkExpr' cmp e t =
verboseBracket "tc.term.expr.top" 5 "checkExpr" $
reportResult "tc.term.expr.top" 15 (\ v -> vcat
[ "checkExpr" <?> fsep [ prettyTCM e, ":", prettyTCM t ]
, " returns" <?> prettyTCM v ]) $
traceCall (CheckExprCall cmp e t) $ localScope $ doExpandLast $ unfoldInlined =<< do
reportSDoc "tc.term.expr.top" 15 $
"Checking" <+> sep
[ fsep [ prettyTCM e, ":", prettyTCM t ]
, nest 2 $ "at " <+> (text . prettyShow =<< getCurrentRange)
]
reportSDoc "tc.term.expr.top.detailed" 80 $
"Checking" <+> fsep [ prettyTCM e, ":", text (show t) ]
tReduced <- reduce t
reportSDoc "tc.term.expr.top" 15 $
" --> " <+> prettyTCM tReduced
e <- scopedExpr e
irrelevantIfProp <- isPropM t >>= \case
True -> do
let mod = defaultModality { modRelevance = Irrelevant }
return $ fmap dontCare . applyModalityToContext mod
False -> return id
irrelevantIfProp $ tryInsertHiddenLambda e tReduced $ case e of
A.ScopedExpr scope e -> __IMPOSSIBLE__
A.QuestionMark i ii -> checkQuestionMark (newValueMeta' RunMetaOccursCheck) cmp t i ii
A.Underscore i -> checkUnderscore cmp t 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
(genericError "Use --universe-polymorphism to enable level arguments to Set")
$ do
n <- applyRelevanceToContext NonStrict $ checkLevel arg
reportSDoc "tc.univ.poly" 10 $
"checking Set " <+> prettyTCM n <+>
"against" <+> prettyTCM t
coerce cmp (Sort $ Type n) (sort $ Type $ levelSuc n) t
A.App i s arg@(Arg ai l)
| A.Prop _ 0 <- unScope s, visible ai ->
ifNotM hasUniversePolymorphism
(genericError "Use --universe-polymorphism to enable level arguments to Prop")
$ do
n <- applyRelevanceToContext NonStrict $ checkLevel arg
reportSDoc "tc.univ.poly" 10 $
"checking Prop " <+> prettyTCM n <+>
"against" <+> prettyTCM t
coerce cmp (Sort $ Prop n) (sort $ Type $ levelSuc 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 p) | Just x <- getUnambiguous p = return x
quoted (A.Proj o p) =
genericError $ "quote: Ambigous name: " ++ prettyShow (unAmbQ p)
quoted (A.Con c) | Just x <- getUnambiguous c = return x
quoted (A.Con c) =
genericError $ "quote: Ambigous name: " ++ prettyShow (unAmbQ c)
quoted (A.ScopedExpr _ e) = quoted e
quoted _ =
genericError "quote: not a defined name"
x <- quoted (namedThing e)
ty <- qNameType
coerce cmp (quoteName x) ty t
| A.QuoteTerm _ <- unScope q -> do
(et, _) <- inferExpr (namedThing e)
doQuoteTerm cmp et t
A.Quote{} -> genericError "quote must be applied to a defined name"
A.QuoteTerm{} -> genericError "quoteTerm must be applied to a term"
A.Unquote{} -> genericError "unquote must be applied to a term"
A.AbsurdLam i h -> checkAbsurdLambda cmp i h e t
A.ExtendedLam i di qname cs -> checkExtendedLambda cmp i di qname cs e t
A.Lam i (A.DomainFull b) e -> checkLambda cmp b e t
A.Lam i (A.DomainFree _ x) e0
| isNothing (nameOf $ unArg x) && isNothing (A.binderPattern $ namedArg x) ->
checkExpr' cmp (A.Lam i (domainFree (getArgInfo x) $ fmap A.unBind $ namedArg x) e0) t
| otherwise -> typeError $ NotImplemented "named arguments in lambdas"
A.Lit lit -> checkLiteral lit t
A.Let i ds e -> checkLetBindings ds $ checkExpr' cmp e t
A.Pi _ tel e | null tel -> checkExpr' cmp 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)
checkTelePiSort t'
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 $ "t =" <+> prettyTCM t'
, nest 2 $ "cxt =" <+> (prettyTCM =<< getContextTelescope)
]
coerce cmp v (sort s) t
A.Generalized s e -> do
(_, t') <- generalizeType s $ isType_ e
noFunctionsIntoSize t' t'
let s = getSort t'
v = unEl t'
when (s == Inf) $ reportSDoc "tc.term.sort" 20 $
vcat [ text ("reduced to omega:")
, nest 2 $ "t =" <+> prettyTCM t'
, nest 2 $ "cxt =" <+> (prettyTCM =<< getContextTelescope)
]
coerce cmp v (sort s) t
A.Fun _ (Arg info a) b -> do
a' <- isType_ a
let adom = defaultArgDom info a'
b' <- isType_ b
s <- inferFunSort adom (getSort b')
let v = Pi adom (NoAbs underscore b')
noFunctionsIntoSize b' $ El s v
coerce cmp v (sort s) t
A.Set _ n -> do
coerce cmp (Sort $ mkType n) (sort $ mkType $ n + 1) t
A.Prop _ n -> do
unlessM isPropEnabled $ typeError NeedOptionProp
coerce cmp (Sort $ mkProp n) (sort $ mkType $ n + 1) t
A.Rec _ fs -> checkRecordExpression cmp fs e t
A.RecUpdate ei recexpr fs -> checkRecordUpdate cmp ei recexpr fs e tReduced
A.DontCare e ->
ifM ((Irrelevant ==) <$> asksTC getRelevance)
(dontCare <$> do applyRelevanceToContext Irrelevant $ checkExpr' cmp e t)
(internalError "DontCare may only appear in irrelevant contexts")
A.ETel _ -> __IMPOSSIBLE__
A.Dot{} -> genericError "Invalid dotted expression"
_ | Application hd args <- appView e -> checkApplication cmp hd args e t
`catchIlltypedPatternBlockedOnMeta` \ (err, x) -> do
reportSDoc "tc.term" 50 $ vcat $
[ "checking pattern got stuck on meta: " <+> text (show x) ]
postponeTypeCheckingProblem (CheckExpr cmp e t) $ isInstantiatedMeta x
where
tryInsertHiddenLambda
:: A.Expr
-> Type
-> TCM Term
-> TCM Term
tryInsertHiddenLambda e tReduced fallback
| Pi (Dom{domInfo = info, unDom = a}) b <- unEl tReduced
, let h = getHiding info
, notVisible h
, not (hiddenLambdaOrHole h e)
= do
let proceed = doInsert (setOrigin Inserted info) $ absName b
expandHidden <- asksTC envExpandLast
if definitelyIntroduction then proceed else
if expandHidden == ReallyDontExpandLast then fallback else do
reduce a >>= isSizeType >>= \case
Just (BoundedLt u) -> ifBlocked u (\ _ _ -> fallback) $ \ _ v -> do
ifM (checkSizeNeverZero v) proceed fallback
`catchError` \_ -> fallback
_ -> proceed
| otherwise = fallback
where
re = getRange e
rx = caseMaybe (rStart re) noRange $ \ pos -> posToRange pos pos
doInsert info y = do
x <- C.setNotInScope <$> freshName rx y
reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda"
checkExpr' cmp (A.Lam (A.ExprRange re) (domainFree info $ A.mkBinder x) e) tReduced
hiddenLambdaOrHole h e = case e of
A.AbsurdLam _ h' -> sameHiding h h'
A.ExtendedLam _ _ _ cls -> any hiddenLHS cls
A.Lam _ bind _ -> sameHiding h bind
A.QuestionMark{} -> True
_ -> False
hiddenLHS (A.Clause (A.LHS _ (A.LHSHead _ (a : _))) _ _ _ _) = notVisible a
hiddenLHS _ = False
definitelyIntroduction = case e of
A.Lam{} -> True
A.AbsurdLam{} -> True
A.Lit{} -> True
A.Pi{} -> True
A.Fun{} -> True
A.Set{} -> True
A.Prop{} -> True
A.Rec{} -> True
A.RecUpdate{} -> True
A.ScopedExpr{} -> __IMPOSSIBLE__
A.ETel{} -> __IMPOSSIBLE__
_ -> False
doQuoteTerm :: Comparison -> Term -> Type -> TCM Term
doQuoteTerm cmp et t = do
et' <- etaContract =<< instantiateFull et
case allMetasList et' of
[] -> do
q <- quoteTerm et'
ty <- el primAgdaTerm
coerce cmp q ty t
metas -> postponeTypeCheckingProblem (DoQuoteTerm cmp et t) $ andM $ map isInstantiatedMeta metas
unquoteM :: A.Expr -> Term -> Type -> TCM ()
unquoteM tacA hole holeType = do
tac <- checkExpr tacA =<< (el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit))
inFreshModuleIfFreeParams $ unquoteTactic tac hole holeType
unquoteTactic :: Term -> Term -> Type -> TCM ()
unquoteTactic tac hole goal = do
reportSDoc "tc.term.tactic" 40 $ sep
[ "Running tactic" <+> prettyTCM tac
, nest 2 $ "on" <+> prettyTCM hole <+> ":" <+> prettyTCM goal ]
ok <- runUnquoteM $ unquoteTCM tac hole
case ok of
Left (BlockedOnMeta oldState x) -> do
putTC oldState
mi <- lookupMeta' x
(r, meta) <- case mi of
Nothing -> do
(noRange,) . firstMeta <$> instantiateFull goal
Just mi -> return (getRange mi, Just x)
setCurrentRange r $
addConstraint (UnquoteTactic meta tac hole goal)
Left err -> typeError $ UnquoteFailed err
Right _ -> return ()
checkQuestionMark
:: (Comparison -> Type -> TCM (MetaId, Term))
-> Comparison
-> Type
-> A.MetaInfo
-> InteractionId
-> TCM Term
checkQuestionMark new cmp t0 i ii = do
reportSDoc "tc.interaction" 20 $ sep
[ "Found interaction point"
, text . show =<< asksTC (^. lensIsAbstract)
, pretty ii
, ":"
, prettyTCM t0
]
reportSDoc "tc.interaction" 60 $ sep
[ "Raw:"
, text (show t0)
]
checkMeta (newQuestionMark' new ii) cmp t0 i
checkUnderscore :: Comparison -> Type -> A.MetaInfo -> TCM Term
checkUnderscore = checkMeta (newValueMeta RunMetaOccursCheck)
checkMeta :: (Comparison -> Type -> TCM (MetaId, Term)) -> Comparison -> Type -> A.MetaInfo -> TCM Term
checkMeta newMeta cmp t i = fst <$> checkOrInferMeta newMeta (Just (cmp , t)) i
inferMeta :: (Comparison -> Type -> TCM (MetaId, Term)) -> A.MetaInfo -> TCM (Elims -> Term, Type)
inferMeta newMeta i = mapFst applyE <$> checkOrInferMeta newMeta Nothing i
checkOrInferMeta
:: (Comparison -> Type -> TCM (MetaId, Term))
-> Maybe (Comparison , Type)
-> A.MetaInfo
-> TCM (Term, Type)
checkOrInferMeta newMeta mt i = do
case A.metaNumber i of
Nothing -> do
setScope (A.metaScope i)
(cmp , t) <- maybe ((CmpEq,) <$> workOnTypes newTypeMeta_) return mt
(x, v) <- newMeta cmp t
setMetaNameSuggestion x (A.metaNameSuggestion i)
return (v, t)
Just x -> do
let v = MetaV x []
reportSDoc "tc.meta.check" 20 $
"checking existing meta " <+> prettyTCM v
t' <- metaType x
reportSDoc "tc.meta.check" 20 $
nest 2 $ "of type " <+> prettyTCM t'
case mt of
Nothing -> return (v, t')
Just (cmp , t) -> (,t) <$> coerce cmp v t' t
domainFree :: ArgInfo -> A.Binder' A.Name -> A.LamBinding
domainFree info x =
A.DomainFull $ A.mkTBind r [unnamedArg info $ fmap A.mkBindName x]
$ A.Underscore underscoreInfo
where
r = getRange x
underscoreInfo = A.MetaInfo
{ A.metaRange = r
, A.metaScope = emptyScopeInfo
, A.metaNumber = Nothing
, A.metaNameSuggestion = prettyShow $ A.nameConcrete $ A.binderName x
}
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
"Invalid projection parameter " <+> prettyA arg
checkKnownArgument arg (Arg _ v : vs) t = do
(dom@Dom{ unDom = a }, b) <- mustBePi t
if not $ fromMaybe __IMPOSSIBLE__ $ fittingNamedArg arg dom
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 = bareNameWithDefault "" e0
traceCall (CheckExprCall CmpLeq e t0) $ do
reportSDoc "tc.term.args.named" 15 $ do
"Checking named arg" <+> sep
[ fsep [ prettyTCM arg, ":", prettyTCM t0 ]
]
reportSLn "tc.term.args.named" 75 $ " arg = " ++ show (deepUnscope arg)
let checkU = checkMeta (newMetaArg (setHiding Hidden info) x) CmpLeq t0
let checkQ = checkQuestionMark (newInteractionMetaArg (setHiding Hidden info) x) CmpLeq 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
inferExpr :: A.Expr -> TCM (Term, Type)
inferExpr = inferExpr' DontExpandLast
inferExpr' :: ExpandHidden -> A.Expr -> TCM (Term, Type)
inferExpr' exh e = traceCall (InferExpr e) $ do
let Application hd args = appView e
reportSDoc "tc.infer" 30 $ vcat
[ "inferExpr': appView of " <+> prettyA e
, " hd = " <+> prettyA hd
, " args = " <+> prettyAs args
]
reportSDoc "tc.infer" 60 $ vcat
[ text $ " hd (raw) = " ++ show hd
]
inferApplication exh hd args e
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 :: Comparison -> A.Expr -> Type -> TCM Term
checkDontExpandLast cmp e t = case e of
_ | Application hd args <- appView e, defOrVar hd ->
traceCall (CheckExprCall cmp e t) $ localScope $ dontExpandLast $ do
checkApplication cmp hd args e t
_ -> checkExpr' cmp 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 $ "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 v0 of
Var i [] -> whenM (isModuleFreeVar i) $ do
reportSDoc "tc.with.infer" 80 $ vcat
[ text $ "with expression is variable " ++ show i
, "current modules = " <+> do text . show =<< currentModule
, "current module free vars = " <+> do text . show =<< getCurrentModuleFreeVars
, "context size = " <+> do text . show =<< getContextSize
, "current context = " <+> do prettyTCM =<< getContextTelescope
]
typeError $ WithOnFreeVariable e v0
_ -> return ()
TelV tel t0 <- telViewUpTo' (-1) (not . visible) t
case unEl t0 of
Def d vs -> do
res <- isDataOrRecordType d
case res of
Nothing -> return (v, t)
Just{} -> do
(args, t1) <- implicitArgs (-1) notVisible 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 =
traceCall (CheckLetBinding b) $ do
t <- isType_ t
v <- applyModalityToContext info $ checkDontExpandLast CmpLeq e t
addLetBinding info (A.unBind x) v t ret
checkLetBinding b@(A.LetPatBind i p e) ret =
traceCall (CheckLetBinding b) $ do
p <- expandPatternSynonyms p
(v, t) <- inferExpr' ExpandLast e
let
t0 = El (getSort t) $ Pi (defaultDom t) (NoAbs underscore __DUMMY_TYPE__)
p0 = Arg defaultArgInfo (Named Nothing p)
reportSDoc "tc.term.let.pattern" 10 $ vcat
[ "let-binding pattern p at type t"
, nest 2 $ vcat
[ "p (A) =" <+> prettyA p
, "t =" <+> prettyTCM t
, "cxtRel=" <+> do pretty =<< asksTC getRelevance
, "cxtQnt=" <+> do pretty =<< asksTC getQuantity
]
]
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
[ "p (I) =" <+> prettyTCM p
, "delta =" <+> prettyTCM delta
, "cxtRel=" <+> do pretty =<< asksTC getRelevance
, "cxtQnt=" <+> do pretty =<< asksTC getQuantity
]
reportSDoc "tc.term.let.pattern" 80 $ nest 2 $ vcat
[ "p (I) =" <+> (text . show) p
]
fs <- recordPatternToProjections p
cxt0 <- getContext
let (binds, cxt) = splitAt (size delta) cxt0
toDrop = length binds
sigma = map ($ v) fs
sub = parallelS (reverse sigma)
updateContext sub (drop toDrop) $ do
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ "delta =" <+> prettyTCM delta
, "binds =" <+> prettyTCM binds
]
let fdelta = flattenTel delta
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
[ "fdelta =" <+> addContext delta (prettyTCM 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 $ List.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
[ "context =" <+> (prettyTCM =<< getContextTelescope)
, "module =" <+> (prettyTCM =<< currentModule)
, "fv =" <+> (text $ show fv)
]
checkSectionApplication i x modapp copyInfo
withAnonymousModule x new ret
checkLetBinding A.LetOpen{} ret = ret
checkLetBinding (A.LetDeclaredVariable _) ret = ret