{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Decl where
import Prelude hiding ( null )
import Control.Monad
import Control.Monad.Writer (tell)
import Data.Either (partitionEithers)
import qualified Data.Foldable as Fold
import qualified Data.List as List
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.IntSet as IntSet
import Data.Set (Set)
import Agda.Interaction.Highlighting.Generate
import Agda.Interaction.Options
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (deepUnscopeDecl, deepUnscopeDecls)
import Agda.Syntax.Internal
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Benchmark (MonadBench, Phase)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.IApplyConfluence
import Agda.TypeChecking.Generalize
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Level.Solve
import Agda.TypeChecking.Positivity
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.ProjectionLike
import Agda.TypeChecking.Unquote
import Agda.TypeChecking.Records
import Agda.TypeChecking.RecordPatterns
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rewriting
import Agda.TypeChecking.SizedTypes.Solve
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Rules.Application
import Agda.TypeChecking.Rules.Term
import Agda.TypeChecking.Rules.Data ( checkDataDef )
import Agda.TypeChecking.Rules.Record ( checkRecDef )
import Agda.TypeChecking.Rules.Def ( checkFunDef, newSection, useTerPragma )
import Agda.TypeChecking.Rules.Builtin
import Agda.TypeChecking.Rules.Display ( checkDisplayPragma )
import Agda.Termination.TermCheck
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size
import Agda.Utils.Update
import qualified Agda.Utils.SmallSet as SmallSet
import Agda.Utils.Impossible
checkDeclCached :: A.Declaration -> TCM ()
checkDeclCached d@A.ScopedDecl{} = checkDecl d
checkDeclCached d@(A.Section minfo mname (A.GeneralizeTel _ tbinds) _) = do
e <- readFromCachedLog
reportSLn "cache.decl" 10 $ "checkDeclCached: " ++ show (isJust e)
case e of
Just (EnterSection minfo' mname' tbinds', _)
| killRange minfo == killRange minfo' && mname == mname' && tbinds == tbinds' -> do
return ()
_ -> do
cleanCachedLog
writeToCurrentLog $ EnterSection minfo mname tbinds
checkDecl d
e' <- readFromCachedLog
case e' of
Just (LeaveSection mname', _) | mname == mname' -> do
return ()
_ -> do
cleanCachedLog
writeToCurrentLog $ LeaveSection mname
checkDeclCached d = do
e <- readFromCachedLog
reportSLn "cache.decl" 10 $ "checkDeclCached: " ++ show (isJust e)
case e of
(Just (Decl d',s)) | compareDecl d d' -> do
restorePostScopeState s
reportSLn "cache.decl" 50 $ "range: " ++ show (getRange d)
printSyntaxInfo (getRange d)
_ -> do
cleanCachedLog
checkDeclWrap d
writeToCurrentLog $ Decl d
where
compareDecl A.Section{} A.Section{} = __IMPOSSIBLE__
compareDecl A.ScopedDecl{} A.ScopedDecl{} = __IMPOSSIBLE__
compareDecl x y = x == y
ignoreChanges m = localCache $ do
cleanCachedLog
m
checkDeclWrap d@A.RecDef{} = ignoreChanges $ checkDecl d
checkDeclWrap d@A.Mutual{} = ignoreChanges $ checkDecl d
checkDeclWrap d = checkDecl d
checkDecls :: [A.Declaration] -> TCM ()
checkDecls ds = do
reportSLn "tc.decl" 45 $ "Checking " ++ show (length ds) ++ " declarations..."
mapM_ checkDecl ds
checkDecl :: A.Declaration -> TCM ()
checkDecl d = setCurrentRange d $ do
reportSDoc "tc.decl" 10 $ "checking declaration"
debugPrintDecl d
reportSDoc "tc.decl" 90 $ (text . show) (deepUnscopeDecl d)
reportSDoc "tc.decl" 10 $ prettyA d
let
none m = m $> Nothing
meta m = m $> Just (return ())
mutual i ds m = m <&> Just . uncurry (mutualChecks i d ds)
impossible m = m $> __IMPOSSIBLE__
(finalChecks, metas) <- metasCreatedBy $ case d of
A.Axiom{} -> meta $ checkTypeSignature d
A.Generalize s i info x e -> meta $ inConcreteMode $ checkGeneralize s i info x e
A.Field{} -> typeError FieldOutsideRecord
A.Primitive i x e -> meta $ checkPrimitive i x e
A.Mutual i ds -> mutual i ds $ checkMutual i ds
A.Section i x tel ds -> meta $ checkSection i x tel ds
A.Apply i x modapp ci _adir -> meta $ checkSectionApplication i x modapp ci
A.Import i x _adir -> none $ checkImport i x
A.Pragma i p -> none $ checkPragma i p
A.ScopedDecl scope ds -> none $ setScope scope >> mapM_ checkDeclCached ds
A.FunDef i x delayed cs -> impossible $ check x i $ checkFunDef delayed i x cs
A.DataDef i x uc ps cs -> impossible $ check x i $ checkDataDef i x uc ps cs
A.RecDef i x uc ind eta c ps tel cs -> impossible $ check x i $ do
checkRecDef i x uc ind eta c ps tel cs
blockId <- mutualBlockOf x
verboseS "tc.decl.mutual" 70 $ do
current <- asksTC envMutualBlock
unless (Just blockId == current) $ do
reportS "" 0
[ "mutual block id discrepancy for " ++ prettyShow x
, " current mut. bl. = " ++ show current
, " calculated mut. bl. = " ++ show blockId
]
return (blockId, Set.singleton x)
A.DataSig i x ps t -> impossible $ checkSig i x ps t
A.RecSig i x ps t -> none $ checkSig i x ps t
A.Open{} -> none $ return ()
A.PatternSynDef{} -> none $ return ()
A.UnquoteDecl mi is xs e -> checkMaybeAbstractly is $ checkUnquoteDecl mi is xs e
A.UnquoteDef is xs e -> impossible $ checkMaybeAbstractly is $ checkUnquoteDef is xs e
whenNothingM (asksTC envMutualBlock) $ do
highlight_ DontHightlightModuleContents d
whenM (optCumulativity <$> pragmaOptions) $ defaultLevelsToZero metas
whenJust finalChecks $ \ theMutualChecks -> do
reportSLn "tc.decl" 20 $ "Attempting to solve constraints before freezing."
wakeupConstraints_
checkingWhere <- asksTC envCheckingWhere
solveSizeConstraints $ if checkingWhere then DontDefaultToInfty else DefaultToInfty
wakeupConstraints_
case d of
A.Generalize{} -> pure ()
_ -> do
reportSLn "tc.decl" 20 $ "Freezing all metas."
void $ freezeMetas' $ \ (MetaId x) -> IntSet.member x metas
theMutualChecks
where
checkSig i x gtel t = checkTypeSignature' (Just gtel) $
A.Axiom A.NoFunSig i defaultArgInfo Nothing x t
check :: forall m i a
. ( MonadTCEnv m, MonadPretty m, MonadDebug m, MonadBench Phase m
, AnyIsAbstract i )
=> QName -> i -> m a -> m a
check x i m = Bench.billTo [Bench.Definition x] $ do
reportSDoc "tc.decl" 5 $ ("Checking" <+> prettyTCM x) <> "."
reportSLn "tc.decl.abstract" 25 $ show $ anyIsAbstract i
r <- checkMaybeAbstractly i m
reportSDoc "tc.decl" 5 $ ("Checked" <+> prettyTCM x) <> "."
return r
checkMaybeAbstractly :: forall m i a . ( MonadTCEnv m , AnyIsAbstract i )
=> i -> m a -> m a
checkMaybeAbstractly = localTC . set lensIsAbstract . anyIsAbstract
mutualChecks :: Info.MutualInfo -> A.Declaration -> [A.Declaration] -> MutualId -> Set QName -> TCM ()
mutualChecks mi d ds mid names = do
let nameList = Set.toList names
mapM_ instantiateDefinitionType nameList
modifyAllowedReductions (SmallSet.delete UnconfirmedReductions) $
checkPositivity_ mi names
localTC (\ e -> e { envMutualBlock = Just mid }) $
checkTermination_ d
revisitRecordPatternTranslation nameList
mapM_ checkIApplyConfluence_ nameList
checkInjectivity_ names
checkProjectionLikeness_ names
revisitRecordPatternTranslation :: [QName] -> TCM ()
revisitRecordPatternTranslation qs = do
(rs, qccs) <- partitionEithers . catMaybes <$> mapM classify qs
unless (null rs) $ forM_ qccs $ \(q,cc) -> do
(cc, recordExpressionBecameCopatternLHS) <- runChangeT $ translateCompiledClauses cc
modifySignature $ updateDefinition q
$ updateTheDef (updateCompiledClauses $ const $ Just cc)
. updateDefCopatternLHS (|| recordExpressionBecameCopatternLHS)
where
classify q = inConcreteOrAbstractMode q $ \ def -> do
case theDef def of
Record{ recEtaEquality' = Inferred YesEta } -> return $ Just $ Left q
Function
{ funProjection = Nothing
, funCompiled = Just cc
} -> return $ Just $ Right (q, cc)
_ -> return Nothing
type FinalChecks = Maybe (TCM ())
checkUnquoteDecl :: Info.MutualInfo -> [A.DefInfo] -> [QName] -> A.Expr -> TCM FinalChecks
checkUnquoteDecl mi is xs e = do
reportSDoc "tc.unquote.decl" 20 $ "Checking unquoteDecl" <+> sep (map prettyTCM xs)
Nothing <$ unquoteTop xs e
checkUnquoteDef :: [A.DefInfo] -> [QName] -> A.Expr -> TCM ()
checkUnquoteDef _ xs e = do
reportSDoc "tc.unquote.decl" 20 $ "Checking unquoteDef" <+> sep (map prettyTCM xs)
() <$ unquoteTop xs e
unquoteTop :: [QName] -> A.Expr -> TCM [QName]
unquoteTop xs e = do
tcm <- primAgdaTCM
unit <- primUnit
lzero <- primLevelZero
let vArg = defaultArg
hArg = setHiding Hidden . vArg
m <- checkExpr e $ El (mkType 0) $ apply tcm [hArg lzero, vArg unit]
res <- runUnquoteM $ tell xs >> evalTCM m
case res of
Left err -> typeError $ UnquoteFailed err
Right (_, xs) -> return xs
instantiateDefinitionType :: QName -> TCM ()
instantiateDefinitionType q = do
reportSLn "tc.decl.inst" 20 $ "instantiating type of " ++ prettyShow q
t <- defType . fromMaybe __IMPOSSIBLE__ . lookupDefinition q <$> getSignature
t' <- instantiateFull t
modifySignature $ updateDefinition q $ updateDefType $ const t'
reportSDoc "tc.decl.inst" 30 $ vcat
[ " t = " <+> prettyTCM t
, " t' = " <+> prettyTCM t'
]
data HighlightModuleContents = DontHightlightModuleContents | DoHighlightModuleContents
deriving (Eq)
highlight_ :: HighlightModuleContents -> A.Declaration -> TCM ()
highlight_ hlmod d = do
let highlight d = generateAndPrintSyntaxInfo d Full True
Bench.billTo [Bench.Highlighting] $ case d of
A.Axiom{} -> highlight d
A.Field{} -> __IMPOSSIBLE__
A.Primitive{} -> highlight d
A.Mutual i ds -> mapM_ (highlight_ DoHighlightModuleContents) $ deepUnscopeDecls ds
A.Apply{} -> highlight d
A.Import{} -> highlight d
A.Pragma{} -> highlight d
A.ScopedDecl{} -> return ()
A.FunDef{} -> highlight d
A.DataDef{} -> highlight d
A.DataSig{} -> highlight d
A.Open{} -> highlight d
A.PatternSynDef{} -> highlight d
A.Generalize{} -> highlight d
A.UnquoteDecl{} -> highlight d
A.UnquoteDef{} -> highlight d
A.Section i x tel ds -> do
highlight (A.Section i x tel [])
when (hlmod == DoHighlightModuleContents) $ mapM_ (highlight_ hlmod) (deepUnscopeDecls ds)
A.RecSig{} -> highlight d
A.RecDef i x uc ind eta c ps tel cs ->
highlight (A.RecDef i x uc ind eta c A.noDataDefParams dummy cs)
where
dummy = A.Lit $ LitString noRange $
"do not highlight construct(ed/or) type"
checkTermination_ :: A.Declaration -> TCM ()
checkTermination_ d = Bench.billTo [Bench.Termination] $ do
reportSLn "tc.decl" 20 $ "checkDecl: checking termination..."
unlessNullM (termDecl d) $ \ termErrs -> do
warning $ TerminationIssue termErrs
checkPositivity_ :: Info.MutualInfo -> Set QName -> TCM ()
checkPositivity_ mi names = Bench.billTo [Bench.Positivity] $ do
reportSLn "tc.decl" 20 $ "checkDecl: checking positivity..."
checkStrictlyPositive mi names
computePolarity $ Set.toList names
checkCoinductiveRecords :: [A.Declaration] -> TCM ()
checkCoinductiveRecords ds = forM_ ds $ \case
A.RecDef _ q _ (Just (Ranged r CoInductive)) _ _ _ _ _ -> setCurrentRange r $ do
unlessM (isRecursiveRecord q) $ typeError $ GenericError $
"Only recursive records can be coinductive"
_ -> return ()
checkInjectivity_ :: Set QName -> TCM ()
checkInjectivity_ names = Bench.billTo [Bench.Injectivity] $ do
reportSLn "tc.decl" 20 $ "checkDecl: checking injectivity..."
Fold.forM_ names $ \ q -> inConcreteOrAbstractMode q $ \ def -> do
case theDef def of
d@Function{ funClauses = cs, funTerminates = term, funProjection = mproj }
| term /= Just True -> do
reportSLn "tc.inj.check" 35 $
prettyShow q ++ " is not verified as terminating, thus, not considered for injectivity"
| isProperProjection d -> do
reportSLn "tc.inj.check" 40 $
prettyShow q ++ " is a projection, thus, not considered for injectivity"
| otherwise -> do
inv <- checkInjectivity q cs
modifySignature $ updateDefinition q $ updateTheDef $ const $
d { funInv = inv }
_ -> do
abstr <- asksTC envAbstractMode
reportSLn "tc.inj.check" 40 $
"we are in " ++ show abstr ++ " and " ++
prettyShow q ++ " is abstract or not a function, thus, not considered for injectivity"
checkProjectionLikeness_ :: Set QName -> TCM ()
checkProjectionLikeness_ names = Bench.billTo [Bench.ProjectionLikeness] $ do
let ds = Set.toList names
reportSLn "tc.proj.like" 20 $ "checkDecl: checking projection-likeness of " ++ prettyShow ds
case ds of
[d] -> do
def <- getConstInfo d
case theDef def of
Function{} -> makeProjection (defName def)
_ -> reportSLn "tc.proj.like" 25 $
prettyShow d ++ " is abstract or not a function, thus, not considered for projection-likeness"
_ -> reportSLn "tc.proj.like" 25 $
"mutual definitions are not considered for projection-likeness"
whenAbstractFreezeMetasAfter :: A.DefInfo -> TCM a -> TCM a
whenAbstractFreezeMetasAfter Info.DefInfo{ defAccess, defAbstract} m = do
let pubAbs = defAccess == PublicAccess && defAbstract == AbstractDef
if not pubAbs then m else do
(a, ms) <- metasCreatedBy m
reportSLn "tc.decl" 20 $ "Attempting to solve constraints before freezing."
wakeupConstraints_
xs <- freezeMetas' $ (`IntSet.member` ms) . metaId
reportSDoc "tc.decl.ax" 20 $ vcat
[ "Abstract type signature produced new metas: " <+> sep (map prettyTCM $ IntSet.toList ms)
, "We froze the following ones of these: " <+> sep (map prettyTCM xs)
]
return a
checkGeneralize :: Set QName -> A.DefInfo -> ArgInfo -> QName -> A.Expr -> TCM ()
checkGeneralize s i info x e = do
reportSDoc "tc.decl.gen" 20 $ sep
[ "checking type signature of generalizable variable" <+> prettyTCM x <+> ":"
, nest 2 $ prettyTCM e
]
(telNames, tGen) <-
generalizeType s $ locallyTC eGeneralizeMetas (const YesGeneralize) $
workOnTypes $ isType_ e
let n = length telNames
reportSDoc "tc.decl.gen" 10 $ sep
[ "checked type signature of generalizable variable" <+> prettyTCM x <+> ":"
, nest 2 $ prettyTCM tGen
]
addConstant x $ (defaultDefn info x tGen GeneralizableVar)
{ defArgGeneralizable = SomeGeneralizableArgs n }
checkAxiom :: A.Axiom -> A.DefInfo -> ArgInfo ->
Maybe [Occurrence] -> QName -> A.Expr -> TCM ()
checkAxiom = checkAxiom' Nothing
checkAxiom' :: Maybe A.GeneralizeTelescope -> A.Axiom -> A.DefInfo -> ArgInfo ->
Maybe [Occurrence] -> QName -> A.Expr -> TCM ()
checkAxiom' gentel funSig i info0 mp x e = whenAbstractFreezeMetasAfter i $ defaultOpenLevelsToZero $ do
rel <- max (getRelevance info0) <$> asksTC getRelevance
q <- asksTC getQuantity <&> \case
q@Quantity0{} -> q
_ -> getQuantity info0
let c = getCohesion info0
let mod = Modality rel q c
let info = setModality mod info0
applyCohesionToContext c $ do
reportSDoc "tc.decl.ax" 20 $ sep
[ text $ "checking type signature"
, nest 2 $ (prettyTCM mod <> prettyTCM x) <+> ":" <+> prettyTCM e
, nest 2 $ caseMaybe gentel "(no gentel)" $ \ _ -> "(has gentel)"
]
(genParams, npars, t) <- workOnTypes $ case gentel of
Nothing -> ([], 0,) <$> isType_ e
Just gentel ->
checkGeneralizeTelescope gentel $ \ genParams ptel -> do
t <- workOnTypes $ isType_ e
return (genParams, size ptel, abstract ptel t)
reportSDoc "tc.decl.ax" 10 $ sep
[ text $ "checked type signature"
, nest 2 $ (prettyTCM mod <> prettyTCM x) <+> ":" <+> prettyTCM t
, nest 2 $ "of sort " <+> prettyTCM (getSort t)
]
when (not $ null genParams) $
reportSLn "tc.decl.ax" 40 $ " generalized params: " ++ show genParams
when (funSig == A.NoFunSig) $ do
whenM ((== SizeUniv) <$> do reduce $ getSort t) $ do
whenM ((> 0) <$> getContextSize) $ do
typeError $ GenericError $ "We don't like postulated sizes in parametrized modules."
(occs, pols) <- case mp of
Nothing -> return ([], [])
Just occs -> do
TelV tel _ <- telView t
let n = length (telToList tel)
when (n < length occs) $
typeError $ TooManyPolarities x n
let pols = map polFromOcc occs
reportSLn "tc.polarity.pragma" 10 $
"Setting occurrences and polarity for " ++ prettyShow x ++ ":\n " ++
prettyShow occs ++ "\n " ++ prettyShow pols
return (occs, pols)
let blk = case funSig of
A.FunSig{} -> NotBlocked MissingClauses ()
A.NoFunSig{} -> NotBlocked ReallyNotBlocked ()
addConstant x =<< do
useTerPragma $
(defaultDefn info x t $
case funSig of
A.FunSig -> set funMacro (Info.defMacro i == MacroDef) emptyFunction
A.NoFunSig | isJust gentel -> DataOrRecSig npars
A.NoFunSig -> Axiom)
{ defArgOccurrences = occs
, defPolarity = pols
, defGeneralizedParams = genParams
, defBlocked = blk
}
case Info.defInstance i of
InstanceDef _r -> setCurrentRange x $ addTypedInstance x t
NotInstanceDef -> pure ()
traceCall (IsType_ e) $ do
checkingWhere <- asksTC envCheckingWhere
solveSizeConstraints $ if checkingWhere then DontDefaultToInfty else DefaultToInfty
checkPrimitive :: A.DefInfo -> QName -> A.Expr -> TCM ()
checkPrimitive i x e =
traceCall (CheckPrimitive (getRange i) x e) $ do
(name, PrimImpl t' pf) <- lookupPrimitiveFunctionQ x
let builtinPrimitives =
[ "primNatPlus"
, "primNatMinus"
, "primNatTimes"
, "primNatDivSucAux"
, "primNatModSucAux"
, "primNatEquality"
, "primNatLess"
, "primLevelZero"
, "primLevelSuc"
, "primLevelMax"
, "primSetOmega"
]
when (name `elem` builtinPrimitives) $ typeError $ NoSuchPrimitiveFunction name
t <- isType_ e
noConstraints $ equalType t t'
let s = prettyShow $ qnameName x
bindPrimitive s pf
addConstant x $
defaultDefn defaultArgInfo x t $
Primitive { primAbstr = Info.defAbstract i
, primName = s
, primClauses = []
, primInv = NotInjective
, primCompiled = Nothing }
checkPragma :: Range -> A.Pragma -> TCM ()
checkPragma r p =
traceCall (CheckPragma r p) $ case p of
A.BuiltinPragma x e -> bindBuiltin (rangedThing x) e
A.BuiltinNoDefPragma b x -> bindBuiltinNoDef (rangedThing b) x
A.RewritePragma _ qs -> addRewriteRules qs
A.CompilePragma b x s -> do
x' <- defName <$> getConstInfo x
unlessM ((x' `isInModule`) <$> currentModule) $
typeError $ GenericError $
"COMPILE pragmas must appear in the same module as their corresponding definitions,"
addPragma (rangedThing b) x s
A.StaticPragma x -> do
def <- getConstInfo x
case theDef def of
Function{} -> markStatic x
_ -> typeError $ GenericError "STATIC directive only works on functions"
A.InjectivePragma x -> markInjective x
A.InlinePragma b x -> do
def <- getConstInfo x
case theDef def of
Function{} -> markInline b x
_ -> typeError $ GenericError $ sINLINE ++ " directive only works on functions"
where sINLINE = if b then "INLINE" else "NOINLINE"
A.OptionsPragma{} -> typeError $ GenericError $ "OPTIONS pragma only allowed at beginning of file, before top module declaration"
A.DisplayPragma f ps e -> checkDisplayPragma f ps e
A.EtaPragma r -> do
let noRecord = typeError $ GenericError $
"ETA pragma is only applicable to coinductive records"
caseMaybeM (isRecord r) noRecord $ \case
Record{ recInduction = ind, recEtaEquality' = eta } -> do
unless (ind == Just CoInductive) $ noRecord
when (eta == Specified NoEta) $ typeError $ GenericError $
"ETA pragma conflicts with no-eta-equality declaration"
_ -> __IMPOSSIBLE__
modifySignature $ updateDefinition r $ updateTheDef $ \case
def@Record{} -> def { recEtaEquality' = Specified YesEta }
_ -> __IMPOSSIBLE__
checkMutual :: Info.MutualInfo -> [A.Declaration] -> TCM (MutualId, Set QName)
checkMutual i ds = inMutualBlock $ \ blockId -> defaultOpenLevelsToZero $ do
reportSDoc "tc.decl.mutual" 20 $ vcat $
(("Checking mutual block" <+> text (show blockId)) <> ":") :
map (nest 2 . prettyA) ds
insertMutualBlockInfo blockId i
localTC ( set eTerminationCheck (() <$ Info.mutualTerminationCheck i)
. set eCoverageCheck (Info.mutualCoverageCheck i)) $
mapM_ checkDecl ds
(blockId, ) . mutualNames <$> lookupMutualBlock blockId
checkTypeSignature :: A.TypeSignature -> TCM ()
checkTypeSignature = checkTypeSignature' Nothing
checkTypeSignature' :: Maybe A.GeneralizeTelescope -> A.TypeSignature -> TCM ()
checkTypeSignature' gtel (A.ScopedDecl scope ds) = do
setScope scope
mapM_ (checkTypeSignature' gtel) ds
checkTypeSignature' gtel (A.Axiom funSig i info mp x e) =
Bench.billTo [Bench.Definition x] $
Bench.billTo [Bench.Typing, Bench.TypeSig] $
let abstr = case Info.defAccess i of
PrivateAccess{}
| Info.defAbstract i == AbstractDef -> inAbstractMode
| otherwise -> inConcreteMode
PublicAccess -> inConcreteMode
in abstr $ checkAxiom' gtel funSig i info mp x e
checkTypeSignature' _ _ =
__IMPOSSIBLE__
checkSection :: Info.ModuleInfo -> ModuleName -> A.GeneralizeTelescope -> [A.Declaration] -> TCM ()
checkSection _ x tel ds = newSection x tel $ mapM_ checkDeclCached ds
checkModuleArity
:: ModuleName
-> Telescope
-> [NamedArg A.Expr]
-> TCM Telescope
checkModuleArity m tel args = check tel args
where
bad = typeError $ ModuleArityMismatch m tel args
check :: Telescope -> [NamedArg A.Expr] -> TCM Telescope
check tel [] = return tel
check EmptyTel (_:_) = bad
check (ExtendTel dom@Dom{domInfo = info} btel) args0@(Arg info' arg : args) =
let name = bareNameOf arg
my = bareNameOf dom
tel = absBody btel in
case (argInfoHiding info, argInfoHiding info', name) of
(Instance{}, NotHidden, _) -> check tel args0
(Instance{}, Hidden, _) -> check tel args0
(Instance{}, Instance{}, Nothing) -> check tel args
(Instance{}, Instance{}, Just x)
| Just x == my -> check tel args
| otherwise -> check tel args0
(Hidden, NotHidden, _) -> check tel args0
(Hidden, Instance{}, _) -> check tel args0
(Hidden, Hidden, Nothing) -> check tel args
(Hidden, Hidden, Just x)
| Just x == my -> check tel args
| otherwise -> check tel args0
(NotHidden, NotHidden, _) -> check tel args
(NotHidden, Hidden, _) -> bad
(NotHidden, Instance{}, _) -> bad
checkSectionApplication
:: Info.ModuleInfo
-> ModuleName
-> A.ModuleApplication
-> A.ScopeCopyInfo
-> TCM ()
checkSectionApplication i m1 modapp copyInfo =
traceCall (CheckSectionApplication (getRange i) m1 modapp) $
checkSectionApplication' i m1 modapp copyInfo
checkSectionApplication'
:: Info.ModuleInfo
-> ModuleName
-> A.ModuleApplication
-> A.ScopeCopyInfo
-> TCM ()
checkSectionApplication' i m1 (A.SectionApp ptel m2 args) copyInfo = do
extraParams <- do
mfv <- getCurrentModuleFreeVars
fv <- getContextSize
return (fv - mfv)
when (extraParams > 0) $ reportSLn "tc.mod.apply" 30 $ "Extra parameters to " ++ prettyShow m1 ++ ": " ++ show extraParams
checkTelescope ptel $ \ ptel -> do
tel <- lookupSection m2
vs <- moduleParamsToApply m2
let tel' = apply tel vs
etaTel <- checkModuleArity m2 tel' args
let tel'' = telFromList $ take (size tel' - size etaTel) $ telToList tel'
reportSDoc "tc.mod.apply" 15 $ vcat
[ "applying section" <+> prettyTCM m2
, nest 2 $ "args =" <+> sep (map prettyA args)
, nest 2 $ "ptel =" <+> escapeContext __IMPOSSIBLE__ (size ptel) (prettyTCM ptel)
, nest 2 $ "tel =" <+> prettyTCM tel
, nest 2 $ "tel' =" <+> prettyTCM tel'
, nest 2 $ "tel''=" <+> prettyTCM tel''
, nest 2 $ "eta =" <+> escapeContext __IMPOSSIBLE__ (size ptel) (addContext tel'' $ prettyTCM etaTel)
]
ts <- (noConstraints $ checkArguments_ DontExpandLast (getRange i) args tel') >>= \case
(ts', etaTel') | (size etaTel == size etaTel')
, Just ts <- allApplyElims ts' -> return ts
_ -> __IMPOSSIBLE__
let aTel = tel' `apply` ts
reportSDoc "tc.mod.apply" 15 $ vcat
[ nest 2 $ "aTel =" <+> prettyTCM aTel
]
addContext (KeepNames aTel) $ do
reportSDoc "tc.mod.apply" 80 $
"addSection" <+> prettyTCM m1 <+> (getContextTelescope >>= \ tel -> inTopContext (prettyTCM tel))
addSection m1
reportSDoc "tc.mod.apply" 20 $ vcat
[ sep [ "applySection", prettyTCM m1, "=", prettyTCM m2, fsep $ map prettyTCM (vs ++ ts) ]
, nest 2 $ pretty copyInfo
]
args <- instantiateFull $ vs ++ ts
let n = size aTel
etaArgs <- inTopContext $ addContext aTel getContextArgs
addContext (KeepNames aTel) $
applySection m1 (ptel `abstract` aTel) m2 (raise n args ++ etaArgs) copyInfo
checkSectionApplication' i m1 (A.RecordModuleInstance x) copyInfo = do
let name = mnameToQName x
tel' <- lookupSection x
vs <- moduleParamsToApply x
let tel = tel' `apply` vs
args = teleArgs tel
telInst :: Telescope
telInst = instFinal tel
instFinal :: Telescope -> Telescope
instFinal (ExtendTel _ NoAbs{}) = __IMPOSSIBLE__
instFinal (ExtendTel dom (Abs n EmptyTel)) =
ExtendTel do' (Abs n EmptyTel)
where do' = makeInstance dom { domName = Just $ WithOrigin Inserted $ unranged "r" }
instFinal (ExtendTel arg (Abs n tel)) =
ExtendTel arg (Abs n (instFinal tel))
instFinal EmptyTel = __IMPOSSIBLE__
reportSDoc "tc.mod.apply" 20 $ vcat
[ sep [ "applySection", prettyTCM name, "{{...}}" ]
, nest 2 $ "x =" <+> prettyTCM x
, nest 2 $ "name =" <+> prettyTCM name
, nest 2 $ "tel =" <+> prettyTCM tel
, nest 2 $ "telInst =" <+> prettyTCM telInst
, nest 2 $ "vs =" <+> sep (map prettyTCM vs)
]
reportSDoc "tc.mod.apply" 60 $ vcat
[ nest 2 $ "vs =" <+> text (show vs)
]
when (tel == EmptyTel) $
typeError $ GenericError $ prettyShow (qnameToConcrete name) ++ " is not a parameterised section"
addContext telInst $ do
vs <- moduleParamsToApply x
reportSDoc "tc.mod.apply" 20 $ vcat
[ nest 2 $ "vs =" <+> sep (map prettyTCM vs)
, nest 2 $ "args =" <+> sep (map (parens . prettyTCM) args)
]
reportSDoc "tc.mod.apply" 60 $ vcat
[ nest 2 $ "vs =" <+> text (show vs)
, nest 2 $ "args =" <+> text (show args)
]
addSection m1
applySection m1 telInst x (vs ++ args) copyInfo
checkImport :: Info.ModuleInfo -> ModuleName -> TCM ()
checkImport i x = return ()
class ShowHead a where
showHead :: a -> String
instance ShowHead A.Declaration where
showHead d =
case d of
A.Axiom {} -> "Axiom"
A.Field {} -> "Field"
A.Primitive {} -> "Primitive"
A.Mutual {} -> "Mutual"
A.Section {} -> "Section"
A.Apply {} -> "Apply"
A.Import {} -> "Import"
A.Pragma {} -> "Pragma"
A.Open {} -> "Open"
A.FunDef {} -> "FunDef"
A.DataSig {} -> "DataSig"
A.DataDef {} -> "DataDef"
A.RecSig {} -> "RecSig"
A.RecDef {} -> "RecDef"
A.PatternSynDef{} -> "PatternSynDef"
A.Generalize {} -> "Generalize"
A.UnquoteDecl {} -> "UnquoteDecl"
A.ScopedDecl {} -> "ScopedDecl"
A.UnquoteDef {} -> "UnquoteDef"
debugPrintDecl :: A.Declaration -> TCM ()
debugPrintDecl d = do
verboseS "tc.decl" 45 $ do
reportSLn "tc.decl" 45 $ "checking a " ++ showHead d
case d of
A.Section info mname tel ds -> do
reportSLn "tc.decl" 45 $
"section " ++ prettyShow mname ++ " has "
++ show (length $ A.generalizeTel tel) ++ " parameters and "
++ show (length ds) ++ " declarations"
reportSDoc "tc.decl" 45 $ prettyA $ A.Section info mname tel []
forM_ ds $ \ d -> do
reportSDoc "tc.decl" 45 $ prettyA d
_ -> return ()