Changeset 2993 for src/ASM/Interpret2.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/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.