Module Astral_internal.Lists

Singly-linked list parametrised by a sort S and field F.

include module type of struct include ID end
type t = InductiveDefinition.t = {
  1. name : string;
  2. header : SL.Variable.t list;
  3. base_cases : SL.t list;
  4. inductive_cases : SL.t list;
}
include Datatype_sig.PRINTABLE with type t := t
include Datatype_sig.SHOW with type t := 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
include Datatype_sig.COMPARABLE with type t := t
include Datatype_sig.COMPARISON with type t := t
val compare : t -> t -> int
val equal : t -> t -> bool
include Datatype_sig.COLLECTIONS with type t := t
module Set = ID.Set

Set over type t

module MonoList = ID.MonoList

Monomorphic list over type t

module Map = ID.Map

Polymorphic map from t to 'a

module MonoMap = ID.MonoMap

Monomorphic map from t to Data.t

val hash : t -> int
val name : t -> string
val header : t -> SL.Variable.t list
val cases : ?refresh:bool -> ?base_only:bool -> ?params:SL.Term.t list -> t -> SL.t list

Return a list of formula used in definition.

  • parameter refresh

    Refresh name of existential variables inside each definition (default true)

  • parameter base_only

    Only base cases (default false)

val instantiate_rules : t -> SL.Term.t list -> SL.t list
val show : t -> string
val mk : string -> SL.Variable.t list -> SL.t -> t
val refresh : t -> t
val mk_call : t -> SL.Term.t list -> SL.t
val arity : t -> int
val fields : t -> MemoryModel.Field.t list
val dependencies : t -> string list

Return names of predicates used in inductive cases.

val is_ite : t -> bool
val map : (SL.t -> SL.t) -> t -> t
val map_cases : (SL.t -> SL.t) -> t -> t
val to_formula : ?params:SL.Term.t list -> t -> SL.t

Create a call of the given inductive definitions.

If not parameters are provided, formal parameters will be used

val instantiate : refresh:bool -> t -> SL.Term.t list -> SL.t
val instantiate_formals : ?refresh:bool -> t -> SL.t
val unfold_finite : t -> SL.Term.t list -> SL.t
val smt2_decl : t -> string
val ls : ID.t

Singly-linked list

val ls_two_plus : ID.t

Singly-linked list of length 2+

val dls : ID.t

Doubly-linked list

val dls_simple : ID.t

Three-parameter DLS

val dls_simple_two_plus : ID.t

Three-parameter DLS

val dls_three_plus : ID.t

Doubly-linked list of length 3+

val nls : ID.t
val nls_two_plus : ID.t