Syntaxe plus liberale pour le type des arguments de filtrage du 'match'

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

5 files changed, 64 insertions, 22 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d1ce067126..f8bd7b3d9b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -32,6 +32,8 @@ let for_grammar f x =
   interning_grammar := false;
   a
 
+let variables_bind = ref false
+
 (* For the translator *)
 let temporary_implicits_in = ref []
 let set_temporary_implicits_in l = temporary_implicits_in := l
@@ -107,6 +109,10 @@ let error_unbound_patvar loc n =
     (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ 
       str " is unbound")
 
+let error_bad_inductive_type loc =
+  user_err_loc (loc,"",str 
+    "This should be an inductive type applied to names or \"_\"")
+
 (**********************************************************************)
 (* Dump of globalization (to be used by coqdoc)                       *)
 
@@ -583,18 +589,13 @@ let internalise sigma env allow_soapp lvar c =
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
     | CCases (loc, (po,rtnpo), tms, eqns) ->
-        let rtnids = List.fold_right (fun (_,(na,x)) ids ->
-          let ids = match x with
-            | Some (_,_,nal) -> List.fold_right (name_fold Idset.add) nal ids
-            | _ -> ids in
-          name_fold Idset.add na ids) tms ids in
+        let tms,rtnids = List.fold_right (fun (tm,indnalo) (inds,ids) ->
+	  let typ,ids = intern_return_type env indnalo ids in
+	  (intern env tm,ref typ)::inds,ids)
+	  tms ([],ids) in
         let rtnpo =
           option_app (intern_type (rtnids,impls,tmp_scope,scopes)) rtnpo in
