Correct handling of implicit arguments in [Equations] definitions,

support for "where" notation declarations as well. Better checking of
recursivity or not, after type-checking.


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

1 files changed, 52 insertions, 21 deletions

diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
index 3ef591959..ea4d693dd 100644
--- a/test-suite/success/Equations.v
+++ b/test-suite/success/Equations.v
@@ -21,51 +21,60 @@ Equations tail {A} (l : list A) : (list A) :=
 tail A nil := nil ;
 tail A (cons a v) := v.
 
-Eval compute in tail.
+Eval compute in @tail.
 
-Eval compute in (tail _ (cons 1 nil)).
+Eval compute in (tail (cons 1 nil)).
+
+Reserved Notation " x ++ y " (at level 60, right associativity).
+
+Equations app (l l' : list nat) : list nat :=
+  [] ++ l       := l ;
+  (a :: v) ++ l := a :: (v ++ l) 
+
+where " x ++ y " := (app x y).
 
 Equations app' {A} (l l' : list A) : (list A) :=
 app' A nil l := l ;
-app' A (cons a v) l := cons a (app' A v l).
+app' A (cons a v) l := cons a (app' v l).
 
-Eval compute in app'.
+
+Eval compute in @app'.
 
 Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) :=
 zip' A f nil nil := nil ;
-zip' A f (cons a v) (cons b w) := cons (f a b) (zip' _ f v w) ;
+zip' A f (cons a v) (cons b w) := cons (f a b) (zip' f v w) ;
 zip' A f nil (cons b w) := nil ;
 zip' A f (cons a v) nil := nil.
 
-Eval compute in zip'.
+Eval compute in @zip'.
 
-Eval cbv delta [ zip' zip'_obligation_1 zip'_obligation_2 zip'_obligation_3 ] beta iota zeta in zip'.
+Eval cbv delta [ zip' zip'_obligation_1 zip'_obligation_2 zip'_obligation_3 ] beta iota zeta in @zip'.
 
 Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) :=
 zip'' A f nil nil def := nil ;
-zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' _ f v w def) ;
+zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' f v w def) ;
 zip'' A f nil (cons b w) def := def ;
 zip'' A f (cons a v) nil def := def.
 
-Eval compute in zip''.
-Eval cbv delta [ zip'' ] beta iota zeta in zip''.
+Eval compute in @zip''.
+Eval cbv delta [ zip'' ] beta iota zeta in @zip''.
 
 Implicit Arguments Vnil [[A]].
 Implicit Arguments Vcons [[A] [n]].
 
-Equations vhead A n (v : vector A (S n)) : A := 
+Equations vhead {A n} (v : vector A (S n)) : A := 
 vhead A n (Vcons a v) := a.
 
-Eval compute in (vhead _ _ (Vcons 2 (Vcons 1 Vnil))).
-Eval compute in vhead.
+Eval compute in (vhead (Vcons 2 (Vcons 1 Vnil))).
+Eval compute in @vhead.
 
-Equations vmap {A B} (f : A -> B) n (v : vector A n) : (vector B n) :=
+Equations vmap {A B} (f : A -> B) {n} (v : vector A n) : (vector B n) :=
 vmap A B f 0 Vnil := Vnil ;
-vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap A B f n v).
+vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap f v).
 
-Eval compute in (vmap _ _ id _ (@Vnil nat)).
-Eval compute in (vmap _ _ id _ (@Vcons nat 2 _ Vnil)).
-Eval compute in vmap.
+Eval compute in (vmap id (@Vnil nat)).
+Eval compute in (vmap id (@Vcons nat 2 _ Vnil)).
+Eval compute in @vmap.
 
 Inductive fin : nat -> Set :=
 | fz : Π {n}, fin (S n)
@@ -79,12 +88,12 @@ Implicit Arguments finle [[n]].
 
 Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k :=
 trans (S n) fz j k leqz q := leqz ;
-trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (trans _ _ _ _ p q).
+trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (trans p q).
 
-Lemma trans_eq1 n (j k : fin (S n)) q : trans (S n) fz j k leqz q = leqz.
+Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz.
 Proof. intros. simplify_equations ; reflexivity. Qed.
 
-Lemma trans_eq2 n i j k p q : trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans _ _ _ _ p q).
+Lemma trans_eq2 n i j k p q : @trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans p q).
 Proof. intros. simplify_equations ; reflexivity. Qed.
 
 Section Image.
@@ -100,3 +109,25 @@ Section Image.
 
 End Image.
 
+Section Univ.
+
+  Inductive univ : Set :=
+  | ubool | unat | uarrow (from:univ) (to:univ).
+
+  Equations interp (u : univ) : Type :=
+  interp ubool := bool ; interp unat := nat ; 
+  interp (uarrow from to) := interp from -> interp to.
+
+  Equations foo (u : univ) (el : interp u) : interp u :=
+  foo ubool true := false ;
+  foo ubool false := true ;
+  foo unat t := t ;
+  foo (uarrow from to) f := id ∘ f.
+
+  Eval lazy beta delta [ foo foo_obligation_1 foo_obligation_2 ] iota zeta in foo.
+
+End Univ.
+
+Eval compute in (foo ubool false).
+Eval compute in (foo (uarrow ubool ubool) negb).
+Eval compute in (foo (uarrow ubool ubool) id).