ctl/pretty_print_ctl.ml

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