fix zero pattern, more work on types

Author: flupe

NOTES.md

@@ -120,7 +120,25 @@ All the remaining transformations optimize this program, but remain in λ□*.
     Rebuild the efficient lookup table.
 12. `constructors_as_blocks_transformation`:
     Eta-expand and fully apply constructors.
-    
+
     This is currently implemented on our side in the backend,
     but it makes way more sense to do it on the Coq side.
     Let's use this transformation!
+
+---
+
+- Actually, now that I get a better understanding of typed λ□ environments, it looks like
+  generation of the type information never fails.
+  Worst case, it's always `TBox`, but we try to generate as much valid types as we can.
+
+---
+
+- Type erasure is defined in this paper, from ConCert: https://arxiv.org/pdf/2108.02995
+  I should just look at what they describe.
+  I think I need something like:
+
+  ```hs
+  compileTopLevelType :: Type -> C ([TypeVarInfo], LamBox.Type)
+  
+  compileType :: Type -> C (LamBox.Type)
+  ```

README.md

@@ -42,6 +42,7 @@ cabal run agda2lambox -- --out-dir build -itest test/Nat.agda
   - [x] With-generated lambdas
   - [ ] Module applications
   - [ ] Projection-like
+  - [ ] Check that treeless generates exhaustive cases
 - [ ] Support primitives (ints and floats)
 
 - [ ] Setup compilation to Wasm/Rust using Certicoq
@@ -62,8 +63,8 @@ Things that ought to be implemented, but not right now.
 - [Verified Extraction from Coq to OCaml](https://github.com/yforster/coq-verified-extraction/)
   and its [accompanying paper](https://dl.acm.org/doi/10.1145/3656379)
 - [Certified Erasure for Coq, in Coq](https://inria.hal.science/hal-04077552)
-- [Syntax of LambdaBox in MetaCoq](https://github.com/MetaCoq/metacoq/blob/coq-8.20/erasure/theories/Typed/ExAst.v) 
-- [Erasure of types in MetaCoq](https://github.com/MetaCoq/metacoq/blob/coq-8.20/erasure/theories/Typed/Erasure.v#L765)
+- [Extracting functional programs from Coq, in Coq](https://arxiv.org/pdf/2108.02995)
+- [Lambdabox syntax and untyped environments](https://github.com/MetaCoq/metacoq/blob/coq-8.20/erasure/theories/EAst.v) 
+- [Lambdabox typed environments](https://github.com/MetaCoq/metacoq/blob/coq-8.20/erasure/theories/Typed/ExAst.v) 
 - [Coq Extraction Pipeline](https://gist.github.com/4ever2/991007b4418b0ba44f2ee7ed51147e19)
-- [MetaCoq Extracted Terms](https://metacoq.github.io/metacoq/html/MetaCoq.Erasure.EAst.html)
 - [Extraction Example](https://gist.github.com/4ever2/7fbfb3bf843c4773c933c2fdf6315b5c)

src/Agda2Lambox/Compile.hs

@@ -39,7 +39,7 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
     case theDef of
 
       Axiom{} -> do
-        typ <- whenTyped target $ liftTCM $ ([],) <$> compileType defType
+        typ <- whenTyped target $ ([],) <$> compileType defType
         pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
 
       Constructor{conData} -> Nothing <$ requireDef conData
@@ -52,7 +52,7 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
         reportSDoc "agda2lambox.compile" 5 $
           "Found primitive: " <> prettyTCM defName <> ". Compiling it as axiom."
 
-        typ <- liftTCM $ whenTyped target $ ([],) <$> compileType defType
+        typ <- whenTyped target $ ([],) <$> compileType defType
         pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
 
       _ -> genericError $ "Cannot compile: " <> prettyShow defName

src/Agda2Lambox/Compile/Function.hs

@@ -72,7 +72,7 @@ compileFunction (t :: Target t) defn@Defn{theDef, defType} = do
   let mnames = map defName mdefs
 
   -- compile function type, if necessary
-  typ <- liftTCM $ whenTyped t $ ([],) <$> compileType defType
+  typ <- whenTyped t $ ([],) <$> compileType defType
 
   let builder :: LBox.Term -> Maybe (LBox.GlobalDecl t)
       builder = Just . ConstantDecl . ConstantBody typ . Just

src/Agda2Lambox/Compile/Inductive.hs

@@ -19,8 +19,8 @@ import Agda.TypeChecking.Monad.Env ( withCurrentModule )
 import Agda.TypeChecking.Datatypes ( ConstructorInfo(..), getConstructorInfo, isDatatype )
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Telescope (telViewUpTo, piApplyM, teleArgs, telView)
-import Agda.TypeChecking.Substitute (TelView, TelV(theTel))
-import Agda.Compiler.Backend ( getConstInfo, lookupMutualBlock, reportSDoc, AddContext (addContext))
+import Agda.TypeChecking.Substitute (TelView, TelV(theTel), apply)
+import Agda.Compiler.Backend ( getConstInfo, lookupMutualBlock, reportSDoc, AddContext (addContext), constructorForm)
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Common (Arg)
 import Agda.Syntax.Internal ( ConHead(..), unDom, Term)
@@ -69,19 +69,25 @@ compileInductive t defn@Defn{defName} = do
     unless (all (isDataOrRecDef . theDef) defs) $
       genericError "Mutually-defined datatypes/records *and* functions not supported."
 
-    bodies <- liftTCM $ forM defs $ actuallyConvertInductive t
+    bodies <- forM defs $ actuallyConvertInductive t
 
     return $ Just $ LBox.InductiveDecl $ LBox.MutualInductive
       { indFinite = LBox.Finite -- TODO(flupe)
       , indPars   = 0
       , indBodies = NEL.toList bodies
       }
 
-actuallyConvertInductive :: forall t. Target t -> Definition -> TCM (LBox.OneInductiveBody t)
+-- TODO(flupe):
+--   currently the compilation of constructor types is incorrect
+--   indeed, it doesn't account for the fact that for a given constructor,
+--   each argument is in scope for the next ones
+
+-- TODO(flupe):
+--  actually really unify the compilation of both, they do exactly the same thing
+actuallyConvertInductive :: forall t. Target t -> Definition -> CompileM (LBox.OneInductiveBody t)
 actuallyConvertInductive t defn@Defn{defName, theDef} = case theDef of
   Datatype{..} -> do
     params <- theTel <$> telViewUpTo dataPars (defType defn)
-
     reportSDoc "agda2lambox.compile.inductive" 10 $
       "Datatype parameters:" <+> prettyTCM params
 
@@ -101,14 +107,13 @@ actuallyConvertInductive t defn@Defn{defName, theDef} = case theDef of
 
     ctors :: [LBox.ConstructorBody t] <-
       forM dataCons \cname -> do
-        DataCon arity <- getConstructorInfo cname
+        DataCon arity <- liftTCM $ getConstructorInfo cname
 
         typs <- whenTyped t do
           conType <- liftTCM $ (`piApplyM` pvars) =<< defType <$> getConstInfo cname
           conTel  <- toList . theTel <$> telView conType
 
-          forM conTel \dom ->
-            (LBox.Anon,) <$> compileType (unDom dom)
+          forM conTel \dom -> (LBox.Anon,) <$> compileType (unDom dom)
 
         pure LBox.Constructor
           { cstrName  = prettyShow $ qnameName cname
@@ -129,9 +134,18 @@ actuallyConvertInductive t defn@Defn{defName, theDef} = case theDef of
 
     let ConHead{conName, conFields} = recConHead
 
+    params <- theTel <$> telViewUpTo recPars (defType defn)
+    reportSDoc "agda2lambox.compile.inductive" 10 $
+      "Record parameters:" <+> prettyTCM params
+    let pvars :: [Arg Term] = reverse $ teleArgs params
+
     -- TODO
     tyvars  <- whenTyped t $ pure []
-    contyps <- whenTyped t $ pure []
+
+    -- constructor arg types
+    typ <- whenTyped t $
+      let conTel  = toList $ recTel `apply` pvars
+      in forM conTel \dom -> (LBox.Anon,) <$> compileType (unDom dom)
 
     pure LBox.OneInductive
       { indName          = prettyShow $ qnameName defName
@@ -141,7 +155,7 @@ actuallyConvertInductive t defn@Defn{defName, theDef} = case theDef of
           [ LBox.Constructor
               (prettyShow $ qnameName conName)
               (length conFields)
-              contyps
+              typ
           ]
       , indProjs         = []
       , indTypeVars      = tyvars

src/Agda2Lambox/Compile/Term.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE NamedFieldPuns, DerivingVia #-}
+{-# LANGUAGE NamedFieldPuns, DerivingVia, OverloadedStrings #-}
 module Agda2Lambox.Compile.Term
   ( compileTerm
   ) where
@@ -17,7 +17,7 @@ import Agda.Compiler.Backend ( getConstInfo, theDef, pattern Datatype, dataMutua
 import Agda.Syntax.Abstract.Name ( ModuleName(..), QName(..) )
 import Agda.Syntax.Builtin ( builtinNat, builtinZero, builtinSuc )
 import Agda.Syntax.Common ( Erased(..) )
-import Agda.Syntax.Common.Pretty ( prettyShow )
+import Agda.Syntax.Common.Pretty
 import Agda.Syntax.Literal
 import Agda.Syntax.Treeless ( TTerm(..), TAlt(..), CaseInfo(..), CaseType(..) )
 import Agda.TypeChecking.Datatypes ( getConstructorData, getConstructors )
@@ -149,16 +149,53 @@ compileLit = \case
 
   l -> genericError $ "unsupported literal: " <> prettyShow l
 
+compileLitPattern :: Literal -> C LBox.Term
+compileLitPattern = \case
+
+  LitNat i -> do
+    qn <- liftTCM $ getBuiltinName_ builtinNat
+    qz <- liftTCM $ getBuiltinName_ builtinZero
+    qs <- liftTCM $ getBuiltinName_ builtinSuc
+    z  <- liftTCM $ toConApp qz []
+    let ss = take (fromInteger i) $ repeat (toConApp qs . singleton)
+    lift $ requireDef qn
+    liftTCM $ foldrM ($) z ss
+
+  l -> genericError $ "unsupported literal: " <> prettyShow l
+
 compileCaseType :: CaseType -> C LBox.Inductive
 compileCaseType = \case
-  CTData qn -> do lift $ requireDef qn
-                  liftTCM $ toInductive qn
-  _         -> genericError "case type not supported"
-
+  CTData qn -> do 
+    lift $ requireDef qn
+    liftTCM $ toInductive qn
+  CTNat -> do
+    qn <- liftTCM $ getBuiltinName_ builtinNat
+    lift $ requireDef qn
+    liftTCM $ toInductive qn
+  ct -> genericError $ "Case type not supported: " <> show ct
+
+-- TODO: flupe
+--   literal patterns are a bit annoying.
+--   3 -> body
+--   should get compiled to:
+--   succ n -> case n of
+--     succ n -> case n of
+--       succ n -> case n of
+--         zero -> body
+--   but how do we handle the generation of other branches?
+--   perhaps there's already a treeless translation to prevent this
+--   to inverstigate...
 
 compileAlt :: TAlt -> C ([LBox.Name], LBox.Term)
 compileAlt = \case
   TACon{..}   -> let names = take aArity $ repeat LBox.Anon
                  in (names,) <$> underBinders aArity (compileTermC aBody)
-  TALit{..}   -> genericError "literal patterns not supported"
-  TAGuard{..} -> genericError "case guards not supported"
+
+  -- hardcoded support for zero nat literal pattern
+  TALit (LitNat 0) body -> do
+    qn <- liftTCM $ getBuiltinName_ builtinNat
+    lift $ requireDef qn
+    ([],) <$> compileTermC body
+
+  lit@TALit{..} -> genericError $ "Literal pattern not supported:" <> show lit
+  TAGuard{..}   -> genericError "case guards not supported"

src/Agda2Lambox/Compile/Type.hs

@@ -5,6 +5,7 @@ module Agda2Lambox.Compile.Type
   ) where
 
 
+import Control.Monad.Reader
 import Control.Monad ( mapM )
 import Data.List ( foldl' )
 import Data.Function ( (&) )
@@ -18,27 +19,80 @@ import qualified LambdaBox as LBox
 import Agda2Lambox.Compile.Utils ( qnameToKName )
 import Agda2Lambox.Compile.Monad
 
+-- NOTE(flupe):
+--   strategy for type compilation (for future me)
+--   like for terms, we need to keep track of bound variables.
+--   In particular, in λ□ type syntax, variables refer to type variables, using DeBruijn *levels*.
+--   So, when compiling var k,
+--     we should check that if k is below the amount of locally bound bars.
+--       If such => tBox.
+--       otherwise, it HAS to point to a type variable, and we 
+--   
 
-compileType :: Type -> TCM LBox.Type
-compileType = compileType' . unEl
+-- | λ□ type compilation environment.
+data CompileEnv = CompileEnv
+  { typeVars  :: Int
+    -- ^ Type variables, bound outside of the type.
+  , boundVars :: Int
+    -- ^ Amount of locally-bound variables.
+  }
 
+initEnv :: Int -> CompileEnv
+initEnv tvs = CompileEnv
+  { typeVars  = tvs
+  , boundVars = 0
+  }
+
+runC :: Int -> C a -> CompileM a
+runC tvs m = runReaderT m (initEnv tvs)
+
+-- | Increment the number of locally-bound variables.
+underBinder :: C a -> C a
+underBinder = local \e -> e { boundVars = boundVars e + 1 }
+
+-- | Compilation monad.
+type C a = ReaderT CompileEnv CompileM a
+
+
+compileTopLevelType :: Type -> CompileM (LBox.Type)
+compileTopLevelType = undefined
+
+-- | Compile a type, given a number of type variables in scope.
+compileType :: Type -> CompileM LBox.Type
+compileType = runC 0 . compileType'
+
+compileType' :: Type -> C LBox.Type
+compileType' = compileType'' . unEl
+
+compileType'' :: Term -> C LBox.Type
+compileType'' = \case
+  Var n es -> do
+    CompileEnv{..} <- ask
+    if n < boundVars then
+      pure LBox.TBox -- NOTE(flupe): should we still apply the parameters to the box?
+    else do
+      let k = typeVars - (n - boundVars)
+      -- NOTE(flupe): reading the paper, type variables are restricted to Hindley-Milner
+      --              so cannot be type constructors: we don't compile elims
+      pure $ LBox.TVar k
+      -- foldl' LBox.TApp (LBox.TVar k) <$> compileElims es
 
-compileType' :: Term -> TCM LBox.Type
-compileType' = \case
-  Var n es -> foldl' LBox.TApp (LBox.TVar n) <$> compileElims es
   Def q es -> do
-    -- TODO(flupe): check if it's an inductive
+    -- TODO(flupe): check if it's an inductive, or a type alias
     foldl' LBox.TApp (LBox.TConst $ qnameToKName q) <$> compileElims es
   Pi dom abs ->
-    LBox.TArr <$> compileType (unDom dom)
-              <*> compileType (unAbs abs)
+    LBox.TArr <$> compileType' (unDom dom)
+              <*> underBinder (compileType' (unAbs abs))
 
-  Lit{}   -> genericError "type-level literals not supported."
-  Lam{}   -> genericError "type-level abstractions not supported."
-  Con{}   -> genericError "type-level constructors not supported."
-  Sort{}  -> pure LBox.TBox
-  Level{} -> pure LBox.TBox
-  t       -> genericError $ "unsupported type: " <> prettyShow t
+  -- NOTE(flupe):
+  --  My current understanding of typed lambox is that the type translation 
+  t       -> pure LBox.TBox
+
+compileElims :: Elims -> C [LBox.Type]
+compileElims = mapM \case
+  Apply a  -> compileType'' $ unArg a
+  Proj{}   -> genericError "type-level projection elim not supported."
+  IApply{} -> genericError "type-level cubical path application not supported."
 
 -- See: https://github.com/MetaCoq/metacoq/blob/coq-8.20/erasure/theories/Typed/Erasure.v#L780-L817
 -- | Compile a telescope (of parameters) into a list of λ□ type variables.
@@ -57,12 +111,7 @@ compileTele tel =
       , tvarIsArity   = False
           -- ^ type t is an arity if it is "an n-ary dependent function ending with a sort"
       , tvarIsSort    = False
-          -- ^ t : Prop?
+          -- ^ if the type of the parameter ends in a sort.
+          --     say, @(T : Type)@ or @(T : nat -> Type)@ or @(T : Type -> Type)@.
       }
 
-
-compileElims :: Elims -> TCM [LBox.Type]
-compileElims = mapM \case
-  Apply a  -> compileType' $ unArg a
-  Proj{}   -> genericError "type-level projection elim not supported."
-  IApply{} -> genericError "type-level cubical path application not supported."

src/LambdaBox/Env.hs

@@ -38,7 +38,12 @@ data ProjectionBody t = Projection
 data TypeVarInfo = TypeVarInfo
   { tvarName      :: Name
   , tvarIsLogical :: Bool
+     -- ^ A parameter @t@ is *logical* if it is "a proposition when fully applied"
+     --    i.e @t : Prop@ means  t is logical,
+     --        @t a₁ a₂ : Prop@ means t is logical
   , tvarIsArity   :: Bool
+     -- ^ a parameter @t@ is an arity if it is a type when fully applied.
+     --     Consider @(T : Type → Type) (A : T Nat)@. @A@ is an arity, because @T : @
   , tvarIsSort    :: Bool
   }
 
@@ -96,7 +101,10 @@ instance Pretty (OneInductiveBody t) where
 instance Pretty (GlobalDecl t) where
   pretty = \case
     ConstantDecl ConstantBody{..} ->
-      hang "constant:" 2 $ pretty cstBody
+      vsep
+      [ hang "constant:" 2 $ pretty cstBody
+      , foldMap (("type:" <+>) . pretty) cstType
+      ]
 
     InductiveDecl MutualInductive{..} ->
       hang "mutual inductive(s):" 2 $