diff options
| -rw-r--r-- | library/lib.ml | 39 | ||||
| -rw-r--r-- | library/lib.mli | 2 | ||||
| -rw-r--r-- | tactics/declare.ml | 27 |
3 files changed, 35 insertions, 33 deletions
diff --git a/library/lib.ml b/library/lib.ml index 851f086961..1f97424590 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -421,7 +421,7 @@ type secentry = | Variable of { id:Names.Id.t; } - | Context of Univ.ContextSet.t + | Context of Name.t array * Univ.UContext.t type section_data = { sec_entry : secentry list; @@ -454,12 +454,12 @@ let add_section_variable ~name ~poly = let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in sectab := s :: sl -let add_section_context ctx = +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 ctx :: s.sec_entry } in + 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 *) @@ -470,8 +470,8 @@ let is_polymorphic_univ u = let vars = s.sec_entry in List.iter (function | Variable _ -> () - | Context (univs,_) -> - if LSet.mem u univs then raise PolyFound + | Context (_, univs) -> + if Array.mem u (Instance.to_array (UContext.instance univs)) then raise PolyFound ) vars ) !sectab; false @@ -485,11 +485,11 @@ let extract_hyps poly (secs,ohyps) = | (Variable _::idl,hyps) -> let l, r = aux (idl,hyps) in l, r - | (Context ctx :: idl, hyps) -> + | (Context (nas, ctx) :: idl, hyps) -> let () = assert poly in - let l, r = aux (idl, hyps) in - l, Univ.ContextSet.union r ctx - | [], _ -> [],Univ.ContextSet.empty + 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 = @@ -502,31 +502,12 @@ let extract_worklist info = let make_worklist (cmap, mmap) = Cmap.map extract_worklist cmap, Mindmap.map extract_worklist mmap -let name_instance inst = - (* FIXME: this should probably be done at an upper level, by storing the - name information in the section data structure. *) - let map lvl = match Univ.Level.name lvl with - | None -> (* Having Prop/Set/Var as section universes makes no sense *) - assert false - | Some na -> - try - let qid = Nametab.shortest_qualid_of_universe na in - Name (Libnames.qualid_basename qid) - with Not_found -> - (* Best-effort naming from the string representation of the level. - See univNames.ml for a similar hack. *) - Name (Id.of_string_soft (Univ.Level.to_string lvl)) - in - Array.map map (Univ.Instance.to_array inst) - let add_section_replacement g poly hyps = match !sectab with | [] -> () | s :: sl -> let () = check_same_poly poly s in - let sechyps,ctx = extract_hyps s.sec_poly (s.sec_entry, hyps) in - let ctx = Univ.ContextSet.to_context ctx in - let nas = name_instance (Univ.UContext.instance ctx) 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; diff --git a/library/lib.mli b/library/lib.mli index 9ffa69ef93..db6df4395b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -182,7 +182,7 @@ 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 : Univ.ContextSet.t -> 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 diff --git a/tactics/declare.ml b/tactics/declare.ml index 3a02e5451a..2f9da373aa 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -40,9 +40,30 @@ let input_universe_context : Univ.ContextSet.t -> Libobject.obj = ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) ~discharge:(fun (_, x) -> Some x) +let name_instance inst = + let map lvl = match Univ.Level.name lvl with + | None -> (* Having Prop/Set/Var as section universes makes no sense *) + assert false + | Some na -> + try + let qid = Nametab.shortest_qualid_of_universe na in + Name (Libnames.qualid_basename qid) + with Not_found -> + (* Best-effort naming from the string representation of the level. + See univNames.ml for a similar hack. *) + Name (Id.of_string_soft (Univ.Level.to_string lvl)) + in + Array.map map (Univ.Instance.to_array inst) + let declare_universe_context ~poly ctx = if poly then - (Global.push_context_set true ctx; Lib.add_section_context ctx) + (* FIXME: some upper layers declare universes several times, we hack around + by checking whether the universes already exist. *) + let (univs, cstr) = ctx in + let univs = Univ.LSet.filter (fun u -> not (Lib.is_polymorphic_univ u)) univs in + let uctx = Univ.ContextSet.to_context (univs, cstr) in + let nas = name_instance (Univ.UContext.instance uctx) in + (Global.push_context_set true ctx; Lib.add_section_context (nas, uctx)) else Lib.add_anonymous_leaf (input_universe_context ctx) @@ -632,9 +653,9 @@ let do_universe ~poly l = let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) Univ.LSet.empty l, Univ.Constraint.empty in - let () = declare_universe_context ~poly ctx in let src = if poly then BoundUniv else UnqualifiedUniv in - Lib.add_anonymous_leaf (input_univ_names (src, l)) + let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in + declare_universe_context ~poly ctx let do_constraint ~poly l = let open Univ in |