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