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