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