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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
open Pp
open Genarg
open Misctypes
open Locus
open Genredexpr
let pr_located pr (loc, x) =
match loc with
| Some loc when !Flags.beautify ->
let (b, e) = Loc.unloc loc in
(* Side-effect: order matters *)
let before = Pp.comment (CLexer.extract_comments b) in
let x = pr x in
let after = Pp.comment (CLexer.extract_comments e) in
before ++ x ++ after
| _ -> pr x
let pr_or_var pr = function
| ArgArg x -> pr x
| ArgVar (_,s) -> Names.Id.print s
let pr_with_occurrences pr keyword (occs,c) =
match occs with
| AllOccurrences ->
pr c
| NoOccurrences ->
failwith "pr_with_occurrences: no occurrences"
| OnlyOccurrences nl ->
hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
hov 0 (prlist_with_sep spc (pr_or_var int) nl))
| AllOccurrencesBut nl ->
hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
hov 0 (prlist_with_sep spc (pr_or_var int) nl))
exception ComplexRedFlag
let pr_short_red_flag pr r =
if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then
raise ComplexRedFlag
else if List.is_empty r.rConst then
if r.rDelta then mt () else raise ComplexRedFlag
else (if r.rDelta then str "-" else mt ()) ++
hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
let pr_red_flag pr r =
try pr_short_red_flag pr r
with complexRedFlags ->
(if r.rBeta then pr_arg str "beta" else mt ()) ++
(if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
(if r.rMatch then pr_arg str "match" else mt ()) ++
(if r.rFix then pr_arg str "fix" else mt ()) ++
(if r.rCofix then pr_arg str "cofix" else mt ())) ++
(if r.rZeta then pr_arg str "zeta" else mt ()) ++
(if List.is_empty r.rConst then
if r.rDelta then pr_arg str "delta"
else mt ()
else
pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
let pr_union pr1 pr2 = function
| Inl a -> pr1 a
| Inr b -> pr2 b
let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
| Red false -> keyword "red"
| Hnf -> keyword "hnf"
| Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
| Cbv f ->
if f.rBeta && f.rMatch && f.rFix && f.rCofix &&
f.rZeta && f.rDelta && List.is_empty f.rConst then
keyword "compute"
else
hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
| Lazy f ->
hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
| Cbn f ->
hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
| Unfold l ->
hov 1 (keyword "unfold" ++ spc() ++
prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l)
| Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
| Pattern l ->
hov 1 (keyword "pattern" ++
pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l)
| Red true ->
CErrors.user_err Pp.(str "Shouldn't be accessible from user.")
| ExtraRedExpr s ->
str s
| CbvVm o ->
keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
| CbvNative o ->
keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
let pr_or_by_notation f = function
| AN v -> f v
| ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
let rec pr_raw_generic env (GenArg (Rawwit wit, x)) =
match wit with
| ListArg wit ->
let map x = pr_raw_generic env (in_gen (rawwit wit) x) in
let ans = pr_sequence map x in
hov_if_not_empty 0 ans
| OptArg wit ->
let ans = match x with
| None -> mt ()
| Some x -> pr_raw_generic env (in_gen (rawwit wit) x)
in
hov_if_not_empty 0 ans
| PairArg (wit1, wit2) ->
let p, q = x in
let p = in_gen (rawwit wit1) p in
let q = in_gen (rawwit wit2) q in
hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q])
| ExtraArg s ->
let open Genprint in
match generic_raw_print (in_gen (rawwit wit) x) with
| PrinterBasic pp -> pp ()
| PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
let rec pr_glb_generic env (GenArg (Glbwit wit, x)) =
match wit with
| ListArg wit ->
let map x = pr_glb_generic env (in_gen (glbwit wit) x) in
let ans = pr_sequence map x in
hov_if_not_empty 0 ans
| OptArg wit ->
let ans = match x with
| None -> mt ()
| Some x -> pr_glb_generic env (in_gen (glbwit wit) x)
in
hov_if_not_empty 0 ans
| PairArg (wit1, wit2) ->
let p, q = x in
let p = in_gen (glbwit wit1) p in
let q = in_gen (glbwit wit2) q in
let ans = pr_sequence (pr_glb_generic env) [p; q] in
hov_if_not_empty 0 ans
| ExtraArg s ->
let open Genprint in
match generic_glb_print (in_gen (glbwit wit) x) with
| PrinterBasic pp -> pp ()
| PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded
|
