In the syntax of pattern matching, "in" clauses are patterns.

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

4 files changed, 162 insertions, 81 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b3810bb6d..f7bd32815 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -705,29 +705,26 @@ let rec extern inctx scopes vars r =
       CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 
   | GCases (loc,sty,rtntypopt,tml,eqns) ->
-      let vars' =
-	List.fold_right (name_fold Idset.add)
-	  (cases_predicate_names tml) vars in
-      let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
-      let tml = List.map (fun (tm,(na,x)) ->
-        let na' = match na,tm with
-            Anonymous, GVar (_,id) when
-              rtntypopt<>None & occur_glob_constr id (Option.get rtntypopt)
-              -> Some (dummy_loc,Anonymous)
-          | Anonymous, _ -> None
-          | Name id, GVar (_,id') when id=id' -> None
-          | Name _, _ -> Some (dummy_loc,na) in
-	(sub_extern false scopes vars tm,
-	(na',Option.map (fun (loc,ind,n,nal) ->
-	  let params = list_tabulate
-	    (fun _ -> GHole (dummy_loc,Evd.InternalHole)) n in
-	  let args = List.map (function
-	    | Anonymous -> GHole (dummy_loc,Evd.InternalHole)
-	    | Name id -> GVar (dummy_loc,id)) nal in
-	  let t = GApp (dummy_loc,GRef (dummy_loc,IndRef ind),params@args) in
-	  (extern_typ scopes vars t)) x))) tml in
-      let eqns = List.map (extern_eqn inctx scopes vars) eqns in
-      CCases (loc,sty,rtntypopt',tml,eqns)
+    let vars' =
+      List.fold_right (name_fold Idset.add)
+	(cases_predicate_names tml) vars in
+    let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
+    let tml = List.map (fun (tm,(na,x)) ->
+      let na' = match na,tm with
+          Anonymous, GVar (_,id) when
+	      rtntypopt<>None & occur_glob_constr id (Option.get rtntypopt)
+	      -> Some (dummy_loc,Anonymous)
+        | Anonymous, _ -> None
+        | Name id, GVar (_,id') when id=id' -> None
+        | Name _, _ -> Some (dummy_loc,na) in
+      (sub_extern false scopes vars tm,
+       (na',Option.map (fun (loc,ind,n,nal) ->
+	 let params = list_tabulate
+	   (fun _ -> CPatAtom (dummy_loc,None)) n in
+	 let args = List.map (fun x -> CPatAtom (dummy_loc, match x with Anonymous -> None | Name id -> Some (Ident (dummy_loc,id)))) nal in
+	 CPatCstr (dummy_loc, extern_reference loc vars (IndRef ind),params@args)) x))) tml in
+    let eqns = List.map (extern_eqn inctx scopes vars) eqns in
+    CCases (loc,sty,rtntypopt',tml,eqns)
 
   | GLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal,
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 12376eb89..992cf3edf 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -741,10 +741,10 @@ let rec simple_adjust_scopes n scopes =
   | [] -> None :: simple_adjust_scopes (n-1) []
   | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
 
-let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
+let find_remaining_scopes pl1 pl2 ref =
   snd (list_chop (List.length pl1)
     (simple_adjust_scopes (List.length pl1 + List.length pl2)
-      (find_arguments_scope (ConstructRef cstr))))
+      (find_arguments_scope ref)))
 
 (**********************************************************************)
 (* Cases                                                              *)
@@ -799,10 +799,7 @@ 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 add_implicits_check_length nargs impls_st len_pl1 pl2 fail =
   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
@@ -810,12 +807,35 @@ let add_implicits_check_constructor_length env loc c idslpl1 pl2 =
   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)
+	     else fail (nargs - List.length impl_list + i)
+    |imp::q,l when is_status_implicit imp -> CPatAtom(dummy_loc,None):: aux i (q,l)
+    |il,[] -> fail (remaining_args (len_pl1+i) il)
     |_::q,hh::tt -> hh::aux (succ i) (q,tt)
   in aux 0 (impl_list,pl2)
 
