Changeset 1635 for src/ASM


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
Location:
src/ASM
Files:
2 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.                                                       *)
  • src/ASM/I8051.ma

    r1600 r1635  
    2020inductive Op1: Type[0] ≝
    2121  Cmpl: Op1
    22 | Inc: Op1.
     22| Inc: Op1
     23| Rl: Op1. (* TODO: implement left rotation *)
    2324
    2425inductive Op2: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.