actually do generate projections

Author: flupe

Playground.v

@@ -1,27 +1,17 @@
-From MetaCoq.Template Require Import Loader.
+From MetaCoq.Template      Require Import Loader Ast.
 From MetaCoq.ErasurePlugin Require Import Erasure Loader.
-From MetaCoq.Utils Require Import utils.
-From MetaCoq.Template Require Import Ast.
-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.
-From Coq Require Import List.
-From Coq Require Import String.
-From Coq Require Import Nat.
-
-Import MCMonadNotation.
+From MetaCoq.Utils         Require Import utils.
+From Coq Require Import ZArith List String Nat.
+
 Import ListNotations.
 
-Local Open Scope string.
-Local Notation "'bs_to_s' s" := (bytestring.String.to_string s) (at level 200).
-Local Notation "'s_to_bs' s" := (bytestring.String.of_string s) (at level 200).
+Check run_erase_program.
 
+Locate run_erase_program.
 
-Program Definition cic_to_box p :=
-  run_erase_program default_erasure_config ([], p) _.
+Program Definition cic_to_box (p : program) :=
+  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].
@@ -52,7 +42,23 @@ with odd (n : nat)  :=
     | S n => even n
   end.
 
-Definition prog  := double.
+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 := prog.
+MetaCoq Quote Recursively Definition ex1 := fst.
+Check ex1.
+Print ex1.
 Eval vm_compute in cic_to_box ex1.

src/Agda/Utils.hs

@@ -113,6 +113,17 @@ etaExpandAlt = \case
   TALit l b   -> TALit l <$> etaExpandCtor b
 
 
