Merge pull request #663 from MetaCoq/bytestring

Bytestrings

(cherry picked from commit a4854ff)

.gitignore

@@ -475,3 +475,5 @@ erasure/src/envMap.ml
 erasure/src/envMap.mli
 erasure/src/eEtaExpanded.ml
 erasure/src/eEtaExpanded.mli
+erasure/src/pCUICEqualityDec.ml
+erasure/src/pCUICEqualityDec.mli

TODO.md

@@ -1,9 +1,12 @@
+# Performance
+
+- change eq_kername to use comparison rather than eq_dec, check we're not using 
+  eq_dec unnecessarily so that erasure/typechecking runs faster inside Coq 
+  (and we avoid useless sumbool to bool conversions in ML/extracted code)
 # Small stuffs
 
 - `assumption_context` should be a boolean function.
 
-- remove duplication of eq_context / eq_context_upto  and eq_decl / eq_decl_upto
-
 - Make `wf Σ` `wf_ext Σ` some typeclasses (as at the begining of PCUICCanonicity)
   et changer les : wf Σ -> en {wfΣ : wf Σ} partout, ce qui éviterait bien des
   conditions de bord triviales

erasure/_PluginProject.in

@@ -5,22 +5,6 @@ src/META.coq-metacoq-erasure
 # src/classes0.mli
 # src/classes0.ml
 
-# From Coq's stdlib
-src/orderedTypeAlt.mli
-src/orderedTypeAlt.ml
-src/orderedType0.mli
-src/orderedType0.ml
-src/fMapList.mli
-src/fMapList.ml
-src/decidableType.mli
-src/decidableType.ml
-src/fMapInterface.mli
-src/fMapInterface.ml
-src/fMapAVL.mli
-src/fMapAVL.ml
-src/fMapFacts.mli
-src/fMapFacts.ml
-
 # src/string2pos.mli
 # src/string2pos.ml
 # src/canonicalTries.mli
@@ -31,8 +15,6 @@ src/uGraph0.ml
 src/uGraph0.mli
 src/wGraph.ml
 src/wGraph.mli
-src/kernames.mli
-src/kernames.ml
 src/envMap.mli
 src/envMap.ml
 

erasure/src/g_metacoq_erasure.mlg

@@ -23,11 +23,11 @@ let bytes_of_list l =
 
 let pr_char_list l =
   (* We allow utf8 encoding *)
-  str (Bytes.to_string (bytes_of_list l))
+  str (Caml_bytestring.caml_string_of_bytestring l)
 
 let check ~bypass ~fast env evm c =
   debug (fun () -> str"Quoting");
