actually topo sort defs

Author: flupe

src/Agda2Lambox/Compile.hs

@@ -6,13 +6,20 @@ module Agda2Lambox.Compile
 import Control.Monad.IO.Class ( liftIO )
 import Data.IORef
 
+import Control.Monad.State
+
+import Data.Bifunctor (bimap)
+import Data.Set (Set)
+import Data.Map (Map)
+import Data.Map qualified as Map
+import Data.Set qualified as Set
 import Agda.Compiler.Backend
 import Agda.Syntax.Internal ( QName )
 import Agda.Syntax.Common (Arg(..))
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.TypeChecking.Monad ( liftTCM, getConstInfo )
 import Agda.TypeChecking.Pretty
-import Agda.Utils.Monad ( whenM, ifM, unlessM, ifNotM, orM )
+import Agda.Utils.Monad ( whenM, ifM, unlessM, ifNotM, orM, forM_ )
 
 import Agda.Utils ( hasPragma, isDataOrRecDef, treeless, isArity )
 
@@ -29,12 +36,46 @@ import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), ConstantBody(..))
 import LambdaBox.Type qualified as LamBox
 
 import Agda2Lambox.Compile.Type (compileTopLevelType)
+import Data.Foldable (foldrM)
+import Agda.Utils.Maybe (catMaybes, mapMaybe, isJust)
 
 -- | Compile the given names to a λ□ environment.
 compile :: Target t -> [QName] -> TCM (GlobalEnv t)
-compile t qs = GlobalEnv <$> compileLoop (compileDefinition t) qs
+compile t qs = do
+  items <- topoSort <$> compileLoop (compileDefinition t) qs
+
+  let skipped = flip mapMaybe items \item ->
+        case itemValue item of
+          Nothing -> Nothing
+          Just x  -> Just (item { itemValue = x })
+
+  pure $ GlobalEnv $ flip map skipped \CompiledItem{..} ->
+    (qnameToKName itemName, itemValue)
+
+
+-- TODO(flupe): move this somewhere else
+type TopoM a = State (Set QName, [CompiledItem a])
+
+topoSort :: forall a. [CompiledItem a] -> [CompiledItem a]
+topoSort defs = snd $ execState (traverse (visit Set.empty) defs) (Set.empty, [])
+  where
+    items = Map.fromList $ map (\x -> (itemName x, x)) defs
+
+    isMarked :: QName -> TopoM a Bool
+    isMarked q = Set.member q <$> gets fst
+
+    push :: CompiledItem a -> TopoM a ()
+    push item@CompiledItem{itemName} = modify $ bimap (Set.insert itemName) (item:)
+
+    visit :: Set QName -> CompiledItem a -> TopoM a ()
+    visit temp item@CompiledItem{..} = do
+      unlessM ((Set.member itemName temp ||) <$> isMarked itemName) do
+        let deps = catMaybes $ (`Map.lookup` items) <$> itemDeps
+        traverse (visit (Set.insert itemName temp)) deps
+        push item
+
 
-compileDefinition :: Target t -> Definition -> CompileM (Maybe (KerName, GlobalDecl t))
+compileDefinition :: Target t -> Definition -> CompileM (Maybe (GlobalDecl t))
 compileDefinition target defn@Defn{..} = setCurrentRange defName do
   reportSDoc "agda2lambox.compile" 1 $ "Compiling definition: " <+> prettyTCM defName
 
@@ -45,8 +86,8 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
          , liftTCM $ isLogical $ Arg defArgInfo defType])
     (pure Nothing) do
 
-  -- prepend kername
-  fmap (qnameToKName defName,) <$> case theDef of
+  case theDef of
+    PrimitiveSort{}    -> pure Nothing
     GeneralizableVar{} -> pure Nothing
 
     Axiom{} -> do

src/Agda2Lambox/Compile/Monad.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DerivingVia, GeneralizedNewtypeDeriving, OverloadedStrings #-}
+{-# LANGUAGE DerivingVia, GeneralizedNewtypeDeriving, OverloadedStrings, DeriveFunctor, DeriveTraversable #-}
 -- | Compilation monad.
 module Agda2Lambox.Compile.Monad
   ( CompileM
@@ -7,6 +7,7 @@ module Agda2Lambox.Compile.Monad
   , genericError
   , genericDocError
   , internalError
+  , CompiledItem(..)
   ) where
 
 import Control.Monad ( unless )
@@ -18,7 +19,7 @@ import Queue.Ephemeral ( EphemeralQueue(..) )
 import Queue.Ephemeral qualified as Queue
 
 import Agda.Syntax.Abstract (QName)
-import Agda.Compiler.Backend (getConstInfo, PureTCM, HasConstInfo, HasBuiltins)
+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)
@@ -32,6 +33,8 @@ data CompileState = CompileState
     -- ^ Names that we have seen, either already compiled or in the queue.
   , compileQueue :: EphemeralQueue QName
     -- ^ Compilation queue.
