From cc1a93fa74a0fd25b13a399ca2c1524b2d4e4bed Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 17 Aug 2021 23:58:49 -0400
Subject: [PATCH] feat: add `sidekick.lit` small library for literals

---
 src/lit/Sidekick_lit.ml | 40 ++++++++++++++++++++++++++++++++++++++++
 src/lit/dune            |  7 +++++++
 2 files changed, 47 insertions(+)
 create mode 100644 src/lit/Sidekick_lit.ml
 create mode 100644 src/lit/dune

diff --git a/src/lit/Sidekick_lit.ml b/src/lit/Sidekick_lit.ml
new file mode 100644
index 00000000..29fd8fb9
--- /dev/null
+++ b/src/lit/Sidekick_lit.ml
@@ -0,0 +1,40 @@
+
+(** Implementation of literals from terms *)
+
+module Make(T : Sidekick_core.TERM)
+  : Sidekick_core.LIT with module T = T
+= struct
+  module T = T
+  type term = T.Term.t
+  type t = {
+    lit_term: term;
+    lit_sign : bool
+  }
+
+  let[@inline] neg l = {l with lit_sign=not l.lit_sign}
+  let[@inline] sign t = t.lit_sign
+  let[@inline] abs t = {t with lit_sign=true}
+  let[@inline] term (t:t): term = t.lit_term
+  let[@inline] signed_term t = term t, sign t
+
+  let make ~sign t = {lit_sign=sign; lit_term=t}
+
+  let atom tst ?(sign=true) (t:term) : t =
+    let t, sign' = T.Term.abs tst t in
+    let sign = if not sign' then not sign else sign in
+    make ~sign t
+
+  let equal a b =
+    a.lit_sign = b.lit_sign &&
+    T.Term.equal a.lit_term b.lit_term
+
+  let hash a =
+    let sign = a.lit_sign in
+    CCHash.combine3 2 (CCHash.bool sign) (T.Term.hash a.lit_term)
+
+  let pp out l =
+    if l.lit_sign then T.Term.pp out l.lit_term
+    else Format.fprintf out "(@[@<1>¬@ %a@])" T.Term.pp l.lit_term
+
+  let norm_sign l = if l.lit_sign then l, true else neg l, false
+end
diff --git a/src/lit/dune b/src/lit/dune
new file mode 100644
index 00000000..7429ee17
--- /dev/null
+++ b/src/lit/dune
@@ -0,0 +1,7 @@
+
+(library
+  (name sidekick_lit)
+  (public_name sidekick.lit)
+  (synopsis "Implementation of literals for Sidekick")
+  (libraries containers sidekick.core sidekick.util)
+  (flags :standard -warn-error -a+8 -open Sidekick_util))