WarblreEquiv: don't generate a Union with CdEmpty for each Class Ranges

WarblreEquiv/CharDescrCharSet.v

@@ -46,6 +46,27 @@ Section CharDescrCharSet.
         rewrite CharSet.exist_iff. exists c0. auto.
   Qed.
 
+  (* Correctness of simplifying the union with empty *)
+  Lemma equiv_cd_union_emp:
+    forall cd1 cd2 s1 s2,
+      equiv_cd_charset cd1 s1 -> equiv_cd_charset cd2 s2 ->
+      equiv_cd_charset (union_emp_r cd1 cd2) (CharSet.union s1 s2).
+  Proof.
+    intros cd1 cd2 s1 s2 EQ1 EQ2. destruct cd2; simpl; try apply equiv_cd_union; auto.
+    unfold equiv_cd_charset in *. intros c. specialize (EQ1 c). rewrite EQ1.
+    rewrite !CharSet.exist_canonicalized_equiv in *.
+    unfold char_match, char_match' in EQ2.
+    symmetry. destruct (CharSet.exist s1) eqn:EX.
+    - rewrite CharSet.exist_iff in *. destruct EX as [c1 [CONT CAN]]. exists c1. split; auto.
+      rewrite CharSet.union_contains. setoid_rewrite Bool.orb_true_iff. left. auto.
+    - symmetry in EQ2. rewrite CharSet.exist_false_iff in *. intros c1. specialize (EX c1) as [CONT|CAN].
+      + left. rewrite CharSet.union_contains. setoid_rewrite Bool.orb_false_iff. split; auto.
+        specialize (EQ2 c1). rewrite CharSet.exist_canonicalized_equiv in EQ2.
+        rewrite CharSet.exist_false_iff in EQ2. specialize (EQ2 c1). destruct EQ2; auto.
+        rewrite EqDec.reflb in H. inversion H.
+      + right; auto.
+  Qed.
+
   (* Lemmas for various character descriptors *)
   Lemma equiv_cd_empty:
     equiv_cd_charset CdEmpty CharSet.empty.
@@ -235,7 +256,9 @@ Section CharDescrCharSet.
     - simpl. pose proof equiv_cd_ClassAtom ca cacd Hequiv' as [A [HeqA Hequivatom]].
       rewrite HeqA. simpl.
       destruct IH as [B [HeqB IH]]. rewrite HeqB. simpl.
-      unfold Coercions.Coercions.wrap_CharSet. eexists. split. + reflexivity. + now apply equiv_cd_union.
+      unfold Coercions.Coercions.wrap_CharSet. eexists. split.
+      + reflexivity.
+      + now apply equiv_cd_union_emp.
     - simpl.
       rewrite equiv_ClassAtom_single_charset with (c := cl) by auto.
       rewrite equiv_ClassAtom_single_charset with (c := ch) by auto.
@@ -246,6 +269,6 @@ Section CharDescrCharSet.
       pose proof Hl_le_h as Hl_le_h'. rewrite <- PeanoNat.Nat.leb_le in Hl_le_h'. rewrite Hl_le_h'. simpl.
       unfold Coercions.Coercions.wrap_CharSet. eexists. split.
       + reflexivity.
-      + apply equiv_cd_union; auto. do 2 rewrite Character.numeric_pseudo_bij. apply equiv_cd_range. assumption.
+      + apply equiv_cd_union_emp; auto. do 2 rewrite Character.numeric_pseudo_bij. apply equiv_cd_range. assumption.
   Qed.
 End CharDescrCharSet.

WarblreEquiv/RegexpTranslation.v

@@ -150,15 +150,23 @@ Section RegexpTranslation.
   | Equiv_SourceCharacter: forall c: Parameters.Character, equiv_ClassAtom (Patterns.SourceCharacter c) (CdSingle c)
   | Equiv_ClassEsc: forall esc cd, equiv_ClassEscape esc cd -> equiv_ClassAtom (Patterns.ClassEsc esc) cd.
 
