aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Record.v
blob: 8334322c99d065220759923b54072b9e7344bb89 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
(* Nijmegen expects redefinition of sorts *)
Definition CProp := Prop.
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. *)

Inductive 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}
}.

(* Test syntactic sugar suggested by wish report #2138 *)

Record R : Type := {
  P (A : Type) : Prop := exists x : A -> A, x = x;
  Q A : P A -> P A
}.