Deplacement de l'optim singleton depuis extraction vers mlutil. Autres modifs mineures

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

5 files changed, 73 insertions, 98 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 65cc52fe8..637a30bd7 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -21,6 +21,12 @@ open Nametab
 
 let current_module = ref None
 
+let sp_of_r r = match r with 
+    | ConstRef sp -> sp
+    | IndRef (sp,_) -> sp
+    | ConstructRef ((sp,_),_) -> sp
+    | _ -> assert false
+
 let module_of_r r = 
   snd (split_dirpath (dirpath (sp_of_r r)))
 
@@ -36,7 +42,6 @@ let check_ml r d =
     with Not_found -> d
   else d
 
-
 (*s tables of global renamings *)
 
 let keywords = ref Idset.empty
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 33f93a8ac..e322cc0a6 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -21,7 +21,9 @@ open Nametab
 open Vernacinterp
 open Common
 
-(*s [extract_module m] returns all the global reference declared in a module *)
+(*s [extract_module m] returns all the global reference declared 
+  in a module. This is done by traversing the segment of module [M]. 
+  We just keep constants and inductives. *)
 
 let extract_module m =
   let m = Nametab.locate_loaded_library (Nametab.make_short_qualid m) in
@@ -146,6 +148,7 @@ let local_optimize refs =
   let prm = 
     { lang = "ocaml" ; toplevel = true; 
       mod_name = None; to_appear = refs} in
+  clear_singletons ();
   optimize prm (decl_of_refs refs)
 
 let print_user_extract r = 
@@ -185,7 +188,7 @@ let _ =
        let rl = refs_of_vargl vl in 
        let ml_rl = List.filter is_ml_extraction rl in
        let rl = List.filter (fun x -> not (is_ml_extraction x)) rl in 
-       let dl = decl_of_refs rl in
+       let dl = local_optimize rl in
        List.iter print_user_extract ml_rl ;
        List.iter (fun d -> mSGNL (ToplevelPp.pp_decl d)) dl)
 
