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

5 files changed, 29 insertions, 2 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 69d5ad67a9..eb69e12257 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -722,6 +722,15 @@ 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,
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b2c7728fdb..156d155667 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -917,6 +917,11 @@ 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 f3c3506b5c..082db5a390 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -64,6 +64,8 @@ let rec unloc = function
         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 97a0f94da5..accccdeee7 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -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 _ | RIf _ | RCast _),_
+    | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _),_
   | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
-      | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
+      | RPatVar _ | REvar _ | RLetTuple _ | RLetPattern _ | RIf _ | RCast _)
       -> error "Unsupported construction in recursive notations"
   | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
       -> false
@@ -196,6 +196,7 @@ 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)
@@ -563,6 +564,7 @@ type constr_expr =
       (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
@@ -632,6 +634,7 @@ let constr_loc = function
   | CApp (loc,_,_) -> loc
   | CCases (loc,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
+  | CLetPattern (loc,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
   | CHole (loc, _) -> loc
   | CPatVar (loc,_) -> loc
@@ -733,6 +736,10 @@ 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
@@ -844,6 +851,9 @@ let map_constr_expr_with_binders g f e = function
       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 6bbc64cca2..6bfbcf07f8 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -123,6 +123,7 @@ type constr_expr =
       (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