Changement de la structure des points fixes

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

10 files changed, 48 insertions, 42 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index e909d45111..b8d295aefd 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -30,7 +30,7 @@ with mindnames : ast :=
   mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ]
         -> [(VERNACARGLIST $id ($LIST $idl))]
 
-with idorstring_list: List :=
+with idorstring_list: ast list :=
   ids_nil  [ ] -> [ ]
 | ids_cons [ idorstring($x) idorstring_list($l) ] -> [ $x ($LIST $l) ]
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 807c7d4484..f08e69161f 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -65,7 +65,7 @@ and visit_ast eenv a =
     | MLcons (r,l) -> visit_reference eenv r; List.iter visit l
     | MLcase (a,br) -> 
 	visit a; Array.iter (fun (r,_,a) -> visit_reference eenv r; visit a) br
-    | MLfix (_,_,l) -> List.iter visit l
+    | MLfix (_,_,l) -> Array.iter visit l
     | MLcast (a,t) -> visit a; visit_type eenv t
     | MLmagic a -> visit a
     | MLrel _ | MLprop | MLarity | MLexn _ -> ()
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 99dce2f004..f559857e99 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -525,10 +525,10 @@ and extract_term_info_with_type env ctx c t =
 	  abstract_n n (abstract [] 1 s)
       | IsMutCase ((ni,(ip,cnames,_,_,_)),p,c,br) ->
 	  extract_case env ctx ni ip cnames p c br
-      | IsFix ((_,i),(ti,fi,ci)) -> 
-	  extract_fix env ctx i ti fi ci 
-      | IsCoFix (i,(ti,fi,ci)) -> 
-	  extract_fix env ctx i ti fi ci  
+      | IsFix ((_,i),recd) -> 
+	  extract_fix env ctx i recd
+      | IsCoFix (i,recd) -> 
+	  extract_fix env ctx i recd  
       | IsLetIn (n, c1, t1, c2) ->
 	  let id = id_of_name n in
 	  let env' = push_rel_def (n,c1,t1) env in
@@ -591,11 +591,13 @@ and extract_case env ctx ni ip cnames p c br =
 	 assert (Array.length br = 1);
 	 snd (extract_branch_aux 0 br.(0)))
   
-and extract_fix env ctx i ti fi ci = 
+and extract_fix env ctx i (fi,ti,ci as recd) = 
   let n = Array.length ti in
+  let env' = push_rec_types recd env in
   let ti' = Array.mapi lift ti in 
-  let lb = (List.combine fi (Array.to_list ti')) in
-  let env' = push_rels_assum (List.rev lb) env in
+  let lb =
+    Array.to_list
+      (array_map2_i (fun i na t -> (na, type_app (lift i) t)) fi ti) in
   let ctx' = 
     lbinders_fold (fun _ _ v a -> (snd v = NotArity) :: a) ctx env lb in
   let extract_fix_body c t =
@@ -603,8 +605,8 @@ and extract_fix env ctx i ti fi ci =
       | Emltype _ -> MLarity
       | Emlterm a -> a
   in
-  let ei = Array.to_list (array_map2 extract_fix_body ci ti) in
-  MLfix (i, List.map id_of_name fi, ei)
+  let ei = array_map2 extract_fix_body ci ti in
+  MLfix (i, Array.map id_of_name fi, ei)
 
 and extract_app env ctx (f,tyf,sf) args =
   let nargs = List.length args in
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 565932596e..c2ed8e7a97 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -39,7 +39,7 @@ type ml_ast =
   | MLglob  of global_reference
   | MLcons  of global_reference * ml_ast list
   | MLcase  of ml_ast * (global_reference * identifier list * ml_ast) array
-  | MLfix   of int * identifier list * ml_ast list
+  | MLfix   of int * identifier array * ml_ast array
   | MLexn   of identifier
   | MLprop
   | MLarity
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 0bd5ec3a60..fafdcdd012 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -46,11 +46,13 @@ let rec occurs k = function
       (occurs k t) ||
       (array_exists
 	 (fun (_,l,t') -> let k' = List.length l in occurs (k + k') t') pv)
-  | MLfix(_,l,cl) -> let k' = List.length l in occurs_list (k + k') cl
+  | MLfix(_,l,cl) -> let k' = Array.length l in occurs_vect (k + k') cl
   | _ -> false
 
 and occurs_list k l = List.exists (occurs k) l
 
+and occurs_vect k v = array_exists (occurs k) v
+
 (*s map over ML asts *)
 
 let rec ast_map f = function
@@ -59,7 +61,7 @@ let rec ast_map f = function
   | MLletin (id,a,b) -> MLletin (id, f a, f b)
   | MLcons (c,al) -> MLcons (c, List.map f al)
   | MLcase (a,eqv) -> MLcase (f a, Array.map (ast_map_eqn f) eqv)
-  | MLfix (fi,ids,al) -> MLfix (fi, ids, List.map f al)
+  | MLfix (fi,ids,al) -> MLfix (fi, ids, Array.map f al)
   | MLcast (a,t) -> MLcast (f a, t)
   | MLmagic a -> MLmagic (f a)
   | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> a
@@ -84,7 +86,7 @@ let ml_liftn k n c =
 			     (id, idl, liftrec (n+k) p)) pl)
     | MLfix (n0,idl,pl) -> 
 	MLfix (n0,idl,
-	       let k = List.length idl in List.map (liftrec (n+k)) pl)
+	       let k = Array.length idl in Array.map (liftrec (n+k)) pl)
     | a -> ast_map (liftrec n) a
   in 
   if k = 0 then c else liftrec n c
