Module Gil_syntax.Asrt

GIL Assertions

type t =
  1. | Emp
    (*

    Empty heap

    *)
  2. | Star of t * t
    (*

    Separating conjunction

    *)
  3. | Pred of string * Gillian.Gil_syntax.Expr.t list
    (*

    Predicates

    *)
  4. | Pure of Gillian.Gil_syntax.Formula.t
    (*

    Pure formula

    *)
  5. | Types of (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Type.t) list
    (*

    Typing assertion

    *)
  6. | GA of string * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list
    (*

    Core assertion

    *)
  7. | Wand of {
    1. lhs : string * Gillian.Gil_syntax.Expr.t list;
    2. rhs : string * Gillian.Gil_syntax.Expr.t list;
    }
    (*

    Magic wand of the form P(...) -* Q(...)

    *)
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> int

Comparison of assertions

val prioritise : t -> t -> int

Sorting of assertions

module Set : Stdlib.Set.S with type elt := t

Sets of assertions

val map : (t -> t * bool) option -> (t -> t) option -> (Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t) option -> (Gillian.Gil_syntax.Formula.t -> Gillian.Gil_syntax.Formula.t) option -> t -> t
val list_lexprs : t -> Expr.Set.t

Get all the logical expressions of a that denote a list and are not logical variables

val lvars : t -> Utils.Prelude.SS.t

Get all the logical variables in a

val pvars : t -> Utils.Prelude.SS.t

Get all the program variables in a

val alocs : t -> Utils.Prelude.SS.t

Get all the abstract locations in a

val clocs : t -> Utils.Prelude.SS.t

Get all the concrete locations in a

val locs : t -> Utils.Prelude.SS.t

Get all locations in a

val pred_names : t -> string list

Returns a list with the names of the predicates that occur in a

val pure_asrts : t -> Gillian.Gil_syntax.Formula.t list

Returns a list with the pure assertions that occur in a

val simple_asrts : t -> t list

Returns a list with the pure assertions that occur in a

val is_pure_asrt : t -> bool

Check if a is a pure assertion

val is_pure_non_rec_asrt : t -> bool

Check if a is a pure assertion & non-recursive assertion. It assumes that only pure assertions are universally quantified

val make_pure : t -> Gillian.Gil_syntax.Formula.t

Eliminate LStar and LTypes assertions. LTypes disappears. LStar is replaced by LAnd. This function expects its argument to be a PURE assertion.

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

Pretty-printer

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

Full pretty-printer

val star : t list -> t

star [a1; a2; ...; an] will return [a1 * a2 * ... * an]

val subst_clocs : (string -> Gillian.Gil_syntax.Expr.t) -> t -> t

subst_clocs subst a Substitutes expressions of the form Lit (Loc l) with subst l in a

val subst_expr_for_expr : to_subst:Gillian.Gil_syntax.Expr.t -> subst_with:Gillian.Gil_syntax.Expr.t -> t -> t

subst_expr_for_expr ~to_subst ~subst_with a substitutes every occurence of the expression to_subst with the expression subst_with in a

val pvars_to_lvars : t -> t

Move pvars to lvars

module Infix : sig ... end