source: src/LIN/joint_LTL_LIN_semantics.ma @ 1380

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

LTL and LIN semantics factorized out in joint_LTL_LIN_semantics.ma.
Very cool.

File size: 3.4 KB
Line 
1include "LIN/joint_LTL_LIN.ma".
2include "joint/SemanticUtils.ma".
3
4(*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
5definition ltl_lin_more_sem_params: ∀succT:Type[0].∀succ:succT → address → address. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
6 λsuccT,succ.
7 mk_more_sem_params ?
8  unit hw_register_env succ
9   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
10    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
11    (λ_.hwreg_store RegisterDPL) (λe.λ_.hwreg_retrieve e RegisterDPL)
12    (λ_.hwreg_store RegisterDPH) (λe.λ_.hwreg_retrieve e RegisterDPH)
13     (λlocals,dest_src.
14       match dest_src with
15       [ from_acc reg ⇒
16          do v ← hwreg_retrieve locals RegisterA ;
17          hwreg_store reg v locals
18       | to_acc reg ⇒
19          do v ← hwreg_retrieve locals reg ;
20          hwreg_store RegisterA v locals ])
21     pointer_of_label.
22
23definition ltl_lin_sem_params:
24 ∀succT:Type[0].∀succ:succT → address → address. sem_params ≝
25 λsuccT,succ.mk_sem_params … (ltl_lin_more_sem_params … succ).
26
27definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
28definition ltl_lin_pop_frame:
29 ∀succT:Type[0].∀succ:succT → address → address. state … (ltl_lin_sem_params … succ) → res ((state … (ltl_lin_sem_params … succ)) × address) ≝
30 λ_.λ_.fetch_ra ….
31definition ltl_lin_save_frame:
32 ∀succT:Type[0].∀succ:succT → address → address. address → nat → unit → nat → unit → state … (ltl_lin_sem_params … succ) → res (state … (ltl_lin_sem_params … succ)) ≝
33 λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
34
35definition ltl_lin_more_sem_params1 : ∀succT:Type[0].∀succ:succT → address → address.more_sem_params1 … ltl_lin_params1 ≝
36 λsuccT,succ.
37 mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params ? succ)
38  ltl_lin_init_locals (ltl_lin_pop_frame … succ) (ltl_lin_save_frame … succ).
39
40(*CSC: XXXXX, for is_final only *)
41axiom ltl_lin_fetch_result: ∀succT:Type[0].∀succ:succT → address → address.state (ltl_lin_sem_params … succ) → res (list beval).
42
43(*CSC: XXXX, for external functions only*)
44axiom ltl_lin_fetch_external_args: ∀succT:Type[0].∀succ:succT → address → address.external_function → state (ltl_lin_sem_params … succ) → res (list val).
45axiom ltl_lin_set_result: ∀succT:Type[0].∀succ:succT → address → address.list val → state (ltl_lin_sem_params … succ) → res (state (ltl_lin_sem_params … succ)).
46
47definition ltl_lin_exec_extended: ∀succT:Type[0].∀succ:succT → address → address.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params … succ) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ)))
48 ≝ λsuccT,succ,p,globals,ge,abs. ⊥.
49@abs qed.
50
51definition ltl_lin_more_sem_params2:
52 ∀succT,succ,codeT,lookup,fetch.
53 ∀globals. more_sem_params2 … (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) ≝
54 λsuccT,succ,codeT,lookup,fetch,globals.
55  mk_more_sem_params2 … (ltl_lin_more_sem_params1 … succ)
56   (fetch globals) (ltl_lin_fetch_result …) (ltl_lin_fetch_external_args …)
57   (ltl_lin_set_result …) (ltl_lin_exec_extended …).
58
59definition ltl_lin_fullexec ≝
60 λsuccT,succ,codeT,lookup,fetch.
61  joint_fullexec … (λp. ltl_lin_more_sem_params2 succT succ codeT lookup fetch (prog_var_names … p)).
Note: See TracBrowser for help on using the repository browser.