blob: 40ae1a7b05e931c74c809fa277c0253fcb48b093 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
open Names
open Univ
let pp x = Pp.pp_with Format.std_formatter x
(** Future printer *)
let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
(* name printers *)
let ppid id = pp (Id.print id)
let pplab l = pp (Label.print l)
let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
let ppdir dir = pp (DirPath.print dir)
let ppmp mp = pp(str (ModPath.debug_to_string mp))
let ppcon con = pp(Constant.debug_print con)
let ppproj con = pp(Constant.debug_print (Projection.constant con))
let ppkn kn = pp(str (KerName.to_string kn))
let ppmind kn = pp(MutInd.debug_print kn)
let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
(* term printers *)
let ppbigint n = pp (str (Bigint.to_string n));;
let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
let ppintset l = pp (prset int (Int.Set.elements l))
let ppidset l = pp (prset Id.print (Id.Set.elements l))
let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
let pridmap pr l =
let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in
prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
let ppidmap pr l = pp (pridmap pr l)
let pridmapgen l =
let dom = Id.Set.elements (Id.Map.domain l) in
if dom = [] then str "[]" else
str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]"
let ppidmapgen l = pp (pridmapgen l)
let prididmap = pridmap (fun _ -> Id.print)
let ppididmap = ppidmap (fun _ -> Id.print)
let pP s = pp (hov 0 s)
(* proof printers *)
let ppuni u = pp(Universe.pr u)
let ppuni_level u = pp (Level.pr u)
let ppuniverse_set l = pp (LSet.pr l)
let ppuniverse_instance l = pp (Instance.pr l)
let ppauniverse_context l = pp (AUContext.pr Level.pr l)
let ppuniverse_context l = pp (pr_universe_context Level.pr l)
let ppconstraints c = pp (pr_constraints Level.pr c)
let ppuniverse_context_future c =
let ctx = Future.force c in
ppuniverse_context ctx
let ppuniverses u = pp (Univ.pr_universes u)
let pploc x = let (l,r) = Loc.unloc x in
print_string"(";print_int l;print_string",";print_int r;print_string")"
|
