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