From: Alberto Griggio Date: Fri, 13 May 2005 09:05:27 +0000 (+0000) Subject: moved string_of_equality into utils X-Git-Tag: single_binding~79 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6cce91267c785d7790e9377717a13d0546bb68e1;p=helm.git moved string_of_equality into utils --- diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 405ba15a6..6508e75da 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -15,24 +15,6 @@ let string_of_sign = function ;; -let string_of_equality ?env = - match env with - | None -> ( - function - | _, (ty, left, right), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty) - (CicPp.ppterm left) (CicPp.ppterm right) - ) - | Some (_, context, _) -> ( - let names = names_of_context context in - function - | _, (ty, left, right), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names) - (CicPp.pp left names) (CicPp.pp right names) - ) -;; - - module OrderedEquality = struct type t = Inference.equality diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 01293a958..8d97e0c4b 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -287,3 +287,22 @@ let names_of_context context = context ;; + +let string_of_equality ?env = + match env with + | None -> ( + function + | _, (ty, left, right), _, _ -> + Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty) + (CicPp.ppterm left) (CicPp.ppterm right) + ) + | Some (_, context, _) -> ( + let names = names_of_context context in + function + | _, (ty, left, right), _, _ -> + Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names) + (CicPp.pp left names) (CicPp.pp right names) + ) +;; + + diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 471e6e307..164d4f303 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -19,6 +19,9 @@ val compare_weights: ?normalize:bool -> weight -> weight -> comparison val nonrec_kbo: Cic.term -> Cic.term -> comparison +val string_of_equality: + ?env:Inference.environment -> Inference.equality -> string + val nonrec_kbo_w: (Cic.term * weight) -> (Cic.term * weight) -> comparison val names_of_context: Cic.context -> (Cic.name option) list