diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 1 | ||||
| -rw-r--r-- | printing/prettyp.ml | 117 | ||||
| -rw-r--r-- | printing/prettyp.mli | 47 | ||||
| -rw-r--r-- | printing/printer.ml | 40 | ||||
| -rw-r--r-- | printing/printer.mli | 7 |
5 files changed, 132 insertions, 80 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index aea4f23205..5ed96dd5e3 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -21,7 +21,6 @@ open Glob_term open Constrexpr open Constrexpr_ops open Notation_gram -open Decl_kinds open Namegen (*i*) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f82b9cef68..fb0b1eca8d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -35,14 +35,14 @@ module NamedDecl = Context.Named.Declaration type object_pr = { 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_constant_with_infos : Opaqueproof.indirect_accessor -> 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 -> 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_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : Opaqueproof.indirect_accessor -> 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; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } @@ -221,14 +221,22 @@ let print_if_is_coercion ref = (*******************) (* *) +let pr_template_variables = function + | [] -> mt () + | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars + let print_polymorphism ref = let poly = Global.is_polymorphic ref in let template_poly = Global.is_template_polymorphic ref in - [ pr_global ref ++ str " is " ++ str - (if poly then "universe polymorphic" + let template_checked = Global.is_template_checked ref in + let template_variables = Global.get_template_polymorphic_variables ref in + [ pr_global ref ++ str " is " ++ + (if poly then str "universe polymorphic" else if template_poly then - "template universe polymorphic" - else "not universe polymorphic") ] + (if not template_checked then str "assumed " else mt()) ++ + str "template universe polymorphic " + ++ h 0 (pr_template_variables template_variables) + else str "not universe polymorphic") ] let print_type_in_type ref = let unsafe = Global.is_type_in_type ref in @@ -552,10 +560,10 @@ let print_instance sigma cb = let inst = Univ.make_abstract_instance univs in pr_universe_instance sigma inst else mt() - -let print_constant with_values sep sp udecl = + +let print_constant indirect_accessor with_values sep sp udecl = let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in + let val_0 = Global.body_of_constant_body indirect_accessor cb in let typ = cb.const_type in let univs = let open Univ in @@ -563,7 +571,7 @@ let print_constant with_values sep sp udecl = match cb.const_body with | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in + let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in match cb.const_universes with | Monomorphic ctx -> Monomorphic (ContextSet.union body_uctxs ctx) @@ -593,8 +601,8 @@ let print_constant with_values sep sp udecl = (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universes sigma univs ?priv) -let gallina_print_constant_with_infos sp udecl = - print_constant true " = " sp udecl ++ +let gallina_print_constant_with_infos indirect_accessor sp udecl = + print_constant indirect_accessor true " = " sp udecl ++ with_line_skip (print_name_infos (GlobRef.ConstRef sp)) let gallina_print_syntactic_def env kn = @@ -610,7 +618,7 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> @@ -621,7 +629,7 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> - Some (print_constant with_values sep (Constant.make1 kn) None) + Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) | (_,"INDUCTIVE") -> Some (gallina_print_inductive (MutInd.make1 kn) None) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| @@ -637,24 +645,24 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = Some (print_modtype (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry env sigma with_values ent = +let gallina_print_library_entry indirect_accessor env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry env sigma with_values (oname,lobj) + gallina_print_leaf_entry indirect_accessor env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> - Some (str " >>>>>>> Section " ++ pr_name oname) + Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> - Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) + Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> - Some (str " >>>>>>> Module " ++ pr_name oname) + Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context env sigma with_values = +let gallina_print_context indirect_accessor env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry env sigma with_values h with - | None -> prec n rest - | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) + (match gallina_print_library_entry indirect_accessor env sigma with_values h with + | None -> prec n rest + | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () in prec @@ -712,10 +720,10 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context env sigma = print_context env sigma true None (Lib.contents ()) -let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ()) +let print_full_context indirect_accessor env sigma = print_context indirect_accessor env sigma true None (Lib.contents ()) +let print_full_context_typ indirect_accessor env sigma = print_context indirect_accessor env sigma false None (Lib.contents ()) -let print_full_pure_context env sigma = +let print_full_pure_context ~library_accessor env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with @@ -731,8 +739,8 @@ let print_full_pure_context env sigma = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc)) - | Def c -> + str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) + | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ pr_lconstr_env env sigma (Mod_subst.force_constr c) @@ -779,11 +787,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context env sigma sec = - print_context env sigma true None (read_sec_context sec) +let print_sec_context indirect_accessor env sigma sec = + print_context indirect_accessor env sigma true None (read_sec_context sec) -let print_sec_context_typ env sigma sec = - print_context env sigma false None (read_sec_context sec) +let print_sec_context_typ indirect_accessor env sigma sec = + print_context indirect_accessor env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -793,11 +801,11 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name env sigma na udecl = +let print_any_name indirect_accessor env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with - | Term (ConstRef sp) -> print_constant_with_infos sp udecl + | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl | Term (IndRef (sp,_)) -> print_inductive sp udecl | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp @@ -816,34 +824,34 @@ let print_any_name env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name env sigma na udecl = +let print_name indirect_accessor env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name env sigma - (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + print_any_name indirect_accessor env sigma + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) - udecl + udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name env sigma (locate_any_name ref) udecl + print_any_name indirect_accessor env sigma (locate_any_name ref) udecl -let print_opaque_name env sigma qid = +let print_opaque_name indirect_accessor env sigma qid = let open GlobRef in match Nametab.global qid with | ConstRef cst -> - let cb = Global.lookup_constant cst in - if Declareops.constant_has_body cb then - print_constant_with_infos cst None - else - user_err Pp.(str "Not a defined constant.") + let cb = Global.lookup_constant cst in + if Declareops.constant_has_body cb then + print_constant_with_infos indirect_accessor cst None + else + user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> - print_inductive sp None + print_inductive sp None | ConstructRef cstr as gr -> - let ty, ctx = Typeops.type_of_global_in_context env gr in - let ty = EConstr.of_constr ty in - let open EConstr in - print_typed_value_in_env env sigma (mkConstruct cstr, ty) + let ty, ctx = Typeops.type_of_global_in_context env gr in + let ty = EConstr.of_constr ty in + let open EConstr in + print_typed_value_in_env env sigma (mkConstruct cstr, ty) | VarRef id -> - env |> lookup_named id |> print_named_decl env sigma + env |> lookup_named id |> print_named_decl env sigma let print_about_any ?loc env sigma k udecl = maybe_error_reject_univ_decl k udecl; @@ -880,9 +888,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect env sigma depth = - print_context env sigma false (Some depth) (Lib.contents ()) - +let inspect indirect_accessor env sigma depth = + print_context indirect_accessor env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 7485f4bd19..4299bcc880 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -18,22 +18,41 @@ open Libnames val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref -val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t -val print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option -val print_full_context : env -> Evd.evar_map -> Pp.t -val print_full_context_typ : env -> Evd.evar_map -> Pp.t -val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t -val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t +val print_context + : Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry + : Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option +val print_full_context + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t +val print_full_context_typ + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + +val print_full_pure_context + : library_accessor:Opaqueproof.indirect_accessor + -> env + -> Evd.evar_map + -> Pp.t + +val print_sec_context + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> - UnivNames.univ_name_list option -> Pp.t -val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t +val print_name + : Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation + -> UnivNames.univ_name_list option -> Pp.t +val print_opaque_name + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t @@ -50,7 +69,7 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect : env -> Evd.evar_map -> int -> Pp.t +val inspect : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -83,14 +102,14 @@ val print_located_other : string -> qualid -> Pp.t type object_pr = { 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_constant_with_infos : Opaqueproof.indirect_accessor -> 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 -> Constr.named_declaration -> Pp.t; - print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : Opaqueproof.indirect_accessor -> 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; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/printing/printer.ml b/printing/printer.ml index ec1b9b8e49..328082fbc2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -853,7 +853,10 @@ let pr_goal_emacs ~proof gid sid = type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism + on parameter universes has not been checked. *) + | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) @@ -872,10 +875,13 @@ struct Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 + | TemplatePolymorphic m1, TemplatePolymorphic m2 -> + MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> - Constant.CanOrd.compare k1 k2 + GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 + | _, TemplatePolymorphic _ -> 1 | _ -> -1 let compare x y = @@ -903,14 +909,20 @@ let pr_assumptionset env sigma s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> - (* FIXME? *) - let mp,lab = Constant.repr2 kn in - str (ModPath.to_string mp) ++ str "." ++ Label.print lab + Names.Constant.print kn + in + let safe_pr_global env gr = + try pr_global_env (Termops.vars_of_env env) gr + with Not_found -> + let open GlobRef in match gr with + | VarRef id -> Id.print id + | ConstRef con -> Constant.print con + | IndRef (mind,_) -> MutInd.print mind + | ConstructRef _ -> assert false in let safe_pr_inductive env kn = try pr_inductive env (kn,0) with Not_found -> - (* FIXME? *) MutInd.print kn in let safe_pr_ltype env sigma typ = @@ -927,9 +939,14 @@ let pr_assumptionset env sigma s = | Constant kn -> safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> - hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.") - | Guarded kn -> - hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") + hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") + | Guarded gr -> + hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") + | TemplatePolymorphic m -> + hov 2 (safe_pr_inductive env m ++ spc () ++ + strbrk"is assumed template polymorphic on all its universe parameters.") + | TypeInType gr -> + hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in let fold t typ accu = let (v, a, o, tr) = accu in @@ -1003,3 +1020,8 @@ let print_and_diff oldp newp = pr_open_subgoals ~proof in Feedback.msg_notice output;; + +let pr_typing_flags flags = + str "check_guarded: " ++ bool flags.check_guarded ++ fnl () + ++ str "check_positive: " ++ bool flags.check_positive ++ fnl () + ++ str "check_universes: " ++ bool flags.check_universes diff --git a/printing/printer.mli b/printing/printer.mli index a72f319636..d62d3789d3 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -191,7 +191,10 @@ val print_and_diff : Proof.t option -> Proof.t option -> unit type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) - | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) + | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism + on parameter universes has not been checked. *) + | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) @@ -207,3 +210,5 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t + +val pr_typing_flags : Declarations.typing_flags -> Pp.t |