Add support for recursive definitions to [Equations], deciding if a

definition is recursive or not based on occurence of a rec call in 
the body. Examples updated, enjoy!


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

3 files changed, 48 insertions, 25 deletions

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index 15ea15f353..ab2fa6cfbf 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -566,7 +566,7 @@ let term_of_tree isevar env (i, delta, ty) tree =
 			Some (Class_tactics.coq_nat_of_int (length before)),
 			Lazy.force Class_tactics.coq_nat)
 	  in
-	  let ty = it_mkLambda_or_LetIn ty [nbbranches;nbdiscr] in
+	  let ty = it_mkLambda_or_LetIn (lift 2 ty) [nbbranches;nbdiscr] in
 	  let term = e_new_evar isevar env ~src:(dummy_loc, QuestionMark true) ty in
 	    term
 	in       
@@ -650,13 +650,35 @@ let define_by_eqs i l t eqs =
   let isevar = ref (create_evar_defs Evd.empty) in
   let (env', sign), impls = interp_context_evars isevar env l in
   let arity = interp_type_evars isevar env' t in
-  let equations = map (interp_eqn isevar env ([],[]) sign arity) eqs in
+  let is_recursive, fixenv = 
+    let occur_eqn (_, _, rhs) =
+      match rhs with
+      | Program c -> occur_var_constr_expr i c
+      | _ -> false
+    in 
+      if exists occur_eqn eqs then 
+	let ty = it_mkProd_or_LetIn arity sign in
+	let fixenv = push_rel (Name i, None, ty) env in
+	  true, fixenv
+      else false, env
+  in
+  let equations = map (interp_eqn isevar fixenv ([],[]) sign arity) eqs in
   let sign = nf_rel_context_evar (Evd.evars_of !isevar) sign in
   let arity = nf_evar (Evd.evars_of !isevar) arity in
   let prob = (i, sign, arity) in
-  let split = make_split env prob equations in
+  let fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in
+  let split = make_split fixenv prob equations in
     (* if valid_tree prob split then *)
-  let t, ty = term_of_tree isevar env prob split in
+  let t, ty = term_of_tree isevar fixenv prob split in
+  let t = 
+    if is_recursive then
+      let firstsplit = 
+	match split with
+	| Split (ctx, lhs, rel, indf, unif, sp) -> (length ctx - rel)
+	| _ -> 0
+      in mkFix (([|firstsplit|], 0), ([|Name i|], [|ty|], [|t|]))
+    else t
+  in
   let undef = undefined_evars !isevar in
   let obls, t', ty' = Eterm.eterm_obligations env i !isevar (Evd.evars_of undef) 0 t ty in
     ignore(Subtac_obligations.add_definition i t' ty' obls)
diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
index d08ce884c5..3ef5919596 100644
--- a/test-suite/success/Equations.v
+++ b/test-suite/success/Equations.v
@@ -6,7 +6,7 @@ Obligation Tactic := try equations.
 Equations neg (b : bool) : bool :=
 neg true := false ;
 neg false := true.
-
+ 
 Eval compute in neg.
 
 Require Import Coq.Lists.List.
@@ -27,20 +27,13 @@ Eval compute in (tail _ (cons 1 nil)).
 
 Equations app' {A} (l l' : list A) : (list A) :=
 app' A nil l := l ;
-app' A (cons a v) l := cons a (app v l).
+app' A (cons a v) l := cons a (app' A v l).
 
 Eval compute in app'.
 
-Fixpoint zip {A} (f : A -> A -> A) (l l' : list A) : list A :=
-  match l, l' with
-    | nil, nil => nil
-    | cons a v, cons b v' => cons (f a b) (zip f v v')
-    | _, _ => nil
-  end.
-
 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.
 
@@ -50,7 +43,7 @@ Eval cbv delta [ zip' zip'_obligation_1 zip'_obligation_2 zip'_obligation_3 ] be
 
 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) ;
+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.
 
@@ -64,15 +57,15 @@ 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))).
-
-Axiom cheat : Π A, A.
+Eval compute in vhead.
 
 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) (cheat _).
+vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap A B f n v).
 
 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)
@@ -86,13 +79,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) fz (leqs p) q :=! q ;
-trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) := leqs (cheat _).
+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.
 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 (cheat _).
+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.
@@ -106,4 +98,5 @@ Section Image.
 
   Eval compute in inv.
 
-End Image.
\ No newline at end of file
+End Image.
+
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 44d2f4f7e4..869df369b8 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -411,7 +411,7 @@ Ltac simplify_method H := clear H ; simplify_dep_elim ; reverse.
 Ltac solve_method :=
   match goal with
     | [ H := ?body : nat |- _ ] => simplify_method H ; solve_empty body
-    | [ H := ?body |- _ ] => simplify_method H ; try_intros body
+    | [ H := ?body |- _ ] => simplify_method H ; (try intro) ; try_intros body
   end.
 
 (** Impossible cases, by splitting on a given target. *)
@@ -421,9 +421,17 @@ Ltac solve_split :=
     | [ |- let split := ?x : nat in _ ] => intros _ ; solve_empty x
   end.
 
+(** If defining recursive functions, the prototypes come first. *)
+
+Ltac intro_prototypes :=
+  match goal with 
+    | [ |- Π x : _, _ ] => intro ; intro_prototypes
+    | _ => idtac
+  end.
+
 (** The [equations] tactic is the toplevel tactic for solving goals generated
    by [Equations]. *)
 
-Ltac equations := 
-  solve [ solve_split ] || solve [solve_equations solve_method] || fail "Unnexpcted equations goal".
+Ltac equations := intro_prototypes ;
+  solve [solve_equations solve_method] || solve [ solve_split ] || fail "Unnexpcted equations goal".