gillian » Gillian » Debugger » Utils » Exec_map

Module Utils.Exec_map

type ('c, 'bd) next_kind =

1. | One of 'bd
   (*

   A command that doesn't branch or terminate

   *)
2. | Many of ('c * 'bd) list
   (*

   A branching command

   *)
3. | Zero
   (*

   A terminating command

   *)

The "kind" of a command in an exec map

val next_kind_to_yojson :
  'c 'bd. ('c -> Yojson.Safe.t) ->
  ('bd -> Yojson.Safe.t) ->
  ('c, 'bd) next_kind ->
  Yojson.Safe.t

val next_kind_of_yojson :
  'c 'bd. (Yojson.Safe.t -> 'c Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'bd Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  ('c, 'bd) next_kind Ppx_deriving_yojson_runtime.error_or

val kind_of_cases : 'a list -> ('a, unit) next_kind

Maps a list of branches to Normal if empty, or Branch

An exec map / node in an exec map; takes the following type parameters:

• 'branch_case: the type that identifies a branch case
• 'cmd_data: the type of the data attached to each non-Nothing node
• 'branch_data: additional data attached to each branch case

type ('id, 'case, 'branch_data) next =

1. | Single of 'id option * 'branch_data
2. | Branch of ('case * ('id option * 'branch_data)) list

val next_to_yojson :
  'id 'case 'branch_data. ('id -> Yojson.Safe.t) ->
  ('case -> Yojson.Safe.t) ->
  ('branch_data -> Yojson.Safe.t) ->
  ('id, 'case, 'branch_data) next ->
  Yojson.Safe.t

val next_of_yojson :
  'id 'case 'branch_data. (Yojson.Safe.t ->
                            'id Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'case Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'branch_data Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  ('id, 'case, 'branch_data) next Ppx_deriving_yojson_runtime.error_or

type ('id, 'case, 'data, 'bdata) node = {

1. data : 'data;
2. next : ('id, 'case, 'bdata) next option;

}

val node_to_yojson :
  'id 'case 'data 'bdata. ('id -> Yojson.Safe.t) ->
  ('case -> Yojson.Safe.t) ->
  ('data -> Yojson.Safe.t) ->
  ('bdata -> Yojson.Safe.t) ->
  ('id, 'case, 'data, 'bdata) node ->
  Yojson.Safe.t

val node_of_yojson :
  'id 'case 'data 'bdata. (Yojson.Safe.t ->
                            'id Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'case Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'data Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'bdata Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  ('id, 'case, 'data, 'bdata) node Ppx_deriving_yojson_runtime.error_or

type ('id, 'case, 'cmd_data, 'branch_data) entry =

1. | Node of ('id, 'case, 'cmd_data, 'branch_data) node
2. | Alias of 'id

val entry_to_yojson :
  'id 'case 'cmd_data 'branch_data. ('id -> Yojson.Safe.t) ->
  ('case -> Yojson.Safe.t) ->
  ('cmd_data -> Yojson.Safe.t) ->
  ('branch_data -> Yojson.Safe.t) ->
  ('id, 'case, 'cmd_data, 'branch_data) entry ->
  Yojson.Safe.t

val entry_of_yojson :
  'id 'case 'cmd_data 'branch_data. (Yojson.Safe.t ->
                                      'id Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'case Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'cmd_data Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'branch_data Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  ('id, 'case, 'cmd_data, 'branch_data) entry
    Ppx_deriving_yojson_runtime.error_or

type ('id, 'branch_case, 'cmd_data, 'branch_data) map = {

1. mutable root : 'id option;
2. entries : ('id, ('id, 'branch_case, 'cmd_data, 'branch_data) entry)
            Utils.Prelude.Hashtbl.t;

}

val map_to_yojson :
  'id 'branch_case 'cmd_data 'branch_data. ('id -> Yojson.Safe.t) ->
  ('branch_case -> Yojson.Safe.t) ->
  ('cmd_data -> Yojson.Safe.t) ->
  ('branch_data -> Yojson.Safe.t) ->
  ('id, 'branch_case, 'cmd_data, 'branch_data) map ->
  Yojson.Safe.t

val map_of_yojson :
  'id 'branch_case 'cmd_data 'branch_data. (Yojson.Safe.t ->
                                             'id
                                               Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'branch_case Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'cmd_data Ppx_deriving_yojson_runtime.error_or) ->
  (Yojson.Safe.t -> 'branch_data Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  ('id, 'branch_case, 'cmd_data, 'branch_data) map
    Ppx_deriving_yojson_runtime.error_or

A command in an exec map

type stop_at =

1. | StartOfPath
   (*

   Stop at the start of the path, i.e. as soon as possible

   *)
2. | EndOfPath
   (*

   Stop at the end of the path, i.e. as late as possible

   *)
3. | BeforeNothing
   (*

   As with EndOfPath, but if the path ends with Nothing, step back to the previous command

   *)

Used for various map-traversal commands; signifies when to stop exploring paths

type 't submap =

1. | NoSubmap
2. | Submap of 't
   (*

   Embed an Exec_map as a submap

   *)
3. | Proc of string
   (*

   Embed the execution of another proc as a submap

   *)

val submap_to_yojson : 't. ('t -> Yojson.Safe.t) -> 't submap -> Yojson.Safe.t

val submap_of_yojson :
  't. (Yojson.Safe.t -> 't Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  't submap Ppx_deriving_yojson_runtime.error_or

val _ :
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a submap Ppx_deriving_yojson_runtime.error_or

val make : unit -> ('a, 'b, 'c, 'd) map

val get_with_id :
  ('a, 'b, 'c, 'd) map ->
  'a ->
  (('a, 'b, 'c, 'd) node * 'a) option

val get : ('a, 'b, 'c, 'd) map -> 'a -> ('a, 'b, 'c, 'd) node option

val map_node_extra :
  ('a, 'b, 'c, 'd) map ->
  'a ->
  (('a, 'b, 'c, 'd) node -> ('a, 'b, 'c, 'd) node * 'e) ->
  'e option

val map_node_extra_exn :
  ('a, 'b, 'c, 'd) map ->
  'a ->
  (('a, 'b, 'c, 'd) node -> ('a, 'b, 'c, 'd) node * 'e) ->
  'e

val map_node :
  ('a, 'b, 'c, 'd) map ->
  'a ->
  (('a, 'b, 'c, 'd) node -> ('a, 'b, 'c, 'd) node) ->
  bool

val map_node_exn :
  ('a, 'b, 'c, 'd) map ->
  (('a, 'b, 'c, 'd) node -> ('a, 'b, 'c, 'd) node) ->
  'a ->
  unit

val insert :
  ('a, 'b, 'c, 'd) map ->
  id:'a ->
  all_ids:'a list ->
  ('a, 'b, 'c, 'd) node ->
  unit

val get_exn : ('a, 'b, 'c, 'd) map -> 'a -> ('a, 'b, 'c, 'd) node

val find_path :
  (('a, 'b, 'c, 'd) node -> bool) ->
  ('a, 'b, 'c, 'd) map ->
  'b list option

Traverse the map depth-first, giving the path to the first node that matches the given predicate (or None otherwise)

val find_path_exn :
  (('a, 'b, 'c, 'd) node -> bool) ->
  ('a, 'b, 'c, 'd) map ->
  'b list

Exception-raising equivalent to find_path

val at_path :
  ?stop_at:stop_at ->
  'a list ->
  ('b, 'a, 'c, 'd) map ->
  ('b, 'a, 'c, 'd) node option

Gets the node at the given path

val at_path_exn :
  ?stop_at:stop_at ->
  'a list ->
  ('b, 'a, 'c, 'd) map ->
  ('b, 'a, 'c, 'd) node

Exception-raising equivalent to at_path

module Packaged : sig ... end

An Exec_map to be passed to the debugger frontend and displayed