Update a few debug levels

Author: jespercockx

src/Agda2Hs/Compile/Function.hs

@@ -140,7 +140,7 @@ compileFun' withSig def@Defn{..} = do
         -- We only instantiate the clauses to the current module parameters
         -- if the current module isn't the toplevel module
         unless weAreOnTop $
-          reportSDoc "agda2hs.compile.type" 6 $ "Applying module parameters to clauses: " <+> prettyTCM pars
+          reportSDoc "agda2hs.compile.type" 8 $ "Applying module parameters to clauses: " <+> prettyTCM pars
         let clauses = if weAreOnTop then filtered else filtered `apply` pars
 
         typ <- if weAreOnTop then pure defType else piApplyM defType pars
@@ -228,7 +228,7 @@ compileClause' curModule projName x ty c@Clause{..} = do
 compilePats :: Type -> NAPs -> C [Hs.Pat ()]
 compilePats _ [] = pure []
 compilePats ty ((namedArg -> ProjP po pn):ps) = do
-  reportSDoc "agda2hs.compile" 6 $ "compiling copattern: " <+> text (prettyShow pn)
+  reportSDoc "agda2hs.compile" 10 $ "compiling copattern: " <+> text (prettyShow pn)
   unlessM (asks copatternsEnabled `or2M` (isJust <$> isUnboxProjection pn)) $
     genericDocError =<< "not supported in Haskell: copatterns"
 
@@ -239,7 +239,7 @@ compilePats ty ((namedArg -> ProjP po pn):ps) = do
 
 compilePats ty ((namedArg -> pat):ps) = do
   (a, b) <- mustBePi ty
-  reportSDoc "agda2hs.compile.pattern" 5 $ text "Compiling pattern:" <+> prettyTCM pat
+  reportSDoc "agda2hs.compile.pattern" 10 $ text "Compiling pattern:" <+> prettyTCM pat
   let rest = compilePats (absApp b (patternToTerm pat)) ps
   compileDom a >>= \case
     DOInstance -> rest

src/Agda2Hs/Compile/Term.hs

@@ -128,7 +128,7 @@ primWord64FromNat ty args = compileArgs ty args >>= \case
 -- should really be named compileVar, TODO: rename compileVar
 compileVar :: Int -> Type -> [Term] -> C (Hs.Exp ())
 compileVar i ty es = do
-  reportSDoc "agda2hs.compile.term" 10 $ text "Reached variable"
+  reportSDoc "agda2hs.compile.term" 15 $ text "Reached variable"
   name <- compileDBVar i
   compileApp (hsVar name) ty es
 
@@ -383,7 +383,7 @@ compileCon h i ty args = do
 compileTerm :: Type -> Term -> C (Hs.Exp ())
 compileTerm ty v = do
 
-  reportSDoc "agda2hs.compile" 7  $ text "compiling term:" <+> prettyTCM v
+  reportSDoc "agda2hs.compile.term" 10  $ text "compiling term:" <+> prettyTCM v
 
   let bad s t = genericDocError =<< vcat
         [ text "agda2hs: cannot compile" <+> text (s ++ ":")

src/Agda2Hs/Compile/Type.hs

@@ -91,7 +91,7 @@ compileTopLevelType
     -> (Hs.Type () -> C a) -- ^ Continuation with the compiled type.
     -> C a
 compileTopLevelType keepType t cont = do
-    reportSDoc "agda2hs.compile.type" 12 $ text "Compiling top-level type" <+> prettyTCM t
+    reportSDoc "agda2hs.compile.type" 8 $ text "Compiling top-level type" <+> prettyTCM t
     -- NOTE(flupe): even though we only quantify variable for definitions inside anonymous modules,
     --              they will still get quantified over the toplevel module parameters.
     weAreOnTop <- isJust <$> liftTCM  (currentModule >>= isTopLevelModule)

src/Agda2Hs/Compile/Utils.hs

@@ -238,7 +238,7 @@ isInlinedFunction q = do
 
 checkInstance :: Term -> C ()
 checkInstance u | varOrDef u = liftTCM $ noConstraints $ do
-  reportSDoc "agda2hs.checkInstance" 5 $ text "checkInstance" <+> prettyTCM u
+  reportSDoc "agda2hs.checkInstance" 12 $ text "checkInstance" <+> prettyTCM u
   t <- infer u
   reportSDoc "agda2hs.checkInstance" 15 $ text "  inferred type:" <+> prettyTCM t
   (m, v) <- newInstanceMeta "" t