Commit | Line | Data |
---|---|---|
9f8e26f4 C |
1 | (* |
2 | * Copyright 2005-2009, 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 | ||
34e49164 C |
23 | open Common |
24 | open Format | |
25 | ||
26 | open Ast_ctl | |
27 | ||
28 | (* todo?: a txt_to_latex, that use Format to compute the good space but | |
29 | * then generate latex to better output. | |
30 | *) | |
31 | ||
32 | let char_and = "&" | |
33 | let char_and_any = "&+" | |
34 | let char_hack = "&h+" | |
35 | let char_or = "v" | |
36 | let char_seqor = "|" | |
37 | let char_not = "!" | |
38 | let char_back = "^" | |
39 | ||
40 | (* | |
41 | let char_and = "/\\" | |
42 | let char_or = "\\/" | |
43 | let char_not = "-|" | |
44 | *) | |
45 | ||
46 | (* need introduce the Val constructor, or use -rectype. *) | |
47 | type ('a,'b,'c) environment = (string, ('a,'b,'c) binding_val) Common.assoc | |
48 | and ('a, 'b, 'c) binding_val = | |
49 | Val of ('a,'b,'c) generic_ctl * ('a,'b,'c) environment | |
50 | ||
51 | let rec (pp_ctl: | |
52 | ('pred -> unit) * ('mvar -> unit) -> bool -> | |
53 | ('pred, 'mvar, 'info) generic_ctl -> | |
54 | unit) = | |
55 | fun (pp_pred, pp_mvar) inline_let_def ctl -> | |
56 | ||
57 | let rec pp_aux env = function | |
58 | False -> pp "False" | |
59 | | True -> pp "True" | |
60 | | Pred(p) -> pp_pred p | |
61 | | Not(phi) -> | |
62 | pp char_not; Common.pp_do_in_box (fun () -> pp_aux env phi) | |
63 | | Exists(keep,v,phi) -> | |
64 | pp "("; | |
65 | if keep then pp ("Ex ") else pp ("Ex_ "); | |
66 | pp_mvar v; | |
67 | pp " . "; | |
68 | print_cut(); | |
69 | Common.pp_do_in_box (fun () -> pp_aux env phi); | |
70 | pp ")"; | |
71 | | AndAny(dir,s,phi1,phi2) -> | |
72 | pp_2args env (char_and_any^(pp_dirc dir)^(pp_sc s)) phi1 phi2; | |
73 | | HackForStmt(dir,s,phi1,phi2) -> | |
74 | pp_2args env (char_hack^(pp_dirc dir)^(pp_sc s)) phi1 phi2; | |
75 | | And(s,phi1,phi2) -> pp_2args env (char_and^(pp_sc s)) phi1 phi2; | |
76 | | Or(phi1,phi2) -> pp_2args env char_or phi1 phi2; | |
77 | | SeqOr(phi1,phi2) -> pp_2args env char_seqor phi1 phi2; | |
78 | | Implies(phi1,phi2) -> pp_2args env "=>" phi1 phi2; | |
79 | | AF(dir,s,phi1) -> pp "AF"; pp_dir dir; pp_s s; pp_arg_paren env phi1; | |
80 | | AX(dir,s,phi1) -> pp "AX"; pp_dir dir; pp_s s; pp_arg_paren env phi1; | |
81 | | AG(dir,s,phi1) -> pp "AG"; pp_dir dir; pp_s s; pp_arg_paren env phi1; | |
82 | | EF(dir,phi1) -> pp "EF"; pp_dir dir; pp_arg_paren env phi1; | |
83 | | EX(dir,phi1) -> pp "EX"; pp_dir dir; pp_arg_paren env phi1; | |
84 | | EG(dir,phi1) -> pp "EG"; pp_dir dir; pp_arg_paren env phi1; | |
85 | | AW(dir,s,phi1,phi2) -> | |
86 | pp "A"; pp_dir dir; pp_s s; pp "["; | |
87 | pp_2args_bis env "W" phi1 phi2; | |
88 | pp "]" | |
89 | | AU(dir,s,phi1,phi2) -> | |
90 | pp "A"; pp_dir dir; pp_s s; pp "["; | |
91 | pp_2args_bis env "U" phi1 phi2; | |
92 | pp "]" | |
93 | | EU(dir,phi1,phi2) -> | |
94 | pp "E"; pp_dir dir; pp "["; | |
95 | pp_2args_bis env "U" phi1 phi2; | |
96 | pp "]" | |
97 | | Let (x,phi1,phi2) -> | |
98 | let env' = (x, (Val (phi1,env)))::env in | |
99 | ||
100 | if not inline_let_def | |
101 | then | |
102 | begin | |
103 | pp ("Let"^" "^x); | |
104 | pp " = "; | |
105 | print_cut(); | |
106 | Common.pp_do_in_box (fun () -> pp_aux env phi1); | |
107 | print_space (); | |
108 | pp "in"; | |
109 | print_space (); | |
110 | end; | |
111 | pp_do_in_zero_box (fun () -> pp_aux env' phi2); | |
112 | | LetR (dir,x,phi1,phi2) -> | |
113 | let env' = (x, (Val (phi1,env)))::env in | |
114 | ||
115 | if not inline_let_def | |
116 | then | |
117 | begin | |
118 | pp ("LetR"^" "^x); pp_dir dir; | |
119 | pp " = "; | |
120 | print_cut(); | |
121 | Common.pp_do_in_box (fun () -> pp_aux env phi1); | |
122 | print_space (); | |
123 | pp "in"; | |
124 | print_space (); | |
125 | end; | |
126 | pp_do_in_zero_box (fun () -> pp_aux env' phi2); | |
127 | | Ref(s) -> | |
128 | if inline_let_def | |
129 | then | |
130 | let Val (phi1,env') = List.assoc s env in | |
131 | pp_aux env' phi1 | |
132 | else | |
133 | (* pp "Ref("; *) | |
134 | pp s | |
135 | (* pp ")" *) | |
136 | | Uncheck(phi1) -> | |
137 | pp "Uncheck"; pp_arg_paren env phi1 | |
138 | | InnerAnd(phi1) -> | |
139 | pp "InnerAnd"; pp_arg_paren env phi1 | |
140 | | XX _ -> failwith "should be removed" | |
141 | ||
142 | and pp_dir = function | |
143 | FORWARD -> () | |
144 | | BACKWARD -> pp char_back | |
145 | ||
146 | and pp_dirc = function | |
147 | FORWARD -> "" | |
148 | | BACKWARD -> char_back | |
149 | ||
150 | and pp_s = function | |
151 | STRICT -> if !Flag_ctl.partial_match then pp "," else () | |
152 | | NONSTRICT -> () | |
153 | ||
154 | and pp_sc = function | |
155 | STRICT -> "," | |
156 | | NONSTRICT -> "" | |
157 | ||
158 | and pp_2args env sym phi1 phi2 = | |
159 | begin | |
160 | pp "("; | |
161 | Common.pp_do_in_box (fun () -> pp_aux env phi1); | |
162 | print_space(); | |
163 | pp sym; | |
164 | print_space (); | |
165 | Common.pp_do_in_box (fun () -> pp_aux env phi2); | |
166 | pp ")"; | |
167 | end | |
168 | and pp_2args_bis env sym phi1 phi2 = | |
169 | begin | |
170 | Common.pp_do_in_box (fun () -> pp_aux env phi1); | |
171 | print_space(); | |
172 | pp sym; | |
173 | print_space(); | |
174 | Common.pp_do_in_box (fun () -> pp_aux env phi2); | |
175 | end | |
176 | ||
177 | and pp_arg_paren env phi = Common.pp_do_in_box (fun () -> | |
178 | pp "("; | |
179 | pp_aux env phi; | |
180 | pp ")"; | |
181 | ) | |
182 | in | |
183 | Common.pp_do_in_box (fun () -> pp_aux [] ctl;) |