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

4 files changed, 105 insertions, 58 deletions

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index ab2fa6cfbf..4464d1ca63 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -579,7 +579,7 @@ open Topconstr
 open Constrintern
 open Decl_kinds
 
-type equation = identifier located * constr_expr list * (constr_expr, identifier located) rhs
+type equation = constr_expr * (constr_expr, identifier located) rhs
 
 let locate_reference qid =
   match Nametab.extended_locate qid with
@@ -612,9 +612,10 @@ let ids_of_patc c ?(bound=Idset.empty) l =
 	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
     | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
   in aux bound l c
-    
-let interp_pats isevar env impls pats sign =
-  let vars = fold_left (fun acc patc -> ids_of_patc patc acc) [] pats in
+
+let interp_pats i isevar env impls pat sign recu =
+  let bound = Idset.singleton i in
+  let vars = ids_of_patc pat ~bound [] in
   let varsctx, env' = 
     fold_right (fun (loc, id) (ctx, env) ->
       let decl =
@@ -624,19 +625,21 @@ let interp_pats isevar env impls pats sign =
 	decl::ctx, push_rel decl env)
       vars ([], env)
   in
-  let patcs = 
-    fold_left2 (fun subst pat (_, _, ty) -> 
-      let ty = substl subst ty in
-	interp_casted_constr_evars isevar env' ~impls pat ty :: subst)
-      [] pats (List.rev sign)
+  let pats =
+    let patenv = match recu with None -> env' | Some ty -> push_named (i, None, ty) env' in
+    let patt, _ = interp_constr_evars_impls ~evdref:isevar patenv ~impls:([],[]) pat in
+      match kind_of_term patt with
+      | App (m, args) -> Array.to_list args
+      | _ -> user_err_loc (constr_loc pat, "interp_pats",
+			  str "Error parsing pattern: unnexpected left-hand side")
   in
     isevar := nf_evar_defs !isevar;
     (nf_rel_context_evar (Evd.evars_of !isevar) varsctx, 
     nf_env_evar (Evd.evars_of !isevar) env',
-    map (nf_evar (Evd.evars_of !isevar)) patcs)
+    rev_map (nf_evar (Evd.evars_of !isevar)) pats)
       
-let interp_eqn isevar env impls sign arity (idl, pats, rhs) =
-  let ctx, env', patcs = interp_pats isevar env impls pats sign in
+let interp_eqn i isevar env impls sign arity recu (pats, rhs) =
+  let ctx, env', patcs = interp_pats i isevar env impls pats sign recu in
   let rhs' = match rhs with
     | Program p -> 
 	Program (interp_casted_constr_evars isevar env' ~impls p (substl patcs arity))
@@ -645,31 +648,34 @@ let interp_eqn isevar env impls sign arity (idl, pats, rhs) =
 
 open Entries
 
-let define_by_eqs i l t eqs =
+let define_by_eqs i l t nt eqs =
   let env = Global.env () in
   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 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
+  let ty = it_mkProd_or_LetIn arity sign in
+  let data = Command.compute_interning_datas env [] [i] [ty] [impls] in
+  let fixenv = push_rel (Name i, None, ty) env in
+  let equations = 
+    States.with_heavy_rollback (fun () -> 
+      Option.iter (Command.declare_interning_data data) nt;
+      map (interp_eqn i isevar fixenv data sign arity None) eqs) ()
   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 fixenv = nf_env_evar (Evd.evars_of !isevar) fixenv in
-  let split = make_split fixenv prob equations in
+  let ce = check_evars fixenv Evd.empty !isevar in
+  let is_recursive, env' =
+    let occur_eqn (ctx, _, rhs) =
+      match rhs with
+      | Program c -> dependent (mkRel (succ (length ctx))) c
+      | _ -> false
+    in if exists occur_eqn equations then true, fixenv else false, env
+  in
+  let split = make_split env' prob equations in
     (* if valid_tree prob split then *)
-  let t, ty = term_of_tree isevar fixenv prob split in
+  let t, ty = term_of_tree isevar env' prob split in
   let t = 
     if is_recursive then
       let firstsplit = 
@@ -681,7 +687,7 @@ let define_by_eqs i l t eqs =
   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)
+    ignore(Subtac_obligations.add_definition ~implicits:impls i t' ty' obls)
       
 module Gram = Pcoq.Gram
 module Vernac = Pcoq.Vernac_
@@ -694,6 +700,9 @@ struct
   let deppat_equations : equation list Gram.Entry.e = gec "deppat_equations"
 
   let binders_let2 : local_binder list Gram.Entry.e = gec "binders_let2"
+
+(*   let where_decl : decl_notation Gram.Entry.e = gec "where_decl" *)
+
 end
 
 open Rawterm
@@ -702,6 +711,7 @@ open Util
 open Pcoq
 open Prim
 open Constr
+open G_vernac
 
 GEXTEND Gram
   GLOBAL: (* deppat_gallina_loc *) deppat_equations binders_let2;
@@ -715,11 +725,7 @@ GEXTEND Gram
   ;
 
   equation:
-    [ [ c = Constr.lconstr; r=rhs ->
-      match c with
-      | CApp (loc, (None, CRef (Ident lid)), l) ->
-	  (lid, List.map fst l, r)
-      | _ -> error "Error parsing equation" ] ]
+    [ [ c = Constr.lconstr; r=rhs -> (c, r) ] ]
   ;
 
   rhs:
@@ -744,10 +750,19 @@ let (wit_binders_let2 : Genarg.tlevel binders_let2_argtype),
   (rawwit_binders_let2 : Genarg.rlevel binders_let2_argtype) =
   Genarg.create_arg "binders_let2"
 
+type 'a decl_notation_argtype = (Vernacexpr.decl_notation, 'a) Genarg.abstract_argument_type
+
+let (wit_decl_notation : Genarg.tlevel decl_notation_argtype),
+  (globwit_decl_notation : Genarg.glevel decl_notation_argtype),
+  (rawwit_decl_notation : Genarg.rlevel decl_notation_argtype) =
+  Genarg.create_arg "decl_notation"
+
+
 
 VERNAC COMMAND EXTEND Define_equations
-| [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs) ] ->
-    [ define_by_eqs i l t eqs ]
+| [ "Equations" ident(i) binders_let2(l) ":" lconstr(t) ":=" deppat_equations(eqs)
+      decl_notation(nt) ] ->
+    [ define_by_eqs i l t nt eqs ]
 END
 
 open Tacmach
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5f656ed5c2..c9fc4e2ffb 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,6 +46,7 @@ let noedit_mode = Gram.Entry.create "vernac:noedit_command"
 let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
 let thm_token = Gram.Entry.create "vernac:thm_token"
 let def_body = Gram.Entry.create "vernac:def_body"
+let decl_notation = Gram.Entry.create "vernac:decl_notation"
 let typeclass_context = Gram.Entry.create "vernac:typeclass_context"
 let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion"
 
@@ -119,7 +120,7 @@ let no_coercion loc (c,x) =
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    typeclass_context typeclass_constraint;
+    typeclass_context typeclass_constraint decl_notation;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
index 3ef5919596..ea4d693dda 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).
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 869df369b8..2bf25c8e70 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -389,7 +389,7 @@ Ltac depelim id :=
    (used internally). *)
 
 Ltac destruct_last :=
-  on_last_hyp ltac:(fun id => generalize_eqs id ; destruct id).
+  on_last_hyp ltac:(fun id => simpl in id ; generalize_eqs id ; destruct id).
 
 (** The rest is support tactics for the [Equations] command. *)