@@ -198,6 +201,7 @@ let _ =
     (function 
        | VARG_STRING lang :: VARG_STRING f :: vl ->
 	   (fun () -> 
+	      clear_singletons ();
 	      let refs = refs_of_vargl vl in
 	      let prm = {lang=lang;
 			 toplevel=false;
@@ -209,10 +213,8 @@ let _ =
 	      extract_to_file f prm decls)
        | _ -> assert false)
 
-(*s Extraction of a module. The vernacular command is \verb!Extraction Module!
-    [M]. We build the environment to extract by traversing the segment of
-    module [M]. We just keep constants and inductives, and we remove
-    those having an ML extraction. *)
+(*s Extraction of a module. The vernacular command is 
+  \verb!Extraction Module! [M]. *) 
 
 let decl_in_m m = function 
   | Dglob (r,_) -> m = module_of_r r
@@ -231,6 +233,7 @@ let _ =
     (function 
        | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
+	      clear_singletons ();
 	      let f = (String.uncapitalize (string_of_id m))
 		       ^ (file_suffix lang) in
 	      let prm = {lang=lang;
@@ -244,12 +247,15 @@ let _ =
 	      extract_to_file f prm decls)
        | _ -> assert false)
 
+(*s Recusrive Extraction of all the modules [M] depends on. 
+  The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
 
 let _ = 
   vinterp_add "RecursiveExtractionModule"
         (function 
        | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
+	      clear_singletons ();
 	      let modules,refs = modules_extract_env m in 
 	      let dummy_prm = {lang=lang;
 			      toplevel=false;
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 15d0977e3..34f7a78dc 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -557,21 +557,14 @@ and extract_term_info_with_type env ctx c t =
    produces: 
 
    [fun ]$p_1 \ldots p_n ~ x_1 \ldots x_n $[-> C(]$x_{i_1},\ldots, x_{i_k}$[)].
-   This ML term will be reduced later on when applied, see [mlutil.ml].
-
-   In the special case of a informative singleton inductive, [C] is identity *)
+   This ML term will be reduced later on when applied, see [mlutil.ml]. *)
 
 and abstract_constructor cp  =
   let s,n = signature_of_constructor cp in 
   let rec abstract rels i = function
     | [] -> 
 	let rels = List.rev_map (fun x -> MLrel (i-x)) rels in
-	if is_singleton_constructor cp then 
-	  match rels with 
-	    | [var]->var
-	    | _ -> assert false
-	else
-	  MLcons (ConstructRef cp, rels)
+	MLcons (ConstructRef cp, rels)
     | (Info,NotArity) :: l -> 
 	MLlam (id_of_name Anonymous, abstract (i :: rels) (succ i) l)
     | (Logic,NotArity) :: l ->
@@ -611,18 +604,7 @@ and extract_case env ctx ip c br =
   (* [c] has an inductive type, not an arity type *)
   (match extract_term env ctx c with
      | Rmlterm a -> 
-	 if is_singleton_inductive ip then 
-	   begin
-	     (* Informative singleton case: *)
-	     (* [match c with C i -> t] becomes [let i = c' in t'] *)
-	     assert (Array.length br = 1);
-	     let (_,ids,e') = extract_branch 0 br.(0) in
-	     assert (List.length ids = 1);
-	     MLletin (List.hd ids,a,e')
-	   end
-	 else
-	   (* Standard case: we apply [extract_branch]. *)
-	   MLcase (a, Array.mapi extract_branch br)
+	 MLcase (a, Array.mapi extract_branch br)
      | Rprop -> 
 	 (* Logical singleton case: *)
 	 (* [match c with C i j k -> t] becomes [t'] *)
@@ -756,21 +738,6 @@ and extract_constructor (((sp,_),_) as c) =
   extract_mib sp;
   lookup_constructor_extraction c
 
-(* Looking for informative singleton case, i.e. an inductive with one 
-   constructor which has one informative argument. This dummy case will 
-   be simplified. *)
-
-and is_singleton_inductive ind = 
-  let (mib,mip) = Global.lookup_inductive ind in 
-  (mib.mind_ntypes = 1) &&
-  (Array.length mip.mind_consnames = 1) && 
-  match extract_constructor (ind,1) with 
-    | Cml ([mlt],_,_)-> not (type_mem_sp (fst ind) mlt)
-    | _ -> false
-	  
-and is_singleton_constructor ((sp,i),_) = 
-  is_singleton_inductive (sp,i) 
-
 and signature_of_constructor cp = match extract_constructor cp with
   | Cprop -> assert false
   | Cml (_,s,n) -> (s,n)
@@ -859,39 +826,27 @@ and extract_mib sp =
 
 and extract_inductive_declaration sp =
   extract_mib sp;
-  let ip = (sp,0) in 
-  if is_singleton_inductive ip then
-    let t = match lookup_constructor_extraction (ip,1) with 
-      | Cml ([t],_,_)-> t
-      | _ -> assert false
-    in
-    let vl = match lookup_inductive_extraction ip with 
-      | Iml (_,vl) -> vl
-      | _ -> assert false
-    in 
-    Dabbrev (IndRef ip,vl,t)
-  else
-    let mib = Global.lookup_mind sp in
-    let one_ind ip n = 
-	iterate_for (-n) (-1)
-	   (fun j l -> 
-	      let cp = (ip,-j) in 
-	      match lookup_constructor_extraction cp with 
-		| Cprop -> assert false
-		| Cml (t,_,_) -> (ConstructRef cp, t)::l) []
-    in
-    let l = 
-      iterate_for (1 - mib.mind_ntypes) 0
-	(fun i acc -> 
-	   let ip = (sp,-i) in
-	   let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
-	   match lookup_inductive_extraction ip with
-	     | Iprop -> acc
-	     | Iml (_,vl) -> 
-		 (List.rev vl, IndRef ip, one_ind ip nc) :: acc)
-	[] 
-    in
-    Dtype (l, not mib.mind_finite)
+  let mib = Global.lookup_mind sp in
+  let one_ind ip n = 
+    iterate_for (-n) (-1)
+      (fun j l -> 
+	 let cp = (ip,-j) in 
+	 match lookup_constructor_extraction cp with 
+	   | Cprop -> assert false
+	   | Cml (t,_,_) -> (ConstructRef cp, t)::l) []
+  in
+  let l = 
+    iterate_for (1 - mib.mind_ntypes) 0
+      (fun i acc -> 
+	 let ip = (sp,-i) in
+	 let nc = Array.length mib.mind_packets.(-i).mind_consnames in 
+	 match lookup_inductive_extraction ip with
+	   | Iprop -> acc
+	   | Iml (_,vl) -> 
+	       (List.rev vl, IndRef ip, one_ind ip nc) :: acc)
+      [] 
+  in
+  Dtype (l, not mib.mind_finite)
 
 (*s Extraction of a global reference i.e. a constant or an inductive. *)
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 6b331ac2e..48d8a6e7b 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -43,21 +43,24 @@ let rec update_args sp vl = function
       Tarr (update_args sp vl a, update_args sp vl b)
   | a -> a
 
-(*s Does one particular section path occur in a type ? *)
-
-let sp_of_r r = match r with 
-    | ConstRef sp -> sp
-    | IndRef (sp,_) -> sp
-    | ConstructRef ((sp,_),_) -> sp
-    | _ -> assert false
-
-let type_mem_sp sp t= 
-  let rec mem_sp = function 
-    | Tglob r when (sp_of_r r)=sp -> raise Found
-    | Tapp l -> List.iter mem_sp l
-    | Tarr (a,b) -> mem_sp a; mem_sp b
-    | _ -> ()
-  in try mem_sp t; false with Found -> true
+(*s Informative singleton optimization *)
+
+(* We simplify informative singleton inductive, i.e. an inductive with one 
+   constructor which has one informative argument. *) 
+
+let rec type_mem r0 = function 
+    | Tglob r when r=r0 -> true
+    | Tapp l -> List.exists (type_mem r0) l
+    | Tarr (a,b) -> (type_mem r0 a) || (type_mem r0 b)
+    | _ -> false
+
+let singletons = ref Refset.empty
+
+let is_singleton r = Refset.mem r !singletons 
+
+let add_singleton r = singletons:= Refset.add r !singletons
+
+let clear_singletons () = singletons:= Refset.empty
 
 (*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns
     the list [idn;...;id1] and the term [t]. *)
@@ -302,8 +305,11 @@ let rec simplify o = function
       simplify o f
   | MLapp (f, a) -> 
       simplify_app o (List.map (simplify o) a) (simplify o f)
+  | MLcons (r,[t]) when is_singleton r -> simplify o t (* Informative singleton *) 
   | MLcase (e,[||]) ->
       MLexn "Empty inductive"
+  | MLcase (e,[|r,[i],c|]) when is_singleton r -> (* Informative singleton *)
+      simplify o (MLletin (i,e,c))
   | MLcase (e,br) ->
       simplify_case o br (simplify o e) 
   | MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) -> 
@@ -389,11 +395,12 @@ let optimize_fix a =
 	     let new_c = named_lams (ml_subst new_f c) ids
 	     in MLfix(0,[|f|],[|new_c|])
 	 | MLapp(a',args) ->
+	     let m = List.length args in 
 	     (match a' with 
-		| MLfix(_,[|_|],[|_|]) when (test_eta_args_lift 0 n args)-> a'
+		| MLfix(_,[|_|],[|_|]) when 
+		    (test_eta_args_lift 0 n args) && not (occurs_itvl 1 m a') -> a'
 		| MLfix(_,[|f|],[|c|]) -> 
-		    let m = List.length args
-		    and v = Array.make n 0 in 
+		    let v = Array.make n 0 in 
 		    for i=0 to (n-1) do v.(i)<-i done;
 		    let aux i = function 
 			MLrel j when v.(j-1)>=0 -> v.(j-1)<-(-i-1)
@@ -594,7 +601,7 @@ let rec optimize prm = function
       let b = expand (strict_language prm.lang) r t in
       let l = if b then 
 	begin
-	  if prm.toplevel then if_verbose warning_expansion r;
+	  if not (prm.toplevel) then if_verbose warning_expansion r;
 	  List.map (subst_glob_decl r t) l
 	end
       else l in 
@@ -603,6 +610,10 @@ let rec optimize prm = function
 	Dglob (r,t) :: (optimize prm l)
       else
 	optimize prm l
+  | Dtype ([ids,r,[r0,[t0]]],false) :: l when not (type_mem r t0) ->
+      (* Detection of informative singleton. *)
+      add_singleton r0; 
+      Dabbrev (r, ids, t0) :: (optimize prm l)
   | (Dtype _ | Dabbrev _ | Dcustom _) as d :: l -> 
       d :: (optimize prm l)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 7d5373a91..6ce52c055 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -33,9 +33,7 @@ val anonym_lams : ml_ast -> int -> ml_ast
 
 val update_args : section_path -> ml_type list -> ml_type -> ml_type
 
-val sp_of_r : global_reference -> section_path
-
-val type_mem_sp : section_path -> ml_type -> bool
+val clear_singletons : unit -> unit
 
 (*s Utility functions over ML terms. [occurs n t] checks whether [Rel
     n] occurs (freely) in [t]. [ml_lift] is de Bruijn