gillian » Gillian » Concrete » Subst

Module Concrete.Subst

type vt = Concrete.Values.t

Type of GIL values

type t

Type of GIL substitutions

val init : (Gil_syntax.Var.t * vt) list -> t

Substitution constructor, with a list of bindings of the form (variable, value)

val is_empty : t -> bool

Is the substitution empty?

val clear : t -> unit

Reset substitution

val domain : t -> (Gil_syntax.Var.t -> bool) option -> Gil_syntax.Var.Set.t

Domain of the substitution

val range : t -> vt list

Range of the substitution

val get : t -> Gil_syntax.Var.t -> vt option

Substitution lookup

val add : t -> Gil_syntax.Var.t -> vt -> unit

Substitution incremental update

val put : t -> Gil_syntax.Var.t -> vt -> unit

Substitution update

val mem : t -> Gil_syntax.Var.t -> bool

Substitution membership

val copy : t -> t

Substitution copy

val extend : t -> (Gil_syntax.Var.t * vt) list -> unit

Substitution extension with a list of bindings

val merge_left : t -> t -> unit

Substution merge into left

val filter : t -> (Gil_syntax.Var.t -> vt -> bool) -> t

Substitution filter

val projection : t -> Gil_syntax.Var.Set.t -> t

Substitution variable filter

val iter : t -> (Gil_syntax.Var.t -> vt -> unit) -> unit

Substitution iterator

val fold : t -> (Gil_syntax.Var.t -> vt -> 'a -> 'a) -> 'a -> 'a

Substitution fold

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

Pretty Printer

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

Full pretty Printer

val filter_in_place : t -> (Gil_syntax.Var.t -> vt -> vt option) -> unit

val to_list : t -> (Gil_syntax.Var.t * vt) list

Convert substitution to list

val subst_in_expr : t -> partial:bool -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t

Substitution inside a logical expression

val subst_in_expr_opt : t -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t option

Optional substitution inside a logical expression

val substitute_asrt :
  t ->
  partial:bool ->
  Gil_syntax.Asrt.t ->
  Gil_syntax.Asrt.t

val substitute_slcmd :
  t ->
  partial:bool ->
  Gil_syntax.SLCmd.t ->
  Gil_syntax.SLCmd.t

val substitute_lcmd :
  t ->
  partial:bool ->
  Gil_syntax.LCmd.t ->
  Gil_syntax.LCmd.t