@@ -115,10 +117,10 @@ let rec ml_subst v =
       	       		     (id,ids,subst (n+k) (ml_lift k m) t)) pv)
     | MLfix (i,ids,cl) -> 
 	MLfix (i,ids, 
-	       let k = List.length ids in
-	       List.map (subst (n+k) (ml_lift k m)) cl)
-    | a -> 
-	ast_map (subst n m) a
+	       let k = Array.length ids in
+	       Array.map (subst (n+k) (ml_lift k m)) cl)
+    | a ->
+        ast_map (subst n m) a
   in 
   subst 1 v
 
@@ -145,7 +147,7 @@ let nb_occur a =
 	count n t;
 	Array.iter (fun (_,l,t) -> let k = List.length l in count (n + k) t) pv
     | MLfix (_,ids,cl) -> 
-	let k = List.length ids in List.iter (count (n + k)) cl
+	let k = Array.length ids in Array.iter (count (n + k)) cl
     | MLapp (a,l) -> count n a; List.iter (count n) l
     | MLcons (_,l) ->  List.iter (count n) l
     | MLmagic a -> count n a
@@ -238,7 +240,7 @@ let rec ml_size = function
   | MLcons(_,l) -> ml_size_list l
   | MLcase(t,pv) -> 
       1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
-  | MLfix(_,_,f) -> ml_size_list f
+  | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
   | MLcast (t,_) -> ml_size t
   | MLmagic t -> ml_size t
@@ -246,6 +248,8 @@ let rec ml_size = function
 
 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
 
+and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l
+
 let is_fix = function MLfix _ -> true | _ -> false
 
 let rec is_constr = function
@@ -296,9 +300,9 @@ let rec non_stricts add cand = function
       let cand = non_stricts false cand t1 in 
       pop 1 (non_stricts add (lift 1 cand) t2)
   | MLfix (_,i,f)-> 
-      let n = List.length i in
+      let n = Array.length i in
       let cand = lift n cand in 
