modif des fixpoints pour que si on donne une notation au produit, les pts fixes s'affichent correctement

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

5 files changed, 151 insertions, 53 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fa1faf9cf3..0f0968aad7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1009,14 +1009,16 @@ let rec check_same_type ty1 ty2 =
   match ty1, ty2 with
   | CRef r1, CRef r2 -> check_same_ref r1 r2
   | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
-      List.iter2 (fun (id1,i1,_,a1,b1) (id2,i2,_,a2,b2) ->
+      List.iter2 (fun (id1,i1,bl1,a1,b1) (id2,i2,bl2,a2,b2) ->
         if id1<>id2 || i1<>i2 then failwith "not same fix";
+        check_same_fix_binder bl1 bl2;
         check_same_type a1 a2;
         check_same_type b1 b2)
         fl1 fl2
   | CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 ->
-      List.iter2 (fun (id1,a1,b1) (id2,a2,b2) ->
+      List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) ->
         if id1<>id2 then failwith "not same fix";
+        check_same_fix_binder bl1 bl2;
         check_same_type a1 a2;
         check_same_type b1 b2)
         fl1 fl2
@@ -1066,6 +1068,15 @@ and check_same_binder (nal1,e1) (nal2,e2) =
     if na1<>na2 then failwith "not same name") nal1 nal2;
   check_same_type e1 e2
 
+and check_same_fix_binder bl1 bl2 =
+  List.iter2 (fun b1 b2 ->
+    match b1,b2 with
+        LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) ->
+          check_same_binder (nal1,ty1) (nal2,ty2)
+      | LocalRawDef(na1,def1), LocalRawDef(na2,def2) ->
+          check_same_binder ([na1],def1) ([na2],def2)          
+      | _ -> failwith "not same binder") bl1 bl2
+
 let same c d = try check_same_type c d; true with _ -> false
 
 (**********************************************************************)
@@ -1502,21 +1513,27 @@ let rec extern inctx scopes vars r =
         (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars b1, sub_extern false scopes vars b2)
 