+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
+  add_implicits_check_length nargs impls_st len_pl1 pl2
+    (error_wrong_numarg_constructor_loc loc env c)
+
+let check_ind_length env loc ind pl pl0 =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let nparams = mib.Declarations.mind_nparams in
+  let nargs = mip.Declarations.mind_nrealargs + nparams in
+  let n = List.length pl + List.length pl0 in
+  if n = nargs then nparams else
+      (error_wrong_numarg_inductive_loc loc env ind nargs)
+
+let add_implicits_check_ind_length env loc c idslpl1 pl2 =
+  let (mib,mip) = Global.lookup_inductive c in
+  let nparams = mib.Declarations.mind_nparams in
+  let nargs = mip.Declarations.mind_nrealargs + nparams in
+  let len_pl1 = List.length idslpl1 in
+  let impls_st = implicits_of_global (IndRef c) in
+  nparams, add_implicits_check_length nargs impls_st len_pl1 pl2
+    (error_wrong_numarg_inductive_loc loc env c)
 (* Manage multiple aliases *)
 
   (* [merge_aliases] returns the sets of all aliases encountered at this
@@ -903,19 +923,39 @@ let subst_cases_pattern loc alias intern fullsubst env a =
   | t -> error_invalid_pattern_notation loc
   in aux alias fullsubst a
 
+let subst_ind_pattern loc intern_ind_patt intern (subst,_ as fullsubst) env = function
+  | AVar id ->
+      begin
+	(* subst remembers the delimiters stack in the interpretation *)
+	(* of the notations *)
+	try
+	  let (a,(scopt,subscopes)) = List.assoc id subst in
+	    intern_ind_patt {env with scopes=subscopes@env.scopes;
+		      tmp_scope = scopt} a
+	with Not_found ->
+	  anomaly ("Unbound pattern notation variable: "^(string_of_id id))
+      end
+  | ARef (IndRef c) ->
+      Inductiveops.inductive_nparams c, (c, [])
+  | AApp (ARef (IndRef ind),args) ->
+      let idslpll = List.map (subst_cases_pattern loc Anonymous intern fullsubst env) args in
+      begin
+	match product_of_cases_patterns [] idslpll with
+	  |_,[_,pl]->
+	    let pl' = chop_params_pattern loc (ind,42) pl false in
+            Inductiveops.inductive_nparams ind, (ind,pl')
+	  |_ ->  error_invalid_pattern_notation loc
+      end
+  | t -> error_invalid_pattern_notation loc
+
+
 (* Differentiating between constructors and matching variables *)
 type pattern_qualid_kind =
   | ConstrPat of constructor * (identifier list *
       ((identifier * identifier) list * cases_pattern) list) list
   | VarPat of identifier
 
-let find_constructor add_params ref f aliases pats env =
-  let add_params (ind,_ as c) = match add_params with
-    |Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c
-      then fst (Inductiveops.inductive_nargs ind)
-      else Inductiveops.inductive_nparams ind in
-      Util.list_make nb ([],[([],PatVar(dummy_loc,Anonymous))])
-    |None -> [] in
+let find_at_head looked_for add_params ref f pats env =
   let (loc,qid) = qualid_of_reference ref in
   let gref =
     try locate_extended qid
@@ -924,10 +964,12 @@ let find_constructor add_params ref f aliases pats env =
     | SynDef sp ->
       let (vars,a) = Syntax_def.search_syntactic_definition sp in
       (match a with
-	| ARef (ConstructRef cstr) ->
+	| ARef g ->
+	  let cstr = looked_for g in
 	  assert (vars=[]);
 	  cstr,add_params cstr, pats
-	| AApp (ARef (ConstructRef cstr),args) ->
+	| AApp (ARef g,args) ->
+	  let cstr = looked_for g in
 	  let nvars = List.length vars in
 	  if List.length pats < nvars then error_not_enough_arguments loc;
 	  let pats1,pats2 = list_chop nvars pats in
@@ -941,19 +983,29 @@ let find_constructor add_params ref f aliases pats env =
         | ConstRef cst ->
 	  let v = Environ.constant_value (Global.env()) cst in
 	  unf (global_of_constr v)
-        | ConstructRef cstr ->
+        | g ->
+	  let cstr = looked_for g in
 	  Dumpglob.add_glob loc r;
 	  cstr, add_params cstr, pats
-        | _ -> raise Not_found
       in unf r
 
+let find_constructor add_params =
+  find_at_head (function ConstructRef cstr -> cstr |_ -> raise Not_found)
+    (function (ind,_ as c) -> match add_params with
+      |Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c
+	then fst (Inductiveops.inductive_nargs ind)
+	else Inductiveops.inductive_nparams ind in
+		       Util.list_make nb ([],[([],PatVar(dummy_loc,Anonymous))])
+      |None -> [])
+
+
 let find_pattern_variable = function
   | Ident (loc,id) -> id
   | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
 
-let maybe_constructor add_params ref f aliases env =
+let maybe_constructor add_params ref f env =
   try
-    let c,idspl1,pl2 = find_constructor add_params ref f aliases [] env in
+    let c,idspl1,pl2 = find_constructor add_params ref f [] env in
     assert (pl2 = []);
     ConstrPat (c,idspl1)
   with
@@ -965,11 +1017,17 @@ let maybe_constructor add_params ref f aliases env =
 			     str " is understood as a pattern variable");
       VarPat (find_pattern_variable ref)
 
-let mustbe_constructor loc add_params ref f aliases patl env =
-  try find_constructor add_params ref f aliases patl env
+let mustbe_constructor loc add_params ref f patl env =
+  try find_constructor add_params ref f patl env
   with (Environ.NotEvaluableConst _ | Not_found) ->
     raise (InternalizationError (loc,NotAConstructor ref))
 
+let mustbe_inductive loc ref f patl env =
+  try find_at_head (function IndRef ind -> ind|_ -> raise Not_found) (function _ -> []) ref f patl env
+  with (Environ.NotEvaluableConst _ | Not_found|
+      InternalizationError (_,NotAConstructor _)) ->
+    error_bad_inductive_type loc
+
 let sort_fields mode loc l completer =
 (*mode=false if pattern and true if constructor*)
   match l with
@@ -1062,7 +1120,7 @@ let sort_fields mode loc l completer =
 let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
   let intern_pat = intern_cases_pattern genv in
   let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
-    let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
+    let argscs2 = find_remaining_scopes idslpl1 pl2 (ConstructRef c) in
     let idslpl2 = List.map2 (fun x -> intern_pat {env with tmp_scope = x} ([],[])) argscs2 pl2 in
     let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
     let pl' = List.map (fun (asubst,pl) ->
@@ -1082,15 +1140,15 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
 	intern_pat env aliases self_patt
   | CPatCstr (loc, head, pl) ->
       if !Topconstr.oldfashion_patterns then
-	let c,idslpl1,pl2 = mustbe_constructor loc (Some (List.length pl)) head intern_pat aliases pl env in
+	let c,idslpl1,pl2 = mustbe_constructor loc (Some (List.length pl)) head intern_pat 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 c,idslpl1,pl2 = mustbe_constructor loc None head intern_pat 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 c,idslpl1,pl2 = mustbe_constructor loc None head intern_pat pl env in
       let with_letin = check_constructor_length genv loc c true idslpl1 pl2 in
       intern_cstr_with_all_args loc c with_letin idslpl1 pl2
   | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]))
