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 +------- library/lib.mli | 1 - printing/prettyp.ml | 2 -- 3 files changed, 1 insertion(+), 10 deletions(-) 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 [])) diff --git a/library/lib.mli b/library/lib.mli index 5abfccfc7d..2915a5fd64 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -23,7 +23,6 @@ type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fd7135b6a6..6911013464 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -663,8 +663,6 @@ let gallina_print_library_entry env sigma with_values ent = Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) - | (oname,Lib.ClosedModule _) -> - Some (str " >>>>>>> Closed Module " ++ pr_name oname) let gallina_print_context env sigma with_values = let rec prec n = function -- 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 +++-------- library/lib.mli | 3 +-- printing/prettyp.ml | 5 ----- 3 files changed, 4 insertions(+), 15 deletions(-) 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 } | _ -> diff --git a/library/lib.mli b/library/lib.mli index 2915a5fd64..eff72ea63f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -24,9 +24,8 @@ type node = | CompilingLibrary of Libnames.object_prefix | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen | OpenedSection of Libnames.object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_segment = (Libnames.object_name * node) list +type library_segment = (Libnames.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 6911013464..170b96280f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -657,8 +657,6 @@ let gallina_print_library_entry env sigma with_values ent = gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> - Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { obj_dir; _ }) -> Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> @@ -791,9 +789,6 @@ let read_sec_context qid = let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest -> if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | (_,Lib.ClosedSection _)::rest -> - user_err Pp.(str "Cannot print the contents of a closed section.") - (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in -- cgit v1.2.3