Option to see constructors as block in EWcbvEval, needed for extracti…

…on in CertiCoq and to OCaml/Malfunction (MetaCoq#716) * constructors as blocks * evaluation rules for constructors as blocks * tranformation to constructors as blocks * correctness proof for constructors as blocks
SwampertX · Jun 25, 2022 · 63906fb · 63906fb
1 parent ffd483d
commit 63906fb
Show file tree

Hide file tree

Showing 27 changed files with 1,708 additions and 429 deletions.
diff --git a/erasure/_CoqProject.in b/erasure/_CoqProject.in
@@ -34,4 +34,5 @@ theories/EProgram.v
 theories/ERemoveParams.v
 theories/EInlineProjections.v
 theories/ETransform.v
+theories/EConstructorsAsBlocks.v
 theories/Erasure.v
diff --git a/erasure/theories/EAst.v b/erasure/theories/EAst.v
@@ -33,7 +33,7 @@ Inductive term : Set :=
 | tLetIn     : name -> term (* the term *) -> term -> term
 | tApp       : term -> term -> term
 | tConst     : kername -> term
-| tConstruct : inductive -> nat -> term
+| tConstruct : inductive -> nat -> list term -> term
 | tCase      : (inductive * nat) (* # of parameters *) ->
                term (* discriminee *) -> list (list name * term) (* branches *) -> term
 | tProj      : projection -> term -> term

diff --git a/erasure/theories/EAstUtils.v b/erasure/theories/EAstUtils.v
@@ -283,7 +283,7 @@ Definition isCoFix t :=
 
 Definition isConstruct t :=
   match t with
-  | tConstruct _ _ => true
+  | tConstruct _ _ _ => true
   | _ => false
   end.
 
@@ -328,6 +328,8 @@ Definition string_of_def {A : Set} (f : A -> string) (def : def A) :=
   "(" ^ string_of_name (dname def) ^ "," ^ f (dbody def) ^ ","
       ^ string_of_nat (rarg def) ^ ")".
 
+Definition maybe_string_of_list {A} f (l : list A) := match l with [] => "" | _ => string_of_list f l end.
+
 Fixpoint string_of_term (t : term) : string :=
   match t with
   | tBox => "∎"
@@ -338,7 +340,7 @@ Fixpoint string_of_term (t : term) : string :=
   | tLetIn na b t => "LetIn(" ^ string_of_name na ^ "," ^ string_of_term b ^ "," ^ string_of_term t ^ ")"
   | tApp f l => "App(" ^ string_of_term f ^ "," ^ string_of_term l ^ ")"
   | tConst c => "Const(" ^ string_of_kername c ^ ")"
-  | tConstruct i n => "Construct(" ^ string_of_inductive i ^ "," ^ string_of_nat n ^ ")"
+  | tConstruct i n args => "Construct(" ^ string_of_inductive i ^ "," ^ string_of_nat n ^ maybe_string_of_list string_of_term args ^ ")"
   | tCase (ind, i) t brs =>
     "Case(" ^ string_of_inductive ind ^ "," ^ string_of_nat i ^ "," ^ string_of_term t ^ ","
             ^ string_of_list (fun b => string_of_term (snd b)) brs ^ ")"
@@ -354,8 +356,10 @@ Fixpoint string_of_term (t : term) : string :=
 
 Fixpoint term_global_deps (t : EAst.term) :=
   match t with
-  | EAst.tConst kn
-  | EAst.tConstruct {| inductive_mind := kn |} _ => KernameSet.singleton kn
+  | EAst.tConst kn => KernameSet.singleton kn
+  | EAst.tConstruct {| inductive_mind := kn |} _ args =>
+     List.fold_left (fun acc x => KernameSet.union (term_global_deps x) acc) args
+          (KernameSet.singleton kn)
   | EAst.tLambda _ x => term_global_deps x
   | EAst.tApp x y
   | EAst.tLetIn _ x y => KernameSet.union (term_global_deps x) (term_global_deps y)

diff --git a/erasure/theories/ECSubst.v b/erasure/theories/ECSubst.v
@@ -36,6 +36,7 @@ Fixpoint csubst t k u :=
     let k' := List.length mfix + k in
     let mfix' := List.map (map_def (csubst t k')) mfix in
     tCoFix mfix' idx
+  | tConstruct ind n args => tConstruct ind n (map (csubst t k) args)
   | x => x
   end.
 
@@ -57,7 +58,7 @@ Proof.
       destruct (nth_error_spec [t] (n - k) ).
       simpl in l0; lia.
       now rewrite Nat.sub_1_r.
-    + now destruct (Nat.leb_spec k n); try lia.  
+    + now destruct (Nat.leb_spec k n); try lia.
 Qed.
 
 Lemma substl_subst s u : forallb (closedn 0) s ->