helm/software/components/ng_paramodulation/pp.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 module Pp (B : Terms.Blob) = struct
  15
  16 (* Main pretty printing functions *)
  17
  18 let pp_foterm ~formatter:f t =
  19   let rec aux ?(toplevel=false) = function
  20     | Terms.Leaf x ->
  21         Format.fprintf f "%s" (B.pp x)
  22     | Terms.Var i ->
  23         Format.fprintf f "?%d" i
  24     | Terms.Node (hd::tl) ->
  25         Format.fprintf f "@[<hov 2>";
  26         if not toplevel then Format.fprintf f "(";
  27         aux hd;
  28         List.iter (fun x -> Format.fprintf f "@;";
  29                      aux x) tl;
  30         if not toplevel then Format.fprintf f ")";
  31         Format.fprintf f "@]"
  32     | _ ->
  33         assert false
  34   in
  35     aux ~toplevel:true t
  36 ;;
  37
  38 let string_of_rule = function
  39   | Terms.Superposition -> "Super"
  40   | Terms.Demodulation ->  "Demod"
  41 ;;
  42
  43 let string_of_direction = function
  44     | Terms.Left2Right -> "Left to right"
  45     | Terms.Right2Left -> "Right to left"
  46     | Terms.Nodir -> "No direction"
  47 ;;
  48
  49 let pp_substitution ~formatter:f subst =
  50   Format.fprintf f "@[<v 2>";
  51   List.iter
  52     (fun (i, t) ->
  53        (Format.fprintf f "?%d -> " i;
  54         pp_foterm f t;
  55         Format.fprintf f "@;"))
  56     subst;
  57   Format.fprintf f "@]";
  58 ;;
  59
  60 let pp_proof bag ~formatter:f p =
  61   let rec aux eq = function
  62     | Terms.Exact t ->
  63         Format.fprintf f "%d: Exact (" eq;
  64         pp_foterm f t;
  65         Format.fprintf f ")@;";
  66     | Terms.Step (rule,eq1,eq2,dir,pos,subst) ->
  67         Format.fprintf f "%d: %s("
  68           eq (string_of_rule rule);
  69         Format.fprintf f "|%d with %d dir %s))" eq1 eq2
  70           (string_of_direction dir);
  71         let (_, _, _, _, proof1),_,_ = Terms.get_from_bag eq1 bag in
  72         let (_, _, _, _, proof2),_,_ = Terms.get_from_bag eq2 bag in
  73           Format.fprintf f "@[<v 2>";
  74           aux eq1 proof1;
  75           aux eq2 proof2;
  76           Format.fprintf f "@]";
  77   in
  78     Format.fprintf f "@[<v>";
  79     aux 0 p;
  80     Format.fprintf f "@]"
  81 ;;
  82
  83 let string_of_comparison = function
  84   | Terms.Lt -> "=<="
  85   | Terms.Gt -> "=>="
  86   | Terms.Eq -> "==="
  87   | Terms.Incomparable -> "=?="
  88   | Terms.Invertible -> "=<->="
  89
  90 let pp_literal ~formatter:f l =
  91     match l with
  92       | Terms.Predicate t,sel ->
  93           Format.fprintf f "@[<hv>{";
  94           if sel then Format.fprintf f "*";
  95           pp_foterm f t;
  96           if sel then Format.fprintf f "*";
  97           Format.fprintf f "}@;"
  98       | Terms.Equation (lhs, rhs, ty, comp),sel ->
  99           Format.fprintf f "@[<hv>{";
 100           if sel then Format.fprintf f "*";
 101           pp_foterm f ty;
 102           Format.fprintf f "}:@;@[<hv>";
 103           pp_foterm f lhs;
 104           Format.fprintf f "@;%s@;" (string_of_comparison comp);
 105           pp_foterm f rhs;
 106           if sel then Format.fprintf f "*";
 107           Format.fprintf f "@]@;"
 108 ;;
 109
 110 let pp_unit_clause ~formatter:f c =
 111   let (id, l, vars, proof) = c in
 112     Format.fprintf f "Id : %3d, " id ;
 113     match l with
 114       | Terms.Predicate t ->
 115           Format.fprintf f "@[<hv>{";
 116           pp_foterm f t;
 117           Format.fprintf f "@;[%s] by "
 118             (String.concat ", " (List.map string_of_int vars));
 119           (match proof with
 120            | Terms.Exact t -> pp_foterm f t
 121            | Terms.Step (rule, id1, id2, _, p, _) ->
 122                Format.fprintf f "%s %d with %d at %s"
 123                  (string_of_rule rule) id1 id2 (String.concat
 124                   "," (List.map string_of_int p)));
 125           Format.fprintf f "@]"
 126       | Terms.Equation (lhs, rhs, ty, comp) ->
 127           Format.fprintf f "@[<hv>{";
 128           pp_foterm f ty;
 129           Format.fprintf f "}:@;@[<hv>";
 130           pp_foterm f lhs;
 131           Format.fprintf f "@;%s@;" (string_of_comparison comp);
 132           pp_foterm f rhs;
 133           Format.fprintf f "@]@;[%s] by "
 134             (String.concat ", " (List.map string_of_int vars));
 135           (match proof with
 136            | Terms.Exact t -> pp_foterm f t
 137            | Terms.Step (rule, id1, id2, _, p, _) ->
 138                Format.fprintf f "%s %d with %d at %s"
 139                  (string_of_rule rule) id1 id2 (String.concat
 140                   "," (List.map string_of_int p)));
 141            Format.fprintf f "@]"
 142 ;;
 143
 144 let pp_clause ~formatter:f c =
 145    let (id, nlit, plit, vars, proof) = c in
 146     Format.fprintf f "Id : %3d, " id ;
 147     let pr_literals l =
 148       if l <> [] then begin
 149         pp_literal f (List.hd l);
 150         List.iter (fun lit -> Format.fprintf f "\\/"; pp_literal f lit) (List.tl l);
 151       end
 152     in
 153     pr_literals nlit;
 154     Format.fprintf f " -> ";
 155     pr_literals plit;
 156     Format.fprintf f "[%s] by " (String.concat ", " (List.map string_of_int vars));
 157     match proof with
 158       | Terms.Exact t -> pp_foterm f t
 159       | Terms.Step (rule, id1, id2, _, p, _) ->
 160            Format.fprintf f "%s %d with %d at %s"
 161              (string_of_rule rule) id1 id2 (String.concat
 162              "," (List.map string_of_int p))
 163 ;;
 164
 165 let pp_bag ~formatter:f (_,bag) =
 166   Format.fprintf f "@[<v>";
 167   Terms.M.iter
 168   (fun _ (c,d,_) -> pp_clause ~formatter:f c;
 169      if d then Format.fprintf f " (discarded)@;"
 170      else Format.fprintf f "@;") bag;
 171   Format.fprintf f "@]"
 172 ;;
 173
 174 (* String buffer implementation *)
 175 let on_buffer ?(margin=80) f t =
 176   let buff = Buffer.create 100 in
 177   let formatter = Format.formatter_of_buffer buff in
 178   Format.pp_set_margin formatter margin;
 179   f ~formatter:formatter t;
 180   Format.fprintf formatter "@?";
 181   Buffer.contents buff
 182 ;;
 183
 184 let pp_bag =
 185   on_buffer pp_bag
 186 ;;
 187
 188 let pp_foterm =
 189  on_buffer pp_foterm
 190 ;;
 191
 192 let pp_substitution =
 193   on_buffer pp_substitution
 194 ;;
 195
 196 let pp_proof bag =
 197   on_buffer (pp_proof bag)
 198 ;;
 199
 200 let pp_unit_clause ?margin x=
 201   on_buffer ?margin pp_unit_clause x
 202 ;;
 203
 204 let pp_clause ?margin x =
 205   on_buffer ?margin pp_clause x
 206 ;;
 207
 208 end