Notations are back in the "in" clause of pattern matching.

Fixes the test-suite.

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

6 files changed, 145 insertions, 69 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9fdf57ad9f..d0e26b3baf 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -355,7 +355,8 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
   match pat with
-    | PatCstr(loc,cstrsp,args,na) when Inductiveops.mis_constructor_has_local_defs cstrsp ->
+    | PatCstr(loc,cstrsp,args,na)
+	when !in_debugger||Inductiveops.mis_constructor_has_local_defs cstrsp ->
       let c = extern_reference loc Idset.empty (ConstructRef cstrsp) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       CPatCstrExpl (loc, c, add_patt_for_params (fst cstrsp) args)
@@ -399,7 +400,6 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	    with
 		Not_found | No_match | Exit ->
                   let c = extern_reference loc Idset.empty (ConstructRef cstrsp) in
-                  if !in_debugger then CPatCstr (loc, c, args) else
 		  if !Topconstr.oldfashion_patterns then
 		    if pattern_printable_in_both_syntax cstrsp
 		    then CPatCstr (loc, c, args)
@@ -410,57 +410,92 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 		      |Some true_args -> CPatCstr (loc, c, true_args)
 		      |None -> CPatCstrExpl (loc, c, full_args)
 	  in insert_pat_alias loc p na
-
+and apply_notation_to_pattern loc ((subst,substlist),more_args) (tmp_scope, scopes as allscopes) vars =
+  function
+    | NotationRule (sc,ntn) ->
+      begin match more_args with
+	|_::_ ->
+	  (* Parser and Constrintern do not understand a notation for
+	     partially applied constructor. *)
+	  raise No_match
+	|[] ->
+	  match availability_of_notation (sc,ntn) allscopes with
+	    (* Uninterpretation is not allowed in current context *)
+	    | None -> raise No_match
+	    (* Uninterpretation is allowed in current context *)
+	    | Some (scopt,key) ->
+	      let scopes' = Option.List.cons scopt scopes in
+	      let l =
+		List.map (fun (c,(scopt,scl)) ->
+		  extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
+		  subst in
+	      let ll =
+		List.map (fun (c,(scopt,scl)) ->
+		  let subscope = (scopt,scl@scopes') in
+		  List.map (extern_cases_pattern_in_scope subscope vars) c)
+		  substlist in
+	      insert_pat_delimiters loc
+		(make_pat_notation loc ntn (l,ll)) key
+      end
+    | SynDefRule kn ->
+      let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+      let l1 =
+	List.rev_map (fun (c,(scopt,scl)) ->
+          extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
+          subst in
+      let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+      assert (substlist = []);
+      mkPat loc qid (List.rev_append l1 l2)
 and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
-      match t,n with
-	| PatCstr (loc,_,_,na),_ ->
-	  (* Try matching ... *)
-	  let (subst,substlist),more_args = match_aconstr_cases_pattern t pat in
-	  (* Try availability of interpretation ... *)
-	  let p = match keyrule with
-            | NotationRule (sc,ntn) ->
-	      begin match more_args with
-		|_::_ ->
-		  (* Parser and Constrintern do not understand a notation for
-		     partially applied constructor. *)
-		  raise No_match
-		|[] ->
-		  match availability_of_notation (sc,ntn) allscopes with
-		    (* Uninterpretation is not allowed in current context *)
-		    | None -> raise No_match
-		    (* Uninterpretation is allowed in current context *)
-		    | Some (scopt,key) ->
-	              let scopes' = Option.List.cons scopt scopes in
-	              let l =
-			List.map (fun (c,(scopt,scl)) ->
-			  extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
-			  subst in
-		      let ll =
-			List.map (fun (c,(scopt,scl)) ->
-			  let subscope = (scopt,scl@scopes') in
-			  List.map (extern_cases_pattern_in_scope subscope vars) c)
-			  substlist in
-		      insert_pat_delimiters loc
-			(make_pat_notation loc ntn (l,ll)) key
-	      end
-            | SynDefRule kn ->
-	      let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
-	      let l1 =
-		List.rev_map (fun (c,(scopt,scl)) ->
-                  extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
-                  subst in
-	      let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
-              assert (substlist = []);
-	      mkPat loc qid (List.rev_append l1 l2) in
+      match t with
+	| PatCstr (loc,_,_,na) ->
+	  let p = apply_notation_to_pattern loc
+	    (match_aconstr_cases_pattern t pat) allscopes vars keyrule in
 	  insert_pat_alias loc p na
-	| PatVar (loc,Anonymous),_ -> CPatAtom (loc, None)
-	| PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id)))
+	| PatVar (loc,Anonymous) -> CPatAtom (loc, None)
+	| PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id)))
     with
 	No_match -> extern_symbol_pattern allscopes vars t rules
 
