Adapt erasure for primitive arrays

Author: mattam82

.vscode/metacoq.code-workspace

@@ -11,27 +11,28 @@
 
 
 
-			"-R", "safechecker-plugin/theories,MetaCoq.SafeCheckerPlugin",
 
-			"-R", "utils/theories,MetaCoq.Utils",
-			"-R", "common/theories,MetaCoq.Common",
-			"-R", "template-pcuic/theories,MetaCoq.TemplatePCUIC",
+			"-R", "safechecker-plugin/theories","MetaCoq.SafeCheckerPlugin",
 
-		"-I template-coq",
+			"-R", "utils/theories","MetaCoq.Utils",
+			"-R", "common/theories","MetaCoq.Common",
+			"-R", "template-pcuic/theories","MetaCoq.TemplatePCUIC",
+
+		"-I", "template-coq",
     	//	"-bt", get backtraces from Coq on errors
-		"-I template-coq/build",
-		"-R", "template-coq/theories,MetaCoq.Template",
-		"-R", "examples,MetaCoq.Examples",
-		"-R", "checker/theories,MetaCoq.Checker",
-		"-R", "pcuic/theories,MetaCoq.PCUIC",
-		"-I safechecker/src",
-		"-R", "safechecker/theories,MetaCoq.SafeChecker",
-		"-I erasure/src",
-		"-R", "erasure/theories,MetaCoq.Erasure",
-		"-R", "erasure-plugin/theories,MetaCoq.ErasurePlugin",
-		"-R", "translations,MetaCoq.Translations",
-		"-R", "test-suite/plugin-demo/theories,MetaCoq.ExtractedPluginDemo",
-		"-R", "test-suite,MetaCoq.TestSuite"
+		"-I", "template-coq/build",
+		"-R", "template-coq/theories", "MetaCoq.Template",
+		"-R", "examples", "MetaCoq.Examples",
+		"-R", "checker/theories" "MetaCoq.Checker",
+		"-R", "pcuic/theories","MetaCoq.PCUIC",
+		"-I", "safechecker/src",
+		"-R", "safechecker/theories","MetaCoq.SafeChecker",
+		"-I", "erasure/src",
+		"-R", "erasure/theories","MetaCoq.Erasure",
+		"-R", "erasure-plugin/theories","MetaCoq.ErasurePlugin",
+		"-R", "translations","MetaCoq.Translations",
+		"-R", "test-suite/plugin-demo/theories","MetaCoq.ExtractedPluginDemo",
+		"-R", "test-suite","MetaCoq.TestSuite"
 	    ],
 
 	 // When enabled, will trim trailing whitespace when saving a file.

erasure-plugin/_PluginProject.in

@@ -50,6 +50,8 @@ src/pCUICSafeReduce.ml
 src/pCUICSafeRetyping.ml
 src/pCUICSafeRetyping.mli
 
+src/ePrimitive.mli
+src/ePrimitive.ml
 src/eAst.ml
 src/eAst.mli
 src/eAstUtils.ml

erasure-plugin/src/metacoq_erasure_plugin.mlpack

@@ -39,6 +39,7 @@ PCUICUnivSubst
 PCUICSafeReduce
 PCUICSafeRetyping
 
+EPrimitive
 EAst
 EAstUtils
 ELiftSubst

erasure/theories/EAstUtils.v

@@ -2,7 +2,7 @@
 From Equations Require Import Equations.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import BasicAst Kernames.
-From MetaCoq.Erasure Require Import EAst.
+From MetaCoq.Erasure Require Import EPrimitive EAst.
 Require Import ssreflect ssrbool.
 
 Global Hint Resolve app_tip_nil : core.
@@ -378,24 +378,36 @@ Fixpoint string_of_term (t : term) : string :=
 
 (** Compute all the global environment dependencies of the term *)
 
-Fixpoint term_global_deps (t : EAst.term) :=
+Section PrimDeps.
+  Context (deps : term -> KernameSet.t).
+
+  Equations prim_global_deps (p : prim_val term) : KernameSet.t :=
+   | (primInt; primIntModel i) => KernameSet.empty
+   | (primFloat; primFloatModel f) => KernameSet.empty
+   | (primArray; primArrayModel a) =>
+      List.fold_left (fun acc x => KernameSet.union (deps x) acc) a.(array_value) (deps a.(array_default)).
+
+End PrimDeps.
+
+Fixpoint term_global_deps (t : term) :=
   match t with
