Prise en compte des definitions locales dans les (co-)points-fixes

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

2 files changed, 51 insertions, 38 deletions

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index f3883c7634..bd8ca6aadb 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -45,11 +45,39 @@ let mk_lam = function
 let mk_match (loc,cil,rty,br) =
   CCases(loc,(None,rty),cil,br)
 
-let index_of_annot bl ann =
-  match bl,ann with
-      [([_],_)], None -> 0
-    | _, Some x ->
-        let ids = List.map snd (List.flatten (List.map fst bl)) in
+let loc_of_binder_let = function
+  | LocalRawAssum ((loc,_)::_,_)::_ -> loc
+  | LocalRawDef ((loc,_),_)::_ -> loc
+  | _ -> dummy_loc
+
+let rec mkCProdN loc bll c =
+  match bll with
+  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
+      CProdN (loc,[idl,t],mkCProdN (join_loc loc1 loc) bll c)
+  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
+      CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
+  | [] -> c
+  | LocalRawAssum ([],_) :: bll -> mkCProdN loc bll c
+
+let rec mkCLambdaN loc bll c =
+  match bll with
+  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
+      CLambdaN (loc,[idl,t],mkCLambdaN (join_loc loc1 loc) bll c)
+  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
+      CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
+  | [] -> c
+  | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
+
+let rec decls_of_binders = function
+  | [] -> []
+  | LocalRawDef _::bl -> decls_of_binders bl
+  | LocalRawAssum (idl,_)::bl -> idl @ decls_of_binders bl
+
+let rec index_of_annot bl ann =
+  match decls_of_binders bl,ann with
+    | [_], None -> 0
+    | lids, Some x ->
+        let ids = List.map snd lids in
         (try list_index (snd x) ids - 1
         with Not_found -> error "no such fix variable")
     | _ -> error "cannot guess decreasing argument of fix"
@@ -58,8 +86,8 @@ let mk_fixb (loc,id,bl,ann,body,(tloc,tyc)) =
   let n = index_of_annot bl ann in
   let ty = match tyc with
       None -> CHole tloc
-    | Some t -> CProdN(loc,bl,t) in
-  (snd id,n,ty,CLambdaN(loc,bl,body))
+    | Some t -> mkCProdN loc bl t in
+  (snd id,n,ty,mkCLambdaN loc bl body)
 
 let mk_cofixb (loc,id,bl,ann,body,(tloc,tyc)) =
   let _ = option_app (fun (aloc,_) ->
@@ -68,8 +96,8 @@ let mk_cofixb (loc,id,bl,ann,body,(tloc,tyc)) =
        Pp.str"Annotation forbidden in cofix expression")) ann in
   let ty = match tyc with
       None -> CHole tloc
-    | Some t -> CProdN(loc,bl,t) in
-  (snd id,ty,CLambdaN(loc,bl,body))
+    | Some t -> mkCProdN loc bl t in
+  (snd id,ty,mkCLambdaN loc bl body)
 
 let mk_fix(loc,kw,id,dcls) =
   if kw then 
@@ -85,24 +113,6 @@ let mk_single_fix (loc,kw,dcl) =
 let binder_constr =
   create_constr_entry (get_univ "constr") "binder_constr"
 
-let rec mkCProdN loc bll c =
-  match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
-      CProdN (loc,[idl,t],mkCProdN (join_loc loc1 loc) bll c)
-  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
-      CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
-  | [] -> c
-  | LocalRawAssum ([],_) :: bll -> mkCProdN loc bll c
-
-let rec mkCLambdaN loc bll c =
-  match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
-      CLambdaN (loc,[idl,t],mkCLambdaN (join_loc loc1 loc) bll c)
-  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
-      CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
-  | [] -> c
-  | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
-
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
 (* admissible notation "(x t)" *)
 let lpar_id_coloneq =
@@ -195,10 +205,7 @@ GEXTEND Gram
           mkCLambdaN loc bl c
       | "let"; id=name; bl = LIST0 binder_let; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
-          let loc1 = match bl with
-            | LocalRawAssum ((loc,_)::_,_)::_ -> loc
-            | LocalRawDef ((loc,_),_)::_ -> loc
-            | _ -> dummy_loc in
+          let loc1 = loc_of_binder_let bl in
           CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
@@ -245,7 +252,7 @@ GEXTEND Gram
       | "cofix" -> false ] ]
   ;
   fix_decl:
-    [ [ id=identref; bl=LIST0 binder; ann=fixannot; ty=type_cstr; ":=";
+    [ [ id=identref; bl=LIST0 binder_let; ann=fixannot; ty=type_cstr; ":=";
         c=operconstr LEVEL "200" -> (loc,id,bl,ann,c,ty) ] ]
   ;
   fixannot:
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 965b11bfd5..4ea3368532 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -206,10 +206,10 @@ GEXTEND Gram
   ;
   (* (co)-fixpoints *)
   rec_definition:
-    [ [ id = base_ident; bl = LIST1 binder_nodef;
+    [ [ id = base_ident; bl = LIST1 binder_let;
         annot = OPT rec_annotation; type_ = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
-          let names = List.map snd (List.flatten (List.map fst bl)) in
+          let names = List.map snd (G_constrnew.decls_of_binders bl) in
           let ni =
             match annot with
                 Some id ->
@@ -223,15 +223,17 @@ GEXTEND Gram
                       (loc,"Fixpoint",
                        Pp.str "the recursive argument needs to be specified");
                   0 in
-          let loc0 = fst (List.hd (fst (List.hd bl))) in
+          let loc0 = G_constrnew.loc_of_binder_let bl in
           let loc1 = join_loc loc0 (constr_loc type_) in
           let loc2 = join_loc loc0 (constr_loc def) in
-	  ((id, ni, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)),ntn) ] ]
+	  ((id, ni, G_constrnew.mkCProdN loc1 bl type_,
+	    G_constrnew.mkCLambdaN loc2 bl def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = base_ident; bl = LIST0 binder_nodef; c = type_cstr; ":=";
+    [ [ id = base_ident; bl = LIST0 binder_let; c = type_cstr; ":=";
         def = lconstr ->
-          (id,CProdN(loc,bl,c),CLambdaN(loc,bl,def)) ] ]
+          (id,G_constrnew.mkCProdN loc bl c ,
+	   G_constrnew.mkCLambdaN loc bl def) ] ]
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> id_of_string id ] ]
@@ -251,6 +253,7 @@ GEXTEND Gram
       | IDENT "Minimality" -> false ] ]
   ;
   (* Various Binders *)
+(*
   (* ... without coercions *)
   binder_nodef:
     [ [ b = binder_let ->
@@ -260,6 +263,7 @@ GEXTEND Gram
             Util.user_err_loc
               (loc,"fix_param",Pp.str"defined binder not allowed here")) ] ]
   ;
+*)
   (* ... with coercions *)
   record_field:
     [ [ id = base_ident -> (false,AssumExpr(id,CHole loc))
@@ -589,7 +593,9 @@ GEXTEND Gram
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> PrintCoercionPaths (s,t)
       | IDENT "Tables" -> PrintTables
+(* Obsolete: was used for cooking V6.3 recipes ??
       | IDENT "Proof"; qid = global -> PrintOpaqueName qid
+*)
       | IDENT "Hint" -> PrintHintGoal
       | IDENT "Hint"; qid = global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb