source: LTS/frame_variable_pass.ma @ 3560

Last change on this file since 3560 was 3560, checked in by piccolo, 5 years ago

language example

File size: 2.8 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 "Simulation.ma".
16include "variable.ma".
17
18let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝
19match l1 with
20[ nil ⇒ match l2 with [nil ⇒ True | cons _ _ ⇒ False]
21| cons x xs ⇒ match l2 with [nil ⇒ False | cons y ys ⇒ f x y ∧ All2 … f xs ys]
22].
23
24definition store_rel : store_t → frame_store_t → Prop ≝
25λst1,st2.
26All2 … (λel1,el2.\snd el1 = \snd el2 ∧ All … (λx.let 〈v,val〉 ≝ x in read_frame … (\fst el2) (to_shift + val) O = return val)
27       (\fst el1)) st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
28       
29definition imp_variable_pass_rel ≝ 
30λprog : Program imp_state_params imp_state_params imp_state_params.
31mk_relations flat_labels (operational_semantics imp_state_params imp_sem_state_params prog)
32 (operational_semantics frame_state_params frame_sem_state_params prog)
33(λs1,s2.store_rel (store … s1) (store … s2) ∧ (code … s1) = (code … s2) ∧ (cont … s1) = (cont … s2))
34(λ_.λ_.False).
35
36definition simulation_imp_frame ≝ λprog.mk_simulation_conditions … (imp_variable_pass_rel prog) ???????????.
37[ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon
38| cases daemon
39| cases daemon
40| #s1 #s2 #s1' #H inversion H
41  [ #s11 #s22 * #act #instr #cont #EQcode_s11 #EQcont_s11 #EQ #EQ1 destruct #EQstore #Hio1 #Hio2
42    #act_no_ret #EQ1 #EQ2 #EQ3 destruct #_ ** #Hstore #EQcode #EQcont #_ #_
43    %{(mk_state … (code … s22) (cont … s22) (store … s2) (io_info … s22))}
44    %{(t_ind … (t_base …))}
45    [2: @(cost_act … (None ?))
46    | @hide_prf whd applyS(empty) [9: <EQcode assumption |2: normalize % * |3: % |4: cases daemon (*da mettere a posto io *)
47    |5: % |6: % |7: % |8: <EQcont assumption |*:]
48    | % [ % // % // ] %1 %2 [cases daemon] %1 cases daemon
49    ]
50  |*: cases daemon 
51  ]
52|*: cases daemon
53]
54qed.
55   
56   
Note: See TracBrowser for help on using the repository browser.