From 6a9d0dc7b5c9a6a1c10c0c94eba5e72543080399 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 19 Jul 2018 23:49:54 +0200
Subject: Remove ClosedModule from libstack

Seems unused and probably holds a lot of pointers.
---
 library/lib.ml | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index a20de55bf6..5e9d2baa1d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -26,7 +26,6 @@ type node =
   | Leaf of obj
   | CompilingLibrary of object_prefix
   | OpenedModule of is_type * export * object_prefix * Summary.frozen
-  | ClosedModule  of library_segment
   | OpenedSection of object_prefix * Summary.frozen
   | ClosedSection of library_segment
 
@@ -74,9 +73,6 @@ let classify_segment seg =
 	     | Anticipate o' ->
 		 clean (substl, keepl, o'::anticipl) stk)
     | (_,ClosedSection _) :: stk -> clean acc stk
-    (* LEM; TODO: Understand what this does and see if what I do is the
-                  correct thing for ClosedMod(ule|type) *)
-    | (_,ClosedModule _) :: stk -> clean acc stk
     | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
       user_err ~hdr:"Lib.classify_segment"
@@ -307,7 +303,6 @@ let end_mod is_type =
   in
   let (after,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
-  add_entry oname (ClosedModule (List.rev (mark::after)));
   let prefix = !lib_state.path_prefix in
   recalc_path_prefix ();
   (oname, prefix, fs, after)
@@ -555,7 +550,7 @@ let discharge_item ((sp,_ as oname),e) =
   match e with
   | Leaf lobj ->
       Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
-  | ClosedSection _ | ClosedModule _ -> None
+  | ClosedSection _ -> None
   | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
       anomaly (Pp.str "discharge_item.")
 
@@ -589,7 +584,6 @@ let freeze ~marshallable =
         | n, (CompilingLibrary _ as x) -> Some (n,x)
         | n, OpenedModule (it,e,op,_) ->
                Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
-        | n, ClosedModule _ -> Some (n,ClosedModule [])
         | n, OpenedSection (op, _) ->
                Some(n,OpenedSection(op,Summary.empty_frozen))
         | n, ClosedSection _ -> Some (n,ClosedSection []))
-- 
cgit v1.2.3


From 32caa7b700cb2f561edec9b86fbb4583d2962d4d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 19 Jul 2018 23:58:52 +0200
Subject: Also remove ClosedSection (same reasoning as ClosedModule)

---
 library/lib.ml | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index 5e9d2baa1d..4aee82079d 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -27,11 +27,10 @@ type node =
   | CompilingLibrary of object_prefix
   | OpenedModule of is_type * export * object_prefix * Summary.frozen
   | OpenedSection of object_prefix * Summary.frozen
-  | ClosedSection of library_segment
 
-and library_entry = object_name * node
+type library_entry = object_name * node
 
-and library_segment = library_entry list
+type library_segment = library_entry list
 
 type lib_objects =  (Names.Id.t * obj) list
 
@@ -72,7 +71,6 @@ let classify_segment seg =
 		 clean ((id,o')::substl, keepl, anticipl) stk
 	     | Anticipate o' ->
 		 clean (substl, keepl, o'::anticipl) stk)
-    | (_,ClosedSection _) :: stk -> clean acc stk
     | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections")
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
       user_err ~hdr:"Lib.classify_segment"
@@ -550,7 +548,6 @@ let discharge_item ((sp,_ as oname),e) =
   match e with
   | Leaf lobj ->
       Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
-  | ClosedSection _ -> None
   | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
       anomaly (Pp.str "discharge_item.")
 
@@ -565,7 +562,6 @@ let close_section () =
   let (secdecls,mark,before) = split_lib_at_opening oname in
   lib_state := { !lib_state with lib_stk = before };
   pop_path_prefix ();
-  add_entry oname (ClosedSection (List.rev (mark::secdecls)));
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls
@@ -585,8 +581,7 @@ let freeze ~marshallable =
         | n, OpenedModule (it,e,op,_) ->
                Some(n,OpenedModule(it,e,op,Summary.empty_frozen))
         | n, OpenedSection (op, _) ->
-               Some(n,OpenedSection(op,Summary.empty_frozen))
-        | n, ClosedSection _ -> Some (n,ClosedSection []))
+               Some(n,OpenedSection(op,Summary.empty_frozen)))
       !lib_state.lib_stk in
     { !lib_state with lib_stk }
   | _ ->
-- 
cgit v1.2.3