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.SuperpositionRight -> "SupR"
  40   | Terms.SuperpositionLeft -> "SupL"
  41   | Terms.Demodulation -> "Demod"
  42 ;;
  43
  44 let string_of_direction = function
  45     | Terms.Left2Right -> "Left to right"
  46     | Terms.Right2Left -> "Right to left"
  47     | Terms.Nodir -> "No direction"
  48 ;;
  49
  50 let pp_substitution ~formatter:f subst =
  51      (List.iter
  52        (fun (i, t) ->
  53           (Format.fprintf f "?%d -> " i;
  54            pp_foterm f t)
  55        )
  56        subst)
  57 ;;
  58
  59 let pp_proof bag ~formatter:f p =
  60   let rec aux eq = function
  61     | Terms.Exact t ->
  62         Format.fprintf f "%d: Exact (" eq;
  63         pp_foterm f t;
  64         Format.fprintf f ")@;";
  65     | Terms.Step (rule,eq1,eq2,dir,pos,subst) ->
  66         Format.fprintf f "%d: %s("
  67           eq (string_of_rule rule);
  68         Format.fprintf f "|%d with %d dir %s))" eq1 eq2
  69           (string_of_direction dir);
  70         let (_, _, _, proof1) = Terms.M.find eq1 bag in
  71         let (_, _, _, proof2) = Terms.M.find eq2 bag in
  72           Format.fprintf f "@[<v 2>";
  73           aux eq1 proof1;
  74           aux eq2 proof2;
  75           Format.fprintf f "@]";
  76   in
  77     Format.fprintf f "@[<v>";
  78     aux 0 p;
  79     Format.fprintf f "@]"
  80 ;;
  81
  82 let string_of_comparison = function
  83   | Terms.Lt -> "<"
  84   | Terms.Gt -> ">"
  85   | Terms.Eq -> "="
  86   | Terms.Incomparable -> "I"
  87
  88 let pp_unit_clause ~formatter:f c =
  89   let (id, l, vars, _) = c in
  90     Format.fprintf f "Id : %d, " id ;
  91     match l with
  92       | Terms.Predicate t ->
  93           pp_foterm f t
  94       | Terms.Equation (lhs, rhs, ty, comp) ->
  95           Format.fprintf f "{";
  96           pp_foterm f ty;
  97           Format.fprintf f "}: ";
  98           pp_foterm f lhs;
  99           Format.fprintf f " =(%s) " (string_of_comparison comp);
 100           pp_foterm f rhs;
 101           Format.fprintf f " [%s]"
 102             (String.concat ", " (List.map string_of_int vars))
 103 ;;
 104
 105 (* String buffer implementation *)
 106 let on_buffer f t =
 107   let buff = Buffer.create 100 in
 108   let formatter = Format.formatter_of_buffer buff in
 109   f ~formatter:formatter t;
 110   Format.fprintf formatter "@?";
 111   Buffer.contents buff
 112 ;;
 113
 114 let pp_foterm =
 115  on_buffer pp_foterm
 116 ;;
 117
 118 let pp_substitution =
 119   on_buffer pp_substitution
 120 ;;
 121
 122 let pp_proof bag =
 123   on_buffer (pp_proof bag)
 124 ;;
 125
 126 let pp_unit_clause =
 127   on_buffer pp_unit_clause
 128 ;;
 129
 130 end