- Second pass on implementation of let pattern. Parse "let ' par [as x]?

  [in I] := t [return pred] in b", just as SSReflect does with let:. 
  Change implementation: no longer a separate AST node, just add a case_style
  annotation on Cases to indicate it (if ML was dependently typed we
  could ensure that LetPatternStyle Cases have only one term to be
  matched and one branch, alas...). This factors out most code and we lose
  no functionality (win ! win !). Add LetPat.v test suite.

- Slight improvement of inference of return clauses for dependent
  pattern matching. If matching a variable of non-dependent type
  under a tycon that mentions it while giving no return clause, the
  dependency will be automatically infered. Examples at the end of
  DepPat. Should get rid of most explicit returns under tycons.


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

3 files changed, 20 insertions, 45 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 7385bf652f..aaa1b466da 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -224,11 +224,9 @@ let rec is_rec names =
 	  )
 	  b
     | RApp(_,f,args) -> List.exists (lookup names) (f::args)
-    | RCases(_,_,el,brl) -> 
+    | RCases(_,_,_,el,brl) -> 
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
-    | RLetPattern (_,(c,_),p) -> 
-	lookup names c || lookup_br names p
   and lookup_br names (_,idl,_,rt) = 
     let new_names = List.fold_right Idset.remove idl names in 
     lookup new_names rt
@@ -590,8 +588,8 @@ let rec add_args id new_args b =
   | CApp(loc,(pf,b),bl) -> 
       CApp(loc,(pf,add_args id new_args b), 
 	   List.map (fun (e,o) -> add_args id new_args e,o) bl)
-  | CCases(loc,b_option,cel,cal) -> 
-      CCases(loc,Option.map (add_args id new_args) b_option,
+  | CCases(loc,sty,b_option,cel,cal) -> 
+      CCases(loc,sty,Option.map (add_args id new_args) b_option,
 	     List.map (fun (b,(na,b_option)) -> 
 			 add_args id new_args b,
 			 (na,Option.map (add_args id new_args) b_option)) cel, 
@@ -603,9 +601,6 @@ let rec add_args id new_args b =
 		add_args id new_args b2
 	       )
 		
-  | CLetPattern(loc,p,b,c) ->
-      CLetPattern(loc,p,add_args id new_args b,add_args id new_args c)
-
   | CIf(loc,b1,(na,b_option),b2,b3) -> 
       CIf(loc,add_args id new_args b1, 
 	  (na,Option.map (add_args id new_args) b_option),
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 9276898e18..08a97fd221 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -567,7 +567,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		  funnames 
 		  avoid
 		  (mkRLetIn(new_n,t,mkRApp(new_b,args)))
-	    | RCases _ | RLambda _ | RIf _ | RLetTuple _ | RLetPattern _ -> 
+	    | RCases _ | RLambda _ | RIf _ | RLetTuple _ -> 
 		(* we have [(match e1, ...., en with ..... end) t1 tn]
 		   we first compute the result from the case and 
 		   then combine each of them with each of args one
@@ -627,14 +627,12 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 	in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_letin n) v_res b_res
-    | RCases(_,_,el,brl) -> 
+    | RCases(_,_,_,el,brl) -> 
 	(* we create the discrimination function 
 	   and treat the case itself 
 	*)
 	let make_discr = make_discr_match brl in 
 	build_entry_lc_from_case env funnames make_discr el brl avoid
-    | RLetPattern (loc,c,p) -> 
-	build_entry_lc env funnames avoid (RCases (loc, None, [c], [p]))
     | RIf(_,b,(na,e_option),lhs,rhs) -> 
 	let b_as_constr = Pretyping.Default.understand Evd.empty env b in
 	let b_typ = Typing.type_of env Evd.empty b_as_constr in 
@@ -1021,7 +1019,7 @@ let rec compute_cst_params relnames params = function
   | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> 
       let t_params = compute_cst_params relnames params t in 
       compute_cst_params relnames t_params b
-  | RCases _ | RLetPattern _ -> 
+  | RCases _ ->
       params  (* If there is still cases at this point they can only be 
 		 discriminitation ones *)
   | RSort _ -> params
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index c9341ba998..92396af590 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -15,7 +15,7 @@ let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
 let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
 let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
 let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
-let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
+let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,rto,l,brl)
 let mkRSort s = RSort(dummy_loc,s)
 let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
 let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
@@ -163,14 +163,12 @@ let change_vars =
 		    change_vars mapping b, 
 		    change_vars new_mapping e
 		   )
