diff --git a/WarblreEquiv/CharDescrCharSet.v b/WarblreEquiv/CharDescrCharSet.v index cb0c451..66a8b4a 100644 --- a/WarblreEquiv/CharDescrCharSet.v +++ b/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. diff --git a/WarblreEquiv/RegexpTranslation.v b/WarblreEquiv/RegexpTranslation.v index 3be666f..02e7009 100644 --- a/WarblreEquiv/RegexpTranslation.v +++ b/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.