Source

z3 / src / api / ml / mlx_mk_datatypes.idl

quote(mlmli,"
(** A constructor of a datatype is described by: *)
type datatype_constructor_desc = {
  constructor_desc : symbol;            	(** name of the constructor function *)
  recognizer_desc : symbol;             	(** name of the recognizer function *)
  accessor_descs : (symbol * sort) array;	(** names and sorts of the fields *)
}

(** A datatype is described by a name and constructor descriptors. *)
type datatype_desc = symbol * datatype_constructor_desc array

(** A constructor of a datatype is represented by: *)
type datatype_constructor = {
  constructor : func_decl;              	(** constructor function *)
  recognizer : func_decl;               	(** recognizer function *)
  accessors : func_decl array;          	(** field accessor functions *)
}

(** A datatype is represented by a sort and constructors. *)
type datatype = sort * datatype_constructor array
");

quote(mli,"
(** [mk_datatypes ctx sorts_to_descriptors] creates mutually recursive datatypes described by
    [sorts_to_descriptors], which is a function from the sorts of the datatypes to be created to
    descriptors of the datatypes' constructors. {b See also}: {!Test_mlapi.forest_example} *)
val mk_datatypes: context -> (sort array -> (datatype_desc array) option) -> datatype array
");
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.