-  let term = time (str"Quoting") (Ast_quoter.quote_term_rec bypass env) (EConstr.to_constr evm c) in
+  let term = time (str"Quoting") (Ast_quoter.quote_term_rec ~bypass env) (EConstr.to_constr evm c) in
   let checker_flags = Config0.extraction_checker_flags in
   let erase = time (str"Erasure")
       (if fast then Erasure.erase_fast_and_print_template_program checker_flags

erasure/src/metacoq_erasure_plugin.mlpack

@@ -5,14 +5,6 @@ Utils
 
 WGraph
 UGraph0
-OrderedTypeAlt
-OrderedType0
-Kernames
-FMapList
-DecidableType
-FMapInterface
-FMapAVL
-FMapFacts
 EnvMap
 
 WcbvEval

erasure/theories/EDeps.v

@@ -461,24 +461,21 @@ Proof.
   apply PCUICWeakeningEnvConv.lookup_env_Some_fresh in H as not_fresh.
   econstructor.
   - unfold PCUICAst.declared_constant in *; cbn.
-    unfold eq_kername.
     inversion wfΣ; subst.
-    destruct kername_eq_dec as [<-|]; [congruence|].
+    destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
     eassumption.
-  - unfold ETyping.declared_constant in *. cbn -[Reflect.eqb].
+  - unfold ETyping.declared_constant in *. cbn -[ReflectEq.eqb].
     inversion wfΣ; subst.
-    change (eq_kername kn0 kn) with (Reflect.eqb kn0 kn).
-    destruct (Reflect.eqb_spec kn0 kn); [congruence|].
+    destruct (ReflectEq.eqb_spec kn0 kn); [congruence|].
     eassumption.
   - unfold erases_constant_body in *.
     destruct PCUICAst.PCUICEnvironment.cst_body eqn:body.
     + destruct E.cst_body eqn:ebody; [|easy].
       assert (PCUICAst.declared_constant (add_global_decl Σ (kn, decl)) kn0 cb).
       { unfold PCUICAst.declared_constant.
         cbn.
-        unfold eq_kername.
         inversion wfΣ; subst.
-        destruct kername_eq_dec as [<-|]; [congruence|].
+        destruct (eqb_spec kn0 kn) as [<-|]; [congruence|].
         easy. }
       inversion wfΣ; subst.
       eapply declared_constant_inv in H4; eauto.
@@ -503,37 +500,37 @@ Proof.
     invs wfΣ.
     destruct H0. split. 2: eauto.
     destruct d. split; eauto.
-    red. cbn. unfold eq_kername. destruct kername_eq_dec; eauto.
+    red. cbn. cbn in *.
+    destruct (eqb_spec (inductive_mind ind) kn). cbn in *.
     subst. 
-    eapply PCUICWeakeningEnvConv.lookup_env_Some_fresh in H5. eauto. eapply H.
+    eapply PCUICWeakeningEnvConv.lookup_env_Some_fresh in H5. eauto. eapply H. exact H0.
   - econstructor; eauto.
     destruct H as [H H'].
     split; eauto. red in H |- *.
     inv wfΣ.
     unfold PCUICEnvironment.lookup_env.
-    simpl. unfold eq_kername.
-    destruct (kername_eq_dec (inductive_mind p.1) kn); auto. subst.
+    simpl. destruct (eqb_spec (inductive_mind p.1) kn); auto. subst.
     eapply PCUICWeakeningEnvConv.lookup_env_Some_fresh in H; eauto. contradiction.
     destruct H0 as [H0 H0'].
     split; eauto. red in H0 |- *.
-    inv wfΣ. cbn. change (eq_kername (inductive_mind p.1) kn) with (Reflect.eqb (inductive_mind p.1) kn).    
-    destruct (Reflect.eqb_spec (inductive_mind p.1) kn); auto. subst.
+    inv wfΣ. cbn. change (eq_kername (inductive_mind p.1) kn) with (ReflectEq.eqb (inductive_mind p.1) kn).    
+    destruct (ReflectEq.eqb_spec (inductive_mind p.1) kn); auto. subst.
     destruct H as [H _].
     eapply PCUICWeakeningEnvConv.lookup_env_Some_fresh in H. eauto. contradiction.
   - econstructor; eauto.
     destruct H as [H H'].
     split; eauto. red in H |- *.
     inv wfΣ. unfold PCUICEnvironment.lookup_env.
     simpl.
-    change (eq_kername (inductive_mind p.1.1) kn) with (Reflect.eqb (inductive_mind p.1.1) kn); auto.
-    destruct (Reflect.eqb_spec (inductive_mind p.1.1) kn). subst.
+    change (eq_kername (inductive_mind p.1.1) kn) with (ReflectEq.eqb (inductive_mind p.1.1) kn); auto.
+    destruct (ReflectEq.eqb_spec (inductive_mind p.1.1) kn). subst.
     eapply PCUICWeakeningEnvConv.lookup_env_Some_fresh in H; eauto. contradiction.
     apply H.
     destruct H0 as [H0 H0'].
     split; eauto. red in H0 |- *.
     inv wfΣ. simpl.
-    change (eq_kername (inductive_mind p.1.1) kn) with (Reflect.eqb (inductive_mind p.1.1) kn); auto.
-    destruct (Reflect.eqb_spec (inductive_mind p.1.1) kn); auto. subst.
+    change (eq_kername (inductive_mind p.1.1) kn) with (ReflectEq.eqb (inductive_mind p.1.1) kn); auto.
+    destruct (ReflectEq.eqb_spec (inductive_mind p.1.1) kn); auto. subst.
     destruct H as [H _].
     eapply PCUICWeakeningEnvConv.lookup_env_Some_fresh in H. eauto. contradiction.
 Qed.
@@ -716,14 +713,13 @@ Proof.
       apply IH in erg'. 2:{ depelim wf. now depelim o0. }
       assert (decl_ext: PCUICAst.declared_constant Σu kn' cst').
       { unfold PCUICAst.declared_constant in *; cbn in *.
-        unfold eq_kername in *.
-        now destruct kername_eq_dec; [|congruence]. }
+        destruct (eqb_spec kn' kn); [|congruence]. subst. contradiction. }
       specialize (proj1 erg' kn' cst' decl_ext) as (cst & decl'' & ? & ?).
       exists cst.
       split; [|split].
       * unfold declared_constant in *; cbn. rewrite decl''.
-        change (eq_kername kn' kn) with (Reflect.eqb kn' kn).
-        destruct (Reflect.eqb_spec kn' kn); auto. congruence.
+        change (eq_kername kn' kn) with (ReflectEq.eqb kn' kn).
+        destruct (ReflectEq.eqb_spec kn' kn); auto. congruence.
       * inversion wf; subst.
         eapply declared_constant_inv in decl_ext; eauto.
         2: exact weaken_env_prop_typing.
@@ -745,14 +741,13 @@ Proof.
       destruct decli as [decli ?]. split; auto.
       red in decli |- *. simpl in decli |- *.
       unfold PCUICEnvironment.lookup_env in decli |- *. simpl in *.
-      unfold eq_kername in decli |- *.
-      destruct kername_eq_dec. subst. discriminate. auto.
+      destruct (eqb_spec (inductive_mind k) kn).  subst. discriminate. auto.
       destruct IH as [mdecl' [idecl' [decli' er]]].
       exists mdecl', idecl'. split; auto.
       red. destruct decli'; split; auto.
       red in decli.
       unfold declared_minductive in *.
-      simpl. unfold eq_kername. destruct kername_eq_dec; subst; auto.
+      simpl. destruct (eqb_spec (inductive_mind k) kn); subst; auto.
       unfold PCUICAst.declared_minductive in decli.
       unfold PCUICEnvironment.lookup_env in decli.
       simpl in decli. rewrite eq_kername_refl in decli. intuition discriminate.
@@ -762,16 +757,15 @@ Proof.
       simpl in decli |- *.
       unfold PCUICAst.declared_minductive, PCUICEnvironment.lookup_env in decli.
       simpl in decli.
-      unfold eq_kername in decli |- *. simpl in *.
-      destruct kername_eq_dec. subst. noconf decli.
+      destruct (eqb_specT (inductive_mind k) kn). simpl in *. subst. noconf decli.
       destruct (Forall2_nth_error_left (proj1 H) _ _ H3); eauto.
       eexists _, _; intuition eauto. split; eauto. red.
-      simpl. unfold eq_kername. destruct kername_eq_dec; try congruence.
+      simpl. rewrite eqb_refl. congruence.
       destruct (proj2 IH _ _ _ (conj decli H3)) as [m' [i' [decli' ei]]].
       eexists _, _; intuition eauto.
       destruct decli'; red; split; eauto.
       red in d |- *. simpl.
-      unfold eq_kername; destruct kername_eq_dec; subst; try congruence.
+      apply neqb in n. destruct eqb; cbn in n; try congruence.
 Qed.       
 
 Lemma erases_global_erases_deps Σ Γ t T et Σ' :

erasure/theories/EExtends.v

@@ -18,7 +18,7 @@ Lemma lookup_env_Some_fresh {Σ c decl} :
   lookup_env Σ c = Some decl -> ~ (fresh_global c Σ).
 Proof.
   induction Σ; cbn. 1: congruence.
-  unfold BasicAst.eq_kername. destruct BasicAst.kername_eq_dec; subst.
+  destruct (eqb_spec c a.1); subst.
   - intros [= <-] H2. invs H2.
     contradiction.
   - intros H1 H2. apply IHΣ; tas.
@@ -37,8 +37,8 @@ Proof.
   - specialize (IHΣ'' c decl). forward IHΣ''.
     + now inv wfΣ'.
     + intros HΣ. specialize (IHΣ'' HΣ).
-      inv wfΣ'. simpl in *. unfold BasicAst.eq_kername.
-      destruct BasicAst.kername_eq_dec; subst; auto.
+      inv wfΣ'. simpl in *.
+      destruct (eqb_spec c kn); subst; auto.
       apply lookup_env_Some_fresh in IHΣ''; contradiction.
 Qed.
 

erasure/theories/EOptimizePropDiscr.v

@@ -455,7 +455,7 @@ Lemma lookup_env_optimize Σ kn :
 Proof.
   unfold optimize_env.
   induction Σ at 2 4; simpl; auto.
-  unfold eq_kername; destruct kername_eq_dec => //.
+  case: eqb_spec => //.
 Qed.
 
 Lemma is_propositional_optimize Σ ind :