# Changeset 2796 for src/ASM/Arithmetic.ma

Ignore:
Timestamp:
Mar 7, 2013, 12:10:42 PM (8 years ago)
Message:
• added global notation for existence in Type[1] (\exists[1] x.P)
• in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
• in joint_semantics, moved out and around some parameters in primitive semantics functions
• fixed all back end semantics
• added skeleton files for single passes correctness proofs
File:
1 edited

Unmodified
Removed
• ## src/ASM/Arithmetic.ma

 r2782 (* This one by Paolo is efficient, but it is for the opposite indianess. -(* jpb: we already have bitvector_of_nat and friends in the library, maybe - * we should unify this in some way *) -let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝ -  match n with -  [ O ⇒ VEmpty ? -  | S n' ⇒ -    eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2) -  ]. - - * we should unify this in some way *) (* Paolo: converted to good endianness *) let rec bitvector_of_nat_aux (n_acc : nat) (acc :BitVector n_acc) n (k : nat) on n : BitVector (plus n_acc n) ≝ match n return λn.BitVector (plus n_acc n) with [ O ⇒ acc⌈BitVector n_acc ↦ ?⌉ | S n' ⇒ bitvector_of_nat_aux (S n_acc) (eqb (k mod 2) 1 ::: acc) n' (k ÷ 2) ⌈BitVector (S n_acc + n') ↦ ?⌉ ]. [ cases (plus_n_O ?) | cases (plus_n_Sm ??) ] % qed. definition bitvector_of_nat : ∀n.ℕ → BitVector n ≝ bitvector_of_nat_aux' ? [[ ]]. -let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝ -  match b with
Note: See TracChangeset for help on using the changeset viewer.