-  | RRec (loc,fk,idv,tyv,bv) ->
+  | RRec (loc,fk,idv,blv,tyv,bv) ->
       let vars' = Array.fold_right Idset.add idv vars in
       (match fk with
 	 | RFix (nv,n) ->
 	     let listdecl = 
 	       Array.mapi (fun i fi ->
-		 (fi,nv.(i), None, extern_type scopes vars tyv.(i),
-                  extern false scopes vars' bv.(i))) idv
+                 let (ids,bl) = extern_local_binder scopes vars blv.(i) in
+                 let vars0 = List.fold_right (name_fold Idset.add) ids vars in
+                 let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+		 (fi,nv.(i), bl, extern_type scopes vars1 tyv.(i),
+                  extern false scopes vars0 bv.(i))) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
 	 | RCoFix n -> 
 	     let listdecl =
                Array.mapi (fun i fi ->
-		 (fi,extern_type scopes vars tyv.(i),
-                  sub_extern false scopes vars' bv.(i))) idv
+                 let (ids,bl) = extern_local_binder scopes vars blv.(i) in
+                 let vars0 = List.fold_right (name_fold Idset.add) ids vars in
+                 let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+		 (fi,bl,extern_type scopes vars1 tyv.(i),
+                  sub_extern false scopes vars0 bv.(i))) idv
 	     in
 	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
 
@@ -1557,6 +1574,29 @@ and factorize_lambda inctx scopes vars aty = function
            ((loc,na)::nal,c)
   | c -> ([],sub_extern inctx scopes vars c)
 
+and extern_local_binder scopes vars = function
+    [] -> ([],[])
+  | (na,Some bd,ty)::l ->
+      let na = name_app translate_ident na in
+      let (ids,l) =
+        extern_local_binder scopes (name_fold Idset.add na vars) l in
+      (na::ids,
+       LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
+      
+  | (na,None,ty)::l ->
+      let na = name_app translate_ident na in
+      let ty = extern_type scopes vars (anonymize_if_reserved na ty) in
+      (match extern_local_binder scopes (name_fold Idset.add na vars) l with
+          (ids,LocalRawAssum(nal,ty')::l)
+            when same ty ty' &
+              match na with Name id -> not (occur_var_constr_expr id ty')
+                | _ -> true ->
+              (na::ids,
+               LocalRawAssum((dummy_loc,na)::nal,ty')::l)
+        | (ids,l) ->
+            (na::ids,
+             LocalRawAssum([(dummy_loc,na)],ty) :: l))
+
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
    extern inctx scopes vars c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a12df82f5b..0812baaac5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -530,18 +530,6 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function
 (**********************************************************************)
 (* Fix and CoFix                                                      *)
 
-let rec intern_fix = function
-  | [] -> ([],[],[],[])
-  | (fi, n, on, c, t)::rest->
-      let (lf,ln,lc,lt) = intern_fix rest in
-      (fi::lf, n::ln, c::lc, t::lt)
-
-let rec intern_cofix = function
-  | [] -> ([],[],[])
-  | (fi, c, t)::rest -> 
-      let (lf,lc,lt) = intern_cofix rest in
-      (fi::lf, c::lc, t::lt)
-
 (**********************************************************************)
 (* Utilities for binders                                              *)
 
@@ -688,8 +676,9 @@ let internalise sigma env allow_soapp lvar c =
 	(match intern_impargs c env imp subscopes l with
           | [] -> c
           | l -> RApp (constr_loc x, c, l))
-    | CFix (loc, (locid,iddef), ldecl) ->
-	let (lf,ln,lc,lt) = intern_fix ldecl in
+    | CFix (loc, (locid,iddef), dl) ->
+        let lf = List.map (fun (id,_,_,_,_) -> id) dl in
+        let dl = Array.of_list dl in
 	let n =
 	  try
 	    (list_index iddef lf) -1
@@ -697,12 +686,22 @@ let internalise sigma env allow_soapp lvar c =
 	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
 	in
 	let ids' = List.fold_right Idset.add lf ids in
-	let defl =
-	  Array.of_list (List.map (intern (ids',None,scopes)) lt) in
-	let arityl = Array.of_list (List.map (intern_type env) lc) in
-	RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
-    | CCoFix (loc, (locid,iddef), ldecl) ->
-	let (lf,lc,lt) = intern_cofix ldecl in
+        let idl = Array.map
+          (fun (id,n,bl,ty,bd) ->
+            let ((ids'',_,_),rbl) =
+              List.fold_left intern_local_binder (env,[]) bl in
+	    let ids''' = List.fold_right Idset.add lf ids'' in
+            (List.rev rbl,
+             intern_type (ids'',tmp_scope,scopes) ty,
+             intern (ids''',None,scopes) bd)) dl in
+	RRec (loc,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n),
+              Array.of_list lf,
+              Array.map (fun (bl,_,_) -> bl) idl,
+              Array.map (fun (_,ty,_) -> ty) idl,
+              Array.map (fun (_,_,bd) -> bd) idl)
+    | CCoFix (loc, (locid,iddef), dl) ->
+        let lf = List.map (fun (id,_,_,_) -> id) dl in
+        let dl = Array.of_list dl in
 	let n =
           try 
 	    (list_index iddef lf) -1
@@ -710,10 +709,19 @@ let internalise sigma env allow_soapp lvar c =
 	    raise (InternalisationError (locid,UnboundFixName (true,iddef)))
 	in
 	let ids' = List.fold_right Idset.add lf ids in
-	let defl =
-	  Array.of_list (List.map (intern (ids',None,scopes)) lt) in
-	let arityl = Array.of_list (List.map (intern_type env) lc) in
-	RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
+        let idl = Array.map
+          (fun (id,bl,ty,bd) ->
+            let ((ids'',_,_),rbl) =
+              List.fold_left intern_local_binder (env,[]) bl in
+	    let ids''' = List.fold_right Idset.add lf ids'' in
+            (List.rev rbl,
+             intern_type (ids'',tmp_scope,scopes) ty,
+             intern (ids''',None,scopes) bd)) dl in
+	RRec (loc,RCoFix n,
+              Array.of_list lf,
+              Array.map (fun (bl,_,_) -> bl) idl,
+              Array.map (fun (_,ty,_) -> ty) idl,
+              Array.map (fun (_,_,bd) -> bd) idl)
     | CArrow (loc,c1,c2) ->
         RProd (loc, Anonymous, intern_type env c1, intern_type env c2)
     | CProdN (loc,[],c2) ->
@@ -813,6 +821,17 @@ let internalise sigma env allow_soapp lvar c =
   and intern_type (ids,_,scopes) =
     intern (ids,Some Symbols.type_scope,scopes)
 
+  and intern_local_binder ((ids,ts,sc as env),bl) = function
+      LocalRawAssum(nal,ty) ->
+        let ids' = List.fold_left
+          (fun ids (_,na) -> name_fold Idset.add na ids) ids nal in
+        ((ids',ts,sc),
+         List.map (fun (_,na) ->
+           (na,None,intern_type env ty)) nal @bl)
+    | LocalRawDef((loc,na),def) ->
+        ((name_fold Idset.add na ids,ts,sc),
+         (na,Some(intern env def),RHole(loc,BinderType na))::bl)
+
   and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) =
 	let (idsl_substl_list,pl) =
 	  List.split 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index ed4cdba39f..8334922741 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -69,8 +69,13 @@ let rec unloc = function
       RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
   | RIf (_,c,(na,po),b1,b2) ->
       RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2)
-  | RRec (_,fk,idl,tyl,bv) ->
-      RRec (dummy_loc,fk,idl,Array.map unloc tyl,Array.map unloc bv)
+  | RRec (_,fk,idl,bl,tyl,bv) ->
+      RRec (dummy_loc,fk,idl,
+            Array.map (List.map 
+              (fun (na,obd,ty) -> (na,option_app unloc obd, unloc ty)))
+              bl,
+            Array.map unloc tyl,
+            Array.map unloc bv)
   | RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t)
   | RSort (_,x) -> RSort (dummy_loc,x)
   | RHole (_,x)  -> RHole (dummy_loc,x)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 3d26e9d7f8..1fe8edaca3 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -361,22 +361,27 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr = identifier * int * int option * constr_expr * constr_expr
+and fixpoint_expr =
+    identifier * int * local_binder list * constr_expr * constr_expr
 
-and cofixpoint_expr = identifier * constr_expr * constr_expr
+and local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * constr_expr
+
+and cofixpoint_expr =
+    identifier * local_binder list * constr_expr * constr_expr
 
 (***********************)
 (* For binders parsing *)
 
-type local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * constr_expr
-
 let rec local_binders_length = function
   | [] -> 0
   | LocalRawDef _::bl -> 1 + local_binders_length bl
   | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
 
+let names_of_local_assums bl =
+  List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
+
 (**********************************************************************)
 (* Functions on constr_expr *)
 
@@ -475,8 +480,19 @@ let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
 
 let map_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
-  let h (nal,t) (e,bl) = (map_binder g e nal,(nal,f e t)::bl) in
-  List.fold_right h bl (e,[])
+  let h (e,bl) (nal,t) = (map_binder g e nal,(nal,f e t)::bl) in
+  let (e,rbl) = List.fold_left h (e,[]) bl in
+  (e, List.rev rbl)
+
+let map_local_binders f g e bl =
+  (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
+  let h (e,bl) = function
+      LocalRawAssum(nal,ty) ->
+        (map_binder g e nal, LocalRawAssum(nal,f e ty)::bl)
+    | LocalRawDef((loc,na),ty) ->
+        (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in
+  let (e,rbl) = List.fold_left h (e,[]) bl in
+  (e, List.rev rbl)
 
 let map_constr_expr_with_binders f g e = function
   | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
@@ -518,9 +534,20 @@ let map_constr_expr_with_binders f g e = function
       let e' = option_fold_right (name_fold g) ona e in
       CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
-      CFix (loc,id,List.map (fun (id,n,on,t,d) -> (id,n,on,f e t,f e d)) dl)
+      CFix (loc,id,List.map (fun (id,n,bl,t,d) -> 
+        let (e',bl') = map_local_binders f g e bl in
+        let t' = f e' t in
+        (* Note: fix names should be inserted before the arguments... *)
+        let e'' = List.fold_left (fun e (id,_,_,_,_) -> g id e) e' dl in
+        let d' = f e'' d in
+        (id,n,bl',t',d')) dl)
   | CCoFix (loc,id,dl) ->
-      CCoFix (loc,id,List.map (fun (id,t,d) -> (id,f e t,f e d)) dl)
+      CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
+        let (e',bl') = map_local_binders f g e bl in
+        let t' = f e' t in
+        let e'' = List.fold_left (fun e (id,_,_,_) -> g id e) e' dl in
+        let d' = f e'' d in
+        (id,bl',t',d')) dl)
 
 (* Used in constrintern *)
 let rec replace_vars_constr_expr l = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index d35418b515..a56a96dea6 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -107,9 +107,16 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_expr = identifier * int * int option * constr_expr * constr_expr
+and fixpoint_expr =
+    identifier * int * local_binder list * constr_expr * constr_expr
+
+and cofixpoint_expr =
+    identifier * local_binder list * constr_expr * constr_expr
+
+and local_binder =
+  | LocalRawDef of name located * constr_expr
+  | LocalRawAssum of name located list * constr_expr
 
-and cofixpoint_expr = identifier * constr_expr * constr_expr
 
 val constr_loc : constr_expr -> loc
 
@@ -131,6 +138,14 @@ val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
 val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
 
+(* For binders parsing *)
+
+(* Includes let binders *)
+val local_binders_length : local_binder list -> int
+
+(* Does not take let binders into account *)
+val names_of_local_assums : local_binder list -> name located list
+
 (* Used in correctness and interface; absence of var capture not guaranteed *)
 (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
 
@@ -138,14 +153,6 @@ val map_constr_expr_with_binders :
   ('a -> constr_expr -> constr_expr) ->
       (identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr
 
-(* For binders parsing *)
-
-type local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * constr_expr
-
-val local_binders_length : local_binder list -> int
-
 (* Concrete syntax for modules and modules types *)
 
 type with_declaration_ast =