Ignore:
Timestamp:
Oct 7, 2011, 3:45:13 PM (8 years ago)
Author:
mulligan
Message:

finished implementing the translate constant function

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1315 r1325  
    153153qed.
    154154
    155 let rec translate_cst
    156   (globals: list ident) (cst: constant) (destrs: list register)
    157     (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
    158       on cst: rtl_internal_function globals ≝
    159   match cst with
    160   [ Ointconst size const ⇒
    161     match destrs with
    162     [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
    163     | _   ⇒
    164       let size' ≝ size_intsize size in
    165         match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
    166         [ true  ⇒ λgood_case.
    167           match split_into_bytes size const with
    168           [ dp bytes bytes_length_proof ⇒
    169             let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
    170               adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
    171           ]
    172         | false ⇒ λbad_case. ?
    173         ] (refl … (eqb size' (|destrs|)))
    174     ]
    175   | Ofloatconst float ⇒ ⊥
    176   | Oaddrsymbol id offset ⇒
    177     let 〈r1, r2〉 ≝ make_addr … destrs ? in
    178       add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def
    179   | Oaddrstack offset ⇒
    180     let 〈r1, r2〉 ≝ make_addr … destrs ? in
    181       ?
    182       (* add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def *)
    183   ].
    184   [1: >bytes_length_proof
    185       cut(size' = |destrs|)
    186       [1: @eqb_implies_eq
    187           assumption
    188       |2: #EQ_HYP
    189           <EQ_HYP %
    190       ]
    191   |5: cases not_implemented (* XXX: float, error_float in o'caml *)
    192   |*: cases daemon
    193   ].
    194 qed.
    195  
    196 definition translate_move_internal ≝
    197   λglobals.
    198   λdestr: register.
    199   λsrcr: register.
    200     sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
    201 
    202 definition translate_move ≝
    203   λglobals.
    204   λdestrs: list register.
    205   λsrcrs: list register.
    206   λstart_lbl: label.
    207     match reduce_strong register register destrs srcrs with
    208     [ dp crl_crr len_proof ⇒
    209       let commonl ≝ \fst (\fst crl_crr) in
    210       let commonr ≝ \fst (\snd crl_crr) in
    211       let restl ≝ \snd (\fst crl_crr) in
    212       let restr ≝ \snd (\snd crl_crr) in
    213       let f_common ≝ translate_move_internal globals in
    214       let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
    215       let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
    216         add_translates … [ translate1 ; translate2 ] start_lbl
    217     ].
    218     @len_proof
    219 qed.
    220 
    221 let rec make
    222   (A: Type[0]) (elt: A) (n: nat) on n ≝
    223   match n with
    224   [ O ⇒ [ ]
    225   | S n' ⇒ elt :: make A elt n'
    226   ].
    227  
    228 lemma make_length:
    229   ∀A: Type[0].
    230   ∀elt: A.
    231   ∀n: nat.
    232     n = length ? (make A elt n).
    233   #A #ELT #N
    234   elim N
    235   [ normalize %
    236   | #N #IH
    237     normalize <IH %
    238   ]
    239 qed.
    240 
    241 definition translate_cast_unsigned ≝
    242   λglobals.
    243   λdestrs.
    244   λstart_lbl.
    245   λdest_lbl.
    246   λdef: joint_internal_function … (rtl_params globals).
    247   let 〈def, tmp_zero〉 ≝ fresh_reg … def in
    248   let zeros ≝ make … tmp_zero (length … destrs) in
    249     add_translates … [
    250       adds_graph rtl_params1 … [
    251         sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
    252         ];
    253       translate_move globals destrs zeros
    254     ] start_lbl dest_lbl def.
    255 
    256 definition translate_cast_signed:
    257     ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
    258   λglobals: list ident.
    259   λdestrs.
    260   λsrcr.
    261   λstart_lbl.
    262   λdest_lbl.
    263   λdef.
    264   let 〈def, tmp_128〉 ≝ fresh_reg … def in
    265   let 〈def, tmp_255〉 ≝ fresh_reg … def in
    266   let 〈def, tmpr〉 ≝ fresh_reg … def in
    267   let 〈def, dummy〉 ≝ fresh_reg … def in
    268   let insts ≝ [
    269     sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
    270     sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
    271     sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
    272     sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
    273     sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
    274   ]
    275   in
    276   let srcrs ≝ make … tmpr (length … destrs) in
    277     add_translates rtl_params1 globals [
    278       adds_graph rtl_params1 globals insts;
    279       translate_move globals destrs srcrs
    280     ] start_lbl dest_lbl def.
    281 
    282 definition translate_cast ≝
    283   λglobals: list ident.
    284   λsrc_size: nat.
    285   λsrc_sign: signedness.
    286   λdest_size: nat.
    287   λdestrs: list register.
    288   λsrcrs: list register.
    289   match |srcrs| return λx. |srcrs| = x → ? with
    290   [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
    291   | S n' ⇒ λsucc_prf.
    292     if ltb dest_size src_size then
    293       translate_move globals destrs srcrs
    294     else
    295       match reduce_strong register register destrs srcrs with
    296       [ dp crl len_proof ⇒
    297         let commonl ≝ \fst (\fst crl) in
    298         let commonr ≝ \fst (\snd crl) in
    299         let restl ≝ \snd (\fst crl) in
    300         let restr ≝ \snd (\snd crl) in
    301         let insts_common ≝ translate_move globals commonl commonr in
    302         let sign_reg ≝ last_safe ? srcrs ? in
    303         let insts_sign ≝
    304           match src_sign with
    305           [ Unsigned ⇒ translate_cast_unsigned globals restl
    306           | Signed ⇒ translate_cast_signed globals restl sign_reg
    307           ]
    308         in
    309           add_translates rtl_params1 globals [ insts_common; insts_sign ]
    310       ]
    311   ] (refl ? (|srcrs|)).
    312   >succ_prf //
    313 qed.
    314 
    315 definition translate_negint ≝
    316   λglobals: list ident.
    317   λdestrs: list register.
    318   λsrcrs: list register.
    319   λstart_lbl: label.
    320   λdest_lbl: label.
    321   λdef: rtl_internal_function globals.
    322   λprf: |destrs| = |srcrs|. (* assert in caml code *)
    323   let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    324   let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
    325   let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
    326   let insts_init ≝ [
    327     sequential … (SET_CARRY …);
    328     sequential … (INT rtl_params_ globals tmpr (zero ?))
    329   ] in
    330   let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
    331   let insts_add ≝ map … f_add destrs in
    332     adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
    333 
    334 definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
    335   λglobals: list ident.
    336   λdestrs: list register.
    337   λsrcrs: list register.
    338   λstart_lbl: label.
    339   λdest_lbl: label.
    340   λdef: rtl_internal_function globals.
    341   match destrs with
    342   [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
    343   | cons destr destrs ⇒
    344     let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    345     let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
    346     let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
    347     let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
    348     let f ≝ λtmp_srcr. [
    349       sequential … (CLEAR_CARRY rtl_params_ globals);
    350       sequential … (INT rtl_params_ globals tmpr (zero ?));
    351       sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
    352       sequential … (INT rtl_params_ globals tmpr (zero ?));
    353       sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
    354       sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
    355     ] in
    356     let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in
    357     let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
    358       add_translates rtl_params1 globals [
    359         save_srcrs; adds_graph rtl_params1 globals insts; epilogue
    360       ] start_lbl dest_lbl def
    361   ].
    362 
    363 (* TODO: examine this properly.  This is a change from the O'caml code due
    364    to us dropping the explicit use of a cast destination size field.  We
    365    instead infer the size of the cast's destination from the context.  Is
    366    this correct?
    367 *)
    368 definition translate_op1 ≝
    369   λglobals: list ident.
    370   λop1: unary_operation.
    371   λdestrs: list register.
    372   λsrcrs: list register.
    373   λprf: |destrs| = |srcrs|.
    374   λstart_lbl: label.
    375   λdest_lbl: label.
    376   λdef: rtl_internal_function globals.
    377   match op1 with
    378   [ Ocastint src_sign src_size ⇒
    379     let dest_size ≝ |destrs| * 8 in
    380     let src_size ≝ bitsize_of_intsize src_size in
    381       translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
    382   | Onegint ⇒
    383       translate_negint globals destrs srcrs start_lbl dest_lbl def prf
    384   | Onotbool ⇒
    385       translate_notbool globals destrs srcrs start_lbl dest_lbl def
    386   | Onotint ⇒
    387     let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
    388     let l ≝ map2 … f destrs srcrs prf in
    389       adds_graph rtl_params1 globals l start_lbl dest_lbl def
    390   | Optrofint r ⇒
    391       translate_move globals destrs srcrs start_lbl dest_lbl def
    392   | Ointofptr r ⇒
    393       translate_move globals destrs srcrs start_lbl dest_lbl def
    394   | Oid ⇒
    395       translate_move globals destrs srcrs start_lbl dest_lbl def
    396   | _ ⇒ ? (* float operations implemented in runtime *)
    397   ].
    398   cases not_implemented
    399 qed.
    400  
    401155definition translate_op: ∀globals. ? → list register → list register → list register →
    402156  label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     
    444198  |*: cases daemon (* XXX: some of these look like they may be false *)
    445199  ]
     200qed.
     201
     202let rec translate_cst
     203  (globals: list ident) (cst: constant) (destrs: list register)
     204    (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
     205      on cst: rtl_internal_function globals ≝
     206  match cst with
     207  [ Ointconst size const ⇒
     208    match destrs with
     209    [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
     210    | _   ⇒
     211      let size' ≝ size_intsize size in
     212        match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
     213        [ true  ⇒ λgood_case.
     214          match split_into_bytes size const with
     215          [ dp bytes bytes_length_proof ⇒
     216            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
     217              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
     218          ]
     219        | false ⇒ λbad_case. ?
     220        ] (refl … (eqb size' (|destrs|)))
     221    ]
     222  | Ofloatconst float ⇒ ⊥
     223  | Oaddrsymbol id offset ⇒
     224    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     225    let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def in
     226    let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
     227      def
     228  | Oaddrstack offset ⇒
     229    let 〈r1, r2〉 ≝ make_addr … destrs ? in
     230    let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_address r1 r2)) dest_lbl) def in
     231    let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
     232      def
     233  ].
     234  [1: >bytes_length_proof
     235      cut(size' = |destrs|)
     236      [1: @eqb_implies_eq
     237          assumption
     238      |2: #EQ_HYP
     239          <EQ_HYP %
     240      ]
     241  |2: cases daemon (* XXX: bad case where destrs is of the wrong length *)
     242  |3: cases not_implemented (* XXX: float, error_float in o'caml *)
     243  |*: cases daemon (* XXX: various proofs to be filled in *)
     244  ].
     245qed.
     246 
     247definition translate_move_internal ≝
     248  λglobals.
     249  λdestr: register.
     250  λsrcr: register.
     251    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
     252
     253definition translate_move ≝
     254  λglobals.
     255  λdestrs: list register.
     256  λsrcrs: list register.
     257  λstart_lbl: label.
     258    match reduce_strong register register destrs srcrs with
     259    [ dp crl_crr len_proof ⇒
     260      let commonl ≝ \fst (\fst crl_crr) in
     261      let commonr ≝ \fst (\snd crl_crr) in
     262      let restl ≝ \snd (\fst crl_crr) in
     263      let restr ≝ \snd (\snd crl_crr) in
     264      let f_common ≝ translate_move_internal globals in
     265      let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
     266      let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
     267        add_translates … [ translate1 ; translate2 ] start_lbl
     268    ].
     269    @len_proof
     270qed.
     271
     272let rec make
     273  (A: Type[0]) (elt: A) (n: nat) on n ≝
     274  match n with
     275  [ O ⇒ [ ]
     276  | S n' ⇒ elt :: make A elt n'
     277  ].
     278 
     279lemma make_length:
     280  ∀A: Type[0].
     281  ∀elt: A.
     282  ∀n: nat.
     283    n = length ? (make A elt n).
     284  #A #ELT #N
     285  elim N
     286  [ normalize %
     287  | #N #IH
     288    normalize <IH %
     289  ]
     290qed.
     291
     292definition translate_cast_unsigned ≝
     293  λglobals.
     294  λdestrs.
     295  λstart_lbl.
     296  λdest_lbl.
     297  λdef: joint_internal_function … (rtl_params globals).
     298  let 〈def, tmp_zero〉 ≝ fresh_reg … def in
     299  let zeros ≝ make … tmp_zero (length … destrs) in
     300    add_translates … [
     301      adds_graph rtl_params1 … [
     302        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
     303        ];
     304      translate_move globals destrs zeros
     305    ] start_lbl dest_lbl def.
     306
     307definition translate_cast_signed:
     308    ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     309  λglobals: list ident.
     310  λdestrs.
     311  λsrcr.
     312  λstart_lbl.
     313  λdest_lbl.
     314  λdef.
     315  let 〈def, tmp_128〉 ≝ fresh_reg … def in
     316  let 〈def, tmp_255〉 ≝ fresh_reg … def in
     317  let 〈def, tmpr〉 ≝ fresh_reg … def in
     318  let 〈def, dummy〉 ≝ fresh_reg … def in
     319  let insts ≝ [
     320    sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
     321    sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
     322    sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
     323    sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
     324    sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
     325  ]
     326  in
     327  let srcrs ≝ make … tmpr (length … destrs) in
     328    add_translates rtl_params1 globals [
     329      adds_graph rtl_params1 globals insts;
     330      translate_move globals destrs srcrs
     331    ] start_lbl dest_lbl def.
     332
     333definition translate_cast ≝
     334  λglobals: list ident.
     335  λsrc_size: nat.
     336  λsrc_sign: signedness.
     337  λdest_size: nat.
     338  λdestrs: list register.
     339  λsrcrs: list register.
     340  match |srcrs| return λx. |srcrs| = x → ? with
     341  [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
     342  | S n' ⇒ λsucc_prf.
     343    if ltb dest_size src_size then
     344      translate_move globals destrs srcrs
     345    else
     346      match reduce_strong register register destrs srcrs with
     347      [ dp crl len_proof ⇒
     348        let commonl ≝ \fst (\fst crl) in
     349        let commonr ≝ \fst (\snd crl) in
     350        let restl ≝ \snd (\fst crl) in
     351        let restr ≝ \snd (\snd crl) in
     352        let insts_common ≝ translate_move globals commonl commonr in
     353        let sign_reg ≝ last_safe ? srcrs ? in
     354        let insts_sign ≝
     355          match src_sign with
     356          [ Unsigned ⇒ translate_cast_unsigned globals restl
     357          | Signed ⇒ translate_cast_signed globals restl sign_reg
     358          ]
     359        in
     360          add_translates rtl_params1 globals [ insts_common; insts_sign ]
     361      ]
     362  ] (refl ? (|srcrs|)).
     363  >succ_prf //
     364qed.
     365
     366definition translate_negint ≝
     367  λglobals: list ident.
     368  λdestrs: list register.
     369  λsrcrs: list register.
     370  λstart_lbl: label.
     371  λdest_lbl: label.
     372  λdef: rtl_internal_function globals.
     373  λprf: |destrs| = |srcrs|. (* assert in caml code *)
     374  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     375  let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
     376  let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
     377  let insts_init ≝ [
     378    sequential … (SET_CARRY …);
     379    sequential … (INT rtl_params_ globals tmpr (zero ?))
     380  ] in
     381  let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
     382  let insts_add ≝ map … f_add destrs in
     383    adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
     384
     385definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     386  λglobals: list ident.
     387  λdestrs: list register.
     388  λsrcrs: list register.
     389  λstart_lbl: label.
     390  λdest_lbl: label.
     391  λdef: rtl_internal_function globals.
     392  match destrs with
     393  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
     394  | cons destr destrs ⇒
     395    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     396    let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
     397    let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
     398    let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
     399    let f ≝ λtmp_srcr. [
     400      sequential … (CLEAR_CARRY rtl_params_ globals);
     401      sequential … (INT rtl_params_ globals tmpr (zero ?));
     402      sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
     403      sequential … (INT rtl_params_ globals tmpr (zero ?));
     404      sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
     405      sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
     406    ] in
     407    let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in
     408    let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
     409      add_translates rtl_params1 globals [
     410        save_srcrs; adds_graph rtl_params1 globals insts; epilogue
     411      ] start_lbl dest_lbl def
     412  ].
     413
     414(* TODO: examine this properly.  This is a change from the O'caml code due
     415   to us dropping the explicit use of a cast destination size field.  We
     416   instead infer the size of the cast's destination from the context.  Is
     417   this correct?
     418*)
     419definition translate_op1 ≝
     420  λglobals: list ident.
     421  λop1: unary_operation.
     422  λdestrs: list register.
     423  λsrcrs: list register.
     424  λprf: |destrs| = |srcrs|.
     425  λstart_lbl: label.
     426  λdest_lbl: label.
     427  λdef: rtl_internal_function globals.
     428  match op1 with
     429  [ Ocastint src_sign src_size ⇒
     430    let dest_size ≝ |destrs| * 8 in
     431    let src_size ≝ bitsize_of_intsize src_size in
     432      translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
     433  | Onegint ⇒
     434      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
     435  | Onotbool ⇒
     436      translate_notbool globals destrs srcrs start_lbl dest_lbl def
     437  | Onotint ⇒
     438    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
     439    let l ≝ map2 … f destrs srcrs prf in
     440      adds_graph rtl_params1 globals l start_lbl dest_lbl def
     441  | Optrofint r ⇒
     442      translate_move globals destrs srcrs start_lbl dest_lbl def
     443  | Ointofptr r ⇒
     444      translate_move globals destrs srcrs start_lbl dest_lbl def
     445  | Oid ⇒
     446      translate_move globals destrs srcrs start_lbl dest_lbl def
     447  | _ ⇒ ? (* float operations implemented in runtime *)
     448  ].
     449  cases not_implemented
    446450qed.
    447451
     
    512516  λdummy_lbl: label.
    513517  λi: nat.
    514   λi_prf.
     518  λi_prf: i ≤ |tmp_destrs|.
    515519  λtranslates: list ?.
    516520  λsrcr2i: register.
     
    535539    translates @ tmp_destrs2'.
    536540
    537 axiom translate_mul:
    538   ∀globals: list ident.
    539   ∀destrs: list register.
    540   ∀srcrs1: list register.
    541   ∀srcrs2: list register.
    542   ∀start_lbl: label.
    543   ∀dest_lbl: label.
    544   ∀def: rtl_internal_function globals.
    545     rtl_internal_function globals.
    546 
    547541(*
    548542definition translate_mul ≝
     
    569563    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
    570564*)
     565
     566axiom translate_mul:
     567  ∀globals: list ident.
     568  ∀destrs: list register.
     569  ∀srcrs1: list register.
     570  ∀srcrs2: list register.
     571  ∀start_lbl: label.
     572  ∀dest_lbl: label.
     573  ∀def: rtl_internal_function globals.
     574    rtl_internal_function globals.
    571575
    572576definition translate_divumodu8 ≝
Note: See TracChangeset for help on using the changeset viewer.