+let rec extern_symbol_ind_pattern allscopes vars ind args = function
+  | [] -> raise No_match
+  | (keyrule,pat,n as _rule)::rules ->
+    try
+      apply_notation_to_pattern dummy_loc
+	(match_aconstr_ind_pattern ind args pat) allscopes vars keyrule
+    with
+	No_match -> extern_symbol_ind_pattern allscopes vars ind args rules
+
+let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
+  (* pboutill: There are letins in pat which is incompatible with notations and
+     not explicit application. *)
+  if !in_debugger||Inductiveops.inductive_has_local_defs ind then
+    let c = extern_reference dummy_loc vars (IndRef ind) in
+    let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+    CPatCstrExpl (dummy_loc, c, add_patt_for_params ind args)
+  else
+    try
+      if !Flags.raw_print or !print_no_symbol then raise No_match;
+      let (sc,p) = uninterp_prim_token_ind_pattern ind args in
+      match availability_of_prim_token p sc scopes with
+	| None -> raise No_match
+	| Some key ->
+	  insert_pat_delimiters dummy_loc (CPatPrim(dummy_loc,p)) key
+    with No_match ->
+      try
+	if !Flags.raw_print or !print_no_symbol then raise No_match;
+	extern_symbol_ind_pattern scopes vars ind args
+	  (uninterp_ind_pattern_notations ind)
+    with No_match ->
+      let c = extern_reference dummy_loc vars (IndRef ind) in
+      let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+      match drop_implicits_in_patt ind args with
+	   |Some true_args -> CPatCstr (dummy_loc, c, true_args)
+	   |None -> CPatCstrExpl (dummy_loc, c, args)
+
 let extern_cases_pattern vars p =
   extern_cases_pattern_in_scope (None,[]) vars p
 
