- 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

8 files changed, 31 insertions, 76 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 
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index 16357fc472..39eaa0b98b 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -210,7 +210,7 @@ let rec depends_of_rawconstr rc acc = match rc with
   | RLambda (_, _, _, rct, rcb)
   | RProd   (_, _, _, rct, rcb)
   | RLetIn  (_, _, rct, rcb) -> depends_of_rawconstr rcb (depends_of_rawconstr rct acc)
-  | RCases  (_, rco, tmt, cc) ->
+  | RCases  (_, _, rco, tmt, cc) ->
       (* LEM TODO: handle the cc *)
       (Option.fold_right depends_of_rawconstr rco
          (list_union_map
@@ -221,13 +221,6 @@ let rec depends_of_rawconstr rc acc = match rc with
 	    acc))
   | RLetTuple (_,_,(_,rco),rc0,rc1) ->
      depends_of_rawconstr rc1 (depends_of_rawconstr rc0 (Option.fold_right depends_of_rawconstr rco acc))
-  | RLetPattern (_, tmt, cc) ->
-      (* LEM TODO: handle the cc *)
-      (fun (rc, pp) acc ->
-	 Option.fold_right (fun (_,ind,_,_) acc -> (IndRef ind)::acc) (snd pp)
-	   (depends_of_rawconstr rc acc))
-	tmt
-	acc
   | RIf (_, rcC, (_, rco), rcT, rcF) -> let dorc = depends_of_rawconstr in
       dorc rcF (dorc rcT (dorc rcF (dorc rcC (Option.fold_right dorc rco acc))))
   | RRec (_, _, _, rdla, rca0, rca1) -> let dorca = array_union_map depends_of_rawconstr in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 2219e327ca..aa7a50dce2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -360,8 +360,6 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
    | CLetIn(_, v, a, b) -> 
        CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
-   | CLetPattern(_, v, a, b) -> 
-       error "TODO: xlate_formula let | pattern"
    | CAppExpl(_, (Some n, r), l) -> 
        let l', last = decompose_last l in
 	 CT_proj(xlate_formula last,
@@ -379,8 +377,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		 (xlate_formula f, List.map xlate_formula_expl l'))
    | CApp(_, (_,f), l) -> 
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
-   | CCases (_, _, [], _) -> assert false
-   | CCases (_, ret_type, tm::tml, eqns)->
+   | CCases (_, _, _, [], _) -> assert false
+   | CCases (_, _, ret_type, tm::tml, eqns)->
        CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
 					   List.map xlate_matched_formula tml),
 		xlate_formula_opt ret_type,
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index dd776088cc..8d9bfdbc51 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1070,7 +1070,7 @@ let (value_f:constr list -> global_reference -> constr) =
     in
     let fun_body = 
       RCases
-	(d0,None,
+	(d0,RegularStyle,None,
 	 [RApp(d0, RRef(d0,fterm), List.rev_map (fun x_id -> RVar(d0, x_id)) rev_x_id_l),
 	  (Anonymous,None)],
 	 [d0, [v_id], [PatCstr(d0,(ind_of_ref 
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 54ed30a5dc..5b8bb9c0f8 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -241,6 +241,7 @@ type pattern_matching_problem =
       history  : pattern_continuation;
       mat      : matrix;
       caseloc  : loc;
+      casestyle: case_style;
       typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
 
 (*--------------------------------------------------------------------------*
@@ -1263,7 +1264,7 @@ and match_current pb tomatch =
 	  let (pred,typ,s) =
 	    find_predicate pb.caseloc pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt pb.tomatch in
-	  let ci = make_case_info pb.env mind RegularStyle in
+	  let ci = make_case_info pb.env mind pb.casestyle in
 	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  { uj_val = applist (case, inst);
@@ -2081,7 +2082,7 @@ let nf_evars_env evar_defs (env : env) : env =
     Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
      ~init:env' env
       
-let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
+let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env eqns in
      
@@ -2151,6 +2152,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 	  history  = start_history (List.length initial_pushed);
 	  mat      = matx;
 	  caseloc  = loc;
+	  casestyle= style;
 	  typing_function = typing_fun } in
 	
       let j = compile pb in
@@ -2180,6 +2182,7 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
 	      history  = start_history (List.length initial_pushed);
 	      mat      = matx;
 	      caseloc  = loc;
+	      casestyle= style;
 	      typing_function = typing_fun } in
 	    
 	  let j = compile pb in
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 730b12605e..d3edb6e3cd 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -488,22 +488,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  in
 	    { uj_val = v; uj_type = p }
 
-    | RLetPattern (loc, c, p) ->
-	(* Just use cases typing *)
-	let j = 
-	  pretype tycon env isevars lvar 
-	    (RCases (loc, None, [c], [p]))
-	in
-	  (* Change case info *)
-	let j' = match kind_of_term j.uj_val with
-	    Case (ci, po, c, br) ->
-	      let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in
-		{ j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) }
-	  | _ -> j
-	in j'
-
-    | RCases (loc,po,tml,eqns) ->
-	Cases.compile_cases loc
+    | RCases (loc,sty,po,tml,eqns) ->
+	Cases.compile_cases loc sty
 	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
 	  tycon env (* loc *) (po,tml,eqns)