diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 61 |
1 files changed, 27 insertions, 34 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1f17d844..1810cc65 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -26,7 +26,6 @@ open Libobject open Libnames open Globnames open Recordops -open Misctypes open Printer open Printmod open Context.Rel.Declaration @@ -35,13 +34,13 @@ open Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type object_pr = { - print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t; - print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t; + print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; @@ -77,7 +76,9 @@ let print_ref reduce ref udecl = let typ = EConstr.of_constr typ in let typ = if reduce then - let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ + 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 @@ -93,11 +94,12 @@ let print_ref reduce ref udecl = 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 = Universes.universe_binders_with_opt_names ref + 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 univs + if Global.is_polymorphic ref + then Printer.pr_universe_instance sigma (Univ.UContext.instance univs) else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ @@ -245,13 +247,13 @@ let print_type_in_type ref = else [] let print_primitive_record recflag mipv = function - | Some (Some (_, ps,_)) -> + | PrimRecord _ -> let eta = match recflag with | CoFinite | Finite -> str" without eta conversion" | BiFinite -> str " with eta conversion" in [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] - | _ -> [] + | FakeRecord | NotRecord -> [] let print_primitive ref = match ref with @@ -328,7 +330,7 @@ type 'a locatable_info = { type locatable = Locatable : 'a locatable_info -> locatable type logical_name = - | Term of global_reference + | Term of GlobRef.t | Dir of global_dir_reference | Syntactic of KerName.t | ModuleType of ModPath.t @@ -343,8 +345,7 @@ let register_locatable name f = exception ObjFound of logical_name -let locate_any_name ref = - let {v=qid} = qualid_of_reference ref in +let locate_any_name qid = try Term (Nametab.locate qid) with Not_found -> try Syntactic (Nametab.locate_syndef qid) @@ -376,7 +377,6 @@ let pr_located_qualid = function | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir | DirModule { obj_dir ; _ } -> "Module", obj_dir - | DirClosedSection dir -> "Closed Section", dir in str s ++ spc () ++ DirPath.print dir | ModuleType mp -> @@ -452,8 +452,7 @@ type locatable_kind = | LocOther of string | LocAny -let print_located_qualid name flags ref = - let {v=qid} = qualid_of_reference ref in +let print_located_qualid name flags qid = let located = match flags with | LocTerm -> locate_term qid | LocModule -> locate_modtype qid @ locate_module qid @@ -554,8 +553,7 @@ 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 univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in - pr_universe_instance sigma univs + pr_universe_instance sigma inst else mt() let print_constant with_values sep sp udecl = @@ -595,7 +593,7 @@ let print_constant with_values sep sp udecl = in let ctx = UState.of_binders - (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl) + (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in @@ -659,14 +657,10 @@ let gallina_print_library_entry env sigma with_values ent = gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> - Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { obj_dir; _ }) -> Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) - | (oname,Lib.ClosedModule _) -> - Some (str " >>>>>>> Closed Module " ++ pr_name oname) let gallina_print_context env sigma with_values = let rec prec n = function @@ -718,7 +712,10 @@ let print_eval x = !object_pr.print_eval x (**** Printing declarations and judgments *) (**** Abstract layer *****) -let print_typed_value x = print_typed_value_in_env (Global.env ()) Evd.empty x +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) @@ -784,18 +781,14 @@ let print_full_pure_context env sigma = follows the definition of the inductive type *) (* This is designed to print the contents of an opened section *) -let read_sec_context r = - let qid = qualid_of_reference r in +let read_sec_context qid = let dir = - try Nametab.locate_section qid.v + try Nametab.locate_section qid with Not_found -> user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest -> if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | (_,Lib.ClosedSection _)::rest -> - user_err Pp.(str "Cannot print the contents of a closed section.") - (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in @@ -839,12 +832,12 @@ let print_any_name env sigma na udecl = let print_name env sigma na udecl = match na with - | {loc; v=ByNotation (ntn,sc)} -> + | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | {loc; v=AN ref} -> + | {loc; v=Constrexpr.AN ref} -> print_any_name env sigma (locate_any_name ref) udecl let print_opaque_name env sigma qid = @@ -892,11 +885,11 @@ let print_about_any ?loc env sigma k udecl = let print_about env sigma na udecl = match na with - | {loc;v=ByNotation (ntn,sc)} -> + | {loc;v=Constrexpr.ByNotation (ntn,sc)} -> print_about_any ?loc env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl - | {loc;v=AN ref} -> + | {loc;v=Constrexpr.AN ref} -> print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) @@ -909,7 +902,7 @@ let inspect env sigma depth = open Classops -let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v) +let print_coercion_value env sigma v = Printer.pr_global v.coe_value let print_class i = let cl,_ = class_info_from_index i in |