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

Code performance improved a bit by hand.

File:
1 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 :
Note: See TracChangeset for help on using the changeset viewer.