Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899(* This file is free software, part of Archsat. See file "LICENSE" for more details. *)
(** Expressions
This modules defines the smallest signatures for expressions that allow to instantiates the {Pipes.Make} functor. *)
module type S = sig
type ty type ty_var type ty_cst type ty_def
type term type term_var type term_cst
type formula
end
module type Print = sig
include S
val ty : Format.formatter -> ty -> unit val ty_var : Format.formatter -> ty_var -> unit val ty_cst : Format.formatter -> ty_cst -> unit val ty_def : Format.formatter -> ty_def -> unit
val term : Format.formatter -> term -> unit val term_var : Format.formatter -> term_var -> unit val term_cst : Format.formatter -> term_cst -> unit
val formula : Format.formatter -> formula -> unit
end
module type Export = sig
include S
type 'a tag
module Tags : sig
val named : string tag
end
module Ty : sig type t = ty module Var : sig include Dolmen_intf.Id.Scope with type t = ty_var and type path := Dolmen_std.Path.t end module Const : sig include Dolmen_intf.Id.Scope with type t = ty_cst and type path := Dolmen_std.Path.t end end
module Term : sig type t = term
val neg : t -> t (** Logical negation. *)
val _or : t list -> t (** Disjunction. *)
val of_cst : term_cst -> t (** Create a formula out of a constant. *)
module Var : sig include Dolmen_intf.Id.Scope with type t = term_var and type path := Dolmen_std.Path.t end
module Const : sig include Dolmen_intf.Id.Scope with type t = term_cst and type path := Dolmen_std.Path.t
val mk : Dolmen_std.Path.t -> ty -> t (** Create a constant symbol *)
val get_tag : t -> 'a tag -> 'a option (** Return the value bound to a tag (if any). *) end end
end