1 files changed, 87 insertions, 0 deletions
diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v
new file mode 100644
index 00000000..11726675
--- /dev/null
+++ b/plugins/quote/Quote.v
@@ -0,0 +1,87 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+Declare ML Module "quote_plugin".
+
+(***********************************************************************
+  The "abstract" type index is defined to represent variables.
+
+  index : Set
+  index_eq : index -> bool
+  index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m
+  index_lt : index -> bool
+  varmap : Type -> Type.
+  varmap_find : (A:Type)A -> index -> (varmap A) -> A.
+
+  The first arg. of varmap_find is the default value to take
+  if the object is not found in the varmap.
+
+  index_lt defines a total well-founded order, but we don't prove that.
+
+***********************************************************************)
+
+Set Implicit Arguments.
+Unset Boxed Definitions.
+
+Section variables_map.
+
+Variable A : Type.
+
+Inductive varmap : Type :=
+  | Empty_vm : varmap
+  | Node_vm : A -> varmap -> varmap -> varmap.
+
+Inductive index : Set :=
+  | Left_idx : index -> index
+  | Right_idx : index -> index
+  | End_idx : index.
+
+Fixpoint varmap_find (default_value:A) (i:index) (v:varmap) {struct v} : A :=
+  match i, v with
+  | End_idx, Node_vm x _ _ => x
+  | Right_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v2
+  | Left_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v1
+  | _, _ => default_value
+  end.
+
+Fixpoint index_eq (n m:index) {struct m} : bool :=
+  match n, m with
+  | End_idx, End_idx => true
+  | Left_idx n', Left_idx m' => index_eq n' m'
+  | Right_idx n', Right_idx m' => index_eq n' m'
+  | _, _ => false
+  end.
+
+Fixpoint index_lt (n m:index) {struct m} : bool :=
+  match n, m with
+  | End_idx, Left_idx _ => true
+  | End_idx, Right_idx _ => true
+  | Left_idx n', Right_idx m' => true
+  | Right_idx n', Right_idx m' => index_lt n' m'
+  | Left_idx n', Left_idx m' => index_lt n' m'
+  | _, _ => false
+  end.
+
+Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m.
+  simple induction n; simple induction m; simpl in |- *; intros.
+  rewrite (H i0 H1); reflexivity.
+  discriminate.
+  discriminate.
+  discriminate.
+  rewrite (H i0 H1); reflexivity.
+  discriminate.
+  discriminate.
+  discriminate.
+  reflexivity.
+Qed.
+
+End variables_map.
+
+Unset Implicit Arguments.