6 (* todo?: a txt_to_latex, that use Format to compute the good space but
7 * then generate latex to better output.
11 let char_and_any = "&+"
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
30 ('pred
-> unit) * ('mvar
-> unit) -> bool ->
31 ('pred
, 'mvar
, 'info
) generic_ctl
->
33 fun (pp_pred
, pp_mvar
) inline_let_def ctl
->
35 let rec pp_aux env
= function
38 | Pred
(p
) -> pp_pred p
40 pp
char_not; Common.pp_do_in_box
(fun () -> pp_aux env phi
)
41 | Exists
(keep
,v
,phi
) ->
43 if keep
then pp
("Ex ") else pp
("Ex_ ");
47 Common.pp_do_in_box
(fun () -> pp_aux env phi
);
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
;
67 | AU
(dir
,s
,phi1
,phi2
) ->
68 pp
"A"; pp_dir dir
; pp_s s
; pp
"[";
69 pp_2args_bis env
"U" phi1 phi2
;
71 | EU
(dir
,phi1
,phi2
) ->
72 pp
"E"; pp_dir dir
; pp
"[";
73 pp_2args_bis env
"U" phi1 phi2
;
75 | Let
(x
,phi1
,phi2
) ->
76 let env'
= (x
, (Val
(phi1
,env)))::env in
84 Common.pp_do_in_box
(fun () -> pp_aux env phi1
);
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
96 pp
("LetR"^
" "^x
); pp_dir dir
;
99 Common.pp_do_in_box
(fun () -> pp_aux env phi1
);
104 pp_do_in_zero_box
(fun () -> pp_aux env' phi2
);
108 let Val (phi1
,env'
) = List.assoc s
env in
115 pp
"Uncheck"; pp_arg_paren
env phi1
117 pp
"InnerAnd"; pp_arg_paren
env phi1
118 | XX _
-> failwith
"should be removed"
120 and pp_dir
= function
122 | BACKWARD
-> pp
char_back
124 and pp_dirc
= function
126 | BACKWARD
-> char_back
129 STRICT
-> if !Flag_ctl.partial_match
then pp
"," else ()
136 and pp_2args
env sym phi1 phi2
=
139 Common.pp_do_in_box
(fun () -> pp_aux env phi1
);
143 Common.pp_do_in_box
(fun () -> pp_aux env phi2
);
146 and pp_2args_bis
env sym phi1 phi2
=
148 Common.pp_do_in_box
(fun () -> pp_aux env phi1
);
152 Common.pp_do_in_box
(fun () -> pp_aux env phi2
);
155 and pp_arg_paren
env phi
= Common.pp_do_in_box
(fun () ->
161 Common.pp_do_in_box
(fun () -> pp_aux [] ctl
;)