From f59b591eb48a06518b34d7f809bee51989307404 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 23 Mar 2010 15:45:06 +0000 Subject: [PATCH] "flat" function (subst unfolding) From: asperti --- helm/software/components/ng_paramodulation/foSubst.ml | 4 ++++ helm/software/components/ng_paramodulation/foSubst.mli | 2 ++ 2 files changed, 6 insertions(+) diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml index 2d63d34af..aab240168 100644 --- a/helm/software/components/ng_paramodulation/foSubst.ml +++ b/helm/software/components/ng_paramodulation/foSubst.ml @@ -57,6 +57,10 @@ Terms.Node (List.map (fun t -> apply_subst subst t) l) ;; + let flat subst = + List.map (fun (x,t) -> (x, apply_subst subst t)) subst +;; + let concat x y = x @ y;; (* end *) diff --git a/helm/software/components/ng_paramodulation/foSubst.mli b/helm/software/components/ng_paramodulation/foSubst.mli index 29516c57f..36a4c12ea 100644 --- a/helm/software/components/ng_paramodulation/foSubst.mli +++ b/helm/software/components/ng_paramodulation/foSubst.mli @@ -26,6 +26,8 @@ module Subst (B : Terms.Blob) : 'a Terms.substitution -> 'a Terms.foterm -> 'a Terms.foterm val apply_subst : 'a Terms.substitution -> 'a Terms.foterm -> 'a Terms.foterm + val flat: + 'a Terms.substitution -> 'a Terms.substitution val concat: 'a Terms.substitution -> 'a Terms.substitution -> 'a Terms.substitution -- 2.39.2