Changeset 2217 for src/RTLabs


Ignore:
Timestamp:
Jul 19, 2012, 6:13:54 PM (7 years ago)
Author:
tranquil
Message:
  • collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
  • completed update of RTL, LTL and LIN semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2214 r2217  
    88include alias "ASM/BitVector.ma".
    99include alias "arithmetics/nat.ma".
     10
     11definition rtl_fresh_reg:
     12 ∀globals.freshT RTL globals register ≝
     13  λglobals,def.
     14    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     15    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
     16
     17definition rtl_fresh_reg_no_local :
     18 ∀globals.freshT RTL globals register ≝
     19  λglobals,def.
     20    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     21    〈set_runiverse ?? def runiverse, r〉.
     22
    1023definition size_of_sig_type ≝
    1124  λsig.
     
    4861  λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf).
    4962
    50 definition m_fresh : ∀tag.state_monad (universe tag) (identifier tag) ≝
    51 λtag,univ.let pr ≝ fresh … univ in 〈\snd pr, \fst pr〉.
    52 
    53 let rec register_freshes (n: nat) on n :
    54   state_monad (universe RegisterTag) (Σl.|l| = n) ≝
    55   match n return λx.state_monad ? (Σl.|l| = x) with
    56   [ O ⇒ return «[ ],?»
    57   | S n' ⇒
    58     ! r ← m_fresh ?;
    59     ! res ← register_freshes n';
    60     return «r::res,?»
    61   ].[2: cases res -res #res #EQ <EQ] % qed.
    62 
    6363definition initialize_local_env_internal :
    64   (universe RegisterTag × local_env) → (register×typ) → (universe RegisterTag × local_env) ≝
    65   λlenv_runiverse,r_sig.
    66   let 〈runiverse,lenv〉 ≝ lenv_runiverse in
     64  ∀globals.
     65  ((joint_internal_function RTL globals) × local_env) → (register×typ) →
     66  ((joint_internal_function RTL globals) × local_env) ≝
     67  λglobals,def_env,r_sig.
     68  let 〈def,lenv〉 ≝ def_env in
    6769  let 〈r, sig〉 ≝ r_sig in
    6870  let size ≝ size_of_sig_type sig in
    69   let 〈runiverse,rs〉 ≝ register_freshes size runiverse in
    70     〈runiverse,add … lenv r rs〉.
    71 
    72 definition initialize_local_env :
    73   list (register×typ) →
    74   state_monad (universe RegisterTag) local_env ≝
    75   λregisters,runiverse.
    76   foldl … initialize_local_env_internal 〈runiverse,empty_map …〉 registers.
     71  let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in
     72    〈def,add … lenv r rs〉.
    7773
    7874include alias "common/Identifiers.ma".
     
    8480  | cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ?
    8581  ].cases prf #A #B assumption qed.
     82
     83definition initialize_local_env :
     84  ∀globals.
     85  list (register×typ) →
     86  freshT RTL globals local_env ≝
     87  λglobals,registers,def.
     88  foldl ?? (initialize_local_env_internal globals) 〈def,empty_map …〉 registers.
     89
     90lemma initialize_local_env_in : ∀globals,l,def,r.
     91  Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def).
     92#globals #l #U #r @(list_elim_left … l)
     93[ *
     94| * #tl #sig #hd #IH #G elim (Exists_append … G) -G
     95  whd in match initialize_local_env; normalize nodelta
     96  >foldl_step change with (initialize_local_env ???) in match (foldl ?????);
     97  [ #H lapply (IH H)
     98  | * [2: *] #EQ destruct(EQ)
     99  ] 
     100  cases (initialize_local_env ???)
     101  #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta
     102  elim (repeat_fresh ??????) #U'' #rs
     103  [ >mem_set_add @orb_Prop_r assumption
     104  | @mem_set_add_id
     105  ]
     106qed.
     107
     108example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.
     109// qed-.
     110example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.
     111// qed-.
     112
     113definition initialize_locals_params_ret :
     114  ∀globals.
     115  (* locals *) list (register×typ) →
     116  (* params *) list (register×typ) →
     117  (* return *) option (register×typ) →
     118  freshT RTL globals local_env ≝
     119  λglobals,locals,params,ret,def.
     120  let 〈def',lenv〉 as EQ ≝
     121    initialize_local_env globals
     122    ((match ret with
     123     [ Some r_sig ⇒ [r_sig]
     124     | None ⇒ [ ]
     125     ]) @ locals @ params) def in
     126  let locals' ≝ map_list_local_env lenv locals ? in
     127  let params' ≝ map_list_local_env lenv params ? in
     128  let ret' ≝ match ret return λx.ret = x → ? with
     129    [ Some r_sig ⇒ λprf.find_local_env (\fst r_sig) lenv ?
     130    | None ⇒ λ_.[ ]
     131    ] (refl …) in
     132  let def'' ≝
     133    mk_joint_internal_function RTL globals
     134      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
     135      params' locals' (joint_if_stacksize … def')
     136      (joint_if_code … def') (joint_if_entry … def') (joint_if_exit … def') in
     137   〈def'', lenv〉. @hide_prf
     138[ >(proj2_rewrite ????? EQ)
     139  @initialize_local_env_in >prf %1 %
     140|*: >(proj2_rewrite ????? EQ)
     141  @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr)))
     142  [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params))
     143    [ #a #H @Exists_append_r @Exists_append_r @H
     144    | generalize in match params;
     145    ]
     146  | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) locals))
     147    [ #a #H @Exists_append_r @Exists_append_l @H
     148    | generalize in match locals;
     149    ]
     150  ]
     151  #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}
     152]
     153qed.
    86154
    87155definition make_addr ≝
     
    834902qed.
    835903
    836 lemma initialize_local_env_in : ∀l,runiverse,r.
    837   Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env l runiverse).
    838 #l #U #r @(list_elim_left … l)
    839 [ *
    840 | * #tl #sig #hd #IH #G elim (Exists_append … G) -G
    841   whd in match initialize_local_env; normalize nodelta
    842   >foldl_step change with (initialize_local_env ??) in match (foldl ?????);
    843   [ #H lapply (IH H)
    844   | * [2: *] #EQ destruct(EQ)
    845   ] 
    846   cases (initialize_local_env ??)
    847   #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta
    848   elim (register_freshes ??) #U'' #rs
    849   [ >mem_set_add @orb_Prop_r assumption
    850   | @mem_set_add_id
    851   ]
    852 qed.
    853 
    854 definition proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.
    855 // qed.
    856 definition proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.
    857 // qed.
    858 
    859 
    860904(* XXX: we use a "hack" here to circumvent the proof obligations required to
    861905   create res, an empty internal_function record.  we insert into our graph
     
    865909  λglobals: list ident.
    866910  λdef.
    867   let runiverse ≝ f_reggen def in
    868   let 〈runiverse',lenv〉 as pr_eq ≝ initialize_local_env
    869     (match f_result def with [ None ⇒ [ ] | Some r_sig ⇒ [r_sig]] @
    870      f_params def @ f_locals def) runiverse in
    871   let params' ≝ map_list_local_env lenv (f_params def) ? in
    872   let locals' ≝ map_list_local_env lenv (f_locals def) ? in
    873   let result' ≝
    874     match (f_result def) return λx.f_result def = x → ? with
    875     [ None ⇒ λ_.[ ]
    876     | Some r_typ ⇒ λEQ.
    877        find_local_env (\fst r_typ) lenv ?
    878     ] (refl …)
    879   in
     911  let runiverse' ≝ f_reggen def in
    880912  let luniverse' ≝ f_labgen def in
    881913  let stack_size' ≝ f_stacksize def in
     
    887919  let graph' ≝ add LabelTag ? graph' exit'
    888920    (RETURN …) in
     921  let init ≝
     922    mk_joint_internal_function RTL globals luniverse' runiverse' [ ] [ ]
     923     [ ] stack_size' graph' (pi1 … entry') (pi1 … exit') in
     924  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
     925    (f_locals def) (f_params def) (f_result def) init in
    889926  let f_trans ≝ λlbl,stmt,def.
    890927    let pr ≝ translate_statement … lenv stmt in
    891     b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
    892   let res ≝
    893     mk_joint_internal_function RTL globals luniverse' runiverse' result' params'
    894      locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
    895     foldi … f_trans (f_graph def) res. 
    896    
    897 [1,2: >graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add
    898 | >(proj2_rewrite ????? pr_eq)
    899   @initialize_local_env_in >EQ normalize nodelta %1 %
    900 |*: >(proj2_rewrite ????? pr_eq)
    901   @(All_mp ??? (λpr.initialize_local_env_in ?? (\fst pr)))
    902   [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_locals def)))
    903     [ #a #H @Exists_append_r @Exists_append_r @H
    904     | generalize in match (f_locals def);
    905     ]
    906   | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_params def)))
    907     [ #a #H @Exists_append_r @Exists_append_l @H
    908     | generalize in match (f_params def);
    909     ]
    910   ]
    911   #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}
    912 ]
     928    b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
     929  foldi … f_trans (f_graph def) init'.
     930@hide_prf
     931>graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add
    913932qed.
    914933
Note: See TracChangeset for help on using the changeset viewer.