Source file expr_intf.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
(* 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 isntantiates the {Pipes.Make} functor. *)

module type S = sig

  type ty
  type ty_var
  type ty_cst

  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 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