diff options
| -rw-r--r-- | engine/univNames.ml | 33 | ||||
| -rw-r--r-- | printing/prettyp.ml | 51 | ||||
| -rw-r--r-- | printing/printer.ml | 19 | ||||
| -rw-r--r-- | printing/printer.mli | 5 | ||||
| -rw-r--r-- | printing/printmod.ml | 46 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.out | 26 | ||||
| -rw-r--r-- | vernac/himsg.ml | 3 |
7 files changed, 96 insertions, 87 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml index e861913de2..29d92c46ea 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Util open Names open Univ open Nametab @@ -65,6 +66,24 @@ let subst_ubinder (subst,(ref,l as orig)) = if ref == ref' then orig else ref', l 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 + | 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 + in + let l = Array.fold_left_i fold l (Instance.to_array sec_inst) in Some (Lib.discharge_global ref, l) let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = @@ -86,6 +105,20 @@ let register_universe_binders ref 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 + in if not (Id.Map.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9ed985195f..605c1ae957 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -71,17 +71,18 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref udecl = - let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in - let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in + 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 sigma = Evd.from_ctx (UState.of_binders bl) in let typ = EConstr.of_constr typ in let typ = if reduce then let env = Global.env () in - let sigma = Evd.from_env env in let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in - let univs = Global.universes_of_global ref in let variance = match ref with | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> @@ -91,19 +92,14 @@ let print_ref reduce ref udecl = | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) end in - let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in let env = Global.env () in - let bl = UnivNames.universe_binders_with_opt_names ref - (Array.to_list (Univ.Instance.to_array inst)) udecl in - let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = if Global.is_polymorphic ref - then Printer.pr_universe_instance sigma (Univ.UContext.instance univs) + then Printer.pr_universe_instance sigma inst else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_universe_ctx sigma ?variance univs) + Printer.pr_abstract_universe_ctx sigma ?variance univs) (********************************) (** Printing implicit arguments *) @@ -552,43 +548,36 @@ let print_typed_body env evd (val_0,typ) = let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then let univs = Declareops.constant_polymorphic_context cb in - let inst = Univ.AUContext.instance univs in + let inst = Univ.make_abstract_instance univs in pr_universe_instance sigma inst else mt() 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 = - match cb.const_universes with - | Monomorphic_const _ -> cb.const_type - | Polymorphic_const univs -> - let inst = Univ.AUContext.instance univs in - Vars.subst_instance_constr inst cb.const_type - in + let typ = cb.const_type in let univs, ulist = - let open Entries in 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_entry ctx, [] + | Monomorphic_const ctx -> Monomorphic_const ctx, [] | Polymorphic_const ctx -> - let inst = AUContext.instance ctx in - Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)), + let inst = make_abstract_instance ctx in + Polymorphic_const ctx, Array.to_list (Instance.to_array inst) end | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with | Monomorphic_const ctx -> - Monomorphic_const_entry (ContextSet.union body_uctxs ctx), [] + Monomorphic_const (ContextSet.union body_uctxs ctx), [] | Polymorphic_const ctx -> assert(ContextSet.is_empty body_uctxs); - let inst = AUContext.instance ctx in - Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)), + let inst = make_abstract_instance ctx in + Polymorphic_const ctx, Array.to_list (Instance.to_array inst) in let ctx = @@ -605,7 +594,6 @@ let print_constant with_values sep sp udecl = str" ]" ++ Printer.pr_constant_universes sigma univs | Some (c, ctx) -> - let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_constant_universes sigma univs) @@ -712,11 +700,6 @@ let print_eval x = !object_pr.print_eval x (**** Printing declarations and judgments *) (**** Abstract layer *****) -let print_typed_value x = - let env = Global.env () in - let sigma = Evd.from_env env in - print_typed_value_in_env env sigma x - let print_judgment env sigma {uj_val=trm;uj_type=typ} = print_typed_value_in_env env sigma (trm, typ) @@ -852,11 +835,9 @@ let print_opaque_name env sigma qid = print_inductive sp None | ConstructRef cstr as gr -> let ty, ctx = Global.type_of_global_in_context env gr in - let inst = Univ.AUContext.instance ctx in - let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in let open EConstr in - print_typed_value (mkConstruct cstr, ty) + print_typed_value_in_env env sigma (mkConstruct cstr, ty) | VarRef id -> env |> lookup_named id |> print_named_decl env sigma diff --git a/printing/printer.ml b/printing/printer.ml index 5b3ead181f..043371be73 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -270,9 +270,16 @@ let pr_universe_ctx sigma ?variance c = else mt() +let pr_abstract_universe_ctx sigma ?variance c = + if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c + else + mt() + let pr_constant_universes sigma = function - | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx - | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx + | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx + | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx let pr_cumulativity_info sigma cumi = if !Detyping.print_universes @@ -282,6 +289,14 @@ let pr_cumulativity_info sigma cumi = else mt() +let pr_abstract_cumulativity_info sigma cumi = + if !Detyping.print_universes + && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + else + mt() + (**********************************************************************) (* Global references *) diff --git a/printing/printer.mli b/printing/printer.mli index 971241d5f9..f977ab2372 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -123,9 +123,12 @@ val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t +val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> + Univ.AUContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t -val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t +val pr_constant_universes : evar_map -> Declarations.constant_universes -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t +val pr_abstract_cumulativity_info : evar_map -> Univ.ACumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index e2d9850bf8..f8d88aea07 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -90,9 +90,7 @@ let build_ind_type env mip = Inductive.type_of_inductive env mip let print_one_inductive env sigma mib ((_,i) as ind) = - let u = if Declareops.inductive_is_polymorphic mib then - Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) - else Univ.Instance.empty in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in @@ -111,16 +109,6 @@ let print_one_inductive env sigma mib ((_,i) as ind) = str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes -let instantiate_cumulativity_info cumi = - let open Univ in - let univs = ACumulativityInfo.univ_context cumi in - let expose ctx = - let inst = AUContext.instance ctx in - let cst = AUContext.instantiate inst ctx in - UContext.make (inst, cst) - in - CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi) - let print_mutual_inductive env mind mib udecl = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in @@ -135,7 +123,7 @@ let print_mutual_inductive env mind mib udecl = let open Univ in if Declareops.inductive_is_polymorphic mib then Array.to_list (Instance.to_array - (AUContext.instance (Declareops.inductive_polymorphic_context mib))) + (make_abstract_instance (Declareops.inductive_polymorphic_context mib))) else [] in let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in @@ -150,8 +138,7 @@ let print_mutual_inductive env mind mib udecl = match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> - Printer.pr_cumulativity_info - sigma (instantiate_cumulativity_info cumi)) + Printer.pr_abstract_cumulativity_info sigma cumi) let get_fields = let rec prodec_rec l subst c = @@ -167,11 +154,7 @@ let get_fields = prodec_rec [] [] let print_record env mind mib udecl = - let u = - if Declareops.inductive_is_polymorphic mib then - Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) - else Univ.Instance.empty - in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in @@ -210,8 +193,7 @@ let print_record env mind mib udecl = match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> - Printer.pr_cumulativity_info - sigma (instantiate_cumulativity_info cumi) + Printer.pr_abstract_cumulativity_info sigma cumi ) let pr_mutual_inductive_body env mind mib udecl = @@ -315,12 +297,6 @@ let print_body is_impl env mp (l,body) = | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> let ctx = Declareops.constant_polymorphic_context cb in - let u = - if Declareops.constant_is_polymorphic cb then - Univ.AUContext.instance ctx - else Univ.Instance.empty - in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -328,18 +304,18 @@ 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 sigma = Evd.from_ctx (UState.of_binders bl) in str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env (Evd.from_env env) - (Vars.subst_instance_constr u - cb.const_type)) ++ + hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env (Evd.from_env env) - (Vars.subst_instance_constr u (Mod_subst.force_constr l))) + Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx (Evd.from_env env) ctx) + Printer.pr_abstract_universe_ctx sigma ctx) | SFBmind mib -> try let env = Option.get env in diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 926114a1e1..22b998fab9 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -42,10 +42,10 @@ bar@{u} = nat *) bar is universe polymorphic -foo@{u Top.17 v} = -Type@{Top.17} -> Type@{v} -> Type@{u} - : Type@{max(u+1,Top.17+1,v+1)} -(* u Top.17 v |= *) +foo@{u Var(1) v} = +Type@{Var(1)} -> Type@{v} -> Type@{u} + : Type@{max(u+1,Var(1)+1,v+1)} +(* u Var(1) v |= *) foo is universe polymorphic Type@{i} -> Type@{j} @@ -86,10 +86,10 @@ Type@{M} -> Type@{N} -> Type@{E} (* E M N |= *) foo is universe polymorphic -foo@{Top.16 Top.17 Top.18} = -Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16} - : Type@{max(Top.16+1,Top.17+1,Top.18+1)} -(* Top.16 Top.17 Top.18 |= *) +foo@{Var(0) Var(1) Var(2)} = +Type@{Var(1)} -> Type@{Var(2)} -> Type@{Var(0)} + : Type@{max(Var(0)+1,Var(1)+1,Var(2)+1)} +(* Var(0) Var(1) Var(2) |= *) foo is universe polymorphic NonCumulative Inductive Empty@{E} : Type@{E} := @@ -125,7 +125,7 @@ bind_univs.poly@{u} = Type@{u} bind_univs.poly is universe polymorphic insec@{v} = Type@{u} -> Type@{v} - : Type@{max(u+1,v+1)} + : Type@{max(v+1,u+1)} (* v |= *) insec is universe polymorphic @@ -155,14 +155,14 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i} -(* i Top.48 Top.49 |= *) +axfoo@{i Var(1) Var(2)} : Type@{Var(1)} -> Type@{i} +(* i Var(1) Var(2) |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i} -(* i Top.48 Top.49 |= *) +axbar@{i Var(1) Var(2)} : Type@{Var(2)} -> Type@{i} +(* i Var(1) Var(2) |= *) axbar is universe polymorphic Argument scope is [type_scope] diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a4650cfd92..1b6d12a976 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -896,7 +896,8 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ - let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in + let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in + (** FIXME: provide a proper naming for the bound variables *) quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = |