Changeset 2965


Ignore:
Timestamp:
Mar 26, 2013, 6:35:16 PM (4 years ago)
Author:
sacerdot
Message:

Code performance improved a bit by hand.

Location:
extracted
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCostsSplit.ml

    r2909 r2965  
    124124let rec traverse_code_internal prog program_counter program_size =
    125125  (match program_size with
    126    | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag)
    127    | Nat.S program_size' ->
     126   | 0 -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag)
     127   | _ -> let program_size' = program_size - 1 in
    128128     (fun _ ->
    129129       let new_program_counter' =
     
    153153    ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0 **)
    154154let traverse_code prog =
     155prerr_endline "<TRAVERSE_CODE"; let res =
    155156  Types.pi1
    156157    (traverse_code_internal prog
     
    158159        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    159160        Nat.O)))))))))))))))))
    160       (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    161         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    162         (Nat.S Nat.O))))))))))))))))))
     161      (Glue.int_of_matitanat (List.length (ASM.oc prog))))
     162in prerr_endline "TRAVERSE_CODE>"; res
    163163
    164164(** val compute_costs :
  • extracted/aSMCostsSplit.mli

    r2909 r2965  
    119119open UtilBranch
    120120
    121 val traverse_code_internal :
    122   ASM.labelled_object_code -> BitVector.word -> Nat.nat -> Nat.nat
    123   Identifiers.identifier_map Types.sig0
    124 
    125121val traverse_code :
    126122  ASM.labelled_object_code -> Nat.nat Identifiers.identifier_map Types.sig0
Note: See TracChangeset for help on using the changeset viewer.