Changeset 3561 for LTS


Ignore:
Timestamp:
Jun 16, 2015, 2:39:12 PM (4 years ago)
Author:
piccolo
Message:
 
Location:
LTS
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3549 r3561  
    8787].
    8888
    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
     89lemma 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
    9492[* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
    9593  lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
     
    105103  [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    106104        >(\b (refl …)) in ABS; #EQ destruct]
    107   #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2
    108   [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    109 *)
     105  #EQseq cases daemon
     106|*: cases daemon
     107qed.
    110108
    111109record env_params : Type[1] ≝
  • LTS/frame_variable_pass.ma

    r3560 r3561  
    1616include "variable.ma".
    1717
     18definition 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
     21let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝
     22match 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
     29let rec map_cond (c : condition) (map : variable → variable) on c : condition ≝
     30match 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
     35let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions  ≝
     36match 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].
     54cases io qed.
     55
     56
    1857let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝
    1958match l1 with
     
    2261].
    2362
    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)
     63definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝
     64λmap,st1,st2.
     65All2 … (λel1,el2.\snd el1 = \snd el2 ∧ All … (λx.let 〈v,val〉 ≝ x in read_frame … (\fst el2) (to_shift + (map v)) O = return val)
    2766       (\fst el1)) st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
    28        
     67
     68definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels →
     69Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog.
     70mk_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
    2977definition imp_variable_pass_rel ≝ 
     78λmap : variable → variable.
    3079λprog : Program imp_state_params imp_state_params imp_state_params.
     80let t_prog ≝ trans_imp_prog map prog in
    3181mk_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 ∧ 
     84cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1))
     85(λ_.λ_.True).
    3586
    36 definition simulation_imp_frame ≝ λprog.mk_simulation_conditions … (imp_variable_pass_rel prog) ???????????.
     87definition 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).
     91mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????.
     92cases daemon (*TODO*)
     93qed.
     94
     95(*
    3796[ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon
    3897| cases daemon
     
    52111|*: cases daemon
    53112]
    54 qed.
     113qed.*)
    55114   
    56115   
  • LTS/variable.ma

    r3560 r3561  
    1515include "imp.ma".
    1616
    17 definition to_shift : ℕ ≝ 3.
     17definition to_shift : ℕ ≝ 2.
    1818
    1919definition activation_frame ≝ DeqSet_List DeqNat.
     
    5454definition frame_store_t≝ DeqProd (DeqSet_List (DeqProd activation_frame variable)) (DeqProd DeqNat DeqNat). (*frame_pointer e stack_pointer*)
    5555
     56definition frame_env_params ≝ mk_env_params unit.
     57
    5658definition frame_state_params:state_params≝
    57 mk_state_params imp_instr_params imp_env_params flat_labels frame_store_t (*DeqEnv*).
     59mk_state_params imp_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
    5860
    5961definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return \fst hd.
     
    9193definition frame_eval_call:(signature frame_state_params imp_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
    9294λsgn,e,st.
    93   match sgn with
    94   [ mk_signature fun fpt rt ⇒
    9595    let 〈var,act_exp〉 ≝ e in
    9696    match (\fst st) with
     
    9898    |cons hd tl⇒ let 〈env,v〉≝ hd in
    9999                 !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
    102101  ].
    103102
     
    124123
    125124
    126 definition frame_envitem≝ (env_item imp_env_params imp_instr_params flat_labels).
     125definition frame_envitem≝ (env_item frame_env_params imp_instr_params flat_labels).
Note: See TracChangeset for help on using the changeset viewer.