reinstate debug printing

Author: flupe

src/Agda2Lambox/Convert/Data.hs

@@ -5,8 +5,9 @@ module Agda2Lambox.Convert.Data
   ) where
 
 import Control.Monad.Reader ( ask, liftIO )
-import Control.Monad ( forM )
+import Control.Monad ( forM, when, unless )
 import Data.List ( elemIndex )
+import Data.Maybe ( isJust )
 
 import Utils
 
@@ -31,10 +32,15 @@ import Agda.Utils.Monad (guardWithError)
 
 -- | Convert a datatype definition to a Lambdabox declaration.
 convertDatatype :: Definition :~> GlobalDecl
-convertDatatype defn@Defn{defName, theDef} =
+convertDatatype defn@Defn{defName, theDef, defMutual} =
   withCurrentModule (qnameModule defName) do
     let Datatype{..} = theDef
 
+    let Just muts = dataMutual
+
+    unless (length muts < 2) $
+      fail $ "mututal datatypes not supported" <> prettyShow dataMutual
+
     ctors :: [ConstructorBody]
       <- forM dataCons \cname -> do
            DataCon arity <- getConstructorInfo cname

src/CoqGen.hs

@@ -160,12 +160,6 @@ instance Pretty (ToCoq t) => Pretty (ToCoq (Def t)) where
            , ("rarg",  pcoq dArgs)
            ]
 
--- | Generated module
-data CoqModule = CoqModule
-  { coqEnv      :: [(KerName, GlobalDecl)]
-  , coqPrograms :: [KerName]
-  }
-
 instance Pretty (ToCoq CoqModule) where
   pretty (ToCoq CoqModule{..}) = vsep
     [ vcat

src/LambdaBox.hs

@@ -186,6 +186,13 @@ data GlobalDecl
 
 type GlobalDecls = [(KerName, GlobalDecl)]
 
+-- | Generated module
+data CoqModule = CoqModule
+  { coqEnv      :: [(KerName, GlobalDecl)]
+  , coqPrograms :: [KerName]
+  }
+
+
 instance Pretty Term where
   prettyPrec p v =
     case v of
@@ -227,3 +234,32 @@ instance Pretty Name where
   prettyPrec _ = \case
     Anon -> text "_"
     Named s -> text s
+
+
+instance Pretty ConstructorBody where
+  pretty Ctor{..} =
+    pretty ctorName <+> parens (pretty ctorArgs <+> "arg(s)")
+
+instance Pretty OneInductiveBody where
+  pretty OneInductive{..} =
+    vcat
+      [ pretty indName
+      , "constructors:" <+> pretty indCtors
+      ]
+
+instance Pretty GlobalDecl where
+  pretty = \case
+    ConstantDecl (Just b) ->
+      hang "constant:" 2 $ pretty b
+
+    ConstantDecl Nothing ->
+      "primitive constant"
+
+    InductiveDecl MutualInductive{..} ->
+      hang "mutual inductive(s):" 2 $ 
+        vsep $ map pretty indBodies
+
+instance Pretty CoqModule where
+  pretty CoqModule{..} =
+    vsep $ flip map (reverse coqEnv) \(kn, d) ->
+      hang (pretty kn <> ":") 2 (pretty d)

src/Main.hs

@@ -24,8 +24,8 @@ import Agda2Lambox.Convert.Function ( convertFunction )
 import Agda2Lambox.Convert.Data     ( convertDatatype )
 import Agda2Lambox.Convert.Record   ( convertRecord   )
 import Agda2Lambox.Monad ( runC0, inMutuals )
-import CoqGen ( ToCoq(ToCoq), CoqModule(..) )
-import LambdaBox ( KerName, GlobalDecl, qnameToKerName )
+import CoqGen ( ToCoq(ToCoq) )
+import LambdaBox ( KerName, GlobalDecl, qnameToKerName, CoqModule(CoqModule) )
 
 
 main :: IO ()
@@ -109,9 +109,15 @@ writeModule opts menv _ m (reverse . catMaybes -> cdefs) = do
 
   liftIO $ createDirectoryIfMissing True outDir
 
+  let mod = CoqModule cdefs progs
+
   unless (null cdefs) $ liftIO do
-    putStrLn $ "Writing " <> fileName ".v"
+    putStrLn $ "Writing " <> fileName ".{v,txt}"
+
+    writeFile (fileName ".txt")
+      $ (<> "\n")
+      $ pp $ mod
 
     writeFile (fileName ".v")
       $ (<> "\n")
-      $ pp $ ToCoq $ CoqModule cdefs progs
+      $ pp $ ToCoq $ mod