diff options
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/extraction/common.ml | 25 | ||||
-rw-r--r-- | contrib/extraction/common.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 5 | ||||
-rw-r--r-- | contrib/extraction/haskell.ml | 2 | ||||
-rw-r--r-- | contrib/extraction/mlutil.ml | 16 | ||||
-rw-r--r-- | contrib/extraction/test/custom/all | 1 |
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. |