Changeset 1288 for src/RTLabs


Ignore:
Timestamp:
Oct 3, 2011, 5:33:11 PM (9 years ago)
Author:
mulligan
Message:

more added to rtlabs to rtl pass

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/RTLAbstoRTL.ma

    r1287 r1288  
    806806
    807807definition translate_op2 ≝
     808  λglobals: list ident.
    808809  λop2.
    809810  λdestrs: list register.
    … …  
    817818  λstart_lbl: label.
    818819  λdest_lbl: label.
    819   λdef: rtl_internal_function.
     820  λdef: rtl_internal_function globals.
    820821  match op2 with
    821822  [ Oadd ⇒
    822     translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
     823    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
    823824  | Oaddp ⇒
    824     translate_op Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
     825    translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def
    825826  | Osub ⇒
    826     translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     827    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    827828  | Osubpi ⇒
    828     translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     829    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    829830  | Osubpp sz ⇒
    830     translate_op Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     831    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    831832  | Omul ⇒
    832     translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def
     833    translate_mul globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
    833834  | Odivu ⇒
    834     match srcrs1 return λx. 0 < |x| → rtl_internal_function with
     835    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
    835836    [ cons hd tl ⇒ λcons_prf.
    836837      match tl with
    837       [ nil ⇒ translate_divumodu8 true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
     838      [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
    838839      | _ ⇒ ? (* not implemented *)
    839840      ]
    … …  
    841842    ] srcrs1_prf
    842843  | Omodu ⇒
    843     match srcrs1 return λx. 0 < |x| → rtl_internal_function with
     844    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
    844845    [ cons hd tl ⇒ λcons_prf.
    845846      match tl with
    846       [ nil ⇒ translate_divumodu8 false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
     847      [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def
    847848      | _ ⇒ ? (* not implemented *)
    848849      ]
    … …  
    850851    ] srcrs1_prf
    851852  | Oand ⇒
    852     translate_op And destrs srcrs1 srcrs2 start_lbl dest_lbl def
     853    translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def
    853854  | Oor ⇒
    854     translate_op Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
     855    translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def
    855856  | Oxor ⇒
    856     translate_op Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
     857    translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def
    857858  | Ocmp c ⇒
    858859    match c with
    859860    [ Ceq ⇒
    860       add_translates [
    861         translate_ne destrs srcrs1 srcrs2;
    862         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     861      add_translates rtl_params1 globals [
     862        translate_ne globals destrs srcrs1 srcrs2;
     863        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    863864      ] start_lbl dest_lbl def
    864     | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
    865     | Clt ⇒ translate_lts destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
    866     | Cgt ⇒ translate_lts destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
     865    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     866    | Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def
     867    | Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def
    867868    | Cle ⇒
    868       add_translates [
    869         translate_lts destrs destrs_prf srcrs2 srcrs1 ? ?;
    870         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     869      add_translates rtl_params1 globals [
     870        translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?;
     871        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    871872      ] start_lbl dest_lbl def
    872873    | Cge ⇒
    873       add_translates [
    874         translate_lts destrs destrs_prf srcrs1 srcrs2 ? ?;
    875         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     874      add_translates rtl_params1 globals [
     875        translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?;
     876        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    876877      ] start_lbl dest_lbl def
    877878    ]
    … …  
    879880    match c with
    880881    [ Ceq ⇒
    881       add_translates [
    882         translate_ne destrs srcrs1 srcrs2;
    883         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     882      add_translates rtl_params1 globals [
     883        translate_ne globals destrs srcrs1 srcrs2;
     884        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    884885      ] start_lbl dest_lbl def
    885     | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
    886     | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
    887     | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
     886    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     887    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
     888    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
    888889    | Cle ⇒
    889       add_translates [
    890         translate_lt destrs destrs_prf srcrs2 srcrs1;
    891         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     890      add_translates rtl_params1 globals [
     891        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
     892        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    892893      ] start_lbl dest_lbl def
    893894    | Cge ⇒
    894       add_translates [
    895         translate_lt destrs destrs_prf srcrs1 srcrs2;
    896         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     895      add_translates rtl_params1 globals [
     896        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
     897        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    897898      ] start_lbl dest_lbl def
    898899    ]
    … …  
    900901    match c with
    901902    [ Ceq ⇒
    902       add_translates [
    903         translate_ne destrs srcrs1 srcrs2;
    904         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     903      add_translates rtl_params1 globals [
     904        translate_ne globals destrs srcrs1 srcrs2;
     905        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    905906      ] start_lbl dest_lbl def
    906     | Cne ⇒ translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def
    907     | Clt ⇒ translate_lt destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
    908     | Cgt ⇒ translate_lt destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
     907    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     908    | Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def
     909    | Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def
    909910    | Cle ⇒
    910       add_translates [
    911         translate_lt destrs destrs_prf srcrs2 srcrs1;
    912         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     911      add_translates rtl_params1 globals [
     912        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
     913        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    913914      ] start_lbl dest_lbl def
    914915    | Cge ⇒
    915       add_translates [
    916         translate_lt destrs destrs_prf srcrs1 srcrs2;
    917         translate_op1 Onotbool destrs destrs (refl ? (|destrs|))
     916      add_translates rtl_params1 globals [
     917        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
     918        translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
    918919      ] start_lbl dest_lbl def
    919920    ]
    … …  
    929930qed.
    930931
    931 definition translate_cond ≝
     932definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     933  λglobals: list ident.
    932934  λsrcrs: list register.
    933935  λstart_lbl: label.
    934936  λlbl_true: label.
    935937  λlbl_false: label.
    936   λdef: rtl_internal_function.
    937   let 〈def, tmpr〉 ≝ fresh_reg def in
    938   let 〈def, tmp_lbl〉 ≝ fresh_label def in
    939   let init ≝ rtl_st_int tmpr (zero ?) start_lbl in
    940   let f ≝ λsrcr. rtl_st_op2 Or tmpr tmpr srcr start_lbl in
    941   let def ≝ adds_graph (init :: (map … f srcrs)) start_lbl tmp_lbl def in
    942     add_graph tmp_lbl (rtl_st_cond tmpr lbl_true lbl_false) def. 
     938  λdef: rtl_internal_function globals.
     939  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     940  let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in
     941  let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in
     942  let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in
     943  let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in
     944    add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true lbl_false)) def.
    943945
    944946definition translate_load ≝
Note: See TracChangeset for help on using the changeset viewer.