Add an EPrimitiveFlags to control the presence of ints/floats/arrays

erasure/theories/EImplementBox.v

@@ -672,7 +672,7 @@ Proof.
     rewrite lookup_constructor_implement_box; eauto.
     eapply All2_All2_Set.
     solve_all. now destruct b.
-  - intros H; depelim H; simp implement_box; repeat constructor.
+  - intros wf H; depelim H; simp implement_box; repeat constructor.
     destruct a0. eapply All2_over_undep in a. eapply All2_All2_Set, All2_map.
     cbn -[implement_box]. solve_all. now destruct H. now destruct a0.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].

erasure/theories/EInlineProjections.v

@@ -166,7 +166,7 @@ Section optimize.
     - len. rtoProp; solve_all. solve_all.
       now eapply isLambda_optimize. solve_all.
     - len. rtoProp; repeat solve_all.
-    - rewrite test_prim_map. solve_all.
+    - rewrite test_prim_map. rtoProp; intuition eauto; solve_all.
   Qed.
 
   Lemma optimize_csubst {a k b} n :
@@ -716,11 +716,12 @@ Proof.
         rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         destruct v => /= //.
-  - depelim X; repeat constructor.
+  - intros; rtoProp; intuition eauto.
+    depelim X; repeat constructor.
     eapply All2_over_undep in a.
     eapply All2_Set_All2 in ev. eapply All2_All2_Set. primProp.
-    subst a0 a'; cbn in *. depelim H; cbn in *. intuition auto; solve_all.
-    primProp; depelim H; intuition eauto.
+    subst a0 a'; cbn in *. depelim H0; cbn in *. intuition auto; solve_all.
+    primProp; depelim H0; intuition eauto.
   - destruct t => //.
     all:constructor; eauto.
     cbn [atom optimize] in i |- *.

erasure/theories/EWcbvEval.v

@@ -1745,6 +1745,7 @@ Proof.
     eapply All2_over_impl in iha; tea.
     intuition auto.
     depelim a => //.
+  - depelim X; solve_all.
   - depelim X; solve_all.
     eapply All2_over_undep in a. subst a0 a'; depelim Hc'; constructor; cbn in *; solve_all.
     solve_all.

erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v

@@ -42,7 +42,7 @@ Section OnSubterm.
   | on_proj p c : has_tProj -> Q n c -> on_subterms Q n (tProj p c)
   | on_fix mfix idx : has_tFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tFix mfix idx)
   | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx)
-  | on_prim p : has_tPrim -> primProp (Q n) p -> on_subterms Q n (tPrim p).
+  | on_prim p : has_prim p -> primProp (Q n) p -> on_subterms Q n (tPrim p).
   Derive Signature for on_subterms.
 End OnSubterm.
 

erasure/theories/EWcbvEvalCstrsAsBlocksInd.v

@@ -42,7 +42,7 @@ Section OnSubterm.
   | on_proj p c : has_tProj -> Q n c -> on_subterms Q n (tProj p c)
   | on_fix mfix idx : has_tFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tFix mfix idx)
   | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx)
-  | on_prim p : has_tPrim -> primProp (Q n) p -> on_subterms Q n (tPrim p).
+  | on_prim p : has_prim p -> primProp (Q n) p -> on_subterms Q n (tPrim p).
   Derive Signature for on_subterms.
 End OnSubterm.
 
@@ -307,6 +307,7 @@ Lemma eval_preserve_mkApps_ind :
     P' (tConstruct ind i args) (tConstruct ind i args')) →
 
     (forall p p' (ev : eval_primitive (eval Σ) p p'),
+    Q 0 (tPrim p) ->
     eval_primitive_ind _ (fun x y _ => P x y) _ _ ev ->
     P' (tPrim p) (tPrim p')) ->
 

erasure/theories/EWcbvEvalEtaInd.v

@@ -42,7 +42,7 @@ Section OnSubterm.
   | on_proj p c : has_tProj -> Q n c -> on_subterms Q n (tProj p c)
   | on_fix mfix idx : has_tFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tFix mfix idx)
   | on_cofix mfix idx : has_tCoFix -> All (fun d => Q (#|mfix| + n) d.(dbody)) mfix -> on_subterms Q n (tCoFix mfix idx)
-  | on_prim p : has_tPrim -> primProp (Q n) p -> on_subterms Q n (tPrim p).
+  | on_prim p : has_prim p -> primProp (Q n) p -> on_subterms Q n (tPrim p).
   Derive Signature for on_subterms.
 End OnSubterm.
 
@@ -727,7 +727,7 @@ Definition term_flags :=
     has_tProj := false;
     has_tFix := true;
     has_tCoFix := false;
-    has_tPrim := true
+    has_tPrim := all_primitive_flags;
   |}.
 
 Definition env_flags :=

erasure/theories/EWcbvEvalNamed.v

@@ -917,7 +917,7 @@ Definition extraction_term_flags :=
   ; has_tProj := false
   ; has_tFix := true
   ; has_tCoFix := false
-  ; has_tPrim := true
+  ; has_tPrim := all_primitive_flags
   |}.
 
 Definition extraction_env_flags :=
@@ -962,7 +962,7 @@ Definition named_extraction_term_flags :=
   ; has_tProj := false
   ; has_tFix := true
   ; has_tCoFix := false