+-- * projections
+
+isRecordProjection :: Defn -> Maybe (QName, QName)
+isRecordProjection d
+  | Function{..} <- d
+  , Right Projection{..} <- funProjection
+  , Just recName <- projProper
+  = Just (recName, projOrig)
+  | otherwise
+  = Nothing
+
 
 {-
 lookupCtx :: MonadTCEnv m => Int -> m (String, Type)
@@ -419,15 +430,6 @@ isFunDef = \case
   Function{} -> True
   _ -> False
 
-isRecordProjection :: Defn -> Maybe (QName, QName)
-isRecordProjection d
-  | Function{..} <- d
-  , Right Projection{..} <- funProjection
-  , Just recName <- projProper
-  = Just (recName, projOrig)
-  | otherwise
-  = Nothing
-
 funCC :: (MonadTCM m, HasConstInfo m) => QName -> m CompiledClauses
 funCC q = do
   def <- theDef <$> getConstInfo q

src/Agda2Lambox/Convert/Function.hs

@@ -42,18 +42,12 @@ convertFunctionBody Defn{defName} =
     Just t <- liftTCM $ toTreeless EagerEvaluation defName
     convert =<< liftTCM (etaExpandCtor 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.
@@ -71,9 +65,6 @@ convertFunction defn@Defn{defName, theDef} =
       if any (not . isFunction) mdefs then
         fail "Induction-recursion and other weird mutual defs not supported."
       else inMutuals ms do
-        -- 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
 
         Just . ConstantDecl . Just . flip LFix k <$>

src/Agda2Lambox/Convert/Term.hs

@@ -1,35 +1,38 @@
-{-# LANGUAGE LambdaCase, FlexibleInstances #-}
+{-# LANGUAGE LambdaCase, FlexibleInstances, NamedFieldPuns #-}
 module Agda2Lambox.Convert.Term () where
 
 import Control.Monad.Reader ( ask, liftIO )
+import Data.Foldable ( foldlM )
 import Data.List ( elemIndex )
+import Data.Bifunctor ( second )
+import Data.Functor ( (<&>) )
 
 import Utils
 
 import Agda ( liftTCM, getConstructorData, getConstructors )
 import qualified Agda as A
 import Agda.Lib ()
-import Agda.Utils
+import Agda.Utils ( isRecordProjection )
 import Agda.Syntax.Literal
+import Agda.Syntax.Internal ( unDom )
 import Agda.Syntax.Abstract.Name ( QName(..), ModuleName(..) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.TypeChecking.Primitive.Base ( getBuiltinName )
-import Agda.Compiler.Backend ( builtinNat, builtinZero, builtinSuc )
+import Agda.Compiler.Backend hiding (Name)
 
 import LambdaBox
 import qualified LambdaBox as L
 
 import Agda2Lambox.Monad
 import Agda2Lambox.Convert.Class
 
-
 -- | Compiling (treeless) Agda terms into Lambox expressions.
 instance A.TTerm ~> L.Term where
   go = \case
     A.TVar n   -> return $ LRel n
     A.TPrim pr -> go pr 
     A.TDef qn -> do
-      Env{..} <- ask
+      Env{mutuals, boundVars} <- ask
       return case qn `elemIndex` mutuals of
         Nothing -> LConst $ qnameToKerName qn
         Just i  -> LRel   $ i + boundVars
@@ -57,8 +60,8 @@ instance A.TTerm ~> L.Term where
           calts <- traverse go talts
           cind  <- go caseType
           return $ LCase cind 0 (LRel n) calts
-    A.TUnit -> return LBox
-    A.TSort -> return LBox
+    A.TUnit   -> return LBox
+    A.TSort   -> return LBox
     A.TErased -> return LBox
     A.TCoerce tt  -> fail "Coerces are not supported."
     A.TError terr -> fail "Errors are not supported."

src/LambdaBox.hs

@@ -8,8 +8,6 @@ import Agda.Syntax.Common.Pretty
 import Agda.Syntax.Abstract.Name ( QName(..), ModuleName(..) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
--- TODO(flupe): Record projections?
-
 -- | Identifiers.
 -- Used only for pretty-printing by MetaCoq?
 -- MetaCoq uses bytestrings, it doesn't matter here.
@@ -124,18 +122,17 @@ data Term
   | LVar Ident       -- ^ Free variable with identifier
       -- NOTE(flupe): not needed?
   | LLam Term        -- ^ Lambda abstraction
-  | LLet Term Term  
+  | LLet Term Term
       -- ^ Let bindings.
       --   Unused in the backend, since Agda itself no longer has let bindings
       --   in the concrete syntac.
   | LApp Term Term              -- ^ Term application
   | LConst KerName              -- ^ Named constant.
-    -- TODO(flupe): I *think* constructors have to be fully-applied.
   | LCtor Inductive Int [Term]  -- ^ Inductive constructor.
   | LCase Inductive Int Term [([Name], Term)]
       -- ^ Pattern-matching case construct.
   | LFix MFixpoint Int
-      -- ^ Fixpoint combinator. 
+      -- ^ Fixpoint combinator.
       -- The index refers to which fixpoint we select out of
       -- the generated (mutual) fixpoints.
   deriving (Eq, Show)

test/Proj.agda

@@ -0,0 +1,15 @@
+data Bool : Set where true false : Bool
+
+record Pair (A B : Set) : Set where
+  constructor _,_
+  field
+    fst : A
+    snd : B
+open Pair
+
+pair : Pair Bool Bool
+pair = true , false
+
+second : Bool
+second = snd pair
+{-# COMPILE AGDA2LAMBOX second #-}

theories/CheckWF.v

@@ -25,7 +25,23 @@ Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
 
 Definition eflags : EEnvFlags :=
   {| has_axioms      := true;
-     term_switches   := all_term_flags;
+     term_switches   :=
+       {| has_tBox        := true
+        ; has_tRel        := true
+        ; has_tVar        := true
+        ; has_tEvar       := true
+        ; has_tLambda     := true
+        ; has_tLetIn      := true
+        ; has_tApp        := true
+        ; has_tConst      := true
+        ; has_tConstruct  := true
+        ; has_tCase       := true
+        ; has_tProj       := false (* Our backends shouldn't produce projections *)
+        ; has_tFix        := true
+        ; has_tCoFix      := true
+        ; has_tPrim       := all_primitive_flags
+        ; has_tLazy_Force := true
+        |};
      has_cstr_params := false;  (* Agda already drops constructor params *)
      cstr_as_blocks  := true;   (* The backend fully applies ctors       *)
   |}.