Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
(** Interfaces for Tags. Tags are used to attach arbitrary information to ndoes in an ast. *)
(** Base signature for tags. *)module type S = sig
type 'a t (** Polymorphic tags *)
val create : ?print:('a Pretty.print) -> unit -> 'a t (** Create a new tag. *)
end
(** Minium required signature for tags to typecheck Alt-Ergo's core/base theory. *)module type Ae_Base = sig
type term (** The type of terms *)
type 'a t (** Polymorphic tags *)
val predicate : unit t (** A flag (i.e. unit tag), indicating that the declaration is a predicate *)
val ac : unit t (** A flag (i.e. unit tag), indicating that the tagged term/formula is to be considered as a associative and commutative term. *)
val named : string t (** A tag used to name formulas in alt-ergo. *)
val triggers : term list t (** Multi-triggers that can be added to quantified formulas. Each term is a multi-trigger represented as a conjunction of triggers. *)
val filters : term list t (** Filters that can be added to quantified formulas *)
end
(** Minium required signature for tags to typecheck smtlib's core/base theory. *)module type Smtlib_Base = sig
type term (** The type of terms *)
type 'a t (** Polymorphic tags *)
val named : string t (** A tag used to named formulas in smtlib. Should correspond to the `:named` attribute. *)
val triggers : term list t (** Multi-triggers (typically annotated on the body of a quantified formula and not the quantified formula itself). Each term is a multi-trigger represented as a conjunction of triggers. *)
val rwrt : unit t (** A flag (i.e. unit tag), indicating that the tagged term/formula is to be considered as a rewrite rule. *)
end
(** Tags *)module type Zf_Base = sig
type 'a t (** Polymorphic tags *)
val rwrt : unit t (** A flag (i.e. unit tag), indicatgin that the tagged term/formula is to be considered as a rewrite rule. *)
type name (** A type used to specify a name for printing identifiers *)
val name : name t (** A tag used to specify what to print when printing an identifier *)
val exact : string -> name (** Print the identifier with this exact string. *)
type pos (** A type to indicate how to print identifiers *)
val pos : pos t (** A tag to specify how to print identifiers*)
val infix : pos (** The tagged identifier is an infix symbol *)
val prefix : pos (** The tagged identifier is a prefix symbol *)
end