support one-inductive datatypes

Author: flupe

Playground.v

@@ -52,7 +52,7 @@ with odd (n : nat)  :=
     | S n => even n
   end.
 
-Definition prog  := even 2 || odd 2.
+Definition prog  := double.
 
 MetaCoq Quote Recursively Definition ex1 := prog.
 Eval vm_compute in cic_to_box ex1.

README.md

@@ -12,10 +12,14 @@ Compatible with Coq 8.20.0 and MetaCoq 1.3.2.
 - [x] Fix generation of Coq code
 - [x] Add Coq pretty-printing
 - [x] Support mutual definitions
-- [ ] Support one-inductive
+- [x] Support one-inductive
 - [ ] Support mutual inductives
 - [ ] Better error-reporting
 - [ ] "Support" modules
+- [ ] Check support for Agda-specific edge cases
+  - [ ] Pattern-matching lambdas
+  - [ ] With-generated lambdas
+  - [ ] Module applications
 - [ ] Support literals (ints and floats)
 - [ ] Setup compilation to WASM/RUST
 - [ ] Setup proper testing infrastructure

agda2lambox.cabal

@@ -15,14 +15,15 @@ source-repository head
 executable agda2lambox
   hs-source-dirs:      src
   main-is:             Main.hs
-  other-modules:       Agda.Lib,
+  other-modules:       Agda,
+                       Agda.Lib,
                        Agda.Utils,
-                       Agda,
                        Agda2Lambox.Monad,
                        Agda2Lambox.Convert,
                        Agda2Lambox.Convert.Class,
-                       Agda2Lambox.Convert.Term,
+                       Agda2Lambox.Convert.Data,
                        Agda2Lambox.Convert.Function,
+                       Agda2Lambox.Convert.Term,
                        Agda2Lambox,
                        Utils,
                        LambdaBox,
@@ -33,8 +34,8 @@ executable agda2lambox
                        Agda >= 2.7 && <= 2.8,
                        deepseq >= 1.4.4 && < 1.6,
                        pretty-show,
-                       filepath,
                        directory,
+                       filepath,
                        mtl
   default-language:    Haskell2010
   default-extensions:

src/Agda2Lambox/Convert/Data.hs

@@ -0,0 +1,67 @@
+{-# LANGUAGE NamedFieldPuns #-}
+-- | Convert Agda datatypes to λ□ inductive declarations
+module Agda2Lambox.Convert.Data
+  ( convertDatatype
+  ) where
+
+import Control.Monad.Reader ( ask, liftIO )
+import Control.Monad ( forM )
+import Data.List ( elemIndex )
+
+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.Common.Pretty ( prettyShow )
+
+import LambdaBox
+
+import Agda2Lambox.Monad
+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} =
+  withCurrentModule (qnameModule defName) do
+    let Datatype{..} = theDef
+
+    ctors :: [ConstructorBody]
+      <- forM dataCons \cname -> do
+           DataCon arity <- getConstructorInfo cname
+           return Ctor
+             { ctorName = prettyShow $ qnameName cname
+             , 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   = dataPars
+          -- TODO(flupe):
+          --   ^ double-check, but I don't think we'll ever share parameters.
+          --     unless, perhaps, when defined inside a parametrized module (?).
+      , indBodies = [inductive]
+      }

src/Agda2Lambox/Convert/Function.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE NamedFieldPuns #-}
+-- | Convert Agda functions to λ□ constant declarations
 module Agda2Lambox.Convert.Function 
   ( convertFunction
   ) where
@@ -39,28 +40,30 @@ convertFunctionBody Defn{defName} =
     Just t <- liftTCM $ toTreeless EagerEvaluation defName
     convert t
 
--- | Convert a function to a Lambdabox term.
-convertFunction :: Definition :~> Term
+-- | Convert a function definition to a λ□ declaration.
+convertFunction :: Definition :~> GlobalDecl
 convertFunction defn@Defn{defName, theDef} =
   withCurrentModule (qnameModule defName) do
     let Function{funMutual = Just ms} = theDef
 
-    if null ms then convertFunctionBody defn
+    if null ms then 
+      ConstantDecl . Just <$> convertFunctionBody defn
     else do
       mdefs :: [Definition] <- mapM getConstInfo ms
 
-      if (any (not . isFunction) mdefs) then
+      if any (not . isFunction) mdefs then
         fail "Induction-recursion and other weird mutual defs not supported."
       else inMutuals ms do
