{-# 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 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 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.Constraints
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Errors
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 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 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 <- gets $ 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 $ text "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 <- case d of
A.Axiom{} -> meta $ checkTypeSignature d
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 ps cs -> impossible $ check x i $ checkDataDef i x ps cs
A.RecDef i x ind eta c ps tel cs -> mutual empty [d] $ check x i $ do
checkRecDef i x ind eta c ps tel cs
blockId <- mutualBlockOf x
verboseS "tc.decl.mutual" 70 $ do
current <- asks 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 (asks envMutualBlock) $ do
highlight_ d
whenJust finalChecks $ \ theMutualChecks -> do
reportSLn "tc.decl" 20 $ "Attempting to solve constraints before freezing."
wakeupConstraints_
checkingWhere <- asks envCheckingWhere
solveSizeConstraints $ if checkingWhere then DontDefaultToInfty else DefaultToInfty
wakeupConstraints_
reportSLn "tc.decl" 20 $ "Freezing all metas."
_ <- freezeMetas
theMutualChecks
where
checkSig i x ps t = checkTypeSignature $
A.Axiom A.NoFunSig i defaultArgInfo Nothing x
(A.Pi (Info.ExprRange (fuseRange ps t)) ps t)
check x i m = Bench.billTo [Bench.Definition x] $ do
reportSDoc "tc.decl" 5 $ text "Checking" <+> prettyTCM x <> text "."
reportSLn "tc.decl.abstract" 25 $ show (Info.defAbstract i)
r <- abstract (Info.defAbstract i) m
reportSDoc "tc.decl" 5 $ text "Checked" <+> prettyTCM x <> text "."
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
local (\ e -> e { envMutualBlock = Just mid }) $ checkTermination_ d
revisitRecordPatternTranslation 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 $ text "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 $ text "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
[ text " t = " <+> prettyTCM t
, text " t' = " <+> prettyTCM t'
]
highlight_ :: A.Declaration -> TCM ()
highlight_ 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_ $ 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.UnquoteDecl{} -> highlight d
A.UnquoteDef{} -> highlight d
A.Section i x tel _ -> highlight (A.Section i x tel [])
A.RecSig{} -> highlight d
A.RecDef i x ind eta c ps tel cs ->
highlight (A.RecDef i x ind eta c [] 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..."
case d of
A.RecDef {} -> return ()
_ -> disableDestructiveUpdate $ do
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 <- asks 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' $ (`Set.member` ms)
reportSDoc "tc.decl.ax" 20 $ vcat
[ text "Abstract type signature produced new metas: " <+> sep (map prettyTCM $ Set.toList ms)
, text "We froze the following ones of these: " <+> sep (map prettyTCM xs)
]
return a
checkAxiom :: A.Axiom -> Info.DefInfo -> ArgInfo ->
Maybe [Occurrence] -> QName -> A.Expr -> TCM ()
checkAxiom funSig i info0 mp x e = whenAbstractFreezeMetasAfter i $ do
rel <- max (getRelevance info0) <$> asks envRelevance
let info = setRelevance rel info0
t <- workOnTypes $ isType_ e
reportSDoc "tc.decl.ax" 10 $ sep
[ text $ "checked type signature"
, nest 2 $ prettyTCM rel <> prettyTCM x <+> text ":" <+> prettyTCM t
, nest 2 $ text "of sort " <+> prettyTCM (getSort t)
]
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 -> Axiom)
{ defArgOccurrences = occs
, defPolarity = pols
}
when (Info.defInstance i == InstanceDef) $ do
addTypedInstance x t
traceCall (IsType_ e) $ do
checkingWhere <- asks envCheckingWhere
solveSizeConstraints $ if checkingWhere then DontDefaultToInfty else DefaultToInfty
checkPrimitive :: Info.DefInfo -> QName -> A.Expr -> TCM ()
checkPrimitive i x e =
traceCall (CheckPrimitive (getRange i) (qnameName x) e) $ do
(name, PrimImpl t' pf) <- lookupPrimitiveFunctionQ x
let builtinPrimitives =
[ "primNatPlus", "primNatMinus" , "primNatTimes"
, "primNatDivSucAux", "primNatModSucAux"
, "primNatEquality", "primNatLess" ]
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.CompiledTypePragma x hs -> do
def <- getConstInfo x
case theDef def of
Axiom{} -> addHaskellType x hs
_ -> typeError $ GenericError
"COMPILED_TYPE directive only works on postulates"
A.CompiledDataPragma x hs hcs -> do
def <- getConstInfo x
assertCurrentModule x $
"COMPILED_DATA directives must appear in the same module " ++
"as their corresponding datatype definition,"
case theDef def of
Datatype{dataCons = cs} -> addHaskellData x hs hcs
Record{recConHead = ch} -> addHaskellData x hs hcs
_ -> typeError $ GenericError "COMPILED_DATA on non datatype"
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.CompiledPragma x hs -> do
def <- getConstInfo x
let addCompiled = addHaskellCode x hs
case theDef def of
Axiom{} -> addCompiled
Function{} -> addCompiled
_ -> typeError $ GenericError "COMPILED directive only works on postulates and functions"
A.CompiledExportPragma x hs -> do
def <- getConstInfo x
let correct = case theDef def of
Function{} -> True
Constructor{} -> False
_ -> False
if not correct
then typeError $ GenericError "COMPILED_EXPORT directive only works on functions"
else addHaskellExport x hs
A.CompiledJSPragma x ep ->
addJSCode x ep
A.CompiledUHCPragma x cr -> do
def <- getConstInfo x
case theDef def of
Axiom{} -> addCoreCode x cr
_ -> typeError $ GenericError "COMPILED_UHC directive only works on postulates"
A.CompiledDataUHCPragma x crd crcs -> do
def <- getConstInfo x
m <- currentModule
let m' = qnameModule $ defName def
unless (m == m') $ typeError $ GenericError $
"COMPILED_DATA_UHC directives must appear in the same module " ++
"as their corresponding datatype definition,"
case theDef def of
Datatype{dataCons = cs} -> addCoreType x crd crcs
_ -> typeError $ GenericError "COMPILED_DATA_UHC on non datatype"
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 $
(text "Checking mutual block" <+> text (show blockId) <> text ":") :
map (nest 2 . prettyA) ds
insertMutualBlockInfo blockId i
local (\e -> e { envTerminationCheck = () <$ Info.mutualTermCheck i }) $
mapM_ checkDecl ds
(blockId, ) . mutualNames <$> lookupMutualBlock blockId
checkTypeSignature :: A.TypeSignature -> TCM ()
checkTypeSignature (A.ScopedDecl scope ds) = do
setScope scope
mapM_ checkTypeSignature ds
checkTypeSignature (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 funSig i info mp x e
checkTypeSignature _ = __IMPOSSIBLE__
checkSection :: Info.ModuleInfo -> ModuleName -> A.Telescope -> [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 info _) btel) args0@(Arg info' (Named rname _) : args) =
let name = fmap rangedThing rname
y = absName btel
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)
| x == y -> 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)
| x == y -> 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
[ text "applying section" <+> prettyTCM m2
, nest 2 $ text "args =" <+> sep (map prettyA args)
, nest 2 $ text "ptel =" <+> escapeContext (size ptel) (prettyTCM ptel)
, nest 2 $ text "tel =" <+> prettyTCM tel
, nest 2 $ text "tel' =" <+> prettyTCM tel'
, nest 2 $ text "tel''=" <+> prettyTCM tel''
, nest 2 $ text "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 $ text "aTel =" <+> prettyTCM aTel
]
addContext (KeepNames aTel) $ do
reportSDoc "tc.mod.apply" 80 $
text "addSection" <+> prettyTCM m1 <+> (getContextTelescope >>= \ tel -> inTopContext (prettyTCM tel))
addSection m1
reportSDoc "tc.mod.apply" 20 $ vcat
[ sep [ text "applySection", prettyTCM m1, text "=", 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.RecordModuleIFS 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 info t) (Abs n EmptyTel)) =
ExtendTel (Dom ifo' t) (Abs n EmptyTel)
where ifo' = makeInstance info
instFinal (ExtendTel arg (Abs n tel)) =
ExtendTel arg (Abs n (instFinal tel))
instFinal EmptyTel = __IMPOSSIBLE__
reportSDoc "tc.mod.apply" 20 $ vcat
[ sep [ text "applySection", prettyTCM name, text "{{...}}" ]
, nest 2 $ text "x =" <+> prettyTCM x
, nest 2 $ text "name =" <+> prettyTCM name
, nest 2 $ text "tel =" <+> prettyTCM tel
, nest 2 $ text "telInst =" <+> prettyTCM telInst
, nest 2 $ text "vs =" <+> sep (map prettyTCM vs)
]
reportSDoc "tc.mod.apply" 60 $ vcat
[ nest 2 $ text "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 $ text "vs =" <+> sep (map prettyTCM vs)
, nest 2 $ text "args =" <+> sep (map (parens . prettyTCM) args)
]
reportSDoc "tc.mod.apply" 60 $ vcat
[ nest 2 $ text "vs =" <+> text (show vs)
, nest 2 $ text "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.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 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 ()