-  ; has_tPrim := true
+  ; has_tPrim := all_primitive_flags
   |}.
 
 Definition named_extraction_env_flags :=
@@ -1041,7 +1041,7 @@ Proof.
       - econstructor.
       - invs H1. cbn. destruct a; cbn. destruct dname; cbn; econstructor; eauto.
     }
-  - solve_all. eapply primProp_map. solve_all.
+  - repeat solve_all.
 Qed.
 
 Lemma wellformed_annotate Σ Γ s :
@@ -1093,7 +1093,7 @@ Proof.
       - econstructor.
       - cbn. destruct x; cbn. destruct dname; cbn; econstructor; eauto.
     }
-  - constructor; solve_all. depelim H; cbn; solve_all; try econstructor.
+  - constructor; solve_all. depelim H1; cbn; solve_all; try econstructor.
     destruct a; constructor; solve_all. eapply All2_All2_Set. solve_all.
 Qed.
 

erasure/theories/EWellformed.v

@@ -1,7 +1,7 @@
 (* Distributed under the terms of the MIT license. *)
 From Coq Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
-From MetaCoq.Common Require Import config Kernames.
+From MetaCoq.Common Require Import config Kernames Primitive.
 From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils ELiftSubst ECSubst EGlobalEnv.
 From MetaCoq.PCUIC Require Import PCUICTactics.
 
@@ -20,6 +20,18 @@ Definition isSome {A} (o : option A) :=
   | Some _ => true
   end.
 
+Class EPrimitiveFlags :=
+  { has_primint : bool;
+    has_primfloat : bool;
+    has_primarray : bool }.
+
+Definition has_prim {epfl : EPrimitiveFlags} (p : prim_val term) :=
+  match p.π1 with
+  | primInt => has_primint
+  | primFloat => has_primfloat
+  | primArray => has_primarray
+  end.
+
 Class ETermFlags :=
   { has_tBox : bool
   ; has_tRel : bool
@@ -34,17 +46,24 @@ Class ETermFlags :=
   ; has_tProj : bool
   ; has_tFix : bool
   ; has_tCoFix : bool
-  ; has_tPrim : bool
+  ; has_tPrim :: EPrimitiveFlags
   }.
 
-Set Warnings "-future-coercion-class-field".
 Class EEnvFlags := {
   has_axioms : bool;
   has_cstr_params : bool;
-  term_switches :> ETermFlags ;
+  term_switches :: ETermFlags ;
   cstr_as_blocks : bool ;
   }.
-Set Warnings "+future-coercion-class-field".
+
+Definition all_primitive_flags :=
+  {| has_primint := true;
+     has_primfloat := true;
+     has_primarray := true |}.
+
+Lemma has_prim_all_primitive_flags p : @has_prim all_primitive_flags p.
+Proof. destruct p as [? []]; auto. Qed.
+#[global] Hint Resolve has_prim_all_primitive_flags : core.
 
 Definition all_term_flags :=
   {| has_tBox := true
@@ -60,7 +79,7 @@ Definition all_term_flags :=
     ; has_tProj := true
     ; has_tFix := true
     ; has_tCoFix := true
-    ; has_tPrim := true
+    ; has_tPrim := all_primitive_flags
   |}.
 
 Definition all_env_flags :=
@@ -119,11 +138,17 @@ Section wf.
         | _ => true end
         && forallb (wellformed k) block_args else is_nil block_args
     | tVar _ => has_tVar
-    | tPrim p => has_tPrim && test_prim (wellformed k) p
+    | tPrim p => has_prim p && test_prim (wellformed k) p
     end.
 
 End wf.
 
+Lemma has_prim_map_prim {efl : EEnvFlags} f p : has_prim (map_prim f p) = has_prim p.
+Proof.
+  destruct p as [? []]; cbn; auto.
+Qed.
+#[global] Hint Rewrite @has_prim_map_prim : map.
+
 Notation wf_fix Σ := (wf_fix_gen (wellformed Σ)).
 
 Lemma wf_fix_inv {efl : EEnvFlags} Σ k mfix idx : reflect (idx < #|mfix| /\ forallb (test_def (wellformed Σ (#|mfix| + k))) mfix) (wf_fix Σ k mfix idx).

erasure/theories/ErasureFunctionProperties.v

@@ -1456,7 +1456,7 @@ Proof.
     * move/andP: H6; PCUICAstUtils.solve_all.
   - cbn -[lookup_projection] in *. apply/andP; split; eauto.
     now rewrite (declared_projection_lookup H0).
-  - cbn in H, H0 |- *. solve_all_k 7.
+  - cbn in H, H0 |- *. rtoProp; intuition eauto. solve_all_k 7.
 Qed.
 
 Lemma erases_wf_fixpoints Σ Γ t t' : Σ;;; Γ |- t ⇝ℇ t' ->

erasure/theories/ErasureProperties.v

@@ -671,8 +671,6 @@ Proof.
     depelim X0; depelim X1; repeat constructor; cbn; intuition eauto. solve_all.
 Qed.
 
-
-
 Lemma eval_empty_brs {wfl : Ee.WcbvFlags} Σ ci p e : Σ ⊢ E.tCase ci p [] ⇓ e -> False.
 Proof.
   intros He.