Ignore:
Timestamp:
Dec 13, 2011, 2:49:52 PM (8 years ago)
Author:
sacerdot
Message:

Files ported to new version of the standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/RTLabsToRTL.ma

    r1529 r1601  
    176176  λdef: rtl_internal_function globals.
    177177  match reduce_strong register register srcrs1 srcrs2 with
    178   [ dp reduced first_reduced_proof ⇒
     178  [ mk_Sig reduced first_reduced_proof ⇒
    179179    let srcrsl_common ≝ \fst (\fst reduced) in
    180180    let srcrsr_common ≝ \fst (\snd reduced) in
    … …  
    183183    let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in
    184184    match reduce_strong register register destrs srcrsl_common with
    185     [ dp reduced second_reduced_proof ⇒
     185    [ mk_Sig reduced second_reduced_proof ⇒
    186186      let destrs_common ≝ \fst (\fst reduced) in
    187187      let destrs_rest ≝ \snd (\fst reduced) in
    188188      match reduce_strong register register destrs_rest srcrs_rest with
    189       [ dp reduced third_reduced_proof ⇒
     189      [ mk_Sig reduced third_reduced_proof ⇒
    190190        let destrs_cted ≝ \fst (\fst reduced) in
    191191        let destrs_rest ≝ \snd (\fst reduced) in
    … …  
    225225        [ true  ⇒ λgood_case.
    226226          match split_into_bytes size const with
    227           [ dp bytes bytes_length_proof ⇒
     227          [ mk_Sig bytes bytes_length_proof ⇒
    228228            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
    229229              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
    … …  
    269269  λstart_lbl: label.
    270270    match reduce_strong register register destrs srcrs with
    271     [ dp crl_crr len_proof ⇒
     271    [ mk_Sig crl_crr len_proof ⇒
    272272      let commonl ≝ \fst (\fst crl_crr) in
    273273      let commonr ≝ \fst (\snd crl_crr) in
    … …  
    357357    else
    358358      match reduce_strong register register destrs srcrs with
    359       [ dp crl len_proof ⇒
     359      [ mk_Sig crl len_proof ⇒
    360360        let commonl ≝ \fst (\fst crl) in
    361361        let commonr ≝ \fst (\snd crl) in
    … …  
    628628  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    629629    match fresh_regs_strong rtl_params0 globals def (|destrs|) with
    630     [ dp def_tmp_destrs tmp_destrs_prf ⇒
     630    [ mk_Sig def_tmp_destrs tmp_destrs_prf ⇒
    631631      let def ≝ \fst def_tmp_destrs in
    632632      let tmp_destrs ≝ \snd def_tmp_destrs in
    … …  
    689689    let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in
    690690    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
    691     [ dp crl their_proof ⇒
     691    [ mk_Sig crl their_proof ⇒
    692692      let commonl ≝ \fst (\fst crl) in
    693693      let commonr ≝ \fst (\snd crl) in
    … …  
    826826  | _ ⇒
    827827    match fresh_regs_strong globals def (|destrs|) with
    828     [ dp def_tmp_destrs tmp_destrs_proof ⇒
     828    [ mk_Sig def_tmp_destrs tmp_destrs_proof ⇒
    829829      let def ≝ \fst def_tmp_destrs in
    830830      let tmp_destrs ≝ \snd def_tmp_destrs in
    … …  
    836836      let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in
    837837      match complete_regs_strong globals def srcrs1 srcrs2 with
    838       [ dp srcrs12_added srcrs12_proof ⇒
     838      [ mk_Sig srcrs12_added srcrs12_proof ⇒
    839839        let srcrs1 ≝ \fst (\fst srcrs12_added) in
    840840        let srcrs2 ≝ \snd (\fst srcrs12_added) in
    … …  
    893893  λdef: rtl_internal_function globals.
    894894  match fresh_regs_strong globals def (|srcrs1|) with
    895   [ dp def_tmp_srcrs1 srcrs1_prf ⇒
     895  [ mk_Sig def_tmp_srcrs1 srcrs1_prf ⇒
    896896    let def ≝ \fst def_tmp_srcrs1 in
    897897    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
    898898    match fresh_regs_strong globals def (|srcrs2|) with
    899     [ dp def_tmp_srcrs2 srcrs2_prf ⇒
     899    [ mk_Sig def_tmp_srcrs2 srcrs2_prf ⇒
    900900      let def ≝ \fst def_tmp_srcrs2 in
    901901      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
    … …  
    10731073  λdef: rtl_internal_function globals.
    10741074  match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1075   [ dp def_save_addr save_addr_prf ⇒
     1075  [ mk_Sig def_save_addr save_addr_prf ⇒
    10761076    let def ≝ \fst def_save_addr in
    10771077    let save_addr ≝ \snd def_save_addr in
    10781078    match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1079     [ dp def_tmp_addr tmp_addr_prf ⇒
     1079    [ mk_Sig def_tmp_addr tmp_addr_prf ⇒
    10801080      let def ≝ \fst def_tmp_addr in
    10811081      let tmp_addr ≝ \snd def_tmp_addr in
    … …  
    11211121  λdef: rtl_internal_function globals.
    11221122  match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1123   [ dp def_tmp_addr tmp_addr_prf ⇒
     1123  [ mk_Sig def_tmp_addr tmp_addr_prf ⇒
    11241124    let def ≝ \fst def_tmp_addr in
    11251125    let tmp_addr ≝ \snd def_tmp_addr in
Note: See TracChangeset for help on using the changeset viewer.