Add possibility to match on defined hypotheses, using brackets to

disambiguate syntax:
[ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x :
nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will
not parse.
Add applicative contexts in tactics match, to be able to match arbitrary partial
applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end
will bind C to [ ∙ 1 2 ] and x to 0.
Minor improvements in coqdoc.


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

1 files changed, 92 insertions, 41 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2fc6692a8..309aef807 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -135,9 +135,6 @@ let rec pr_value env = function
   | VList (a::_) ->
       str "a list (first element is " ++ pr_value env a ++ str")"
 
-(* Transforms a named_context into a (string * constr) list *)
-let make_hyps = List.map (fun (id,_,typ) -> (id, typ))
-
 (* Transforms an id into a constr if possible, or fails *)
 let constr_of_id env id = 
   construct_reference (Environ.named_context env) id
@@ -620,9 +617,9 @@ let interp_constrpattern_gen sigma env ?(as_type=false) ltacvar c =
 
 (* Reads a pattern *)
 let intern_pattern sigma env ?(as_type=false) lfun = function
-  | Subterm (ido,pc) ->
+  | Subterm (b,ido,pc) ->
       let (metas,pat) = interp_constrpattern_gen sigma env lfun pc in
-      ido, metas, Subterm (ido,pat)
+      ido, metas, Subterm (b,ido,pat)
   | Term pc ->
       let (metas,pat) = interp_constrpattern_gen sigma env ~as_type lfun pc  in
       None, metas, Term pat
@@ -659,6 +656,12 @@ let rec intern_match_context_hyps sigma env lfun = function
       let lfun, metas2, hyps = intern_match_context_hyps sigma env lfun tl in
       let lfun' = name_cons na (Option.List.cons ido lfun) in
       lfun', metas1@metas2, Hyp (locna,pat)::hyps
+  | (Def ((_,na) as locna,mv,mp))::tl ->
+      let ido, metas1, patv = intern_pattern sigma env ~as_type:false lfun mv in
+      let ido', metas2, patt = intern_pattern sigma env ~as_type:true lfun mp in
+      let lfun, metas3, hyps = intern_match_context_hyps sigma env lfun tl in
+      let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
+      lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
   | [] -> lfun, [], []
 
 (* Utilities *)
@@ -1000,7 +1003,7 @@ let eval_pattern lfun c =
   instantiate_pattern lvar c
 
 let read_pattern lfun = function
-  | Subterm (ido,pc) -> Subterm (ido,eval_pattern lfun pc)
+  | Subterm (b,ido,pc) -> Subterm (b,ido,eval_pattern lfun pc)
   | Term pc -> Term (eval_pattern lfun pc)
 
 (* Reads the hypotheses of a Match Context rule *)
@@ -1016,6 +1019,10 @@ let rec read_match_context_hyps lfun lidh = function
       let lidh' = name_fold cons_and_check_name na lidh in
       Hyp (locna,read_pattern lfun mp)::
 	(read_match_context_hyps lfun lidh' tl)
+  | (Def ((loc,na) as locna,mv,mp))::tl ->
+      let lidh' = name_fold cons_and_check_name na lidh in
+      Def (locna,read_pattern lfun mv, read_pattern lfun mp)::
+	(read_match_context_hyps lfun lidh' tl)
   | [] -> []
 
 (* Reads the rules of a Match Context or a Match *)
@@ -1043,37 +1050,69 @@ let rec verify_metas_coherence gl lcm = function
       raise Not_coherent_metas
   | [] -> []
 
+type match_result = 
+  | Matches of (Names.identifier * value) list * (Rawterm.patvar * Term.constr) list *
+      (int * bool)
+  | Fail of int * bool
+
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
-let apply_one_mhyp_context ist env gl lmatch (hypname,pat) (lhyps,nocc) =
+let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) (lhyps,nocc) =
   let get_id_couple id = function
     | Name idpat -> [idpat,VConstr (mkVar id)]
     | Anonymous -> [] in
-  let rec apply_one_mhyp_context_rec nocc = function
-    | (id,hyp)::tl as hyps ->
-      (match pat with
-      | Term t ->
+  let match_pat lmatch nocc id hyp pat =
+    match pat with
+    | Term t ->
         (try
-          let lmeta = verify_metas_coherence gl lmatch (matches t hyp) in
-          (get_id_couple id hypname,lmeta,(id,hyp),(tl,0))
-        with
-	| PatternMatchingFailure | Not_coherent_metas ->
-            apply_one_mhyp_context_rec 0 tl)
-      | Subterm (ic,t) ->
+            let lmeta = verify_metas_coherence gl lmatch (matches t hyp) in
+              Matches ([],lmeta,(0, true))
+          with
+	  | PatternMatchingFailure | Not_coherent_metas ->
+              Fail (0, true))
+    | Subterm (b,ic,t) ->
         (try
-          let (lm,ctxt) = match_subterm nocc t hyp in
+          let (lm,ctxt) = 
+	    if b then match_appsubterm nocc t hyp else match_subterm nocc t hyp 
+	  in
           let lmeta = verify_metas_coherence gl lmatch lm in
-          ((get_id_couple id hypname)@(give_context ctxt ic),
-	   lmeta,(id,hyp),(hyps,nocc + 1))
-         with
-         | PatternMatchingFailure ->
-             apply_one_mhyp_context_rec 0 tl
-         | Not_coherent_metas ->
-             apply_one_mhyp_context_rec (nocc + 1) hyps))
+            Matches 
+	      (give_context ctxt ic,lmeta,(nocc + 1,false))
+          with
+          | PatternMatchingFailure ->
+	      Fail (0, true)
+          | Not_coherent_metas ->
+              Fail (nocc + 1, false))
+  in
+  let rec apply_one_mhyp_context_rec nocc = function
+    | (id,b,hyp as hd)::tl as hyps ->
+	(match patv with
+	| None -> 
+	    (match match_pat lmatch nocc id hyp pat with
+	    | Matches (ids, lmeta, (nocc, cont)) ->
+		(get_id_couple id hypname@ids,
+		lmeta,hd,((if cont then tl else hyps),nocc))
+	    | Fail (nocc, cont) ->
+		apply_one_mhyp_context_rec nocc (if cont then tl else hyps))
+	| Some patv -> 
+	    (match b with
+	    | Some body -> 
+		(match match_pat lmatch nocc id body patv with
+		| Matches (ids, lmeta, (noccv, cont)) ->
+		    (match match_pat (lmatch@lmeta) nocc id hyp pat with
+		    | Matches (ids', lmeta', (nocc', cont')) ->
+			(get_id_couple id hypname@ids@ids',
+			lmeta@lmeta',hd,((if cont || cont' then tl else hyps),nocc'))
+		    | Fail (nocc, cont) ->
+			apply_one_mhyp_context_rec nocc (if cont then tl else hyps))
+		| Fail (nocc, cont) ->
+		    apply_one_mhyp_context_rec nocc (if cont then tl else hyps))
+	    | None -> 
+		apply_one_mhyp_context_rec nocc tl))
     | [] ->
         db_hyp_pattern_failure ist.debug env (hypname,pat);
         raise PatternMatchingFailure
