fix error reporting

Author: flupe

src/Agda2Lambox/Compile/Target.hs

@@ -4,8 +4,11 @@ module Agda2Lambox.Compile.Target
   ( Typing(..)
   , Target(..)
   , WhenTyped(..)
+  , WhenUntyped(..)
   , getTyped
+  , getUntyped
   , whenTyped
+  , whenUntyped
   ) where
 
 import Data.Foldable (Foldable(foldMap))
@@ -40,16 +43,45 @@ instance Foldable (WhenTyped t) where
   foldMap f None     = mempty
   foldMap f (Some x) = f x
 
+-- | Type wrapper that contains a value iff we're in the untyped setting.
+data WhenUntyped (t :: Typing) (a :: Type) :: Type where
+  NoneU ::      WhenUntyped Typed a
+  SomeU :: a -> WhenUntyped Untyped   a
 
--- | Retrieve a value when it's there for sure.
+instance Functor (WhenUntyped t) where
+  fmap f NoneU     = NoneU
+  fmap f (SomeU x) = SomeU (f x)
+
+instance Applicative (WhenUntyped Untyped) where
+  pure = SomeU
+  SomeU f <*> SomeU x = SomeU (f x)
+
+instance Monad (WhenUntyped Untyped) where
+  SomeU x >>= f = f x
+
+instance Foldable (WhenUntyped t) where
+  foldMap f NoneU     = mempty
+  foldMap f (SomeU x) = f x
+
+
+-- | Retrieve a value when it's there for sure, in the typed setting.
 getTyped :: WhenTyped Typed a ->  a
 getTyped (Some x) = x
 
+-- | Retrieve a value when it's there for sure, in the untyped setting.
+getUntyped :: WhenUntyped Untyped a ->  a
+getUntyped (SomeU x) = x
+
 -- | Only perform a computation when targetting typed.
 whenTyped :: Applicative m => Target t -> m a -> m (WhenTyped t a)
 whenTyped ToUntyped _ = pure None
 whenTyped ToTyped   x = Some <$> x
 
+-- | Only perform a computation when targetting untyped.
+whenUntyped :: Applicative m => Target t -> m a -> m (WhenUntyped t a)
+whenUntyped ToTyped   _ = pure NoneU
+whenUntyped ToUntyped x = SomeU <$> x
+
 instance NFData (Target t) where
   rnf ToTyped   = ()
   rnf ToUntyped = ()

src/CoqGen.hs

@@ -4,6 +4,7 @@ module CoqGen (prettyCoq) where
 
 import Data.Bifunctor(bimap)
 import Data.List(intercalate)
+import Data.List.NonEmpty qualified as NEL
 
 import Agda.Syntax.Common.Pretty
 import LambdaBox
@@ -189,8 +190,8 @@ instance ToCoq t (GlobalEnv t) where
   pcoq ToUntyped (GlobalEnv env) = upcoq env
   pcoq ToTyped   (GlobalEnv env) = tpcoq $ flip map env \(kn, decl) -> ((kn, True), decl)
 
-instance ToCoq t (CoqModule t) where
-  pcoq ToUntyped CoqModule{..} = vsep
+instance ToCoq t (LBoxModule t) where
+  pcoq ToUntyped LBoxModule{..} = vsep
     [ vcat
         [ "From Coq             Require Import List."
         , "From MetaCoq.Common  Require Import BasicAst Kernames Universes."
@@ -201,11 +202,11 @@ instance ToCoq t (CoqModule t) where
         ]
 
     , hang "Definition env : global_declarations :=" 2 $
-        upcoq coqEnv <> "."
+        upcoq lboxEnv <> "."
 
     , "Compute @check_wf_glob eflags env."
 
-    , vsep $ flip map (zip [1..] $ reverse coqPrograms) \(i :: Int, kn) -> 
+    , vsep $ flip map (zip [1..] $ reverse $ NEL.toList $ getUntyped lboxMain) \(i :: Int, kn) -> 
         let progname = "prog" <> pretty i in vsep
         [ hang ("Definition " <> progname <> " : program :=") 2 $
             upcoq (text "env" :: Doc, LConst kn) 
@@ -214,7 +215,7 @@ instance ToCoq t (CoqModule t) where
         ]
     ]
 
-  pcoq ToTyped CoqModule{..} = vsep
+  pcoq ToTyped LBoxModule{..} = vsep
     [ vcat
         [ "From Coq             Require Import List."
         , "From MetaCoq.Common  Require Import BasicAst Kernames Universes."
@@ -224,5 +225,5 @@ instance ToCoq t (CoqModule t) where
         , "Import ListNotations."
         ]
 
-    , hang "Definition env : global_env :=" 2 $ tpcoq coqEnv <> "."
+    , hang "Definition env : global_env :=" 2 $ tpcoq lboxEnv <> "."
     ]

src/LambdaBox/Env.hs

@@ -18,6 +18,7 @@ module LambdaBox.Env where
 
 
 import Data.Kind ( Type )
+import Data.List.NonEmpty ( NonEmpty )
 
 import Agda.Syntax.Common.Pretty
 
@@ -121,9 +122,9 @@ data GlobalDecl (t :: Typing) :: Type where
 newtype GlobalEnv t = GlobalEnv [(KerName, GlobalDecl t)]
 
 -- | Generated module
