source: LTS/variable_stack_pass.ma @ 3562

Last change on this file since 3562 was 3562, checked in by piccolo, 4 years ago
File size: 4.0 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "stack.ma".
16
17let rec trans_expr (e : expr) on e : list guard_combinators ≝
18match e with
19[ Var v ⇒ [push_var v]
20| Const n ⇒ [push_const n]
21| Plus e1 e2 ⇒ trans_expr e1 @ trans_expr e2 @ [push_plus]
22| Minus e1 e2 ⇒ trans_expr e1 @ trans_expr e2 @ [push_minus]
23].
24
25let rec trans_cond  (c : condition) on c : list guard_combinators ≝
26match c with
27[ Eq e1 e2 ⇒ trans_expr e1 @ trans_expr e2 @ [push_eq]
28| Not c ⇒ trans_cond c @ [push_not]
29].
30
31definition list_combinators_to_instructions : list guard_combinators → stack_Instructions → stack_Instructions ≝
32λl,i.foldr … (λc,instr.SEQ stack_state_params flat_labels (push c) (None ?) instr) i l.
33
34let rec trans_var_instr (i : frame_Instructions) on i : stack_Instructions ≝
35match i with
36[ EMPTY ⇒ EMPTY …
37| RETURN exp ⇒ list_combinators_to_instructions (trans_expr exp) (RETURN … it)
38| SEQ seq opt_l instr ⇒
39  match seq with
40  [ sNop ⇒ trans_var_instr … instr
41  | sAss v e ⇒ list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l (trans_var_instr … instr))
42  ]
43| COND cond ltrue i_true lfalse i_false instr ⇒
44     list_combinators_to_instructions (trans_cond cond)
45      (COND … it ltrue (trans_var_instr … i_true) lfalse (trans_var_instr … i_false) (trans_var_instr … instr))
46| LOOP cond ltrue i_true lfalse instr ⇒
47     LOOP stack_state_params flat_labels (trans_cond … cond) ltrue (trans_var_instr … i_true) lfalse (trans_var_instr … instr)
48| CALL f act_p opt_l instr ⇒
49     list_combinators_to_instructions (trans_expr (\snd act_p)) (CALL … f (\fst act_p) opt_l (trans_var_instr … instr))
50| IO lin io lout instr ⇒ ?
51].
52cases io
53qed.
54
55definition trans_var_prog : Program frame_env_params imp_instr_params flat_labels →
56Program frame_env_params stack_instr_params flat_labels ≝ λprog.
57mk_Program …
58(foldr … (λx,tail.(mk_env_item …
59   (mk_signature ? stack_instr_params (f_name … (f_sig … x)) (f_pars … (f_sig … x)) it) (f_lab … x)
60        (trans_var_instr … (f_body … x)) ) :: tail) (nil ?) (env … prog))
61(trans_var_instr … (main … prog)).
62
63include "Simulation.ma".
64
65definition frame_variable_pass_rel ≝ 
66λprog : Program frame_state_params frame_state_params frame_state_params.
67let t_prog ≝ trans_var_prog prog in
68mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
69 (operational_semantics stack_state_params stack_sem_state_params t_prog)
70 (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧
71         cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1))
72 (λ_.λ_.True).
73
74
75lemma eval_exp_ok : ∀env:activation_frame.∀e: expr.∀n.
76frame_sem_expr env e = return n →
77∃st'.
78m_fold Option … eval_combinators (trans_expr e)  = return st' ∧
79
80 
81definition simulation_imp_frame ≝
82λprog : Program frame_state_params frame_state_params frame_state_params.
83mk_simulation_conditions … (frame_variable_pass_rel prog) ???????????.
84cases daemon
85qed.
86 
Note: See TracBrowser for help on using the repository browser.