gillian » Gillian » Gil_syntax » SLCmd

Module Gil_syntax.SLCmd

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 : (Asrt.t -> Asrt.t) -> (Expr.t -> Expr.t) -> t -> t

• deprecated

  Use Visitors.endo instead

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

Predicate actions

Some SLCmds are just syntactic sugar for special actions to be executed from the memory. For legacy reason, we have an encoding and decoding from one to the other.

We reserve these memory-action name: each carries Asrt.user_pred_prefix. The interpreter issues Fold, Unfold, GUnfold and Package as calls to these actions instead of through evaluate_slcmd.

val fold_action : string

val unfold_action : string

val gunfold_action : string

val package_action : string

val recover_action : string

Reserved action asking the predicate-carrying memory to recover from a failure by folding/unfolding; its arguments encode a recovery tactic (fold values or none; unfold values or none; "low"/"high"). It does not correspond to any SL command.

val is_pred_action : string -> bool

is_pred_action a holds iff a is one of the reserved actions above.

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

to_action c encodes a predicate-manipulating command as (action_name, args), or None for any other command (those are still handled by evaluate_slcmd). The arguments are left unevaluated (as they are syntactically matched against later).

val of_action : string -> Expr.t list -> t option

of_action name args is the inverse of to_action: it rebuilds the command for one of the four reserved action names, or None otherwise.