cleanup

Author: flupe

src/Agda2Lambox/Compile.hs

@@ -20,10 +20,8 @@ import Agda2Lambox.Compile.Inductive ( compileInductive )
 import LambdaBox
 
 
-compileDefinition :: QName -> CompileM (Maybe (KerName, GlobalDecl))
-compileDefinition q = do
-  defn@Defn{..} <- liftTCM $ getConstInfo q
-
+compileDefinition :: Definition -> CompileM (Maybe (KerName, GlobalDecl))
+compileDefinition defn@Defn{..} = do
   fmap (qnameToKerName defName,) <$> -- prepend kername
     case theDef of
       Constructor{conData} -> Nothing <$ requireDef conData

src/Agda2Lambox/Compile/Monad.hs

@@ -3,7 +3,6 @@
 module Agda2Lambox.Compile.Monad
   ( CompileM
   , requireDef
-  , compile
   , compileLoop
   ) where
 
@@ -15,8 +14,8 @@ import Data.Set qualified as Set
 import Queue.Ephemeral ( EphemeralQueue(..) )
 import Queue.Ephemeral qualified as Queue
 
-import Agda.Syntax.Internal ( QName )
-import Agda.TypeChecking.Monad.Base ( TCM, MonadTCEnv, MonadTCM, MonadTCState, MonadTCEnv, HasOptions )
+import Agda.Compiler.Backend ( QName, Definition, getConstInfo )
+import Agda.TypeChecking.Monad.Base ( TCM, MonadTCEnv, MonadTCM(liftTCM), MonadTCState, MonadTCEnv, HasOptions )
 import Agda.Utils.List ( mcons )
 
 -- | Backend compilation state.
@@ -32,11 +31,11 @@ data CompileState = CompileState
 --   i.e try to compile "related" definitions together.
 -- - We use an EphemeralQueue because we don't rely on persistence at all.
 