-      in
-  apply_one_mhyp_context_rec nocc lhyps
+  in
+    apply_one_mhyp_context_rec nocc lhyps
 
 let constr_to_id loc = function
   | VConstr c when isVar c -> destVar c
@@ -1815,12 +1854,13 @@ and interp_letin ist gl llc u =
 
 (* Interprets the Match Context expressions *)
 and interp_match_context ist g lz lr lmr =
-  let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps =
-    let (lgoal,ctxt) = match_subterm nocc c csr in
+  let rec apply_goal_sub app ist env goal nocc (id,c) csr mt mhyps hyps =
+    let (lgoal,ctxt) = if app then match_appsubterm nocc c csr
+      else match_subterm nocc c csr in
     let lctxt = give_context ctxt id in
       try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps
       with e when is_match_catchable e ->
-	apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
+	apply_goal_sub app ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
   let rec apply_match_context ist env goal nrs lex lpt = 
     begin
       if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
@@ -1833,7 +1873,7 @@ and interp_match_context ist g lz lr lmr =
 		apply_match_context ist env goal (nrs+1) (List.tl lex) tl
 	    end
 	| (Pat (mhyps,mgoal,mt))::tl ->
-	    let hyps = make_hyps (pf_hyps goal) in
+	    let hyps = pf_hyps goal in
 	    let hyps = if lr then List.rev hyps else hyps in
 	    let mhyps = List.rev mhyps (* Sens naturel *) in
 	    let concl = pf_concl goal in
