{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Def where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), mapM, null )
#else
import Prelude hiding ( mapM, null )
#endif
import Control.Arrow ((***))
import Control.Monad.State hiding (forM, mapM)
import Control.Monad.Reader hiding (forM, mapM)
import Data.Function
import Data.Maybe
import Data.Traversable (Traversable, traverse, forM, mapM)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete (exprFieldA)
import Agda.Syntax.Position
import Agda.Syntax.Abstract.Pattern as A
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern as I
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Fixity
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Info
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Inlining
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Patterns.Abstract (expandPatternSynonyms)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.CheckInternal (checkType, inferSort)
import Agda.TypeChecking.With
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.CompiledClause (CompiledClauses'(..), hasProjectionPatterns)
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Primitive hiding (Nat)
import Agda.TypeChecking.Rules.Term ( checkExpr, inferExpr, inferExprForWith, checkDontExpandLast, checkTelescope, catchIlltypedPatternBlockedOnMeta )
import Agda.TypeChecking.Rules.LHS ( checkLeftHandSide, LHSResult(..), bindAsPatterns )
import Agda.TypeChecking.Rules.LHS.Problem ( AsBinding(..) )
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl ( checkDecls )
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Maybe ( whenNothing )
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty ( prettyShow )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
checkFunDef :: Delayed -> Info.DefInfo -> QName -> [A.Clause] -> TCM ()
checkFunDef delayed i name cs = do
t <- typeOfConst name
info <- flip setRelevance defaultArgInfo <$> relOfConst name
case isAlias cs t of
Just (e, mc, x) ->
traceCall (CheckFunDefCall (getRange i) (qnameName name) cs) $ do
whenM (isFrozen x) $ unfreezeMeta x
checkAlias t info delayed i name e mc
_ -> checkFunDef' t info delayed Nothing Nothing i name cs
ismacro <- isMacro . theDef <$> getConstInfo name
when (ismacro || Info.defMacro i == MacroDef) $ checkMacroType t
`catchIlltypedPatternBlockedOnMeta` \ (err, x) -> do
reportSDoc "tc.def" 20 $ vcat $
[ text "checking function definition got stuck on meta: " <+> text (show x) ]
addConstraint $ CheckFunDef delayed i name cs
checkMacroType :: Type -> TCM ()
checkMacroType t = do
t' <- normalise t
TelV tel tr <- telView t'
let telList = telToList tel
resType = abstract (telFromList (drop (length telList - 1) telList)) tr
expectedType <- el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit)
equalType resType expectedType
`catchError` \ _ -> typeError . GenericDocError =<< sep [ text "Result type of a macro must be"
, nest 2 $ prettyTCM expectedType ]
isAlias :: [A.Clause] -> Type -> Maybe (A.Expr, Maybe C.Expr, MetaId)
isAlias cs t =
case trivialClause cs of
Just (e, mc) | Just x <- isMeta (unEl t) -> Just (e, mc, x)
_ -> Nothing
where
isMeta (MetaV x _) = Just x
isMeta _ = Nothing
trivialClause [A.Clause (A.LHS i (A.LHSHead f [])) _ (A.RHS e mc) (A.WhereDecls _ []) _] = Just (e, mc)
trivialClause _ = Nothing
checkAlias :: Type -> ArgInfo -> Delayed -> Info.DefInfo -> QName -> A.Expr -> Maybe C.Expr -> TCM ()
checkAlias t' ai delayed i name e mc = atClause name 0 (A.RHS e mc) $ do
reportSDoc "tc.def.alias" 10 $ text "checkAlias" <+> vcat
[ text (prettyShow name) <+> colon <+> prettyTCM t'
, text (prettyShow name) <+> equals <+> prettyTCM e
]
v <- applyRelevanceToContext (getRelevance ai) $ checkDontExpandLast e t'
let t = t'
reportSDoc "tc.def.alias" 20 $ text "checkAlias: finished checking"
solveSizeConstraints DontDefaultToInfty
v <- instantiateFull v
let bodyMod = case getRelevance ai of
Irrelevant -> dontCare
_ -> id
addConstant name $ defaultDefn ai name t
$ set funMacro (Info.defMacro i == MacroDef) $
emptyFunction
{ funClauses = [ Clause
{ clauseLHSRange = getRange i
, clauseFullRange = getRange i
, clauseTel = EmptyTel
, namedClausePats = []
, clauseBody = Just $ bodyMod v
, clauseType = Just $ Arg ai t
, clauseCatchall = False
, clauseUnreachable = Just False
} ]
, funCompiled = Just $ Done [] $ bodyMod v
, funDelayed = delayed
, funAbstr = Info.defAbstract i
}
when (Info.defInstance i == InstanceDef) $ do
addTypedInstance name t
reportSDoc "tc.def.alias" 20 $ text "checkAlias: leaving"
checkFunDef' :: Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> Info.DefInfo
-> QName
-> [A.Clause]
-> TCM ()
checkFunDef' t ai delayed extlam with i name cs =
checkFunDefS t ai delayed extlam with i name Nothing cs
checkFunDefS :: Type
-> ArgInfo
-> Delayed
-> Maybe ExtLamInfo
-> Maybe QName
-> Info.DefInfo
-> QName
-> Maybe Substitution
-> [A.Clause]
-> TCM ()
checkFunDefS t ai delayed extlam with i name withSub cs = do
traceCall (CheckFunDefCall (getRange i) (qnameName name) cs) $ do
reportSDoc "tc.def.fun" 10 $
sep [ text "checking body of" <+> prettyTCM name
, nest 2 $ text ":" <+> prettyTCM t
, nest 2 $ text "full type:" <+> (prettyTCM . defType =<< getConstInfo name)
]
reportSDoc "tc.def.fun" 70 $
sep $ [ text "clauses:" ] ++ map (nest 2 . text . show . A.deepUnscope) cs
cs <- return $ map A.lhsToSpine cs
reportSDoc "tc.def.fun" 70 $
sep $ [ text "spine clauses:" ] ++ map (nest 2 . text . show . A.deepUnscope) cs
cs <- traceCall NoHighlighting $ do
forM (zip cs [0..]) $ \ (c, clauseNo) -> do
atClause name clauseNo (A.clauseRHS c) $ do
c <- applyRelevanceToContext (getRelevance ai) $ do
checkClause t withSub c
whenNothing extlam $ solveSizeConstraints DontDefaultToInfty
inTopContext $ addClauses name [c]
return c
reportSDoc "tc.def.fun" 70 $ inTopContext $ do
sep $ [ text "checked clauses:" ] ++ map (nest 2 . text . show) cs
modifyFunClauses name (const [])
reportSDoc "tc.cc" 25 $ inTopContext $ do
sep [ text "clauses before injectivity test"
, nest 2 $ prettyTCM $ map (QNamed name) cs
]
reportSDoc "tc.cc" 60 $ inTopContext $ do
sep [ text "raw clauses: "
, nest 2 $ sep $ map (text . show . QNamed name) cs
]
cs <- instantiateFull cs
reportSLn "tc.inj.def" 20 $ "checkFunDef': checking injectivity..."
inv <- Bench.billTo [Bench.Injectivity] $
checkInjectivity name cs
reportSDoc "tc.cc" 15 $ inTopContext $ do
sep [ text "clauses before compilation"
, nest 2 $ sep $ map (prettyTCM . QNamed name) cs
]
inTopContext $ addClauses name cs
fullType <- flip telePi t <$> getContextTelescope
cc <- Bench.billTo [Bench.Coverage] $
inTopContext $ compileClauses (Just (name, fullType)) cs
cs <- defClauses <$> getConstInfo name
reportSDoc "tc.cc" 60 $ inTopContext $ do
sep [ text "compiled clauses of" <+> prettyTCM name
, nest 2 $ pretty cc
]
ismacro <- isMacro . theDef <$> getConstInfo name
inTopContext $ addConstant name =<< do
defn <- autoInline $
set funMacro (ismacro || Info.defMacro i == MacroDef) $
emptyFunction
{ funClauses = cs
, funCompiled = Just cc
, funDelayed = delayed
, funInv = inv
, funAbstr = Info.defAbstract i
, funExtLam = extlam
, funWith = with
, funCopatternLHS = hasProjectionPatterns cc
}
useTerPragma $ defaultDefn ai name fullType defn
reportSDoc "tc.def.fun" 10 $ do
sep [ text "added " <+> prettyTCM name <+> text ":"
, nest 2 $ prettyTCM . defType =<< getConstInfo name
]
useTerPragma :: Definition -> TCM Definition
useTerPragma def@Defn{ defName = name, theDef = fun@Function{}} = do
tc <- asks envTerminationCheck
let terminates = case tc of
NonTerminating -> Just False
Terminating -> Just True
_ -> Nothing
reportSLn "tc.fundef" 30 $ unlines $
[ "funTerminates of " ++ prettyShow name ++ " set to " ++ show terminates
, " tc = " ++ show tc
]
return $ def { theDef = fun { funTerminates = terminates }}
useTerPragma def = return def
insertPatterns :: [A.Pattern] -> A.RHS -> A.RHS
insertPatterns pats = \case
A.WithRHS aux es cs -> A.WithRHS aux es $ for cs $
\ (A.Clause (A.LHS info core) spats rhs ds catchall) ->
A.Clause (A.LHS info (insertPatternsLHSCore pats core)) spats (insertPatterns pats rhs) ds catchall
A.RewriteRHS qes spats rhs wh -> A.RewriteRHS qes spats (insertPatterns pats rhs) wh
rhs@A.AbsurdRHS -> rhs
rhs@A.RHS{} -> rhs
insertPatternsLHSCore :: [A.Pattern] -> A.LHSCore -> A.LHSCore
insertPatternsLHSCore pats = \case
A.LHSWith core wps [] -> A.LHSWith core (pats ++ wps) []
core -> A.LHSWith core pats []
data WithFunctionProblem
= NoWithFunction
| WithFunction
{ wfParentName :: QName
, wfName :: QName
, wfParentType :: Type
, wfParentTel :: Telescope
, wfBeforeTel :: Telescope
, wfAfterTel :: Telescope
, wfExprs :: [Term]
, wfExprTypes :: [EqualityView]
, wfRHSType :: Type
, wfParentPats :: [NamedArg DeBruijnPattern]
, wfParentParams :: Nat
, wfPermSplit :: Permutation
, wfPermParent :: Permutation
, wfPermFinal :: Permutation
, wfClauses :: [A.Clause]
}
checkClause
:: Type
-> Maybe Substitution
-> A.SpineClause
-> TCM Clause
checkClause t withSub c@(A.Clause (A.SpineLHS i x aps) strippedPats rhs0 wh catchall) = do
reportSDoc "tc.lhs.top" 30 $ text "Checking clause" $$ prettyA c
unlessNull (trailingWithPatterns aps) $ \ withPats -> do
typeError $ UnexpectedWithPatterns $ map namedArg withPats
traceCall (CheckClause t c) $ do
aps <- expandPatternSynonyms aps
cxtNames <- reverse . map (fst . unDom) <$> getContext
when (not $ null strippedPats) $ reportSDoc "tc.lhs.top" 50 $
text "strippedPats:" <+> vcat [ prettyA p <+> text "=" <+> prettyTCM v <+> text ":" <+> prettyTCM a | A.ProblemEq p v a <- strippedPats ]
checkLeftHandSide (CheckPatternShadowing c) (Just x) aps t withSub strippedPats $ \ lhsResult@(LHSResult npars delta ps absurdPat trhs patSubst asb) -> do
t' <- case withSub of
Just{} -> return t
Nothing -> do
theta <- lookupSection (qnameModule x)
return $ abstract theta t
let rhs = updateRHS rhs0
updateRHS rhs@A.RHS{} = rhs
updateRHS rhs@A.AbsurdRHS{} = rhs
updateRHS (A.WithRHS q es cs) = A.WithRHS q es (map updateClause cs)
updateRHS (A.RewriteRHS qes spats rhs wh) =
A.RewriteRHS qes (applySubst patSubst spats) (updateRHS rhs) wh
updateClause (A.Clause f spats rhs wh ca) =
A.Clause f (applySubst patSubst spats) (updateRHS rhs) wh ca
(body, with) <- bindAsPatterns asb $ checkWhere wh $ checkRHS i x aps t' lhsResult rhs
inTopContext $ Bench.billTo [Bench.Typing, Bench.With] $ checkWithFunction cxtNames with
reportSDoc "tc.lhs.top" 10 $ vcat
[ text "Clause before translation:"
, nest 2 $ vcat
[ text "delta =" <+> do escapeContext (size delta) $ prettyTCM delta
, text "ps =" <+> do P.fsep <$> prettyTCMPatterns ps
, text "body =" <+> maybe (text "_|_") prettyTCM body
]
]
reportSDoc "tc.lhs.top" 60 $ escapeContext (size delta) $ vcat
[ text "Clause before translation (raw):"
, nest 2 $ vcat
[ text "ps =" <+> text (show ps)
, text "body =" <+> text (show body)
]
]
rel <- asks envRelevance
let bodyMod body = case rel of
Irrelevant -> dontCare <$> body
_ -> body
let catchall' = catchall || isNothing body
return $
Clause { clauseLHSRange = getRange i
, clauseFullRange = getRange c
, clauseTel = killRange delta
, namedClausePats = ps
, clauseBody = bodyMod body
, clauseType = Just trhs
, clauseCatchall = catchall'
, clauseUnreachable = Nothing
}
checkRHS
:: LHSInfo
-> QName
-> [NamedArg A.Pattern]
-> Type
-> LHSResult
-> A.RHS
-> TCM (Maybe Term, WithFunctionProblem)
checkRHS i x aps t lhsResult@(LHSResult _ delta ps absurdPat trhs _ _asb) rhs0 = handleRHS rhs0
where
handleRHS rhs =
case rhs of
A.RHS e _ -> Bench.billTo [Bench.Typing, Bench.CheckRHS] $ do
when absurdPat $ typeError $ AbsurdPatternRequiresNoRHS aps
v <- checkExpr e $ unArg trhs
return (Just v, NoWithFunction)
A.AbsurdRHS -> do
unless absurdPat $ typeError $ NoRHSRequiresAbsurdPattern aps
return (Nothing, NoWithFunction)
A.RewriteRHS [] strippedPats rhs wh -> checkWhere wh $ handleRHS rhs
A.RewriteRHS ((qname,eq):qes) strippedPats rhs wh -> do
st <- get
let recurse = do
st' <- get
let sameIP = (==) `on` (^.stInteractionPoints)
when (sameIP st st') $ put st
handleRHS $ A.RewriteRHS qes strippedPats rhs wh
(proof, eqt) <- inferExpr eq
solveSizeConstraints DefaultToInfty
t' <- reduce =<< instantiateFull eqt
(eqt,rewriteType,rewriteFrom,rewriteTo) <- equalityView t' >>= \case
eqt@(EqualityType _s _eq _params (Arg _ dom) a b) -> do
s <- inferSort dom
return (eqt, El s dom, unArg a, unArg b)
OtherType{} -> typeError . GenericDocError =<< do
text "Cannot rewrite by equation of type" <+> prettyTCM t'
Con reflCon _ [] <- primRefl
reflInfo <- fmap (setOrigin Inserted) <$> getReflArgInfo reflCon
let reflPat = A.ConP (ConPatInfo ConOCon patNoRange False) (unambiguous $ conName reflCon) $
maybeToList $ fmap (\ ai -> Arg ai $ unnamed $ A.WildP patNoRange) reflInfo
let isReflexive = tryConversion $ dontAssignMetas $
equalTerm rewriteType rewriteFrom rewriteTo
(pats, withExpr, withType) <- do
ifM isReflexive
(return ([ reflPat ], proof, OtherType t'))
(return ([ A.WildP patNoRange, reflPat ], proof, eqt))
let rhs' = insertPatterns pats rhs
(rhs'', outerWhere)
| null qes = (rhs', wh)
| otherwise = (A.RewriteRHS qes strippedPats rhs' wh, A.noWhereDecls)
cl = A.Clause (A.LHS i $ insertPatternsLHSCore pats $ A.LHSHead x $ killRange aps)
strippedPats rhs'' outerWhere False
reportSDoc "tc.rewrite" 60 $ vcat
[ text "rewrite"
, text " rhs' = " <> (text . show) rhs'
]
checkWithRHS x qname t lhsResult [withExpr] [withType] [cl]
A.WithRHS aux es cs -> do
reportSDoc "tc.with.top" 15 $ vcat
[ text "TC.Rules.Def.checkclause reached A.WithRHS"
, sep $ prettyA aux : map (parens . prettyA) es
]
reportSDoc "tc.with.top" 20 $ do
nfv <- getCurrentModuleFreeVars
m <- currentModule
sep [ text "with function module:" <+>
prettyList (map prettyTCM $ mnameToList m)
, text $ "free variables: " ++ show nfv
]
(vs0, as) <- unzip <$> mapM inferExprForWith es
solveSizeConstraints DefaultToInfty
checkWithRHS x aux t lhsResult vs0 (map OtherType as) cs
checkWithRHS
:: QName
-> QName
-> Type
-> LHSResult
-> [Term]
-> [EqualityView]
-> [A.Clause]
-> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS x aux t (LHSResult npars delta ps _absurdPat trhs _ _asb) vs0 as cs = Bench.billTo [Bench.Typing, Bench.With] $ do
let withArgs = withArguments vs0 as
perm = fromMaybe __IMPOSSIBLE__ $ dbPatPerm ps
(vs, as) <- normalise (vs0, as)
reportSDoc "tc.with.top" 25 $ escapeContext (size delta) $ vcat
[ text "delta =" <+> prettyTCM delta
]
reportSDoc "tc.with.top" 25 $ vcat
[ text "vs =" <+> prettyTCM vs
, text "as =" <+> prettyTCM as
, text "perm =" <+> text (show perm)
]
(delta1, delta2, perm', t', as, vs) <- return $
splitTelForWith delta (unArg trhs) as vs
let finalPerm = composeP perm' perm
reportSLn "tc.with.top" 75 $ "delta = " ++ show delta
reportSDoc "tc.with.top" 25 $ escapeContext (size delta) $ vcat
[ text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> addContext delta1 (prettyTCM delta2)
]
reportSDoc "tc.with.top" 25 $ vcat
[ text "perm' =" <+> text (show perm')
, text "fPerm =" <+> text (show finalPerm)
]
us <- getContextArgs
let n = size us
m = size delta
(us0, us1') = splitAt (n - m) us
(us1, us2) = splitAt (size delta1) $ permute perm' us1'
v = Def aux $ map Apply $ us0 ++ us1 ++ map defaultArg withArgs ++ us2
addConstant aux =<< do
useTerPragma $ defaultDefn defaultArgInfo aux typeDontCare emptyFunction
reportSDoc "tc.with.top" 20 $
text " with arguments" <+> do escapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM vs)
reportSDoc "tc.with.top" 20 $
text " types" <+> do escapeContext (size delta) $ addContext delta1 $ prettyList (map prettyTCM as)
reportSDoc "tc.with.top" 20 $
text "with function call" <+> prettyTCM v
reportSDoc "tc.with.top" 20 $
text " context" <+> (prettyTCM =<< getContextTelescope)
reportSDoc "tc.with.top" 20 $
text " delta" <+> do escapeContext (size delta) $ prettyTCM delta
reportSDoc "tc.with.top" 20 $
text " delta1" <+> do escapeContext (size delta) $ prettyTCM delta1
reportSDoc "tc.with.top" 20 $
text " delta2" <+> do escapeContext (size delta) $ addContext delta1 $ prettyTCM delta2
reportSDoc "tc.with.top" 20 $
text " body" <+> prettyTCM v
return (Just v, WithFunction x aux t delta delta1 delta2 vs as t' ps npars perm' perm finalPerm cs)
checkWithFunction :: [Name] -> WithFunctionProblem -> TCM ()
checkWithFunction _ NoWithFunction = return ()
checkWithFunction cxtNames (WithFunction f aux t delta delta1 delta2 vs as b qs npars perm' perm finalPerm cs) = do
let
withSub :: Substitution
withSub = liftS (size delta2) (wkS (countWithArgs as) idS) `composeS` renaming __IMPOSSIBLE__ (reverseP perm')
reportSDoc "tc.with.top" 10 $ vcat
[ text "checkWithFunction"
, nest 2 $ vcat
[ text "delta1 =" <+> prettyTCM delta1
, text "delta2 =" <+> addContext delta1 (prettyTCM delta2)
, text "t =" <+> prettyTCM t
, text "as =" <+> addContext delta1 (prettyTCM as)
, text "vs =" <+> do addContext delta1 $ prettyTCM vs
, text "b =" <+> do addContext delta1 $ addContext delta2 $ prettyTCM b
, text "qs =" <+> do addContext delta $ prettyTCMPatternList qs
, text "perm' =" <+> text (show perm')
, text "perm =" <+> text (show perm)
, text "fperm =" <+> text (show finalPerm)
, text "withSub=" <+> text (show withSub)
]
]
delta1 <- normalise delta1
(withFunType, n) <- withFunctionType delta1 vs as delta2 b
reportSDoc "tc.with.type" 10 $ sep [ text "with-function type:", nest 2 $ prettyTCM withFunType ]
reportSDoc "tc.with.type" 50 $ sep [ text "with-function type:", nest 2 $ pretty withFunType ]
setCurrentRange cs
(traceCall NoHighlighting $
checkType withFunType)
`catchError` \err -> case err of
TypeError s e -> do
put s
wt <- reify withFunType
enterClosure e $ traceCall (CheckWithFunctionType wt) . typeError
err -> throwError err
df <- safeInTopContext $ makeOpen =<< withDisplayForm f aux delta1 delta2 n qs perm' perm
reportSLn "tc.with.top" 20 "created with display form"
case dget df of
Display n ts dt ->
reportSDoc "tc.with.top" 20 $ text "Display" <+> fsep
[ text (show n)
, prettyList $ map prettyTCM ts
, prettyTCM dt
]
addConstant aux =<< do
useTerPragma $ (defaultDefn defaultArgInfo aux withFunType emptyFunction)
{ defDisplay = [df] }
reportSDoc "tc.with.top" 10 $ sep
[ text "added with function" <+> (prettyTCM aux) <+> text "of type"
, nest 2 $ prettyTCM withFunType
, nest 2 $ text "-|" <+> (prettyTCM =<< getContextTelescope)
]
reportSDoc "tc.with.top" 70 $ vcat
[ nest 2 $ text $ "raw with func. type = " ++ show withFunType
]
cs <- return $ map (A.lhsToSpine) cs
cs <- buildWithFunction cxtNames f aux t delta qs npars withSub finalPerm (size delta1) n cs
cs <- return $ map (A.spineToLhs) cs
checkFunDefS withFunType defaultArgInfo NotDelayed Nothing (Just f) info aux (Just withSub) cs
where
info = Info.mkDefInfo (nameConcrete $ qnameName aux) noFixity' PublicAccess ConcreteDef (getRange cs)
checkWhere
:: A.WhereDeclarations
-> TCM a
-> TCM a
checkWhere wh@(A.WhereDecls whmod ds) ret = do
ensureNoNamedWhereInRefinedContext whmod
loop ds
where
loop ds = case ds of
[] -> ret
[A.ScopedDecl scope ds] -> withScope_ scope $ loop ds
[A.Section _ m tel ds] -> newSection m tel $ do
local (\ e -> e { envCheckingWhere = True }) $ do
checkDecls ds
ret
_ -> __IMPOSSIBLE__
ensureNoNamedWhereInRefinedContext Nothing = return ()
ensureNoNamedWhereInRefinedContext (Just m) = traceCall (CheckNamedWhere m) $ do
args <- map unArg <$> (moduleParamsToApply =<< currentModule)
unless (isWeakening args) $
genericDocError =<< do
names <- map (argNameToString . fst . unDom) . telToList <$>
(lookupSection =<< currentModule)
let pr x v = text (x ++ " =") <+> prettyTCM v
vcat
[ fsep (pwords $ "Named where-modules are not allowed when module parameters have been refined by pattern matching. " ++
"See https://github.com/agda/agda/issues/2897.")
, text $ "In this case the module parameter" ++
(if length args > 0 then "s have" else " has") ++
" been refined to"
, nest 2 $ vcat (zipWith pr names args) ]
where
isWeakening [] = True
isWeakening (Var i [] : args) = isWk (i - 1) args
where
isWk i [] = True
isWk i (Var j [] : args) = i == j && isWk (i - 1) args
isWk _ _ = False
isWeakening _ = False
newSection :: ModuleName -> A.Telescope -> TCM a -> TCM a
newSection m tel cont = do
reportSDoc "tc.section" 10 $
text "checking section" <+> prettyTCM m <+> fsep (map prettyAs tel)
checkTelescope tel $ \ tel' -> do
reportSDoc "tc.section" 10 $
text "adding section:" <+> prettyTCM m <+> text (show (size tel'))
addSection m
reportSDoc "tc.section" 10 $ inTopContext $
nest 4 $ text "actual tele:" <+> do prettyTCM =<< lookupSection m
withCurrentModule m cont
atClause :: QName -> Int -> A.RHS -> TCM a -> TCM a
atClause name i rhs = local $ \ e -> e { envClause = IPClause name i rhs }