Skip to content

Commit

Permalink
adds the monad choice interface to the knowledge monad (#1428)
Browse files Browse the repository at this point in the history
These operations, e.g., `guard`, `unless`, `on`, and `reject` greatly
improves legibility of promises by straghtening their control flow
structure.
  • Loading branch information
ivg authored Feb 11, 2022
1 parent 6dac0a9 commit 17e2a42
Show file tree
Hide file tree
Showing 2 changed files with 66 additions and 5 deletions.
14 changes: 13 additions & 1 deletion lib/knowledge/bap_knowledge.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2663,10 +2663,22 @@ module Knowledge = struct
let pids = ref Pid.zero

type conflict += Empty : ('a,'b) slot -> conflict
| Reject : conflict

let reject () = Knowledge.fail Reject
let guard cnd = if not cnd
then reject ()
else Knowledge.return ()
let on cnd yes = if cnd
then yes
else reject ()
let unless cnd no = if cnd
then reject ()
else no

let with_empty ~missing scope =
Knowledge.catch (scope ())
(function Empty _ -> Knowledge.return missing
(function Empty _ | Reject -> Knowledge.return missing
| other -> Knowledge.fail other)

let register_watcher (type a b)(s : (a,b) slot) run =
Expand Down
57 changes: 53 additions & 4 deletions lib/knowledge/bap_knowledge.mli
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,7 @@ module Knowledge : sig
@since 2.4.0 if [require] is called in the scope of the promise
and fails, the the whole promise immediately returns the empty
value of the property domain, i.e., [f] is wrapped into
[with_missing].
[with_empty].
*)
val promise : ('a,'p) slot -> ('a obj -> 'p t) -> unit

Expand All @@ -234,7 +234,7 @@ module Knowledge : sig
@since 2.4.0 if [require] is called in the scope of the promise
and fails, the the whole promise immediately returns the empty
value of the property domain, i.e., [promise] (not [f]) wrapped
into [with_missing].
into [with_empty].
*)
val promising : ('a,'p) slot -> promise:('a obj -> 'p t) ->
(unit -> 's t) -> 's t
Expand All @@ -247,7 +247,7 @@ module Knowledge : sig
@since 2.4.0 if [require] is called in the scope of the promise
and fails, the the whole promise immediately returns the empty
value of the property domain, i.e., [f] is wrapped into
[with_missing].
[with_empty].
*)
val propose : agent -> ('a, 'p opinions) slot -> ('a obj -> 'p t) -> unit
Expand All @@ -263,7 +263,7 @@ module Knowledge : sig
@since 2.4.0 if [require] are called in the scope of the proposal
and fails, the the whole proposal immediately returns the empty
value of the property domain, i.e., [propose] (not [f]) wrapped
into [with_missing].
into [with_empty].
*)
val proposing : agent -> ('a, 'p opinions) slot ->
Expand Down Expand Up @@ -296,11 +296,60 @@ module Knowledge : sig
(** [with_empty ~missing f x] evaluates [f ()] and if it fails on an empty
immediately evaluates to [return missing].
Inside of [with_empty] it is possible to use the choice monad
operations, like [reject], [guard], [on], and [unless], in
addition to the knowledge specialized choice operators, such
as [require] and various [*?] operators.
Note, that promised computations are invoked in the [with_empty]
scope.
@since 2.4.0
*)
val with_empty : missing:'r -> (unit -> 'r knowledge) -> 'r knowledge


(** [reject ()] rejects a promised computation.
When in the scope of the [with_empty] function, e.g., in a
promise or proposal, aborts the computation of the promise
and immediately returns an empty value.
@since 2.5.0 *)
val reject : unit -> 'a t

(** [guard cnd] rejects the rest of compuation if [cnd] is [false].
When in the scope of the [with_empty] function, e.g., in a
promise or proposal, aborts the computation of the promise
and immediately returns an empty value.
@since 2.5.0
*)
val guard : bool -> unit t


(** [on cnd x] evaluates to [x] if [cnd], otherwise rejects.
When in the scope of the [with_empty] function, e.g., in a
promise or proposal, aborts the computation of the promise
and immediately returns an empty value if [cnd] is [false].
If it is not, then evaluates to [x].
@since 2.5.0 *)
val on : bool -> unit t -> unit t

(** [unless cnd x] evaluates to [x] if [not cnd], otherwise rejects.
When in the scope of the [with_empty] function, e.g., in a
promise or proposal, aborts the computation of the promise
and immediately returns an empty value if [cnd] is [true].
If it is [false], then evaluates to [x].
@since 2.5.0 *)
val unless : bool -> unit t -> unit t


(** state with no knowledge *)
val empty : state

Expand Down

0 comments on commit 17e2a42

Please sign in to comment.