Implement and verify the naive translation of lazy/force to thunks (#98)

* Implement and verify the naive translation of lazy/force to thunks
based on the latest metacoq. Add a lazy factorial test in the benchmarks

* Fix build instructions to use metacoq submodule

* Fix build.yml?

* Point to the right metacoq dev version in the opam file

* Forgot one file

.github/workflows/build.yml

@@ -23,19 +23,19 @@ jobs:
       fail-fast: false  # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v3
-        # with:
-        #   submodules: true
+        with:
+           submodules: true
       - uses: coq-community/docker-coq-action@v1
         with:
           custom_image: ${{ matrix.image }}
           opam_file: ${{ matrix.opam_file }}
-          # before_install: | # comment back in if MetaCoq commit changes
-          #   startGroup "fix permission issues"
-          #     sudo chown -R coq:coq .
-          #   endGroup
-          #   startGroup "opam pin"
-          #     opam pin -n -y submodules/metacoq
-          #   endGroup
+          before_install: | # comment back in if MetaCoq commit changes
+            startGroup "fix permission issues"
+              sudo chown -R coq:coq .
+            endGroup
+            startGroup "opam pin"
+              opam pin -n -y submodules/metacoq
+            endGroup
           before_script: |
             startGroup "fix permission issues"
               sudo chown -R coq:coq .

benchmarks/TESTS

@@ -5,4 +5,5 @@ vs_easy
 vs_hard
 binom
 color
-sha_fast
+sha_fast
+lazy_factorial

benchmarks/lazy_factorial_main.c

@@ -0,0 +1,35 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "gc_stack.h"
+#include <time.h>
+
+extern value body(struct thread_info *);
+
+int main(int argc, char *argv[]) {
+  value val;
+  struct thread_info* tinfo;
+  clock_t start, end;
+  double msec, sec;
+
+  // Specify number of runs
+  int n = 1;
+  if (argc > 1) n = atoi(argv[1]);
+
+  start = clock();
+  // Run Coq program
+  for (int i = 0; i < n; i ++) {
+    tinfo = make_tinfo();
+    body(tinfo);
+  }
+  end = clock();
+
+  /* TODO write string printers */
+  /* print_Coq_Init_Datatypes_list(val, print_Coq_Init_Datatypes_bool); */
+  /* printf("\n"); */
+
+  sec = (double)(end - start)/CLOCKS_PER_SEC;
+  msec = 1000*sec;
+  printf("Time taken %f seconds %f milliseconds\n", sec, msec);
+
+  return 0;
+}

benchmarks/tests.v

@@ -69,7 +69,7 @@ Definition color := Color.main.
 
 (* Lazy factorial. Needs coinductive types *)
 
-(* Definition lazy_factorial := coq_msg_info (string_of_Z (coind.lfact 150)). *)
+Definition lazy_factorial := string_of_Z (coind.lfact 150).
 
 (* Sha *)
 
@@ -116,6 +116,14 @@ CertiCoq Compile -args 1000 -config 9 -O 1 -ext "_opt_ll" list_sum.
 (* CertiCoq Compile -cps -ext "_cps_opt" list_sum. *)
 CertiCoq Generate Glue -file "glue_list_sum" [ nat ].
 
+Eval compute in "Compiling lazy factorial (using unsafe passes)".
+
+CertiCoq Compile -unsafe-erasure -O 1 lazy_factorial.
+CertiCoq Compile -unsafe-erasure -ext "_opt" lazy_factorial.
+CertiCoq Compile -unsafe-erasure -args 1000 -config 9 -O 1 -ext "_opt_ll" lazy_factorial. 
+(* CertiCoq Compile -O 0 -cps -ext "_cps" demo1. *)
+(* CertiCoq Compile -cps -ext "_cps_opt" demo1. *)
+CertiCoq Generate Glue -file "glue_lazy_factorial" [ ].
 
 Eval compute in "Compiling vs_easy".
 
@@ -145,15 +153,6 @@ CertiCoq Compile -args 1000 -config 9 -O 1 -ext "_opt_ll" binom.
 (* CertiCoq Compile -cps -ext "_cps_opt" binom. *)
 CertiCoq Generate Glue -file "glue_binom" [ nat ].
 
-(* Eval compute in "Compiling lazy factorial". *)
-
-(* CertiCoq Compile -O 1 lazy_factorial.
-CertiCoq Compile -ext "_opt" lazy_factorial.
-CertiCoq Compile -args 1000 -config 9 -O 1 -ext "_opt_ll" lazy_factorial. *)
-(* CertiCoq Compile -O 0 -cps -ext "_cps" demo1. *)
-(* CertiCoq Compile -cps -ext "_cps_opt" demo1. *)
-(* CertiCoq Generate Glue -file "glue_lazy_factorial" [ ]. *)
-
 
 Eval compute in "Compiling color".
 Require Import ZArith.

coq-certicoq.opam

@@ -36,8 +36,8 @@ depends: [
   "coq" {>= "8.19" & < "8.20~"}
   "coq-compcert" {= "3.13.1"}
   "coq-equations" {= "1.3+8.19"}
-  "coq-metacoq-erasure-plugin" {= "1.3.1+8.19"}
-  "coq-metacoq-safechecker-plugin" {= "1.3.1+8.19"}
+  "coq-metacoq-erasure-plugin" {= "8.19.dev"}
+  "coq-metacoq-safechecker-plugin" {= "8.19.dev"}
   "coq-ext-lib" {>= "0.12"}
 ]
 

theories/LambdaBoxMut/compile.v

@@ -342,6 +342,30 @@ Polymorphic Equations trans_prim_val {T} (p : EPrimitive.prim_val T) : option pr
   trans_prim_val (existT _ primFloat (primFloatModel i)) => Some (existT _ AstCommon.primFloat i) ;
   trans_prim_val (existT _ primArray _) => None.
 
+Section LiftSize.
+Import All_Forall MCList ELiftSubst EInduction.
+Lemma size_lift n k t : size (ELiftSubst.lift n k t) = size t.
+Proof.
+  revert k; induction t using term_forall_list_ind; cbn; eauto; try lia; ELiftSubst.solve_all.
+  - destruct Nat.leb; auto.
+  - f_equal. induction X; cbn; auto. specialize (p k). lia.
+  - f_equal. f_equal. specialize (IHt1 k); specialize (IHt2 (S k)). lia.
+  - f_equal.  specialize (IHt1 k); specialize (IHt2 k). lia.
+  - f_equal. induction X; cbn; auto. specialize (p k); lia.
+  - rewrite IHt; cbn. f_equal. f_equal.
+    induction X; cbn; auto. rewrite IHX, p. lia.
+  - f_equal; induction X in k |- *; cbn; auto.
+    specialize (IHX (S k)). rewrite Nat.add_succ_r in IHX. rewrite IHX, p. lia.
+  - f_equal. induction X in k |- *; cbn; auto.
+    specialize (IHX (S k)). rewrite Nat.add_succ_r in IHX. rewrite IHX, p. lia.
+  - depelim X; cbn; auto.
+    destruct p as [p IHX]. rewrite p.
+    f_equal. f_equal.
+    induction IHX in k |- *; cbn; auto.
+    now rewrite p0, IHIHX.
+  Qed.
+End LiftSize.
+
 Section Compile.
   Import MCList (map_InP, In_size).
 
@@ -374,10 +398,8 @@ Section Compile.
     | tPrim p with trans_prim_val p := 
       { | None => TWrong "unsupported primtive type"
         | Some pv => TPrim pv }
-    | tLazy t => TWrong "Lazy" (* TLambda nAnon (lift 1 (compile t)) *)
-    | tForce t => TWrong "Force"
-      (* TmkApps (compile t) 
-      (tcons (TPrim (@existT _ (fun tag => prim_value tag) AstCommon.primInt 0)) tnil) *)
+    | tLazy t => TLambda nAnon (lift 0 (compile t))
+    | tForce t => TmkApps (compile t) (tcons TProof tnil)
     | tVar _ => TWrong "Var"
     | tEvar _ _ => TWrong "Evar" }.
   Proof.

theories/LambdaBoxMut/program.v

@@ -279,6 +279,26 @@ Proof.
     + apply LMiss; assumption.
 Qed.
 
+Lemma Crct_lift:
+  (forall p n t, crctTerm p n t -> forall k, crctTerm p (S n) (lift k t)) /\
+  (forall p n ts, crctTerms p n ts -> forall k, crctTerms p (S n) (lifts k ts)) /\
+  (forall p n ts, crctBs p n ts -> forall k, crctBs p (S n) (liftBs k ts)) /\
+  (forall p n ts, crctDs p n ts -> forall k, crctDs p (S n) (liftDs k ts)) /\
+  (forall p, crctEnv p -> crctEnv p).
+Proof.
+  apply crctCrctsCrctBsDsEnv_ind; intros;
+  try (solve[cbn; repeat econstructor; intuition eauto]).
+  (* 2-9:try (econstructor; intuition auto); try eassumption. *)
+  - cbn. constructor; eauto. destruct (Nat.compare_spec m k); subst; try lia.
+  - cbn. econstructor; eauto. inversion_Clear H. econstructor; eauto.
+    now rewrite lifts_pres_tlength.
+  - econstructor; eauto.
+  - cbn. constructor; eauto. rewrite liftDs_pres_dlength. eauto.
+    rewrite liftDs_pres_dlength; lia.
+  - cbn. constructor; eauto. now rewrite Nat.add_succ_r.
+  - cbn. constructor; eauto. destruct H as [na [body ->]]. now do 2 eexists.
+Qed.
+
 Lemma Crct_weaken_Typ:
   (forall p n t, crctTerm p n t -> 
                  forall nm s, fresh nm p ->

theories/LambdaBoxMut/stripEvalCommute.v

@@ -37,7 +37,8 @@ Definition prim_flags :=
 
 (** Cofixpoints are not supported, Var and Evar don't actually appear 
     in terms to compile, and projections are inlined to cases earlier
-    in the pipeline. *)
+    in the pipeline. We compile down lazy/force to thunks, for a purely
+    functional implementation of cofixpoints. *)
 Definition term_flags :=
   {|
     has_tBox := true;
@@ -54,7 +55,7 @@ Definition term_flags :=
     has_tFix := true;
     has_tCoFix := false;
     has_tPrim := prim_flags;
-    has_tLazy_Force := false;
+    has_tLazy_Force := true;
   |}.
 
 Definition env_flags := 
