Changeset 2875 for src/ASM/Interpret2.ma
- Timestamp:
- Mar 15, 2013, 1:32:50 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret2.ma
r2764 r2875 17 17 18 18 definition mk_fullexec_of_abstract_status: 19 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in 20 ≝ λS,as_eval,as_init. 21 mk_fullexec ?? unit (mk_trans_system_of_abstract_status S as_eval) (λ_.it) 19 ∀program: Type[0]. 20 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in 21 ≝ λprogram,S,as_eval,as_init. 22 mk_fullexec ?? program (mk_trans_system_of_abstract_status S as_eval) (λ_.it) 22 23 (λ_.return as_init). 23 24 24 25 definition mk_preclassified_system_of_abstract_status: 25 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system 26 ≝ λS,as_eval,as_init. 26 ∀program: Type[0]. 27 ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system 28 ≝ λprogram,S,as_eval,as_init. 27 29 mk_preclassified_system 28 (mk_fullexec_of_abstract_status S as_eval as_init)30 (mk_fullexec_of_abstract_status program S as_eval as_init) 29 31 (λ_.λst. ¬(is_none … (as_label … st))) 30 32 (λ_.as_classify S) … … 39 41 let cm ≝ load_code_memory (oc c) in 40 42 mk_preclassified_system_of_abstract_status 43 labelled_object_code 41 44 (ASM_abstract_status cm (costlabels c)) 42 45 (λst. return (execute_1 … st))
Note: See TracChangeset
for help on using the changeset viewer.