#if __GLASGOW_HASKELL__ >= 710
#endif
module Agda.TypeChecking.Rules.Decl where
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State (modify)
import qualified Data.Foldable as Fold
import Data.Maybe
import Data.Map (Map)
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Sequence ((|>))
import Agda.Compiler.HaskellTypes
import Agda.Interaction.Options
import Agda.Interaction.Highlighting.Generate
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal as I
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Translation.InternalToAbstract
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.Polarity
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.ProjectionLike
import Agda.TypeChecking.Quote
import Agda.TypeChecking.Records
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.Rules.Term
import Agda.TypeChecking.Rules.Data ( checkDataDef )
import Agda.TypeChecking.Rules.Record ( checkRecDef )
import Agda.TypeChecking.Rules.Def ( checkFunDef, useTerPragma )
import Agda.TypeChecking.Rules.Builtin
import Agda.Termination.TermCheck
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
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) d
reportSDoc "tc.decl" 10 $ prettyA d
when_ isAbstract freezeMetas
let
none m = m >> return Nothing
meta m = m >> return (Just (return ()))
mutual i ds m = m >>= return . Just . mutualChecks i d ds
impossible m = m >> return __IMPOSSIBLE__
let mi = Info.MutualInfo TerminationCheck noRange
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 rd rm -> meta $ checkSectionApplication i x modapp rd rm
A.Import i x -> none $ checkImport i x
A.Pragma i p -> none $ checkPragma i p
A.ScopedDecl scope ds -> none $ setScope scope >> checkDecls 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 c ps tel cs -> mutual mi [d] $ check x i $ do
checkRecDef i x ind c ps tel cs
return (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
whenNothingM (asks envMutualBlock) $ do
highlight_ d
whenJust finalChecks $ \ theMutualChecks -> do
solveSizeConstraints
wakeupConstraints_
_ <- freezeMetas
theMutualChecks
where
unScope (A.ScopedDecl scope ds) = setScope scope >> unScope d
unScope d = return d
checkSig i x ps t = checkTypeSignature $
A.Axiom A.NoFunSig i defaultArgInfo x (A.Pi (Info.ExprRange (fuseRange ps t)) ps t)
check x i m = 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] -> Set QName -> TCM ()
mutualChecks i d ds names = do
mapM_ instantiateDefinitionType $ Set.toList names
checkTermination_ d
checkPositivity_ names
checkInjectivity_ names
checkProjectionLikeness_ names
type FinalChecks = Maybe (TCM ())
checkUnquoteDecl :: Info.MutualInfo -> Info.DefInfo -> QName -> A.Expr -> TCM FinalChecks
checkUnquoteDecl mi i x e = do
reportSDoc "tc.unquote.decl" 20 $ text "Checking unquoteDecl" <+> prettyTCM x
fundef <- primAgdaFunDef
v <- checkExpr e $ El (mkType 0) fundef
reportSDoc "tc.unquote.decl" 20 $ text "unquoteDecl: Checked term"
uv <- runUnquoteM $ unquote v
case uv of
Left err -> typeError $ UnquoteFailed err
Right (UnQFun a cs) -> do
reportSDoc "tc.unquote.decl" 20 $
vcat $ text "unquoteDecl: Unquoted term"
: [ nest 2 $ text (show c) | c <- cs ]
addConstant x =<< do
useTerPragma $ defaultDefn defaultArgInfo x a emptyFunction
a <- reifyUnquoted $ killRange a
reportSDoc "tc.unquote.decl" 10 $
vcat [ text "unquoteDecl" <+> prettyTCM x <+> text "-->"
, prettyTCM x <+> text ":" <+> prettyA a ]
tel <- getContextTelescope
let tel' = replaceEmptyName "r" $ killRange tel
cs <- mapM (reifyUnquoted . QNamed x . killRange . abstract tel) cs
reportSDoc "tc.unquote.decl" 10 $ vcat $ map prettyA cs
let ds = [ A.Axiom A.FunSig i defaultArgInfo x a
, A.FunDef i x NotDelayed cs ]
xs <- checkMutual mi ds
return $ Just $ mutualChecks mi (A.Mutual mi ds) ds xs
instantiateDefinitionType :: QName -> TCM ()
instantiateDefinitionType q = do
reportSLn "tc.decl.inst" 20 $ "instantiating type of " ++ show q
sig <- getSignature
let t = defType $ fromMaybe __IMPOSSIBLE__ $ lookupDefinition q sig
t <- instantiateFull t
modifySignature $ updateDefinition q $ \ def -> def { defType = t }
highlight_ :: A.Declaration -> TCM ()
highlight_ d = do
let highlight d = generateAndPrintSyntaxInfo d Full
Bench.billTo [Bench.Highlighting] $ case d of
A.Axiom{} -> highlight d
A.Field{} -> __IMPOSSIBLE__
A.Primitive{} -> highlight d
A.Mutual{} -> highlight d
A.Apply{} -> highlight d
A.Import{} -> highlight d
A.Pragma{} -> highlight d
A.ScopedDecl{} -> return ()
A.FunDef{} -> __IMPOSSIBLE__
A.DataDef{} -> __IMPOSSIBLE__
A.DataSig{} -> __IMPOSSIBLE__
A.Open{} -> highlight d
A.PatternSynDef{} -> highlight d
A.UnquoteDecl{} -> highlight d
A.Section i x tel _ -> highlight (A.Section i x tel [])
A.RecSig{} -> highlight d
A.RecDef i x ind c ps tel cs ->
highlight (A.RecDef i x ind c [] tel (fields cs))
where
fields (A.ScopedDecl _ ds1 : ds2) = fields ds1 ++ fields ds2
fields (d@A.Field{} : ds) = d : fields ds
fields (_ : ds) = fields ds
fields [] = []
checkTermination_ :: A.Declaration -> TCM ()
checkTermination_ d = Bench.billTo [Bench.Termination] $ do
reportSLn "tc.decl" 20 $ "checkDecl: checking termination..."
whenM (optTerminationCheck <$> pragmaOptions) $ do
case d of
A.RecDef {} -> return ()
_ -> disableDestructiveUpdate $ do
termErrs <- termDecl d
unless (null termErrs) $
typeError $ TerminationCheckFailed termErrs
checkPositivity_ :: Set QName -> TCM ()
checkPositivity_ names = Bench.billTo [Bench.Positivity] $ do
reportSLn "tc.decl" 20 $ "checkDecl: checking positivity..."
checkStrictlyPositive names
mapM_ computePolarity $ Set.toList names
checkCoinductiveRecords :: [A.Declaration] -> TCM ()
checkCoinductiveRecords ds = forM_ ds $ \ d -> case d of
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 $ do
def <- getConstInfo q
case theDef def of
d@Function{ funClauses = cs, funTerminates = term } -> do
case term of
Just True -> do
inv <- checkInjectivity q cs
modifySignature $ updateDefinition q $ const $
def { theDef = d { funInv = inv }}
_ -> reportSLn "tc.inj.check" 20 $
show 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 " ++
show 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 " ++ show ds
case ds of
[d] -> do
def <- getConstInfo d
case theDef def of
Function{} -> makeProjection (defName def)
_ -> reportSLn "tc.proj.like" 25 $
show 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"
checkAxiom :: A.Axiom -> Info.DefInfo -> A.ArgInfo -> QName -> A.Expr -> TCM ()
checkAxiom funSig i info0 x e = do
rel <- max (getRelevance info0) <$> asks envRelevance
let info = setRelevance rel $ convColor 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."
addConstant x =<< do
useTerPragma $ defaultDefn info x t $
case funSig of
A.FunSig -> emptyFunction
A.NoFunSig -> Axiom
when (Info.defInstance i == InstanceDef) $ do
addTypedInstance x t
traceCall (IsType_ e) $ solveSizeConstraints
checkPrimitive :: Info.DefInfo -> QName -> A.Expr -> TCM ()
checkPrimitive i x e =
traceCall (CheckPrimitive (getRange i) (qnameName x) e) $ do
(_, PrimImpl t' pf) <- lookupPrimitiveFunctionQ x
t <- isType_ e
noConstraints $ equalType t t'
let s = prettyShow $ qnameName x
bindPrimitive s pf
addConstant x $
defaultDefn defaultArgInfo x t $
Primitive (Info.defAbstract i) s [] Nothing
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
do m <- currentModule
let m' = qnameModule $ defName def
unless (m == m') $ typeError $ GenericError $
"COMPILED_DATA directives must appear in the same module " ++
"as their corresponding datatype definition,"
let addCompiledData cs = do
addHaskellType x hs
let computeHaskellType c = do
def <- getConstInfo c
let Constructor{ conPars = np } = theDef def
underPars 0 a = haskellType a
underPars n a = do
a <- reduce a
case unEl a of
Pi a (NoAbs _ b) -> underPars (n 1) b
Pi a b -> underAbstraction a b $ \b -> hsForall <$> getHsVar 0 <*> underPars (n 1) b
_ -> __IMPOSSIBLE__
ty <- underPars np $ defType def
reportSLn "tc.pragma.compile" 10 $ "Haskell type for " ++ show c ++ ": " ++ ty
return ty
hts <- mapM computeHaskellType cs
sequence_ $ zipWith3 addHaskellCode cs hts hcs
case theDef def of
Datatype{dataCons = cs}
| length cs /= length hcs -> do
let n_forms_are = case length hcs of
1 -> "1 compiled form is"
n -> show n ++ " compiled forms are"
only | null hcs = ""
| length hcs < length cs = "only "
| otherwise = ""
err <- fsep $ [prettyTCM x] ++ pwords ("has " ++ show (length cs) ++
" constructors, but " ++ only ++ n_forms_are ++ " given [" ++ unwords hcs ++ "]")
typeError $ GenericError $ show err
| otherwise -> addCompiledData cs
Record{recConHead = ch}
| length hcs == 1 -> addCompiledData [conName ch]
| otherwise -> do
err <- fsep $ [prettyTCM x] ++ pwords ("has 1 constructor, but " ++
show (length hcs) ++ " Haskell constructors are given [" ++ unwords hcs ++ "]")
typeError $ GenericError $ show err
_ -> typeError $ GenericError "COMPILED_DATA on non datatype"
A.CompiledPragma x hs -> do
def <- getConstInfo x
case theDef def of
Axiom{} -> do
ty <- haskellType $ defType def
reportSLn "tc.pragma.compile" 10 $ "Haskell type for " ++ show x ++ ": " ++ ty
addHaskellCode x ty hs
_ -> typeError $ GenericError "COMPILED directive only works on postulates"
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 do
ty <- haskellType $ defType def
addHaskellExport x ty hs
A.CompiledEpicPragma x ep -> do
def <- getConstInfo x
case theDef def of
Axiom{} -> do
addEpicCode x ep
_ -> typeError $ GenericError "COMPILED_EPIC directive only works on postulates"
A.CompiledJSPragma x ep ->
addJSCode x ep
A.StaticPragma x -> do
def <- getConstInfo x
case theDef def of
Function{} -> markStatic x
_ -> typeError $ GenericError "STATIC directive only works on functions"
A.OptionsPragma{} -> typeError $ GenericError $ "OPTIONS pragma only allowed at beginning of file, before top module declaration"
A.EtaPragma r -> do
whenNothingM (isRecord r) $
typeError $ GenericError $ "ETA pragma is only applicable to records"
modifySignature $ updateDefinition r $ updateTheDef $ setEta
where
setEta d = case d of
Record{} -> d { recEtaEquality = True }
_ -> __IMPOSSIBLE__
checkMutual :: Info.MutualInfo -> [A.Declaration] -> TCM (Set QName)
checkMutual i ds = inMutualBlock $ do
verboseS "tc.decl.mutual" 20 $ do
blockId <- currentOrFreshMutualBlock
reportSDoc "tc.decl.mutual" 20 $ vcat $
(text "Checking mutual block" <+> text (show blockId) <> text ":") :
map (nest 2 . prettyA) ds
local (\e -> e { envTerminationCheck = () <$ Info.mutualTermCheck i }) $
mapM_ checkDecl ds
lookupMutualBlock =<< currentOrFreshMutualBlock
checkTypeSignature :: A.TypeSignature -> TCM ()
checkTypeSignature (A.ScopedDecl scope ds) = do
setScope scope
mapM_ checkTypeSignature ds
checkTypeSignature (A.Axiom funSig i info x e) =
case Info.defAccess i of
PublicAccess -> inConcreteMode $ checkAxiom funSig i info x e
PrivateAccess -> inAbstractMode $ checkAxiom funSig i info x e
OnlyQualified -> __IMPOSSIBLE__
checkTypeSignature _ = __IMPOSSIBLE__
checkSection :: Info.ModuleInfo -> ModuleName -> A.Telescope -> [A.Declaration] -> TCM ()
checkSection i x tel ds =
checkTelescope tel $ \ tel' -> do
addSection x (size tel')
verboseS "tc.mod.check" 10 $ do
dx <- prettyTCM x
dtel <- mapM prettyAs tel
dtel' <- prettyTCM =<< lookupSection x
reportSLn "tc.mod.check" 10 $ "checking section " ++ show dx ++ " " ++ show dtel
reportSLn "tc.mod.check" 10 $ " actual tele: " ++ show dtel'
withCurrentModule x $ checkDecls ds
checkModuleArity
:: ModuleName
-> Telescope
-> [I.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.Ren QName
-> A.Ren ModuleName
-> TCM ()
checkSectionApplication i m1 modapp rd rm =
traceCall (CheckSectionApplication (getRange i) m1 modapp) $
checkSectionApplication' i m1 modapp rd rm
checkSectionApplication'
:: Info.ModuleInfo
-> ModuleName
-> A.ModuleApplication
-> A.Ren QName
-> A.Ren ModuleName
-> TCM ()
checkSectionApplication' i m1 (A.SectionApp ptel m2 args) rd rm = do
extraParams <- do
mfv <- getModuleFreeVars =<< currentModule
fv <- size <$> getContextTelescope
return (fv mfv)
when (extraParams > 0) $ reportSLn "tc.mod.apply" 30 $ "Extra parameters to " ++ show m1 ++ ": " ++ show extraParams
checkTelescope ptel $ \ ptel -> do
tel <- lookupSection m2
vs <- freeVarsToApply $ mnameToQName m2
let tel' = apply tel vs
args' = convColor args
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''
let aTel = tel' `apply` ts
reportSDoc "tc.mod.apply" 15 $ vcat
[ nest 2 $ text "aTel =" <+> prettyTCM aTel
]
addCtxTel aTel $ addSection m1 (size ptel + size aTel + extraParams)
reportSDoc "tc.mod.apply" 20 $ vcat
[ sep [ text "applySection", prettyTCM m1, text "=", prettyTCM m2, fsep $ map prettyTCM (vs ++ ts) ]
, nest 2 $ text " defs:" <+> text (show rd)
, nest 2 $ text " mods:" <+> text (show rm)
]
args <- instantiateFull $ vs ++ ts
applySection m1 ptel m2 args rd rm
checkSectionApplication' i m1 (A.RecordModuleIFS x) rd rm = do
let name = mnameToQName x
tel' <- lookupSection x
vs <- freeVarsToApply name
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' = setHiding Instance 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 $ show (qnameToConcrete name) ++ " is not a parameterised section"
addCtxTel telInst $ do
vs <- freeVarsToApply name
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)
]
applySection m1 telInst x (vs ++ args) rd rm
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"
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 " ++ show 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 ()