-      | RCases(loc,infos,el,brl) -> 
-	  RCases(loc,
+      | RCases(loc,sty,infos,el,brl) -> 
+	  RCases(loc,sty,
 		 infos,
 		 List.map (fun (e,x) -> (change_vars mapping e,x)) el, 
 		 List.map (change_vars_br mapping) brl
 		)
-      | RLetPattern(loc, (e,x), br) ->
-	  RLetPattern(loc, (change_vars mapping e, x), change_vars_br mapping br)
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc,
 	      change_vars mapping b,
@@ -348,13 +346,11 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded new_b in 
 	let new_rto = Option.map (alpha_rt new_excluded) new_rto  in
 	RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
-    | RCases(loc,infos,el,brl) -> 
+    | RCases(loc,sty,infos,el,brl) -> 
 	let new_el = 
 	  List.map (function (rt,i) -> alpha_rt excluded rt, i) el 
 	in 
-	RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) 
-    | RLetPattern(loc,(rt,i),br) -> 
-	RLetPattern(loc, (alpha_rt excluded rt, i), alpha_br excluded br) 
+	RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl) 
     | RIf(loc,b,(na,e_o),lhs,rhs) -> 
 	RIf(loc,alpha_rt excluded b,
 	    (na,Option.map (alpha_rt excluded) e_o),
@@ -402,10 +398,9 @@ let is_free_in id =
 	    | _ -> true
 	in
 	is_free_in t || (check_in_b && is_free_in b)
-    | RCases(_,_,el,brl) ->
+    | RCases(_,_,_,el,brl) ->
 	(List.exists (fun (e,_) -> is_free_in e) el) ||
 	  List.exists is_free_in_br brl
-    | RLetPattern(_,(e,_),br) -> is_free_in e || is_free_in_br br
     | RLetTuple(_,nal,_,b,t) -> 
 	let check_in_nal = 
 	  not (List.exists (function Name id' -> id'= id | _ -> false) nal) 
@@ -499,14 +494,12 @@ let replace_var_by_term x_id term =
 		    replace_var_by_pattern def,
 		    replace_var_by_pattern b
 		   )
-      | RCases(loc,infos,el,brl) -> 
-	  RCases(loc,
+      | RCases(loc,sty,infos,el,brl) -> 
+	  RCases(loc,sty,
 		 infos,
 		 List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, 
 		 List.map replace_var_by_pattern_br brl
 		)
-      | RLetPattern(loc,(e,x),br) ->
-	  RLetPattern(loc,(replace_var_by_pattern e, x), replace_var_by_pattern_br br)
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc, replace_var_by_pattern b,
 	      (na,Option.map replace_var_by_pattern e_option),
@@ -608,10 +601,8 @@ let ids_of_rawterm c =
       | RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
       | RLetTuple (_,nal,(na,po),b,c) -> 
           List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
-      | RCases (loc,rtntypopt,tml,brchl) -> 
+      | RCases (loc,sty,rtntypopt,tml,brchl) -> 
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
-      | RLetPattern (loc,tm,(_,idl,patl,c)) -> 
-	  idl @ ids_of_rawterm [] c
       | RRec _ -> failwith "Fix inside a constructor branch"
       | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> []
   in
@@ -658,17 +649,12 @@ let zeta_normalize =
 		    zeta_normalize_term def,
 		    zeta_normalize_term b
 		   )
-      | RCases(loc,infos,el,brl) -> 
-	  RCases(loc,
+      | RCases(loc,sty,infos,el,brl) -> 
+	  RCases(loc,sty,
 		 infos,
 		 List.map (fun (e,x) -> (zeta_normalize_term e,x)) el, 
 		 List.map zeta_normalize_br brl
 		)
-      | RLetPattern(loc,(e,x),br) -> 
-	  RLetPattern(loc,
-		     (zeta_normalize_term e,x),
-		     zeta_normalize_br br
-	  )
       | RIf(loc,b,(na,e_option),lhs,rhs) -> 
 	  RIf(loc, zeta_normalize_term b,
 	      (na,Option.map zeta_normalize_term e_option),
@@ -723,14 +709,10 @@ let expand_as =
       | RDynamic _ -> error "Not handled RDynamic"
       | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
       | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
-      | RCases(loc,po,el,brl) ->
-	  RCases(loc, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+      | RCases(loc,sty,po,el,brl) ->
+	  RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
-      | RLetPattern(loc,(rt,t),br) ->
-	  RLetPattern(loc, (expand_as map rt,t),
-		expand_as_br map br)
-	    
   and expand_as_br map (loc,idl,cpl,rt) = 
-    (loc,idl,cpl,    expand_as (List.fold_left add_as map cpl) rt)
+    (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
   in
   expand_as Idmap.empty