-      let cand = List.fold_left (non_stricts false) cand f in 
+      let cand = Array.fold_left (non_stricts false) cand f in 
       pop n cand
   | MLcase (t,v) -> 
       (* The only interesting case: for a variable to be non-strict, 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 0945b79cb6..2fdc8c8ac6 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -218,8 +218,8 @@ let rec pp_expr par env args =
 		    'fNL; 'sTR "  "; pp_pat env pv >];
 	     if args <> [] then [< 'sTR ")" >] else close_par par >]
     | MLfix (i,ids,defs) ->
-	let ids',env' = push_vars (List.rev ids) env in
-      	pp_fix par env' (Some i) (List.rev ids',defs) args
+	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+      	pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
     | MLexn id -> 
 	[< open_par par; 'sTR "failwith"; 'sPC; 
 	   'qS (string_of_id id); close_par par >]
@@ -256,14 +256,14 @@ and pp_pat env pv =
 and pp_fix par env in_p (ids,bl) args =
   [< open_par par; 
      v 0 [< 'sTR "let rec " ;
-	    prlist_with_sep
+	    prvect_with_sep
       	      (fun () -> [< 'fNL; 'sTR "and " >])
 	      (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	      (List.combine ids bl);
+	      (array_map2 (fun id b -> (id,b)) ids bl);
 	    'fNL;
 	    match in_p with
 	      | Some j -> 
-      		  hOV 2 [< 'sTR "in "; pr_id (List.nth ids j);
+      		  hOV 2 [< 'sTR "in "; pr_id (ids.(j));
 			   if args <> [] then
 			     [< 'sTR " "; 
 				prlist_with_sep (fun () -> [<'sTR " ">])
@@ -351,10 +351,10 @@ let pp_decl = function
       hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; 
 	       pp_type_global r; 'sPC; 'sTR "="; 'sPC; 
 	       pp_type false  t; 'fNL >]
-  | Dglob (r, MLfix (_,[_],[def])) ->
+  | Dglob (r, MLfix (_,[|_|],[|def|])) ->
       let id = P.rename_global r in
       let env' = ([id], !current_ids) in
-      [<  hOV 2 (pp_fix false env' None ([id],[def]) []) >]
+      [<  hOV 2 (pp_fix false env' None ([|id|],[|def|]) []) >]
   | Dglob (r, a) ->
       hOV 0 [< 'sTR "let "; 
 	       pp_function (empty_env ()) (pp_global r) a; 'fNL >]
diff --git a/contrib/field/Field.v b/contrib/field/Field.v
index b3261d3ea3..eb82846d73 100644
--- a/contrib/field/Field.v
+++ b/contrib/field/Field.v
@@ -14,14 +14,14 @@ Require Export Field_Tactic.
 
 Declare ML Module "field".
 
-Grammar vernac opt_arg_list : List :=
+Grammar vernac opt_arg_list : ast list :=
 | noal [] -> []
 | minus [ "minus" ":=" constrarg($aminus) opt_arg_list($l) ] ->
   [ "minus" $aminus ($LIST $l) ]
 | div [ "div" ":=" constrarg($adiv) opt_arg_list($l) ] ->
   [ "div" $adiv ($LIST $l) ]
 
-with extra_args : List :=
+with extra_args : ast list :=
 | nea [] -> []
 | with_a [ "with" opt_arg_list($l)] -> [ ($LIST $l) ]
 
diff --git a/contrib/interface/Centaur.v b/contrib/interface/Centaur.v
index 80142df4d0..f2e1686455 100644
--- a/contrib/interface/Centaur.v
+++ b/contrib/interface/Centaur.v
@@ -34,15 +34,15 @@ Grammar vernac vernac : ast :=
 (* | show_dad_rules [ "Show" "Dad" "Rules" "." ] -> [(Show_dad_rules)] *)
 | start_pcoq [ "Start" "Pcoq" "Mode" "." ] -> [ (START_PCOQ) ]
 | start_pcoq [ "Start" "Pcoq" "Debug" "Mode" "." ] -> [ (START_PCOQ_DEBUG) ].
-Grammar vernac ne_id_list : List :=
+Grammar vernac ne_id_list : ast list :=
    id_one [ identarg($id)] -> [$id]
  | id_more [identarg($id) ne_id_list($others)] -> [$id ($LIST $others)].
 
-Grammar tactic ne_num_list : List :=
+Grammar tactic ne_num_list : ast list :=
   ne_last [ numarg($n) ] -> [ $n ]
 | ne_num_ste  [ numarg($n) ne_num_list($ns) ] -> [ $n ($LIST $ns)].
 
-Grammar tactic two_numarg_list : List :=
+Grammar tactic two_numarg_list : ast list :=
   two_single_and_ne [ numarg($n) "to"  ne_num_list($ns)] ->
         [$n (TACTIC (to)) ($LIST $ns)]
 | two_rec [ numarg($n) two_numarg_list($ns)] -> [ $n ($LIST $ns)].
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index e4297ce85e..7908af7ecd 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -226,7 +226,7 @@ let compute_ivs gl f cs =
   let cst = try destConst f with _ -> i_can't_do_that () in
   let body = constant_value (Global.env()) cst in
   match decomp_term body with
-    | IsFix(([| len |], 0), ([| typ |], [ name ], [| body2 |])) ->
+    | IsFix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
         let (args3, body3) = decompose_lam body2 in
         let nargs3 = List.length args3 in
         begin match decomp_term body3 with
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 3927827276..573f4319b3 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -446,7 +446,7 @@ let print_term inner_types l env csr =
             ) a [<>]
         >]
 )
-   | T.IsFix ((ai,i),((t,f,b) as rec_decl)) ->
+   | T.IsFix ((ai,i),((f,t,b) as rec_decl)) ->
       X.xml_nempty "FIX"
        (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id])
 (force
@@ -458,7 +458,7 @@ let print_term inner_types l env csr =
                      [< term_display idradix false l env ti >] ;
 	            X.xml_nempty "body" [] [<
                      term_display idradix false
-                      ((List.rev f)@l)
+                      ((Array.to_list f)@l)
                       (E.push_rec_types rec_decl env)
                       bi
                     >]
@@ -466,11 +466,11 @@ let print_term inner_types l env csr =
                 i
              >]
            )
-	   (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) (Array.of_list f) )
+	   (Array.mapi (fun j x -> (x,t.(j),b.(j),ai.(j)) ) f )
            [<>]
        >]
 )
-   | T.IsCoFix (i,((t,f,b) as rec_decl)) ->
+   | T.IsCoFix (i,((f,t,b) as rec_decl)) ->
       X.xml_nempty "COFIX"
        (add_sort_attribute true ["noFun", (string_of_int i) ; "id",next_id])
 (force
@@ -481,7 +481,7 @@ let print_term inner_types l env csr =
                     [< term_display idradix false l env ti >] ;
 	           X.xml_nempty "body" [] [<
                     term_display idradix false
-                     ((List.rev f)@l)
+                     ((Array.to_list f)@l)
                      (E.push_rec_types rec_decl env)
                      bi
                    >]
@@ -489,7 +489,7 @@ let print_term inner_types l env csr =
                i
             >]
 	   )
-	   (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) (Array.of_list f) ) [<>]
+	   (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) f ) [<>]
        >]
 )
    | T.IsEvar _ ->