Passage à une représentation des fixpoints plus primitive dans constr_expr (càd avec indices)

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

4 files changed, 40 insertions, 29 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index bd31a78b4c..8644cb724b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -17,28 +17,6 @@ open Libnames
 open Prim
 open Topconstr
 
-(* For the very old syntax of fixpoints *)
-let split_lambda = function
-  | CLambdaN (loc,[[na],t],c) -> (na,t,c)
-  | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
-  | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c))
-  | _ -> Util.error "ill-formed fixpoint body"
-
-let split_product = function
-  | CArrow (loc,t,c) -> ((loc,Anonymous),t,c)
-  | CProdN (loc,[[na],t],c) -> (na,t,c)
-  | CProdN (loc,([na],t)::bl,c) -> (na,t,CProdN(loc,bl,c))
-  | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,t)::bl,c))
-  | _ -> Util.error "ill-formed fixpoint body"
-
-let rec split_fix n typ def =
-  if n = 0 then ([],typ,def)
-  else
-    let (na,_,def) = split_lambda def in
-    let (_,t,typ) = split_product typ in
-    let (bl,typ,def) = split_fix (n-1) typ def in
-    (([na],t)::bl,typ,def)
-
 let coerce_to_var = function
   | CRef (Ident (_,id)) -> id
   | ast -> Util.user_err_loc
@@ -272,12 +250,14 @@ GEXTEND Gram
   fixbinder:
     [ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
         ":="; def = constr ->
-	  Options.if_verbose Pp.warning 
-          "Checking of the fixpoint type not done for very-old-style fixpoint";
-	  let (bl, typ, def) = split_fix recarg type_ def in (id, bl, typ, def)
+          (id, recarg-1, type_, def)
       | id = base_ident; bl = ne_simple_binders_list; ":"; type_ = constr;
 	":="; def = constr ->
-	  (id, bl, type_, def) ] ]
+          let ni = List.length (List.flatten (List.map fst bl)) -1 in
+          let loc0 = fst (List.hd (fst (List.hd 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)) ] ]
   ;
   fixbinders:
     [ [ fbs = LIST1 fixbinder SEP "with" -> fbs ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f347ac20ed..36619758a0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -242,8 +242,13 @@ GEXTEND Gram
       | IDENT "Minimality"; IDENT "for" -> false ] ]
   ;
   onerec:
-    [ [ id = base_ident; idl = ne_fix_binders; ":"; c = constr;
-        ":="; def = constr -> (id,idl,c,def) ] ]
+    [ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
+        ":="; def = constr ->
+          let ni = List.length (List.flatten (List.map fst bl)) - 1 in
+          let loc0 = fst (List.hd (fst (List.hd 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)) ] ]
   ;
   specifrec:
     [ [ l = LIST1 onerec SEP "with" -> l ] ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 6dd9211bb9..baac4a06d7 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -153,7 +153,29 @@ let pr_recursive_decl pr id b t c =
   brk (1,2) ++ str ": " ++ pr ltop t ++ str ":=" ++
   brk (1,2) ++ pr ltop c
 
-let pr_fixdecl pr (id,bl,t,c) =
+let split_lambda = function
+  | CLambdaN (loc,[[na],t],c) -> (na,t,c)
+  | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
+  | CLambdaN (loc,(na::nal,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,t)::bl,c))
+  | _ -> anomaly "ill-formed fixpoint body"
+
+let split_product = function
+  | CArrow (loc,t,c) -> ((loc,Anonymous),t,c)
+  | CProdN (loc,[[na],t],c) -> (na,t,c)
+  | CProdN (loc,([na],t)::bl,c) -> (na,t,CProdN(loc,bl,c))
+  | CProdN (loc,(na::nal,t)::bl,c) -> (na,t,CProdN(loc,(nal,t)::bl,c))
+  | _ -> anomaly "ill-formed fixpoint body"
+
+let rec split_fix n typ def =
+  if n = 0 then ([],typ,def)
+  else
+    let (na,_,def) = split_lambda def in
+    let (_,t,typ) = split_product typ in
+    let (bl,typ,def) = split_fix (n-1) typ def in
+    (([na],t)::bl,typ,def)
+
+let pr_fixdecl pr (id,n,t,c) =
+  let (bl,t,c) = split_fix (n+1) t c in
   pr_recursive_decl pr id 
     (brk (1,2) ++ str "[" ++ pr_binders pr bl ++ str "]") t c
 
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index bd95637fa4..dc305f6330 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -18,6 +18,10 @@ open Extend
 open Coqast
 open Topconstr
 open Names
+open Util
+
+val split_fix : int -> constr_expr -> constr_expr -> 
+  (name located list * constr_expr) list * constr_expr * constr_expr
 
 val pr_global : global_reference -> std_ppcmds