Changeset 2993 for src/ASM/Interpret2.ma

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:

• 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 … st))
+   (λst. return (execute_1 lcm … st))
    (initialise_status … (load_code_memory (oc c))).