From 7bb6ca92a08f24c86f74a1bc134fe1f5b4930595 Mon Sep 17 00:00:00 2001
From: glondu
Date: Mon, 30 Mar 2009 15:22:27 +0000
Subject: Add tests for quote

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12038 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Quote.out | 24 ++++++++++++++++++++++++
 test-suite/output/Quote.v   | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+)
 create mode 100644 test-suite/output/Quote.out
 create mode 100644 test-suite/output/Quote.v

diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out
new file mode 100644
index 0000000000..ca7fc3624b
--- /dev/null
+++ b/test-suite/output/Quote.out
@@ -0,0 +1,24 @@
+(interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx))
+(interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
+   (f_and (f_const A)
+      (f_and (f_or (f_atom End_idx) (f_const A))
+         (f_or (f_const A) (f_not (f_atom End_idx))))))
+1 subgoal
+  
+  H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
+      B
+  ============================
+   interp_f
+     (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop))
+     (f_and (f_atom (Left_idx End_idx))
+        (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx)))
+           (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx)))))
+1 subgoal
+  
+  H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/
+      B
+  ============================
+   interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop))
+     (f_and (f_const A)
+        (f_and (f_or (f_atom End_idx) (f_const A))
+           (f_or (f_const A) (f_not (f_atom End_idx)))))
diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v
new file mode 100644
index 0000000000..2c373d5052
--- /dev/null
+++ b/test-suite/output/Quote.v
@@ -0,0 +1,36 @@
+Require Import Quote.
+
+Parameter A B : Prop.
+
+Inductive formula : Type :=
+  | f_and : formula -> formula -> formula
+  | f_or : formula -> formula -> formula
+  | f_not : formula -> formula
+  | f_true : formula
+  | f_atom : index -> formula
+  | f_const : Prop -> formula.
+
+Fixpoint interp_f (vm:
+                    varmap Prop) (f:formula) {struct f} : Prop :=
+  match f with
+  | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2
+  | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2
+  | f_not f1 => ~ interp_f vm f1
+  | f_true => True
+  | f_atom i => varmap_find True i vm
+  | f_const c => c
+  end.
+
+Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B).
+intro H.
+match goal with
+  | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H)
+end.
+match goal with
+  |- ?g => quote interp_f [ A ] in g using (fun x => idtac x)
+end.
+quote interp_f.
+Show.
+simpl; quote interp_f [ A ].
+Show.
+Admitted.
-- 
cgit v1.2.3