add flag for disabling blocks translation

Author: flupe

Makefile

@@ -2,10 +2,16 @@
 	agda2lambox -o build test/$*.agda
 
 %.wasm: %.ast
-	lbox wasm -o demo/$*.wasm build/$*.ast
+	lbox wasm -o demo/$@ build/$*.ast
+
+%.elm: %.typed
+	lbox elm -o demo/$@ build/$*.ast
+
+%.rs: %.typed
+	lbox rust -o demo/$@ build/$*.ast
 
 %.v:
 	agda2lambox -o build --rocq test/$*.agda
 
 %.typed:
-	agda2lambox -o build --typed test/$*.agda
+	agda2lambox -o build --typed --no-blocks test/$*.agda

src/Agda2Lambox/Compile.hs

@@ -34,7 +34,7 @@ import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), ConstantBody(..))
 
 
 -- | Compile the given names into to a λ□ environment.
-compile :: Target t -> [QName] -> TCM (GlobalEnv t)
+compile :: Target t -> [QName] -> CompileM (GlobalEnv t)
 compile t qs = do
   items <- compileLoop (compileDefinition t) qs
   pure $ GlobalEnv $ map itemToEntry items

src/Agda2Lambox/Compile/Monad.hs

@@ -1,31 +1,48 @@
-{-# LANGUAGE DerivingVia, GeneralizedNewtypeDeriving, OverloadedStrings, DeriveFunctor, DeriveTraversable #-}
+{-# LANGUAGE DerivingVia, GeneralizedNewtypeDeriving, OverloadedStrings, DeriveFunctor, DeriveTraversable, NamedFieldPuns #-}
 -- | Compilation monad.
 module Agda2Lambox.Compile.Monad
   ( CompileM
+  , CompileEnv(..)
   , requireDef
+  , runCompile
   , compileLoop
   , genericError
   , genericDocError
   , internalError
   , CompiledItem(..)
+  , ask
+  , asks
   ) where
 
 import Control.Monad ( unless )
+import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.IO.Class ( MonadIO )
+import Data.Bifunctor ( bimap )
 import Data.Set ( Set )
 import Data.Set qualified as Set
+import Data.Set qualified as Set
+import Data.Map qualified as Map
+import Data.Maybe ( catMaybes )
 
 import Agda.Syntax.Abstract (QName)
 import Agda.Compiler.Backend (getConstInfo, PureTCM, HasConstInfo, HasBuiltins, canonicalName)
 import Agda.TypeChecking.Monad (MonadDebug, MonadTrace, MonadAddContext)
 import Agda.TypeChecking.Monad.Debug (MonadDebug, reportSDoc)
 import Agda.TypeChecking.Monad.Base hiding (initState)
 import Agda.Utils.List ( mcons )
+import Agda.Utils.Monad ( unlessM )
 import Agda.TypeChecking.Pretty
 import Control.Monad.Error.Class (MonadError)
 
-import Agda2Lambox.Compile.Utils (CompiledItem(..), topoSort)
+import Data.Foldable (traverse_)
+
+-- | Compilation Environment
+data CompileEnv = CompileEnv
+  { noBlocks :: Bool
+      -- ^ When set to 'True', constructors take no arguments,
+      -- and regular function application is used instead.
+  }
 
 -- | Backend compilation state.
 data CompileState = CompileState
@@ -37,20 +54,21 @@ data CompileState = CompileState
     -- ^ (Locally) required definitions.
   }
 
--- | Initial compile state, with a set of names required for compilation.
-initState :: [QName] -> CompileState
-initState qs = CompileState
-  { seenDefs     = Set.fromList qs
-  , compileStack = qs
+-- Initial compile state.
+initState :: CompileState
+initState = CompileState
+  { seenDefs     = Set.empty
+  , compileStack = []
   , requiredDefs = Set.empty
   }
 
 -- | Backend compilation monad.
-newtype CompileM a = Compile (StateT CompileState TCM a)
+newtype CompileM a = Compile (ReaderT CompileEnv (StateT CompileState TCM) a)
   deriving newtype (Functor, Applicative, Monad)
   deriving newtype (MonadIO, MonadFail, MonadDebug, ReadTCState, MonadTrace)
   deriving newtype (MonadError TCErr, MonadTCEnv, MonadTCState, HasOptions, MonadTCM)
   deriving newtype (MonadAddContext, MonadReduce, HasConstInfo, HasBuiltins, PureTCM)
+  deriving newtype (MonadReader CompileEnv)
 
 -- | Require a definition to be compiled.
 requireDef :: QName -> CompileM ()
@@ -89,19 +107,71 @@ trackDeps (Compile c) = Compile do
   deps <- gets requiredDefs
   pure (x, Set.toList deps)
 
+-- | Run a compile action in 'TCM'.
+runCompile :: CompileEnv -> CompileM a -> TCM a
+runCompile env (Compile c) = evalStateT (runReaderT c env) initState
+
 -- | Run the processing function as long as there are names to be compiled.
 --  Returns a list of compiled items, (topologically) sorted by dependency order.
 --  This means that whenever @A@ depends on @B@, @A@ will appear before @B@ in the list.
 compileLoop
   :: forall a. (Definition -> CompileM (Maybe a))
-       -- ^ The compilation function
+             -- ^ The compilation function
   -> [QName] -- ^ Initial names to compile
-  -> TCM [CompiledItem a]
-compileLoop step names = topoSort <$> evalStateT unloop (initState names)
+  -> CompileM [CompiledItem a]
+compileLoop step names = do
+  traverse_ requireDef names
+  topoSort <$> loop
   where
   loop :: CompileM [CompiledItem (Maybe a)]
   loop@(Compile unloop) = nextUnit >>= \case
     Nothing -> pure []
     Just q  -> do
       (mr, deps) <- trackDeps . step =<< (liftTCM $ getConstInfo q)
       (CompiledItem q deps mr:) <$> loop
+
+
+-- * Compilation items and topological sort
+
+-- | Named compilation item, with a set of dependencies.
+data CompiledItem a = CompiledItem
+  { itemName  :: QName
+  , itemDeps  :: [QName]
+  , itemValue :: a
+  } deriving (Functor, Foldable, Traversable)
+
+-- | Stateful monad for the topological sort.
+-- State contains the list of items that have been permanently inserted,
+-- along with their names.
+type TopoM a = State (Set QName, [CompiledItem a])
+
+-- | Topological sort of compiled items, based on dependencies.
+-- Skipped items are required for dependency analysis, as they
+-- can transively force ordering
+-- (e.g constructors are skipped but force compilation of their datatype).
+-- In the end, we get a list of items that are effectively compiled.
+topoSort :: forall a. [CompiledItem (Maybe a)] -> [CompiledItem a]
+topoSort defs = snd $ execState (traverse (visit Set.empty) defs) (Set.empty, [])
+  where
+    items = Map.fromList $ map (\x -> (itemName x, x)) defs
+
+    -- | Whether an item has been permanently inserted already
+    isMarked :: QName -> TopoM a Bool
+    isMarked q = Set.member q <$> gets fst
+
+    push :: CompiledItem (Maybe a) -> TopoM a ()
+    push item@CompiledItem{itemName, itemValue}
+      | Just value <- itemValue
+      = modify $ bimap (Set.insert itemName) (item {itemValue = value}:)
+      | otherwise = pure ()
+
+    visit :: Set QName -> CompiledItem (Maybe a) -> TopoM a ()
+    visit temp item@CompiledItem{..} = do
+      -- NOTE(flupe): Visiting an item that has already been temporarily marked
+      --  means something went wrong and we have a cycle in the graph.
+      --  We could throw an error, but this should never happen.
+      --  Here, we continue and pick an arbitrary order.
+      unlessM ((Set.member itemName temp ||) <$> isMarked itemName) do
+        let deps = catMaybes $ (`Map.lookup` items) <$> itemDeps
+        traverse (visit (Set.insert itemName temp)) deps
+        push item

src/Agda2Lambox/Compile/Term.hs

@@ -35,7 +35,7 @@ import Agda2Lambox.Compile.Monad
 -- * Term compilation monad
 
 -- | λ□ compilation environment.
-data CompileEnv = CompileEnv
+data TermEnv = TermEnv
   { mutuals   :: [QName]
     -- ^ When we compile mutual function definitions,
     -- they are introduced at the top of the local context.
@@ -45,14 +45,14 @@ data CompileEnv = CompileEnv
 
 -- | Initial compilation environment.
 -- No mutuals, no bound variables.
-initEnv :: CompileEnv
-initEnv = CompileEnv
+initEnv :: TermEnv
+initEnv = TermEnv
   { mutuals   = []
   , boundVars = 0
   }
 
 -- | Compilation monad.
-type C a = ReaderT CompileEnv CompileM a
+type C a = ReaderT TermEnv CompileM a
 
 -- | Run a compilation unit in @TCM@, in the initial environment.
 runC :: C a -> CompileM a
@@ -100,7 +100,7 @@ compileTermC = \case
   --   - they cannot be types.
   TDef qn -> do
     qn <- liftTCM $ canonicalName qn
-    CompileEnv{mutuals, boundVars} <- ask
+    TermEnv{mutuals, boundVars} <- ask
     case qn `elemIndex` mutuals of
       Nothing -> do lift $ requireDef qn
                     pure $ LConst $ qnameToKName qn
@@ -109,7 +109,7 @@ compileTermC = \case
   TCon q -> do
     q <- liftTCM $ canonicalName q
     lift $ requireDef q
-    liftTCM $ toConApp q []
+    lift $ toConApp q []
 
   -- TODO: maybe not ignore seq? (c.f. issue #12)
   TApp (TPrim PSeq) args -> compileTermC (last args)
@@ -118,7 +118,7 @@ compileTermC = \case
     q <- liftTCM $ canonicalName q
     lift $ requireDef q
     traverse compileTermC args
-      >>= liftTCM . toConApp q
+      >>= lift . toConApp q
   -- ^ For dealing with fully-applied constructors
 
   TApp u es -> do
@@ -154,26 +154,14 @@ compileLit = \case
     qn <- liftTCM $ getBuiltinName_ builtinNat
     qz <- liftTCM $ getBuiltinName_ builtinZero
     qs <- liftTCM $ getBuiltinName_ builtinSuc
-    z  <- liftTCM $ toConApp qz []
-    let ss = take (fromInteger i) $ repeat (toConApp qs . singleton)
-    lift $ requireDef qn
-    liftTCM $ foldrM ($) z ss
+    lift do
+      requireDef qn
+      iterate (toConApp qs . singleton =<<) 
+              (toConApp qz []) 
+        !! fromInteger i
 
   l -> genericError $ "unsupported literal: " <> prettyShow l
 
-compileLitPattern :: Literal -> C LBox.Term
-compileLitPattern = \case
-
-  LitNat i -> do
-    qn <- liftTCM $ getBuiltinName_ builtinNat
-    qz <- liftTCM $ getBuiltinName_ builtinZero
-    qs <- liftTCM $ getBuiltinName_ builtinSuc
-    z  <- liftTCM $ toConApp qz []
-    let ss = take (fromInteger i) $ repeat (toConApp qs . singleton)
-    lift $ requireDef qn
-    liftTCM $ foldrM ($) z ss
-
-  l -> genericError $ "unsupported literal: " <> prettyShow l
 
 compileCaseType :: CaseType -> C LBox.Inductive
 compileCaseType = \case

src/Agda2Lambox/Compile/Type.hs

@@ -34,7 +34,7 @@ import Agda.TypeChecking.Telescope (telView)
 data VarType = TypeVar Int | Other
 
 -- | λ□ type compilation environment.
-data CompileEnv = CompileEnv
+data TypeEnv = TypeEnv
   { typeVars   :: Int
     -- ^ How many type variables we have.
   , boundVars  :: Int
@@ -47,8 +47,8 @@ data CompileEnv = CompileEnv
   }
 
 -- | Initialize compilation environment with a given number of type variables.
-initEnv :: Int -> CompileEnv
-initEnv tvs = CompileEnv
+initEnv :: Int -> TypeEnv
+initEnv tvs = TypeEnv
   { typeVars   = tvs
   , boundVars  = tvs
   , boundTypes = reverse $ TypeVar <$> [0 .. tvs - 1]
@@ -73,15 +73,15 @@ underTypeVar :: Dom Type -> C a -> C a
 underTypeVar b x = do
   shouldInsert <- asks insertVars
   if shouldInsert then
-    addContext b $ local (\e@CompileEnv{..} -> e
+    addContext b $ local (\e@TypeEnv{..} -> e
       { typeVars   = typeVars + 1
       , boundVars  = boundVars + 1
       , boundTypes = TypeVar typeVars : boundTypes
       }) x
   else underBinder b x
 
 -- | Type compilation monad.
-type C a = ReaderT CompileEnv CompileM a
+type C a = ReaderT TypeEnv CompileM a
 
 
 -- | Compile constructor arguments' types, given a set number of type variables.