-  | EAst.tConst kn => KernameSet.singleton kn
-  | EAst.tConstruct {| inductive_mind := kn |} _ args =>
+  | tConst kn => KernameSet.singleton kn
+  | 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)
-  | EAst.tCase (ind, _) x brs =>
+  | tLambda _ x => term_global_deps x
+  | tApp x y
+  | tLetIn _ x y => KernameSet.union (term_global_deps x) (term_global_deps y)
+  | tCase (ind, _) x brs =>
     KernameSet.union (KernameSet.singleton (inductive_mind ind))
       (List.fold_left (fun acc x => KernameSet.union (term_global_deps (snd x)) acc) brs
         (term_global_deps x))
-   | EAst.tFix mfix _ | EAst.tCoFix mfix _ =>
-     List.fold_left (fun acc x => KernameSet.union (term_global_deps (EAst.dbody x)) acc) mfix
+   | tFix mfix _ | tCoFix mfix _ =>
+     List.fold_left (fun acc x => KernameSet.union (term_global_deps (dbody x)) acc) mfix
       KernameSet.empty
-  | EAst.tProj p c =>
+  | tProj p c =>
     KernameSet.union (KernameSet.singleton (inductive_mind p.(proj_ind)))
       (term_global_deps c)
+  | tPrim p => prim_global_deps term_global_deps p
   | _ => KernameSet.empty
   end.

erasure/theories/EConstructorsAsBlocks.v

@@ -2,7 +2,7 @@
 From Coq Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames BasicAst EnvMap.
-From MetaCoq.Erasure Require Import EAst EAstUtils EInduction EArities
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EArities
     ELiftSubst ESpineView EGlobalEnv EWellformed EEnvMap
     EWcbvEval EEtaExpanded ECSubst EWcbvEvalEtaInd EProgram.
 
@@ -62,7 +62,7 @@ Section transform_blocks.
     | tVar n => EAst.tVar n
     | tConst n => EAst.tConst n
     | tConstruct ind i block_args => EAst.tConstruct ind i []
-    | tPrim p => EAst.tPrim p }.
+    | tPrim p => EAst.tPrim (map_primIn p (fun x H => transform_blocks x)) }.
   Proof.
     all:try lia.
     all:try apply (In_size); tea.
@@ -82,6 +82,7 @@ Section transform_blocks.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in *. lia.
+    - now eapply InPrim_size in H.
   Qed.
 
   End Def.
@@ -116,6 +117,7 @@ Section transform_blocks.
     unfold test_def in *;
     simpl closed in *;
     try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy.
+    - solve_all_k 6.
     - rewrite !closedn_mkApps in H1 *.
       rtoProp; intuition auto. solve_all.
     - destruct (chop nargs v) eqn:E.
@@ -714,6 +716,7 @@ Proof.
     cbn -[transform_blocks isEtaExp] in *. rtoProp. eauto.
   - unfold wf_fix in *. len. solve_all. rtoProp; intuition auto.
     solve_all.
+  - solve_all_k 7.
   - rewrite !wellformed_mkApps in Hw |- * => //. rtoProp.
     eapply isEtaExp_mkApps in H1. rewrite decompose_app_mkApps in H1; eauto.
     destruct construct_viewc; eauto. cbn in d. eauto.

erasure/theories/EDeps.v

@@ -1,9 +1,9 @@
 From Coq Require Import Arith List.
 From Equations Require Import Equations.
 From MetaCoq.PCUIC Require Import
-     PCUICAst PCUICAstUtils PCUICTyping PCUICInversion PCUICWeakeningEnv PCUICWeakeningEnvTyp.
+     PCUICPrimitive PCUICAst PCUICAstUtils PCUICTyping PCUICInversion PCUICWeakeningEnv PCUICWeakeningEnvTyp.
 Set Warnings "-notation-overridden".
-From MetaCoq.Erasure Require Import EAst EAstUtils ECSubst EInduction
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils ECSubst EInduction
   ELiftSubst EGlobalEnv EWcbvEval Extract ESubstitution.
 From MetaCoq.Erasure Require EExtends.
 Set Warnings "+notation-overridden".
@@ -84,6 +84,8 @@ Proof.
     depelim X.
     constructor; [|easy].
     now apply e.
