Changeset 2993 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Mar 28, 2013, 9:56:26 AM (7 years ago)
Author:
sacerdot
Message:
  1. performance improved: the type inference was inferring load_code_memory ... in computational positions, duplicating the work at every step of execution of the assembly code. We now force the use of the let-in-ed variable
  2. new extraction after 1)
  3. driver/printer.ml repaired
  4. the output of the intermediate passes is now printed on file
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2910 r2993  
    4242      (λs1,s2. execute_1 … s1 = s2)
    4343      word_deqset
    44       (program_counter …)
    45       (OC_classify )
     44      (program_counter … code_memory)
     45      (OC_classify code_memory)
    4646      (λpc.lookup_opt … pc (costlabels prog))
    4747      (next_instruction_properly_relates_program_counters code_memory)
    48       (λst. as_result_of_finaladdr … st (final_pc prog))
    49       (OC_as_call_ident prog )
     48      (λst. as_result_of_finaladdr … code_memory … st (final_pc prog))
     49      (OC_as_call_ident prog code_memory)
    5050      ?.
    5151 * #st whd in ⊢ (??%? → ?); cases current_instruction [7: *] normalize
Note: See TracChangeset for help on using the changeset viewer.