Changeset 2796 for src/ASM


Ignore:
Timestamp:
Mar 7, 2013, 12:10:42 PM (7 years ago)
Author:
tranquil
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

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

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