From: denes Date: Thu, 4 Jun 2009 13:57:56 +0000 (+0000) Subject: First pretty printing functions X-Git-Tag: make_still_working~3921 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=497563d35f24bbcbcbd8d669d73284b76a823118;p=helm.git First pretty printing functions --- diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index d663e8155..9dac9001b 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -13,9 +13,116 @@ module Pp (B : Terms.Blob) = struct - let pp_foterm = assert false - let pp_proof = assert false - let pp_substitution = assert false - let pp_unit_clause = assert false - +(* Main pretty printing functions *) + +let pp_foterm ~formatter:f t = + let rec aux ?(toplevel=false) = function + | Terms.Leaf x -> + Format.fprintf f "%s" (B.pp x) + | Terms.Var i -> + Format.fprintf f "?%d" i + | Terms.Node (hd::tl) -> + Format.fprintf f "@["; + if not toplevel then Format.fprintf f "("; + aux hd; + List.iter (fun x -> Format.fprintf f "@;"; + aux x) tl; + if not toplevel then Format.fprintf f ")"; + Format.fprintf f "@]" + | _ -> + assert false + in + aux ~toplevel:true t +;; + +let string_of_rule = function + | Terms.SuperpositionRight -> "SupR" + | Terms.SuperpositionLeft -> "SupL" + | Terms.Demodulation -> "Demod" +;; + +let string_of_direction = function + | Terms.Left2Right -> "Left to right" + | Terms.Right2Left -> "Right to left" + | Terms.Nodir -> "No direction" +;; + +let pp_substitution ~formatter:f subst = + (List.iter + (fun (i, t) -> + (Format.fprintf f "?%d -> " i; + pp_foterm f t) + ) + subst) +;; + +let pp_proof bag ~formatter:f p = + let rec aux eq = function + | Terms.Exact t -> + Format.fprintf f "%d: Exact (%s)@;" eq (B.pp t) + | Terms.Step (rule,eq1,eq2,dir,pos,subst) -> + Format.fprintf f "%d: %s(" + eq (string_of_rule rule); + Format.fprintf f "|%d with %d dir %s))" eq1 eq2 + (string_of_direction dir); + let (_, _, _, proof1) = Terms.M.find eq1 bag in + let (_, _, _, proof2) = Terms.M.find eq2 bag in + Format.fprintf f "@["; + aux eq1 proof1; + aux eq2 proof2; + Format.fprintf f "@]"; + in + Format.fprintf f "@["; + aux 0 p; + Format.fprintf f "@]" +;; + +let string_of_comparison = function + | Terms.Lt -> "<" + | Terms.Gt -> ">" + | Terms.Eq -> "=" + | Terms.Incomparable -> "I" + +let pp_unit_clause ~formatter:f c = + let (id, l, vars, _) = c in + Format.fprintf f "Id : %d, " id ; + match l with + | Terms.Predicate t -> + pp_foterm f t + | Terms.Equation (lhs, rhs, ty, comp) -> + Format.fprintf f "{"; + pp_foterm f ty; + Format.fprintf f "}: "; + pp_foterm f lhs; + Format.fprintf f " =(%s) " (string_of_comparison comp); + pp_foterm f rhs; + Format.fprintf f " [%s]" + (String.concat ", " (List.map string_of_int vars)) +;; + +(* String buffer implementation *) +let on_buffer f t = + let buff = Buffer.create 100 in + let formatter = Format.formatter_of_buffer buff in + f ~formatter:formatter t; + Format.fprintf formatter "@?"; + Buffer.contents buff +;; + +let pp_foterm = + on_buffer pp_foterm +;; + +let pp_substitution = + on_buffer pp_substitution +;; + +let pp_proof bag = + on_buffer (pp_proof bag) +;; + +let pp_unit_clause = + on_buffer pp_unit_clause +;; + end