{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Decl where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), null )
#else
import Prelude hiding ( null )
#endif
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State (modify, gets, get)
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 Data.Map (Map)
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import qualified Data.IntSet as IntSet
import qualified Data.Map as Map
import Data.Set (Set)
import Agda.Interaction.Options
import Agda.Interaction.Highlighting.Generate
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (deepUnscopeDecl, deepUnscopeDecls)
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Internal
import qualified Agda.Syntax.Reflected as R
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Translation.ReflectedToAbstract
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.CheckInternal
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.IApplyConfluence
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Generalize
import Agda.TypeChecking.Injectivity
import Agda.TypeChecking.Irrelevance
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.Quote
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.Unquote
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.Except
import Agda.Utils.Functor
import Agda.Utils.Function
import qualified Agda.Utils.HashMap as HMap
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
#include "undefined.h"
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 = do
cs <- getsTC $ stLoadedFileCache . stPersistentState
cleanCachedLog
_ <- m
modifyPersistentState $ \st -> st{stLoadedFileCache = cs}
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
reportSLn "" 0 $ unlines
[ "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 i x e -> checkUnquoteDecl mi i x e
A.UnquoteDef i x e -> impossible $ checkUnquoteDef i x e
whenNothingM (asksTC envMutualBlock) $ do
highlight_ DontHightlightModuleContents d
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 x i m = Bench.billTo [Bench.Definition x] $ do
reportSDoc "tc.decl" 5 $ "Checking" <+> prettyTCM x <> "."
reportSLn "tc.decl.abstract" 25 $ show (Info.defAbstract i)
r <- abstract (Info.defAbstract i) m
reportSDoc "tc.decl" 5 $ "Checked" <+> prettyTCM x <> "."
return r
isAbstract = fmap Info.defAbstract (A.getDefInfo d) == Just AbstractDef
abstract ConcreteDef = inConcreteMode
abstract AbstractDef = inAbstractMode
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 (List.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 <- translateCompiledClauses cc
modifySignature $ updateDefinition q $ updateTheDef $
updateCompiledClauses $ const $ Just cc
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 -> [Info.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 :: [Info.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..."
termErrs <- termDecl d
unless (null 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 } -> do
case term of
Just True -> do
inv <- checkInjectivity q cs
modifySignature $ updateDefinition q $ updateTheDef $ const $
d { funInv = inv }
_ -> reportSLn "tc.inj.check" 20 $
prettyShow q ++ " is not verified as terminating, thus, not considered for injectivity"
_ -> do
abstr <- asksTC envAbstractMode
reportSLn "tc.inj.check" 20 $
"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 :: Info.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
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 -> Info.DefInfo -> ArgInfo -> QName -> A.Expr -> TCM ()
checkGeneralize s i info x e = do
(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 -> Info.DefInfo -> ArgInfo ->
Maybe [Occurrence] -> QName -> A.Expr -> TCM ()
checkAxiom = checkAxiom' Nothing
checkAxiom' :: Maybe A.GeneralizeTelescope -> A.Axiom -> Info.DefInfo -> ArgInfo ->
Maybe [Occurrence] -> QName -> A.Expr -> TCM ()
checkAxiom' gentel funSig i info0 mp x e = whenAbstractFreezeMetasAfter i $ do
rel <- max (getRelevance info0) <$> asksTC envRelevance
let info = setRelevance rel info0
(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 rel <> 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)
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
}
when (Info.defInstance i == InstanceDef) $ do
addTypedInstance x t
traceCall (IsType_ e) $ do
checkingWhere <- asksTC envCheckingWhere
solveSizeConstraints $ if checkingWhere then DontDefaultToInfty else DefaultToInfty
checkPrimitive :: Info.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 (elem name 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 }
assertCurrentModule :: QName -> String -> TCM ()
assertCurrentModule x err =
do def <- getConstInfo x
m <- currentModule
let m' = qnameModule $ defName def
unless (m == m' || isSubModuleOf m' m) $ typeError $ GenericError err
checkPragma :: Range -> A.Pragma -> TCM ()
checkPragma r p =
traceCall (CheckPragma r p) $ case p of
A.BuiltinPragma x e -> bindBuiltin x e
A.BuiltinNoDefPragma b x -> bindBuiltinNoDef b x
A.RewritePragma q -> addRewriteRule q
A.CompilePragma b x s -> do
assertCurrentModule x $
"COMPILE pragmas must appear in the same module " ++
"as their corresponding definitions,"
addPragma 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 -> do
verboseS "tc.decl.mutual" 20 $ do
reportSDoc "tc.decl.mutual" 20 $ vcat $
("Checking mutual block" <+> text (show blockId) <> ":") :
map (nest 2 . prettyA) ds
insertMutualBlockInfo blockId i
localTC (\e -> e { envTerminationCheck = () <$ Info.mutualTermCheck 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
OnlyQualified -> __IMPOSSIBLE__
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 tel [] = return tel
check EmptyTel (_:_) = bad
check (ExtendTel dom@Dom{domInfo = info} btel) args0@(Arg info' (Named rname _) : args) =
let name = fmap rangedThing rname
my = fmap rangedThing $ domName 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 (size ptel) (prettyTCM ptel)
, nest 2 $ "tel =" <+> prettyTCM tel
, nest 2 $ "tel' =" <+> prettyTCM tel'
, nest 2 $ "tel''=" <+> prettyTCM tel''
, nest 2 $ "eta =" <+> escapeContext (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 $ 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 ()