diff options
-rw-r--r-- | plugins/extraction/extract_env.ml | 15 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 1 |
3 files changed, 18 insertions, 4 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 126305566..bc9047c0a 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -339,10 +339,17 @@ and extract_seb env mp all = function | SEBwith (_,_) -> anomaly "Not available yet" and extract_module env mp all mb = - (* [mb.mod_expr <> None ], since we look at modules from outside. *) - (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) - { ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr); - ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) } + (* A module has an empty [mod_expr] when : + - it is a module variable (for instance X inside a Module F [X:SIG]) + - it is a module assumption (Declare Module). + Since we look at modules from outside, we shouldn't have variables. + But a Declare Module at toplevel seems legal (cf #2525). For the + moment we don't support this situation. *) + match mb.mod_expr with + | None -> error_no_module_expr mp + | Some me -> + { ml_mod_expr = extract_seb env mp all me; + ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) } let unpack = function MEstruct (_,sel) -> sel | _ -> assert false diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 4e08079a3..3dbfa7c02 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -329,6 +329,12 @@ let error_module_clash mp1 mp2 = pr_long_mp mp2 ++ str " have the same ML name.\n" ++ str "This is not supported yet. Please do some renaming first.") +let error_no_module_expr mp = + err (str "The module " ++ pr_long_mp mp + ++ str " has no body, it probably comes from\n" + ++ str "some Declare Module outside any Module Type.\n" + ++ str "This situation is currently unsupported by the extraction.") + let error_unknown_module m = err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index dc07349ca..ce57a7840 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -28,6 +28,7 @@ val error_constant : global_reference -> 'a val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : module_path -> module_path -> 'a +val error_no_module_expr : module_path -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a |