Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.mli @ 7c4d2eb4

History | View | Annotate | Download (4.01 KB)

1
(** This module implements coalgebraic formulae
2
    (e.g. parsing, printing, (de-)constructing, ...).
3
    @author Florian Widmann
4
 *)
5

    
6

    
7
exception CoAlgException of string
8

    
9
type sort = int
10

    
11
type formula =
12
  | TRUE
13
  | FALSE
14
  | AP of string
15
  | NOT of formula
16
  | AT of string * formula
17
  | OR of formula * formula
18
  | AND of formula * formula
19
  | EQU of formula * formula
20
  | IMP of formula * formula
21
  | EX of string * formula
22
  | AX of string * formula
23
  | ENFORCES of int list * formula
24
  | ALLOWS   of int list * formula
25
  | MIN of int * string * formula
26
  | MAX of int * string * formula
27
  | MORETHAN of int * string * formula (* diamond of GML *)
28
  | MAXEXCEPT of int * string * formula (* box of GML *)
29
  | CHC of formula * formula
30
  | CHCN of formula * formula
31
  | FUS of bool * formula
32

    
33
type sortedFormula = sort * formula
34

    
35
val isNominal : string -> bool
36

    
37
val sizeFormula : formula -> int
38
val sizeSortedFormula : sortedFormula -> int
39

    
40
val exportFormula : formula -> string
41
val exportTatlFormula : formula -> string
42
val exportSortedFormula : sortedFormula -> string
43
val exportQuery : sortedFormula list -> sortedFormula -> string
44
val exportQueryParsable : sortedFormula list -> sortedFormula -> string
45
val importFormula : string -> formula
46
val importSortedFormula : string -> sortedFormula
47
val importQuery : string -> sortedFormula list * sortedFormula
48

    
49
val nnfNeg : formula -> formula
50
val nnf : formula -> formula
51

    
52
val simplify : formula -> formula
53

    
54
val dest_ap : formula -> string
55
val dest_nom : formula -> string
56
val dest_not : formula -> formula
57
val dest_at : formula -> string * formula
58
val dest_or : formula -> formula * formula
59
val dest_and : formula -> formula * formula
60
val dest_equ : formula -> formula * formula
61
val dest_imp : formula -> formula * formula
62
val dest_ex : formula -> string * formula
63
val dest_ax : formula -> string * formula
64
val dest_min : formula -> int * string * formula
65
val dest_max : formula -> int * string * formula
66
val dest_choice : formula -> formula * formula
67
val dest_fusion : formula -> bool * formula
68

    
69
val is_true : formula -> bool
70
val is_false : formula -> bool
71
val is_ap : formula -> bool
72
val is_nom : formula -> bool
73
val is_not : formula -> bool
74
val is_at : formula -> bool
75
val is_or : formula -> bool
76
val is_and : formula -> bool
77
val is_equ : formula -> bool
78
val is_imp : formula -> bool
79
val is_ex : formula -> bool
80
val is_ax : formula -> bool
81
val is_min : formula -> bool
82
val is_max : formula -> bool
83
val is_choice : formula -> bool
84
val is_fusion : formula -> bool
85
        
86
val const_true : formula
87
val const_false : formula
88
val const_ap : string -> formula
89
val const_nom : string -> formula
90
val const_not : formula -> formula
91
val const_at : string -> formula -> formula
92
val const_or : formula -> formula -> formula
93
val const_and : formula -> formula -> formula
94
val const_equ : formula -> formula -> formula
95
val const_imp : formula -> formula -> formula
96
val const_ex : string -> formula -> formula
97
val const_ax : string -> formula -> formula
98
val const_min : int -> string -> formula -> formula
99
val const_max : int -> string -> formula -> formula
100
val const_enforces : int list -> formula -> formula
101
val const_allows : int list -> formula -> formula
102
val const_choice : formula -> formula -> formula
103
val const_fusion : bool -> formula -> formula
104

    
105
type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed
106
and hcFormula_node =
107
  | HCTRUE
108
  | HCFALSE
109
  | HCAP of string
110
  | HCNOT of string
111
  | HCAT of string * hcFormula
112
  | HCOR of hcFormula * hcFormula
113
  | HCAND of hcFormula * hcFormula
114
  | HCEX of string * hcFormula
115
  | HCAX of string * hcFormula
116
  | HCENFORCES of int list * hcFormula
117
  | HCALLOWS of int list * hcFormula
118
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
119
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
120
  | HCCHC of hcFormula * hcFormula
121
  | HCCHCN of hcFormula * hcFormula
122
  | HCFUS of bool * hcFormula
123

    
124
module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)
125

    
126
val hc_formula : HcFormula.t -> formula -> hcFormula
127

    
128
module HcFHt : (Hashtbl.S with type key = hcFormula)