+  (* If we naively translate a list of Patterns.ClassRanges into a CdUnion, we end up with a CdEmpty at the end,
+     corresponding to the EmptyCR (= nil) that terminates the list. We remove the CdEmpty from the generated Union *)
+  Definition union_emp_r (cd1 cd2: char_descr) :=
+    match cd2 with
+    | CdEmpty => cd1
+    | _ => CdUnion cd1 cd2
+    end.
+
   Inductive equiv_ClassRanges: Patterns.ClassRanges -> char_descr -> Prop :=
   | Equiv_EmptyCR: equiv_ClassRanges Patterns.EmptyCR CdEmpty
-  | Equiv_ClassAtomCR: forall ca cacd t tcd, equiv_ClassAtom ca cacd -> equiv_ClassRanges t tcd -> equiv_ClassRanges (Patterns.ClassAtomCR ca t) (CdUnion cacd tcd)
+  | Equiv_ClassAtomCR: forall ca cacd t tcd, equiv_ClassAtom ca cacd -> equiv_ClassRanges t tcd -> equiv_ClassRanges (Patterns.ClassAtomCR ca t) (union_emp_r cacd tcd)
   | Equiv_RangeCR:
     forall l h cl ch t tcd,
       equiv_ClassAtom l (CdSingle cl) -> equiv_ClassAtom h (CdSingle ch) ->
       Character.numeric_value cl <= Character.numeric_value ch ->
       equiv_ClassRanges t tcd ->
-      equiv_ClassRanges (Patterns.RangeCR l h t) (CdUnion (CdRange cl ch) tcd).
+      equiv_ClassRanges (Patterns.RangeCR l h t) (union_emp_r (CdRange cl ch) tcd).
 
   Inductive equiv_CharClass: Patterns.CharClass -> char_descr -> Prop :=
   | Equiv_NoninvertedCC: forall crs cd, equiv_ClassRanges crs cd -> equiv_CharClass (Patterns.NoninvertedCC crs) cd
@@ -520,13 +528,13 @@ Section RegexpTranslation.
       | Patterns.ClassAtomCR ca t =>
           let cda := classAtom_to_linden ca in
           let! cdt =<< classRanges_to_linden t in
-          Success (CdUnion cda cdt)
+          Success (union_emp_r cda cdt)
       | Patterns.RangeCR l h t =>
           let! cl =<< classAtom_singleCharacter_numValue l in
           let! ch =<< classAtom_singleCharacter_numValue h in
           let! cdt =<< classRanges_to_linden t in
           if cl <=? ch then
-            Success (CdUnion (CdRange (Character.from_numeric_value cl) (Character.from_numeric_value ch)) cdt)
+            Success (union_emp_r (CdRange (Character.from_numeric_value cl) (Character.from_numeric_value ch)) cdt)
           else
             Error WlMalformed
       end.
@@ -745,7 +753,12 @@ Section RegexpTranslation.
       - simpl. intros cd H. injection H as <-. constructor.
       - simpl. intro cd.
         destruct classRanges_to_linden as [cdt|] eqn:Hcdt; try discriminate; simpl.
-        intro H. injection H as <-.
+        intro H. injection H as <-. unfold union_emp_r.
+        destruct cdt eqn:CDT.
+        all: try rewrite <- CDT.
+        all: try replace (CdUnion (classAtom_to_linden ca) cdt) with (union_emp_r (classAtom_to_linden ca) cdt) by (subst; auto).
+        all: try constructor; subst; auto; try apply classAtom_to_linden_sound; auto.
+        replace (classAtom_to_linden ca) with (union_emp_r (classAtom_to_linden ca) CdEmpty) by auto.
         constructor; auto. apply classAtom_to_linden_sound. auto.
       - simpl. intro cd.
         destruct classAtom_singleCharacter_numValue as [cl|] eqn:Hcl; try discriminate; simpl.