- 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

5 files changed, 31 insertions, 59 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index eb69e12257..11cd87763f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -195,7 +195,7 @@ let rec check_same_type ty1 ty2 =
       List.iter2 (fun (a1,e1) (a2,e2) ->
                     if e1<>e2 then failwith "not same expl";
                     check_same_type a1 a2) al1 al2
-  | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
+  | CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) ->
       List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
       List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
         List.iter2 (located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
@@ -264,7 +264,7 @@ let rec same_raw c d =
   | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
       if na1 <> na2 then failwith "RLetIn";
       same_raw t1 t2; same_raw m1 m2
-  | RCases(_,_,c1,b1), RCases(_,_,c2,b2) ->
+  | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) ->
       List.iter2
         (fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
           same_raw t1 t2;
@@ -690,7 +690,7 @@ let rec extern inctx scopes vars r =
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
       CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 
-  | RCases (loc,rtntypopt,tml,eqns) ->
+  | RCases (loc,sty,rtntypopt,tml,eqns) ->
       let vars' = 
 	List.fold_right (name_fold Idset.add)
 	  (cases_predicate_names tml) vars in
@@ -713,7 +713,7 @@ let rec extern inctx scopes vars r =
 	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
 	  (extern_typ scopes vars t)) x))) tml in
       let eqns = List.map (extern_eqn (rtntypopt<>None) scopes vars) eqns in 
