Bidir.TypesDefines the bidirectional imperative language in bidir.
type value = | VInt of intAn arbitrary-size integer.
*)| VStr of string| VBits of stringBitvectors are strings of only 0/1. Bitvector length is the string length.
*)| VTup of value listA value in the bidirectional language.
val equal_value : value -> value -> Ppx_deriving_runtime.boolval pp_value :
Ppx_deriving_runtime.Format.formatter ->
value ->
Ppx_deriving_runtime.unitval show_value : value -> Ppx_deriving_runtime.stringval value_to_yojson : value -> Yojson.Safe.tval value_of_yojson :
Yojson.Safe.t ->
value Ppx_deriving_yojson_runtime.error_orval equal_varname : varname -> varname -> Ppx_deriving_runtime.boolval pp_varname :
Ppx_deriving_runtime.Format.formatter ->
varname ->
Ppx_deriving_runtime.unitval show_varname : varname -> Ppx_deriving_runtime.stringval varname_to_yojson : varname -> Yojson.Safe.tval varname_of_yojson :
Yojson.Safe.t ->
varname Ppx_deriving_yojson_runtime.error_orval str_of_varname : varname -> stringAn expression in the bidirectional language. Every expression can be interpreted bidirectionally, i.e., as a left- or right- expression.
val equal_expr : expr -> expr -> Ppx_deriving_runtime.boolval pp_expr :
Ppx_deriving_runtime.Format.formatter ->
expr ->
Ppx_deriving_runtime.unitval show_expr : expr -> Ppx_deriving_runtime.stringval expr_to_yojson : expr -> Yojson.Safe.tval expr_of_yojson : Yojson.Safe.t -> expr Ppx_deriving_yojson_runtime.error_ortype 'a bidir = | Assign of expr * 'a list * exprAn assignment reading from the first expression, piping left-to-right through the intrinsics, then storing into the second expression.
*)| Decl of varname listRequires the given variables are in scope and narrows the current state to only the specified variables. This behaves identical forwards or backwards.
*)| Delete of varname listRemoves the given variables from the scope. This behaves identically forwards and backwards.
*)| Choice of 'a bidir listA mutually-exclusive choice between the given alternatives. Exactly one alternative must succeed.
*)| Parallel of 'a bidir listParallel execution of the given bidirectional programs. All parallels must succeed. Each parallel should be independent (i.e., input and output disjoint variables) from the others.
*)| Sequential of 'a bidir listA sequential composition of statements. In the backwards direction, the list is reversed.
*)A statement in the bidirectional language which can be interpreted forwards or backwards. The type parameter is the type of intrinsic functions. Unless mentioned otherwise, the descriptions here are for the forwards direction.
val equal_bidir :
'a. ('a -> 'a -> Ppx_deriving_runtime.bool) ->
'a bidir ->
'a bidir ->
Ppx_deriving_runtime.boolval pp_bidir :
'a. (Ppx_deriving_runtime.Format.formatter ->
'a ->
Ppx_deriving_runtime.unit) ->
Ppx_deriving_runtime.Format.formatter ->
'a bidir ->
Ppx_deriving_runtime.unitval show_bidir :
'a. (Ppx_deriving_runtime.Format.formatter ->
'a ->
Ppx_deriving_runtime.unit) ->
'a bidir ->
Ppx_deriving_runtime.stringval bidir_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a bidir -> Yojson.Safe.tval bidir_of_yojson :
'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a bidir Ppx_deriving_yojson_runtime.error_orval _ :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a bidir Ppx_deriving_yojson_runtime.error_ortype state = value Lang.Common.StringMap.tval equal_state : state -> state -> Ppx_deriving_runtime.boolval pp_state :
Ppx_deriving_runtime.Format.formatter ->
state ->
Ppx_deriving_runtime.unitval show_state : state -> Ppx_deriving_runtime.stringFlipped function application, taking a value followed by a function to apply it to. Very useful when folding a list of functions.
Given a list of functions, sends the given input value to every function and collects the results.