Changeset 3561
- Timestamp:
- Jun 16, 2015, 2:39:12 PM (6 years ago)
- Location:
- LTS
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Language.ma
r3549 r3561 87 87 ]. 88 88 89 90 (* 91 lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → 92 (i1 ≠ i2 → P false) → P (eq_instructions p i1 i2). 93 #P #p #i1 elim i1 89 lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,l_p,i1,i2.(i1 = i2 → P true) → 90 (i1 ≠ i2 → P false) → P (eq_instructions p l_p i1 i2). 91 #P #p #l_p #i1 elim i1 94 92 [* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ 95 93 lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') … … 105 103 [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 106 104 >(\b (refl …)) in ABS; #EQ destruct] 107 #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2108 [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 109 *) 105 #EQseq cases daemon 106 |*: cases daemon 107 qed. 110 108 111 109 record env_params : Type[1] ≝ -
LTS/frame_variable_pass.ma
r3560 r3561 16 16 include "variable.ma". 17 17 18 definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ 19 λA,B,f,a,b,x.if x == a then b else f x. 20 21 let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ 22 match e with 23 [ Var v ⇒ Var (map v) 24 | Const n ⇒ Const n 25 | Plus e1 e2 ⇒ Plus (map_exp e1 map) (map_exp e2 map) 26 | Minus e1 e2 ⇒ Minus (map_exp e1 map) (map_exp e2 map) 27 ]. 28 29 let rec map_cond (c : condition) (map : variable → variable) on c : condition ≝ 30 match c with 31 [Eq e1 e2 ⇒ Eq (map_exp e1 map) (map_exp e2 map) 32 | Not c1 ⇒ Not (map_cond c1 map) 33 ]. 34 35 let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions ≝ 36 match i with 37 [ EMPTY ⇒ EMPTY … 38 | RETURN rt ⇒ RETURN … rt 39 | SEQ seq opt_l i ⇒ 40 match seq with 41 [ sNop ⇒ SEQ … sNop opt_l (trans_imp_instr i map) 42 | sAss v e ⇒ SEQ frame_state_params flat_labels (sAss (map v) (map_exp e map)) opt_l (trans_imp_instr i map) 43 ] 44 | COND cond ltrue i_true lfalse i_false instr ⇒ 45 COND frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse (trans_imp_instr i_false map) 46 (trans_imp_instr instr map) 47 | LOOP cond ltrue i_true lfalse instr ⇒ 48 LOOP frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse 49 (trans_imp_instr instr map) 50 | CALL f act_p opt_l instr ⇒ 51 CALL frame_state_params flat_labels f 〈(\fst act_p),(map_exp (\snd act_p) map)〉 opt_l (trans_imp_instr instr map) 52 | IO lin io lout instr ⇒ ? 53 ]. 54 cases io qed. 55 56 18 57 let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝ 19 58 match l1 with … … 22 61 ]. 23 62 24 definition store_rel : store_t → frame_store_t → Prop ≝25 λ st1,st2.26 All2 … (λel1,el2.\snd el1 = \snd el2 ∧ All … (λx.let 〈v,val〉 ≝ x in read_frame … (\fst el2) (to_shift + val) O = return val)63 definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝ 64 λmap,st1,st2. 65 All2 … (λel1,el2.\snd el1 = \snd el2 ∧ All … (λx.let 〈v,val〉 ≝ x in read_frame … (\fst el2) (to_shift + (map v)) O = return val) 27 66 (\fst el1)) st1 (\fst st2) ∧ \snd st2 = 〈O,O〉. 28 67 68 definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels → 69 Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog. 70 mk_Program ??? 71 (foldr … 72 (λx,tail.(mk_env_item … 73 (mk_signature frame_env_params … (f_name … (f_sig … x)) it (f_ret …(f_sig … x))) 74 (f_lab … x) (trans_imp_instr (f_body … x) map)) :: tail) (nil ?) (env … prog)) 75 (trans_imp_instr (main … prog) map). 76 29 77 definition imp_variable_pass_rel ≝ 78 λmap : variable → variable. 30 79 λprog : Program imp_state_params imp_state_params imp_state_params. 80 let t_prog ≝ trans_imp_prog map prog in 31 81 mk_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). 82 (operational_semantics frame_state_params frame_sem_state_params t_prog) 83 (λs1,s2.store_rel map (store … s1) (store … s2) ∧ code … s2 = trans_imp_instr (code … s1) map ∧ 84 cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1)) 85 (λ_.λ_.True). 35 86 36 definition simulation_imp_frame ≝ λprog.mk_simulation_conditions … (imp_variable_pass_rel prog) ???????????. 87 definition simulation_imp_frame ≝ 88 λprog : Program imp_state_params imp_state_params imp_state_params. 89 λmap : variable → variable. 90 λprf : All … (λx.map (f_pars imp_state_params imp_state_params (f_sig … x)) = O) (env … prog). 91 mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????. 92 cases daemon (*TODO*) 93 qed. 94 95 (* 37 96 [ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon 38 97 | cases daemon … … 52 111 |*: cases daemon 53 112 ] 54 qed. 113 qed.*) 55 114 56 115 -
LTS/variable.ma
r3560 r3561 15 15 include "imp.ma". 16 16 17 definition to_shift : ℕ ≝ 3.17 definition to_shift : ℕ ≝ 2. 18 18 19 19 definition activation_frame ≝ DeqSet_List DeqNat. … … 54 54 definition frame_store_t≝ DeqProd (DeqSet_List (DeqProd activation_frame variable)) (DeqProd DeqNat DeqNat). (*frame_pointer e stack_pointer*) 55 55 56 definition frame_env_params ≝ mk_env_params unit. 57 56 58 definition frame_state_params:state_params≝ 57 mk_state_params imp_instr_params imp_env_params flat_labels frame_store_t (*DeqEnv*).59 mk_state_params imp_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*). 58 60 59 61 definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return \fst hd. … … 91 93 definition frame_eval_call:(signature frame_state_params imp_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝ 92 94 λsgn,e,st. 93 match sgn with94 [ mk_signature fun fpt rt ⇒95 95 let 〈var,act_exp〉 ≝ e in 96 96 match (\fst st) with … … 98 98 |cons hd tl⇒ let 〈env,v〉≝ hd in 99 99 !n ← frame_sem_expr env act_exp; 100 frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 fpt n 101 ] 100 frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n 102 101 ]. 103 102 … … 124 123 125 124 126 definition frame_envitem≝ (env_item imp_env_params imp_instr_params flat_labels).125 definition frame_envitem≝ (env_item frame_env_params imp_instr_params flat_labels).
Note: See TracChangeset
for help on using the changeset viewer.