qq inline manuels (sigS_rec ...) + utilisation de library_part

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

6 files changed, 24 insertions, 27 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index e56e151c8..1274d0cf2 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -17,6 +17,7 @@ open Mlutil
 open Ocaml
 open Nametab
 open Util
+open Declare
 
 (*s Modules considerations *)
 
@@ -34,24 +35,6 @@ let qualid_of_dirpath d =
   let dir,id = split_dirpath d in 
   make_qualid dir id 
 
-(* [long_module r] computes the dirpath of the module of the global 
-   reference [r]. The difficulty comes from the possible section names 
-   at the beginning of the dirpath (due to Remark). *)
-
-let long_module r = 
-  let rec check_module d = 
-    try 
-      locate_loaded_library (qualid_of_dirpath d)
-    with Not_found -> 
-      let d' = 
-	try 
-	  dirpath_prefix d 
-	with _ -> errorlabstrm "long_module_message"
-	(str "Can't find the module of" ++ spc () ++ 
-	   Printer.pr_global r)
-      in check_module d' 
-  in check_module (dirpath (sp_of_r r))
-
 (* From a valid module dirpath [d], we check if [r] belongs to this module. *)
       
 let is_long_module d r = 
@@ -62,8 +45,12 @@ let is_long_module d r =
   if l' < l then false 
   else dir = snd (list_chop (l'-l) dir')
 
+(* NB: [library_part r] computes the dirpath of the module of the global 
+   reference [r]. The difficulty comes from the possible section names 
+   at the beginning of the dirpath (due to Remark). *)
+
 let short_module r = 
-  snd (split_dirpath (long_module r))
+  snd (split_dirpath (library_part r))
 
 let module_option r = 
   let m = short_module r in
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index e196fd852..98d91cd71 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -17,8 +17,6 @@ module ToplevelPp : Mlpp
 
 val sp_of_r : global_reference -> section_path
 
-val long_module : global_reference -> dir_path
-
 val is_long_module : dir_path -> global_reference -> bool
 
 val short_module : global_reference -> identifier
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 6f987696b..7d712ce85 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -21,6 +21,7 @@ open Mlutil
 open Nametab
 open Vernacinterp
 open Common
+open Declare
 
 (*s Auxiliary functions dealing with modules. *)
 
@@ -46,7 +47,7 @@ let clash_error sn n1 n2 =
 let check_r m sm r = 
   let rm = String.capitalize (string_of_id (short_module r)) in 
   if rm = sm && not (is_long_module m r) 
-  then clash_error sm m (long_module r)
+  then clash_error sm m (library_part r)
 
 let check_decl m sm = function 
   | Dglob (r,_) -> check_r m sm r 
@@ -122,7 +123,7 @@ let rec visit_reference m eenv r =
        and in module extraction *)
     eenv.visited <- Refset.add r' eenv.visited;
     if m then begin 
-      let m_name = long_module r' in 
+      let m_name = library_part r' in 
       if not (Dirset.mem m_name eenv.modules) then begin
 	eenv.modules <- Dirset.add m_name eenv.modules;
 	List.iter (visit_reference m eenv) (extract_module m_name)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 04f201edd..cb3dd32e3 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -39,7 +39,7 @@ let preamble prm =
   (str "module " ++ str m ++ str " where" ++ fnl () ++ fnl () ++
      str "type Prop = Unit.Unit" ++ fnl () ++
      str "prop = Unit.unit" ++ fnl () ++ fnl () ++
-     str "type Arity = Unit.Unit" ++ fnl () ++
+     str "data Arity = Unit.Unit" ++ fnl () ++
      str "arity = Unit.unit" ++ fnl () ++ fnl ())
 
 let pp_abst = function
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 9cbbf15f6..dd21564ce 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -17,6 +17,7 @@ open Miniml
 open Nametab
 open Table
 open Options
+open Nameops
 
 (*s Exceptions. *)
 
@@ -710,6 +711,16 @@ let expansion_test t =
    (ml_size t < 3) ||
    ((ml_size t < 12) && (is_not_strict t)))
 
+let manual_expand_list = 
+  List.map (fun s -> path_of_string ("Coq.Init."^s))
+    [ "Specif.sigS_rect" ; "Specif.sigS_rec" ; 
+      "Datatypes.prod_rect" ; "Datatypes.prod_rec"; 
+      "Wf.Acc_rec" ; "Wf.well_founded_induction" ]
+
+let manual_expand = function 
+  | ConstRef sp -> List.mem sp manual_expand_list
+  | _ -> false 
+
 (* If the user doesn't say he wants to keep [t], we expand in two cases:
    \begin{itemize}
    \item the user explicitly requests it 
@@ -721,8 +732,9 @@ let expand strict_lang r t =
   (not (to_keep r)) (* The user DOES want to keep it *)
   &&
   ((to_inline r) (* The user DOES want to expand it *) 
-   || 
-   (auto_inline () && strict_lang && expansion_test t)) 
+  || 
+   (auto_inline () && strict_lang && 
+    ((manual_expand r) ||  expansion_test t)))
 
 (*s Optimization *)
 
diff --git a/contrib/extraction/test/custom/all b/contrib/extraction/test/custom/all
index 14bb482ca..e69de29bb 100644
--- a/contrib/extraction/test/custom/all
+++ b/contrib/extraction/test/custom/all
@@ -1 +0,0 @@
-Extraction Inline sigS_rec sigS_rect prod_rec prod_rect.