Commit | Line | Data |
---|---|---|
5636bb2c C |
1 | (* |
2 | * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen | |
3 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
4 | * This file is part of Coccinelle. | |
5 | * | |
6 | * Coccinelle is free software: you can redistribute it and/or modify | |
7 | * it under the terms of the GNU General Public License as published by | |
8 | * the Free Software Foundation, according to version 2 of the License. | |
9 | * | |
10 | * Coccinelle is distributed in the hope that it will be useful, | |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
13 | * GNU General Public License for more details. | |
14 | * | |
15 | * You should have received a copy of the GNU General Public License | |
16 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
17 | * | |
18 | * The authors reserve the right to distribute this or future versions of | |
19 | * Coccinelle under other licenses. | |
20 | *) | |
21 | ||
22 | ||
9f8e26f4 | 23 | (* |
ae4735db | 24 | * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen |
9f8e26f4 C |
25 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix |
26 | * This file is part of Coccinelle. | |
27 | * | |
28 | * Coccinelle is free software: you can redistribute it and/or modify | |
29 | * it under the terms of the GNU General Public License as published by | |
30 | * the Free Software Foundation, according to version 2 of the License. | |
31 | * | |
32 | * Coccinelle is distributed in the hope that it will be useful, | |
33 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
34 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
35 | * GNU General Public License for more details. | |
36 | * | |
37 | * You should have received a copy of the GNU General Public License | |
38 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
39 | * | |
40 | * The authors reserve the right to distribute this or future versions of | |
41 | * Coccinelle under other licenses. | |
42 | *) | |
43 | ||
44 | ||
34e49164 C |
45 | open Common |
46 | open Format | |
47 | ||
48 | open Ast_ctl | |
49 | ||
50 | (* todo?: a txt_to_latex, that use Format to compute the good space but | |
51 | * then generate latex to better output. | |
52 | *) | |
53 | ||
54 | let char_and = "&" | |
55 | let char_and_any = "&+" | |
56 | let char_hack = "&h+" | |
57 | let char_or = "v" | |
58 | let char_seqor = "|" | |
59 | let char_not = "!" | |
60 | let char_back = "^" | |
61 | ||
62 | (* | |
63 | let char_and = "/\\" | |
64 | let char_or = "\\/" | |
65 | let char_not = "-|" | |
66 | *) | |
67 | ||
68 | (* need introduce the Val constructor, or use -rectype. *) | |
ae4735db C |
69 | type ('a,'b,'c) environment = (string, ('a,'b,'c) binding_val) Common.assoc |
70 | and ('a, 'b, 'c) binding_val = | |
34e49164 C |
71 | Val of ('a,'b,'c) generic_ctl * ('a,'b,'c) environment |
72 | ||
ae4735db C |
73 | let rec (pp_ctl: |
74 | ('pred -> unit) * ('mvar -> unit) -> bool -> | |
75 | ('pred, 'mvar, 'info) generic_ctl -> | |
76 | unit) = | |
77 | fun (pp_pred, pp_mvar) inline_let_def ctl -> | |
34e49164 C |
78 | |
79 | let rec pp_aux env = function | |
80 | False -> pp "False" | |
81 | | True -> pp "True" | |
82 | | Pred(p) -> pp_pred p | |
83 | | Not(phi) -> | |
84 | pp char_not; Common.pp_do_in_box (fun () -> pp_aux env phi) | |
ae4735db | 85 | | Exists(keep,v,phi) -> |
34e49164 C |
86 | pp "("; |
87 | if keep then pp ("Ex ") else pp ("Ex_ "); | |
88 | pp_mvar v; | |
ae4735db | 89 | pp " . "; |
34e49164 | 90 | print_cut(); |
ae4735db | 91 | Common.pp_do_in_box (fun () -> pp_aux env phi); |
34e49164 C |
92 | pp ")"; |
93 | | AndAny(dir,s,phi1,phi2) -> | |
ae4735db | 94 | pp_2args env (char_and_any^(pp_dirc dir)^(pp_sc s)) phi1 phi2; |
34e49164 | 95 | | HackForStmt(dir,s,phi1,phi2) -> |
ae4735db C |
96 | pp_2args env (char_hack^(pp_dirc dir)^(pp_sc s)) phi1 phi2; |
97 | | And(s,phi1,phi2) -> pp_2args env (char_and^(pp_sc s)) phi1 phi2; | |
98 | | Or(phi1,phi2) -> pp_2args env char_or phi1 phi2; | |
99 | | SeqOr(phi1,phi2) -> pp_2args env char_seqor phi1 phi2; | |
34e49164 | 100 | | Implies(phi1,phi2) -> pp_2args env "=>" phi1 phi2; |
ae4735db C |
101 | | AF(dir,s,phi1) -> pp "AF"; pp_dir dir; pp_s s; pp_arg_paren env phi1; |
102 | | AX(dir,s,phi1) -> pp "AX"; pp_dir dir; pp_s s; pp_arg_paren env phi1; | |
34e49164 C |
103 | | AG(dir,s,phi1) -> pp "AG"; pp_dir dir; pp_s s; pp_arg_paren env phi1; |
104 | | EF(dir,phi1) -> pp "EF"; pp_dir dir; pp_arg_paren env phi1; | |
ae4735db C |
105 | | EX(dir,phi1) -> pp "EX"; pp_dir dir; pp_arg_paren env phi1; |
106 | | EG(dir,phi1) -> pp "EG"; pp_dir dir; pp_arg_paren env phi1; | |
34e49164 | 107 | | AW(dir,s,phi1,phi2) -> |
ae4735db C |
108 | pp "A"; pp_dir dir; pp_s s; pp "["; |
109 | pp_2args_bis env "W" phi1 phi2; | |
110 | pp "]" | |
34e49164 | 111 | | AU(dir,s,phi1,phi2) -> |
ae4735db C |
112 | pp "A"; pp_dir dir; pp_s s; pp "["; |
113 | pp_2args_bis env "U" phi1 phi2; | |
114 | pp "]" | |
34e49164 | 115 | | EU(dir,phi1,phi2) -> |
ae4735db C |
116 | pp "E"; pp_dir dir; pp "["; |
117 | pp_2args_bis env "U" phi1 phi2; | |
118 | pp "]" | |
119 | | Let (x,phi1,phi2) -> | |
34e49164 | 120 | let env' = (x, (Val (phi1,env)))::env in |
ae4735db | 121 | |
34e49164 C |
122 | if not inline_let_def |
123 | then | |
124 | begin | |
125 | pp ("Let"^" "^x); | |
126 | pp " = "; | |
127 | print_cut(); | |
128 | Common.pp_do_in_box (fun () -> pp_aux env phi1); | |
129 | print_space (); | |
ae4735db | 130 | pp "in"; |
34e49164 C |
131 | print_space (); |
132 | end; | |
133 | pp_do_in_zero_box (fun () -> pp_aux env' phi2); | |
ae4735db | 134 | | LetR (dir,x,phi1,phi2) -> |
34e49164 | 135 | let env' = (x, (Val (phi1,env)))::env in |
ae4735db | 136 | |
34e49164 C |
137 | if not inline_let_def |
138 | then | |
139 | begin | |
140 | pp ("LetR"^" "^x); pp_dir dir; | |
141 | pp " = "; | |
142 | print_cut(); | |
143 | Common.pp_do_in_box (fun () -> pp_aux env phi1); | |
144 | print_space (); | |
ae4735db | 145 | pp "in"; |
34e49164 C |
146 | print_space (); |
147 | end; | |
148 | pp_do_in_zero_box (fun () -> pp_aux env' phi2); | |
ae4735db | 149 | | Ref(s) -> |
34e49164 C |
150 | if inline_let_def |
151 | then | |
152 | let Val (phi1,env') = List.assoc s env in | |
153 | pp_aux env' phi1 | |
ae4735db | 154 | else |
34e49164 | 155 | (* pp "Ref("; *) |
ae4735db | 156 | pp s |
34e49164 C |
157 | (* pp ")" *) |
158 | | Uncheck(phi1) -> | |
159 | pp "Uncheck"; pp_arg_paren env phi1 | |
160 | | InnerAnd(phi1) -> | |
161 | pp "InnerAnd"; pp_arg_paren env phi1 | |
162 | | XX _ -> failwith "should be removed" | |
163 | ||
164 | and pp_dir = function | |
165 | FORWARD -> () | |
166 | | BACKWARD -> pp char_back | |
ae4735db | 167 | |
34e49164 C |
168 | and pp_dirc = function |
169 | FORWARD -> "" | |
170 | | BACKWARD -> char_back | |
ae4735db | 171 | |
34e49164 C |
172 | and pp_s = function |
173 | STRICT -> if !Flag_ctl.partial_match then pp "," else () | |
174 | | NONSTRICT -> () | |
ae4735db | 175 | |
34e49164 C |
176 | and pp_sc = function |
177 | STRICT -> "," | |
178 | | NONSTRICT -> "" | |
ae4735db C |
179 | |
180 | and pp_2args env sym phi1 phi2 = | |
34e49164 C |
181 | begin |
182 | pp "("; | |
ae4735db | 183 | Common.pp_do_in_box (fun () -> pp_aux env phi1); |
34e49164 C |
184 | print_space(); |
185 | pp sym; | |
186 | print_space (); | |
187 | Common.pp_do_in_box (fun () -> pp_aux env phi2); | |
188 | pp ")"; | |
189 | end | |
ae4735db | 190 | and pp_2args_bis env sym phi1 phi2 = |
34e49164 | 191 | begin |
ae4735db | 192 | Common.pp_do_in_box (fun () -> pp_aux env phi1); |
34e49164 C |
193 | print_space(); |
194 | pp sym; | |
195 | print_space(); | |
196 | Common.pp_do_in_box (fun () -> pp_aux env phi2); | |
197 | end | |
ae4735db C |
198 | |
199 | and pp_arg_paren env phi = Common.pp_do_in_box (fun () -> | |
34e49164 C |
200 | pp "("; |
201 | pp_aux env phi; | |
202 | pp ")"; | |
ae4735db | 203 | ) |
34e49164 C |
204 | in |
205 | Common.pp_do_in_box (fun () -> pp_aux [] ctl;) |