gillian » Gillian » Gil_syntax » Proc

Module Gil_syntax.Proc

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 Cmd.t) array;
5. proc_params : string list;
6. proc_spec : 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