-data CoqModule t = CoqModule
-  { coqEnv      :: GlobalEnv t
-  , coqPrograms :: [KerName]
+data LBoxModule t = LBoxModule
+  { lboxEnv  :: GlobalEnv t
+  , lboxMain :: WhenUntyped t (NonEmpty KerName)
   }
 
 
@@ -171,5 +172,8 @@ instance Pretty (GlobalEnv t) where
     vsep $ flip map (reverse env) \(kn, d) ->
       hang (pretty kn <> ":") 2 (pretty d)
 
-instance Pretty (CoqModule t) where
-  pretty CoqModule{..} = pretty coqEnv
+instance Pretty (LBoxModule t) where
+  pretty LBoxModule{..} = vcat
+    [ pretty lboxEnv
+    , flip foldMap lboxMain \kn -> "main program:" <+> pretty kn
+    ]

src/Main.hs

@@ -7,13 +7,15 @@ import Control.Monad ( unless, filterM )
 import Control.Monad.IO.Class ( liftIO )
 import Control.DeepSeq ( NFData(rnf) )
 import Data.Function ( (&) )
+import Data.List.NonEmpty ( NonEmpty )
+import Data.List.NonEmpty qualified as NEL
 import Data.Maybe ( fromMaybe )
 import Data.Version ( showVersion )
 import Data.Text ( pack )
 import GHC.Generics ( Generic )
 import System.Console.GetOpt ( OptDescr(Option), ArgDescr(..) )
 import System.Directory ( createDirectoryIfMissing )
-import System.FilePath ( (</>) )
+import System.FilePath ( (</>), (-<.>) )
 import Data.Text.Lazy.IO qualified as LText
 
 import Paths_agda2lambox ( version )
@@ -32,6 +34,7 @@ import Agda2Lambox.Compile       (compile)
 import CoqGen    ( prettyCoq  )
 import SExpr     ( prettySexp )
 import LambdaBox.Env
+import LambdaBox.Names (KerName)
 import Agda2Lambox.Compile.Monad (runCompile, CompileEnv(..))
 
 
@@ -124,25 +127,37 @@ writeModule
 writeModule opts menv NotMain _ _   = pure ()
 writeModule Options{..} menv IsMain m defs = do
   outDir   <- flip fromMaybe optOutDir <$> compileDir
-  env      <- runCompile (CompileEnv optNoBlocks) $ compile optTarget defs
   programs <- filterM hasPragma defs
 
+  -- get defs annotated with a COMPILE pragma
+  -- throw an error if none, when targetting untyped lbox
+  mains    <- getMain optTarget programs
+  env      <- runCompile (CompileEnv optNoBlocks) $ compile optTarget defs
+
   liftIO $ createDirectoryIfMissing True outDir
 
-  let fileName = (outDir </>) . moduleNameToFileName m
-      coqMod   = CoqModule env (map qnameToKName programs)
+  let fileName = outDir </> prettyShow m
+  let lboxMod  = LBoxModule env mains
 
   liftIO do
-    putStrLn $ "Writing " <> fileName ".txt"
-    pp coqMod <> "\n" & writeFile (fileName ".txt")
+    putStrLn $ "Writing " <> fileName -<.> ".txt"
+    pp lboxMod <> "\n" & writeFile (fileName -<.> ".txt")
 
   liftIO $ case optOutput of
     RocqOutput -> do
-      putStrLn $ "Writing " <> fileName ".v"
-      prettyCoq optTarget coqMod <> "\n"
-        & writeFile (fileName ".v")
+      putStrLn $ "Writing " <> fileName -<.> ".v"
+      prettyCoq optTarget lboxMod <> "\n"
+        & writeFile (fileName -<.> ".v")
 
     AstOutput -> do
-      putStrLn $ "Writing " <> fileName ".ast"
-      prettySexp optTarget coqMod <> "\n"
-        & LText.writeFile (fileName ".ast")
+      putStrLn $ "Writing " <> fileName -<.> ".ast"
+      prettySexp optTarget lboxMod <> "\n"
+        & LText.writeFile (fileName -<.> ".ast")
+
+  where
+    getMain :: Target t -> [QName] -> TCM (WhenUntyped t (NonEmpty KerName))
+    getMain ToTyped   _  = pure NoneU
+    getMain ToUntyped qs =
+      case NEL.nonEmpty qs of
+        Nothing -> genericError "No main program specified. Please use a COMPILE pragma."
+        Just ms -> pure $ SomeU (NEL.map qnameToKName ms)

src/SExpr.hs

@@ -5,6 +5,7 @@ module SExpr (ToSexp, prettySexp) where
 
 import Data.Bifunctor(bimap)
 import Data.List(intercalate)
+import Data.List.NonEmpty qualified as NEL (head)
 
 import Agda.Syntax.Common.Pretty
 import LambdaBox
@@ -184,8 +185,7 @@ instance ToSexp t (GlobalEnv t) where
   toSexp t@ToUntyped (GlobalEnv env) = toSexp t env
   toSexp t@ToTyped   (GlobalEnv env) = toSexp t $ flip map env \(kn, decl) -> ((kn, True), decl)
 
--- TODO(flupe): handle programs
-instance ToSexp t (CoqModule t) where
-  toSexp t@ToUntyped CoqModule{..} =
-    toSexp t (coqEnv, ctor t "tConst" [S $ head coqPrograms])
-  toSexp t@ToTyped   CoqModule{..} = toSexp t coqEnv
+instance ToSexp t (LBoxModule t) where
+  toSexp t@ToUntyped LBoxModule{..} =
+    toSexp t (lboxEnv, ctor t "tConst" [S $ NEL.head $ getUntyped lboxMain])
+  toSexp t@ToTyped LBoxModule{..} = toSexp t lboxEnv