Ignore:
Timestamp:
Apr 7, 2011, 6:53:59 PM (9 years ago)
Author:
campbell
Message:

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r708 r744  
    66 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    77#v #ty #r
    8 cases v; [ | #i | #f | #r1 | #r #b #pc #of ]
     8cases v; [ | #i | #f | #r1 | #r' #b #pc #of ]
    99cases ty; [ 2,11,20,29,38: #sz #sg | 3,12,21,30,39: #sz | 4,13,22,31,40: #r #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
    1010#H whd in H:(??%?); destruct;
    1111[ lapply (eq_spec i zero); elim (eq i zero);
    1212  [ #e >e @bool_of_val_false //;
    13   | #ne @bool_of_val_true /2/;
     13  | #ne (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vint i) (Tint sz sg)) normalize #H @H /2/;
    1414  ]
    1515| elim (eq_dec f Fzero);
    1616  [ #e >e >(Feq_zero_true …) @bool_of_val_false //;
    17   | #ne >(Feq_zero_false …) //; @bool_of_val_true /2/;
     17  | #ne >(Feq_zero_false …) //; (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vfloat f) (Tfloat sz)) normalize #H @H /2/;
    1818  ]
    1919| @bool_of_val_false //
    20 | @bool_of_val_true //
     20| (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vptr r' b pc of) (Tpointer r ty)) normalize #H @H //
    2121] qed.
    2222
Note: See TracChangeset for help on using the changeset viewer.