diff options
| -rw-r--r-- | engine/univNames.ml | 87 | ||||
| -rw-r--r-- | engine/univNames.mli | 11 | ||||
| -rw-r--r-- | engine/universes.ml | 1 | ||||
| -rw-r--r-- | engine/universes.mli | 4 | ||||
| -rw-r--r-- | printing/prettyp.ml | 23 | ||||
| -rw-r--r-- | printing/printmod.ml | 15 |
6 files changed, 53 insertions, 88 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml index 29d92c46ea..a4a08ff18e 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -53,10 +53,10 @@ let empty_binders = Id.Map.empty let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders" -let universe_binders_of_global ref : universe_binders = +let universe_binders_of_global ref : Name.t list = try let l = GlobRef.Map.find ref !universe_binders_table in l - with Not_found -> Names.Id.Map.empty + with Not_found -> [] let cache_ubinder (_,(ref,l)) = universe_binders_table := GlobRef.Map.add ref l !universe_binders_table @@ -68,25 +68,19 @@ let subst_ubinder (subst,(ref,l as orig)) = let discharge_ubinder (_,(ref,l)) = (** Expand polymorphic binders with the section context *) let info = Lib.section_segment_of_reference ref in - let sec_inst = info.Lib.abstr_subst in - let shift = Instance.length sec_inst in - let map lvl = match Level.var_index lvl with - | None -> lvl - | Some n -> Level.var (n + shift) - in - let l = Id.Map.map map l in - let fold i accu lvl = match Level.name lvl with - | None -> accu + let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in + let map i lvl = match Level.name lvl with + | None -> Anonymous | Some na -> try let qid = Nametab.shortest_qualid_of_universe na in - Id.Map.add (snd (Libnames.repr_qualid qid)) (Level.var i) accu - with Not_found -> accu + Name (snd (Libnames.repr_qualid qid)) + with Not_found -> Anonymous in - let l = Array.fold_left_i fold l (Instance.to_array sec_inst) in + let l = List.mapi map sec_inst @ l in Some (Lib.discharge_global ref, l) -let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = +let ubinder_obj : GlobRef.t * Name.t list -> Libobject.obj = let open Libobject in declare_object { (default_object "universe binder") with cache_function = cache_ubinder; @@ -97,42 +91,37 @@ let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = rebuild_function = (fun x -> x); } let register_universe_binders ref ubinders = - (* Add the polymorphic (section) universes *) - let ubinders = UnivIdMap.fold (fun lvl poly ubinders -> - let qid = Nametab.shortest_qualid_of_universe lvl in - let level = Level.make (fst lvl) (snd lvl) in - if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders - else ubinders) - !universe_map ubinders - in - let ubinders = - if Global.is_polymorphic ref then - (** FIXME: little dance to make the named universes refer to bound - universe variables *) - let univs = AUContext.instance (Global.universes_of_global ref) in - let fold i accu l = LMap.add l i accu in - let univs = Array.fold_left_i fold LMap.empty (Instance.to_array univs) in - let fold id lvl accu = - try Id.Map.add id (Level.var (LMap.find lvl univs)) accu - with Not_found -> accu - in - Id.Map.fold fold ubinders Id.Map.empty - else ubinders + (** TODO: change the API to register a [Name.t list] instead. This is the last + part of the code that depends on the internal representation of names in + abstract contexts, but removing it requires quite a rework of the + callers. *) + let univs = AUContext.instance (Global.universes_of_global ref) in + let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in + let map lvl = + try Name (LMap.find lvl revmap) + with Not_found -> Anonymous in - if not (Id.Map.is_empty ubinders) - then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) + let ubinders = Array.map_to_list map (Instance.to_array univs) in + if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders)) type univ_name_list = Names.lname list -let universe_binders_with_opt_names ref levels = function +let universe_binders_with_opt_names ref names = + let udecl = match names with | None -> universe_binders_of_global ref - | Some udecl -> - if Int.equal(List.length levels) (List.length udecl) - then - List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with - | Anonymous -> acc - | Name na -> Names.Id.Map.add na lvl acc) - empty_binders udecl levels - else - CErrors.user_err ~hdr:"universe_binders_with_opt_names" - Pp.(str "Universe instance should have length " ++ int (List.length levels)) + | Some udecl -> List.map (fun na -> na.CAst.v) udecl + in + let () = + try + let ctx = Global.universes_of_global ref in + let len = AUContext.size ctx in + if not (Option.is_empty names || Int.equal len (List.length udecl)) then + CErrors.user_err ~hdr:"universe_binders_with_opt_names" + Pp.(str "Universe instance should have length " ++ int len) + with Not_found -> () + in + let fold i acc = function + | Anonymous -> acc + | Name na -> Names.Id.Map.add na (Level.var i) acc + in + List.fold_left_i fold 0 empty_binders udecl diff --git a/engine/univNames.mli b/engine/univNames.mli index 837beac267..d794d7b744 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -27,15 +27,14 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit -val universe_binders_of_global : Names.GlobRef.t -> universe_binders type univ_name_list = Names.lname list -(** [universe_binders_with_opt_names ref u l] +(** [universe_binders_with_opt_names ref l] - If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous). - May error if the lengths mismatch. + If [l] is [Some univs] return the universe binders naming the bound levels + of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch. - Otherwise return [universe_binders_of_global ref]. *) + Otherwise return the bound universe names registered for [ref]. *) val universe_binders_with_opt_names : Names.GlobRef.t -> - Univ.Level.t list -> univ_name_list option -> universe_binders + univ_name_list option -> universe_binders diff --git a/engine/universes.ml b/engine/universes.ml index ee9668433c..c7e5f654a1 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -26,7 +26,6 @@ let is_polymorphic = UnivNames.is_polymorphic let empty_binders = UnivNames.empty_binders let register_universe_binders = UnivNames.register_universe_binders -let universe_binders_of_global = UnivNames.universe_binders_of_global let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names diff --git a/engine/universes.mli b/engine/universes.mli index ad937471e9..7ca33f47a1 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -39,14 +39,12 @@ val empty_binders : universe_binders val register_universe_binders : Globnames.global_reference -> universe_binders -> unit [@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"] -val universe_binders_of_global : Globnames.global_reference -> universe_binders -[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"] type univ_name_list = UnivNames.univ_name_list [@@ocaml.deprecated "Use [UnivNames.univ_name_list]"] val universe_binders_with_opt_names : Globnames.global_reference -> - Univ.Level.t list -> univ_name_list option -> universe_binders + univ_name_list option -> universe_binders [@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"] (** ****** Deprecated: moved to [UnivGen] *) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 605c1ae957..66f748454d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -73,8 +73,7 @@ let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref udecl = let typ, univs = Global.type_of_global_in_context (Global.env ()) ref in let inst = Univ.make_abstract_instance univs in - let bl = UnivNames.universe_binders_with_opt_names ref - (Array.to_list (Univ.Instance.to_array inst)) udecl in + let bl = UnivNames.universe_binders_with_opt_names ref udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let typ = EConstr.of_constr typ in let typ = @@ -556,33 +555,23 @@ let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in let typ = cb.const_type in - let univs, ulist = + let univs = let open Univ in let otab = Global.opaque_tables () in match cb.const_body with - | Undef _ | Def _ -> - begin - match cb.const_universes with - | Monomorphic_const ctx -> Monomorphic_const ctx, [] - | Polymorphic_const ctx -> - let inst = make_abstract_instance ctx in - Polymorphic_const ctx, - Array.to_list (Instance.to_array inst) - end + | Undef _ | Def _ -> cb.const_universes | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with | Monomorphic_const ctx -> - Monomorphic_const (ContextSet.union body_uctxs ctx), [] + Monomorphic_const (ContextSet.union body_uctxs ctx) | Polymorphic_const ctx -> assert(ContextSet.is_empty body_uctxs); - let inst = make_abstract_instance ctx in - Polymorphic_const ctx, - Array.to_list (Instance.to_array inst) + Polymorphic_const ctx in let ctx = UState.of_binders - (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl) + (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in diff --git a/printing/printmod.ml b/printing/printmod.ml index f8d88aea07..1fc308ac99 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -119,14 +119,7 @@ let print_mutual_inductive env mind mib udecl = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in - let univs = - let open Univ in - if Declareops.inductive_is_polymorphic mib then - Array.to_list (Instance.to_array - (make_abstract_instance (Declareops.inductive_polymorphic_context mib))) - else [] - in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative @@ -164,8 +157,7 @@ let print_record env mind mib udecl = let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) - (Array.to_list (Univ.Instance.to_array u)) udecl in + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in @@ -304,8 +296,7 @@ let print_body is_impl env mp (l,body) = (match env with | None -> mt () | Some env -> - let univs = Array.to_list (Univ.Instance.to_array (Univ.make_abstract_instance ctx)) in - let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) univs None in + let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in let sigma = Evd.from_ctx (UState.of_binders bl) in str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ |