Changeset 2779


Ignore:
Timestamp:
Mar 5, 2013, 11:50:59 PM (7 years ago)
Author:
sacerdot
Message:
  1. bug fixed in the use of vsplit
  2. major speed up (avoid detour via base-1 natural numbers)

Now the IntelHex? file is output.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/IntelHex.ml

    r2778 r2779  
    77type word = Extracted.BitVector.word
    88
    9 let size_of_Size = function `Eight -> 8 | `Sixteen -> 16
     9let size_lookup = function `Eight -> 8 | `Sixteen -> 16
    1010
    1111let zero size =
    12  let size = size_of_Size size in
     12 let size = size_lookup size in
    1313 Extracted.BitVector.zero (Extracted.Glue.matitanat_of_int size)
    1414
     
    2222let complement v = Extracted.Arithmetic.two_complement_negation (Extracted.Glue.matitanat_of_int 8) v
    2323
     24let divide_with_remainder x y = (x / y, x mod y)
     25
     26let rec nat_to_bv n k =
     27  match n with
     28  | Extracted.Nat.O -> Extracted.Vector.VEmpty
     29  | Extracted.Nat.S n' ->
     30    let res,modu = divide_with_remainder k 2 in
     31    Extracted.Vector.VCons (n',
     32     (if modu = 1 then Extracted.Bool.True else Extracted.Bool.False),
     33     nat_to_bv n' res)
     34
    2435let vect_of_int k n =
    25  Extracted.BitVector.nat_to_bv (Extracted.Glue.matitanat_of_int (size_of_Size n)) (Extracted.Glue.matitanat_of_int k)
     36 nat_to_bv (Extracted.Glue.matitanat_of_int (size_lookup n)) k
    2637
    2738let from_word v =
    2839 let {Extracted.Types.fst = fst ; snd = snd} =
    29   Extracted.Vector.vsplit (Extracted.Glue.matitanat_of_int 16)
     40  Extracted.Vector.vsplit (Extracted.Glue.matitanat_of_int 8)
    3041   (Extracted.Glue.matitanat_of_int 8) v in
    3142 fst,snd
Note: See TracChangeset for help on using the changeset viewer.