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
162
163
164
165
166
167
|
(*
* This file is part of Coccinelle, licensed under the terms of the GPL v2.
* See copyright.txt in the Coccinelle source code for more information.
* The Coccinelle source code can be obtained at http://coccinelle.lip6.fr
*)
open Common
open Format
open Ast_ctl
(* todo?: a txt_to_latex, that use Format to compute the good space but
* then generate latex to better output.
*)
let char_and = "&"
let char_and_any = "&+"
let char_hack = "&h+"
let char_or = "v"
let char_seqor = "|"
let char_not = "!"
let char_back = "^"
(*
let char_and = "/\\"
let char_or = "\\/"
let char_not = "-|"
*)
(* need introduce the Val constructor, or use -rectype. *)
type ('a,'b,'c) environment = (string, ('a,'b,'c) binding_val) Common.assoc
and ('a, 'b, 'c) binding_val =
Val of ('a,'b,'c) generic_ctl * ('a,'b,'c) environment
let (pp_ctl:
('pred -> unit) * ('mvar -> unit) -> bool ->
('pred, 'mvar, 'info) generic_ctl ->
unit) =
fun (pp_pred, pp_mvar) inline_let_def ctl ->
let rec pp_aux env = function
False -> pp "False"
| True -> pp "True"
| Pred(p) -> pp_pred p
| Not(phi) ->
pp char_not; Common.pp_do_in_box (fun () -> pp_aux env phi)
| Exists(keep,v,phi) ->
pp "(";
if keep then pp ("Ex ") else pp ("Ex_ ");
pp_mvar v;
pp " . ";
print_cut();
Common.pp_do_in_box (fun () -> pp_aux env phi);
pp ")";
| AndAny(dir,s,phi1,phi2) ->
pp_2args env (char_and_any^(pp_dirc dir)^(pp_sc s)) phi1 phi2;
| HackForStmt(dir,s,phi1,phi2) ->
pp_2args env (char_hack^(pp_dirc dir)^(pp_sc s)) phi1 phi2;
| And(s,phi1,phi2) -> pp_2args env (char_and^(pp_sc s)) phi1 phi2;
| Or(phi1,phi2) -> pp_2args env char_or phi1 phi2;
| SeqOr(phi1,phi2) -> pp_2args env char_seqor phi1 phi2;
| Implies(phi1,phi2) -> pp_2args env "=>" phi1 phi2;
| AF(dir,s,phi1) -> pp "AF"; pp_dir dir; pp_s s; pp_arg_paren env phi1;
| AX(dir,s,phi1) -> pp "AX"; pp_dir dir; pp_s s; pp_arg_paren env phi1;
| AG(dir,s,phi1) -> pp "AG"; pp_dir dir; pp_s s; pp_arg_paren env phi1;
| EF(dir,phi1) -> pp "EF"; pp_dir dir; pp_arg_paren env phi1;
| EX(dir,phi1) -> pp "EX"; pp_dir dir; pp_arg_paren env phi1;
| EG(dir,phi1) -> pp "EG"; pp_dir dir; pp_arg_paren env phi1;
| AW(dir,s,phi1,phi2) ->
pp "A"; pp_dir dir; pp_s s; pp "[";
pp_2args_bis env "W" phi1 phi2;
pp "]"
| AU(dir,s,phi1,phi2) ->
pp "A"; pp_dir dir; pp_s s; pp "[";
pp_2args_bis env "U" phi1 phi2;
pp "]"
| EU(dir,phi1,phi2) ->
pp "E"; pp_dir dir; pp "[";
pp_2args_bis env "U" phi1 phi2;
pp "]"
| Let (x,phi1,phi2) ->
let env' = (x, (Val (phi1,env)))::env in
if not inline_let_def
then
begin
pp ("Let"^" "^x);
pp " = ";
print_cut();
Common.pp_do_in_box (fun () -> pp_aux env phi1);
print_space ();
pp "in";
print_space ();
end;
pp_do_in_zero_box (fun () -> pp_aux env' phi2);
| LetR (dir,x,phi1,phi2) ->
let env' = (x, (Val (phi1,env)))::env in
if not inline_let_def
then
begin
pp ("LetR"^" "^x); pp_dir dir;
pp " = ";
print_cut();
Common.pp_do_in_box (fun () -> pp_aux env phi1);
print_space ();
pp "in";
print_space ();
end;
pp_do_in_zero_box (fun () -> pp_aux env' phi2);
| Ref(s) ->
if inline_let_def
then
let Val (phi1,env') = List.assoc s env in
pp_aux env' phi1
else
(* pp "Ref("; *)
pp s
(* pp ")" *)
| Uncheck(phi1) ->
pp "Uncheck"; pp_arg_paren env phi1
| InnerAnd(phi1) ->
pp "InnerAnd"; pp_arg_paren env phi1
| XX phi1 -> pp "XX"; pp_arg_paren env phi1
and pp_dir = function
FORWARD -> ()
| BACKWARD -> pp char_back
and pp_dirc = function
FORWARD -> ""
| BACKWARD -> char_back
and pp_s = function
STRICT -> if !Flag_ctl.partial_match then pp "," else ()
| NONSTRICT -> ()
and pp_sc = function
STRICT -> ","
| NONSTRICT -> ""
and pp_2args env sym phi1 phi2 =
begin
pp "(";
Common.pp_do_in_box (fun () -> pp_aux env phi1);
print_space();
pp sym;
print_space ();
Common.pp_do_in_box (fun () -> pp_aux env phi2);
pp ")";
end
and pp_2args_bis env sym phi1 phi2 =
begin
Common.pp_do_in_box (fun () -> pp_aux env phi1);
print_space();
pp sym;
print_space();
Common.pp_do_in_box (fun () -> pp_aux env phi2);
end
and pp_arg_paren env phi = Common.pp_do_in_box (fun () ->
pp "(";
pp_aux env phi;
pp ")";
)
in
Common.pp_do_in_box (fun () -> pp_aux [] ctl;)
|