-        -- NOTE(flupe): 
+        -- NOTE(flupe):
         --   maybe reverse ms here?
         --   it's unclear in which order mutual fixpoints are added to the local context
         let Just k = elemIndex defName ms
 
-        flip LFix k <$> forM mdefs \def@Defn{defName} -> do
-          body <- convertFunctionBody def
-          return Def
-            { dName = Named $ prettyShow defName
-            , dBody = body
-            , dArgs = 0 -- TODO(flupe): when is this ever not zero?
-            }
+        ConstantDecl . Just . flip LFix k <$>
+          forM mdefs \def@Defn{defName} -> do
+            body <- convertFunctionBody def
+            return Def
+              { dName = Named $ prettyShow defName
+              , dBody = body
+              , dArgs = 0 -- TODO(flupe): when is this ever not zero?
+              }

src/CoqGen.hs

@@ -41,6 +41,9 @@ instance {-# OVERLAPPING #-} Pretty (ToCoq String) where
 instance Pretty (ToCoq Int) where
   pretty = pretty . unwrap
 
+instance Pretty (ToCoq Bool) where
+  pretty (ToCoq v) = if v then "true" else "false"
+
 instance Pretty (ToCoq a) => Pretty (ToCoq (Maybe a)) where
   pretty (ToCoq x) =
     case x of
@@ -89,13 +92,55 @@ instance Pretty (ToCoq ModPath) where
 instance Pretty (ToCoq KerName) where
   pretty (ToCoq KerName{..}) = pcoq (kerModPath, kerName)
 
+instance Pretty (ToCoq RecursivityKind) where
+  pretty (ToCoq rk) =
+    case rk of
+      Finite   -> ctor "Finite"   []
+      CoFinite -> ctor "CoFinite" []
+      BiFinite -> ctor "BiFinite" []
+
+instance Pretty (ToCoq AllowedElims) where
+  pretty (ToCoq ae) =
+    case ae of
+      IntoSProp        -> ctor "IntoSProp"        []
+      IntoPropSProp    -> ctor "IntoPropSProp"    []
+      IntoSetPropSProp -> ctor "IntoSetPropSProp" []
+      IntoAny          -> ctor "IntoAny"          []
+
+instance Pretty (ToCoq ConstructorBody) where
+  pretty (ToCoq Ctor{..}) =
+    record [ ("cstr_name",  pcoq ctorName)
+           , ("cstr_nargs", pcoq ctorArgs)
+           ]
+
+instance Pretty (ToCoq ProjectionBody) where
+  pretty (ToCoq Proj{..}) =
+    record [ ("proj_name",  pcoq projName)
+           ]
+
+instance Pretty (ToCoq OneInductiveBody) where
+  pretty (ToCoq OneInductive{..}) =
+    record [ ("ind_name",          pcoq indName)
+           , ("ind_propositional", pcoq indPropositional)
+           , ("ind_kelim",         pcoq indKElim)
+           , ("ind_ctors",         pcoq indCtors)
+           , ("ind_projs",         pcoq indProjs)
+           ]
+
+instance Pretty (ToCoq MutualInductiveBody) where
+  pretty (ToCoq MutualInductive{..}) =
+    record [ ("ind_finite", pcoq indFinite)
+           , ("ind_npars",  pcoq indPars)
+           , ("ind_bodies", pcoq indBodies)
+           ]
+
 instance Pretty (ToCoq GlobalDecl) where
   pretty (ToCoq decl) =
     case decl of
       ConstantDecl  body  ->
         ctor "ConstantDecl" [record [("cst_body", pcoq body)]]
       InductiveDecl minds ->
-        ctor "InductiveDecl" []
+        ctor "InductiveDecl" [pcoq minds]
 
 instance Pretty (ToCoq t) => Pretty (ToCoq (Def t)) where
   pretty (ToCoq Def{..}) =

src/LambdaBox.hs

@@ -149,14 +149,13 @@ data AllowedElims
   | IntoAny
   deriving (Eq, Show)
 
-data ConstructorBody = Ctor 
+data ConstructorBody = Ctor
   { ctorName :: Ident
   , ctorArgs :: Int
   } deriving (Eq, Show)
 
 data ProjectionBody = Proj
   { projName :: Ident
-  , projArgs :: Int
   } deriving (Eq, Show)
 
 -- | Inductive datatype declaration body
@@ -168,17 +167,24 @@ data OneInductiveBody = OneInductive
   , indProjs         :: [ProjectionBody]
   } deriving (Eq, Show)
 
