almost done with cleaning up

Author: flupe

agda2lambox.cabal

@@ -18,15 +18,12 @@ executable agda2lambox
   other-modules:       Agda,
                        Agda.Lib,
                        Agda.Utils,
-                       Agda2Lambox.Monad,
-                       Agda2Lambox.Convert,
-                       Agda2Lambox.Convert.Class,
-                       Agda2Lambox.Convert.Data,
-                       Agda2Lambox.Convert.Function,
-                       Agda2Lambox.Convert.Record,
-                       Agda2Lambox.Convert.Term,
-                       Agda2Lambox,
-                       Utils,
+                       Agda2Lambox.Compile.Utils,
+                       Agda2Lambox.Compile.Term,
+                       Agda2Lambox.Compile.Function,
+                       Agda2Lambox.Compile.Data,
+                       Agda2Lambox.Compile.Record,
+                       Agda2Lambox.Compile,
                        LambdaBox,
                        CoqGen,
                        Paths_agda2lambox
@@ -46,3 +43,4 @@ executable agda2lambox
     TypeFamilies TypeOperators TypeApplications
     FunctionalDependencies TypeSynonymInstances ConstraintKinds
     DoAndIfThenElse BlockArguments MultiWayIf
+    ImportQualifiedPost

src/Agda/Utils.hs

@@ -4,7 +4,7 @@
 module Agda.Utils where
 
 import Control.Monad.Error.Class ( MonadError )
-import Control.Monad.IO.Class ( MonadIO )
+import Control.Monad.IO.Class ( MonadIO(liftIO) )
 import Control.Monad ( filterM )
 import Control.Arrow ( first )
 
@@ -13,7 +13,6 @@ import qualified Data.List.NonEmpty as NE ( fromList )
 import Data.Maybe ( isJust, isNothing )
 import Data.Bifunctor ( second )
 
-import Utils
 import Agda.Lib
 import Agda.TypeChecking.Free.Lazy (underBinder)
 import Agda.TypeChecking.Datatypes (getConstructorInfo, ConstructorInfo(..))
@@ -54,7 +53,7 @@ currentCtx = fmap (first pp . unDom) <$> getContext
 reportCurrentCtx :: (MonadIO m, MonadTCEnv m) => m ()
 reportCurrentCtx = do
   ctx <- currentCtx
-  report $ " currentCtx: " <> pp ctx
+  liftIO $ putStrLn $ " currentCtx: " <> pp ctx
 
 unqual :: QName -> String
 unqual = pp . last . qnameToList0

src/Agda2Lambox.hs

@@ -0,0 +1 @@
+module Agda2Lambox.Compile where

src/Agda2Lambox/Compile.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE NamedFieldPuns, ImportQualifiedPost #-}
 -- | Convert Agda datatypes to λ□ inductive declarations
