Skip to content

Commit

Permalink
rewrites knowledge and primus monads (#1361)
Browse files Browse the repository at this point in the history
* reimplements the knowledge monad

* uses the parallel binding operators in the theory merging operators

* publishes `zero` and `succ` in the Monad.State.Multi.Id interface

* rewrites the Primus Monad

* a couple of microoptimzations (with no observable benefits)

* removes the upper bound fro bitstring in opam/opam

* reverts an accidental change to the opam/opam file
  • Loading branch information
ivg authored Nov 10, 2021
1 parent 97cc1a3 commit 6c97e43
Show file tree
Hide file tree
Showing 5 changed files with 321 additions and 183 deletions.
27 changes: 9 additions & 18 deletions lib/bap_core_theory/bap_core_theory_manager.ml
Original file line number Diff line number Diff line change
Expand Up @@ -80,52 +80,43 @@ let declare
}

let (++) x y =
x >>= fun x ->
y >>| fun y ->
let+ x = x and+ y = y in
Value.merge x y
[@@inline]


let join1 p q x =
x >>= fun x ->
let* x = x in
p !!x ++ q !!x
[@@inline]

let join1s p q s x =
x >>= fun x ->
let* x = x in
p s !!x ++ q s !!x
[@@inline]

let join2 p q x y =
x >>= fun x ->
y >>= fun y ->
let* x = x and+ y = y in
p !!x !!y ++ q !!x !!y
[@@inline]

let join2s p q s x y =
x >>= fun x ->
y >>= fun y ->
let* x = x and+ y = y in
p s !!x !!y ++ q s !!x !!y
[@@inline]

let join3 p q x y z =
x >>= fun x ->
y >>= fun y ->
z >>= fun z ->
let* x = x and* y = y and* z = z in
p !!x !!y !!z ++ q !!x !!y !!z
[@@inline]

let join3s p q s x y z =
x >>= fun x ->
y >>= fun y ->
z >>= fun z ->
let* x = x and* y = y and* z = z in
p s !!x !!y !!z ++ q s !!x !!y !!z
[@@inline]

let join4 p q r x y z =
r >>= fun r ->
x >>= fun x ->
y >>= fun y ->
z >>= fun z ->
let* r = r and* x = x and* y = y and* z = z in
p !!r !!x !!y !!z ++ q !!r !!x !!y !!z
[@@inline]

Expand Down
Loading

0 comments on commit 6c97e43

Please sign in to comment.