From 8d2bb0ddcf3d83b4dd54fa3ec6dff50d89f6d93d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 9 Jul 2020 07:44:07 -0700 Subject: [PATCH] [sledge] Refactor: Move Ses.Term.Var.Subst to Fol.Var.Subst Summary: The `Subst` module is not used by `Ses`, so move it out of the Ses-internal APIs. Reviewed By: ngorogiannis Differential Revision: D22170513 fbshipit-source-id: a189a1440 --- sledge/src/fol.ml | 81 ++++++++++++++++++++++++++++++++++++++++- sledge/src/ses/term.ml | 74 ------------------------------------- sledge/src/ses/term.mli | 23 +++--------- 3 files changed, 84 insertions(+), 94 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 83a38d918..a452d1046 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -5,10 +5,87 @@ * LICENSE file in the root directory of this source tree. *) -module Var = Ses.Term.Var +module Var = struct + include Ses.Term.Var + + (** Variable renaming substitutions *) + module Subst = struct + type nonrec t = t Map.t [@@deriving compare, equal, sexp_of] + type x = {sub: t; dom: Set.t; rng: Set.t} + + let t_of_sexp = Map.t_of_sexp t_of_sexp + + let invariant s = + let@ () = Invariant.invariant [%here] s [%sexp_of: t] in + let domain, range = + Map.fold s ~init:(Set.empty, Set.empty) + ~f:(fun ~key ~data (domain, range) -> + (* substs are injective *) + assert (not (Set.mem range data)) ; + (Set.add domain key, Set.add range data) ) + in + assert (Set.disjoint domain range) + + let pp = Map.pp pp pp + let empty = Map.empty + let is_empty = Map.is_empty + + let freshen vs ~wrt = + let dom = Set.inter wrt vs in + ( if Set.is_empty dom then + ({sub= empty; dom= Set.empty; rng= Set.empty}, wrt) + else + let wrt = Set.union wrt vs in + let sub, rng, wrt = + Set.fold dom ~init:(empty, Set.empty, wrt) + ~f:(fun (sub, rng, wrt) x -> + let x', wrt = fresh (name x) ~wrt in + let sub = Map.add_exn sub ~key:x ~data:x' in + let rng = Set.add rng x' in + (sub, rng, wrt) ) + in + ({sub; dom; rng}, wrt) ) + |> check (fun ({sub; _}, _) -> invariant sub) + + let fold sub ~init ~f = + Map.fold sub ~init ~f:(fun ~key ~data s -> f key data s) + + let domain sub = + Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain -> + Set.add domain key ) + + let range sub = + Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range -> + Set.add range data ) + + let invert sub = + Map.fold sub ~init:empty ~f:(fun ~key ~data sub' -> + Map.add_exn sub' ~key:data ~data:key ) + |> check invariant + + let restrict sub vs = + Map.fold sub ~init:{sub; dom= Set.empty; rng= Set.empty} + ~f:(fun ~key ~data z -> + if Set.mem vs key then + {z with dom= Set.add z.dom key; rng= Set.add z.rng data} + else ( + assert ( + (* all substs are injective, so the current mapping is the + only one that can cause [data] to be in [rng] *) + (not (Set.mem (range (Map.remove sub key)) data)) + || violates invariant sub ) ; + {z with sub= Map.remove z.sub key} ) ) + |> check (fun {sub; dom; rng} -> + assert (Set.equal dom (domain sub)) ; + assert (Set.equal rng (range sub)) ) + + let apply sub v = Map.find sub v |> Option.value ~default:v + end +end module Term = struct - include Ses.Term + include ( + Ses.Term : module type of Ses.Term with module Var := Ses.Term.Var ) let ite = conditional let rename s e = rename (Var.Subst.apply s) e diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml index 50952d95c..f1a013b1b 100644 --- a/sledge/src/ses/term.ml +++ b/sledge/src/ses/term.ml @@ -1062,80 +1062,6 @@ module Var = struct let of_regs = Llair.Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r)) end - - (** Variable renaming substitutions *) - module Subst = struct - type t = T.t Map.t [@@deriving compare, equal, sexp_of] - type x = {sub: t; dom: Set.t; rng: Set.t} - - let t_of_sexp = Map.t_of_sexp T.t_of_sexp - - let invariant s = - let@ () = Invariant.invariant [%here] s [%sexp_of: t] in - let domain, range = - Map.fold s ~init:(Set.empty, Set.empty) - ~f:(fun ~key ~data (domain, range) -> - (* substs are injective *) - assert (not (Set.mem range data)) ; - (Set.add domain key, Set.add range data) ) - in - assert (Set.disjoint domain range) - - let pp = Map.pp pp_t pp_t - let empty = Map.empty - let is_empty = Map.is_empty - - let freshen vs ~wrt = - let dom = Set.inter wrt vs in - ( if Set.is_empty dom then - ({sub= empty; dom= Set.empty; rng= Set.empty}, wrt) - else - let wrt = Set.union wrt vs in - let sub, rng, wrt = - Set.fold dom ~init:(empty, Set.empty, wrt) - ~f:(fun (sub, rng, wrt) x -> - let x', wrt = fresh (name x) ~wrt in - let sub = Map.add_exn sub ~key:x ~data:x' in - let rng = Set.add rng x' in - (sub, rng, wrt) ) - in - ({sub; dom; rng}, wrt) ) - |> check (fun ({sub; _}, _) -> invariant sub) - - let fold sub ~init ~f = - Map.fold sub ~init ~f:(fun ~key ~data s -> f key data s) - - let domain sub = - Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain -> - Set.add domain key ) - - let range sub = - Map.fold sub ~init:Set.empty ~f:(fun ~key:_ ~data range -> - Set.add range data ) - - let invert sub = - Map.fold sub ~init:empty ~f:(fun ~key ~data sub' -> - Map.add_exn sub' ~key:data ~data:key ) - |> check invariant - - let restrict sub vs = - Map.fold sub ~init:{sub; dom= Set.empty; rng= Set.empty} - ~f:(fun ~key ~data z -> - if Set.mem vs key then - {z with dom= Set.add z.dom key; rng= Set.add z.rng data} - else ( - assert ( - (* all substs are injective, so the current mapping is the - only one that can cause [data] to be in [rng] *) - (not (Set.mem (range (Map.remove sub key)) data)) - || violates invariant sub ) ; - {z with sub= Map.remove z.sub key} ) ) - |> check (fun {sub; dom; rng} -> - assert (Set.equal dom (domain sub)) ; - assert (Set.equal rng (range sub)) ) - - let apply sub v = Map.find sub v |> Option.value ~default:v - end end (** Destruct *) diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli index e2148b072..54f6652c3 100644 --- a/sledge/src/ses/term.mli +++ b/sledge/src/ses/term.mli @@ -102,7 +102,11 @@ module Var : sig type t = private term [@@deriving compare, equal, sexp] type strength = t -> [`Universal | `Existential | `Anonymous] option - module Map : Map.S with type key := t + module Map : sig + include Map.S with type key := t + + val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t + end module Set : sig include NS.Set.S with type elt := t @@ -132,23 +136,6 @@ module Var : sig variables do not clash with [fresh] variables is to pass the [identified] variables to [fresh] in [wrt]: [Var.fresh name ~wrt:(Var.Set.of_ (Var.identified ~name ~id))]. *) - - module Subst : sig - type var := t - type t [@@deriving compare, equal, sexp] - type x = {sub: t; dom: Set.t; rng: Set.t} - - val pp : t pp - val empty : t - val freshen : Set.t -> wrt:Set.t -> x * Set.t - val invert : t -> t - val restrict : t -> Set.t -> x - val is_empty : t -> bool - val domain : t -> Set.t - val range : t -> Set.t - val apply : t -> var -> var - val fold : t -> init:'a -> f:(var -> var -> 'a -> 'a) -> 'a - end end module Map : sig