simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

add Lit.Tbl,Lit.Set,Lit.Map

Browse source
This commit is contained in:
Simon Cruanes 2022-08-16 21:29:45 -04:00
parent 947f790f9f
commit 310d2183c4
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 16 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/core/lit.ml
View file

@ -28,12 +28,24 @@ let hash a =
let pp out l = let pp out l =
if l.lit_sign then if l.lit_sign then
T.pp_debug out l.lit_term T_printer.pp out l.lit_term
else else
Format.fprintf out "(@[@<1>¬@ %a@])" T.pp_debug l.lit_term Format.fprintf out "(@[@<1>¬@ %a@])" T_printer.pp l.lit_term
let norm_sign l = let norm_sign l =
if l.lit_sign then if l.lit_sign then
l, true l, true
else else
neg l, false neg l, false
module As_key = struct
type nonrec t = t
let equal = equal
let hash = hash
let compare = compare
end
module Map = CCMap.Make (As_key)
module Set = CCSet.Make (As_key)
module Tbl = CCHashtbl.Make (As_key)

2
src/core/lit.mli
View file

@ -42,3 +42,5 @@ val norm_sign : t -> t * bool
(** [norm_sign (+t)] is [+t, true], (** [norm_sign (+t)] is [+t, true],
and [norm_sign (-t)] is [+t, false]. and [norm_sign (-t)] is [+t, false].
In both cases the term is positive, and the boolean reflects the initial sign. *) In both cases the term is positive, and the boolean reflects the initial sign. *)
include Sidekick_sigs.WITH_SET_MAP_TBL with type t := t