Changeset 2999 for src/ASM/Interpret2.ma


Ignore:
Timestamp:
Mar 28, 2013, 12:47:55 PM (8 years ago)
Author:
sacerdot
Message:

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r2993 r2999  
    3939definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
    4040 λc:labelled_object_code.
    41   let lcm ≝ load_code_memory … (oc c) in
    4241  mk_preclassified_system_of_abstract_status
    4342   labelled_object_code
    4443   (OC_abstract_status c)
    45    (λst. return (execute_1 lcm … st))
    46    (initialise_status … (load_code_memory (oc c))).
     44   (λst. return (execute_1 (cm c) … st))
     45   (initialise_status … (cm c)).
    4746
    4847(* Pre-classified system for ASM *)
Note: See TracChangeset for help on using the changeset viewer.