Ignore:
Timestamp:
Nov 22, 2011, 12:28:04 PM (8 years ago)
Author:
campbell
Message:

Update RTLabs to RTL with unary operation types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1521 r1529  
    431431definition translate_op1 ≝
    432432  λglobals: list ident.
    433   λop1: unary_operation.
     433  λty, ty'.
     434  λop1: unary_operation ty ty'.
    434435  λdestrs: list register.
    435436  λsrcrs: list register.
     
    439440  λdef: rtl_internal_function globals.
    440441  match op1 with
    441   [ Ocastint src_sign src_size _ _ ⇒
     442  [ Ocastint src_size src_sign _ _ ⇒
    442443    let dest_size ≝ |destrs| * 8 in
    443444    let src_size ≝ bitsize_of_intsize src_size in
    444445      translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
    445   | Onegint
     446  | Onegint _ _
    446447      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
    447   | Onotbool
     448  | Onotbool _ _ _ _
    448449      translate_notbool globals destrs srcrs start_lbl dest_lbl def
    449   | Onotint
     450  | Onotint _ _
    450451    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
    451452    let l ≝ map2 … f destrs srcrs prf in
    452453      adds_graph rtl_params1 globals l start_lbl dest_lbl def
    453   | Optrofint r ⇒
     454  | Optrofint _ _ r ⇒
    454455      translate_move globals destrs srcrs start_lbl dest_lbl def
    455   | Ointofptr r ⇒
     456  | Ointofptr _ _ r ⇒
    456457      translate_move globals destrs srcrs start_lbl dest_lbl def
    457   | Oid
     458  | Oid _
    458459      translate_move globals destrs srcrs start_lbl dest_lbl def
    459460  | _ ⇒ ? (* float operations implemented in runtime *)
     
    860861  [2: >tmp_destrs_proof @prf_destrs
    861862  |1: normalize nodelta
    862       generalize in match srcrs12_proof
     863      generalize in match srcrs12_proof;
    863864      #HYP >rev_length >rev_length @HYP
    864865  ]
     
    971972      add_translates rtl_params1 globals [
    972973        translate_ne globals destrs srcrs1 srcrs2;
    973         translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
     974        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    974975      ] start_lbl dest_lbl def
    975976    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     
    979980      add_translates rtl_params1 globals [
    980981        translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?;
    981         translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
     982        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    982983      ] start_lbl dest_lbl def
    983984    | Cge ⇒
    984985      add_translates rtl_params1 globals [
    985986        translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?;
    986         translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
     987        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    987988      ] start_lbl dest_lbl def
    988989    ]
     
    992993      add_translates rtl_params1 globals [
    993994        translate_ne globals destrs srcrs1 srcrs2;
    994         translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
     995        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    995996      ] start_lbl dest_lbl def
    996997    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     
    10001001      add_translates rtl_params1 globals [
    10011002        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
    1002         translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
     1003        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    10031004      ] start_lbl dest_lbl def
    10041005    | Cge ⇒
    10051006      add_translates rtl_params1 globals [
    10061007        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
    1007         translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
     1008        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    10081009      ] start_lbl dest_lbl def
    10091010    ]
     
    10131014      add_translates rtl_params1 globals [
    10141015        translate_ne globals destrs srcrs1 srcrs2;
    1015         translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
     1016        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    10161017      ] start_lbl dest_lbl def
    10171018    | Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     
    10211022      add_translates rtl_params1 globals [
    10221023        translate_lt globals destrs destrs_prf srcrs2 srcrs1;
    1023         translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
     1024        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    10241025      ] start_lbl dest_lbl def
    10251026    | Cge ⇒
    10261027      add_translates rtl_params1 globals [
    10271028        translate_lt globals destrs destrs_prf srcrs1 srcrs2;
    1028         translate_op1 globals Onotbool destrs destrs (refl ? (|destrs|))
     1029        translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (|destrs|))
    10291030      ] start_lbl dest_lbl def
    10301031    ]
     
    11681169  | St_const destr cst lbl' ⇒
    11691170    translate_cst globals cst (find_local_env destr lenv) lbl lbl' def
    1170   | St_op1 op1 destr srcr lbl' ⇒
    1171     translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
     1171  | St_op1 ty ty' op1 destr srcr lbl' ⇒
     1172    translate_op1 globals ty ty' op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
    11721173  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
    11731174    translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
Note: See TracChangeset for help on using the changeset viewer.