From 2c9f1e9651556839e1feb6c05efa1fd57c50568b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A8le=20Barri=C3=A8re?= Date: Mon, 29 Jun 2026 19:09:45 +0200 Subject: [PATCH] WarblreEquiv: another way to avoid generating Unions of CdEmpty --- WarblreEquiv/CharDescrCharSet.v | 63 +++++++++++++++---------- WarblreEquiv/RegexpTranslation.v | 79 +++++++++++++++++++------------- 2 files changed, 86 insertions(+), 56 deletions(-) diff --git a/WarblreEquiv/CharDescrCharSet.v b/WarblreEquiv/CharDescrCharSet.v index 66a8b4a..a46d87b 100644 --- a/WarblreEquiv/CharDescrCharSet.v +++ b/WarblreEquiv/CharDescrCharSet.v @@ -46,27 +46,6 @@ 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. @@ -250,15 +229,51 @@ Section CharDescrCharSet. equiv_cd_charset cd a. Proof. intros crs cd Hequiv. - induction Hequiv as [|ca cacd t tcd Hequiv' Hequiv IH | l h cl ch t tcd Hequivl Hequivh Hl_le_h Hequiv IH]. + induction Hequiv as [|ca cacd Hequiv |ca cacd t tcd Hequiv' Hequiv IH | l h cl ch Hequivl Hequivh Hl_le_h |l h cl ch t tcd Hequivl Hequivh Hl_le_h Hequiv IH]. - simpl. unfold Coercions.Coercions.wrap_CharSet. eexists. split. + reflexivity. + apply equiv_cd_empty. + - simpl. pose proof equiv_cd_ClassAtom ca cacd Hequiv as [A [HeqA Hequivatom]]. + rewrite HeqA. simpl. + unfold Coercions.Coercions.wrap_CharSet. eexists. split; try reflexivity. + unfold equiv_cd_charset. intros c. rewrite CharSet.exist_canonicalized_equiv. + symmetry. destruct char_match eqn:MATCH. + + rewrite Hequivatom in MATCH. rewrite CharSet.exist_canonicalized_equiv in MATCH. + rewrite CharSet.exist_iff in *. + destruct MATCH as [c0 [CONT CAN]]. exists c0. + split; auto. + rewrite CharSet.union_contains. rewrite Bool.orb_true_iff. left. auto. + + rewrite Hequivatom in MATCH. rewrite CharSet.exist_canonicalized_equiv in MATCH. + rewrite CharSet.exist_false_iff in *. + intros c0. specialize (MATCH c0) as [CONT|CAN]. + * left. rewrite CharSet.union_contains. rewrite Bool.orb_false_iff. split; auto. + apply CharSet.empty_contains. + * right; auto. - 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_emp. + + now apply equiv_cd_union. + - simpl. + rewrite equiv_ClassAtom_single_charset with (c := cl) by auto. + rewrite equiv_ClassAtom_single_charset with (c := ch) by auto. + simpl. + unfold Semantics.characterRange. setoid_rewrite CharSet.singleton_size. simpl. + do 2 rewrite CharSet.singleton_unique. simpl. + 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; try reflexivity. + unfold equiv_cd_charset. intros c. rewrite CharSet.exist_canonicalized_equiv. + symmetry. destruct char_match eqn:MATCH. + + unfold char_match, char_match' in MATCH. + rewrite CharSet.exist_canonicalized_equiv in MATCH. + rewrite CharSet.exist_iff in *. destruct MATCH as [c0 [CONT CAN]]. exists c0. + split; auto. rewrite CharSet.union_contains. rewrite Bool.orb_true_iff. left. auto. + + unfold char_match, char_match' in MATCH. + rewrite CharSet.exist_canonicalized_equiv in MATCH. + rewrite CharSet.exist_false_iff in *. intros c0. specialize (MATCH c0) as [CONT|CAN]. + * left. rewrite CharSet.union_contains. rewrite Bool.orb_false_iff. split; auto. + apply CharSet.empty_contains. + * right; auto. - simpl. rewrite equiv_ClassAtom_single_charset with (c := cl) by auto. rewrite equiv_ClassAtom_single_charset with (c := ch) by auto. @@ -269,6 +284,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_emp; auto. do 2 rewrite Character.numeric_pseudo_bij. apply equiv_cd_range. assumption. + + apply equiv_cd_union; 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 02e7009..ba8a468 100644 --- a/WarblreEquiv/RegexpTranslation.v +++ b/WarblreEquiv/RegexpTranslation.v @@ -150,23 +150,21 @@ 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) (union_emp_r cacd tcd) + | Equiv_ClassAtomCR_empty: forall ca cacd , equiv_ClassAtom ca cacd -> equiv_ClassRanges (Patterns.ClassAtomCR ca Patterns.EmptyCR) cacd + | 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_RangeCR_empty: + forall l h cl ch, + equiv_ClassAtom l (CdSingle cl) -> equiv_ClassAtom h (CdSingle ch) -> + Character.numeric_value cl <= Character.numeric_value ch -> + equiv_ClassRanges (Patterns.RangeCR l h Patterns.EmptyCR) (CdRange cl ch) | 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) (union_emp_r (CdRange cl ch) tcd). + equiv_ClassRanges (Patterns.RangeCR l h t) (CdUnion (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 @@ -525,16 +523,25 @@ Section RegexpTranslation. Fixpoint classRanges_to_linden (cr: Patterns.ClassRanges): Result char_descr wl_transl_error := match cr with | Patterns.EmptyCR => Success CdEmpty + | Patterns.ClassAtomCR ca Patterns.EmptyCR => + Success (classAtom_to_linden ca) | Patterns.ClassAtomCR ca t => let cda := classAtom_to_linden ca in let! cdt =<< classRanges_to_linden t in - Success (union_emp_r cda cdt) + Success (CdUnion cda cdt) + | Patterns.RangeCR l h Patterns.EmptyCR => + let! cl =<< classAtom_singleCharacter_numValue l in + let! ch =<< classAtom_singleCharacter_numValue h in + if cl <=? ch then + Success (CdRange (Character.from_numeric_value cl) (Character.from_numeric_value ch)) + else + Error WlMalformed | 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 (union_emp_r (CdRange (Character.from_numeric_value cl) (Character.from_numeric_value ch)) cdt) + Success (CdUnion (CdRange (Character.from_numeric_value cl) (Character.from_numeric_value ch)) cdt) else Error WlMalformed end. @@ -751,24 +758,32 @@ Section RegexpTranslation. Proof. intro crs. induction crs. - 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 <-. 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. - destruct (classAtom_singleCharacter_numValue h) as [ch|] eqn:Hch; try discriminate; simpl. - destruct classRanges_to_linden as [cdt|] eqn:Hcdt; try discriminate; simpl. - destruct Nat.leb eqn:Hle; try discriminate; simpl. - apply PeanoNat.Nat.leb_le in Hle. - intro H. injection H as <-. constructor; auto. - 1,2: apply classAtom_singleCharacter_numValue_sound; auto. - apply Character.numeric_round_trip_order; auto. + - simpl. intro cd. destruct crs. + + intros H. inversion H. subst. constructor. apply classAtom_to_linden_sound. auto. + + destruct classRanges_to_linden as [cdt|] eqn:Hcdt; try discriminate; simpl. + intros H. injection H as <-. constructor; auto. apply classAtom_to_linden_sound; auto. + + destruct classRanges_to_linden as [cdt|] eqn:Hcdt; try discriminate; simpl. + intros H. injection H as <-. constructor; auto. apply classAtom_to_linden_sound; auto. + - simpl. destruct crs; intros cd H. + + destruct classAtom_singleCharacter_numValue as [cl|] eqn:Hcl; try discriminate; simpl in H. + destruct (classAtom_singleCharacter_numValue h) as [ch|] eqn:Hch; try discriminate; simpl in H. + destruct Nat.leb eqn:Hle; try discriminate; simpl. injection H as <-. constructor; auto. + 1,2: apply classAtom_singleCharacter_numValue_sound; auto. + apply Character.numeric_round_trip_order; auto. apply PeanoNat.Nat.leb_le in Hle. auto. + + destruct classAtom_singleCharacter_numValue as [cl|] eqn:Hcl; try discriminate. + destruct (classAtom_singleCharacter_numValue h) as [ch|] eqn:Hch; try discriminate. + destruct classRanges_to_linden as [cdt|] eqn:Hcdt; try discriminate. simpl in H. + destruct (Nat.leb cl ch) eqn:Hle; try discriminate; simpl in H. + injection H as <-. constructor; auto. + 1,2: apply classAtom_singleCharacter_numValue_sound; auto. + apply Character.numeric_round_trip_order; auto. apply PeanoNat.Nat.leb_le in Hle. auto. + + destruct classAtom_singleCharacter_numValue as [cl|] eqn:Hcl; try discriminate. + destruct (classAtom_singleCharacter_numValue h) as [ch|] eqn:Hch; try discriminate. + destruct classRanges_to_linden as [cdt|] eqn:Hcdt; try discriminate. simpl in H. + destruct (Nat.leb cl ch) eqn:Hle; try discriminate; simpl in H. + injection H as <-. constructor; auto. + 1,2: apply classAtom_singleCharacter_numValue_sound; auto. + apply Character.numeric_round_trip_order; auto. apply PeanoNat.Nat.leb_le in Hle. auto. Qed. Lemma charclass_to_linden_sound: @@ -927,11 +942,11 @@ Section RegexpTranslation. Proof. intros crs EE. induction EE; simpl. - eexists. reflexivity. - - destruct IHEE as [cdt IHEE]. rewrite IHEE. eexists. reflexivity. + - destruct IHEE as [cdt IHEE]. rewrite IHEE. destruct t; eexists; reflexivity. - destruct IHEE as [cdt IHEE]. rewrite IHEE. rewrite earlyErrors_translation_singletonClassAtom with (cl := cl); auto. rewrite earlyErrors_translation_singletonClassAtom with (cl := ch); auto. - simpl. apply Nat.leb_le in H1. rewrite H1. eexists. reflexivity. + simpl. apply Nat.leb_le in H1. rewrite H1. destruct t; eexists; reflexivity. Qed. Theorem earlyErrors_pass_translation':