ctl/pretty_print_ctl.ml

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