diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 52 |
1 files changed, 18 insertions, 34 deletions
diff --git a/library/lib.ml b/library/lib.ml index 543cb45b..8ebe4489 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -26,13 +26,11 @@ 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 -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 @@ -51,7 +49,7 @@ let subst_objects subst seg = if obj' == obj then node else (id, obj') in - List.smartmap subst_one seg + List.Smart.map subst_one seg (*let load_and_subst_objects i prefix subst seg = List.rev (List.fold_left (fun seg (id,obj as node) -> @@ -73,10 +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 - (* 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" @@ -183,22 +177,11 @@ let split_lib_gen test = | before -> after,equal,before in let rec findeq after = function - | hd :: before -> - if test hd - then Some (collect after [hd] before) - else (match hd with - | (sp,ClosedModule seg) - | (sp,ClosedSection seg) -> - (match findeq after seg with - | None -> findeq (hd::after) before - | Some (sub_after,sub_equal,sub_before) -> - Some (sub_after, sub_equal, (List.append sub_before before))) - | _ -> findeq (hd::after) before) - | [] -> None + | hd :: before when test hd -> collect after [hd] before + | hd :: before -> findeq (hd::after) before + | [] -> user_err Pp.(str "no such entry") in - match findeq [] !lib_state.lib_stk with - | None -> user_err Pp.(str "no such entry") - | Some r -> r + findeq [] !lib_state.lib_stk let eq_object_name (fp1, kn1) (fp2, kn2) = eq_full_path fp1 fp2 && Names.KerName.equal kn1 kn2 @@ -318,7 +301,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) @@ -416,7 +398,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = { @@ -566,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 _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -580,13 +561,10 @@ let close_section () = in let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; - let full_olddir = !lib_state.path_prefix.obj_dir in 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; - Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) + List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls (* State and initialization. *) @@ -602,10 +580,8 @@ 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 [])) + Some(n,OpenedSection(op,Summary.empty_frozen))) !lib_state.lib_stk in { !lib_state with lib_stk } | _ -> @@ -669,6 +645,14 @@ let discharge_kn kn = let discharge_con cst = if con_defined_in_sec cst then Globnames.pop_con cst else cst +let discharge_proj_repr = + Projection.Repr.map_npars (fun mind npars -> + if not (defined_in_sec mind) then mind, npars + else + let modlist = replacement_context () in + let _, newpars = Mindmap.find mind (snd modlist) in + Globnames.pop_kn mind, npars + Array.length newpars) + let discharge_inductive (kn,i) = (discharge_kn kn,i) |