basic record support

Author: flupe

agda2lambox.cabal

@@ -23,6 +23,7 @@ executable agda2lambox
                        Agda2Lambox.Convert.Class,
                        Agda2Lambox.Convert.Data,
                        Agda2Lambox.Convert.Function,
+                       Agda2Lambox.Convert.Record,
                        Agda2Lambox.Convert.Term,
                        Agda2Lambox,
                        Utils,

src/Agda2Lambox/Convert/Function.hs

@@ -7,11 +7,12 @@ module Agda2Lambox.Convert.Function
 import Control.Monad.Reader ( ask, liftIO )
 import Control.Monad ( forM )
 import Data.List ( elemIndex )
+import Data.Maybe ( isNothing, isJust )
 
 import Utils
 
 import Agda ( liftTCM )
-import Agda.Lib ()
+import Agda.Lib ( (^.), funInline )
 import Agda.Utils
 import Agda.Syntax.Abstract.Name ( qnameModule )
 import Agda.TypeChecking.Monad.Base
@@ -20,6 +21,7 @@ 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 LambdaBox
 
@@ -40,14 +42,29 @@ convertFunctionBody Defn{defName} =
     Just t <- liftTCM $ toTreeless EagerEvaluation defName
     convert t
 
+-- | Whether a function is a (true) record projection.
+isProjection :: Either ProjectionLikenessMissing Projection -> Bool
+isProjection (Left _) = False
+isProjection (Right Projection{projProper}) = isJust projProper
+
+-- | 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): ?
+    && not (isProjection funProjection) -- not a record projection
+    && hasQuantityω def                 -- non-erased
+
 -- | Convert a function definition to a λ□ declaration.
-convertFunction :: Definition :~> GlobalDecl
+convertFunction :: Definition :~> Maybe GlobalDecl
+convertFunction defn | not (shouldCompileFunction defn) = return Nothing
 convertFunction defn@Defn{defName, theDef} =
   withCurrentModule (qnameModule defName) do
     let Function{funMutual = Just ms} = theDef
 
     if null ms then 
-      ConstantDecl . Just <$> convertFunctionBody defn
+      Just. ConstantDecl . Just <$> convertFunctionBody defn
     else do
       mdefs :: [Definition] <- mapM getConstInfo ms
 
@@ -59,7 +76,7 @@ convertFunction defn@Defn{defName, theDef} =
         --   it's unclear in which order mutual fixpoints are added to the local context
         let Just k = elemIndex defName ms
 
-        ConstantDecl . Just . flip LFix k <$>
+        Just . ConstantDecl . Just . flip LFix k <$>
           forM mdefs \def@Defn{defName} -> do
             body <- convertFunctionBody def
             return Def

src/Agda2Lambox/Convert/Record.hs

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

src/LambdaBox.hs

@@ -23,11 +23,9 @@ data Inductive = Inductive
       -- ^ Which of those is the inductive we care about.
   } deriving (Eq, Show)
 
-
 data Name = Anon | Named Ident
   deriving (Eq, Show)
 
-
 type DirPath = [Ident]
 
 -- | The module part of the kernel name

src/Main.hs

@@ -17,12 +17,12 @@ import Paths_agda2lambox ( version )
 
 import Agda.Lib hiding ( (<?>), pretty )
 import Agda.Syntax.Common.Pretty ( (<?>), pretty )
-import Agda.Syntax.Common ( hasQuantityω )
 import Agda.Utils ( pp, unqual, hasPragma )
 
 import Agda2Lambox.Convert ( convert )
 import Agda2Lambox.Convert.Function ( convertFunction )
 import Agda2Lambox.Convert.Data     ( convertDatatype )
+import Agda2Lambox.Convert.Record   ( convertRecord   )
 import Agda2Lambox.Monad ( runC0, inMutuals )
 import CoqGen ( ToCoq(ToCoq), CoqModule(..) )
 import LambdaBox ( KerName, GlobalDecl, qnameToKerName )
@@ -82,22 +82,18 @@ compile opts menv _ def@Defn{..} =
   fmap (qnameToKerName defName,) <$> -- prepend kername
     case theDef of
 
-      -- TODO(flupe): offload the check to Convert.Function
-      Function{..}
-        | 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
-        -> do
+      Function{} -> do
           -- if the function is annotated with a COMPILE pragma
           -- then it is added to the list of programs to run
           whenM (hasPragma defName) $ 
             liftIO $ modifyIORef' (modProgs menv) (qnameToKerName defName:)
 
-          Just <$> runC0 (convertFunction def)
+          runC0 (convertFunction def)
 
       Datatype{} -> Just <$> runC0 (convertDatatype def)
 
+      Record{}   -> Just <$> runC0 (convertRecord def)
+
       _          -> Nothing <$ (liftIO $ putStrLn $ "Skipping " <> prettyShow defName)
 
 

test/OddEven.agda

@@ -26,3 +26,9 @@ even (succ n) = odd n
 test : Bool
 test = odd (succ (succ zero))
 {-# COMPILE AGDA2LAMBOX test #-}
+
+record Pair (A : Set) (B : Set) : Set where
+  constructor _,_
+  field
+    fst : A
+    snd : B