[ re #210 ] Add some debug prints

agda · Oct 30, 2023 · 8e2f974 · 8e2f974
1 parent 0ae2778
commit 8e2f974
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 1 deletion.
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
@@ -131,6 +131,8 @@ compileClause' :: ModuleName -> Hs.Name () -> Clause -> C (Maybe (Hs.Match ()))
 compileClause' curModule x c@Clause{ clauseBody = Nothing} = return Nothing
 compileClause' curModule x c@Clause{..} = do
   reportSDoc "agda2hs.compile" 7 $ "compiling clause: " <+> prettyTCM c
+  reportSDoc "agda2hs.compile" 17 $ "Old context: " <+> (prettyTCM =<< getContext)
+  reportSDoc "agda2hs.compile" 17 $ "Clause telescope: " <+> prettyTCM clauseTel
   addContext (KeepNames clauseTel) $ do
     ps <- compilePats namedClausePats
     let isWhereDecl = not . isExtendedLambdaName

diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
@@ -91,6 +91,7 @@ compileTopLevelType :: Bool -> Type -> (Hs.Type () -> C a) -> C a
 compileTopLevelType keepType t cont = do
     reportSDoc "agda2hs.compile.type" 12 $ text "Compiling top-level type" <+> prettyTCM t
     modTel <- moduleParametersToDrop =<< currentModule
+    reportSDoc "agda2hs.compile.type" 19 $ text "Module parameters to drop: " <+> prettyTCM modTel
     go modTel cont
   where
     go :: Telescope -> (Hs.Type () -> C a) -> C a

diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
@@ -163,8 +163,12 @@ moduleParametersToDrop mod = do
    isDatatypeModule mod >>= \case
      Just _ -> return EmptyTel
      Nothing -> do
+       reportSDoc "agda2hs.moduleParameters" 25 $ text "Current context: " <+> (prettyTCM =<< getContext)
        ctxArgs <- getContextArgs
-       (`apply` ctxArgs) <$> lookupSection mod
+       reportSDoc "agda2hs.moduleParameters" 25 $ text "Context arguments: " <+> prettyTCM ctxArgs
+       sec <- lookupSection mod
+       reportSDoc "agda2hs.moduleParameters" 25 $ text "Module section: " <+> prettyTCM sec
+       return $ sec `apply` ctxArgs
 
 isUnboxRecord :: QName -> C (Maybe Strictness)
 isUnboxRecord q = do