Add some example uses of the new record features in Record.v:

- introduction notation with missing fields and interaction with
Program.
- Ability to add (currently a single) "where notation" clause to each
field.
- Use every information available to do type inference and
internalisation.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11552 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 80 insertions, 1 deletions

diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 7fdbcda7b..d9ad721a0 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -1,3 +1,82 @@
 (* Nijmegen expects redefinition of sorts *)
 Definition CProp := Prop.
-Record test : CProp :=  {n : nat}.
+Record test : CProp :=  {n : nat ; m : bool ; _ : n <> 0 }.
+Require Import Program.
+Require Import List.
+
+Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
+Implicit Arguments vector [].
+
+Coercion vec_list : vector >-> list.
+
+Hint Rewrite @vec_len : datatypes.
+
+Ltac crush := repeat (program_simplify ; autorewrite with list datatypes ; auto with *).
+
+Obligation Tactic := crush.
+
+Program Definition vnil {A} : vector A 0 := {| vec_list := [] |}.
+
+Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) := 
+  {| vec_list := cons a (vec_list v) |}.
+
+Hint Rewrite map_length rev_length : datatypes.
+
+Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n := 
+  {| vec_list := map f v |}.
+
+Program Definition vreverse {A n} (v : vector A n) : vector A n := 
+  {| vec_list := rev v |}.
+
+Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B := 
+  match v, w with
+    | nil, nil => nil
+    | cons f fs, cons x xs => cons (f x) (va_list fs xs)
+    | _, _ => nil
+  end.
+
+Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n := 
+  {| vec_list := va_list v w |}.
+
+Next Obligation. 
+  destruct v as [v Hv]; destruct w as [w Hw] ; simpl.
+  subst n. revert w Hw. induction v ; destruct w ; crush. 
+  rewrite IHv ; auto.
+Qed.
+
+(* Correct type inference of record notation. Initial example by Spiwack. *) 
+
+Record Machin := {
+ Bazar : option Machin
+}.
+
+Definition bli : Machin :=
+ {| Bazar := Some ({| Bazar := None |}:Machin) |}.
+
+Definition bli' : option (option Machin)  :=
+ Some (Some {| Bazar := None |} ).
+
+Definition bli'' : Machin :=
+ {| Bazar := Some {| Bazar := None |} |}.
+
+Definition bli''' := {| Bazar := Some {| Bazar := None |} |}.
+
+(** Correctly use scoping information *)
+
+Require Import ZArith.
+
+Record Foo := { bar : Z }.
+Definition foo := {| bar := 0 |}.
+
+(** Notations inside records *)
+
+Require Import Relation_Definitions.
+
+Record DecidableOrder : Type :=
+{ A : Type
+; le : relation A where "x <= y" := (le x y)
+; le_refl : reflexive _ le
+; le_antisym : antisymmetric _ le
+; le_trans : transitive _ le
+; le_total : forall x y, {x <= y}+{y <= x}
+}.