Changeset 1635 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Jan 7, 2012, 12:33:17 AM (8 years ago)
Author:
tranquil
Message:
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r1599 r1635  
    5757  λm, n: nat.
    5858  λb: BitVector n. pad_vector ? false m n b.
    59      
     59 
     60let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
     61  match n with
     62  [ O ⇒ VEmpty ?
     63  | S n' ⇒
     64    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)
     65  ].
     66 
     67let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝
     68  match b with
     69  [ VEmpty ⇒ 0
     70  | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].
     71
    6072(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    6173(* Other manipulations.                                                       *)
Note: See TracChangeset for help on using the changeset viewer.