+  - depelim X; depelim er; constructor; cbn. solve_all.
+    destruct p. solve_all.
 Qed.
 
 Lemma erases_deps_subst Σ Σ' s k t :
@@ -134,6 +136,7 @@ Proof.
     depelim X.
     constructor; [|easy].
     now apply e.
+  - depelim X; depelim er; constructor; cbn; intuition auto; solve_all.
 Qed.
 
 Lemma erases_deps_subst1 Σ Σ' t k u :
@@ -191,6 +194,7 @@ Proof.
     depelim X.
     constructor; [|easy].
     now apply e.
+  - depelim X; depelim er; constructor; cbn; intuition auto; solve_all.
 Qed.
 
 Lemma erases_deps_substl Σ Σ' s t :
@@ -402,7 +406,7 @@ Lemma erases_deps_forall_ind Σ Σ'
          Forall (fun d : Extract.E.def Extract.E.term => erases_deps Σ Σ' (Extract.E.dbody d)) defs ->
          Forall (fun d => P (E.dbody d)) defs ->
          P (Extract.E.tCoFix defs i))
-  (Hprim : forall p, P (Extract.E.tPrim p)):
+  (Hprim : forall p, primProp (erases_deps Σ Σ') p -> primProp P p -> P (Extract.E.tPrim p)):
   forall t, erases_deps Σ Σ' t -> P t.
 Proof.
   fix f 2.
@@ -441,6 +445,15 @@ Proof.
     fix f' 2.
     intros defs []; [now constructor|].
     constructor; [now apply f|now apply f'].
+  - eapply Hprim; tea; constructor.
+  - eapply Hprim; tea; constructor.
+  - eapply Hprim; tea; constructor.
+    intuition auto; solve_all.
+    split. auto. destruct a as [d v]. cbn in *.
+    eapply Forall_All.
+    revert v H.
+    fix aux 2.
+    intros ? [];constructor; auto.
 Defined.
 
 (* Lemma fresh_global_erase {cf : checker_flags} Σ Σ' kn :
@@ -559,6 +572,7 @@ Proof.
     rewrite H in declm.
     eapply PCUICWeakeningEnv.lookup_env_Some_fresh in kn_fresh.
     eauto. eauto.
+  - depelim X0; intuition auto; constructor; auto.
 Qed.
 
 Derive Signature for erases_global_decls.
@@ -681,6 +695,8 @@ Proof.
     depelim all_deps.
     destruct p as (?&?&?).
     now constructor; eauto.
+  - eapply inversion_Prim in wt as [prim_ty [decl []]]; eauto.
+    depelim H0; depelim p1; depelim X; cbn in *; try constructor; cbn; intuition eauto. solve_all.
 Qed.
 
 Lemma Forall2_nth_error_left {A B} {P} {l : list A} {l' : list B} : Forall2 P l l' ->

erasure/theories/EEtaExpanded.v

@@ -5,7 +5,7 @@
 From Coq Require Import Utf8 Program.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.Common Require Import config Kernames EnvMap BasicAst.
-From MetaCoq.Erasure Require Import EAst EAstUtils EInduction EGlobalEnv EExtends EWellformed ELiftSubst ESpineView ECSubst EWcbvEval EWcbvEvalInd EProgram.
+From MetaCoq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EGlobalEnv EExtends EWellformed ELiftSubst ESpineView ECSubst EWcbvEval EWcbvEvalInd EProgram.
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
@@ -75,7 +75,7 @@ Section isEtaExp.
     | tBox => true
     | tVar _ => true
     | tConst _ => true
-    | tPrim _ => true
+    | tPrim p => test_primIn p (fun x H => isEtaExp x)
     | tConstruct ind i block_args => isEtaExp_app ind i 0 && is_nil block_args }.
   Proof.
     all:try lia.
@@ -92,11 +92,15 @@ Section isEtaExp.
       change (fun x => size x) with size in H.
       pose proof (size_mkApps_l napp nnil). lia.
     - eapply (In_size snd size) in H. cbn in H; lia.
+    - destruct p as [? []]; cbn in *; intuition eauto.
+      subst. lia.
+      eapply (In_size id size) in H0. unfold id in H0.
+      change (fun x => size x) with size in H0. lia.
   Qed.
 
 End isEtaExp.
 
-Global Hint Rewrite @forallb_InP_spec : isEtaExp.
+Global Hint Rewrite @test_primIn_spec @forallb_InP_spec : isEtaExp.
 Tactic Notation "simp_eta" "in" hyp(H) := simp isEtaExp in H; rewrite -?isEtaExp_equation_1 in H.
 Ltac simp_eta := simp isEtaExp; rewrite -?isEtaExp_equation_1.
 
@@ -276,8 +280,8 @@ Section WeakEtaExp.
       eapply a0 => //.
     - move/andP: H0 => [] etaexp h.
       rewrite csubst_mkApps /=.
-      rewrite isEtaExp_Constructor. solve_all.
-      rewrite map_length. rtoProp; solve_all. solve_all.
+      rewrite isEtaExp_Constructor; solve_all.
+      rtoProp; solve_all. solve_all.
       now destruct block_args.
     - rewrite csubst_mkApps /=.
       move/andP: H1 => [] eu ev.
@@ -417,6 +421,7 @@ Proof.
   - eapply In_All in H; solve_all.
     move/andP: b => [] -> /=. eauto.
   - eapply In_All in H; solve_all.
+  - solve_all.
   - eapply In_All in H; solve_all.
     rewrite isEtaExp_Constructor //. rtoProp; intuition auto.
     eapply isEtaExp_app_extends; tea.
@@ -471,7 +476,7 @@ Inductive expanded : term -> Prop :=
     #|args| >= cstr_arity mind cdecl ->
     Forall expanded args ->
     expanded (mkApps (tConstruct ind idx []) args)
-| expanded_tPrim p : expanded (tPrim p)
+| expanded_tPrim p : primProp expanded p -> expanded (tPrim p)
 | expanded_tBox : expanded tBox.
 
 End expanded.
@@ -510,7 +515,7 @@ forall (Σ : global_declarations) (P : term -> Prop),
    (args : list term),
  declared_constructor Σ (ind, idx) mind idecl cdecl ->
  #|args| >= cstr_arity mind cdecl -> Forall (expanded Σ) args -> Forall P args -> P (mkApps (tConstruct ind idx []) args)) ->
-(forall p, P (tPrim p)) ->
+(forall p, primProp (expanded Σ) p -> primProp P p -> P (tPrim p)) ->
 (P tBox) ->
 forall t : term, expanded Σ t -> P t.
 Proof.
@@ -523,6 +528,9 @@ Proof.
   - eapply H8; eauto. induction H13; econstructor; cbn in *; intuition eauto.
   - eapply H9; eauto. induction H13; econstructor; cbn in *; eauto.
   - eapply H10; eauto. clear - H15 f. induction H15; econstructor; cbn in *; eauto.
+  - eapply H11; eauto.
+    depelim X; constructor. destruct p; split; eauto.
+    eapply (make_All_All f a0).
 Qed.
 
 Local Hint Constructors expanded : core.
@@ -595,6 +603,7 @@ Proof.
     intuition auto.
   - econstructor. rewrite forallb_InP_spec in H0. eapply forallb_Forall in H0.
     eapply In_All in H. solve_all.
+  - econstructor. rewrite test_primIn_spec in H0. solve_all.
   - rtoProp. eapply In_All in H.
     rewrite forallb_InP_spec in H2. eapply forallb_Forall in H2.
     eapply isEtaExp_app_expanded in H0 as (? & ? & ? & ? & ?).
@@ -621,6 +630,7 @@ Proof.
   - rewrite isEtaExp_Constructor. rtoProp; repeat split.
     2: eapply forallb_Forall.
     2: solve_all. eapply expanded_isEtaExp_app_; eauto.
+  - solve_all.
 Qed.
 
 Lemma expanded_global_env_isEtaExp_env {Σ} : expanded_global_env Σ -> isEtaExp_env Σ.
@@ -695,6 +705,7 @@ Proof.
   - simp_eta. rtoProp; intuition auto.
     eapply In_All in H0; solve_all.
   - eapply In_All in H. simp_eta; rtoProp; intuition auto. solve_all.
+  - simp_eta. solve_all_k 7. primProp. solve_all.
   - eapply In_All in H. simp_eta; rtoProp; intuition auto.
     rewrite EEtaExpanded.isEtaExp_Constructor. rtoProp; repeat split. eauto.
     solve_all. destruct block_args; cbn in *; eauto.