@@ -1119,7 +1177,7 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
 		    tmp_scope = None} aliases e
   | CPatAtom (loc, Some head) ->
       (match maybe_constructor (if !Topconstr.oldfashion_patterns then Some 0 else None)
-	  head intern_pat aliases env with
+	  head intern_pat env with
 	 | ConstrPat (c,idspl) ->
 	   if !Topconstr.oldfashion_patterns then
 	     let with_letin = check_constructor_length genv loc c false idspl [] in
@@ -1140,6 +1198,46 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
       check_or_pat_variables loc ids (List.tl idsl);
       (ids,List.flatten pl')
 
+let rec intern_ind_pattern genv env pat =
+  let intern_ind_with_all_args loc c idslpl1 pl2 =
+    let argscs2 = find_remaining_scopes idslpl1 pl2 (IndRef c) in
+    let idslpl2 = List.map2 (fun x -> intern_cases_pattern genv {env with tmp_scope = x} ([],[])) argscs2 pl2 in
+    match product_of_cases_patterns [] (idslpl1@idslpl2) with
+      |_,[_,pl] ->
+	(c,chop_params_pattern loc (c,42) pl false)
+      |_ -> error_bad_inductive_type loc
+  in
+  match pat with
+    | CPatCstr (loc, head, pl) ->
+      let c,idslpl1,pl2 = mustbe_inductive loc head (intern_cases_pattern genv) pl env in
+      let nargs,pl2' = add_implicits_check_ind_length genv loc c idslpl1 pl2 in
+      nargs,intern_ind_with_all_args loc c idslpl1 pl2'
+    | CPatCstrExpl (loc, head, pl) ->
+      let c,idslpl1,pl2 = mustbe_inductive loc head (intern_cases_pattern genv) pl env in
+      let nargs = check_ind_length genv loc c idslpl1 pl2 in
+      nargs,intern_ind_with_all_args loc c idslpl1 pl2
+    | CPatNotation (_,"( _ )",([a],[])) ->
+      intern_ind_pattern genv env a
+    | CPatNotation (loc, ntn, fullargs) ->
+      let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
+      let ((ids',c),df) = Notation.interp_notation loc ntn (env.tmp_scope,env.scopes) in
+      let (ids',idsl',_) = split_by_type ids' in
+      Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
+      let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
+      let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
+      let ids'',pl =
+	subst_ind_pattern loc (intern_ind_pattern genv) (intern_cases_pattern genv) (subst,substlist)
+	  env c
+      in ids'', pl
+    | CPatDelimiters (loc, key, e) ->
+      intern_ind_pattern genv {env with scopes=find_delimiters_scope loc key::env.scopes;
+	tmp_scope = None} e
+    | CPatAtom (loc, Some head) ->
+      let c,idslpl1,pl2 = mustbe_inductive loc head (intern_cases_pattern genv) [] env in
+      let nargs = check_ind_length genv loc c idslpl1 pl2 in
+      nargs,intern_ind_with_all_args loc c idslpl1 pl2
+    | x -> error_bad_inductive_type (cases_pattern_expr_loc x)
+
 (**********************************************************************)
 (* Utilities for application                                          *)
 
@@ -1432,23 +1530,11 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | Some t ->
 	let tids = ids_of_cases_indtype t in
 	let tids = List.fold_right Idset.add tids Idset.empty in
-	let t = intern_type {env with ids = tids; tmp_scope = None} t in
-	let loc,ind,l = match t with
-	    | GRef (loc,IndRef ind) -> (loc,ind,[])
-	    | GApp (loc,GRef (_,IndRef ind),l) -> (loc,ind,l)
-	    | _ -> error_bad_inductive_type (loc_of_glob_constr t) in
-	let nparams, nrealargs = inductive_nargs_env globalenv ind in
-	let nindargs = nparams + nrealargs in
-	if List.length l <> nindargs then
-	  error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
+	let nparams,(ind,l) = intern_ind_pattern globalenv {env with ids = tids; tmp_scope = None} t in
 	let nal = List.map (function
-	  | GHole (loc,_) -> loc,Anonymous
-	  | GVar (loc,id) -> loc,Name id
-	  | c -> user_err_loc (loc_of_glob_constr c,"",str "Not a name.")) l in
-	let parnal,realnal = list_chop nparams nal in
-	if List.exists (fun (_,na) -> na <> Anonymous) parnal then
-	  error_parameter_not_implicit loc;
-	realnal, Some (loc,ind,nparams,List.map snd realnal)
+	  | PatVar (loc,x) -> loc,x
+	  | c -> user_err_loc (cases_pattern_loc c,"",str "Not a name.")) l in
+	nal, Some (cases_pattern_expr_loc t,ind,nparams,List.map snd nal)
     | None ->
 	[], None in
     let na = match tm', na with
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 32f20e0a8..b2e1a7545 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -30,6 +30,7 @@ type aconstr =
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
+  | AHole of Evd.hole_kind
   | AList of identifier * identifier * aconstr * aconstr * bool
   (* Part only in glob_constr *)
   | ALambda of name * aconstr * aconstr
@@ -45,7 +46,6 @@ type aconstr =
       (name * aconstr option * aconstr) list array * aconstr array *
       aconstr array
   | ASort of glob_sort
-  | AHole of Evd.hole_kind
   | APatVar of patvar
   | ACast of aconstr * aconstr cast_type
 
@@ -877,7 +877,7 @@ type constr_expr =
       (constr_expr * explicitation located option) list
   | CRecord of loc * constr_expr option * (reference * constr_expr) list
   | CCases of loc * case_style * constr_expr option *
-      (constr_expr * (name located option * constr_expr option)) list *
+      (constr_expr * (name located option * cases_pattern_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name located list * (name located option * constr_expr option) *
       constr_expr * constr_expr
@@ -989,16 +989,14 @@ let local_binders_loc bll =
   join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
 
 let ids_of_cases_indtype =
-  let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
-  let rec vars_of = function
+  let rec vars_of ids = function
     (* We deal only with the regular cases *)
-    | CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l)
-    | CNotation (_,_,(l,[],[]))
+    | (CPatCstr (_,_,l)|CPatCstrExpl (_, _, l)|CPatNotation (_,_,(l,[]))) -> List.fold_left vars_of [] l
     (* assume the ntn is applicative and does not instantiate the head !! *)
-    | CAppExpl (_,_,l) -> List.fold_left add_var [] l
-    | CDelimiters(_,_,c) -> vars_of c
-    | _ -> [] in
-  vars_of
+    | CPatDelimiters(_,_,c) -> vars_of ids c
+    | CPatAtom (_, Some (Libnames.Ident (_, x))) -> x::ids
+    | _ -> ids in
+  vars_of []
 
 let ids_of_cases_tomatch tms =
   List.fold_right
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 524df4e1b..5ee0c5bc6 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -27,6 +27,7 @@ type aconstr =
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
+  | AHole of Evd.hole_kind
   | AList of identifier * identifier * aconstr * aconstr * bool
   (** Part only in [glob_constr] *)
   | ALambda of name * aconstr * aconstr
@@ -42,7 +43,6 @@ type aconstr =
       (name * aconstr option * aconstr) list array * aconstr array *
       aconstr array
   | ASort of glob_sort
-  | AHole of Evd.hole_kind
   | APatVar of patvar
   | ACast of aconstr * aconstr cast_type
 
@@ -150,7 +150,7 @@ type constr_expr =
       (constr_expr * explicitation located option) list
   | CRecord of loc * constr_expr option * (reference * constr_expr) list
   | CCases of loc * case_style * constr_expr option *
-      (constr_expr * (name located option * constr_expr option)) list *
+      (constr_expr * (name located option * cases_pattern_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name located list * (name located option * constr_expr option) *
       constr_expr * constr_expr
@@ -212,7 +212,7 @@ val occur_var_constr_expr : identifier -> constr_expr -> bool
 val default_binder_kind : binder_kind
 
 (** Specific function for interning "in indtype" syntax of "match" *)
-val ids_of_cases_indtype : constr_expr -> identifier list
+val ids_of_cases_indtype : cases_pattern_expr -> identifier list
 
 val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr