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, 6 insertions, 28 deletions

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