diff options
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 49 |
1 files changed, 27 insertions, 22 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ab679a71ce..8129a4a867 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -64,8 +64,14 @@ let ppwf_paths x = pp (Rtree.pp_tree prrecarg x) let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma let rawdebug = ref false let ppevar evk = pp (Evar.print evk) -let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) -let ppeconstr x = pp (Termops.print_constr x) +let pr_constr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_constr_env env sigma t +let pr_econstr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_econstr_env env sigma t +let ppconstr x = pp (pr_constr x) +let ppeconstr x = pp (pr_econstr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x @@ -95,9 +101,9 @@ let ppidmapgen l = pp (pridmapgen l) let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 - (Termops.print_constr (EConstr.of_constr c) ++ + (pr_constr c ++ (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++ - Termops.print_constr (EConstr.of_constr c) ++ str">") ++ + pr_constr c ++ str">") ++ (if id = id0 then mt () else spc () ++ str "<canonical: " ++ Id.print id ++ str ">")))) @@ -106,7 +112,7 @@ let ppididmap = ppidmap (fun _ -> Id.print) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") - ++ str "," ++ spc () ++ Termops.print_constr c) + ++ str "," ++ spc () ++ pr_econstr c) let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) @@ -133,7 +139,7 @@ let safe_pr_global = function | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")") | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str ")") - | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++ + | ConstructRef ((kn,i),j) -> pp (str "CONSTRUCTREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str "," ++ int j ++ str ")") | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")") @@ -155,9 +161,9 @@ let ppdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) -let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n) -let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) -let pp_state_t n = pp (Reductionops.pr_state n) +let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n) +let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n) +let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) @@ -546,23 +552,22 @@ open Libnames let encode_path ?loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] - | Some (mp,dir) -> - (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ - DirPath.repr dir) in + | Some mp -> DirPath.repr (dirpath_of_string (ModPath.to_string mp)) + in make_qualid ?loc (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id let raw_string_of_ref ?loc _ = function | ConstRef cst -> - let (mp,dir,id) = Constant.repr3 cst in - encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id) + let (mp,id) = Constant.repr2 cst in + encode_path ?loc "CST" (Some mp) [] (Label.to_id id) | IndRef (kn,i) -> - let (mp,dir,id) = MutInd.repr3 kn in - encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id] + let (mp,id) = MutInd.repr2 kn in + encode_path ?loc "IND" (Some mp) [Label.to_id id] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> - let (mp,dir,id) = MutInd.repr3 kn in - encode_path ?loc "CSTR" (Some (mp,dir)) + let (mp,id) = MutInd.repr2 kn in + encode_path ?loc "CSTR" (Some mp) [Label.to_id id;Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) | VarRef id -> @@ -570,14 +575,14 @@ let raw_string_of_ref ?loc _ = function let short_string_of_ref ?loc _ = function | VarRef id -> qualid_of_ident ?loc id - | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst))) - | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn))) + | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (Constant.label cst)) + | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (MutInd.label kn)) | IndRef (kn,i) -> - encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] + encode_path ?loc "IND" None [Label.to_id (MutInd.label kn)] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> encode_path ?loc "CSTR" None - [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)] + [Label.to_id (MutInd.label kn);Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) (* Anticipate that printers can be used from ocamldebug and that |