matita/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 let string_of_comparison = function
  15   | Terms.Lt -> "=<="
  16   | Terms.Gt -> "=>="
  17   | Terms.Eq -> "==="
  18   | Terms.Incomparable -> "=?="
  19   | Terms.Invertible -> "=<->="
  20
  21 module Pp (B : Terms.Blob) = struct
  22
  23 (* Main pretty printing functions *)
  24
  25 let pp_foterm ~formatter:f t =
  26   let rec aux ?(toplevel=false) = function
  27     | Terms.Leaf x ->
  28         Format.fprintf f "%s" (B.pp x)
  29     | Terms.Var i ->
  30         Format.fprintf f "?%d" i
  31     | Terms.Node (hd::tl) ->
  32         Format.fprintf f "@[<hov 2>";
  33         if not toplevel then Format.fprintf f "(";
  34         aux hd;
  35         List.iter (fun x -> Format.fprintf f "@;";
  36                      aux x) tl;
  37         if not toplevel then Format.fprintf f ")";
  38         Format.fprintf f "@]"
  39     | _ ->
  40         assert false
  41   in
  42     aux ~toplevel:true t
  43 ;;
  44
  45 let string_of_rule = function
  46   | Terms.Superposition -> "Super"
  47   | Terms.Demodulation ->  "Demod"
  48 ;;
  49
  50 let string_of_direction = function
  51     | Terms.Left2Right -> "Left to right"
  52     | Terms.Right2Left -> "Right to left"
  53     | Terms.Nodir -> "No direction"
  54 ;;
  55
  56 let pp_substitution ~formatter:f subst =
  57   Format.fprintf f "@[<v 2>";
  58   List.iter
  59     (fun (i, t) ->
  60        (Format.fprintf f "?%d -> " i;
  61         pp_foterm f t;
  62         Format.fprintf f "@;"))
  63     subst;
  64   Format.fprintf f "@]";
  65 ;;
  66
  67 let pp_proof bag ~formatter:f p =
  68   let rec aux eq = function
  69     | Terms.Exact t ->
  70         Format.fprintf f "%d: Exact (" eq;
  71         pp_foterm f t;
  72         Format.fprintf f ")@;";
  73     | Terms.Step (rule,eq1,eq2,dir,_pos,_subst) ->
  74         Format.fprintf f "%d: %s("
  75           eq (string_of_rule rule);
  76         Format.fprintf f "|%d with %d dir %s))" eq1 eq2
  77           (string_of_direction dir);
  78         let (_, _, _, proof1),_,_ = Terms.get_from_bag eq1 bag in
  79         let (_, _, _, proof2),_,_ = Terms.get_from_bag eq2 bag in
  80           Format.fprintf f "@[<v 2>";
  81           aux eq1 proof1;
  82           aux eq2 proof2;
  83           Format.fprintf f "@]";
  84   in
  85     Format.fprintf f "@[<v>";
  86     aux 0 p;
  87     Format.fprintf f "@]"
  88 ;;
  89
  90 let pp_unit_clause ~formatter:f c =
  91   let (id, l, vars, proof) = c in
  92     Format.fprintf f "Id : %3d, " id ;
  93     match l with
  94       | Terms.Predicate t ->
  95           Format.fprintf f "@[<hv>{";
  96           pp_foterm f t;
  97           Format.fprintf f "@;[%s] by "
  98             (String.concat ", " (List.map string_of_int vars));
  99           (match proof with
 100            | Terms.Exact t -> pp_foterm f t
 101            | Terms.Step (rule, id1, id2, _, p, _) ->
 102                Format.fprintf f "%s %d with %d at %s"
 103                  (string_of_rule rule) id1 id2 (String.concat
 104                   "," (List.map string_of_int p)));
 105           Format.fprintf f "@]"
 106       | Terms.Equation (lhs, rhs, ty, comp) ->
 107           Format.fprintf f "@[<hv>{";
 108           pp_foterm f ty;
 109           Format.fprintf f "}:@;@[<hv>";
 110           pp_foterm f lhs;
 111           Format.fprintf f "@;%s@;" (string_of_comparison comp);
 112           pp_foterm f rhs;
 113           Format.fprintf f "@]@;[%s] by "
 114             (String.concat ", " (List.map string_of_int vars));
 115           (match proof with
 116            | Terms.Exact t -> pp_foterm f t
 117            | Terms.Step (rule, id1, id2, _, p, _) ->
 118                Format.fprintf f "%s %d with %d at %s"
 119                  (string_of_rule rule) id1 id2 (String.concat
 120                   "," (List.map string_of_int p)));
 121           Format.fprintf f "@]"
 122 ;;
 123
 124 let pp_bag ~formatter:f (_,bag) =
 125   Format.fprintf f "@[<v>";
 126   Terms.M.iter
 127   (fun _ (c,d,_) -> pp_unit_clause ~formatter:f c;
 128      if d then Format.fprintf f " (discarded)@;"
 129      else Format.fprintf f "@;") bag;
 130   Format.fprintf f "@]"
 131 ;;
 132
 133 (* String buffer implementation *)
 134 let on_buffer ?(margin=80) f t =
 135   let buff = Buffer.create 100 in
 136   let formatter = Format.formatter_of_buffer buff in
 137   Format.pp_set_margin formatter margin;
 138   f ~formatter:formatter t;
 139   Format.fprintf formatter "@?";
 140   Buffer.contents buff
 141 ;;
 142
 143 let pp_bag =
 144   on_buffer pp_bag
 145 ;;
 146
 147 let pp_foterm =
 148  on_buffer pp_foterm
 149 ;;
 150
 151 let pp_substitution =
 152   on_buffer pp_substitution
 153 ;;
 154
 155 let pp_proof bag =
 156   on_buffer (pp_proof bag)
 157 ;;
 158
 159 let pp_unit_clause ?margin x=
 160   on_buffer ?margin pp_unit_clause x
 161 ;;
 162
 163 end