--- | Initial compile state. Empty queue, no name is known.
-initState :: CompileState
-initState = CompileState
-  { seenDefs     = Set.empty
-  , compileQueue = Queue.empty
+-- | Initial compile state, with a set of names required for compilation.
+initState :: [QName] -> CompileState
+initState qs = CompileState
+  { seenDefs     = Set.fromList qs
+  , compileQueue = Queue.fromList qs
   }
 
 -- | Backend compilation monad.
@@ -48,10 +47,6 @@ newtype CompileM a = Compile (StateT CompileState TCM a)
 -- deriving newtype (MonadState CompileState)
 -- NOTE(flupe): safe to not export this, to make sure the queue is indeed ephemeral
 
--- | Run a compilation unit in TCM.
-compile :: CompileM a -> TCM a
-compile (Compile c) = evalStateT c initState
-
 -- | Require a definition to be compiled.
 requireDef :: QName -> CompileM ()
 requireDef q = Compile $ do
@@ -71,8 +66,14 @@ nextUnit = Compile $
     Full q queue -> Just q <$ modify \s -> s { compileQueue = queue }
 
 -- | Run the processing function as long as there are names to be compiled.
-compileLoop :: (QName -> CompileM (Maybe a)) -> CompileM [a]
-compileLoop step =
-  nextUnit >>= \case
+compileLoop
+  :: (Definition -> CompileM (Maybe a)) -- ^ The compilation function
+  -> [QName]                            -- ^ Names to compile
+  -> TCM [a]
+compileLoop step = evalStateT unloop . initState
+  where
+  loop@(Compile unloop) = nextUnit >>= \case
     Nothing -> pure []
-    Just q  -> mcons <$> step q <*> compileLoop step
+    Just q  -> do
+      mr <- step =<< (liftTCM $ getConstInfo q)
+      mcons mr <$> loop

src/Agda2Lambox/Compile/Term.hs

@@ -3,7 +3,6 @@ module Agda2Lambox.Compile.Term
   ( compileTerm
   ) where
 
-import Control.Monad ( mapM )
 import Control.Monad.Fail ( MonadFail )
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Reader.Class ( MonadReader, ask )
@@ -17,6 +16,7 @@ import Agda.Compiler.Backend ( getConstInfo, theDef, pattern Datatype, dataMutua
 import Agda.Syntax.Abstract.Name ( ModuleName(..), QName(..) )
 import Agda.Syntax.Common ( Erased(..) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
+import Agda.Syntax.Literal
 import Agda.Syntax.Treeless ( TTerm(..), TAlt(..), CaseInfo(..), CaseType(..) )
 import Agda.TypeChecking.Datatypes ( getConstructorData, getConstructors )
 import Agda.TypeChecking.Monad.Base ( TCM , liftTCM, MonadTCEnv, MonadTCM )
@@ -47,14 +47,11 @@ initEnv = CompileEnv
   }
 
 -- | Compilation monad.
-newtype C a = C (ReaderT CompileEnv CompileM a)
-  deriving newtype (Functor, Applicative, Monad, MonadIO)
-  deriving newtype (MonadFail, MonadReader CompileEnv)
-  deriving newtype (MonadTCEnv, MonadTCState, HasOptions, MonadTCM)
+type C a = ReaderT CompileEnv CompileM a
 
 -- | Run a compilation unit in @TCM@, in the initial environment.
 runC :: C a -> CompileM a
-runC (C m) = runReaderT m initEnv
+runC m = runReaderT m initEnv
 
 -- | Increase the number of locally-bound variables.
 underBinders :: Int -> C a -> C a
@@ -69,10 +66,6 @@ underBinder = underBinders 1
 withMutuals :: [QName] -> C a -> C a
 withMutuals ms = local \e -> e { mutuals = reverse ms }
 
--- | Require a name to be compiled
-require :: QName -> C ()
-require = C . lift . requireDef
-
 -- * Term conversion
 
 -- | Convert a treeless term to its λ□ equivalent.
@@ -92,21 +85,26 @@ compileTermC = \case
   TDef qn -> do
     CompileEnv{mutuals, boundVars} <- ask
     case qn `elemIndex` mutuals of
-      Nothing -> do require qn; pure $ LConst $ qnameToKName qn
+      Nothing -> do lift $ requireDef qn; pure $ LConst $ qnameToKName qn
       Just i  -> pure $ LRel  $ i + boundVars
 
-  TCon q             -> do require q; liftTCM (toConApp q [])
-  TApp (TCon q) args -> do require q; liftTCM . toConApp q =<< mapM compileTermC args
+  TCon q -> do
+    lift $ requireDef q
+    liftTCM $ toConApp q []
+
+  TApp (TCon q) args -> do
+    lift $ requireDef q
+    liftTCM . toConApp q =<< traverse compileTermC args
   -- ^ For dealing with fully-applied constructors
 
   TApp u es -> do
     cu  <- compileTermC u
-    ces <- mapM compileTermC es
+    ces <- traverse compileTermC es
     pure $ foldl' LApp cu ces
 
   TLam t -> underBinder $ LLam <$> compileTermC t
 
-  TLit l -> fail "literals not supported"
+  TLit l -> compileLit l
 
   TLet u v -> LLet <$> compileTermC u
                    <*> underBinder (compileTermC v)
@@ -116,7 +114,7 @@ compileTermC = \case
       Erased _    -> fail "Erased matches not supported."
       NotErased _ -> do
         cind  <- compileCaseType caseType
-        LCase cind 0 (LRel n) <$> mapM compileAlt talts
+        LCase cind 0 (LRel n) <$> traverse compileAlt talts
 
   TUnit   -> return LBox
   TSort   -> return LBox
@@ -125,10 +123,14 @@ compileTermC = \case
   TCoerce tt  -> fail "Coerces not supported."
   TError terr -> fail "Errors not supported."
 
+compileLit :: Literal -> C LBox.Term
+compileLit = \case
+  l        -> fail $ "unsupported literal: " <> prettyShow l
 
 compileCaseType :: CaseType -> C LBox.Inductive
 compileCaseType = \case
-  CTData qn -> do require qn; liftTCM $ toInductive qn
+  CTData qn -> do lift $ requireDef qn
+                  liftTCM $ toInductive qn
   _         -> fail "case type not supported"
 
 

src/Main.hs

@@ -2,7 +2,7 @@
 -- | The agda2lambox Agda backend
 module Main (main) where
 
-import Control.Monad ( unless, when, forM_ )
+import Control.Monad ( unless, when, forM_, filterM )
 import Control.Monad.IO.Class ( liftIO )
 import Control.DeepSeq ( NFData )
 import Data.Function ( (&) )
@@ -25,16 +25,15 @@ import Agda.Utils.Monad ( whenM )
 
 import Agda.Utils ( pp, hasPragma, isDataOrRecDef )
 import Agda2Lambox.Compile.Utils (qnameToKName)
-import Agda2Lambox.Compile.Monad (compile, compileLoop, requireDef)
-import Agda2Lambox.Compile (compileDefinition)
+import Agda2Lambox.Compile.Monad (compileLoop)
+import Agda2Lambox.Compile       (compileDefinition)
 import CoqGen    ( ToCoq(ToCoq) )
 import LambdaBox ( KerName, GlobalDecl, qnameToKerName, CoqModule(..) )
 
 
 main :: IO ()
 main = runAgda [agda2lambox]
 
-
 -- | Backend options.
 data Options = Options { optOutDir :: Maybe FilePath }
   deriving (Generic, NFData)
@@ -48,11 +47,7 @@ defaultOptions :: Options
 defaultOptions = Options { optOutDir = Nothing }
 
 -- | Backend module environments.
-data ModuleEnv = ModuleEnv
-  { modProgs :: IORef [QName]
-     -- ^ Names of programs to extract in a module
-  }
-
+type ModuleEnv = ()
 type ModuleRes = ()
 
 -- | The adga2lambox backend.
@@ -73,7 +68,7 @@ agda2lambox = Backend backend
       , postCompile           = \ _ _ _ -> return ()
       , preModule             = moduleSetup
       , postModule            = writeModule
-      , compileDef            = compileDef'
+      , compileDef            = \ _ _ _ -> pure . defName
       , scopeCheckingSuffices = False
       , mayEraseType          = \ _ -> return True
       }
@@ -84,36 +79,18 @@ moduleSetup
   -> TCM (Recompile ModuleEnv ModuleRes)
 moduleSetup _ _ m _ = do
   setScope . iInsideScope =<< curIF
-  Recompile . ModuleEnv <$> liftIO (newIORef [])
-
+  pure $ Recompile ()
 
-compileDef'
-  :: Options -> ModuleEnv -> IsMain
-  -> Definition
-  -> TCM QName
-compileDef' opts menv ismain Defn{defName} = do
-  -- if it has a pragma, that's a program!
-  when (ismain == IsMain) $
-    whenM (hasPragma defName) $
-      liftIO $ modifyIORef' (modProgs menv) (defName :)
 
-  pure defName
-
-
--- | Collect global definitions and programs in a module
--- and write them to disk.
 writeModule
   :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName
   -> [QName]
   -> TCM ModuleRes
-writeModule opts menv NotMain _ _ = pure ()
+writeModule opts menv NotMain _ _   = pure ()
 writeModule opts menv IsMain m defs = do
-  programs   <- liftIO $ readIORef $ modProgs menv
-  outDir     <- flip fromMaybe (optOutDir opts) <$> compileDir
-
-  decls <- compile do
-    forM_ (reverse defs) requireDef
-    compileLoop compileDefinition
+  programs <- filterM hasPragma defs
+  outDir   <- flip fromMaybe (optOutDir opts) <$> compileDir
+  decls    <- compileLoop compileDefinition $ reverse defs
 
   liftIO $ createDirectoryIfMissing True outDir
 

test/Imports.agda

@@ -1,4 +1,5 @@
 open import Agda.Builtin.Bool
+open import Agda.Builtin.List
 
-test : Bool
-test = true
+test : List Bool
+test = true ∷ false ∷ []

test/Map.agda

@@ -12,7 +12,7 @@ data List (A : Set) : Set where
   _::_ : A -> List A -> List A
 
 xs : List Nat
-xs = zero :: succ zero :: succ (succ zero) :: []
+xs = zero :: []
 
 map : {A B : Set} -> (A -> B) -> List A -> List B
 map f [] = []

test/Nat.agda

@@ -1,21 +1,21 @@
-data Nat : Set where
-  zero : Nat
-  succ : Nat → Nat
+open import Agda.Builtin.Nat
 
 one : Nat
-one = succ zero
+one = suc zero
 
+{-
 add : Nat → Nat → Nat
 add zero y = y
-add (succ x) y = succ (add x y)
+add (suc x) y = suc (add x y)
 
 incr : Nat → Nat
-incr = succ
+incr = suc
 
 deux trois : Nat
-deux  = succ (succ zero)
-trois = succ (succ (succ zero))
+deux  = suc (suc zero)
+trois = suc (suc (suc zero))
 
 prog : Nat
 prog = add trois deux
 {-# COMPILE AGDA2LAMBOX prog #-}
+-}