## cool / src / lib / CoAlgFormula.mli @ de84f40d

History | View | Annotate | Download (6.02 KB)

1 | 4fd28192 | Thorsten Wißmann | (** 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 | e5422169 | Thorsten Wißmann | type rational = { nominator: int; denominator: int } |

12 | |||

13 | val rational_of_int : int -> int -> rational |
||

14 | |||

15 | 4fd28192 | Thorsten Wißmann | type formula = |

16 | | TRUE |
||

17 | | FALSE |
||

18 | 0247525c | Thorsten Wißmann | | AP of string (* named atom *) |

19 | 4fd28192 | Thorsten Wißmann | | NOT of formula |

20 | 0247525c | Thorsten Wißmann | | AT of string * formula (* @ *) |

21 | 4fd28192 | Thorsten Wißmann | | OR of formula * formula |

22 | | AND of formula * formula |
||

23 | 0247525c | Thorsten Wißmann | | EQU of formula * formula (* equivalence <=> *) |

24 | | IMP of formula * formula (* implication <-> *) |
||

25 | | EX of string * formula (* exists, diamond of K *) |
||

26 | | AX of string * formula (* forall, box of K *) |
||

27 | | ENFORCES of int list * formula (* CL *) |
||

28 | | ALLOWS of int list * formula (* CL *) |
||

29 | | MIN of int * string * formula (* some more intuitive diamond for GML *) |
||

30 | | MAX of int * string * formula (* some more intuitive box for GML *) |
||

31 | af276a36 | Thorsten Wißmann | | MORETHAN of int * string * formula (* diamond of GML *) |

32 | dbcce612 | Thorsten Wißmann | | MAXEXCEPT of int * string * formula (* box of GML, means: ¬>_nR.¬C *) |

33 | c855ba91 | Thorsten Wißmann | | ATLEASTPROB of rational * formula (* = {>= 1/2} C ---> C occurs with *) |

34 | e5422169 | Thorsten Wißmann | (* probability of at least 50% *) |

35 | 9bae2c4f | Thorsten Wißmann | | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *) |

36 | c49eea11 | Thorsten Wißmann | (* probability of less than 50% *) |

37 | | CONST of string (* constant functor with value string *) |
||

38 | | CONSTN of string (* constant functor with value other than string *) |
||

39 | 19f5dad0 | Dirk Pattinson | | ID of formula (* modality of the identity functor *) |

40 | | NORM of formula * formula (* default implication *) |
||

41 | | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *) |
||

42 | 4fd28192 | Thorsten Wißmann | | CHC of formula * formula |

43 | | FUS of bool * formula |
||

44 | d29d35f7 | Christoph Egger | | MU of string * formula |

45 | | NU of string * formula |
||

46 | 9a3b23cc | Christoph Egger | | VAR of string |

47 | b179a57f | Christoph Egger | | AF of formula |

48 | | EF of formula |
||

49 | | AG of formula |
||

50 | | EG of formula |
||

51 | | AU of formula * formula |
||

52 | | EU of formula * formula |
||

53 | 4fd28192 | Thorsten Wißmann | |

54 | ca99d0c6 | Thorsten Wißmann | exception ConversionException of formula |

55 | |||

56 | 4fd28192 | Thorsten Wißmann | type sortedFormula = sort * formula |

57 | |||

58 | dbcce612 | Thorsten Wißmann | val iter : (formula -> unit) -> formula -> unit (* iterate over all sub formulas *) |

59 | val convert_post : (formula -> formula) -> formula -> formula (* run over all subformulas in post order *) |
||

60 | val convertToK : formula -> formula (* tries to convert a formula to a pure K formula *) |
||

61 | val convertToGML : formula -> formula (* tries to convert a formula to a pure GML formula *) |
||

62 | |||

63 | 4fd28192 | Thorsten Wißmann | val isNominal : string -> bool |

64 | |||

65 | val sizeFormula : formula -> int |
||

66 | val sizeSortedFormula : sortedFormula -> int |
||

67 | |||

68 | ca99d0c6 | Thorsten Wißmann | val string_of_formula : formula -> string |

69 | 4fd28192 | Thorsten Wißmann | val exportFormula : formula -> string |

70 | 01b1ab69 | Thorsten Wißmann | val exportTatlFormula : formula -> string |

71 | 4fd28192 | Thorsten Wißmann | val exportSortedFormula : sortedFormula -> string |

72 | val exportQuery : sortedFormula list -> sortedFormula -> string |
||

73 | b59059c4 | Thorsten Wißmann | val exportQueryParsable : sortedFormula list -> sortedFormula -> string |

74 | 4fd28192 | Thorsten Wißmann | val importFormula : string -> formula |

75 | val importSortedFormula : string -> sortedFormula |
||

76 | val importQuery : string -> sortedFormula list * sortedFormula |
||

77 | |||

78 | 1484d8cb | Christoph Egger | val verifyFormula : formula -> unit |

79 | |||

80 | 4fd28192 | Thorsten Wißmann | val nnfNeg : formula -> formula |

