Line | |
---|

1 | include "Vector.ma". |
---|

2 | include "List.ma". |
---|

3 | include "Nat.ma". |
---|

4 | include "Bool.ma". |
---|

5 | |
---|

6 | ndefinition BitVector ≝ λn: Nat. Vector Bool n. |
---|

7 | ndefinition Bit ≝ BitVector (S Z). |
---|

8 | ndefinition Nibble ≝ BitVector (S (S (S (S Z)))). |
---|

9 | ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))). |
---|

10 | ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))). |
---|

11 | ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). |
---|

12 | |
---|

13 | ndefinition zero ≝ |
---|

14 | λn: Nat. |
---|

15 | replicate Bool n False. |
---|

16 | |
---|

17 | ndefinition conjunction ≝ |
---|

18 | λn: Nat. |
---|

19 | λb: BitVector n. |
---|

20 | λc: BitVector n. |
---|

21 | zip Bool Bool Bool n conjunction b c. |
---|

22 | |
---|

23 | ndefinition inclusive_disjunction ≝ |
---|

24 | λn: Nat. |
---|

25 | λb: BitVector n. |
---|

26 | λc: BitVector n. |
---|

27 | zip Bool Bool Bool n inclusive_disjunction b c. |
---|

28 | |
---|

29 | ndefinition exclusive_disjunction ≝ |
---|

30 | λn: Nat. |
---|

31 | λb: BitVector n. |
---|

32 | λc: BitVector n. |
---|

33 | zip Bool Bool Bool n exclusive_disjunction b c. |
---|

34 | |
---|

35 | ndefinition complement ≝ |
---|

36 | λn: Nat. |
---|

37 | λb: BitVector n. |
---|

38 | map Bool Bool n (negation) b. |
---|

39 | |
---|

40 | ndefinition divide_with_remainder ≝ |
---|

41 | λm, n: Nat. |
---|

42 | mk_Cartesian Nat Nat (m ÷ n) (modulus m n). |
---|

43 | |
---|

44 | nlet rec bitvector_of_nat_aux (n: Nat) on n ≝ |
---|

45 | let div_rem ≝ divide_with_remainder n (S (S Z)) in |
---|

46 | let div ≝ first Nat Nat div_rem in |
---|

47 | let rem ≝ second Nat Nat div_rem in |
---|

48 | match div with |
---|

49 | [ Z ⇒ |
---|

50 | match rem with |
---|

51 | [ Z ⇒ Empty Bool |
---|

52 | | S r ⇒ True :: (bitvector_of_nat_aux Z) |
---|

53 | ] |
---|

54 | | S d ⇒ |
---|

55 | match rem with |
---|

56 | [ Z ⇒ False :: (bitvector_of_nat_aux (S d)) |
---|

57 | | S r ⇒ True :: (bitvector_of_nat_aux (S d)) |
---|

58 | ] |
---|

59 | ]. |
---|

**Note:** See

TracBrowser
for help on using the repository browser.