Reify libobject containers

We make a few libobject constructions (Module, Module Type,
Include,...) first-class and rephrase their handling in direct style (removing
the inversion of control). This makes it easier to define iterators over
objects without hacks like inspecting the tags of dynamic objects.

1 files changed, 21 insertions, 18 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 31dcfdd168..69e5c4231f 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -29,24 +29,27 @@ open Common
 
 let toplevel_env () =
   let get_reference = function
-    | (_,kn), Lib.Leaf o ->
-        let mp,l = KerName.repr kn in
-	begin match Libobject.object_tag o with
-	  | "CONSTANT" ->
-            let constant = Global.lookup_constant (Constant.make1 kn) in
-            Some (l, SFBconst constant)
-	  | "INDUCTIVE" ->
-            let inductive = Global.lookup_mind (MutInd.make1 kn) in
-            Some (l, SFBmind inductive)
-	  | "MODULE" ->
-            let modl = Global.lookup_module (MPdot (mp, l)) in
-            Some (l, SFBmodule modl)
-	  | "MODULE TYPE" ->
-            let modtype = Global.lookup_modtype (MPdot (mp, l)) in
-            Some (l, SFBmodtype modtype)
-          | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.")
-	  | _ -> None
-        end
+    | (_,kn), Lib.Leaf Libobject.AtomicObject o ->
+      let mp,l = KerName.repr kn in
+            begin match Libobject.object_tag o with
+            | "CONSTANT" ->
+        let constant = Global.lookup_constant (Constant.make1 kn) in
+        Some (l, SFBconst constant)
+            | "INDUCTIVE" ->
+        let inductive = Global.lookup_mind (MutInd.make1 kn) in
+        Some (l, SFBmind inductive)
+            | _ -> None
+      end
+    | (_,kn), Lib.Leaf Libobject.ModuleObject _ ->
+      let mp,l = KerName.repr kn in
+      let modl = Global.lookup_module (MPdot (mp, l)) in
+      Some (l, SFBmodule modl)
+    | (_,kn), Lib.Leaf Libobject.ModuleTypeObject _ ->
+      let mp,l = KerName.repr kn in
+      let modtype = Global.lookup_modtype (MPdot (mp, l)) in
+      Some (l, SFBmodtype modtype)
+    | (_,kn), Lib.Leaf Libobject.IncludeObject _ ->
+      user_err Pp.(str "No extraction of toplevel Include yet.")
     | _ -> None
   in
   List.rev (List.map_filter get_reference (Lib.contents ()))