Changeset 2993 for src/ASM


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
Location:
src/ASM
Files:
2 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
  • src/ASM/Interpret2.ma

    r2910 r2993  
    3939definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
    4040 λc:labelled_object_code.
     41  let lcm ≝ load_code_memory … (oc c) in
    4142  mk_preclassified_system_of_abstract_status
    4243   labelled_object_code
    4344   (OC_abstract_status c)
    44    (λst. return (execute_1 … st))
     45   (λst. return (execute_1 lcm … st))
    4546   (initialise_status … (load_code_memory (oc c))).
    4647
Note: See TracChangeset for help on using the changeset viewer.