Changeset 2700 for src/ASM


Ignore:
Timestamp:
Feb 22, 2013, 2:12:24 PM (7 years ago)
Author:
sacerdot
Message:
  1. exponential function dropped in favour of standard library
  2. fixpoint computation and graph colouring abstracted in the back-end, axiomatized in the compiler
  3. minor speedups in Policy.ma
Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2688 r2700  
    11include "ASM/BitVector.ma".
    22include "ASM/Util.ma".
    3 (* include "arithmetics/exp.ma". <-- this does not make it compile on latest matita + Cerco *)
     3include "arithmetics/exp.ma".
    44
    55definition addr16_of_addr11: Word → Word11 → Word ≝
     
    185185 [2,4: change with (?≤2^(S (n+l))) @le_exp /2 by le_n/
    186186 |1,3: @(transitive_le … (2 * (S m)))
    187   [2,4: /2 by le_times/
     187  [2,4: whd in ⊢ (??%); /2 by le_plus/
    188188  |3: // | 1: normalize <plus_n_O <plus_n_Sm // ]]
    189189qed. 
  • src/ASM/Policy.ma

    r2653 r2700  
    322322      cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
    323323      normalize nodelta
    324       [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     324      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le
     325        @monotonic_lt_times_r [/2/] %
    325326      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    326327        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
     
    333334    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
    334335    normalize nodelta
    335     [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/
     336    [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le
     337      @monotonic_lt_times_r try % /2/
    336338    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    337339      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
  • src/ASM/Util.ma

    r2673 r2700  
    784784    mk_Prod … (m ÷ n) (modulus m n).
    785785   
    786 let rec exponential (m: nat) (n: nat) on n ≝
    787   match n with
    788     [ O ⇒ S O
    789     | S o ⇒ m * exponential m o
    790     ].
    791 
    792 interpretation "Nat exponential" 'exp n m = (exponential n m).
    793    
    794786notation "hvbox(a break ⊎ b)"
    795787 left associative with precedence 55
Note: See TracChangeset for help on using the changeset viewer.