diff options
| -rw-r--r-- | plugins/extraction/common.ml | 13 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/modutil.ml | 5 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 58 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 2 |
5 files changed, 38 insertions, 42 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index c329afdbe..83160896e 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -452,11 +452,11 @@ let fstlev_ks k = function let pp_ocaml_local k prefix mp rls olab = (* what is the largest prefix of [mp] that belongs to [visible]? *) assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *) - let rls = list_skipn (mp_length prefix) rls in - let k's = fstlev_ks k rls in + let rls' = list_skipn (mp_length prefix) rls in + let k's = fstlev_ks k rls' in (* Reference r / module path mp is of the form [<prefix>.s.<...>]. *) - if not (visible_clash prefix k's) then dottify rls - else pp_duplicate (fst k's) prefix mp rls olab + if not (visible_clash prefix k's) then dottify rls' + else pp_duplicate (fst k's) prefix mp rls' olab (* [pp_ocaml_bound] : [mp] starts with a [MPbound], and we are not inside (i.e. we are not printing the type of the module parameter) *) @@ -506,8 +506,7 @@ let pp_global k r = let ls = ref_renaming (k,r) in assert (List.length ls > 1); let s = List.hd ls in - let l = label_of_r r in - let mp = modpath_of_r r in + let mp,_,l = repr_of_r r in if mp = top_visible_mp () then (* simpliest situation: definition of r (or use in the same context) *) (* we update the visible environment *) @@ -517,7 +516,7 @@ let pp_global k r = match lang () with | Scheme -> unquote s (* no modular Scheme extraction... *) | Haskell -> if modular () then pp_haskell_gen k mp rls else s - | Ocaml -> pp_ocaml_gen k mp rls (Some (label_of_r r)) + | Ocaml -> pp_ocaml_gen k mp rls (Some l) (* The next function is used only in Ocaml extraction...*) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index db7504e3e..dd0547737 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -335,7 +335,7 @@ let mono_environment refs mpl = let env = Global.env () in let l = List.rev (environment_until None) in List.rev_map - (fun (mp,m) -> mp, unpack (extract_seb env mp false m)) l + (fun (mp,m) -> mp, unpack (extract_seb env mp false m)) l (**************************************) (*S Part II : Input/Output primitives *) diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 4ed6e9a08..8bc98e452 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -185,7 +185,7 @@ let signature_of_structure s = (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *) let get_decl_in_structure r struc = - try + try let base_mp,ll = labels_of_ref r in if not (at_toplevel base_mp) then error_not_visible r; let sel = List.assoc base_mp struc in @@ -200,7 +200,8 @@ let get_decl_in_structure r struc = | MEstruct (_,sel) -> go ll sel | _ -> error_not_visible r in go ll sel - with Not_found -> assert false + with Not_found -> + anomaly "reference not found in extracted structure" (*s Optimization of a [ml_structure]. *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 83f33047e..f19b60103 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -27,26 +27,22 @@ let occur_kn_in_ref kn = function | ConstRef _ -> false | VarRef _ -> assert false -let modpath_of_r = function - | ConstRef kn -> con_modpath kn +let repr_of_r = function + | ConstRef kn -> repr_con kn | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> mind_modpath kn + | ConstructRef ((kn,_),_) -> repr_mind kn | VarRef _ -> assert false -let label_of_r = function - | ConstRef kn -> con_label kn - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> mind_label kn - | VarRef _ -> assert false +let modpath_of_r r = + let mp,_,_ = repr_of_r r in mp + +let label_of_r r = + let _,_,l = repr_of_r r in l let rec base_mp = function | MPdot (mp,l) -> base_mp mp | mp -> mp -let rec mp_length = function - | MPdot (mp, _) -> 1 + (mp_length mp) - | _ -> 1 - let is_modfile = function | MPfile _ -> true | _ -> false @@ -68,7 +64,14 @@ let is_toplevel mp = let at_toplevel mp = is_modfile mp || is_toplevel mp -let visible_kn kn = at_toplevel (base_mp (modpath kn)) +let rec mp_length mp = + let mp0 = current_toplevel () in + let rec len = function + | mp when mp = mp0 -> 1 + | MPdot (mp,_) -> 1 + len mp + | _ -> 1 + in len mp + let visible_con kn = at_toplevel (base_mp (con_modpath kn)) let rec prefixes_mp mp = match mp with @@ -94,18 +97,12 @@ let labels_of_mp mp = parse_labels [] mp let rec parse_labels2 ll mp1 = function | mp when mp1=mp -> mp,ll - | MPdot (mp,l) -> parse_labels (l::ll) mp + | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp | mp -> mp,ll let labels_of_ref r = - let mp_top = fst(Lib.current_prefix()) in - let mp,_,l = - match r with - ConstRef con -> repr_con con - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> repr_mind kn - | VarRef _ -> assert false - in + let mp_top = current_toplevel () in + let mp,_,l = repr_of_r r in parse_labels2 [l] mp_top mp let rec add_labels_mp mp = function @@ -300,7 +297,7 @@ let error_scheme () = let error_not_visible r = err (safe_pr_global r ++ str " is not directly visible.\n" ++ - str "For example, it may be inside an applied functor." ++ + str "For example, it may be inside an applied functor.\n" ++ str "Use Recursive Extraction to get the whole environment.") let error_MPfile_as_mod mp b = @@ -327,14 +324,13 @@ let error_non_implicit msg = fnl () ++ str "Please check the Extraction Implicit declarations.") let check_loaded_modfile mp = match base_mp mp with - | MPfile dp -> if not (Library.library_is_loaded dp) then - let mp1 = (fst(Lib.current_prefix())) in - let rec find_prefix = function - |MPfile dp1 when dp=dp1 -> () - |MPdot(mp,_) -> find_prefix mp - |MPbound(_) -> () - | _ -> err (str ("Please load library "^(string_of_dirpath dp^" first."))) - in find_prefix mp1 + | MPfile dp -> + if not (Library.library_is_loaded dp) then begin + match base_mp (current_toplevel ()) with + | MPfile dp' when dp<>dp' -> + err (str ("Please load library "^(string_of_dirpath dp^" first."))) + | _ -> () + end | _ -> () let info_file f = diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 18904a8b4..590ee0643 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -40,6 +40,7 @@ val info_file : string -> unit (*s utilities about [module_path] and [kernel_names] and [global_reference] *) val occur_kn_in_ref : mutual_inductive -> global_reference -> bool +val repr_of_r : global_reference -> module_path * dir_path * label val modpath_of_r : global_reference -> module_path val label_of_r : global_reference -> label val current_toplevel : unit -> module_path @@ -49,7 +50,6 @@ val string_of_modfile : module_path -> string val file_of_modfile : module_path -> string val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool -val visible_kn : kernel_name -> bool val visible_con : constant -> bool val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t |