Changeset 2649 for extracted/aST.mli
 Timestamp:
 Feb 7, 2013, 10:43:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/aST.mli
r2601 r2649 13 13 open Arithmetic 14 14 15 open Char16 17 open String18 19 15 open Vector 20 16 … … 43 39 open Integers 44 40 45 open Coqlib46 47 open Floats48 49 41 open Proper 50 42 … … 53 45 open Deqsets 54 46 47 open ErrorMessages 48 55 49 open PreIdentifiers 56 50 … … 70 64 71 65 open Identifiers 72 73 val symbolTag : String.string74 66 75 67 type ident = PreIdentifiers.identifier … … 351 343  Init_int16 of bvint 352 344  Init_int32 of bvint 353  Init_float32 of Floats.float354  Init_float64 of Floats.float355 345  Init_space of Nat.nat 356 346  Init_null … … 358 348 359 349 val init_data_rect_Type4 : 360 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Floats.float > 'a1) 361 > (Floats.float > 'a1) > (Nat.nat > 'a1) > 'a1 > (ident > Nat.nat > 362 'a1) > init_data > 'a1 350 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Nat.nat > 'a1) > 351 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 363 352 364 353 val init_data_rect_Type5 : 365 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Floats.float > 'a1) 366 > (Floats.float > 'a1) > (Nat.nat > 'a1) > 'a1 > (ident > Nat.nat > 367 'a1) > init_data > 'a1 354 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Nat.nat > 'a1) > 355 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 368 356 369 357 val init_data_rect_Type3 : 370 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Floats.float > 'a1) 371 > (Floats.float > 'a1) > (Nat.nat > 'a1) > 'a1 > (ident > Nat.nat > 372 'a1) > init_data > 'a1 358 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Nat.nat > 'a1) > 359 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 373 360 374 361 val init_data_rect_Type2 : 375 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Floats.float > 'a1) 376 > (Floats.float > 'a1) > (Nat.nat > 'a1) > 'a1 > (ident > Nat.nat > 377 'a1) > init_data > 'a1 362 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Nat.nat > 'a1) > 363 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 378 364 379 365 val init_data_rect_Type1 : 380 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Floats.float > 'a1) 381 > (Floats.float > 'a1) > (Nat.nat > 'a1) > 'a1 > (ident > Nat.nat > 382 'a1) > init_data > 'a1 366 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Nat.nat > 'a1) > 367 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 383 368 384 369 val init_data_rect_Type0 : 385 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Floats.float > 'a1) 386 > (Floats.float > 'a1) > (Nat.nat > 'a1) > 'a1 > (ident > Nat.nat > 387 'a1) > init_data > 'a1 370 (bvint > 'a1) > (bvint > 'a1) > (bvint > 'a1) > (Nat.nat > 'a1) > 371 'a1 > (ident > Nat.nat > 'a1) > init_data > 'a1 388 372 389 373 val init_data_inv_rect_Type4 : 390 374 init_data > (bvint > __ > 'a1) > (bvint > __ > 'a1) > (bvint > __ 391 > 'a1) > (Floats.float > __ > 'a1) > (Floats.float > __ > 'a1) > 392 (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ > 'a1) > 393 'a1 375 > 'a1) > (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ 376 > 'a1) > 'a1 394 377 395 378 val init_data_inv_rect_Type3 : 396 379 init_data > (bvint > __ > 'a1) > (bvint > __ > 'a1) > (bvint > __ 397 > 'a1) > (Floats.float > __ > 'a1) > (Floats.float > __ > 'a1) > 398 (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ > 'a1) > 399 'a1 380 > 'a1) > (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ 381 > 'a1) > 'a1 400 382 401 383 val init_data_inv_rect_Type2 : 402 384 init_data > (bvint > __ > 'a1) > (bvint > __ > 'a1) > (bvint > __ 403 > 'a1) > (Floats.float > __ > 'a1) > (Floats.float > __ > 'a1) > 404 (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ > 'a1) > 405 'a1 385 > 'a1) > (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ 386 > 'a1) > 'a1 406 387 407 388 val init_data_inv_rect_Type1 : 408 389 init_data > (bvint > __ > 'a1) > (bvint > __ > 'a1) > (bvint > __ 409 > 'a1) > (Floats.float > __ > 'a1) > (Floats.float > __ > 'a1) > 410 (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ > 'a1) > 411 'a1 390 > 'a1) > (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ 391 > 'a1) > 'a1 412 392 413 393 val init_data_inv_rect_Type0 : 414 394 init_data > (bvint > __ > 'a1) > (bvint > __ > 'a1) > (bvint > __ 415 > 'a1) > (Floats.float > __ > 'a1) > (Floats.float > __ > 'a1) > 416 (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ > 'a1) > 417 'a1 395 > 'a1) > (Nat.nat > __ > 'a1) > (__ > 'a1) > (ident > Nat.nat > __ 396 > 'a1) > 'a1 418 397 419 398 val init_data_discr : init_data > init_data > __ … … 499 478 500 479 val transf_program_gen : 501 String.string > Identifiers.universe > (Identifiers.universe > 'a1>502 ( 'a2, Identifiers.universe) Types.prod) > (ident, 'a1) Types.prod503 List.list > ((ident, 'a2) Types.prod List.list, Identifiers.universe)504 Types.prod480 PreIdentifiers.identifierTag > Identifiers.universe > 481 (Identifiers.universe > 'a1 > ('a2, Identifiers.universe) Types.prod) > 482 (ident, 'a1) Types.prod List.list > ((ident, 'a2) Types.prod List.list, 483 Identifiers.universe) Types.prod 505 484 506 485 val transform_program_gen : 507 String.string > Identifiers.universe > ('a1, 'a3) program > (ident 508 List.list > Identifiers.universe > 'a1 > ('a2, Identifiers.universe) 509 Types.prod) > (('a2, 'a3) program, Identifiers.universe) Types.prod 486 PreIdentifiers.identifierTag > Identifiers.universe > ('a1, 'a3) program 487 > (ident List.list > Identifiers.universe > 'a1 > ('a2, 488 Identifiers.universe) Types.prod) > (('a2, 'a3) program, 489 Identifiers.universe) Types.prod 510 490 511 491 val map_partial :
Note: See TracChangeset
for help on using the changeset viewer.