[2601] | 1 | open Preamble |
---|
| 2 | |
---|
| 3 | open Proper |
---|
| 4 | |
---|
| 5 | open PositiveMap |
---|
| 6 | |
---|
| 7 | open Deqsets |
---|
| 8 | |
---|
| 9 | open Extralib |
---|
| 10 | |
---|
| 11 | open Lists |
---|
| 12 | |
---|
| 13 | open Identifiers |
---|
| 14 | |
---|
| 15 | open Integers |
---|
| 16 | |
---|
| 17 | open AST |
---|
| 18 | |
---|
| 19 | open Division |
---|
| 20 | |
---|
[2717] | 21 | open Exp |
---|
| 22 | |
---|
[2601] | 23 | open Arithmetic |
---|
| 24 | |
---|
| 25 | open Extranat |
---|
| 26 | |
---|
| 27 | open Vector |
---|
| 28 | |
---|
| 29 | open FoldStuff |
---|
| 30 | |
---|
| 31 | open BitVector |
---|
| 32 | |
---|
| 33 | open Z |
---|
| 34 | |
---|
| 35 | open BitVectorZ |
---|
| 36 | |
---|
| 37 | open Pointers |
---|
| 38 | |
---|
[2649] | 39 | open ErrorMessages |
---|
| 40 | |
---|
[2601] | 41 | open Option |
---|
| 42 | |
---|
| 43 | open Setoids |
---|
| 44 | |
---|
| 45 | open Monad |
---|
| 46 | |
---|
| 47 | open Positive |
---|
| 48 | |
---|
| 49 | open PreIdentifiers |
---|
| 50 | |
---|
| 51 | open Errors |
---|
| 52 | |
---|
| 53 | open Div_and_mod |
---|
| 54 | |
---|
| 55 | open Jmeq |
---|
| 56 | |
---|
| 57 | open Russell |
---|
| 58 | |
---|
| 59 | open Util |
---|
| 60 | |
---|
| 61 | open Bool |
---|
| 62 | |
---|
| 63 | open Relations |
---|
| 64 | |
---|
| 65 | open Nat |
---|
| 66 | |
---|
| 67 | open List |
---|
| 68 | |
---|
| 69 | open Hints_declaration |
---|
| 70 | |
---|
| 71 | open Core_notation |
---|
| 72 | |
---|
| 73 | open Pts |
---|
| 74 | |
---|
| 75 | open Logic |
---|
| 76 | |
---|
| 77 | open Types |
---|
| 78 | |
---|
| 79 | open Coqlib |
---|
| 80 | |
---|
| 81 | open Values |
---|
| 82 | |
---|
[2717] | 83 | open BitVectorTrie |
---|
| 84 | |
---|
[2601] | 85 | open CostLabel |
---|
| 86 | |
---|
| 87 | type eventval = |
---|
| 88 | | EVint of AST.intsize * AST.bvint |
---|
| 89 | |
---|
| 90 | (** val eventval_rect_Type4 : |
---|
| 91 | (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **) |
---|
| 92 | let rec eventval_rect_Type4 h_EVint = function |
---|
[2730] | 93 | | EVint (sz, x_4706) -> h_EVint sz x_4706 |
---|
[2601] | 94 | |
---|
| 95 | (** val eventval_rect_Type5 : |
---|
| 96 | (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **) |
---|
| 97 | let rec eventval_rect_Type5 h_EVint = function |
---|
[2730] | 98 | | EVint (sz, x_4709) -> h_EVint sz x_4709 |
---|
[2601] | 99 | |
---|
| 100 | (** val eventval_rect_Type3 : |
---|
| 101 | (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **) |
---|
| 102 | let rec eventval_rect_Type3 h_EVint = function |
---|
[2730] | 103 | | EVint (sz, x_4712) -> h_EVint sz x_4712 |
---|
[2601] | 104 | |
---|
| 105 | (** val eventval_rect_Type2 : |
---|
| 106 | (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **) |
---|
| 107 | let rec eventval_rect_Type2 h_EVint = function |
---|
[2730] | 108 | | EVint (sz, x_4715) -> h_EVint sz x_4715 |
---|
[2601] | 109 | |
---|
| 110 | (** val eventval_rect_Type1 : |
---|
| 111 | (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **) |
---|
| 112 | let rec eventval_rect_Type1 h_EVint = function |
---|
[2730] | 113 | | EVint (sz, x_4718) -> h_EVint sz x_4718 |
---|
[2601] | 114 | |
---|
| 115 | (** val eventval_rect_Type0 : |
---|
| 116 | (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **) |
---|
| 117 | let rec eventval_rect_Type0 h_EVint = function |
---|
[2730] | 118 | | EVint (sz, x_4721) -> h_EVint sz x_4721 |
---|
[2601] | 119 | |
---|
| 120 | (** val eventval_inv_rect_Type4 : |
---|
| 121 | eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **) |
---|
| 122 | let eventval_inv_rect_Type4 hterm h1 = |
---|
| 123 | let hcut = eventval_rect_Type4 h1 hterm in hcut __ |
---|
| 124 | |
---|
| 125 | (** val eventval_inv_rect_Type3 : |
---|
| 126 | eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **) |
---|
| 127 | let eventval_inv_rect_Type3 hterm h1 = |
---|
| 128 | let hcut = eventval_rect_Type3 h1 hterm in hcut __ |
---|
| 129 | |
---|
| 130 | (** val eventval_inv_rect_Type2 : |
---|
| 131 | eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **) |
---|
| 132 | let eventval_inv_rect_Type2 hterm h1 = |
---|
| 133 | let hcut = eventval_rect_Type2 h1 hterm in hcut __ |
---|
| 134 | |
---|
| 135 | (** val eventval_inv_rect_Type1 : |
---|
| 136 | eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **) |
---|
| 137 | let eventval_inv_rect_Type1 hterm h1 = |
---|
| 138 | let hcut = eventval_rect_Type1 h1 hterm in hcut __ |
---|
| 139 | |
---|
| 140 | (** val eventval_inv_rect_Type0 : |
---|
| 141 | eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **) |
---|
| 142 | let eventval_inv_rect_Type0 hterm h1 = |
---|
| 143 | let hcut = eventval_rect_Type0 h1 hterm in hcut __ |
---|
| 144 | |
---|
| 145 | (** val eventval_discr : eventval -> eventval -> __ **) |
---|
| 146 | let eventval_discr x y = |
---|
| 147 | Logic.eq_rect_Type2 x |
---|
| 148 | (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y |
---|
| 149 | |
---|
| 150 | (** val eventval_jmdiscr : eventval -> eventval -> __ **) |
---|
| 151 | let eventval_jmdiscr x y = |
---|
| 152 | Logic.eq_rect_Type2 x |
---|
| 153 | (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y |
---|
| 154 | |
---|
| 155 | type event = |
---|
| 156 | | EVcost of CostLabel.costlabel |
---|
| 157 | | EVextcall of AST.ident * eventval List.list * eventval |
---|
| 158 | |
---|
| 159 | (** val event_rect_Type4 : |
---|
| 160 | (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list -> |
---|
| 161 | eventval -> 'a1) -> event -> 'a1 **) |
---|
| 162 | let rec event_rect_Type4 h_EVcost h_EVextcall = function |
---|
[2730] | 163 | | EVcost x_4746 -> h_EVcost x_4746 |
---|
[2601] | 164 | | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res |
---|
| 165 | |
---|
| 166 | (** val event_rect_Type5 : |
---|
| 167 | (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list -> |
---|
| 168 | eventval -> 'a1) -> event -> 'a1 **) |
---|
| 169 | let rec event_rect_Type5 h_EVcost h_EVextcall = function |
---|
[2730] | 170 | | EVcost x_4750 -> h_EVcost x_4750 |
---|
[2601] | 171 | | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res |
---|
| 172 | |
---|
| 173 | (** val event_rect_Type3 : |
---|
| 174 | (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list -> |
---|
| 175 | eventval -> 'a1) -> event -> 'a1 **) |
---|
| 176 | let rec event_rect_Type3 h_EVcost h_EVextcall = function |
---|
[2730] | 177 | | EVcost x_4754 -> h_EVcost x_4754 |
---|
[2601] | 178 | | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res |
---|
| 179 | |
---|
| 180 | (** val event_rect_Type2 : |
---|
| 181 | (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list -> |
---|
| 182 | eventval -> 'a1) -> event -> 'a1 **) |
---|
| 183 | let rec event_rect_Type2 h_EVcost h_EVextcall = function |
---|
[2730] | 184 | | EVcost x_4758 -> h_EVcost x_4758 |
---|
[2601] | 185 | | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res |
---|
| 186 | |
---|
| 187 | (** val event_rect_Type1 : |
---|
| 188 | (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list -> |
---|
| 189 | eventval -> 'a1) -> event -> 'a1 **) |
---|
| 190 | let rec event_rect_Type1 h_EVcost h_EVextcall = function |
---|
[2730] | 191 | | EVcost x_4762 -> h_EVcost x_4762 |
---|
[2601] | 192 | | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res |
---|
| 193 | |
---|
| 194 | (** val event_rect_Type0 : |
---|
| 195 | (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list -> |
---|
| 196 | eventval -> 'a1) -> event -> 'a1 **) |
---|
| 197 | let rec event_rect_Type0 h_EVcost h_EVextcall = function |
---|
[2730] | 198 | | EVcost x_4766 -> h_EVcost x_4766 |
---|
[2601] | 199 | | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res |
---|
| 200 | |
---|
| 201 | (** val event_inv_rect_Type4 : |
---|
| 202 | event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval |
---|
| 203 | List.list -> eventval -> __ -> 'a1) -> 'a1 **) |
---|
| 204 | let event_inv_rect_Type4 hterm h1 h2 = |
---|
| 205 | let hcut = event_rect_Type4 h1 h2 hterm in hcut __ |
---|
| 206 | |
---|
| 207 | (** val event_inv_rect_Type3 : |
---|
| 208 | event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval |
---|
| 209 | List.list -> eventval -> __ -> 'a1) -> 'a1 **) |
---|
| 210 | let event_inv_rect_Type3 hterm h1 h2 = |
---|
| 211 | let hcut = event_rect_Type3 h1 h2 hterm in hcut __ |
---|
| 212 | |
---|
| 213 | (** val event_inv_rect_Type2 : |
---|
| 214 | event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval |
---|
| 215 | List.list -> eventval -> __ -> 'a1) -> 'a1 **) |
---|
| 216 | let event_inv_rect_Type2 hterm h1 h2 = |
---|
| 217 | let hcut = event_rect_Type2 h1 h2 hterm in hcut __ |
---|
| 218 | |
---|
| 219 | (** val event_inv_rect_Type1 : |
---|
| 220 | event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval |
---|
| 221 | List.list -> eventval -> __ -> 'a1) -> 'a1 **) |
---|
| 222 | let event_inv_rect_Type1 hterm h1 h2 = |
---|
| 223 | let hcut = event_rect_Type1 h1 h2 hterm in hcut __ |
---|
| 224 | |
---|
| 225 | (** val event_inv_rect_Type0 : |
---|
| 226 | event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval |
---|
| 227 | List.list -> eventval -> __ -> 'a1) -> 'a1 **) |
---|
| 228 | let event_inv_rect_Type0 hterm h1 h2 = |
---|
| 229 | let hcut = event_rect_Type0 h1 h2 hterm in hcut __ |
---|
| 230 | |
---|
| 231 | (** val event_discr : event -> event -> __ **) |
---|
| 232 | let event_discr x y = |
---|
| 233 | Logic.eq_rect_Type2 x |
---|
| 234 | (match x with |
---|
| 235 | | EVcost a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 236 | | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
| 237 | |
---|
| 238 | (** val event_jmdiscr : event -> event -> __ **) |
---|
| 239 | let event_jmdiscr x y = |
---|
| 240 | Logic.eq_rect_Type2 x |
---|
| 241 | (match x with |
---|
| 242 | | EVcost a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 243 | | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
| 244 | |
---|
| 245 | type trace = event List.list |
---|
| 246 | |
---|
| 247 | (** val e0 : trace **) |
---|
| 248 | let e0 = |
---|
| 249 | List.Nil |
---|
| 250 | |
---|
| 251 | (** val echarge : CostLabel.costlabel -> trace **) |
---|
| 252 | let echarge label = |
---|
| 253 | List.Cons ((EVcost label), List.Nil) |
---|
| 254 | |
---|
| 255 | (** val eextcall : AST.ident -> eventval List.list -> eventval -> trace **) |
---|
| 256 | let eextcall name args res1 = |
---|
| 257 | List.Cons ((EVextcall (name, args, res1)), List.Nil) |
---|
| 258 | |
---|
| 259 | (** val eapp : trace -> trace -> trace **) |
---|
| 260 | let eapp t1 t2 = |
---|
| 261 | List.append t1 t2 |
---|
| 262 | |
---|
| 263 | type traceinf = __traceinf Lazy.t |
---|
| 264 | and __traceinf = |
---|
| 265 | | Econsinf of event * traceinf |
---|
| 266 | |
---|
| 267 | (** val traceinf_inv_rect_Type4 : |
---|
| 268 | traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **) |
---|
| 269 | let traceinf_inv_rect_Type4 hterm h1 = |
---|
| 270 | let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __ |
---|
| 271 | |
---|
| 272 | (** val traceinf_inv_rect_Type3 : |
---|
| 273 | traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **) |
---|
| 274 | let traceinf_inv_rect_Type3 hterm h1 = |
---|
| 275 | let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __ |
---|
| 276 | |
---|
| 277 | (** val traceinf_inv_rect_Type2 : |
---|
| 278 | traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **) |
---|
| 279 | let traceinf_inv_rect_Type2 hterm h1 = |
---|
| 280 | let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __ |
---|
| 281 | |
---|
| 282 | (** val traceinf_inv_rect_Type1 : |
---|
| 283 | traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **) |
---|
| 284 | let traceinf_inv_rect_Type1 hterm h1 = |
---|
| 285 | let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __ |
---|
| 286 | |
---|
| 287 | (** val traceinf_inv_rect_Type0 : |
---|
| 288 | traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **) |
---|
| 289 | let traceinf_inv_rect_Type0 hterm h1 = |
---|
| 290 | let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __ |
---|
| 291 | |
---|
| 292 | (** val traceinf_discr : traceinf -> traceinf -> __ **) |
---|
| 293 | let traceinf_discr x y = |
---|
| 294 | Logic.eq_rect_Type2 x |
---|
| 295 | (let Econsinf (a0, a1) = Lazy.force x in |
---|
| 296 | Obj.magic (fun _ dH -> dH __ __)) y |
---|
| 297 | |
---|
| 298 | (** val traceinf_jmdiscr : traceinf -> traceinf -> __ **) |
---|
| 299 | let traceinf_jmdiscr x y = |
---|
| 300 | Logic.eq_rect_Type2 x |
---|
| 301 | (let Econsinf (a0, a1) = Lazy.force x in |
---|
| 302 | Obj.magic (fun _ dH -> dH __ __)) y |
---|
| 303 | |
---|
| 304 | (** val eappinf : trace -> traceinf -> traceinf **) |
---|
| 305 | let rec eappinf t t0 = |
---|
| 306 | match t with |
---|
| 307 | | List.Nil -> t0 |
---|
| 308 | | List.Cons (ev, t') -> lazy (Econsinf (ev, (eappinf t' t0))) |
---|
| 309 | |
---|
| 310 | (** val remove_costs : trace -> trace **) |
---|
| 311 | let remove_costs = |
---|
| 312 | List.filter (fun e1 -> |
---|
| 313 | match e1 with |
---|
| 314 | | EVcost x -> Bool.False |
---|
| 315 | | EVextcall (x, x0, x1) -> Bool.True) |
---|
| 316 | |
---|
| 317 | type traceinf' = __traceinf' Lazy.t |
---|
| 318 | and __traceinf' = |
---|
| 319 | | Econsinf' of trace * traceinf' |
---|
| 320 | |
---|
| 321 | (** val traceinf'_inv_rect_Type4 : |
---|
| 322 | traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 323 | let traceinf'_inv_rect_Type4 hterm h1 = |
---|
| 324 | let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in |
---|
| 325 | hcut __ |
---|
| 326 | |
---|
| 327 | (** val traceinf'_inv_rect_Type3 : |
---|
| 328 | traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 329 | let traceinf'_inv_rect_Type3 hterm h1 = |
---|
| 330 | let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in |
---|
| 331 | hcut __ |
---|
| 332 | |
---|
| 333 | (** val traceinf'_inv_rect_Type2 : |
---|
| 334 | traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 335 | let traceinf'_inv_rect_Type2 hterm h1 = |
---|
| 336 | let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in |
---|
| 337 | hcut __ |
---|
| 338 | |
---|
| 339 | (** val traceinf'_inv_rect_Type1 : |
---|
| 340 | traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 341 | let traceinf'_inv_rect_Type1 hterm h1 = |
---|
| 342 | let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in |
---|
| 343 | hcut __ |
---|
| 344 | |
---|
| 345 | (** val traceinf'_inv_rect_Type0 : |
---|
| 346 | traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 347 | let traceinf'_inv_rect_Type0 hterm h1 = |
---|
| 348 | let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in |
---|
| 349 | hcut __ |
---|
| 350 | |
---|
| 351 | (** val traceinf'_discr : traceinf' -> traceinf' -> __ **) |
---|
| 352 | let traceinf'_discr x y = |
---|
| 353 | Logic.eq_rect_Type2 x |
---|
| 354 | (let Econsinf' (a0, a1) = Lazy.force x in |
---|
| 355 | Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
| 356 | |
---|
| 357 | (** val traceinf'_jmdiscr : traceinf' -> traceinf' -> __ **) |
---|
| 358 | let traceinf'_jmdiscr x y = |
---|
| 359 | Logic.eq_rect_Type2 x |
---|
| 360 | (let Econsinf' (a0, a1) = Lazy.force x in |
---|
| 361 | Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
| 362 | |
---|
| 363 | (** val split_traceinf' : |
---|
| 364 | trace -> traceinf' -> (event, traceinf') Types.prod **) |
---|
| 365 | let split_traceinf' t t0 = |
---|
| 366 | (match t with |
---|
| 367 | | List.Nil -> (fun _ -> Logic.false_rect_Type0 __) |
---|
| 368 | | List.Cons (e1, t') -> |
---|
| 369 | (fun _ -> |
---|
| 370 | (match t' with |
---|
| 371 | | List.Nil -> (fun _ -> { Types.fst = e1; Types.snd = t0 }) |
---|
| 372 | | List.Cons (e', t'') -> |
---|
| 373 | (fun _ -> { Types.fst = e1; Types.snd = (lazy (Econsinf' (t', |
---|
| 374 | t0))) })) __)) __ |
---|
| 375 | |
---|
| 376 | (** val traceinf_of_traceinf' : traceinf' -> traceinf **) |
---|
| 377 | let rec traceinf_of_traceinf' t' = |
---|
| 378 | let Econsinf' (t, t'') = Lazy.force t' in |
---|
| 379 | let { Types.fst = e1; Types.snd = tl } = split_traceinf' t t'' in |
---|
| 380 | lazy (Econsinf (e1, (traceinf_of_traceinf' tl))) |
---|
| 381 | |
---|