| 1 | include "joint/SemanticUtils.ma". |
|---|
| 2 | include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *) |
|---|
| 3 | |
|---|
| 4 | (*CSC: XXXX*) |
|---|
| 5 | axiom lin_succ_pc: unit → address → address. |
|---|
| 6 | |
|---|
| 7 | (*CSC: re-organize to take succ_pc out of lin_more_sem_params to share the |
|---|
| 8 | following definition between LTL and LIN *) |
|---|
| 9 | definition lin_more_sem_params: more_sem_params lin_params_ := |
|---|
| 10 | mk_more_sem_params lin_params_ |
|---|
| 11 | unit hw_register_env lin_succ_pc |
|---|
| 12 | hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA) |
|---|
| 13 | (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB) |
|---|
| 14 | (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL) |
|---|
| 15 | (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH) |
|---|
| 16 | (λlocals,dest_src. |
|---|
| 17 | match dest_src with |
|---|
| 18 | [ from_acc reg ⇒ |
|---|
| 19 | do v ← hwreg_retrieve locals RegisterA ; |
|---|
| 20 | hwreg_store reg v locals |
|---|
| 21 | | to_acc reg ⇒ |
|---|
| 22 | do v ← hwreg_retrieve locals reg ; |
|---|
| 23 | hwreg_store RegisterA v locals ]) |
|---|
| 24 | pointer_of_label. |
|---|
| 25 | definition lin_sem_params: sem_params ≝ mk_sem_params … lin_more_sem_params. |
|---|
| 26 | |
|---|
| 27 | definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e. |
|---|
| 28 | definition lin_pop_frame: list beval → state … lin_sem_params → res (state … lin_sem_params) ≝ λ_.λst. OK … st. |
|---|
| 29 | definition lin_save_frame: unit → state … lin_sem_params → state … lin_sem_params ≝ λ_.λst.st. |
|---|
| 30 | |
|---|
| 31 | definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝ |
|---|
| 32 | mk_more_sem_params1 ? lin_params1 lin_more_sem_params |
|---|
| 33 | lin_init_locals lin_pop_frame lin_save_frame. |
|---|
| 34 | |
|---|
| 35 | (*CSC: XXXXXXXXXX *) |
|---|
| 36 | axiom lin_fetch_statement: ∀globals. genv … (lin_params globals) → state lin_sem_params → res (pre_lin_statement globals). |
|---|
| 37 | |
|---|
| 38 | (*CSC: XXXXX, for is_final only *) |
|---|
| 39 | axiom lin_fetch_result: state lin_sem_params → res (list beval). |
|---|
| 40 | |
|---|
| 41 | (*CSC: XXXX, for external functions only*) |
|---|
| 42 | axiom lin_fetch_external_args: external_function → state lin_sem_params → res (list val). |
|---|
| 43 | axiom lin_set_result: list val → state lin_sem_params → res (state lin_sem_params). |
|---|
| 44 | |
|---|
| 45 | definition lin_exec_extended: ∀globals. genv globals (lin_params globals) → False → unit → state lin_sem_params → IO io_out io_in (trace × (state lin_sem_params)) |
|---|
| 46 | ≝ λglobals,ge,abs. ⊥. |
|---|
| 47 | @abs qed. |
|---|
| 48 | |
|---|
| 49 | definition lin_more_sem_params2: ∀globals. more_sem_params2 … (lin_params globals) ≝ |
|---|
| 50 | λglobals. |
|---|
| 51 | mk_more_sem_params2 … lin_more_sem_params1 |
|---|
| 52 | (lin_fetch_statement …) lin_fetch_result lin_fetch_external_args lin_set_result |
|---|
| 53 | (lin_exec_extended …). |
|---|
| 54 | |
|---|
| 55 | definition lin_fullexec ≝ |
|---|
| 56 | joint_fullexec … (λp. lin_more_sem_params2 (prog_var_names … p)). |
|---|
