Changeset 2999 for src/ASM/Interpret2.ma

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:

• src/ASM/Interpret2.ma (modified) (1 diff)

src/ASM/Interpret2.ma

@@ -39 +39 @@
 definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
  λc:labelled_object_code.
-  let lcm ≝ load_code_memory … (oc c) in
   mk_preclassified_system_of_abstract_status
    labelled_object_code
    (OC_abstract_status c)
-   (λst. return (execute_1 lcm … st))
-   (initialise_status … (load_code_memory (oc c))).
+   (λst. return (execute_1 (cm c) … st))
+   (initialise_status … (cm c)).
 
 (* Pre-classified system for ASM *)