From d8d9d4b2e5428bb637dca1b8dc49c47f09ac1a5d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 15 Sep 2020 01:48:59 -0700 Subject: [PATCH] [sledge] Refactor: Remove dead Var.of_reg{,s} Reviewed By: ngorogiannis Differential Revision: D23660292 fbshipit-source-id: b1f095b82 --- sledge/src/ses/term.ml | 8 -------- sledge/src/ses/term.mli | 2 -- 2 files changed, 10 deletions(-) diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml index aacccb999..d45b1ac96 100644 --- a/sledge/src/ses/term.ml +++ b/sledge/src/ses/term.ml @@ -1035,11 +1035,6 @@ module Var = struct | Var _ as v -> Some (v |> check invariant) | _ -> None - let of_reg r = - match of_term (of_exp (r : Llair.Reg.t :> Llair.Exp.t)) with - | Some v -> v - | _ -> violates Llair.Reg.invariant r - let program ~name ~global = Var {name; id= (if global then -1 else 0)} let fresh name ~wrt = @@ -1060,9 +1055,6 @@ module Var = struct let pp_xs fs xs = if not (is_empty xs) then Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs - - let of_regs = - Llair.Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r)) end end diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli index 64cdc7b3d..662036eff 100644 --- a/sledge/src/ses/term.mli +++ b/sledge/src/ses/term.mli @@ -116,7 +116,6 @@ module Var : sig val ppx : strength -> t pp val pp : t pp val pp_xs : t pp - val of_regs : Llair.Reg.Set.t -> t end val pp : t pp @@ -127,7 +126,6 @@ module Var : sig val id : t -> int val of_ : term -> t val of_term : term -> t option - val of_reg : Llair.Reg.t -> t val program : name:string -> global:bool -> t val fresh : string -> wrt:Set.t -> t * Set.t