Changeset 2720
 Timestamp:
 Feb 23, 2013, 12:03:13 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/BackEndOps.ma
r2645 r2720 1 1 include "common/ByteValues.ma". 2 include "ASM/Arithmetic.ma". 3 4 (* just to avoid computing div and mod separately *) 5 definition divmodZ ≝ λx,y. 6 match x with 7 [ OZ ⇒ 〈OZ, OZ〉 8  pos n ⇒ 9 match y with 10 [ OZ ⇒ 〈OZ, OZ〉 11  pos m ⇒ let 〈q, r〉 ≝ divide n m in 12 〈natp_to_Z q, natp_to_Z r〉 13  neg m ⇒ let 〈q, r〉 ≝ divide n m in 14 match r with 15 [ pzero ⇒ 〈natp_to_negZ q, OZ〉 16  _ ⇒ 〈Zpred (natp_to_negZ q), y+ natp_to_Z r〉 17 ] 18 ] 19  neg n ⇒ 20 match y with 21 [ OZ ⇒ 〈OZ, OZ〉 22  pos m ⇒ let 〈q,r〉 ≝ divide n m in 23 match r with 24 [ pzero ⇒ 〈natp_to_negZ q, OZ〉 25  _ ⇒ 〈Zpred (natp_to_negZ q), y natp_to_Z r〉 26 ] 27  neg m ⇒ let 〈q, r〉 ≝ divide n m in 28 〈natp_to_Z q, natp_to_Z r〉 29 ] 30 ]. 2 31 3 32 (* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps … … 10 39 Cmpl: Op1 11 40  Inc: Op1 12  Rl: Op1. (* TODO: implement left rotation *)41  Rl: Op1. 13 42 14 43 inductive Op2: Type[0] ≝ … … 27 56 }. 28 57 29 axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte. 30 axiom op1_implementation: Op1 → Byte → Byte. 31 axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit). 58 definition opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte ≝ 59 λop,by1,by2. 60 (* Paolo: in ASM/Interpret.ma we use nats, but using Z is more efficient, isn't it? *) 61 let n1 ≝ Z_of_unsigned_bitvector … by1 in 62 let n2 ≝ Z_of_unsigned_bitvector … by2 in 63 match op with 64 [ Mul ⇒ 65 let prod ≝ vsplit … (bitvector_of_Z (8 + 8) (n1 * n2)) in 66 〈\snd prod, \fst prod〉 67  DivuModu ⇒ 68 if eqZb n2 OZ then 69 (* to mimic ASM/Interpret.ma, we return the arguments *) 70 〈by1, by2〉 71 else 72 let 〈q, r〉 ≝ divmodZ n1 n2 in 73 〈bitvector_of_Z … q, bitvector_of_Z … r〉 74 ]. 75 76 definition op1_implementation: Op1 → Byte → Byte ≝ 77 λop,by. 78 match op with 79 [ Cmpl ⇒ 80 negation_bv ? by 81  Inc ⇒ 82 add … by (bitvector_of_nat 8 1) 83  Rl ⇒ 84 rotate_left … 1 by 85 ]. 86 87 definition op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit) ≝ 88 λcarry,op,by1,by2. 89 match op with 90 [ Add ⇒ 91 let 〈res, flags〉 ≝ add_8_with_carry by1 by2 false in 92 〈res, get_index' ? O ? flags〉 93  Addc ⇒ 94 let 〈res, flags〉 ≝ add_8_with_carry by1 by2 carry in 95 〈res, get_index' ? O ? flags〉 96  Sub ⇒ 97 let 〈res, flags〉 ≝ sub_8_with_carry by1 by2 carry in 98 〈res, get_index' ? O ? flags〉 99  And ⇒ 100 〈conjunction_bv ? by1 by2, carry〉 101  Or ⇒ 102 〈inclusive_disjunction_bv ? by1 by2, carry〉 103  Xor ⇒ 104 〈exclusive_disjunction_bv ? by1 by2, carry〉 105 ]. 32 106 33 107 definition eval : Eval ≝
Note: See TracChangeset
for help on using the changeset viewer.