81 | val nnf : formula -> formula |
||

82 | |||

83 | val simplify : formula -> formula |
||

84 | |||

85 | val dest_ap : formula -> string |
||

86 | val dest_nom : formula -> string |
||

87 | val dest_not : formula -> formula |
||

88 | val dest_at : formula -> string * formula |
||

89 | val dest_or : formula -> formula * formula |
||

90 | val dest_and : formula -> formula * formula |
||

91 | val dest_equ : formula -> formula * formula |
||

92 | val dest_imp : formula -> formula * formula |
||

93 | val dest_ex : formula -> string * formula |
||

94 | val dest_ax : formula -> string * formula |
||

95 | val dest_min : formula -> int * string * formula |
||

96 | val dest_max : formula -> int * string * formula |
||

97 | val dest_choice : formula -> formula * formula |
||

98 | val dest_fusion : formula -> bool * formula |
||

99 | |||

100 | val is_true : formula -> bool |
||

101 | val is_false : formula -> bool |
||

102 | val is_ap : formula -> bool |
||

103 | val is_nom : formula -> bool |
||

104 | val is_not : formula -> bool |
||

105 | val is_at : formula -> bool |
||

106 | val is_or : formula -> bool |
||

107 | val is_and : formula -> bool |
||

108 | val is_equ : formula -> bool |
||

109 | val is_imp : formula -> bool |
||

110 | val is_ex : formula -> bool |
||

111 | val is_ax : formula -> bool |
||

112 | val is_min : formula -> bool |
||

113 | val is_max : formula -> bool |
||

114 | val is_choice : formula -> bool |
||

115 | val is_fusion : formula -> bool |
||

116 | dbcce612 | Thorsten Wißmann | |

117 | 4fd28192 | Thorsten Wißmann | val const_true : formula |

118 | val const_false : formula |
||

119 | val const_ap : string -> formula |
||

120 | val const_nom : string -> formula |
||

121 | val const_not : formula -> formula |
||

122 | val const_at : string -> formula -> formula |
||

123 | val const_or : formula -> formula -> formula |
||

124 | val const_and : formula -> formula -> formula |
||

125 | val const_equ : formula -> formula -> formula |
||

126 | val const_imp : formula -> formula -> formula |
||

127 | val const_ex : string -> formula -> formula |
||

128 | val const_ax : string -> formula -> formula |
||

129 | val const_min : int -> string -> formula -> formula |
||

130 | val const_max : int -> string -> formula -> formula |
||

131 | 7993e0bf | Thorsten Wißmann | val const_enforces : int list -> formula -> formula |

132 | val const_allows : int list -> formula -> formula |
||

133 | 4fd28192 | Thorsten Wißmann | val const_choice : formula -> formula -> formula |

134 | val const_fusion : bool -> formula -> formula |
||

135 | |||

136 | type hcFormula = (hcFormula_node, formula) HashConsing.hash_consed |
||

137 | and hcFormula_node = |
||

138 | | HCTRUE |
||

139 | | HCFALSE |
||

140 | | HCAP of string |
||

141 | | HCNOT of string |
||

142 | | HCAT of string * hcFormula |
||

143 | | HCOR of hcFormula * hcFormula |
||

144 | | HCAND of hcFormula * hcFormula |
||

145 | | HCEX of string * hcFormula |
||

146 | | HCAX of string * hcFormula |
||

147 | f1fa9ad5 | Thorsten Wißmann | | HCENFORCES of int list * hcFormula |

148 | | HCALLOWS of int list * hcFormula |
||

149 | af276a36 | Thorsten Wißmann | | HCMORETHAN of int * string * hcFormula (* GML Diamond *) |

150 | | HCMAXEXCEPT of int * string * hcFormula (* GML Box *) |
||

151 | 86b07be8 | Thorsten Wißmann | | HCATLEASTPROB of rational * hcFormula |

152 | 9bae2c4f | Thorsten Wißmann | | HCLESSPROBFAIL of rational * hcFormula (* the probability for failing is less than ... *) |

153 | c49eea11 | Thorsten Wißmann | | HCCONST of string |

154 | | HCCONSTN of string |
||

155 | 19f5dad0 | Dirk Pattinson | | HCID of hcFormula |

156 | | HCNORM of hcFormula * hcFormula |
||

157 | | HCNORMN of hcFormula * hcFormula |
||

158 | 4fd28192 | Thorsten Wißmann | | HCCHC of hcFormula * hcFormula |

159 | | HCFUS of bool * hcFormula |
||

160 | 87d5082f | Christoph Egger | | HCMU of string * hcFormula |

161 | | HCNU of string * hcFormula |
||

162 | | HCVAR of string |
||

163 | 4fd28192 | Thorsten Wißmann | |

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

165 | |||

166 | val hc_formula : HcFormula.t -> formula -> hcFormula |
||

167 | cc07e93d | Christoph Egger | val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula |

168 | 5e7c8aa1 | Christoph Egger | val hc_freeIn : string -> hcFormula -> bool |

169 | 4fd28192 | Thorsten Wißmann | |

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