Module Gil_syntax.Proc

Labeled GIL procedures

Every command is annotated with a label, and the gotos indicate to which label one should jump. Labels can be of any type. However, we say "labeled" when the labels are strings, and "indexed" when the labels are integers. Most functions in Gillian that work with indexed procedures assume for efficiency that the label of the i-th command is always Some i (starting from 0).

type ('annot, 'label) t = {
  1. proc_name : string;
  2. proc_source_path : string option;
  3. proc_internal : bool;
  4. proc_body : ('annot * 'label option * 'label Gillian.Gil_syntax.Cmd.t) array;
  5. proc_params : string list;
  6. proc_spec : Gillian.Gil_syntax.Spec.t option;
  7. proc_aliases : string list;
  8. proc_calls : string list;
  9. proc_display_name : (string * string) option;
  10. proc_hidden : bool;
}
val to_yojson : ('annot -> Yojson.Safe.t) -> ('label -> Yojson.Safe.t) -> ('annot, 'label) t -> Yojson.Safe.t
val of_yojson : (Yojson.Safe.t -> 'annot Ppx_deriving_yojson_runtime.error_or) -> (Yojson.Safe.t -> 'label Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> ('annot, 'label) t Ppx_deriving_yojson_runtime.error_or
val get_params : ('a, 'b) t -> string list

Gets the parameters of the procedure

val pp : show_labels:bool -> pp_label:'a Fmt.t -> ?pp_annot:'b Fmt.t -> Stdlib.Format.formatter -> ('b, 'a) t -> unit

If the show_labels flag is true, the labels will be written before the command they correspond to

val pp_labeled : Stdlib.Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, string) t -> unit

Print labelled

val pp_indexed : Stdlib.Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, int) t -> unit

Print indexed

val indexed_of_labeled : ('annot, string) t -> ('annot, int) t

Returns the indexed procedure for a labeled procedures where the labels can be of any type. Equality of labels is decided by structural equality

val check_proc_spec_correspondence : (string, ('annot, 'a) t) Utils.Prelude.Hashtbl.t -> unit