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

10 files changed, 57 insertions, 70 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index a5a153bdb7..6d1c1b145e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1602,7 +1602,7 @@ let cvt_fixpoint_binder = function
        xlate_constr c)
   | [],c -> xlate_error "Shouldn't occur"
 
-let cvt_fixpoint_binders args =
+let cvt_fixpoint_binders bl =
   CT_binder_list(List.map cvt_fixpoint_binder args)
 
 let xlate_vernac =
@@ -1872,11 +1872,14 @@ let xlate_vernac =
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
    | VernacFixpoint [] -> xlate_error "mutual recursive"
    | VernacFixpoint (lm :: lmi) ->
-      let strip_mutrec (fid, bl, arf, ardef) =
+      let strip_mutrec (fid, n, arf, ardef) =
+        let arf = xlate_constr arf in
+        let ardef = xlate_constr ardef in
+        let (bl,arf,ardef) = split_fix n arf ardef in
 	match cvt_fixpoint_binders bl with
 	  | CT_binder_list (b :: bl) ->
 	      CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
-	        xlate_constr arf, xlate_constr ardef)
+                arf, ardef)
           | _ -> xlate_error "mutual recursive" in
         CT_fix_decl
 	  (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b9f22ff006..0ae4c2214c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -196,22 +196,9 @@ let rec extern = function
   | RRec (_,fk,idv,tyv,bv) ->
       (match fk with
 	 | RFix (nv,n) ->
-             let rec split_lambda binds = function
-	       | (0, t) -> (List.rev binds,extern t)
-	       | (n, RLambda (_,na,t,b)) ->
-		   split_lambda (([loc,na],extern t)::binds) (n-1,b)
-	       | _ -> anomaly "extern: ill-formed fixpoint body" in
-	     let rec split_product = function
-	       | (0, t) -> extern t
-	       | (n, RProd (_,na,t,b)) -> split_product (n-1,b)
-	       | _ -> anomaly "extern: ill-formed fixpoint type" in
 	     let listdecl = 
 	       Array.mapi
-		 (fun i fi ->
-		    let (lparams,def) = split_lambda [] (nv.(i)+1,bv.(i)) in
-		    let typ = split_product (nv.(i)+1,tyv.(i)) in
-		    (fi, lparams, typ, def))
-		 idv
+		 (fun i fi -> (fi,nv.(i),extern tyv.(i),extern bv.(i))) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
 	 | RCoFix n -> 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2ce1a4db0f..e760f3e929 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -293,12 +293,9 @@ let rec intern_cases_pattern scopes aliases = function
 
 let rec intern_fix = function
   | [] -> ([],[],[],[])
-  | (fi, bl, c, t)::rest->
-      let ni = List.length (List.flatten (List.map fst bl)) - 1 in
+  | (fi, n, c, t)::rest->
       let (lf,ln,lc,lt) = intern_fix rest in
-      (fi::lf, ni::ln, 
-       CProdN (dummy_loc, bl, c)::lc, 
-       CLambdaN (dummy_loc, bl, t)::lt)
+      (fi::lf, n::ln, c::lc, t::lt)
 
 let rec intern_cofix = function
   | [] -> ([],[],[])
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 8569c414bd..6ed371a46c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -163,9 +163,7 @@ type constr_expr =
   | CDelimiters of loc * scope_name * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_binder = name located list * constr_expr 
-
-and fixpoint_expr = identifier * fixpoint_binder list * constr_expr * constr_expr
+and fixpoint_expr = identifier * int * constr_expr * constr_expr
 
 and cofixpoint_expr = identifier * constr_expr * constr_expr
 
@@ -273,9 +271,7 @@ let map_constr_expr_with_binders f g e = function
   | COrderedCase (loc,s,po,a,bl) ->
       COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl)
   | CFix (loc,id,dl) ->
-      let k (id,bl,t,d) = 
-	let (e,bl) = map_binders f g e bl in (id,bl,f e t,f e d) in
-      CFix (loc,id,List.map k dl)
+      CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,f e t,f e d)) dl)
   | CCoFix (loc,id,dl) ->
       CCoFix (loc,id,List.map (fun (id,t,d) -> (id,f e t,f e d)) dl)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 72845f8967..7b9c426350 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -82,9 +82,7 @@ type constr_expr =
   | CDelimiters of loc * scope_name * constr_expr
   | CDynamic of loc * Dyn.t
 
-and fixpoint_binder = name located list * constr_expr 
-
-and fixpoint_expr = identifier * fixpoint_binder list * constr_expr * constr_expr
+and fixpoint_expr = identifier * int * constr_expr * constr_expr
 
 and cofixpoint_expr = identifier * constr_expr * constr_expr
 
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
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 19842ea627..eb911b4d21 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -311,18 +311,13 @@ let build_recursive lnameargsardef =
   let lrecnames = List.map (fun (f,_,_,_) -> f) lnameargsardef 
   and sigma = Evd.empty
   and env0 = Global.env()
-  and nv = Array.of_list 
-    (List.map
-      (fun (_,la,_,_) -> List.length (List.flatten (List.map fst la)) - 1)
-        lnameargsardef)
-  in
+  and nv = Array.of_list (List.map (fun (_,n,_,_) -> n) lnameargsardef) in
   let fs = States.freeze() in
   let (rec_sign,arityl) = 
     try 
       List.fold_left 
-        (fun (env,arl) (recname,lparams,arityc,_) -> 
-           let raw_arity = mkProdCit lparams arityc in
-           let arity = interp_type sigma env0 raw_arity in
+        (fun (env,arl) (recname,_,arityc,_) -> 
+           let arity = interp_type sigma env0 arityc in
            let _ = declare_variable recname
 	     (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in
            (Environ.push_named (recname,None,arity) env, (arity::arl)))
@@ -333,8 +328,8 @@ let build_recursive lnameargsardef =
   let recdef =
     try 
       List.map2
-	(fun (_,lparams,_,def) arity ->
-           interp_casted_constr sigma rec_sign (mkLambdaCit lparams def) arity)
+	(fun (_,_,_,def) arity ->
+          interp_casted_constr sigma rec_sign def arity)
         lnameargsardef arityl
     with e ->
       States.unfreeze fs; raise e