@@ -506,6 +507,16 @@ Proof.
   now rewrite (wellformed_lookup_inductive_pars _ wfΣ hl').
 Qed.
 
+
+Lemma compile_lift n t : compile.lift n (compile t) = compile (lift 1 n t).
+Proof.
+  funelim (compile t); cbn [lift compile.lift]; simp compile => //.
+  - destruct (Nat.compare_spec n n0); 
+    destruct (Nat.leb_spec n0 n); subst; try lia; simp compile; auto.
+  -
+  Admitted.
+
+
 Lemma wellformed_crct {Σ} t :
   wf_glob Σ ->
   crctEnv (compile_ctx Σ) ->
@@ -553,6 +564,7 @@ Proof.
     now eapply compile_isLambda.
   - cbn. rewrite -dlength_hom. move/andP: H0 => [] /Nat.ltb_lt //.
   - destruct p as [? []]; try constructor; eauto. simp trans_prim_val. cbn. now cbn in H.
+  - specialize (H k H0). now eapply Crct_lift in H.
 Qed.
 
 Lemma compile_fresh kn Σ : fresh_global kn Σ -> fresh kn (compile_ctx Σ).
@@ -605,9 +617,9 @@ Proof.
 Qed.
 
 Lemma isLambda_compile f : 
-  ~~ EAst.isLambda f -> ~ isLambda (compile f).
+  ~~ EAst.isLambda f -> ~~ isLazy f -> ~ isLambda (compile f).
 Proof.
-  intros nf. move=> [] na [] bod.
+  intros nf nl. move=> [] na [] bod.
   destruct f; simp_compile => /= //.
   rewrite compile_decompose.
   destruct decompose_app eqn:da.
@@ -755,10 +767,11 @@ Arguments instantiate _ _ !tbod.
 
 Lemma compile_csubst Σ a n k b : 
   wf_glob Σ ->
+  wellformed Σ 0 a ->
   wellformed Σ (n + k) b ->
   compile (ECSubst.csubst a k b) = instantiate (compile a) k (compile b).
 Proof.
-  intros wfΣ.
+  intros wfΣ wfa.
   revert b n k.
   apply: MkAppsInd.rec. all:intros *. 
   all:cbn -[instantiateBrs instantiateDefs lookup_inductive lookup_constructor]; try intros until k; simp_eta;
@@ -779,11 +792,11 @@ Proof.
         - cbn -[instantiates]. rewrite instantiates_tcons.
           f_equal; eauto. now eapply p. }
   - rewrite instantiate_TConstruct. f_equal.
