Boolean Option Patterns Compatibility

switch between "all arguments no parameters" and "explicit params and args"
for constructor arguments in patterns.

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

4 files changed, 76 insertions, 16 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c0d597d2f1..dc328ce75a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -324,6 +324,21 @@ let mkPat loc qid l =
 let add_patt_for_params (ind,k) l =
     Util.list_addn (Inductiveops.inductive_nparams ind) (CPatAtom (dummy_loc,None)) l
 
+let drop_implicits_in_patt c args =
+  let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
+  let rec impls_fit l = function
+    |[],t -> Some (List.rev_append l t)
+    |_,[] -> None
+    |h::t,CPatAtom(_,None)::tt when is_status_implicit h -> impls_fit l (t,tt)
+    |h::_,_ when is_status_implicit h -> None
+    |_::t,hh::tt -> impls_fit (hh::l) (t,tt)
+  in let rec aux = function
+    |[] -> None
+    |(_,imps)::t -> match impls_fit [] (imps,args) with
+	|None -> aux t
+	|x -> x
+     in aux impl_st
+
 let pattern_printable_in_both_syntax (ind,_ as c) =
   let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
   let nb_params = Inductiveops.inductive_nparams ind in
@@ -373,10 +388,16 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	      CPatRecord(loc, List.rev (ip projs args []))
 	    with
 		Not_found | No_match | Exit ->
