Add new LetPattern construct to replace dest. syntax: let| pat := t in b is backwards compatible. Update CHANGES with things i've done.

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

6 files changed, 54 insertions, 12 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e71083c509..b7317b5be0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -69,7 +69,7 @@ module type S = sig
     (type_constraint -> env -> rawconstr -> unsafe_judgment) *
       Evd.evar_defs ref ->
     type_constraint -> 
-    env -> rawconstr option * tomatch_tuple * cases_clauses ->
+    env -> rawconstr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
 end
 
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index adb66ef475..d105ca2d0f 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -53,7 +53,7 @@ module type S = sig
     loc ->
     (type_constraint -> env -> rawconstr -> unsafe_judgment) * evar_defs ref ->
     type_constraint -> 
-    env -> rawconstr option * tomatch_tuple * cases_clauses ->
+    env -> rawconstr option * tomatch_tuples * cases_clauses ->
     unsafe_judgment
 end
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a9e550bf7c..c9e68d1e3b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -616,7 +616,29 @@ let rec subst_rawconstr subst raw =
       and c' = subst_rawconstr subst c in
 	if po' == po && b' == b && c' == c then raw else
           RLetTuple (loc,nal,(na,po'),b',c')
-      
+
+  | RLetPattern (loc, (a,x as c), (loc',idl,cpl,r as branch)) ->
+      let c' = 
+	let a' = subst_rawconstr subst a in
+        let (n,topt) = x in 
+        let topt' = Option.smartmap
+          (fun (loc,(sp,i),x,y as t) ->
+            let sp' = subst_kn subst sp in
+              if sp == sp' then t else (loc,(sp',i),x,y))
+	  topt 
+	in
+          if a == a' && topt == topt' then c else (a',(n,topt'))
+      in
+      let p' = 
+	let cpl' =
+	  list_smartmap (subst_cases_pattern subst) cpl
+	and r' = subst_rawconstr subst r in
+	  if cpl' == cpl && r' == r then branch else
+	    (loc',idl,cpl',r')
+      in 
+	if c' == c && p' == branch then raw else
+	  RLetPattern (loc, c', p')
+	        
   | RIf (loc,c,(na,po),b1,b2) ->
       let po' = Option.smartmap (subst_rawconstr subst) po
       and b1' = subst_rawconstr subst b1 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c9d44e3dc9..5b4e8e7cf2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -583,6 +583,13 @@ module Pretyping_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 evdref lvar 
+	    (RCases (loc, None, [c], [p]))
+	in j
+	
     | RCases (loc,po,tml,eqns) ->
 	Cases.compile_cases loc
 	  ((fun vtyc env -> pretype vtyc env evdref lvar),evdref)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index bf5cc22723..e7f5de028f 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -62,9 +62,10 @@ type rawconstr =
   | RLambda of loc * name * binding_kind * rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
+  | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
+  | RLetPattern of loc * tomatch_tuple * cases_clause
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
@@ -84,10 +85,13 @@ and fix_kind =
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
 
-and tomatch_tuple = (rawconstr * predicate_pattern) list
+and tomatch_tuple = (rawconstr * predicate_pattern)
 
-and cases_clauses =
-    (loc * identifier list * cases_pattern list * rawconstr) list
+and tomatch_tuples = tomatch_tuple list
+
+and cases_clause = (loc * identifier list * cases_pattern list * rawconstr)
+
+and cases_clauses = cases_clause list
 
 let cases_predicate_names tml =
   List.flatten (List.map (function
@@ -117,6 +121,8 @@ let map_rawconstr f = function
         List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
   | RLetTuple (loc,nal,(na,po),b,c) ->
       RLetTuple (loc,nal,(na,Option.map f po),f b,f c)
+  | RLetPattern (loc,(b,x),(loc',idl,p,c)) ->
+      RLetPattern (loc,(f b,x),(loc',idl,p,f c))
   | RIf (loc,c,(na,po),b1,b2) ->
       RIf (loc,f c,(na,Option.map f po),f b1,f b2)
   | RRec (loc,fk,idl,bl,tyl,bv) ->
@@ -178,6 +184,7 @@ let occur_rawconstr id =
     | RLetTuple (loc,nal,rtntyp,b,c) -> 
 	occur_return_type rtntyp id
         or (occur b) or (not (List.mem (Name id) nal) & (occur c))
+    | RLetPattern (loc, (b, _), p) -> (occur b) or (occur_pattern p)
     | RIf (loc,c,rtntyp,b1,b2) -> 
 	occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
     | RRec (loc,fk,idl,bl,tyl,bv) ->
@@ -226,6 +233,7 @@ let free_rawvars  =
 	let vs2 = vars bounded vs1 b in 
 	let bounded' = List.fold_left add_name_to_ids bounded nal in
 	vars bounded' vs2 c
+    | RLetPattern (loc, (c, _), p) -> vars_pattern bounded (vars bounded vs c) p
     | RIf (loc,c,rtntyp,b1,b2) -> 
 	let vs1 = vars_return_type bounded vs rtntyp in 
 	let vs2 = vars bounded vs1 c in 
@@ -277,6 +285,7 @@ let loc_of_rawconstr = function
   | RLambda (loc,_,_,_,_) -> loc
   | RProd (loc,_,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
+  | RLetPattern (loc,_,_) -> loc
   | RCases (loc,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 2a5dab6e40..7b342c4115 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -66,9 +66,10 @@ type rawconstr =
   | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
+  | RCases of loc * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
+  | RLetPattern of loc * tomatch_tuple * cases_clause
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * rawdecl list array *
       rawconstr array * rawconstr array
@@ -88,12 +89,15 @@ and fix_kind =
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
 
-and tomatch_tuple = (rawconstr * predicate_pattern) list
+and tomatch_tuple = (rawconstr * predicate_pattern)
 
-and cases_clauses =
-    (loc * identifier list * cases_pattern list * rawconstr) list
+and tomatch_tuples = tomatch_tuple list
 
-val cases_predicate_names : tomatch_tuple -> name list
+and cases_clause = (loc * identifier list * cases_pattern list * rawconstr)
+
+and cases_clauses = cases_clause list
+
+val cases_predicate_names : tomatch_tuples -> name list
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the