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