gillian » Gillian » Gil_syntax » Asrt

Module Gil_syntax.Asrt

type atom =

1. | Emp
   (*

   Empty heap

   *)
2. | Pure of Expr.t
   (*

   Pure formula

   *)
3. | Types of (Expr.t * Type.t) list
   (*

   Typing assertion

   *)
4. | CorePred of string * Expr.t list * Expr.t list
   (*

   Core assertion

   *)

val atom_to_yojson : atom -> Yojson.Safe.t

val atom_of_yojson : Yojson.Safe.t -> atom Ppx_deriving_yojson_runtime.error_or

val equal_atom : atom -> atom -> Ppx_deriving_runtime.bool

type t = atom list

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 user_pred_prefix : string

Prefix encoding a user-defined predicate as a CorePred name. Set once; never hardcode it elsewhere.

val user_pred_name : string -> string

user_pred_name p is the core-predicate name encoding user predicate p.

val as_user_pred_name : string -> string option

as_user_pred_name s is Some p when s encodes the user predicate p, and None when s is a genuine core predicate.

val pred : string -> Expr.t list -> Expr.t list -> atom

pred name ins outs builds a user-predicate assertion atom.

val wand_prefix : string

Prefix and separator encoding a magic wand lname(..) -* rname(..) as a CorePred name wand_prefix ^ lname ^ wand_sep ^ rname. Set once; never hardcode elsewhere.

val wand_sep : string

val wand_name : string -> string -> string

wand_name lname rname is the core-predicate name encoding the wand lname(..) -* rname(..).

val as_wand_name : string -> (string * string) option

as_wand_name s is Some (lname, rname) when s encodes a magic wand, and None otherwise.

val wand_to_core_pred :
  (string * Expr.t list) ->
  (string * Expr.t list) ->
  Expr.t list ->
  string * Expr.t list * Expr.t list

val wand :
  (string * Expr.t list) ->
  (string * Expr.t list) ->
  Expr.t list ->
  atom

wand (lname, largs) (rname, r_ins) r_outs builds a magic-wand assertion atom. A wand's semantic ins are largs @ r_ins and its outs are r_outs (only the rhs out-arguments); these are stored as the CorePred's ins and outs respectively.

val as_wand :
  rhs_ins_number:int ->
  atom ->
  ((string * Expr.t list) * (string * Expr.t list)) option

as_wand ~rhs_ins_number a recovers Some (lhs, rhs) when a is a wand-encoding CorePred, and None otherwise. rhs_ins_number is the number of in-parameters of the rhs predicate, needed to split the stored ins back into largs and r_ins.

type Stdlib.Effect.t +=

1. | Pred_ins_number : string -> int option Stdlib.Effect.t

Effect looking up a predicate's number of in-parameters. Performed by the wand printer; handled by Engine.MP.with_pred_table.

val pred_ins_number : string -> int option

pred_ins_number name performs Pred_ins_number, returning None when no handler (predicate table) is installed.

val compare : atom -> atom -> int

Comparison of assertions

val prioritise : atom -> atom -> int

Sorting of assertions

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

Sets of assertions

val map : (Expr.t -> Expr.t) -> t -> t

• deprecated

  Use Visitors.endo instead

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 -> Expr.t list

Returns a list with the pure assertions that occur in a

val is_pure_asrt : atom -> bool

Check if a is a pure assertion

val make_pure : t -> Expr.t

Eliminate Emp assertions. Pure assertions are converted to a single formula. This function expects its argument to be a PURE assertion.

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

Pretty-printer

val pp_atom : Stdlib.Format.formatter -> atom -> unit

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

Full pretty-printer

val pp_atom_full : Stdlib.Format.formatter -> atom -> unit

val subst_clocs : (string -> 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:Expr.t -> subst_with: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