Module Product.Make

Parameters

module IDs : MyUtils.IDs

Signature

type t = S1.t * S2.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
type err_t
val pp_err_t : Ppx_deriving_runtime.Format.formatter -> err_t -> Ppx_deriving_runtime.unit
val show_err_t : err_t -> Ppx_deriving_runtime.string
val err_t_to_yojson : err_t -> Yojson.Safe.t
val err_t_of_yojson : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or
type action
type pred
val action_from_str : string -> action option
val action_to_str : action -> string
val pred_from_str : string -> pred option
val pred_to_str : pred -> string
val empty : unit -> t

Returns an empty state

val execute_action : action -> t -> Gillian.Gil_syntax.Expr.t list -> (t * Gillian.Gil_syntax.Expr.t list, err_t) Stdlib.result Gillian.Monadic.Delayed.t

Execute an action

val consume : pred -> t -> Gillian.Gil_syntax.Expr.t list -> (t * Gillian.Gil_syntax.Expr.t list, err_t) Stdlib.result Gillian.Monadic.Delayed.t

Consume a predicate with the given ins

Produce a predicate with the given ins and outs

val compose : t -> t -> t Gillian.Monadic.Delayed.t

Compose two states together

val is_exclusively_owned : t -> Gillian.Gil_syntax.Expr.t list -> bool Gillian.Monadic.Delayed.t

For Freeable: if a state can be freed. Must only be true if no non-empty state can be composed with the state. The Expr list is irrelevant; it's required because of Gillian-C.

val is_empty : t -> bool

If this state is observably empty.

val is_concrete : t -> bool

If this state is entirely made up of concrete expressions.

val instantiate : Gillian.Gil_syntax.Expr.t list -> t * Gillian.Gil_syntax.Expr.t list

Instantiates this state with a list of arguments. This is used by PMap, either in static mode with the 'instantiate' action, or in dynamic mode when accessing a missing index.

val assertions : t -> (pred * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list) list

The list of core predicates corresponding to the state.

val assertions_others : t -> Gillian.Gil_syntax.Asrt.atom list

The list of assertions that aren't core predicates corresponding to the state.

val can_fix : err_t -> bool

If the error can be fixed

val get_fixes : err_t -> pred MyAsrt.t list list

Get the fixes for an error, as a list of fixes -- a fix is a list of core predicates to produce onto the state.

The recovery tactic to attempt to resolve an error, by eg. unfolding predicates

The set of logical variables in the state

The set of abstract locations in the state

val substitution_in_place : Gillian.Symbolic.Subst.t -> t -> t Gillian.Monadic.Delayed.t

Applies a substitution to the state. This can branch, eg. when attempting to resolve equality of expressions.

val pp : Stdlib.Format.formatter -> t -> unit

Pretty print the state

val list_actions : unit -> (action * string list * string list) list

(Debug only) Return all available (action * arguments * outputs)

val list_preds : unit -> (pred * string list * string list) list

(Debug only) Return all available (predicates * ins * outs)