source: LTS/stack_monostack_pass.ma @ 3572

Last change on this file since 3572 was 3572, checked in by piccolo, 4 years ago

pass stack to mono stack in place

File size: 2.2 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 "mono_stack.ma".
16include "Simulation.ma".
17
18let rec mono_env_store_rel (s1 : list (list ℕ)) (s2 : list ℕ) (fp : ℕ) on s1 : Prop ≝
19match s1 with
20[ nil ⇒ s2 = nil ?
21| cons x xs ⇒ ∃old_fp,s21,s22.s2 = s21 @ [old_fp] @ s22 ∧
22              match x with [ nil ⇒ False | cons y ys ⇒ ys = s21 ] ∧
23              mono_env_store_rel xs s22 old_fp ∧ |s22| = fp
24].
25
26definition mono_store_rel : frame_store_t → mono_stack_store_t → Prop ≝
27λst1,st2.mono_env_store_rel (\fst st1) (\fst st2) (\fst (\snd st2)) ∧ (\snd (\snd st1)) = (\snd (\snd st2)).
28
29definition mono_stack_relations :
30∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound.
31relations flat_labels
32(operational_semantics stack_state_params (stack_sem_state_params bound) prog)
33(operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog) ≝
34λprog.λbound.
35mk_relations … (λs1,s2.mono_store_rel … (store … s1) (store … s2) ∧ code … s1 = code … s2 ∧ cont … s1 = cont … s2)
36  (λ_.λ_.True).
37 
38definition stack_mono_stack_simulation : ∀prog : Program stack_env_params stack_instr_params flat_labels.∀bound.
39simulation_conditions … (mono_stack_relations prog bound) ≝λprog.λbound.mk_simulation_conditions ….
40cases daemon
41qed.
Note: See TracBrowser for help on using the repository browser.