Changeset 2875 for src/ASM/Interpret2.ma

Timestamp:

Mar 15, 2013, 1:32:50 AM (8 years ago)

Author:

sacerdot

Message:

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

File:

• src/ASM/Interpret2.ma (modified) (2 diffs)

src/ASM/Interpret2.ma

@@ -17 +17 @@
 
 definition mk_fullexec_of_abstract_status:
- ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
-≝ λS,as_eval,as_init.
-   mk_fullexec ?? unit (mk_trans_system_of_abstract_status S as_eval) (λ_.it) 
+ ∀program: Type[0].
+  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
+≝ λprogram,S,as_eval,as_init.
+   mk_fullexec ?? program (mk_trans_system_of_abstract_status S as_eval) (λ_.it) 
     (λ_.return as_init).
 
 definition mk_preclassified_system_of_abstract_status:
- ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
-≝ λS,as_eval,as_init.
+ ∀program: Type[0].
+  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
+≝ λprogram,S,as_eval,as_init.
    mk_preclassified_system
-    (mk_fullexec_of_abstract_status S as_eval as_init)
+    (mk_fullexec_of_abstract_status program S as_eval as_init)
     (λ_.λst. ¬(is_none … (as_label … st)))
     (λ_.as_classify S)
@@ -39 +41 @@
   let cm ≝ load_code_memory (oc c) in
   mk_preclassified_system_of_abstract_status
+   labelled_object_code
    (ASM_abstract_status cm (costlabels c))
    (λst. return (execute_1 … st))