source: src/LIN/semantics.ma @ 1304

Last change on this file since 1304 was 1304, checked in by sacerdot, 8 years ago

Work in progress.

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