source: src/ASM/Interpret2.ma @ 2875

Last change on this file since 2875 was 2875, checked in by sacerdot, 7 years ago

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

File size: 1.6 KB
Line 
1include "ASM/ASMCosts.ma".
2include "common/Measurable.ma".
3
4(* Move where abstract_status is defined! *)
5definition mk_trans_system_of_abstract_status:
6 ∀S:abstract_status. (S → IOMonad io_out io_in S) → trans_system io_out io_in
7
8 λS,as_eval.
9  mk_trans_system ?? unit (λ_.as_status S) (λ_.as_result S)
10   (λ_.λstatus.
11     let tr ≝
12      match as_label … status with
13      [ Some cst ⇒ Echarge cst
14      | None ⇒ E0 ] in
15     ! status' ← as_eval … status ;
16     return 〈 tr, status' 〉).
17
18definition mk_fullexec_of_abstract_status:
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)
23    (λ_.return as_init).
24
25definition mk_preclassified_system_of_abstract_status:
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.
29   mk_preclassified_system
30    (mk_fullexec_of_abstract_status program S as_eval as_init)
31    (λ_.λst. ¬(is_none … (as_label … st)))
32    (λ_.as_classify S)
33    (λ_.λst,prf. as_call_ident S «st,?»).
34 @hide_prf cases (as_classify ??) in prf; normalize // *
35qed.
36
37(* End move *)
38
39definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
40 λc:labelled_object_code.
41  let cm ≝ load_code_memory (oc c) in
42  mk_preclassified_system_of_abstract_status
43   labelled_object_code
44   (ASM_abstract_status cm (costlabels c))
45   (λst. return (execute_1 … st))
46   (initialise_status … cm).
Note: See TracBrowser for help on using the repository browser.