-      CCases (loc,rtntypopt',tml,eqns)
+      CCases (loc,sty,rtntypopt',tml,eqns)
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,nal,
@@ -722,15 +722,6 @@ let rec extern inctx scopes vars r =
         sub_extern false scopes vars tm,
         extern false scopes (List.fold_left add_vname vars nal) b)
 
-  | RLetPattern (loc,(tm,_), eqn) ->
-      let p, c = 
-	match extern_eqn false scopes vars eqn with
-	    (loc,[loc',[p]], c) -> p,c
-	  | _ -> assert false
-      in
-      let t = extern inctx scopes vars tm in
-	CLetPattern(loc, p, t, c)
-
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
         (Option.map (fun _ -> na) typopt,
@@ -948,7 +939,7 @@ let rec raw_of_pat env = function
       let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
       RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
   | PCase (_,PMeta None,tm,[||]) ->
-      RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[])
+      RCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[])
   | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
       let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
       let brns = Array.to_list cstr_nargs in
@@ -960,7 +951,7 @@ let rec raw_of_pat env = function
 	else 
 	  let nparams,n = Option.get ind_nargs in
 	  return_type_of_predicate ind nparams n (raw_of_pat env p) in
-      RCases (loc,rtn,[raw_of_pat env tm,indnames],mat)
+      RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ce445c3f6d..9e962267db 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -901,7 +901,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
           (* Now compact "(f args') args" *)
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
-    | CCases (loc, rtnpo, tms, eqns) ->
+    | CCases (loc, sty, rtnpo, tms, eqns) ->
         let tms,env' = List.fold_right
           (fun citm (inds,env) ->
 	    let (tm,ind),nal = intern_case_item env citm in
@@ -909,7 +909,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	  tms ([],env) in
         let rtnpo = Option.map (intern_type env') rtnpo in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
-	RCases (loc, rtnpo, tms, List.flatten eqns')
+	RCases (loc, sty, rtnpo, tms, List.flatten eqns')
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
         let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
@@ -917,11 +917,6 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let p' = Option.map (intern_type env'') po in
         RLetTuple (loc, nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar) env nal) c)
-    | CLetPattern (loc, p, c, b) ->
-	let loc' = cases_pattern_expr_loc p in
-	let (tm,ind), nal = intern_case_item env (c,(None,None)) in
-	let eqn' = intern_eqn 1 env (loc, [loc',[p]], b) in
-	RLetPattern (loc, (tm,ind), List.hd eqn')
     | CIf (loc, c, (na,po), b1, b2) ->
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 082db5a390..f49c42a55d 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -57,15 +57,13 @@ let rec unloc = function
   | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c)
   | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c)
   | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
-  | RCases (_,rtntypopt,tml,pl) ->
-      RCases (dummy_loc,
+  | RCases (_,sty,rtntypopt,tml,pl) ->
+      RCases (dummy_loc,sty,
         (Option.map unloc rtntypopt),
 	List.map (fun (tm,x) -> (unloc tm,x)) tml,
         List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
   | RLetTuple (_,nal,(na,po),b,c) ->
       RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c)
-  | RLetPattern (_,(tm,x),(_,idl,p,c)) -> 
-      RLetPattern (dummy_loc,(unloc tm,x),(dummy_loc,idl,p,unloc c))
   | RIf (_,c,(na,po),b1,b2) ->
       RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
   | RRec (_,fk,idl,bl,tyl,bv) ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c9a33c7eba..05a1465ac8 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -37,7 +37,7 @@ type aconstr =
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
-  | ACases of aconstr option *
+  | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
       (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
@@ -79,7 +79,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
   | ALetIn (na,b,c) ->
       let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
-  | ACases (rtntypopt,tml,eqnl) ->
+  | ACases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
@@ -94,7 +94,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
 	let ((idl,e),patl) =
 	  list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
 	(loc,idl,patl,f e rhs)) eqnl in
-      RCases (loc,Option.map (f e') rtntypopt,tml',eqnl')
+      RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
       let e,nal = list_fold_map (name_fold_map g) e nal in 
       let e,na = name_fold_map g e na in
@@ -138,9 +138,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
   | RHole _, RHole _ -> true
   | RSort (_,s1), RSort (_,s2) -> s1 = s2
   | (RLetIn _ | RCases _ | RRec _ | RDynamic _
-    | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _),_
+    | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
   | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
-      | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _)
+      | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
       -> error "Unsupported construction in recursive notations"
   | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
       -> false
@@ -183,9 +183,9 @@ let aconstr_and_vars_of_rawconstr a =
   | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
   | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
   | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
-  | RCases (_,rtntypopt,tml,eqnl) ->
+  | RCases (_,sty,rtntypopt,tml,eqnl) ->
       let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
-      ACases (Option.map aux rtntypopt,
+      ACases (sty,Option.map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
 	  Option.iter
@@ -196,7 +196,6 @@ let aconstr_and_vars_of_rawconstr a =
       add_name found na;
       List.iter (add_name found) nal;
       ALetTuple (nal,(na,Option.map aux po),aux b,aux c)
-  | RLetPattern (loc, c, p) -> error "TODO: aconstr of letpattern"
   | RIf (loc,c,(na,po),b1,b2) ->
       add_name found na;
       AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
@@ -208,8 +207,7 @@ let aconstr_and_vars_of_rawconstr a =
   | RRef (_,r) -> ARef r
   | RPatVar (_,(_,n)) -> APatVar n
   | RDynamic _ | RRec _ | REvar _ ->
-      error "Fixpoints, cofixpoints, existential variables and pattern-matching  not \
-allowed in abbreviatable expressions"
+      error "Fixpoints, cofixpoints and existential variables not allowed in abbreviatable expressions"
 
   (* Recognizing recursive notations *)
   and terminator_of_pat f1 ll1 lr1 = function
@@ -305,7 +303,7 @@ let rec subst_aconstr subst bound raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  ALetIn (n,r1',r2')
 
-  | ACases (rtntypopt,rl,branches) -> 
+  | ACases (sty,rtntypopt,rl,branches) -> 
       let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
       and rl' = list_smartmap
         (fun (a,(n,signopt) as x) -> 
@@ -325,7 +323,7 @@ let rec subst_aconstr subst bound raw =
       in
         if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &
           rl' == rl && branches' == branches then raw else
-          ACases (rtntypopt',rl',branches')
+          ACases (sty,rtntypopt',rl',branches')
 
   | ALetTuple (nal,(na,po),b,c) ->
       let po' = Option.smartmap (subst_aconstr subst bound) po
@@ -447,8 +445,9 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
   | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
      match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
-  | RCases (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2) 
-      when List.length tml1 = List.length tml2
+  | RCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2) 
+      when sty1 = sty2
+	 & List.length tml1 = List.length tml2
 	 & List.length eqnl1 = List.length eqnl2 ->
       let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
       let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
@@ -559,12 +558,11 @@ type constr_expr =
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) * 
       (constr_expr * explicitation located option) list
-  | CCases of loc * constr_expr option *
+  | CCases of loc * case_style * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
-  | CLetPattern of loc * cases_pattern_expr * constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of loc * Evd.hole_kind option
@@ -577,7 +575,6 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-
 and fixpoint_expr =
     identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
@@ -632,9 +629,8 @@ let constr_loc = function
   | CLetIn (loc,_,_,_) -> loc
   | CAppExpl (loc,_,_) -> loc
   | CApp (loc,_,_) -> loc
-  | CCases (loc,_,_,_) -> loc
+  | CCases (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
-  | CLetPattern (loc,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
   | CHole (loc, _) -> loc
   | CPatVar (loc,_) -> loc
@@ -726,7 +722,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CDelimiters (loc,_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
       acc
-  | CCases (loc,rtnpo,al,bl) ->
+  | CCases (loc,sty,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
       let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map fst al) in
@@ -736,10 +732,6 @@ let fold_constr_expr_with_binders g f n acc = function
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let n' = List.fold_right (name_fold g) nal n in
       f (Option.fold_right (name_fold g) ona n') (f n acc b) c
-  | CLetPattern (loc,p,b,c) ->
-      let acc = f n acc b in
-      let ids = cases_pattern_fold_names Idset.add Idset.empty p in
-	f (Idset.fold g ids n) acc c
   | CIf (_,c,(ona,po),b1,b2) ->
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po
@@ -841,19 +833,16 @@ let map_constr_expr_with_binders g f e = function
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
   | CPrim _ | CDynamic _ | CRef _ as x -> x
-  | CCases (loc,rtnpo,a,bl) ->
+  | CCases (loc,sty,rtnpo,a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
       let ids = ids_of_cases_tomatch a in
       let po = Option.map (f (List.fold_right g ids e)) rtnpo in
-      CCases (loc, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+      CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (name_fold g) nal e in
       let e'' = Option.fold_right (name_fold g) ona e in
       CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
-  | CLetPattern (loc, p, b, c) -> 
-      (* TODO: apply g on the binding variables in pat... *)
-      CLetPattern (loc, p, f e b,f e c)
   | CIf (loc,c,(ona,po),b1,b2) ->
       let e' = Option.fold_right (name_fold g) ona e in
       CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 26805aa13e..4e46d95902 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -33,7 +33,7 @@ type aconstr =
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
-  | ACases of aconstr option *
+  | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
       (cases_pattern list * aconstr) list
   | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
@@ -117,13 +117,12 @@ type constr_expr =
   | CLetIn of loc * name located * constr_expr * constr_expr
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) * 
-        (constr_expr * explicitation located option) list
-  | CCases of loc * constr_expr option *
+      (constr_expr * explicitation located option) list
+  | CCases of loc * case_style * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
   | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
-  | CLetPattern of loc * cases_pattern_expr * constr_expr * constr_expr
   | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of loc * Evd.hole_kind option