fully-apply constructors

Author: flupe

src/Agda/Utils.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleContexts, OverloadedStrings #-}
+{-# LANGUAGE FlexibleContexts, OverloadedStrings, BangPatterns #-}
 
 -- | Agda utilities.
 module Agda.Utils where
@@ -11,9 +11,12 @@ import Control.Arrow ( first )
 import Data.List ( partition )
 import qualified Data.List.NonEmpty as NE ( fromList )
 import Data.Maybe ( isJust, isNothing )
+import Data.Bifunctor ( second )
 
 import Utils
 import Agda.Lib
+import Agda.TypeChecking.Free.Lazy (underBinder)
+import Agda.TypeChecking.Datatypes (getConstructorInfo, ConstructorInfo(..))
 
 -- ** useful monad constraint kinds
 
@@ -59,6 +62,58 @@ unqual = pp . last . qnameToList0
 hasPragma :: QName -> TCM Bool
 hasPragma qn = isJust <$> getUniqueCompilerPragma "AGDA2LAMBOX" qn
 
+
+-- ** eta-expansion of constructors
+
+-- NOTE(flupe):
+--  We do this because CertiCoq requires fully-applied constructors.
+--  In the future, this transformation should be made on the Coq side.
+--  (as it would be proven correct).
+--  NB: MetaCoq provides eta-expansion of constructors, but only for eprograms.
+--  (see : erasure/theories/EConstructorsAsBlocks.v)
+
+-- | Check whether a treeless term is a constructor applied to (many) terms.
+unSpineCon :: TTerm -> Maybe (QName, [TTerm])
+unSpineCon (TCon q)   = Just (q, [])
+unSpineCon (TApp u v) = second (++ v) <$> unSpineCon u
+unSpineCon _          = Nothing
+
+-- | Return the arity of a constructor. Ignores parameters.
+conArity :: ConstructorInfo -> Int
+conArity (DataCon a) = a
+conArity (RecordCon _ _ a _) = a
+
+-- | Eta-expand treeless constructors.
+etaExpandCtor :: TTerm -> TCM TTerm
+etaExpandCtor t | Just (q, args) <- unSpineCon t = do
+  arity <- conArity <$> getConstructorInfo q
+  let nargs = length args
+
+  if nargs >= arity then -- should really be (==), but just in case
+    TApp (TCon q) <$> mapM etaExpandCtor args
+  else do
+    let nlam = arity - nargs
+    exargs <- mapM (etaExpandCtor . raise nlam) args
+    let vars = TVar <$> [(nlam - 1) .. 0]
+    pure $ iterate TLam (TApp (TCon q) $ exargs ++ vars) !! nlam
+
+etaExpandCtor t | otherwise = case t of
+  TApp u v             -> TApp <$> etaExpandCtor u <*> mapM etaExpandCtor v
+  TLam u               -> TLam <$> etaExpandCtor u
+  TLet u v             -> TLet <$> etaExpandCtor u <*> etaExpandCtor v
+  TCase k ci tdef alts -> TCase k ci <$> etaExpandCtor tdef 
+                                     <*> mapM etaExpandAlt alts
+  TCoerce u            -> TCoerce <$> etaExpandCtor u
+  _                    -> pure t
+
+etaExpandAlt :: TAlt -> TCM TAlt
+etaExpandAlt = \case
+  TACon q a b -> TACon q a <$> etaExpandCtor b
+  TAGuard a b -> TAGuard a <$> etaExpandCtor b
+  TALit l b   -> TALit l <$> etaExpandCtor b
+
+  
+
 {-
 lookupCtx :: MonadTCEnv m => Int -> m (String, Type)
 lookupCtx i = first transcribe . (!! i) {-. reverse-} <$> currentCtx

src/Agda2Lambox/Convert/Function.hs

@@ -40,7 +40,7 @@ convertFunctionBody :: Definition :~> Term
 convertFunctionBody Defn{defName} =
   withCurrentModule (qnameModule defName) do
     Just t <- liftTCM $ toTreeless EagerEvaluation defName
-    convert t
+    convert =<< liftTCM (etaExpandCtor t)
 
 -- | Whether a function is a (true) record projection.
 isProjection :: Either ProjectionLikenessMissing Projection -> Bool

src/Agda2Lambox/Convert/Term.hs

@@ -22,10 +22,6 @@ import qualified LambdaBox as L
 import Agda2Lambox.Monad
 import Agda2Lambox.Convert.Class
 
--- quick fix, remove this asap
-app :: L.Term -> L.Term -> L.Term
-app (LCtor ind k es) arg = LCtor ind k (es ++ [arg])
-app t arg                = LApp t arg
 
 -- | Compiling (treeless) Agda terms into Lambox expressions.
 instance A.TTerm ~> L.Term where
@@ -37,19 +33,22 @@ instance A.TTerm ~> L.Term where
       return case qn `elemIndex` mutuals of
         Nothing -> LConst $ qnameToKerName qn
         Just i  -> LRel   $ i + boundVars
+    -- fully-applied constructors
+    A.TApp tc@(A.TCon q) args -> do
+      LCtor ind i [] <- go tc
+      LCtor ind i <$> mapM go args
     A.TApp t args -> do
       ct    <- go t
       cargs <- mapM go args
-      return $ foldl app ct cargs
+      return $ foldl LApp ct cargs
     A.TLam t -> inBoundVar $ LLam <$> go t
     A.TLit l -> go l
     A.TCon qn -> do
       dt   <- liftTCM $ getConstructorData qn
       ctrs <- liftTCM $ getConstructors dt
       Just i <- pure $ qn `elemIndex` ctrs
       return $ LCtor (L.Inductive (qnameToKerName dt) 0) i [] 
-      -- TODO(flupe): I *think* constructors have to be fully-applied
-      -- TODO(flupe): mutual inductives
+      -- TODO(flupe): ^ mutual inductives
     A.TLet tt tu -> LLet <$> go tt <*> inBoundVar (go tu)
     A.TCase n A.CaseInfo{..} tt talts ->
       case caseErased of
@@ -91,7 +90,7 @@ instance A.Literal ~> L.Term where
 
       let indnat = L.Inductive (qnameToKerName qnat) 0
 
-      return $ (!! fromInteger n) $ iterate (app (LCtor indnat 1 [])) (LCtor indnat 0 [])
+      return $ (!! fromInteger n) $ iterate (LApp (LCtor indnat 1 [])) (LCtor indnat 0 [])
 
     LitWord64 w -> fail "Literal int64 not supported"
     LitFloat  f -> fail "Literal float not supported"

test/Map.agda

@@ -19,5 +19,5 @@ map f [] = []
 map f (x :: xs) = f x :: map f xs
 
 ys : List Nat
-ys = map (\x -> add x x) xs
+ys = map succ xs
 {-# COMPILE AGDA2LAMBOX ys #-}

theories/CheckWF.v

@@ -26,8 +26,8 @@ Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
 Definition eflags : EEnvFlags :=
   {| has_axioms      := true;
      term_switches   := all_term_flags;
-     has_cstr_params := false;  (* CertiCoq doesn't want params in ctors *)
-     cstr_as_blocks  := true     (* CertiCoq seem to require fully-applied ctors *)
+     has_cstr_params := false;  (* Agda already drops constructor params *)
+     cstr_as_blocks  := true;   (* The backend fully applies ctors       *)
   |}.
 
 Fixpoint check_fresh_global (k : kername) (decls : global_declarations) : bool :=

theories/Eval.v

@@ -6,9 +6,11 @@ From MetaCoq.Erasure       Require Import EAst.
 From CertiCoq.Common       Require Import Common.
 From CertiCoq.LambdaBoxMut Require Import compile term program wcbvEval.
 
+(* TODO: eta-expand here *)
+
 (* convert a lambda box program to certicoq lambda box mut, and run it *)
 Definition eval_program (p : EAst.program) : exception Term :=
   let prog := {| env  := LambdaBoxMut.compile.compile_ctx (fst p);
       main := compile (snd p)
-  |} 
+  |}
   in wcbvEval (env prog) (2 ^ 14) (main prog).