Module Gil_syntax.SLCmd

GIL Separation-Logic Commands

type t =
  1. | Fold of string * Expr.t list * (string * (string * Expr.t) list) option
    (*

    Fold predicate

    *)
  2. | Unfold of string * Expr.t list * (string * string) list option * bool
    (*

    Unfold predicate

    *)
  3. | Package of {
    1. lhs : string * Expr.t list;
    2. rhs : string * Expr.t list;
    }
    (*

    Magic wand packaging

    *)
  4. | GUnfold of string
    (*

    Global Unfold

    *)
  5. | ApplyLem of string * Expr.t list * string list
    (*

    Apply lemma

    *)
  6. | SepAssert of Asrt.t * string list
    (*

    Assert

    *)
  7. | Invariant of Asrt.t * string list
    (*

    Invariant

    *)
  8. | Consume of Asrt.t * string list
  9. | Produce of Asrt.t
  10. | SymbExec
val map : (t -> t) option -> (Asrt.t -> Asrt.t) option -> (Expr.t -> Expr.t) option -> t -> t
val pp_folding_info : (string * (string * Expr.t) list) option Fmt.t

Pretty-printer of folding info

val pp_unfold_info : (string * string) list option Fmt.t
val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer