Module Debugger_utils.Match_map

A map of a matching.

A matching is either a single string of assertions for most matches (Direct) or potentially multiple strings of assertions when folding a predicate (Fold), each representing a case of the predicate.

Each string of assertions (dubbed match_seg) is essentially a singly linked list of Assertions (each of which contains information about that assertion - see assertion_data), terminated by a MatchResult that states whether that matching (or that case in the matching) was a success.

Describes why this matching is happening

val kind_to_yojson : kind -> Yojson.Safe.t
val kind_of_yojson : Yojson.Safe.t -> kind Ppx_deriving_yojson_runtime.error_or
type match_result =
  1. | Success
  2. | Failure
val match_result_to_yojson : match_result -> Yojson.Safe.t
val match_result_of_yojson : Yojson.Safe.t -> match_result Ppx_deriving_yojson_runtime.error_or
type substitution = {
  1. assert_id : Gillian.Logging.Report_id.t;
  2. subst : string * string;
}

A substitution, and the ID of the assertion where it was learned

val substitution_to_yojson : substitution -> Yojson.Safe.t
val substitution_of_yojson : Yojson.Safe.t -> substitution Ppx_deriving_yojson_runtime.error_or
type assertion_data = {
  1. id : Gillian.Logging.Report_id.t;
    (*

    The report ID of the assertion in the log database

    *)
  2. fold : (Gillian.Logging.Report_id.t * match_result) option;
    (*

    The ID of the fold matching and its result, if this assertion requires a fold

    *)
  3. assertion : string;
    (*

    The string representation of this assertion

    *)
  4. substitutions : substitution list;
    (*

    A list of the substitutions learned from this assertion specifically

    *)
}

Represents one step of a matching

val assertion_data_to_yojson : assertion_data -> Yojson.Safe.t
val assertion_data_of_yojson : Yojson.Safe.t -> assertion_data Ppx_deriving_yojson_runtime.error_or
type match_seg =
  1. | Assertion of assertion_data * match_seg
    (*

    A single assertion

    *)
  2. | MatchResult of Gillian.Logging.Report_id.t * match_result
    (*

    The end of this matching segment

    *)

A segment of matching

val match_seg_to_yojson : match_seg -> Yojson.Safe.t
val match_seg_of_yojson : Yojson.Safe.t -> match_seg Ppx_deriving_yojson_runtime.error_or
type map =
  1. | Direct of match_seg
  2. | Fold of match_seg list

A matching map. matching is either a single segment in the normal case, or potentially multiple segments when folding (i.e. when a predicate has multiple cases)

val map_to_yojson : map -> Yojson.Safe.t
val map_of_yojson : Yojson.Safe.t -> map Ppx_deriving_yojson_runtime.error_or
type t = kind * map
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val result : t -> match_result
module type Build = Match_map.Build

Build.f: Given the ID of a matching, build the representative matching map