+  , requiredDefs :: Set QName
+    -- ^ (Locally) required definitions.
   }
 
 -- NOTE(flupe):
@@ -44,6 +47,7 @@ initState :: [QName] -> CompileState
 initState qs = CompileState
   { seenDefs     = Set.fromList qs
   , compileQueue = Queue.fromList qs
+  , requiredDefs = Set.empty
   }
 
 -- | Backend compilation monad.
@@ -56,6 +60,12 @@ newtype CompileM a = Compile (StateT CompileState TCM a)
 -- | Require a definition to be compiled.
 requireDef :: QName -> CompileM ()
 requireDef q = Compile $ do
+  q <- liftTCM $ canonicalName q
+
+
+  -- add name to the required list
+  modify \ s -> s { requiredDefs = Set.insert q (requiredDefs s) }
+
   seen <- gets seenDefs
 
   -- a name is only added to the queue if we haven't seen it yet
@@ -76,15 +86,35 @@ nextUnit = Compile $
     Empty        -> pure Nothing
     Full q queue -> Just q <$ modify \s -> s { compileQueue = queue }
 
+data CompiledItem a = CompiledItem
+  { itemName  :: QName
+  , itemDeps  :: [QName]
+  , itemValue :: a
+  } deriving (Functor, Foldable, Traversable)
+
+-- | Record the required definitions of a compilation unit.
+trackDeps :: CompileM a -> CompileM (a, [QName])
+trackDeps (Compile c) = Compile do
+  modify \s -> s {requiredDefs = Set.empty}
+  x <- c
+  deps <- gets requiredDefs
+  pure (x, Set.toList deps)
+
 -- | Run the processing function as long as there are names to be compiled.
 compileLoop
-  :: (Definition -> CompileM (Maybe a)) -- ^ The compilation function
+  :: forall a. (Definition -> CompileM a) -- ^ The compilation function
   -> [QName]                            -- ^ Names to compile
-  -> TCM [a]
+  -> TCM [CompiledItem a]
 compileLoop step = evalStateT unloop . initState
   where
+  loop :: CompileM [CompiledItem a]
   loop@(Compile unloop) = nextUnit >>= \case
     Nothing -> pure []
     Just q  -> do
-      mr <- step =<< (liftTCM $ getConstInfo q)
-      mcons mr <$> loop
+      (mr, deps) <- trackDeps . step =<< (liftTCM $ getConstInfo q)
+      let item = CompiledItem 
+              { itemName  = q
+              , itemDeps  = deps
+              , itemValue = mr
+              }
+      (item:) <$> loop

src/Agda2Lambox/Compile/Term.hs

@@ -12,7 +12,7 @@ import Data.List ( elemIndex, foldl', singleton )
 import Data.Maybe ( fromMaybe, listToMaybe )
 import Data.Foldable ( foldrM )
 
-import Agda.Compiler.Backend ( MonadTCState, HasOptions )
+import Agda.Compiler.Backend ( MonadTCState, HasOptions, canonicalName )
 import Agda.Compiler.Backend ( getConstInfo, theDef, pattern Datatype, dataMutual )
 import Agda.Syntax.Abstract.Name ( ModuleName(..), QName(..) )
 import Agda.Syntax.Builtin ( builtinNat, builtinZero, builtinSuc )
@@ -99,20 +99,23 @@ compileTermC = \case
   --   - they cannot be propositions.
   --   - they cannot be types.
   TDef qn -> do
+    qn <- liftTCM $ canonicalName qn
     CompileEnv{mutuals, boundVars} <- ask
     case qn `elemIndex` mutuals of
       Nothing -> do lift $ requireDef qn
                     pure $ LConst $ qnameToKName qn
       Just i  -> pure $ LRel  $ i + boundVars
 
   TCon q -> do
+    q <- liftTCM $ canonicalName q
     lift $ requireDef q
     liftTCM $ toConApp q []
 
   -- TODO: maybe not ignore seq? (c.f. issue #12)
   TApp (TPrim PSeq) args -> compileTermC (last args)
 
   TApp (TCon q) args -> do
+    q <- liftTCM $ canonicalName q
     lift $ requireDef q
     traverse compileTermC args
       >>= liftTCM . toConApp q
@@ -175,6 +178,7 @@ compileLitPattern = \case
 compileCaseType :: CaseType -> C LBox.Inductive
 compileCaseType = \case
   CTData qn -> do
+    qn <- liftTCM $ canonicalName qn
     lift $ requireDef qn
     liftTCM $ toInductive qn
   CTNat -> do

src/Main.hs

@@ -110,7 +110,8 @@ agda2lambox = Backend backend
 moduleSetup
   :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath
   -> TCM (Recompile ModuleEnv ModuleRes)
-moduleSetup _ _ m _ = do
+moduleSetup _ NotMain m _ = pure $ Skip ()
+moduleSetup _ IsMain m _ = do
   setScope . iInsideScope =<< curIF
   pure $ Recompile ()