From dd50ab079e2d967b7c93f9451c97e3f5e8f33d50 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 30 Jul 2022 23:59:15 -0400
Subject: [PATCH] remove most proof-trace code

---
 .../dummy/Sidekick_proof_trace_dummy.ml       | 35 -------------------
 src/proof-trace/dummy/dune                    |  6 ----
 .../dyn/Sidekick_proof_trace_dyn.ml           | 23 ------------
 src/proof-trace/dyn/dune                      |  6 ----
 .../bare/dump => proof-tracy-bare-dump}/dune  |  0
 .../proof_trace_dump.ml                       |  0
 6 files changed, 70 deletions(-)
 delete mode 100644 src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml
 delete mode 100644 src/proof-trace/dummy/dune
 delete mode 100644 src/proof-trace/dyn/Sidekick_proof_trace_dyn.ml
 delete mode 100644 src/proof-trace/dyn/dune
 rename src/{proof-trace/bare/dump => proof-tracy-bare-dump}/dune (100%)
 rename src/{proof-trace/bare/dump => proof-tracy-bare-dump}/proof_trace_dump.ml (100%)

diff --git a/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml b/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml
deleted file mode 100644
index 15b463ed..00000000
--- a/src/proof-trace/dummy/Sidekick_proof_trace_dummy.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-(** Dummy proof traces.
-
-    These proof traces will not record information. *)
-
-module type S = Sidekick_sigs_proof_trace.S
-
-module type ARG = sig
-  include Sidekick_sigs_proof_trace.ARG
-
-  val dummy_step_id : step_id
-end
-
-module Make (A : ARG) : S with type t = unit and module A = A = struct
-  module A = A
-
-  type t = unit
-
-  let enabled _ = false
-  let add_step _ _ = A.dummy_step_id
-  let add_unsat _ _ = ()
-  let delete _ _ = ()
-end
-
-(** Dummy proof trace where everything is [unit]. Use this if you don't care
-   for proofs at all. *)
-module Unit :
-  S with type t = unit and type A.rule = unit and type A.step_id = unit =
-Make (struct
-  type rule = unit
-  type step_id = unit
-
-  module Step_vec = Vec_unit
-
-  let dummy_step_id = ()
-end)
diff --git a/src/proof-trace/dummy/dune b/src/proof-trace/dummy/dune
deleted file mode 100644
index 57140a75..00000000
--- a/src/proof-trace/dummy/dune
+++ /dev/null
@@ -1,6 +0,0 @@
-(library
- (name sidekick_proof_trace_dummy)
- (public_name sidekick.proof-trace.dummy)
- (synopsis "Dummy proof trace that stores nothing")
- (libraries sidekick.util sidekick.sigs.proof-trace)
- (flags :standard -open Sidekick_util))
diff --git a/src/proof-trace/dyn/Sidekick_proof_trace_dyn.ml b/src/proof-trace/dyn/Sidekick_proof_trace_dyn.ml
deleted file mode 100644
index 9deee8f7..00000000
--- a/src/proof-trace/dyn/Sidekick_proof_trace_dyn.ml
+++ /dev/null
@@ -1,23 +0,0 @@
-module type ARG = Sidekick_sigs_proof_trace.ARG
-module type S = Sidekick_sigs_proof_trace.S
-
-(** Dynamic version.
-
-    The proof trace is a first-class module that can be provided at runtime. *)
-module Make_dyn (A : ARG) : S with module A = A = struct
-  module A = A
-
-  module type DYN = sig
-    val enabled : unit -> bool
-    val add_step : A.rule -> A.step_id
-    val add_unsat : A.step_id -> unit
-    val delete : A.step_id -> unit
-  end
-
-  type t = (module DYN)
-
-  let[@inline] enabled ((module Tr) : t) : bool = Tr.enabled ()
-  let[@inline] add_step ((module Tr) : t) rule : A.step_id = Tr.add_step rule
-  let[@inline] add_unsat ((module Tr) : t) s : unit = Tr.add_unsat s
-  let[@inline] delete ((module Tr) : t) s : unit = Tr.delete s
-end
diff --git a/src/proof-trace/dyn/dune b/src/proof-trace/dyn/dune
deleted file mode 100644
index 24ca6785..00000000
--- a/src/proof-trace/dyn/dune
+++ /dev/null
@@ -1,6 +0,0 @@
-(library
- (name sidekick_proof_trace_dyn)
- (public_name sidekick.proof-trace.dyn)
- (synopsis "Dynamic version of the proof trace")
- (libraries sidekick.util sidekick.sigs.proof-trace)
- (flags :standard -open Sidekick_util))
diff --git a/src/proof-trace/bare/dump/dune b/src/proof-tracy-bare-dump/dune
similarity index 100%
rename from src/proof-trace/bare/dump/dune
rename to src/proof-tracy-bare-dump/dune
diff --git a/src/proof-trace/bare/dump/proof_trace_dump.ml b/src/proof-tracy-bare-dump/proof_trace_dump.ml
similarity index 100%
rename from src/proof-trace/bare/dump/proof_trace_dump.ml
rename to src/proof-tracy-bare-dump/proof_trace_dump.ml