Skip to content

WarblreEquiv: another way to avoid generating Unions of CdEmpty #38

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Aurele-Barriere merged 1 commit into from
Jun 30, 2026
Merged

WarblreEquiv: another way to avoid generating Unions of CdEmpty #38

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 39 additions & 24 deletions WarblreEquiv/CharDescrCharSet.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
79 changes: 47 additions & 32 deletions WarblreEquiv/RegexpTranslation.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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':
Expand Down
Loading