Merge PR#546: Fix for bug #4499 and other minor related bugs

3 files changed, 64 insertions, 29 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index dd8a48b85..74504e36d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -274,17 +274,8 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
 
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 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 !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
-      let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
-      let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-      CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
-    | _ ->
   try
-    if !Flags.raw_print || !print_no_symbol then raise No_match;
+    if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
     match availability_of_prim_token p sc scopes with
       | None -> raise No_match
@@ -293,7 +284,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
   with No_match ->
     try
-      if !Flags.raw_print || !print_no_symbol then raise No_match;
+      if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
       extern_notation_pattern scopes vars pat
 	(uninterp_cases_pattern_notations pat)
     with No_match ->
@@ -307,16 +298,19 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
               if !Flags.raw_print then raise Exit;
 	      let projs = Recordops.lookup_projections (fst cstrsp) in
 	      let rec ip projs args acc =
-		match projs with
-		  | [] -> acc
-		  | None :: q -> ip q args acc
-		  | Some c :: q ->
-		    match args with
-		      | [] -> raise No_match
-		      | CPatAtom(_, None) :: tail -> ip q tail acc
-		    (* we don't want to have 'x = _' in our patterns *)
-		      | head :: tail -> ip q tail
-		        ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
+		match projs, args with
+		  | [], [] -> acc
+		  | proj :: q, pat :: tail ->
+                     let acc =
+                       match proj, pat with
+		       | _, CPatAtom(_, None) ->
+		          (* we don't want to have 'x := _' in our patterns *)
+                          acc
+		       | Some c, _ ->
+		          ((extern_reference loc Id.Set.empty (ConstRef c), pat) :: acc)
+                       | _ -> raise No_match in
+                     ip q tail acc
+	          | _ -> assert false
 	      in
 	      CPatRecord(loc, List.rev (ip projs args []))
 	    with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4e76fe9aa..8400fdc96 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -960,6 +960,45 @@ let check_constructor_length env loc cstr len_pl pl0 =
       (error_wrong_numarg_constructor_loc loc env cstr
          (Inductiveops.constructor_nrealargs cstr)))
 
+open Term
+open Declarations
+
+(* Similar to Cases.adjust_local_defs but on RCPat *)
+let insert_local_defs_in_pattern (ind,j) l =
+  let (mib,mip) = Global.lookup_inductive ind in
+  if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
+    (* Optimisation *) l
+  else
+    let typi = mip.mind_nf_lc.(j-1) in
+    let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in
+    let (decls,_) = decompose_prod_assum typi in
+    let rec aux decls args =
+      match decls, args with
+      | Context.Rel.Declaration.LocalDef _ :: decls, args -> Constrexpr.RCPatAtom (Loc.ghost,None) :: aux decls args
+      | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *)
+      | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
+      | _ -> assert false in
+    aux (List.rev decls) l
+
+let add_local_defs_and_check_length loc env g pl args = match g with
+  | ConstructRef cstr ->
+     (* We consider that no variables corresponding to local binders
+        have been given in the "explicit" arguments, which come from a
+        "@C args" notation or from a custom user notation *)
+     let pl' = insert_local_defs_in_pattern cstr pl in
+     let maxargs = Inductiveops.constructor_nalldecls cstr in
+     if List.length pl' + List.length args > maxargs then
+       error_wrong_numarg_constructor_loc loc env cstr (Inductiveops.constructor_nrealargs cstr);
+     (* Two possibilities: either the args are given with explict
+     variables for local definitions, then we give the explicit args
+     extended with local defs, so that there is nothing more to be
+     added later on; or the args are not enough to have all arguments,
+     which a priori means local defs to add in the [args] part, so we
+     postpone the insertion of local defs in the explicit args *)
+     (* Note: further checks done later by check_constructor_length *)
+     if List.length pl' + List.length args = maxargs then pl' else pl
+  | _ -> pl
+
 let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
   let impl_list = if Int.equal len_pl1 0
     then select_impargs_size (List.length pl2) impls_st
@@ -1198,7 +1237,7 @@ let rec subst_pat_iterator y t p = match p with
   | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a)
   | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl)
 
-let drop_notations_pattern looked_for =
+let drop_notations_pattern looked_for genv =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
      only constructor are allowed *)
   let ensure_kind top loc g =
@@ -1327,9 +1366,9 @@ let drop_notations_pattern looked_for =
     | NApp (NRef g,pl) ->
       ensure_kind top loc g;
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
-      RCPatCstr (loc, g,
-		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
-		 List.map (in_pat false scopes) args, [])
+      let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in
+      let pl = add_local_defs_and_check_length loc genv g pl args in
+      RCPatCstr (loc, g, pl @ List.map (in_pat false scopes) args, [])
     | NList (x,y,iter,terminator,lassoc) ->
       if not (List.is_empty args) then user_err_loc
         (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
@@ -1422,7 +1461,7 @@ and check_no_patcast_subst (pl,pll) =
 let intern_cases_pattern genv scopes aliases pat =
   check_no_patcast pat;
   intern_pat genv aliases
-    (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
+    (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat)
 
 let _ =
   intern_cases_pattern_fwd :=
@@ -1432,7 +1471,7 @@ let intern_ind_pattern genv scopes pat =
   check_no_patcast pat;
   let no_not =
     try
-      drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
+      drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
     with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc
   in
   match no_not with
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0c5393cf4..564882153 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1158,6 +1158,7 @@ let match_notation_constr u c (metas,pat) =
     metas ([],[],[])
 
 (* Matching cases pattern *)
+
 let add_patterns_for_params ind l =
   let mib,_ = Global.lookup_inductive ind in
   let nparams = mib.Declarations.mind_nparams in
@@ -1190,10 +1191,11 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
   | PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
   | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
-      sigma,(0,add_patterns_for_params (fst r1) largs)
+      let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
+      sigma,(0,l)
   | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
-      let l1 = add_patterns_for_params (fst r1) args1 in
+      let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
       if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
       then