aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-15 16:46:18 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-15 16:46:18 +0000
commitca04c9042de024eb559e7841dfce1cf67056a145 (patch)
tree0d5f2070cfc0f20ed03bcf3d8a50bda1e8ac8499 /plugins/extraction
parent18214ca9f822ed39bb5ecf48f27f119508b97d28 (diff)
Extraction: nicer error when a toplevel module has no body (#2525)
I thought this situation wasn't possible, hence the Option.get. But it's apparently legal to use Declare Module anywhere, even outside a Module Type. No idea on how to handle that at extraction for the moment, hence a proper "unsupported" error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14013 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/extract_env.ml15
-rw-r--r--plugins/extraction/table.ml6
-rw-r--r--plugins/extraction/table.mli1
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