Changeset 1064 for src/common
 Timestamp:
 Jul 12, 2011, 5:52:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r1060 r1064 104 104  I32: intsize. 105 105 106 (* unary operations used in the backend intermediate languages, there's also a separate107 type for unary operations at the assembly level in ASM/I8051.ma *)108 inductive intermediate_op1: Type[0] ≝109  intermediate_op1_cast: nat → signedness → nat → intermediate_op1 (**r size in bytes, signedness, to size *)110  intermediate_op1_negint: intermediate_op1 (**r integer opposite *)111  intermediate_op1_notbool: intermediate_op1 (**r boolean negation *)112  intermediate_op1_notint: intermediate_op1 (**r bitwise complement *)113  intermediate_op1_id: intermediate_op1 (**r identity *)114  intermediate_op1_ptrofint: intermediate_op1 (**r int to pointer *)115  intermediate_op1_intofptr: intermediate_op1. (**r pointer to int *)116 117 106 (* * Float types come in two sizes: 32 bits (single precision) 118 107 and 64bit (double precision). *) … … 409 398 410 399 Remark map_partial_identity: 411 forall (A B: Type) (prefix: A > errmsg) (l: list (A * B)), 400 forall (A B: Type) (prefix: A > errmsg) (l: list (A * B)),cmp 412 401 map_partial prefix (fun b => OK b) l = OK l. 413 402 Proof. … … 665 654 666 655 inductive op1: Type[0] ≝ 667  op_cast8_unsigned: op1 (**r 8bit zero extension *) 668  op_cast8_signed: op1 (**r 8bit sign extension *) 669  op_cast16_unsigned: op1 (**r 16bit zero extension *) 670  op_cast16_signed: op1 (**r 16bit sign extension *) 656  op_cast: nat → signedness → nat → op1 671 657  op_neg_int: op1 (**r integer opposite *) 672 658  op_not_bool: op1 (**r boolean negation *) 673 659  op_not_int: op1 (**r bitwise complement *) 674  op_negf: op1 (**r float opposite *)675  op_absf: op1 (**r float absolute value *)676  op_single_of_float: op1 (**r float truncation *)677  op_int_of_float: op1 (**r signed integer to float *)678  op_intu_of_float: op1 (**r unsigned integer to float *)679  op_float_of_int: op1 (**r float to signed integer *)680  op_float_of_intu: op1 (**r float to unsigned integer *)681 660  op_id: op1 (**r identity *) 682 661  op_ptr_of_int: op1 (**r int to pointer *) … … 697 676  op_shr: op2 (**r right signed shift *) 698 677  op_shru: op2 (**r right unsigned shift *) 699  op_addf: op2 (**r float addition *)700  op_subf: op2 (**r float subtraction *)701  op_mulf: op2 (**r float multiplication *)702  op_divf: op2 (**r float division *)703 678  op_cmp: Compare → op2 (**r integer signed comparison *) 704 679  op_cmpu: Compare → op2 (**r integer unsigned comparison *) 705  op_cmpf: Compare → op2 (**r float comparison *)706 680  op_addp: op2 (**r addition for a pointer and an integer *) 707 681  op_subp: op2 (**r substraction for a pointer and a integer *) 682  op_subpp: op2 708 683  op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracChangeset
for help on using the changeset viewer.