Source file tag.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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99

(* 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 : 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 list t
  (** Multi-triggers that can be added to quantified formulas *)

  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 list t
    (** Multi-triggers (typically annotated on the body of
        a quantified formula and not the quantified formula itself). *)

    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