@@ -721,16 +756,9 @@ let rec extern inctx scopes vars r =
         | Name _, _ -> Some (dummy_loc,na) in
       (sub_extern false scopes vars tm,
        (na',Option.map (fun (loc,ind,nal) ->
-	 let args = List.map (fun x -> CPatAtom (dummy_loc, match x with Anonymous -> None | Name id -> Some (Ident (dummy_loc,id)))) nal in
-	 let full_args = add_patt_for_params ind args in
-	 let c = extern_reference loc vars (IndRef ind) in
-	 (* pboutill: There are letins in full_args which is incompatible with not
-	    explicit application. *)
-	 if Inductiveops.inductive_has_local_defs ind
-	 then CPatCstrExpl (dummy_loc, c, full_args)
-	 else match drop_implicits_in_patt ind full_args with
-	   |Some true_args -> CPatCstr (dummy_loc, c, true_args)
-	   |None -> CPatCstrExpl (dummy_loc, c, full_args)
+	 let args = List.map (fun x -> PatVar (dummy_loc, x)) nal in
+	 let fullargs = Topconstr.add_patterns_for_params ind args in
+	 extern_ind_pattern_in_scope scopes vars ind fullargs
 	) x))) tml in
     let eqns = List.map (extern_eqn inctx scopes vars) eqns in
     CCases (loc,sty,rtntypopt',tml,eqns)
diff --git a/interp/notation.ml b/interp/notation.ml
index 102d42c213..72a7138669 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -387,6 +387,9 @@ let uninterp_notations c =
 let uninterp_cases_pattern_notations c =
   Gmapl.find (cases_pattern_key c) !notations_key_table
 
+let uninterp_ind_pattern_notations ind =
+  Gmapl.find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
+
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
     Gmap.mem ntn (Gmap.find scope !scope_map).notations in
@@ -401,6 +404,20 @@ let uninterp_prim_token c =
       | Some n -> (sc,n)
   with Not_found -> raise No_match
 
+let uninterp_prim_token_ind_pattern ind args =
+  let ref = IndRef ind in
+  try
+    let (sc,numpr,b) = Hashtbl.find prim_token_key_table
+      (RefKey (canonical_gr ref)) in
+    if not b then raise No_match;
+    let args' = List.map
+      (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
+    let ref = GRef (dummy_loc,ref) in
+    match numpr (GApp (dummy_loc,ref,args')) with
+      | None -> raise No_match
+      | Some n -> (sc,n)
+  with Not_found -> raise No_match
+
 let uninterp_prim_token_cases_pattern c =
   try
     let k = cases_pattern_key c in
diff --git a/interp/notation.mli b/interp/notation.mli
index 1a02bc8a2c..6eaac73dbe 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -94,6 +94,8 @@ val uninterp_prim_token :
   glob_constr -> scope_name * prim_token
 val uninterp_prim_token_cases_pattern :
   cases_pattern -> name * scope_name * prim_token
+val uninterp_prim_token_ind_pattern :
+ inductive -> cases_pattern list -> scope_name * prim_token
 
 val availability_of_prim_token :
   prim_token -> scope_name -> local_scopes -> delimiters option option
@@ -119,6 +121,8 @@ val uninterp_notations : glob_constr ->
       (interp_rule * interpretation * int option) list
 val uninterp_cases_pattern_notations : cases_pattern ->
       (interp_rule * interpretation * int option) list
+val uninterp_ind_pattern_notations : inductive ->
+      (interp_rule * interpretation * int option) list
 
 (** Test if a notation is available in the scopes 
    context [scopes]; if available, the result is not None; the first 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cbbf384a89..9cad91068c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -786,7 +786,7 @@ let match_aconstr u c (metas,pat) =
     metas ([],[],[])
 
 (* Matching cases pattern *)
-let add_patterns_for_params (ind,k) l =
+let add_patterns_for_params ind l =
   let mib,_ = Global.lookup_inductive ind in
   let nparams = mib.Declarations.mind_nparams in
     Util.list_addn nparams (PatVar (dummy_loc,Anonymous)) l
@@ -800,10 +800,6 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
     (var,v)::sigma,sigmalist,x
 
 let rec match_cases_pattern metas sigma a1 a2 =
-  let match_cases_pattern_no_more_args metas sigma a1 a2 =
-    match match_cases_pattern metas sigma a1 a2 with
-      |out,[] -> out
-      |_ -> raise No_match in
  match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[]
   | PatVar (_,Anonymous), AHole _ -> sigma,[]
@@ -811,7 +807,7 @@ let rec match_cases_pattern metas sigma a1 a2 =
       sigma,largs
   | PatCstr (loc,(ind,_ as r1),args1,_), AApp (ARef (ConstructRef r2),l2)
       when r1 = r2 ->
-      let l1 = add_patterns_for_params r1 args1 in
+      let l1 = add_patterns_for_params (fst r1) args1 in
       let le2 = List.length l2 in
       if le2 > List.length l1
       then
@@ -823,17 +819,43 @@ let rec match_cases_pattern metas sigma a1 a2 =
       (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas)
 	(metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),[]
   | _ -> raise No_match
+and match_cases_pattern_no_more_args metas sigma a1 a2 =
+    match match_cases_pattern metas sigma a1 a2 with
+      |out,[] -> out
+      |_ -> raise No_match
+
+let match_ind_pattern metas sigma ind pats a2 =
+  match a2 with
+  | ARef (IndRef r2) when ind = r2 ->
+      sigma,pats
+  | AApp (ARef (IndRef r2),l2)
+      when ind = r2 ->
+      let le2 = List.length l2 in
+      if le2 > List.length pats
+      then
+	raise No_match
+      else
+	let l1',more_args = Util.list_chop le2 pats in
+	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args
+  |_ -> raise No_match
+
+let reorder_canonically_substitution terms termlists metas =
+  List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
+    match typ with
+      | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists')
+      | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists')
+      | NtnTypeBinderList -> assert false)
+    metas ([],[])
 
 let match_aconstr_cases_pattern c (metas,pat) =
   let vars = List.map fst metas in
   let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in
-  (* Reorder canonically the substitution *)
-  (List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
-    match typ with
-    | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists')
-    | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists')
-    | NtnTypeBinderList -> assert false)
-    metas ([],[])),more_args
+  reorder_canonically_substitution terms termlists metas,more_args
+
+let match_aconstr_ind_pattern ind args (metas,pat) =
+  let vars = List.map fst metas in
+  let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in
+  reorder_canonically_substitution terms termlists metas,more_args
 
 (**********************************************************************)
 (*s Concrete syntax for terms *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 518ae06b8f..a7871d41ba 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -100,6 +100,9 @@ val match_aconstr : bool -> glob_constr -> interpretation ->
 val match_aconstr_cases_pattern :  cases_pattern -> interpretation ->
       ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list)
 
+val match_aconstr_ind_pattern : inductive -> cases_pattern  list -> interpretation ->
+      ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list)
+
 (** Substitution of kernel names in interpretation data                *)
 
 val subst_interpretation : substitution -> interpretation -> interpretation
@@ -273,3 +276,5 @@ val patntn_loc :
 (** For cases pattern parsing errors *)
 
 val error_invalid_pattern_notation : Pp.loc -> 'a
+
+val add_patterns_for_params : inductive -> cases_pattern list -> cases_pattern list
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index c99e03276e..14dc16072b 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -2,7 +2,7 @@ t_rect =
 fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
-  | k _ x0 => f x0 (F x0)
+  | @k _ x0 => f x0 (F x0)
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t