diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 1 | ||||
| -rw-r--r-- | library/global.mli | 5 | ||||
| -rw-r--r-- | library/lib.ml | 147 | ||||
| -rw-r--r-- | library/lib.mli | 6 |
4 files changed, 26 insertions, 133 deletions
diff --git a/library/global.ml b/library/global.ml index e51c147f6e..3d28178d7b 100644 --- a/library/global.ml +++ b/library/global.ml @@ -83,6 +83,7 @@ let i2l = Label.of_id let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let push_section_context c = globalize0 (Safe_typing.push_section_context c) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) diff --git a/library/global.mli b/library/global.mli index 9ac6b1f53c..b809e9b241 100644 --- a/library/global.mli +++ b/library/global.mli @@ -44,6 +44,7 @@ val sprop_allowed : unit -> bool val push_named_assum : (Id.t * Constr.types) -> unit val push_named_def : (Id.t * Entries.section_def_entry) -> unit +val push_section_context : (Name.t array * Univ.UContext.t) -> unit val export_private_constants : in_section:bool -> Safe_typing.private_constants Entries.proof_output -> @@ -74,7 +75,11 @@ val add_include : (** Sections *) val open_section : poly:bool -> unit +(** [poly] is true when the section should be universe polymorphic *) + val close_section : Summary.frozen -> unit +(** Close the section and reset the global state to the one at the time when + the section what opened. *) (** Interactive modules and module types *) diff --git a/library/lib.ml b/library/lib.ml index 367a84409b..1c6f82e8a6 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -410,87 +410,11 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type abstr_info = { +type abstr_info = Section.abstr_info = private { abstr_ctx : Constr.named_context; abstr_subst : Univ.Instance.t; abstr_uctx : Univ.AUContext.t; } -type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t - -type secentry = - | Variable of { - id:Names.Id.t; - } - | Context of Name.t array * Univ.UContext.t - -type section_data = { - sec_entry : secentry list; - sec_abstr : abstr_list; - sec_poly : bool; -} - -let empty_section_data ~poly = { - sec_entry = []; - sec_abstr = (Names.Cmap.empty,Names.Mindmap.empty); - sec_poly = poly; -} - -let sectab = - Summary.ref ([] : section_data list) ~name:"section-context" - -let check_same_poly p sec = - if p != sec.sec_poly then - user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") - -let add_section ~poly () = - List.iter (fun tab -> check_same_poly poly tab) !sectab; - sectab := empty_section_data ~poly :: !sectab - -let add_section_variable ~name ~poly = - match !sectab with - | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | s :: sl -> - List.iter (fun tab -> check_same_poly poly tab) !sectab; - let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in - sectab := s :: sl - -let add_section_context (nas, ctx) = - match !sectab with - | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | s :: sl -> - check_same_poly true s; - let s = { s with sec_entry = Context (nas, ctx) :: s.sec_entry } in - sectab := s :: sl - -exception PolyFound (* make this a let exception once possible *) -let is_polymorphic_univ u = - try - let open Univ in - List.iter (fun s -> - let vars = s.sec_entry in - List.iter (function - | Variable _ -> () - | Context (_, univs) -> - if Array.mem u (Instance.to_array (UContext.instance univs)) then raise PolyFound - ) vars - ) !sectab; - false - with PolyFound -> true - -let extract_hyps poly (secs,ohyps) = - let rec aux = function - | (Variable {id}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) -> - let l, r = aux (idl,hyps) in - decl :: l, r - | (Variable _::idl,hyps) -> - let l, r = aux (idl,hyps) in - l, r - | (Context (nas, ctx) :: idl, hyps) -> - let () = assert poly in - let l, (snas, sctx) = aux (idl, hyps) in - l, (Array.append snas nas, Univ.UContext.union sctx ctx) - | [], _ -> [], ([||], Univ.UContext.empty) - in aux (secs,ohyps) let instance_from_variable_context = List.rev %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list @@ -499,47 +423,21 @@ let extract_worklist info = let args = instance_from_variable_context info.abstr_ctx in info.abstr_subst, args -let make_worklist (cmap, mmap) = - Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap - -let add_section_replacement g poly hyps = - match !sectab with - | [] -> () - | s :: sl -> - let () = check_same_poly poly s in - let sechyps, (nas, ctx) = extract_hyps s.sec_poly (s.sec_entry, hyps) in - let subst, ctx = Univ.abstract_universes nas ctx in - let info = { - abstr_ctx = sechyps; - abstr_subst = subst; - abstr_uctx = ctx; - } in - let s = { s with - sec_abstr = g info s.sec_abstr; - } in - sectab := s :: sl - -let add_section_kn ~poly kn = - let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in - add_section_replacement f poly - -let add_section_constant ~poly kn = - let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f poly - -let replacement_context () = make_worklist (List.hd !sectab).sec_abstr +let sections () = Safe_typing.sections_of_safe_env @@ Global.safe_env () + +let is_polymorphic_univ u = + Section.is_polymorphic_univ u (sections ()) + +let replacement_context () = + Section.replacement_context (Global.env ()) (sections ()) let section_segment_of_constant con = - Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) + Section.segment_of_constant (Global.env ()) con (sections ()) let section_segment_of_mutual_inductive kn = - Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) + Section.segment_of_inductive (Global.env ()) kn (sections ()) -let empty_segment = { - abstr_ctx = []; - abstr_subst = Univ.Instance.empty; - abstr_uctx = Univ.AUContext.empty; -} +let empty_segment = Section.empty_segment let section_segment_of_reference = let open GlobRef in function | ConstRef c -> section_segment_of_constant c @@ -550,25 +448,20 @@ let section_segment_of_reference = let open GlobRef in function let variable_section_segment_of_reference gr = (section_segment_of_reference gr).abstr_ctx +let is_in_section ref = + Section.is_in_section (Global.env ()) ref (sections ()) + let section_instance = let open GlobRef in function | VarRef id -> - let eq = function - | Variable {id=id'} -> Names.Id.equal id id' - | Context _ -> false - in - if List.exists eq (List.hd !sectab).sec_entry - then Univ.Instance.empty, [||] - else raise Not_found + if is_in_section (VarRef id) then (Univ.Instance.empty, [||]) + else raise Not_found | ConstRef con -> - let data = Names.Cmap.find con (fst (List.hd !sectab).sec_abstr) in + let data = section_segment_of_constant con in extract_worklist data | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - let data = Names.Mindmap.find kn (snd (List.hd !sectab).sec_abstr) in + let data = section_segment_of_mutual_inductive kn in extract_worklist data -let is_in_section ref = - try ignore (section_instance ref); true with Not_found -> false - (*************) (* Sections. *) let open_section ~poly id = @@ -582,9 +475,7 @@ let open_section ~poly id = add_entry (make_foname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirOpenSection prefix)); - lib_state := { !lib_state with path_prefix = prefix }; - add_section ~poly () - + lib_state := { !lib_state with path_prefix = prefix } (* Restore lib_stk and summaries as before the section opening, and add a ClosedSection object. *) diff --git a/library/lib.mli b/library/lib.mli index db6df4395b..5ce601f2d3 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -163,7 +163,7 @@ val drop_objects : frozen -> frozen val init : unit -> unit (** {6 Section management for discharge } *) -type abstr_info = private { +type abstr_info = Section.abstr_info = private { abstr_ctx : Constr.named_context; (** Section variables of this prefix *) abstr_subst : Univ.Instance.t; @@ -181,10 +181,6 @@ val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : name:Id.t -> poly:bool -> unit -val add_section_context : Name.t array * Univ.UContext.t -> unit -val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit -val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list val is_polymorphic_univ : Univ.Level.t -> bool |