-		  if pattern_printable_in_both_syntax cstrsp
-		  then CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args)
-		  else CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), add_patt_for_params cstrsp args) in
-	  insert_pat_alias loc p na
+		  if !Topconstr.oldfashion_patterns then
+		    if pattern_printable_in_both_syntax cstrsp
+		    then CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args)
+		    else CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), add_patt_for_params cstrsp args)
+		  else
+		    let full_args = add_patt_for_params cstrsp args in
+		    match drop_implicits_in_patt cstrsp full_args with
+		      |Some true_args -> CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), true_args)
+		      |None -> CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), full_args)
+	  in insert_pat_alias loc p na
 
 and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0f5d66282f..7b0d4ff2b8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -750,10 +750,10 @@ let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
 let product_of_cases_patterns ids idspl =
   List.fold_right (fun (ids,pl) (ids',ptaill) ->
     (ids@ids',
-    (* Cartesian prod of the or-pats for the nth arg and the tail args *)
-    List.flatten (
-    List.map (fun (subst,p) ->
-      List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)))
+     (* Cartesian prod of the or-pats for the nth arg and the tail args *)
+     List.flatten (
+       List.map (fun (subst,p) ->
+	 List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)))
     idspl (ids,[[],[]])
 
 let simple_product_of_cases_patterns pl =
@@ -797,6 +797,23 @@ let check_constructor_length env loc cstr with_params pl pl0 =
       (error_wrong_numarg_constructor_loc loc env cstr
 	 (if with_params then nargs else nargs - (Inductiveops.inductive_nparams (fst cstr))))
 
+let add_implicits_check_constructor_length env loc c idslpl1 pl2 =
+  let nargs = Inductiveops.mis_constructor_nargs c in
+  let len_pl1 = List.length idslpl1 in
+  let impls_st = implicits_of_global (ConstructRef c) in
+  let impl_list = if len_pl1 = 0
+    then select_impargs_size (List.length pl2) impls_st
+    else snd (list_chop len_pl1 (select_stronger_impargs impls_st)) in
+  let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in
+  let rec aux i = function
+    |[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in
+	     if args_len = nargs then l
+	     else error_wrong_numarg_constructor_loc loc env c (nargs - List.length impl_list + i)
+    |imp::q,l when is_status_implicit imp -> CPatAtom(loc,None):: aux i (q,l)
+    |il,[] -> error_wrong_numarg_constructor_loc loc env c (remaining_args (len_pl1+i) il)
+    |_::q,hh::tt -> hh::aux (succ i) (q,tt)
+  in aux 0 (impl_list,pl2)
+
 (* Manage multiple aliases *)
 
   (* [merge_aliases] returns the sets of all aliases encountered at this
@@ -932,9 +949,9 @@ let find_pattern_variable = function
   | Ident (loc,id) -> id
   | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
 
-let maybe_constructor ref f aliases env =
+let maybe_constructor add_params ref f aliases env =
   try
-    let c,idspl1,pl2 = find_constructor (Some 0) ref f aliases [] env in
+    let c,idspl1,pl2 = find_constructor add_params ref f aliases [] env in
     assert (pl2 = []);
     ConstrPat (c,idspl1)
   with
@@ -1062,9 +1079,14 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
 	  in
 	intern_pat env aliases self_patt
   | CPatCstr (loc, head, pl) ->
-      let c,idslpl1,pl2 = mustbe_constructor loc (Some (List.length pl)) head intern_pat aliases pl env in
-      let with_letin = check_constructor_length genv loc c false idslpl1 pl2 in
-      intern_cstr_with_all_args loc c with_letin idslpl1 pl2
+      if !Topconstr.oldfashion_patterns then
+	let c,idslpl1,pl2 = mustbe_constructor loc (Some (List.length pl)) head intern_pat aliases pl env in
+	let with_letin = check_constructor_length genv loc c false idslpl1 pl2 in
+	intern_cstr_with_all_args loc c with_letin idslpl1 pl2
+      else
+	let c,idslpl1,pl2 = mustbe_constructor loc None head intern_pat aliases pl env in
+	let pl2' = add_implicits_check_constructor_length genv loc c idslpl1 pl2 in
+	intern_cstr_with_all_args loc c false idslpl1 pl2'
   | CPatCstrExpl (loc, head, pl) ->
       let c,idslpl1,pl2 = mustbe_constructor loc None head intern_pat aliases pl env in
       let with_letin = check_constructor_length genv loc c true idslpl1 pl2 in
@@ -1094,10 +1116,15 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
       intern_pat {env with scopes=find_delimiters_scope loc key::env.scopes;
 		    tmp_scope = None} aliases e
   | CPatAtom (loc, Some head) ->
-      (match maybe_constructor head intern_pat aliases env with
+      (match maybe_constructor (if !Topconstr.oldfashion_patterns then Some 0 else None)
+	  head intern_pat aliases env with
 	 | ConstrPat (c,idspl) ->
-	   let with_letin = check_constructor_length genv loc c false idspl [] in
-	   intern_cstr_with_all_args loc c with_letin idspl []
+	   if !Topconstr.oldfashion_patterns then
+	     let with_letin = check_constructor_length genv loc c false idspl [] in
+	     intern_cstr_with_all_args loc c with_letin idspl []
+	   else
+	     let pl2 = add_implicits_check_constructor_length genv loc c idspl [] in
+	     intern_cstr_with_all_args loc c false idspl pl2
 	 | VarPat id ->
 	     let ids,asubst = merge_aliases aliases id in
 	     (ids,[asubst, PatVar (loc,alias_of (ids,asubst))]))
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index ab85f84651..0db70e59c1 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -916,6 +916,16 @@ and typeclass_context = typeclass_constraint list
 
 type constr_pattern_expr = constr_expr
 
+let oldfashion_patterns = ref (true)
+let write_oldfashion_patterns = Goptions.declare_bool_option {
+  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optname =
+    "Constructors in atterns require all their arguments but no parameters instead of explicit parameters and arguments";
+  Goptions.optkey = ["Asymmetric";"Patterns"];
+  Goptions.optread = (fun () -> !oldfashion_patterns);
+  Goptions.optwrite = (fun a -> oldfashion_patterns:=a);
+}
+
 (***********************)
 (* For binders parsing *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 66aa1ba58c..524df4e1b6 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -193,6 +193,8 @@ and typeclass_context = typeclass_constraint list
 
 type constr_pattern_expr = constr_expr
 
+val oldfashion_patterns : bool ref
+
 (** Utilities on constr_expr                                           *)
 
 val constr_loc : constr_expr -> loc