evaluate programs in coq

Author: flupe

README.md

@@ -12,7 +12,6 @@ The backend builds off Agda 2.7.0.1.
 Compatible with Coq 8.19.0, MetaCoq 1.3.1 and CertiCoq 0.9.
 
 ```
-opam pin add coq 8.19.0
 opam pin add certicoq 0.9+8.19
 coq_makefile -f _CoqProject -o CoqMakefile
 make -f CoqMakefile
@@ -29,9 +28,8 @@ cabal run agda2lambox -- --out-dir build -itest test/Nat.agda
 - [x] Make pretty-printer prettier
 - [x] Ensure well-formedness of generated programs inside Coq
   - [x] Make well-formedness check faster by splitting it into boolean and propositional.
-- [ ] Evaluate λ□ programs from inside Coq to start testing
-  - [ ] Possibly salvage an existing interpreter
-  - [ ] Or implement our own...
+- [x] Evaluate λ□ programs from inside Coq to start testing
+  - [x] Using the λ□-Mut from CertiCoq
 - [ ] Support mutual inductives
 - [x] Support (one-inductive) records
   - [ ] Properly translate projections in terms.

_CoqProject

@@ -1,3 +1,3 @@
 -R theories Agda2Lambox
--R build Build
 theories/CheckWF.v
+theories/Eval.v

src/Agda2Lambox/Convert/Data.hs

@@ -59,9 +59,6 @@ convertDatatype defn@Defn{defName, theDef} =
           -- 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 (?).
+      , indPars   = 0
       , indBodies = [inductive]
       }

src/Agda2Lambox/Convert/Term.hs

@@ -22,6 +22,10 @@ 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
@@ -36,7 +40,7 @@ instance A.TTerm ~> L.Term where
     A.TApp t args -> do
       ct    <- go t
       cargs <- mapM go args
-      return $ foldl LApp ct cargs
+      return $ foldl app ct cargs
     A.TLam t -> inBoundVar $ LLam <$> go t
     A.TLit l -> go l
     A.TCon qn -> do
@@ -87,7 +91,7 @@ instance A.Literal ~> L.Term where
 
       let indnat = L.Inductive (qnameToKerName qnat) 0
 
-      return $ (!! fromInteger n) $ iterate (LApp (LCtor indnat 1 [])) (LCtor indnat 0 [])
+      return $ (!! fromInteger n) $ iterate (app (LCtor indnat 1 [])) (LCtor indnat 0 [])
 
     LitWord64 w -> fail "Literal int64 not supported"
     LitFloat  f -> fail "Literal float not supported"

src/CoqGen.hs

@@ -173,7 +173,7 @@ instance Pretty (ToCoq CoqModule) where
         , "From MetaCoq.Common  Require Import BasicAst Kernames Universes."
         , "From MetaCoq.Utils   Require Import bytestring."
         , "From MetaCoq.Erasure Require Import EAst."
-        , "From Agda2Lambox     Require Import CheckWF."
+        , "From Agda2Lambox     Require Import CheckWF Eval."
         , "Import ListNotations."
         ]
 
@@ -182,9 +182,11 @@ instance Pretty (ToCoq CoqModule) where
 
     , "Compute @check_wf_glob eflags env."
 
-    , vsep $ flip map (zip [1..] coqPrograms) \(i :: Int, kn) -> vsep
-        [ hang ("Definition prog" <> pretty i <> " : program :=") 2 $
+    , vsep $ flip map (zip [1..] $ reverse coqPrograms) \(i :: Int, kn) -> 
+        let progname = "prog" <> pretty i in vsep
+        [ hang ("Definition " <> progname <> " : program :=") 2 $
             pcoq (text "env" :: Doc, LConst kn) 
             <> "."
+        , "Compute eval_program " <> progname <> "."
         ]
     ]

test/Map.agda

@@ -0,0 +1,23 @@
+data Nat : Set where
+  zero : Nat
+  succ : Nat → Nat
+
+add : Nat -> Nat -> Nat
+add zero y = y
+add (succ x) y = succ (add x y)
+
+infixr 7 _::_
+data List (A : Set) : Set where
+  []   : List A
+  _::_ : A -> List A -> List A
+
+xs : List Nat
+xs = zero :: succ zero :: succ (succ zero) :: []
+
+map : {A B : Set} -> (A -> B) -> List A -> List B
+map f [] = []
+map f (x :: xs) = f x :: map f xs
+
+ys : List Nat
+ys = map (\x -> add x x) xs
+{-# COMPILE AGDA2LAMBOX ys #-}

test/Nat.agda

@@ -1,16 +1,18 @@
 data Nat : Set where
   zero : Nat
   succ : Nat → Nat
-{-# BUILTIN NATURAL Nat #-}
+
+one : Nat
+one = succ zero
 
 add : Nat → Nat → Nat
 add zero y = y
 add (succ x) y = succ (add x y)
 
+deux trois : Nat
+deux  = succ (succ zero)
+trois = succ (succ (succ zero))
+
 prog : Nat
-prog = add 3 2
+prog = add trois deux
 {-# COMPILE AGDA2LAMBOX prog #-}
-
--- 5
-res : Nat
-res = 5

theories/CheckWF.v

@@ -23,7 +23,12 @@ Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).
           try auto.
 *)
 
-Definition eflags : EEnvFlags := all_env_flags.
+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 *)
+  |}.
 
 Fixpoint check_fresh_global (k : kername) (decls : global_declarations) : bool :=
   match decls with

theories/Eval.v

@@ -0,0 +1,14 @@
+(* This file provides utilises to evaluate lambda box programs *)
+
+From Coq                   Require Import Nat.
+From MetaCoq.Utils         Require Import utils.
+From MetaCoq.Erasure       Require Import EAst.
+From CertiCoq.Common       Require Import Common.
+From CertiCoq.LambdaBoxMut Require Import compile term program wcbvEval.
+
+(* 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).