+data RecursivityKind
+  = Finite   -- ^ Inductive datatype.
+  | CoFinite -- ^ Coinductive datatype.
+  | BiFinite -- ^ Non-recursive.
+  deriving (Eq, Show)
+
 -- | Declaration of mutually defined inductive types
 data MutualInductiveBody = MutualInductive
-  { indPars   :: Int
+  { indFinite :: RecursivityKind
+  , indPars   :: Int
   , indBodies :: [OneInductiveBody]
   } deriving (Eq, Show)
 
 -- | Definition of a constant in the environment
 type ConstantBody = Maybe Term
 
 -- | Global declarations.
-data GlobalDecl 
+data GlobalDecl
   = ConstantDecl ConstantBody
   | InductiveDecl MutualInductiveBody
   deriving (Eq, Show)

src/Main.hs

@@ -5,7 +5,7 @@ module Main where
 import Control.Monad ( unless )
 import Control.Monad.IO.Class ( MonadIO(liftIO) )
 import Control.DeepSeq ( NFData(..) )
-import Data.Maybe ( fromMaybe, catMaybes, isJust )
+import Data.Maybe ( fromMaybe, catMaybes, isJust, isNothing )
 import Data.Version ( showVersion )
 import GHC.Generics ( Generic )
 import System.Console.GetOpt ( OptDescr(Option), ArgDescr(ReqArg) )
@@ -21,9 +21,11 @@ import LambdaBox
 import qualified LambdaBox as L
 import Agda2Lambox.Convert ( convert )
 import Agda2Lambox.Convert.Function ( convertFunction )
+import Agda2Lambox.Convert.Data     ( convertDatatype )
 import Agda2Lambox.Monad ( runC0, inMutuals )
 import CoqGen ( ToCoq(ToCoq) )
 import Agda.Syntax.Common.Pretty ( (<?>), pretty )
+import Agda.Syntax.Common (hasQuantityω)
 
 
 main :: IO ()
@@ -90,30 +92,28 @@ moduleSetup _ _ m _ = do
   setScope . iInsideScope =<< curIF
   return $ Recompile ()
 
--- | Which Agda definitions to ignore.
-ignoreDef :: Definition -> Bool
-ignoreDef d@Defn{..}
-  | hasQuantity0 d
-  = True
-  | Function {..} <- theDef
-  = (theDef ^. funInline) -- inlined functions (from module application)
-  -- || funErasure           -- @0 functions
-  || isJust funExtLam     -- pattern-lambdas
-  || isJust funWith       -- with-generated
-  | otherwise
-  = True
-
 compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM (Maybe (KerName, GlobalDecl))
-compile _ _ _ defn | ignoreDef defn = return Nothing
-compile opts tlm _ def@Defn{..} = do
-  body <- runC0 $ convertFunction def
-  return $ Just $ ( qnameToKerName defName
-                  , ConstantDecl $ Just body)
+compile opts tlm _ 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
+        -> Just <$> runC0 (convertFunction def)
+
+      Datatype{} -> Just <$> runC0 (convertDatatype def)
+
+      _          -> Nothing <$ (liftIO $ putStrLn $ "Skipping " <> prettyShow defName)
+
 
 writeModule :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName
             -> [Maybe (KerName, GlobalDecl)]
             -> TCM ModuleRes
-writeModule opts _ _ m (catMaybes -> cdefs) = do
+writeModule opts _ _ m (reverse . catMaybes -> cdefs) = do
   compDir <- compileDir
 
   let outDir   = fromMaybe compDir (optOutDir opts)
@@ -134,7 +134,7 @@ writeModule opts _ _ m (catMaybes -> cdefs) = do
   where
   coqModuleTemplate :: [(KerName, GlobalDecl)] -> String
   coqModuleTemplate coqterms = unlines
-    [ "From MetaCoq.Common Require Import BasicAst Kernames."
+    [ "From MetaCoq.Common Require Import BasicAst Kernames Universes."
     , "From MetaCoq.Erasure Require Import EAst."
     , "From MetaCoq.Utils Require Import bytestring MCString."
     , "From Coq Require Import List."

test/OddEven.agda

@@ -4,6 +4,10 @@ data Nat : Set where
   zero : Nat
   succ : Nat -> Nat
 
+double : Nat -> Nat
+double zero = zero
+double (succ n) = succ (succ (double n))
+
 odd even : Nat -> Bool
 
 odd zero = false