Changeset 793 for src/common
- Timestamp:
- May 12, 2011, 5:33:22 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/AST.ma
r764 r793 540 540 541 541 definition Trace ≝ list Identifier. 542 543 (* dpm: how are floats represented? *) 544 inductive cast: Type[0] ≝ 545 | cast_int: Byte → cast (* integer constant *) 546 | cast_float: Byte → cast (* float constant *) 547 | cast_addr_symbol: ident → cast (* address of a global symbol *) 548 | cast_stack_offset: Byte → cast. 549 550 inductive op1: Type[0] ≝ 551 | op_cast8_unsigned: op1 (**r 8-bit zero extension *) 552 | op_cast8_signed: op1 (**r 8-bit sign extension *) 553 | op_cast16_unsigned: op1 (**r 16-bit zero extension *) 554 | op_cast16_signed: op1 (**r 16-bit sign extension *) 555 | op_neg_int: op1 (**r integer opposite *) 556 | op_not_bool: op1 (**r boolean negation *) 557 | op_not_int: op1 (**r bitwise complement *) 558 | op_negf: op1 (**r float opposite *) 559 | op_absf: op1 (**r float absolute value *) 560 | op_single_of_float: op1 (**r float truncation *) 561 | op_int_of_float: op1 (**r signed integer to float *) 562 | op_intu_of_float: op1 (**r unsigned integer to float *) 563 | op_float_of_int: op1 (**r float to signed integer *) 564 | op_float_of_intu: op1 (**r float to unsigned integer *) 565 | op_id: op1 (**r identity *) 566 | op_ptr_of_int: op1 (**r int to pointer *) 567 | op_int_of_ptr: op1. (**r pointer to int *) 568 569 inductive op2: Type[0] ≝ 570 | op_add: op2 (**r integer addition *) 571 | op_sub: op2 (**r integer subtraction *) 572 | op_mul: op2 (**r integer multiplication *) 573 | op_div: op2 (**r integer signed division *) 574 | op_divu: op2 (**r integer unsigned division *) 575 | op_mod: op2 (**r integer signed modulus *) 576 | op_modu: op2 (**r integer unsigned modulus *) 577 | op_and: op2 (**r bitwise ``and'' *) 578 | op_or: op2 (**r bitwise ``or'' *) 579 | op_xor: op2 (**r bitwise ``xor'' *) 580 | op_shl: op2 (**r left shift *) 581 | op_shr: op2 (**r right signed shift *) 582 | op_shru: op2 (**r right unsigned shift *) 583 | op_addf: op2 (**r float addition *) 584 | op_subf: op2 (**r float subtraction *) 585 | op_mulf: op2 (**r float multiplication *) 586 | op_divf: op2 (**r float division *) 587 | op_cmp: Compare → op2 (**r integer signed comparison *) 588 | op_cmpu: Compare → op2 (**r integer unsigned comparison *) 589 | op_cmpf: Compare → op2 (**r float comparison *) 590 | op_addp: op2 (**r addition for a pointer and an integer *) 591 | op_subp: op2 (**r substraction for a pointer and a integer *) 592 | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracChangeset
for help on using the changeset viewer.