-    move/and3P: H => [] _ _ wfa. solve_all.
-    induction wfa; auto.
+    move/and3P: H => [] _ _ wfa'. solve_all.
+    induction wfa'; auto.
     cbn -[instantiates].
     rewrite instantiates_tcons. f_equal. repeat eapply p.
-    eapply IHwfa.
+    eapply IHwfa'.
   - rewrite map_map_compose.
     move/andP: H0 => [] /andP[] wfi wft wfl.
     set (brs' := map _ l). cbn in brs'.
@@ -808,6 +821,11 @@ Proof.
       destruct p; len.
       f_equal; eauto. apply (e n0) => //. eapply wellformed_up; tea. lia.
   - destruct p as [? []]; simp trans_prim_val; cbn => //.
+  - cbn. f_equal. rewrite (H n); auto. 
+    pose proof (instantiate_lift (compile a)) as [il _].
+    specialize (il (compile t) k 0).
+    apply il. lia. eapply Crct_WFTrm.
+    eapply wellformed_crct; tea. now eapply wellformed_env_crctEnv.
 Qed.
 
 Fixpoint substl_rev terms k body :=
@@ -936,7 +954,7 @@ Proof.
   rewrite !Nat.add_0_r. cbn. intros wfb. rewrite IHcla.
   eapply (wellformed_csubst _ _ 0) => //.
   f_equal. 
-  rewrite tlength_hom. eapply (compile_csubst _ 1) => //. apply wf. eapply wfb.
+  rewrite tlength_hom. eapply (compile_csubst _ 1); tea.
 Qed.
 
 Lemma compile_substl_nrev Σ a b : 
@@ -989,6 +1007,15 @@ Proof.
   f_equal. now rewrite -compile_fix_subst.
 Qed.
 
+Lemma nisLazyApp_isLazy t : ~~ isLazyApp t -> ~~ isLazy t.
+Proof.
+  unfold isLazyApp.
+  have da := decompose_app_head_spine t.
+  rewrite -{2}(mkApps_head_spine t).
+  destruct (spine t) using rev_case => //.
+  rewrite mkApps_app //=.
+Qed.
+
 From MetaCoq.Erasure Require Import EConstructorsAsBlocks EWcbvEvalCstrsAsBlocksInd.
 
 Lemma WcbvEval_hom (fl := block_wcbv_flags) :
@@ -1086,16 +1113,21 @@ Proof.
     destruct (decompose_app (tApp f' a')) eqn:da'.
     constructor; eauto.
     rewrite !negb_or in nlam. rtoProp; intuition auto.
-    eapply (isLambda_compile) in H. contradiction.
-    eapply (isFix_compile) in H3; auto.
-    eapply (isConstructApp_compile) in H4; auto.
-    eapply (isBox_compile) in H2. contradiction.
-    now eapply isPrimApp_compile in H4.
+    eapply (isLambda_compile) in H. contradiction. now eapply nisLazyApp_isLazy in H0.
+    eapply (isFix_compile) in H4; auto.
+    eapply (isConstructApp_compile) in H5; auto.
+    eapply (isBox_compile) in H3. contradiction.
+    now eapply isPrimApp_compile in H5.
   - intros hl hargs evargs IHargs.
     simp_compile. econstructor. clear hargs.
     move: IHargs. cbn. induction 1; cbn; constructor; intuition auto.
     apply r. apply IHIHargs. now depelim evargs.
   - cbn. move/andP=> [hasp testp] ih. depelim ih; simp_compile; simp trans_prim_val; cbn => //; try constructor.
+  - intros evt evt' [IHt wft wfl] [IHt' wft' wfv].
+    simp_compile. simp_compile in IHt. cbn.
+    eapply wAppLam; tea. eapply wProof.
+    unfold whBetaStep.
+    rewrite (proj1 (instantiate_noLift TProof) (compile t') 0). exact IHt'.
   - intros isat wf.
     destruct t => //; simp_compile; econstructor.
     cbn in isat. destruct args => //.