-module Agda2Lambox.Convert.Data
-  ( convertDatatype
+module Agda2Lambox.Compile.Data
+  ( compileData
   ) where
 
 import Control.Monad.Reader ( ask, liftIO )
@@ -11,11 +11,7 @@ import Data.Foldable ( toList )
 import Data.List ( elemIndex )
 import Data.Maybe ( isJust, listToMaybe )
 
-import Utils
-
 import Agda ( liftTCM )
-import Agda.Lib ()
-import Agda.Utils
 import Agda.Syntax.Abstract.Name ( qnameModule, qnameName )
 import Agda.TypeChecking.Monad.Base
 import Agda.TypeChecking.Monad.Env ( withCurrentModule )
@@ -25,24 +21,24 @@ import Agda.Compiler.Backend ( getConstInfo, lookupMutualBlock )
 import Agda.Syntax.Treeless ( EvaluationStrategy(EagerEvaluation) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
-import LambdaBox
-
-import Agda2Lambox.Monad
-import Agda2Lambox.Convert.Class
-import Agda.Utils.Monad (guardWithError)
+import Agda2Lambox.Compile.Utils
+import LambdaBox qualified as LBox
 
 
 -- | Toplevel conversion from a datatype definition to a Lambdabox declaration.
-convertDatatype :: Definition :~> Maybe GlobalDecl
-convertDatatype defn@Defn{defName, defMutual} = do
+compileData :: Definition -> TCM (Maybe LBox.GlobalDecl)
+compileData defn@Defn{defName, defMutual} = do
   let Datatype{..} = theDef defn
-  let Just names = dataMutual
+  let names = case dataMutual of
+        Just [] -> [defName]
+        Just xs -> xs
+        Nothing -> fail "error"
 
   -- we consider that the *lowest name* in the mutual block
   -- is the *representative* of the mutual block
   -- i.e that's when we trigger the compilation of the mutual block
 
-  if not (null names) && Just defName /= listToMaybe names then return Nothing
+  if Just defName /= listToMaybe names then return Nothing
   else do
 
     -- when it's time to compile the mutual block
@@ -52,10 +48,10 @@ convertDatatype defn@Defn{defName, defMutual} = do
 
     unless onlyDatas $ fail "not supported: mutual datatypes with non-datatypes"
 
-    bodies <- forM names $ liftTCM . getConstInfo >=> actuallyConvertDatatype
+    bodies <- forM names $ getConstInfo >=> actuallyConvertDatatype
 
-    return $ Just $ InductiveDecl $ MutualInductive
-      { indFinite = Finite
+    return $ Just $ LBox.InductiveDecl $ LBox.MutualInductive
+      { indFinite = LBox.Finite
           -- NOTE(flupe): Agda's datatypes are *always* finite?
           -- Co-induction is restricted to records.
           -- We may want to set BiFinite for non-recursive datatypes, but I don't know yet.
@@ -66,24 +62,23 @@ convertDatatype defn@Defn{defName, defMutual} = do
 
 
 
-actuallyConvertDatatype :: Definition :~> OneInductiveBody
-actuallyConvertDatatype defn@Defn{defName, theDef, defMutual} =
-  withCurrentModule (qnameModule defName) do
+actuallyConvertDatatype :: Definition -> TCM LBox.OneInductiveBody
+actuallyConvertDatatype defn@Defn{defName, theDef, defMutual} = do
     let Datatype{..} = theDef
 
-    ctors :: [ConstructorBody]
+    ctors :: [LBox.ConstructorBody]
       <- forM dataCons \cname -> do
            DataCon arity <- getConstructorInfo cname
-           return Ctor
+           return LBox.Ctor
              { ctorName = prettyShow $ qnameName cname
              , ctorArgs = arity
              }
 
-    return OneInductive
+    return LBox.OneInductive
       { indName          = prettyShow $ qnameName defName
       , indPropositional = False
           -- TODO(flupe): ^ take care of this (use datatypeSort to figure this out)
-      , indKElim         = IntoAny
+      , indKElim         = LBox.IntoAny
           -- TODO(flupe): also take care of this (with the Sort)
       , indCtors         = ctors
       , indProjs         = []

src/Agda2Lambox/Convert/Data.hs src/Agda2Lambox/Compile/Data.hssrc/Agda2Lambox/Convert/Data.hs renamed to src/Agda2Lambox/Compile/Data.hs

@@ -0,0 +1,74 @@
+{-# LANGUAGE NamedFieldPuns #-}
+-- | Convert Agda functions to λ□ constant declarations
+module Agda2Lambox.Compile.Function 
+  ( compileFunction
+  ) where
+
+import Control.Monad ( forM, when )
+import Data.List ( elemIndex )
+import Data.Maybe ( isNothing, fromMaybe )
+
+import Agda.Lib ( (^.), funInline )
+import Agda.Syntax.Abstract.Name ( QName, qnameModule )
+import Agda.TypeChecking.Monad.Base
+import Agda.Compiler.ToTreeless ( toTreeless )
+import Agda.Compiler.Backend ( getConstInfo )
+import Agda.Syntax.Treeless ( EvaluationStrategy(EagerEvaluation) )
+import Agda.Syntax.Common.Pretty ( prettyShow )
+import Agda.Syntax.Common ( hasQuantityω )
+import Agda.Utils.Monad (guardWithError)
+
+import Agda.Utils ( etaExpandCtor )
+import Agda2Lambox.Compile.Utils
+import Agda2Lambox.Compile.Term ( runC, compileTerm, withMutuals )
+import LambdaBox qualified as LBox
+
+
+-- | Check whether a definition is a function.
+isFunction :: Definition -> Bool
+isFunction Defn{..} | Function{} <- theDef = True
+isFunction _ = False
+
+
+-- | Convert a function body to a Lambdabox term.
+compileFunctionBody :: [QName] -> Definition -> TCM LBox.Term
+compileFunctionBody fixpoints Defn{defName} = do
+    Just t <-toTreeless EagerEvaluation defName
+    runC . withMutuals fixpoints . compileTerm =<< etaExpandCtor t
+
+
+-- | Whether to compile a function definition to λ□.
+shouldCompileFunction :: Definition -> Bool
+shouldCompileFunction def@Defn{theDef} | Function{..} <- theDef
+  = not (theDef ^. funInline) -- not inlined (from module application)
+    && isNothing funExtLam    -- not a pattern-lambda-generated function   NOTE(flupe): ?
+    && isNothing funWith      -- not a with-generated function             NOTE(flupe): ?
+    && hasQuantityω def       -- non-erased
+
+
+-- | Convert a function definition to a λ□ declaration.
+compileFunction :: Definition -> TCM (Maybe LBox.GlobalDecl)
+compileFunction defn | not (shouldCompileFunction defn) = return Nothing
+compileFunction defn@Defn{defName, theDef} = do
+    let Function{funMutual = Just ms} = theDef
+
+    -- if the function is at most recursive with itself, just compile body
+    if null ms then
+      Just. LBox.ConstantDecl . Just <$> compileFunctionBody [] defn
+
+    -- otherwise, take fixpoint
+    else do
+      mdefs :: [Definition] <- mapM getConstInfo ms
+
+      when (any (not . isFunction) mdefs) $ fail "only mutually defined functions are supported."
+
+      let k = fromMaybe 0 $ elemIndex defName ms
+
+      Just . LBox.ConstantDecl . Just . flip LBox.LFix k <$>
+        forM mdefs \def@Defn{defName} -> do
+          body <- compileFunctionBody ms def
+          return LBox.Def
+            { dName = LBox.Named $ prettyShow defName
+            , dBody = body
+            , dArgs = 0
+            }

src/Agda2Lambox/Compile/Function.hs

@@ -0,0 +1,54 @@
+{-# LANGUAGE NamedFieldPuns #-}
+-- | Convert Agda records to λ□ inductive declarations
+module Agda2Lambox.Compile.Record
+  ( compileRecord
+  ) where
+
+import Control.Monad ( forM )
+import Control.Monad.Reader ( ask, liftIO )
+import Data.List ( elemIndex )
+import Data.Maybe ( maybe )
+
+import Agda.Syntax.Abstract.Name ( qnameModule, qnameName )
+import Agda.TypeChecking.Monad.Base
+import Agda.TypeChecking.Datatypes ( ConstructorInfo(..), getConstructorInfo )
+import Agda.Syntax.Internal ( ConHead(..), unDom )
+import Agda.Syntax.Common.Pretty ( prettyShow )
+import Agda.Syntax.Common ( Induction(..) )
+
+import Agda2Lambox.Compile.Utils
+import LambdaBox qualified as LBox
+
+inductionToRecKind :: Induction -> LBox.RecursivityKind
+inductionToRecKind = \case
+  Inductive   -> LBox.Finite
+  CoInductive -> LBox.CoFinite
+
+-- | Convert a datatype definition to a Lambdabox declaration.
+compileRecord :: Definition -> TCM LBox.GlobalDecl
+compileRecord defn@Defn{defName, theDef} =
+  let
+
+    Record{..} = theDef
+    ConHead{conName, conFields} = recConHead
+
+    fields :: [LBox.ProjectionBody]
+      = LBox.Proj . prettyShow . qnameName . unDom <$> recFields
+
+    record = LBox.OneInductive
+      { indName          = prettyShow $ qnameName defName
+      , indPropositional = False        -- TODO(flupe): take care of this
+      , indKElim         = LBox.IntoAny -- TODO(flupe): also take care of this
+      , indCtors         = [ LBox.Ctor (prettyShow $ qnameName conName) 
+                                  (length conFields) ]
+      , indProjs         = fields
+      }
+
+  in return $ LBox.InductiveDecl LBox.MutualInductive
+    { indFinite = maybe LBox.BiFinite inductionToRecKind recInduction
+    , indPars   = 0
+        -- TODO(flupe):
+        --   ^ double-check, but it doesn't look like 
+        --     this could be anything other than 0.
+    , indBodies = [record]
+    }