69 open Hints_declaration
86 | EVint of AST.intsize * AST.bvint
88 val eventval_rect_Type4 :
89 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
91 val eventval_rect_Type5 :
92 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
94 val eventval_rect_Type3 :
95 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
97 val eventval_rect_Type2 :
98 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
100 val eventval_rect_Type1 :
101 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
103 val eventval_rect_Type0 :
104 (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
106 val eventval_inv_rect_Type4 :
107 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
109 val eventval_inv_rect_Type3 :
110 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
112 val eventval_inv_rect_Type2 :
113 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
115 val eventval_inv_rect_Type1 :
116 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
118 val eventval_inv_rect_Type0 :
119 eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
121 val eventval_discr : eventval -> eventval -> __
123 val eventval_jmdiscr : eventval -> eventval -> __
126 | EVcost of CostLabel.costlabel
127 | EVextcall of AST.ident * eventval List.list * eventval
129 val event_rect_Type4 :
130 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
131 eventval -> 'a1) -> event -> 'a1
133 val event_rect_Type5 :
134 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
135 eventval -> 'a1) -> event -> 'a1
137 val event_rect_Type3 :
138 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
139 eventval -> 'a1) -> event -> 'a1
141 val event_rect_Type2 :
142 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
143 eventval -> 'a1) -> event -> 'a1
145 val event_rect_Type1 :
146 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
147 eventval -> 'a1) -> event -> 'a1
149 val event_rect_Type0 :
150 (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
151 eventval -> 'a1) -> event -> 'a1
153 val event_inv_rect_Type4 :
154 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
155 List.list -> eventval -> __ -> 'a1) -> 'a1
157 val event_inv_rect_Type3 :
158 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
159 List.list -> eventval -> __ -> 'a1) -> 'a1
161 val event_inv_rect_Type2 :
162 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
163 List.list -> eventval -> __ -> 'a1) -> 'a1
165 val event_inv_rect_Type1 :
166 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
167 List.list -> eventval -> __ -> 'a1) -> 'a1
169 val event_inv_rect_Type0 :
170 event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
171 List.list -> eventval -> __ -> 'a1) -> 'a1
173 val event_discr : event -> event -> __
175 val event_jmdiscr : event -> event -> __
177 type trace = event List.list
181 val echarge : CostLabel.costlabel -> trace
183 val eextcall : AST.ident -> eventval List.list -> eventval -> trace
185 val eapp : trace -> trace -> trace
187 type traceinf = __traceinf Lazy.t
189 | Econsinf of event * traceinf
191 val traceinf_inv_rect_Type4 :
192 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
194 val traceinf_inv_rect_Type3 :
195 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
197 val traceinf_inv_rect_Type2 :
198 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
200 val traceinf_inv_rect_Type1 :
201 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
203 val traceinf_inv_rect_Type0 :
204 traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
206 val traceinf_discr : traceinf -> traceinf -> __
208 val traceinf_jmdiscr : traceinf -> traceinf -> __
210 val eappinf : trace -> traceinf -> traceinf
212 val remove_costs : trace -> trace
214 type traceinf' = __traceinf' Lazy.t
216 | Econsinf' of trace * traceinf'
218 val traceinf'_inv_rect_Type4 :
219 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
221 val traceinf'_inv_rect_Type3 :
222 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
224 val traceinf'_inv_rect_Type2 :
225 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
227 val traceinf'_inv_rect_Type1 :
228 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
230 val traceinf'_inv_rect_Type0 :
231 traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
233 val traceinf'_discr : traceinf' -> traceinf' -> __
235 val traceinf'_jmdiscr : traceinf' -> traceinf' -> __
237 val split_traceinf' : trace -> traceinf' -> (event, traceinf') Types.prod
239 val traceinf_of_traceinf' : traceinf' -> traceinf