-	RCases (loc, (option_app (intern_type env) po, ref rtnpo),
-		List.map (fun (tm,(na,indnalo)) ->
-		  (intern env tm,ref (na,option_app (fun (loc,r,nal) ->
-		    let ind,l = intern_inductive r in
-		    (loc,ind,l@nal)) indnalo))) tms,
+	RCases (loc, (option_app (intern_type env) po, ref rtnpo), tms,
 		List.map (intern_eqn (List.length tms) env) eqns)
     | COrderedCase (loc, tag, po, c, cl) ->
 	let env = reset_tmp_scope env in
@@ -634,7 +635,7 @@ let internalise sigma env allow_soapp lvar c =
 
     | CDynamic (loc,d) -> RDynamic (loc,d)
 
-  and intern_type (ids,impls,tmp_scope,scopes) =
+  and intern_type (ids,impls,_,scopes) =
     intern (ids,impls,Some Symbols.type_scope,scopes)
 
   and intern_eqn n (ids,impls,tmp_scope,scopes as env) (loc,lhs,rhs) =
@@ -653,6 +654,27 @@ let internalise sigma env allow_soapp lvar c =
 	let env_ids = List.fold_right Idset.add eqn_ids ids in
 	(loc, eqn_ids,pl,intern (env_ids,impls,tmp_scope,scopes) rhs)
 
+  and intern_return_type (_,_,_,scopes as env) (na,t) ids =
+    let ids,typ = match t with
+    | Some t -> 
+	let tids = names_of_cases_indtype t in
+	let tids = List.fold_right Idset.add tids Idset.empty in
+	let t = intern_type (tids,[],None,scopes) t in
+	begin match t with
+	  | RApp (loc,RRef (_,IndRef ind),l) ->
+	      let nal = List.map (function
+		| RHole _ -> Anonymous
+		| RVar (_,id) -> Name id
+		| c ->
+		    user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
+	      List.fold_right (name_fold Idset.add) nal ids,
+	      Some (loc,ind,nal)
+	  | _ -> error_bad_inductive_type (loc_of_rawconstr t)
+	end
+    | None -> 
+	ids, None in
+    (na,typ), name_fold Idset.add na ids
+
   and iterate_prod loc2 env ty body = function
     | (loc1,na)::nal ->
 	if nal <> [] then check_capture loc1 ty na;
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 0848833496..f83c6e3508 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -168,8 +168,8 @@ let rec subst_aconstr subst raw =
       let ref' = subst_global subst ref in 
 	if ref' == ref then raw else
 	  AHole (ImplicitArg (ref',i))
-  | AHole ( (BinderType _ | QuestionMark | CasesType |
-      InternalHole | TomatchTypeParameter _)) -> raw
+  | AHole (BinderType _ | QuestionMark | CasesType |
+      InternalHole | TomatchTypeParameter _) -> raw
 
   | ACast (r1,r2) -> 
       let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in
@@ -423,7 +423,7 @@ type constr_expr =
   | CApp of loc * (proj_flag * constr_expr) * 
       (constr_expr * explicitation located option) list
   | CCases of loc * (constr_expr option * constr_expr option) *
-      (constr_expr * (name * (loc * reference * name list) option)) list *
+      (constr_expr * (name * constr_expr option)) list *
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
@@ -536,6 +536,15 @@ let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
 
 (* Used in correctness and interface *)
 
+let names_of_cases_indtype =
+  let rec aux ids = function
+    (* We deal only with the regular cases *)
+  | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> aux ids a) ids l
+  | CNotation (_,_,l) | CAppExpl (_,_,l) -> List.fold_left aux ids l
+  | CRef (Ident (_,id)) -> id::ids
+  | _ -> ids
+  in aux []
+
 let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
 
 let map_binders f g e bl =
@@ -565,8 +574,9 @@ let map_constr_expr_with_binders f g e = function
 	List.fold_right
 	  (fun (tm,(na,indnal)) e ->
 	    option_fold_right
-	      (fun (loc,ind,nal) ->
-		List.fold_right (name_fold g) nal) indnal (name_fold g na e))
+	      (fun t ->
+		let ids = names_of_cases_indtype t in
+		List.fold_right g ids) indnal (name_fold g na e))
 	  a e
       in
       CCases (loc,(option_app (f e) po, option_app (f e') rtnpo),
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index a4b20b65ca..3d9def4dd9 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -86,7 +86,7 @@ type constr_expr =
   | CApp of loc * (proj_flag * constr_expr) * 
         (constr_expr * explicitation located option) list
   | CCases of loc * (constr_expr option * constr_expr option) *
-      (constr_expr * (name * (loc * reference * name list) option)) list *
+      (constr_expr * (name * constr_expr option)) list *
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
@@ -117,6 +117,9 @@ val replace_vars_constr_expr :
 
 val occur_var_constr_expr : identifier -> constr_expr -> bool
 
+(* Specific function for interning "in indtype" syntax of "match" *)
+val names_of_cases_indtype : constr_expr -> identifier list
+
 val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index c3a7c27b3a..e8f9c38c5e 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -287,9 +287,7 @@ GEXTEND Gram
   ;
   pred_pattern:
     [ [ oid = ["as"; id=name -> snd id | -> Names.Anonymous];
-        ty = OPT ["in"; r=global; nal=LIST0 name ->
-          (loc,r,List.map snd nal)] ->
-          (oid,ty) ] ]
+        ty = OPT ["in"; t=lconstr -> t] -> (oid,ty) ] ]
   ;
   case_type:
     [ [ ty = OPT [ "return"; c = operconstr LEVEL "100" -> c ] -> ty ] ]
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 5e5a3236b4..51b2a69535 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -336,7 +336,13 @@ let is_var id = function
   | _ -> false
 
 let tm_clash = function
-  | (CRef (Ident (_,id)), Some (_,_,nal)) when List.exists ((=) (Name id)) nal
+  | (CRef (Ident (_,id)), Some (CApp (_,_,nal))) 
+      when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false)
+	nal
+      -> Some id
+  | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal))) 
+      when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false)
+	nal
       -> Some id
   | _ -> None
 
@@ -350,9 +356,12 @@ let pr_case_item pr (tm,(na,indnalopt)) =
     | _ -> mt ()) ++
   (match indnalopt with
     | None -> mt ()
+(*
     | Some (_,ind,nal) ->
         spc () ++ str "in " ++ 
-        hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal)))
+        hov 0 (pr_reference ind ++ prlist (pr_arg pr_name) nal))
+*)
+    | Some t -> spc () ++ str "in " ++ pr lsimple t))
 
 let pr_case_type pr po =
   match po with