add flag for typed compil, weird gadts

Author: flupe

Playground.v

@@ -1,24 +1,49 @@
 From MetaCoq.Template      Require Import Loader Ast.
 From MetaCoq.ErasurePlugin Require Import Erasure Loader.
 From MetaCoq.Utils         Require Import utils.
+From MetaCoq.Erasure.Typed Require Import ResultMonad.
+From MetaCoq.Erasure.Typed Require Import Optimize.
+From MetaCoq.Erasure.Typed Require Import Extraction.
 From Coq Require Import ZArith List String Nat.
 
+Import MCMonadNotation.
 Import ListNotations.
 
 Check run_erase_program.
 
 Locate run_erase_program.
 
 Program Definition cic_to_box (p : program) :=
-  run_erase_program default_erasure_config p _.
+  run_erase_program default_erasure_config ([], p) _.
 Next Obligation.
+  split. easy.
   split.
   now eapply assume_that_we_only_erase_on_welltyped_programs.
   cbv [PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn].
   pose proof @PCUICSN.normalization.
   split; typeclasses eauto.
 Qed.
 
+Definition no_check_args :=
+  {| check_wf_env_func Σ := Ok (assume_env_wellformed Σ);
+     template_transforms := [];
+     pcuic_args :=
+       {| optimize_prop_discr := true;
+          extract_transforms := [dearg_transform (fun _ => None) true true false false false] |} |}.
+
+Definition cic_to_box_typed p :=
+  entry <- match p.2 with
+           | tConst kn _ => Ok kn
+           | tInd ind _ => Ok (inductive_mind ind)
+           | _ => Err ("Expected program to be a tConst or tInd")
+           end;;
+  Σ <- extract_template_env
+         no_check_args
+         p.1
+         (KernameSet.singleton entry)
+         (fun k => false);;
+  Ok Σ.
+
 Definition not (x : bool) := 
   match x with 
     | true => true
@@ -42,23 +67,5 @@ with odd (n : nat)  :=
     | S n => even n
   end.
 
-Set Primitive Projections.
-Set Printing Projections.
-
-Record Prod (A B : Type) : Type := Pair
-  { fst : A
-  ; snd : B
-  }.
-
-Arguments Pair {_ _} _ _.
-Arguments fst {_ _} _.
-Arguments snd {_ _} _.
-
-Definition pair : Prod bool bool := Pair true false.
-
-Definition prog  := pair.(fst).
-
-MetaCoq Quote Recursively Definition ex1 := fst.
-Check ex1.
-Print ex1.
-Eval vm_compute in cic_to_box ex1.
+MetaCoq Quote Recursively Definition ex1 := odd.
+Eval vm_compute in cic_to_box_typed ex1.

agda2lambox.cabal

@@ -16,13 +16,18 @@ executable agda2lambox
   hs-source-dirs:      src
   main-is:             Main.hs
   other-modules:       Agda.Utils,
+                       Agda2Lambox.Compile.Target,
                        Agda2Lambox.Compile.Utils,
                        Agda2Lambox.Compile.Monad,
                        Agda2Lambox.Compile.Term,
                        Agda2Lambox.Compile.Function,
                        Agda2Lambox.Compile.Inductive,
                        Agda2Lambox.Compile.Type,
                        Agda2Lambox.Compile,
+                       LambdaBox.Names,
+                       LambdaBox.Term,
+                       LambdaBox.Type,
+                       LambdaBox.Env,
                        LambdaBox,
                        CoqGen,
                        Paths_agda2lambox

src/Agda2Lambox/Compile.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NamedFieldPuns, DataKinds #-}
 module Agda2Lambox.Compile 
   ( compileDefinition
   ) where
@@ -13,14 +13,18 @@ import Agda.TypeChecking.Monad ( liftTCM, getConstInfo )
 import Agda.Utils.Monad ( whenM )
 
 import Agda.Utils ( hasPragma, isDataOrRecDef )
+
 import Agda2Lambox.Compile.Monad
+import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Function  ( compileFunction  )
 import Agda2Lambox.Compile.Inductive ( compileInductive )
-import LambdaBox
+
+import LambdaBox.Names
+import LambdaBox.Env ( GlobalDecl )
 
 
-compileDefinition :: Definition -> CompileM (Maybe (KerName, GlobalDecl))
+compileDefinition :: Definition -> CompileM (Maybe (KerName, GlobalDecl Untyped))
 compileDefinition defn@Defn{..} = do
   fmap (qnameToKerName defName,) <$> -- prepend kername
     case theDef of

src/Agda2Lambox/Compile/Function.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NamedFieldPuns, DataKinds #-}
 -- | Convert Agda functions to λ□ constant declarations
 module Agda2Lambox.Compile.Function 
   ( compileFunction
@@ -10,7 +10,7 @@ import Data.List ( elemIndex )
 import Data.Maybe ( isNothing, fromMaybe )
 
 import Agda.Syntax.Abstract.Name ( QName, qnameModule )
-import Agda.TypeChecking.Monad.Base
+import Agda.TypeChecking.Monad.Base hiding ( None )
 import Agda.Compiler.ToTreeless ( toTreeless )
 import Agda.Compiler.Backend ( getConstInfo, funInline )
 import Agda.Syntax.Treeless ( EvaluationStrategy(EagerEvaluation) )
@@ -20,10 +20,13 @@ import Agda.Utils.Monad (guardWithError, whenM)
 import Agda.Utils.Lens ( (^.) )
 
 import Agda.Utils ( etaExpandCtor, treeless, pp )
+import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
 import Agda2Lambox.Compile.Term ( compileTerm )
+
 import LambdaBox qualified as LBox
+import LambdaBox.Env
 
 
 -- | Check whether a definition is a function.
@@ -49,7 +52,7 @@ shouldCompileFunction def@Defn{theDef} | Function{..} <- theDef
 
 
 -- | Convert a function definition to a λ□ declaration.
-compileFunction :: Definition -> CompileM (Maybe LBox.GlobalDecl)
+compileFunction :: Definition -> CompileM (Maybe (LBox.GlobalDecl Untyped))
 compileFunction defn | not (shouldCompileFunction defn) = return Nothing
 compileFunction defn@Defn{theDef} = do
   let Function{funMutual = Just mutuals} = theDef
@@ -65,13 +68,14 @@ compileFunction defn@Defn{theDef} = do
   let mnames = map defName mdefs
 
   -- if the function is not recursive, just compile the body
-  if null mdefs then Just. LBox.ConstantDecl . Just <$> compileFunctionBody [] defn
+  if null mdefs then
+    Just . ConstantDecl . ConstantBody None . Just <$> compileFunctionBody [] defn
 
   -- otherwise, take fixpoint
   else do
     let k = fromMaybe 0 $ elemIndex (defName defn) mnames
 
-    Just . LBox.ConstantDecl . Just . flip LBox.LFix k <$>
+    Just . ConstantDecl . ConstantBody None . Just . flip LBox.LFix k <$>
       forM mdefs \def@Defn{defName} -> do
         body <- compileFunctionBody mnames def
         return LBox.Def

src/Agda2Lambox/Compile/Inductive.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE NamedFieldPuns, ImportQualifiedPost #-}
+{-# LANGUAGE NamedFieldPuns, ImportQualifiedPost, DataKinds #-}
 -- | Convert Agda datatypes to λ□ inductive declarations
 module Agda2Lambox.Compile.Inductive
   ( compileInductive
@@ -14,7 +14,7 @@ import Data.Maybe ( isJust, listToMaybe, fromMaybe )
 import Data.Traversable ( mapM )
 
 import Agda.Syntax.Abstract.Name ( qnameModule, qnameName )
-import Agda.TypeChecking.Monad.Base
+import Agda.TypeChecking.Monad.Base hiding (None)
 import Agda.TypeChecking.Monad.Env ( withCurrentModule )
 import Agda.TypeChecking.Datatypes ( ConstructorInfo(..), getConstructorInfo, isDatatype )
 import Agda.Compiler.Backend ( getConstInfo, lookupMutualBlock )
@@ -23,13 +23,14 @@ import Agda.Syntax.Internal ( ConHead(..), unDom )
 import Agda.Utils.Monad ( unlessM )
 
 import Agda.Utils ( isDataOrRecDef )
+import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
 import LambdaBox qualified as LBox
 
 
 -- | Toplevel conversion from a datatype/record definition to a Lambdabox declaration.
-compileInductive :: Definition -> CompileM (Maybe LBox.GlobalDecl)
+compileInductive :: Definition -> CompileM (Maybe (LBox.GlobalDecl Untyped))
 compileInductive defn@Defn{defName} = do
   mutuals <- liftTCM $ dataOrRecDefMutuals defn
 
@@ -69,16 +70,17 @@ compileInductive defn@Defn{defName} = do
       , indBodies = NEL.toList bodies
       }
 
-actuallyConvertInductive :: Definition -> TCM LBox.OneInductiveBody
+actuallyConvertInductive :: Definition -> TCM (LBox.OneInductiveBody Untyped)
 actuallyConvertInductive Defn{defName, theDef, defMutual} = case theDef of
   Datatype{..} -> do
 
-    ctors :: [LBox.ConstructorBody]
+    ctors :: [LBox.ConstructorBody Untyped]
       <- forM dataCons \cname -> do
            DataCon arity <- getConstructorInfo cname
-           return LBox.Ctor
-             { ctorName = prettyShow $ qnameName cname
-             , ctorArgs = arity
+           return LBox.Constructor
+             { cstrName  = prettyShow $ qnameName cname
+             , cstrArgs  = arity
+             , cstrTypes = None
              }
 
     pure LBox.OneInductive
@@ -87,19 +89,23 @@ actuallyConvertInductive Defn{defName, theDef, defMutual} = case theDef of
       , indKElim         = LBox.IntoAny -- TODO(flupe)
       , indCtors         = ctors
       , indProjs         = []
+      , indTypeVars      = None
       }
 
   Record{..} -> do
 
     let ConHead{conName, conFields} = recConHead
-        fields :: [LBox.ProjectionBody] = LBox.Proj . prettyShow . qnameName . unDom <$> recFields
+        fields :: [LBox.ProjectionBody Untyped] =
+          flip LBox.Projection None . prettyShow . qnameName . unDom <$> recFields
 
     pure LBox.OneInductive
       { indName          = prettyShow $ qnameName defName
       , indPropositional = False        -- TODO(flupe)
       , indKElim         = LBox.IntoAny -- TODO(flupe)
-      , indCtors         = [ LBox.Ctor (prettyShow $ qnameName conName) (length conFields) ]
+      , indCtors         = 
+          [ LBox.Constructor (prettyShow $ qnameName conName) (length conFields) None ]
       , indProjs         = fields
+      , indTypeVars      = None
       }
 
   -- { indFinite = maybe LBox.BiFinite inductionToRecKind recInduction

src/Agda2Lambox/Compile/Target.hs

@@ -0,0 +1,33 @@
+{-# LANGUAGE DataKinds, GADTs #-}
+-- | Compile targets for the backend
+module Agda2Lambox.Compile.Target 
+  ( Typing(..)
+  , Target(..)
+  , WhenTyped(..)
+  , extract
+  ) where
+
+import Control.DeepSeq ( NFData(rnf) )
+import Data.Kind ( Type )
+
+-- | Supported targets.
+data Typing = Typed | Untyped
+
+-- | Compile targets, indexed by the kind of target.
+data Target :: Typing -> Type where
+  ToTyped   :: Target Typed
+  ToUntyped :: Target Untyped
+
+-- | Type wrapper that contains a value iff we're in the typed setting.
+data WhenTyped a :: Typing -> Type where
+  None ::      WhenTyped a Untyped
+  Some :: a -> WhenTyped a Typed
+
+-- | Attempt retrieving value.
+extract :: WhenTyped a t -> Maybe a
+extract None = Nothing
+extract (Some x) = Just x
+
+instance NFData (Target t) where
+  rnf ToTyped   = ()
+  rnf ToUntyped = ()

src/Agda2Lambox/Compile/Term.hs

@@ -24,6 +24,7 @@ import Agda.TypeChecking.Datatypes ( getConstructorData, getConstructors )
 import Agda.TypeChecking.Monad.Base ( TCM , liftTCM, MonadTCEnv, MonadTCM )
 import Agda.TypeChecking.Monad.Builtin ( getBuiltinName_ )
 
+import LambdaBox.Names ( Name(..) )
 import LambdaBox ( Term(..) )
 import LambdaBox qualified as LBox
 import Agda2Lambox.Compile.Utils
@@ -105,12 +106,12 @@ compileTermC = \case
     ces <- traverse compileTermC es
     pure $ foldl' LApp cu ces
 
-  TLam t -> underBinder $ LLam <$> compileTermC t
+  TLam t -> underBinder $ LLambda Anon <$> compileTermC t
 
   TLit l -> compileLit l
 
-  TLet u v -> LLet <$> compileTermC u
-                   <*> underBinder (compileTermC v)
+  TLet u v -> LLetIn Anon <$> compileTermC u
+                          <*> underBinder (compileTermC v)
 
   TCase n CaseInfo{..} dt talts ->
     case caseErased of

src/Agda2Lambox/Compile/Utils.hs

@@ -59,4 +59,5 @@ toConApp qn es = do
   ctrs <- getConstructors dt
   ind  <- toInductive dt
   let idx = fromMaybe 0 $ qn `elemIndex` ctrs
-  pure $ LBox.LCtor ind idx es
+  pure $ LBox.LConstruct ind idx es
+