diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 15 | ||||
| -rw-r--r-- | printing/prettyp.mli | 8 | ||||
| -rw-r--r-- | printing/printer.ml | 12 | ||||
| -rw-r--r-- | printing/printer.mli | 9 |
4 files changed, 27 insertions, 17 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e2c0f55f8..93970512d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -42,8 +42,8 @@ type object_pr = { print_named_decl : Context.Named.Declaration.t -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds; } let gallina_print_module = print_module @@ -433,8 +433,8 @@ let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MOD (**** Gallina layer *****) let gallina_print_typed_value_in_env env sigma (trm,typ) = - (pr_lconstr_env env sigma trm ++ fnl () ++ - str " : " ++ pr_ltype_env env sigma typ) + (pr_leconstr_env env sigma trm ++ fnl () ++ + str " : " ++ pr_letype_env env sigma typ) (* To be improved; the type should be used to provide the types in the abstractions. This should be done recursively inside pr_lconstr, so that @@ -595,8 +595,7 @@ let gallina_print_context with_values = prec let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env sigma (EConstr.of_constr trm) in - let ntrm = EConstr.Unsafe.to_constr ntrm in + let ntrm = red_fun env sigma trm in (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) (******************************************) @@ -643,6 +642,8 @@ let print_judgment env sigma {uj_val=trm;uj_type=typ} = let print_safe_judgment env sigma j = let trm = Safe_typing.j_val j in let typ = Safe_typing.j_type j in + let trm = EConstr.of_constr trm in + let typ = EConstr.of_constr typ in print_typed_value_in_env env sigma (trm, typ) (*********************) @@ -762,7 +763,9 @@ let print_opaque_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> + let open EConstr in let ty = Universes.unsafe_type_of_global gr in + let ty = EConstr.of_constr ty in print_typed_value (mkConstruct cstr, ty) | VarRef id -> env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 0eab15579..38e111034 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -27,11 +27,11 @@ val print_full_context_typ : unit -> std_ppcmds val print_full_pure_context : unit -> std_ppcmds val print_sec_context : reference -> std_ppcmds val print_sec_context_typ : reference -> std_ppcmds -val print_judgment : env -> Evd.evar_map -> unsafe_judgment -> std_ppcmds +val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> std_ppcmds val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds val print_eval : reduction_function -> env -> Evd.evar_map -> - Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds + Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds val print_name : reference or_by_notation -> std_ppcmds val print_opaque_name : reference -> std_ppcmds @@ -69,8 +69,8 @@ type object_pr = { print_named_decl : Context.Named.Declaration.t -> std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; - print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> unsafe_judgment -> std_ppcmds + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds; + print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds } val set_object_pr : object_pr -> unit diff --git a/printing/printer.ml b/printing/printer.ml index 4a6c83bd7..ba4b68296 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -99,7 +99,6 @@ let pr_type_core goal_concl_style env sigma t = let pr_ltype_core goal_concl_style env sigma t = pr_lconstr_expr (extern_type goal_concl_style env sigma t) -let pr_goal_concl_style_env env = pr_ltype_core true env let pr_ltype_env env = pr_ltype_core false env let pr_type_env env = pr_type_core false env @@ -110,8 +109,13 @@ let pr_type t = let (sigma, env) = get_current_context () in pr_type_env env sigma t +let pr_etype_env env sigma c = pr_type_env env sigma (EConstr.to_constr sigma c) +let pr_letype_env env sigma c = pr_ltype_env env sigma (EConstr.to_constr sigma c) +let pr_goal_concl_style_env env sigma c = + pr_ltype_core true env sigma (EConstr.to_constr sigma c) + let pr_ljudge_env env sigma j = - (pr_lconstr_env env sigma j.uj_val, pr_lconstr_env env sigma j.uj_type) + (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) let pr_ljudge j = let (sigma, env) = get_current_context () in @@ -390,7 +394,7 @@ let pr_transparent_state (ids, csts) = let default_pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in let env = Goal.V82.env sigma g in - let concl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma g) in + let concl = Goal.V82.concl sigma g in let goal = pr_context_of env sigma ++ cut () ++ str "============================" ++ cut () ++ @@ -413,7 +417,7 @@ let pr_goal_name sigma g = let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in - let pc = pr_goal_concl_style_env env sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in + let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in str (emacs_str "") ++ str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++ str " is:" ++ cut () ++ str" " ++ pc diff --git a/printing/printer.mli b/printing/printer.mli index 7521468e2..504392e35 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -43,6 +43,9 @@ val pr_econstr : EConstr.t -> std_ppcmds val pr_leconstr_env : env -> evar_map -> EConstr.t -> std_ppcmds val pr_leconstr : EConstr.t -> std_ppcmds +val pr_etype_env : env -> evar_map -> EConstr.types -> std_ppcmds +val pr_letype_env : env -> evar_map -> EConstr.types -> std_ppcmds + val pr_open_constr_env : env -> evar_map -> open_constr -> std_ppcmds val pr_open_constr : open_constr -> std_ppcmds @@ -55,7 +58,7 @@ val pr_constr_under_binders : constr_under_binders -> std_ppcmds val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds -val pr_goal_concl_style_env : env -> evar_map -> types -> std_ppcmds +val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> std_ppcmds val pr_ltype_env : env -> evar_map -> types -> std_ppcmds val pr_ltype : types -> std_ppcmds @@ -65,8 +68,8 @@ val pr_type : types -> std_ppcmds val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> std_ppcmds val pr_closed_glob : closed_glob_constr -> std_ppcmds -val pr_ljudge_env : env -> evar_map -> unsafe_judgment -> std_ppcmds * std_ppcmds -val pr_ljudge : unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge : EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds val pr_lglob_constr_env : env -> glob_constr -> std_ppcmds val pr_lglob_constr : glob_constr -> std_ppcmds |