@@ -1849,8 +1889,8 @@ and interp_match_context ist g lz lr lmr =
 			   | Eval_fail s -> db_eval_failure ist.debug s
 			   | _ -> db_logic_failure ist.debug e);
 			apply_match_context ist env goal (nrs+1) (List.tl lex) tl)
-		 | Subterm (id,mg) ->
-		     (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
+		 | Subterm (b,id,mg) ->
+		     (try apply_goal_sub b ist env goal 0 (id,mg) concl mt mhyps hyps
 		      with
 			| PatternMatchingFailure ->
 			    apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
@@ -1868,9 +1908,14 @@ and interp_match_context ist g lz lr lmr =
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
   let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function
-    | Hyp ((_,hypname),mhyp)::tl as mhyps ->
+    | hyp::tl as mhyps ->
+	let (hypname, mbod, mhyp) = 
+	  match hyp with
+	  | Hyp ((_,hypname),mhyp) -> hypname, None, mhyp
+	  | Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp
+	in
         let (lids,lm,hyp_match,next) =
-          apply_one_mhyp_context ist env goal lmatch (hypname,mhyp) current in
+          apply_one_mhyp_context ist env goal lmatch (hypname,mbod,mhyp) current in
         db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
         begin 
 	  try
@@ -1977,13 +2022,16 @@ and interp_genarg_var_list1 ist gl x =
 
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
-  let rec apply_match_subterm ist nocc (id,c) csr mt =
-    let (lm,ctxt) = match_subterm nocc c csr in
+  let rec apply_match_subterm app ist nocc (id,c) csr mt =
+    let (lm,ctxt) = 
+      if app then match_appsubterm nocc c csr 
+      else match_subterm nocc c csr 
+    in
     let lctxt = give_context ctxt id in
     let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
     try eval_with_fail {ist with lfun=lm@lctxt@ist.lfun} lz g mt
     with e when is_match_catchable e ->
-      apply_match_subterm ist (nocc + 1) (id,c) csr mt
+      apply_match_subterm app ist (nocc + 1) (id,c) csr mt
   in
   let rec apply_match ist csr = function
     | (All t)::_ ->
@@ -2010,8 +2058,8 @@ and interp_match ist g lz constr lmr =
            debugging_step ist (fun () -> str "switching to the next rule");
            apply_match ist csr tl)
 
-    | (Pat ([],Subterm (id,c),mt))::tl ->
-        (try apply_match_subterm ist 0 (id,c) csr mt
+    | (Pat ([],Subterm (b,id,c),mt))::tl ->
+        (try apply_match_subterm b ist 0 (id,c) csr mt
          with PatternMatchingFailure -> apply_match ist csr tl)
     | _ ->
       errorlabstrm "Tacinterp.apply_match" (str
@@ -2419,13 +2467,16 @@ let subst_raw_may_eval subst = function
   | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)
 
 let subst_match_pattern subst = function
-  | Subterm (ido,pc) -> Subterm (ido,subst_pattern subst pc)
+  | Subterm (b,ido,pc) -> Subterm (b,ido,subst_pattern subst pc)
   | Term pc -> Term (subst_pattern subst pc)
 
 let rec subst_match_context_hyps subst = function
   | Hyp (locs,mp) :: tl ->
       Hyp (locs,subst_match_pattern subst mp)
       :: subst_match_context_hyps subst tl
+  | Def (locs,mv,mp) :: tl ->
+      Def (locs,subst_match_pattern subst mv, subst_match_pattern subst mp)
+      :: subst_match_context_hyps subst tl
   | [] -> []
 
 let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with