File: pretty_print_ctl.ml

package info (click to toggle)
coccinelle 1.0.8.deb-5
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid
  • size: 26,148 kB
  • sloc: ml: 136,392; ansic: 23,594; sh: 2,189; makefile: 2,157; perl: 1,576; lisp: 840; python: 823; awk: 70; csh: 12
file content (167 lines) | stat: -rw-r--r-- 4,900 bytes parent folder | download
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;)