Fix the translation of cofix to fix to move the head constructors's l…

…azy at the toplevel of the definition

erasure/theories/ECoInductiveToInductive.v

@@ -36,6 +36,29 @@ Hint Constructors eval : core.
 Section trans.
   Context (Σ : GlobalContextMap.t).
 
+  Fixpoint remove_head_lazy (t : term) : term :=
+    match t with
+    | tRel _ => t
+    | tEvar _ _ => t
+    | tLambda na M => tLambda na (remove_head_lazy M)
+    | tApp u v => tApp (remove_head_lazy u) v
+    | tLetIn na b b' => tLetIn na b (remove_head_lazy b')
+    | tCase ind c brs => tCase ind c (List.map (on_snd remove_head_lazy) brs)
+    | tProj _ _ => t
+    | tFix _ _  => t
+    | tCoFix _ _ => t
+    | tBox => t
+    | tVar _ => t
+    | tConst _ => t
+    | tConstruct _ _ _ => t
+    | tPrim _ => t
+    | tLazy t => t
+    | tForce _ => t
+    end.
+
+  Definition hoist_head_lazy (t : term) :=
+    tLazy (remove_head_lazy t).
+
   Fixpoint trans (t : term) : term :=
     match t with
     | tRel i => tRel i
@@ -60,6 +83,7 @@ Section trans.
       tFix mfix' idx
     | tCoFix mfix idx =>
       let mfix' := List.map (map_def trans) mfix in
+      let mfix' := List.map (map_def hoist_head_lazy) mfix' in
       tFix mfix' idx
     | tBox => t
     | tVar _ => t
@@ -127,6 +151,7 @@ Section trans.
     - move/andP: H => [] clt clargs.
       destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; rtoProp; solve_all; solve_all.
     - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; rtoProp; solve_all; solve_all.
+    - apply trust_cofix.
     - primProp. solve_all_k 6.
   Qed.
 
@@ -185,6 +210,9 @@ Section trans.
     - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //.
       all:f_equal; eauto; try (rewrite /on_snd map_map_compose; solve_all).
       f_equal; eauto.
+    - f_equal; eauto. solve_all_k 6.
+      unfold map_def; f_equal; cbn. unfold hoist_head_lazy. f_equal.
+      apply trust_cofix.
   Qed.
 
   Lemma trans_substl s t :
@@ -851,7 +879,7 @@ Proof.
     now constructor.
     constructor; eauto; solve_all.
   - cbn. econstructor; eauto. solve_all. now eapply isLambda_trans.
-  - cbn. econstructor; eauto; solve_all. apply trust_cofix.
+  - cbn. rewrite map_map_compose. apply trust_cofix.
   - cbn -[GlobalContextMap.lookup_inductive_kind].
     rewrite GlobalContextMap.lookup_inductive_kind_spec.
     destruct lookup_inductive_kind as [[]|] => /= //.

make-opam-files.sh

@@ -6,16 +6,33 @@ then
     exit 0
 fi
 
+archive=`basename $3`
+tag=${archive/.tar.gz/}
+
 echo "Target directory: " $1
 echo "Target version: " $2
 echo "Releases package: " $3
+echo "Archive:" $archive
+echo "Tag:" $tag
+
+if [ -f $archive ]
+then
+    echo "Removing existing archive!"
+    rm $archive
+fi
 
 wget $3
-archive=`basename $3`
+
 hash=`shasum -a 512 $archive | cut -f 1 -d " "`
 
 echo "Shasum = " $hash
 
+echo "Uploading to release assets"
+
+gh release upload $tag $archive
+
+release=https://github.com/MetaCoq/metacoq/releases/download/$tag/$archive
+
 for f in *.opam;
 do
     opamf=${f/.opam/};
@@ -24,7 +41,7 @@ do
     mkdir -p $1/$opamf/$opamf.$2
     gsed -e "/^version:.*/d" $f > $target
     echo url { >> $target
-    echo "  src:" \"$3\" >> $target
+    echo "  src:" \"$release\" >> $target
     echo "  checksum:" \"sha512=$hash\" >> $target
     echo } >> $target
 done

test-suite/erasure_live_test.v

@@ -372,12 +372,13 @@ Print P_provedCopyx.
 From Coq Require Import Streams.
 
 CoFixpoint ones : Stream nat := Cons 1 ones.
-
 MetaCoq Erase ones.
 MetaCoq Erase -unsafe ones.
-
 MetaCoq Erase -typed -time -unsafe (map S ones).
 
+CoFixpoint ones_broken : Stream nat := let t := ones_broken in Cons 1 t.
+MetaCoq Erase ones_broken.
+MetaCoq Erase -unsafe ones_broken.
 
 (* 0.2s purely in the bytecode VM *)
 (*Time Definition P_provedCopyxvm' := Eval vm_compute in (test p_provedCopyx). *)