diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-09 17:28:10 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-09 17:28:10 +0000 |
commit | e29b0c71f446ea6267711c7cc19294fd93fb81ad (patch) | |
tree | 0317ddbba0cc4a81175f6e05e337d56211a29a26 /lib/Maps.v | |
parent | 20eea14b1c678722642da5c22afd6e87b6cdf686 (diff) | |
download | compcert-e29b0c71f446ea6267711c7cc19294fd93fb81ad.tar.gz compcert-e29b0c71f446ea6267711c7cc19294fd93fb81ad.zip |
Assorted cleanups, esp. to avoid generating _rec and _rect recursors in
submodules. (Extraction does not remove them, then.)
common/Switch: replaced use of FMaps by our own Maps.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Maps.v')
-rw-r--r-- | lib/Maps.v | 26 |
1 files changed, 5 insertions, 21 deletions
@@ -34,6 +34,10 @@ Require Import Coqlib. +(* To avoid useless definitions of inductors in extracted code. *) +Local Unset Elimination Schemes. +Local Unset Case Analysis Schemes. + Set Implicit Arguments. (** * The abstract signatures of trees *) @@ -42,8 +46,6 @@ Module Type TREE. Variable elt: Type. Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}. Variable t: Type -> Type. - Variable eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) -> - forall (a b: t A), {a = b} + {a <> b}. Variable empty: forall (A: Type), t A. Variable get: forall (A: Type), elt -> t A -> option A. Variable set: forall (A: Type), elt -> A -> t A -> t A. @@ -202,18 +204,10 @@ Module PTree <: TREE. . Implicit Arguments Leaf [A]. Implicit Arguments Node [A]. + Scheme tree_ind := Induction for tree Sort Prop. Definition t := tree. - Theorem eq : forall (A : Type), - (forall (x y: A), {x=y} + {x<>y}) -> - forall (a b : t A), {a = b} + {a <> b}. - Proof. - intros A eqA. - decide equality. - generalize o o0; decide equality. - Qed. - Definition empty (A : Type) := (Leaf : t A). Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A := @@ -1084,14 +1078,6 @@ Module PMap <: MAP. Definition t (A : Type) : Type := (A * PTree.t A)%type. - Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) -> - forall (a b: t A), {a = b} + {a <> b}. - Proof. - intros. - generalize (PTree.eq X). intros. - decide equality. - Qed. - Definition init (A : Type) (x : A) := (x, PTree.empty A). @@ -1175,8 +1161,6 @@ Module IMap(X: INDEXED_TYPE). Definition elt := X.t. Definition elt_eq := X.eq. Definition t : Type -> Type := PMap.t. - Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) -> - forall (a b: t A), {a = b} + {a <> b} := PMap.eq. Definition init (A: Type) (x: A) := PMap.init x. Definition get (A: Type) (i: X.t) (m: t A) := PMap.get (X.index i) m. Definition set (A: Type) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m. |