backup

Author: flupe

README.md

@@ -31,6 +31,10 @@ cabal run agda2lambox -- --out-dir build -itest test/Nat.agda
 - [x] Evaluate λ□ programs from inside Coq to start testing
   - [x] Using the λ□-Mut from CertiCoq
 - [ ] Support mutual inductives
+- [ ] Refactor backend
+  - Get rid of the Convert class.
+  - Possibly put everything in a single module.
+  - Unify compilation of records and datatypes.
 - [x] Support (one-inductive) records
   - [x] Properly translate projections in terms (by actually generating projections)
 - [ ] Support mutual (possibly inductive) records

agda2lambox.cabal

@@ -31,9 +31,10 @@ executable agda2lambox
                        CoqGen,
                        Paths_agda2lambox
   autogen-modules:     Paths_agda2lambox
-  build-depends:       base >= 4.10 && < 4.22,
-                       Agda >= 2.7 && <= 2.8,
-                       deepseq >= 1.4.4 && < 1.6,
+  build-depends:       base       >= 4.10  && < 4.22,
+                       Agda       >= 2.7   && <= 2.8,
+                       deepseq    >= 1.4.4 && < 1.6,
+                       containers >= 0.7   && < 0.8,
                        pretty-show,
                        directory,
                        filepath,

src/Agda2Lambox/Convert/Data.hs

@@ -1,11 +1,13 @@
-{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NamedFieldPuns, ImportQualifiedPost #-}
 -- | Convert Agda datatypes to λ□ inductive declarations
 module Agda2Lambox.Convert.Data
   ( convertDatatype
   ) where
 
 import Control.Monad.Reader ( ask, liftIO )
-import Control.Monad ( forM, when, unless )
+import Control.Monad ( forM, when, unless, (>=>) )
+import Data.Traversable ( mapM )
+import Data.Foldable ( toList )
 import Data.List ( elemIndex )
 import Data.Maybe ( isJust )
 
@@ -17,9 +19,9 @@ 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.TypeChecking.Datatypes ( ConstructorInfo(..), getConstructorInfo, isDatatype )
 import Agda.Compiler.ToTreeless ( toTreeless )
-import Agda.Compiler.Backend ( getConstInfo )
+import Agda.Compiler.Backend ( getConstInfo, lookupMutualBlock )
 import Agda.Syntax.Treeless ( EvaluationStrategy(EagerEvaluation) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
@@ -30,16 +32,46 @@ import Agda2Lambox.Convert.Class
 import Agda.Utils.Monad (guardWithError)
 
 
--- | Convert a datatype definition to a Lambdabox declaration.
-convertDatatype :: Definition :~> GlobalDecl
-convertDatatype defn@Defn{defName, theDef, defMutual} =
-  withCurrentModule (qnameModule defName) do
-    let Datatype{..} = theDef
+-- | Toplevel conversion from a datatype definition to a Lambdabox declaration.
+convertDatatype :: Definition :~> Maybe GlobalDecl
+convertDatatype defn@Defn{defName, defMutual} = do
+  -- we lookup names in the mutual block
+  MutualBlock{mutualNames} <- lookupMutualBlock defMutual
+
+  let names = toList mutualNames
+
+  -- 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 defName /= head names then return Nothing
+  else do
+
+    -- when it's time to compile the mutual block
+    -- we make sure that all definitions in the block are datatypes (for now)
+
+    onlyDatas :: Bool <- and <$> mapM (liftTCM . isDatatype) names
+
+    unless onlyDatas $ fail "not supported: mutual datatypes with non-datatypes"
+
+    bodies <- forM names $ liftTCM . getConstInfo >=> actuallyConvertDatatype
+
+    return $ Just $ InductiveDecl $ MutualInductive
+      { indFinite = 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.
+          -- in anycase, once we also accept coinductive records in the mix, probably we should pick CoFinite
+      , indPars   = 0
+      , indBodies = bodies
+      }
 
-    let Just muts = dataMutual
 
-    unless (length muts < 2) $
-      fail $ "mututal datatypes not supported" <> prettyShow dataMutual
+
+actuallyConvertDatatype :: Definition :~> OneInductiveBody
+actuallyConvertDatatype defn@Defn{defName, theDef, defMutual} =
+  withCurrentModule (qnameModule defName) do
+    let Datatype{..} = theDef
 
     ctors :: [ConstructorBody]
       <- forM dataCons \cname -> do
@@ -49,22 +81,14 @@ convertDatatype defn@Defn{defName, theDef, defMutual} =
              , ctorArgs = arity
              }
 
-    let
-      inductive = OneInductive
-        { indName          = prettyShow $ qnameName defName
-        , indPropositional = False
-            -- TODO(flupe): ^ take care of this (use datatypeSort to figure this out)
-        , indKElim         = IntoAny
-            -- TODO(flupe): also take care of this (with the Sort)
-        , indCtors         = ctors
-        , indProjs         = []
-        }
-
-    return $ InductiveDecl $ MutualInductive
-      { indFinite = 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.
-      , indPars   = 0
-      , indBodies = [inductive]
+    return OneInductive
+      { indName          = prettyShow $ qnameName defName
+      , indPropositional = False
+          -- TODO(flupe): ^ take care of this (use datatypeSort to figure this out)
+      , indKElim         = IntoAny
+          -- TODO(flupe): also take care of this (with the Sort)
+      , indCtors         = ctors
+      , indProjs         = []
       }
+
+

src/Agda2Lambox/Convert/Function.hs

@@ -57,7 +57,7 @@ convertFunction defn@Defn{defName, theDef} =
   withCurrentModule (qnameModule defName) do
     let Function{funMutual = Just ms} = theDef
 
-    if null ms then 
+    if length ms < 2 then 
       Just. ConstantDecl . Just <$> convertFunctionBody defn
     else do
       mdefs :: [Definition] <- mapM getConstInfo ms

src/Main.hs

@@ -90,7 +90,7 @@ compile opts menv _ def@Defn{..} =
 
           runC0 (convertFunction def)
 
-      Datatype{} -> Just <$> runC0 (convertDatatype def)
+      Datatype{} -> runC0 (convertDatatype def)
 
       Record{}   -> Just <$> runC0 (convertRecord def)