diff options
Diffstat (limited to 'cparser/validator/Alphabet.v')
| -rw-r--r-- | cparser/validator/Alphabet.v | 321 |
1 files changed, 321 insertions, 0 deletions
diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v new file mode 100644 index 0000000..f47f136 --- /dev/null +++ b/cparser/validator/Alphabet.v @@ -0,0 +1,321 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Int31. +Require Import Cyclic31. +Require Import Omega. +Require Import List. +Require Import Syntax. +Require Import Relations. +Require Import RelationClasses. + +Local Obligation Tactic := intros. + +(** A comparable type is equiped with a [compare] function, that define an order + relation. **) +Class Comparable (A:Type) := { + compare : A -> A -> comparison; + compare_antisym : forall x y, CompOpp (compare x y) = compare y x; + compare_trans : forall x y z c, + (compare x y) = c -> (compare y z) = c -> (compare x z) = c +}. + +Theorem compare_refl {A:Type} (C: Comparable A) : + forall x, compare x x = Eq. +Proof. +intros. +pose proof (compare_antisym x x). +destruct (compare x x); intuition; try discriminate. +Qed. + +(** The corresponding order is a strict order. **) +Definition comparableLt {A:Type} (C: Comparable A) : relation A := + fun x y => compare x y = Lt. + +Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) : + StrictOrder (comparableLt C). +Proof. +apply Build_StrictOrder. +unfold Irreflexive, Reflexive, complement, comparableLt. +intros. +pose proof H. +rewrite <- compare_antisym in H. +rewrite H0 in H. +discriminate H. +unfold Transitive, comparableLt. +intros x y z. +apply compare_trans. +Qed. + +(** nat is comparable. **) +Program Instance natComparable : Comparable nat := + { compare := nat_compare }. +Next Obligation. +symmetry. +destruct (nat_compare x y) as [] eqn:?. +rewrite nat_compare_eq_iff in Heqc. +destruct Heqc. +rewrite nat_compare_eq_iff. +trivial. +rewrite <- nat_compare_lt in *. +rewrite <- nat_compare_gt in *. +trivial. +rewrite <- nat_compare_lt in *. +rewrite <- nat_compare_gt in *. +trivial. +Qed. +Next Obligation. +destruct c. +rewrite nat_compare_eq_iff in *; destruct H; assumption. +rewrite <- nat_compare_lt in *. +apply (lt_trans _ _ _ H H0). +rewrite <- nat_compare_gt in *. +apply (gt_trans _ _ _ H H0). +Qed. + +(** A pair of comparable is comparable. **) +Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) : + Comparable (A*B) := + { compare := fun x y => + let (xa, xb) := x in let (ya, yb) := y in + match compare xa ya return comparison with + | Eq => compare xb yb + | x => x + end }. +Next Obligation. +destruct x, y. +rewrite <- (compare_antisym a a0). +rewrite <- (compare_antisym b b0). +destruct (compare a a0); intuition. +Qed. +Next Obligation. +destruct x, y, z. +destruct (compare a a0) as [] eqn:?, (compare a0 a1) as [] eqn:?; +try (rewrite <- H0 in H; discriminate); +try (destruct (compare a a1) as [] eqn:?; + try (rewrite <- compare_antisym in Heqc0; + rewrite CompOpp_iff in Heqc0; + rewrite (compare_trans _ _ _ _ Heqc0 Heqc2) in Heqc1; + discriminate); + try (rewrite <- compare_antisym in Heqc1; + rewrite CompOpp_iff in Heqc1; + rewrite (compare_trans _ _ _ _ Heqc2 Heqc1) in Heqc0; + discriminate); + assumption); +rewrite (compare_trans _ _ _ _ Heqc0 Heqc1); +try assumption. +apply (compare_trans _ _ _ _ H H0). +Qed. + +(** Special case of comparable, where equality is usual equality. **) +Class ComparableUsualEq {A:Type} (C: Comparable A) := + compare_eq : forall x y, compare x y = Eq -> x = y. + +(** Boolean equality for a [Comparable]. **) +Definition compare_eqb {A:Type} {C:Comparable A} (x y:A) := + match compare x y with + | Eq => true + | _ => false + end. + +Theorem compare_eqb_iff {A:Type} {C:Comparable A} {U:ComparableUsualEq C} : + forall x y, compare_eqb x y = true <-> x = y. +Proof. +unfold compare_eqb. +intuition. +apply compare_eq. +destruct (compare x y); intuition; discriminate. +destruct H. +rewrite compare_refl; intuition. +Qed. + +(** [Comparable] provides a decidable equality. **) +Definition compare_eqdec {A:Type} {C:Comparable A} {U:ComparableUsualEq C} (x y:A): + {x = y} + {x <> y}. +Proof. +destruct (compare x y) as [] eqn:?; [left; apply compare_eq; intuition | ..]; + right; intro; destruct H; rewrite compare_refl in Heqc; discriminate. +Defined. + +Instance NComparableUsualEq : ComparableUsualEq natComparable := nat_compare_eq. + +(** A pair of ComparableUsualEq is ComparableUsualEq **) +Instance PairComparableUsualEq + {A:Type} {CA:Comparable A} (UA:ComparableUsualEq CA) + {B:Type} {CB:Comparable B} (UB:ComparableUsualEq CB) : + ComparableUsualEq (PairComparable CA CB). +Proof. +intros x y; destruct x, y; simpl. +pose proof (compare_eq a a0); pose proof (compare_eq b b0). +destruct (compare a a0); try discriminate. +intuition. +destruct H2, H0. +reflexivity. +Qed. + +(** An [Finite] type is a type with the list of all elements. **) +Class Finite (A:Type) := { + all_list : list A; + all_list_forall : forall x:A, In x all_list +}. + +(** An alphabet is both [ComparableUsualEq] and [Finite]. **) +Class Alphabet (A:Type) := { + AlphabetComparable :> Comparable A; + AlphabetComparableUsualEq :> ComparableUsualEq AlphabetComparable; + AlphabetFinite :> Finite A +}. + +(** The [Numbered] class provides a conveniant way to build [Alphabet] instances, + with a good computationnal complexity. It is mainly a injection from it to + [Int31] **) +Class Numbered (A:Type) := { + inj : A -> int31; + surj : int31 -> A; + surj_inj_compat : forall x, surj (inj x) = x; + inj_bound : int31; + inj_bound_spec : forall x, (phi (inj x) < phi inj_bound)%Z +}. + +Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A := + { AlphabetComparable := + {| compare := fun x y => compare31 (inj x) (inj y) |}; + AlphabetFinite := + {| all_list := fst (iter_int31 inj_bound _ + (fun p => (cons (surj (snd p)) (fst p), incr (snd p))) ([], 0%int31)) |} }. +Next Obligation. apply Zcompare_antisym. Qed. +Next Obligation. +destruct c. unfold compare31 in *. +rewrite Z.compare_eq_iff in *. congruence. +eapply Zcompare_Lt_trans; eauto. +eapply Zcompare_Gt_trans; eauto. +Qed. +Next Obligation. +intros x y H. unfold compare, compare31 in H. +rewrite Z.compare_eq_iff in *. +rewrite <- surj_inj_compat, <- phi_inv_phi with (inj y), <- H. +rewrite phi_inv_phi, surj_inj_compat; reflexivity. +Qed. +Next Obligation. +rewrite iter_int31_iter_nat. +pose proof (inj_bound_spec x). +match goal with |- In x (fst ?p) => destruct p as [] eqn:? end. +replace inj_bound with i in H. +revert l i Heqp x H. +apply iter_nat_invariant; intros. +inversion Heqp; clear Heqp; subst. +destruct x; specialize (H _ _ (eq_refl _) x0); simpl in *. +rewrite phi_incr in H0. +pose proof (phi_bounded i). +pose proof (phi_bounded (inj x0)). +destruct (Z_lt_le_dec (Zsucc (phi i)) (2 ^ Z_of_nat size)%Z). +rewrite Zmod_small in H0 by omega. +apply Zlt_succ_le, Zle_lt_or_eq in H0. +destruct H0; eauto. +left. +rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x0), H0, phi_inv_phi; reflexivity. +replace (Zsucc (phi i)) with (2 ^ Z_of_nat size)%Z in H0 by omega. +rewrite Z_mod_same_full in H0. +exfalso; omega. +exfalso; inversion Heqp; subst; + pose proof (phi_bounded (inj x)); change (phi 0) with 0%Z in H; omega. +clear H. +rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal. +pose proof (phi_bounded inj_bound); pose proof (phi_bounded i). +rewrite <- Zabs_eq with (phi i), <- Zabs_eq with (phi inj_bound) by omega. +clear H H0. +do 2 rewrite <- inj_Zabs_nat. +f_equal. +revert l i Heqp. +assert (Zabs_nat (phi inj_bound) < Zabs_nat (2^31)). +apply Zabs_nat_lt, phi_bounded. +induction (Zabs_nat (phi inj_bound)); intros. +inversion Heqp; reflexivity. +inversion Heqp; clear H1 H2 Heqp. +match goal with |- _ (_ (_ (snd ?p))) = _ => destruct p end. +pose proof (phi_bounded i0). +erewrite <- IHn, <- Zabs_nat_Zsucc in H |- *; eauto; try omega. +rewrite phi_incr, Zmod_small; intuition; try omega. +apply inj_lt in H. +pose proof Zle_le_succ. +do 2 rewrite inj_Zabs_nat, Zabs_eq in H; eauto. +Qed. + +(** Previous class instances for [option A] **) +Program Instance OptionComparable {A:Type} (C:Comparable A) : Comparable (option A) := + { compare := fun x y => + match x, y return comparison with + | None, None => Eq + | None, Some _ => Lt + | Some _, None => Gt + | Some x, Some y => compare x y + end }. +Next Obligation. +destruct x, y; intuition. +apply compare_antisym. +Qed. +Next Obligation. +destruct x, y, z; try now intuition; +try (rewrite <- H in H0; discriminate). +apply (compare_trans _ _ _ _ H H0). +Qed. + +Instance OptionComparableUsualEq {A:Type} {C:Comparable A} (U:ComparableUsualEq C) : + ComparableUsualEq (OptionComparable C). +Proof. +intros x y. +destruct x, y; intuition; try discriminate. +rewrite (compare_eq a a0); intuition. +Qed. + +Program Instance OptionFinite {A:Type} (E:Finite A) : Finite (option A) := + { all_list := None :: map Some all_list }. +Next Obligation. +destruct x; intuition. +right. +apply in_map. +apply all_list_forall. +Defined. + +(** Definitions of [FSet]/[FMap] from [Comparable] **) +Require Import OrderedType. +Require Import OrderedTypeAlt. +Require FSetAVL. +Require FMapAVL. + +Module Type ComparableM. + Parameter t : Type. + Declare Instance tComparable : Comparable t. +End ComparableM. + +Module OrderedTypeAlt_from_ComparableM (C:ComparableM) <: OrderedTypeAlt. + Definition t := C.t. + Definition compare : t -> t -> comparison := compare. + + Infix "?=" := compare (at level 70, no associativity). + + Lemma compare_sym x y : (y?=x) = CompOpp (x?=y). + Proof. exact (Logic.eq_sym (compare_antisym x y)). Qed. + Lemma compare_trans c x y z : + (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + Proof. + apply compare_trans. + Qed. +End OrderedTypeAlt_from_ComparableM. + +Module OrderedType_from_ComparableM (C:ComparableM) <: OrderedType. + Module Alt := OrderedTypeAlt_from_ComparableM C. + Include (OrderedType_from_Alt Alt). +End OrderedType_from_ComparableM. |