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