Module Astral_internal.SID

module ID : sig ... end
type t
include Datatype_sig.PRINTABLE with type t := t
include Datatype_sig.SHOW with type t := t
val show : t -> string

String representation of type t

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

Output to formatter

val print : ?prefix:string -> t -> unit

Output to stdout.

val show_option : t option -> string
val print_option : ?prefix:string -> t option -> unit
val dump : string -> t -> unit

Dump to file given by filename

Lists of printable values

val show_list : ?separator:string -> t list -> string
val pp_list : Stdlib.Format.formatter -> t list -> unit
val print_list : ?separator:string -> ?prefix:string -> t list -> unit
val empty : t
val register_builtin : t -> (module ID_sig.BUILTIN) -> t
val register_user_defined : t -> InductiveDefinition.t -> t
val update_user_defined : t -> InductiveDefinition.t -> t
val compute_graph : t -> t
val is_builtin : t -> string -> bool
val is_user_defined : t -> string -> bool
val find : t -> string -> ID.t
val find_builtin : t -> string -> (module ID_sig.BUILTIN)
val find_user_defined : t -> string -> InductiveDefinition.t
val get_user_defined : t -> InductiveDefinition.t list
val get_builtin : t -> (module ID_sig.BUILTIN) list
val filter_map : (ID.t -> ID.t option) -> t -> t
val fold : (ID.t -> 'a -> 'a) -> t -> 'a -> 'a
val fold_builtin : ((module ID_sig.BUILTIN) -> 'a -> 'a) -> t -> 'a -> 'a
val fold_user_defined : (InductiveDefinition.t -> 'a -> 'a) -> t -> 'a -> 'a

Unfolding

val unfold : t -> string -> SL.Term.t list -> int -> SL.t

Predicate dependencies

val dependency_graph : t -> DependencyGraph.t
val is_self_recursive : t -> string -> bool

True if inductive definition contains a recursive call of itself.

val dependencies : t -> string -> InductiveDefinition.t list

For an user-defined predicate, return it and all the predicates it can directly and indirectly call.