Merge branch 'v8.6'

3 files changed, 63 insertions, 38 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 19ca8d50b5..d254520e0e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -288,17 +288,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
-    | { loc; v = PatCstr(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
-      CAst.make ?loc @@ CPatCstr (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
@@ -307,7 +298,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim 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 ->
@@ -321,21 +312,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
-
-
-
-
-
-	| { CAst.v = 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
+		       | _, { CAst.v = 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(List.rev (ip projs args []))
 	    with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6f17324a19..3d484a02da 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -963,6 +963,45 @@ let check_constructor_length env loc cstr len_pl pl0 =
       (error_wrong_numarg_constructor ?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 -> (CAst.make @@ RCPatAtom 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 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
@@ -1200,7 +1239,7 @@ let rec subst_pat_iterator y t = CAst.(map (function
   | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
   | RCPatOr pl -> RCPatOr (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 =
@@ -1355,9 +1394,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
-      CAst.make ?loc @@ RCPatCstr (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
+      CAst.make ?loc @@ RCPatCstr (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 
         (strbrk "Application of arguments to a recursive notation not supported in patterns.");
@@ -1418,7 +1457,7 @@ let rec intern_pat genv aliases pat =
 
 let intern_cases_pattern genv scopes aliases 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 :=
@@ -1427,7 +1466,7 @@ let _ =
 let intern_ind_pattern genv scopes 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
   let loc = no_not.CAst.loc in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 08b9fbe8ec..33b93606ec 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1154,10 +1154,6 @@ 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
-    Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l
 
 let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
   try
@@ -1187,10 +1183,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 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
   | PatCstr ((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 ((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