Changeset 1343 for src/RTLabs


Ignore:
Timestamp:
Oct 10, 2011, 5:27:34 PM (8 years ago)
Author:
mulligan
Message:

fixed some bugs in the translation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1331 r1343  
    9898  λA.
    9999  λlst: list A.
    100   λprf: 2 length A lst.
    101   match lst return λx. 2 |x| → A × A with
     100  λprf: 2 = length A lst.
     101  match lst return λx. 2 = |x| → A × A with
    102102  [ nil ⇒ λlst_nil_prf. ?
    103103  | cons hd tl ⇒ λprf.
    104     match tl return λx. 1 |x| → A × A with
     104    match tl return λx. 1 = |x| → A × A with
    105105    [ nil ⇒ λtl_nil_prf. ?
    106106    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
     
    108108  ] prf.
    109109  [1: normalize in lst_nil_prf;
    110       cases(not_le_Sn_O 1);
    111       #HYP cases(HYP lst_nil_prf)
     110      destruct(lst_nil_prf)
    112111  |2: normalize in prf;
    113       @le_S_S_to_le
     112      @injective_S
    114113      assumption
    115114  |3: normalize in tl_nil_prf;
    116       cases(not_le_Sn_O 0)
    117       #HYP cases(HYP tl_nil_prf)]
     115      destruct(tl_nil_prf)
     116  ]
    118117qed.
    119118
     
    228227  | Oaddrstack offset ⇒
    229228    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
     229    let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_stack_address r1 r2)) dest_lbl) def in
    231230    let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
    232231      def
     
    538537  in
    539538    translates @ tmp_destrs2'.
    540 
     539 
    541540axiom foldi_strong:
    542541  ∀a: Type[0].
    543542  ∀b: Type[0].
    544543  ∀the_list: list b.
    545   ∀f: ∀n: nat. n ≤ |the_list| → a → b → a.
     544  ∀f: (∀i: nat. ∀proof: i ≤ |the_list|. a → b → a).
    546545  ∀seed: a.
    547546    a.
     
    552551  λsrcrs1: list register.
    553552  λsrcrs2: list register.
    554   λregs_proof: |srcrs2| = |destrs|.
     553  λregs_proof: |destrs| = |srcrs2|.
    555554  λstart_lbl: label.
    556555  λdest_lbl: label.
     
    571570      in
    572571        let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
    573         let f' ≝ λi. λproof: i ≤ |srcrs2|. f i ? in
    574         let insts_mul ≝ foldi_strong ? ? srcrs2 f' [ ] in
     572        let f' ≝ λi. λi_proof: i ≤ |srcrs2|. f i ? in
     573        let insts_mul ≝ foldi_strong srcrs2 f' [ ] in
    575574          add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def
    576575    ].
    577576  >tmp_destrs_prf
    578   <regs_proof
     577  >regs_proof
    579578  assumption
    580579qed.
     
    856855  λsrcrs1: list register.
    857856  λsrcrs2: list register.
    858   λsrcrs1_prf: 0 < |srcrs1|. (* XXX: can this be relaxed? i think it can
    859                                      but we need more dep. typ. in modu/divu
    860                                      cases *)
    861   λsrcrs2_prf: |srcrs2| = |destrs|.
     857  λsrcrs2_destrs_prf: |srcrs2| = |destrs|.
     858  λsrcrs1_destrs_prf: |srcrs1| = |destrs|.
    862859  λstart_lbl: label.
    863860  λdest_lbl: label.
     
    884881      ]
    885882    | nil ⇒ λnil_absrd. ?
    886     ] srcrs1_prf
     883    ] ?
    887884  | Omodu ⇒
    888885    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
     
    893890      ]
    894891    | nil ⇒ λnil_absrd. ?
    895     ] srcrs1_prf
     892    ] ?
    896893  | Oand ⇒
    897894    translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def
     
    965962  | _ ⇒ ? (* assert false, implemented in run time or float op *)
    966963  ].
    967   [ 3,7: normalize in nil_absrd;
    968          cases(not_le_Sn_O 0)
    969          #HYP cases(HYP nil_absrd)
    970   | 4,8,19,20,21,22,17,18,24:
    971          >srcrs2_prf
    972          assumption
    973   | 1,23:
    974          assumption
    975   | *:   cases not_implemented (* yes, really *)
     964  [1:
     965    @sym_eq
     966    assumption
     967  |3,8,19,22,24,25:
     968    >srcrs1_destrs_prf
     969    assumption
     970  |4,9:
     971    normalize in nil_absrd;
     972    cases(not_le_Sn_O 0)
     973    #HYP cases(HYP nil_absrd)
     974  |5,10,20,21,23,26:
     975    >srcrs2_destrs_prf
     976    assumption
     977  |*:
     978    cases not_implemented (* XXX: yes, really *)
    976979  ]
    977980qed.
     
    994997  λglobals: list ident.
    995998  λaddr.
    996   λaddr_prf: 2 |addr|.
     999  λaddr_prf: 2 = |addr|.
    9971000  λdestrs: list register.
    9981001  λstart_lbl: label.
     
    10091012      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
    10101013      let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     1014      let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    10111015      let insts_save_addr ≝ translate_move globals save_addr addr in
    10121016      let f ≝ λtranslates_off. λr.
     
    10161020            sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
    10171021          ];
    1018           translate_op2 globals Oaddp tmp_addr ? save_addr [tmpr] ? ?;
     1022          translate_op2 globals Oaddp tmp_addr ? save_addr [dummy; tmpr] ? ?;
    10191023          adds_graph rtl_params1 globals [
    10201024            sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2)
     
    10291033    ]
    10301034  ].
    1031   [1: normalize //
    1032   |2: >save_addr_prf normalize
    1033       @(transitive_le 1 2 (|addr|)) //
     1035  [1: >tmp_addr_prf >save_addr_prf %
     1036  |2: >save_addr_prf >tmp_addr_prf
     1037      @addr_prf
    10341038  |3: >tmp_addr_prf normalize
    1035       @(transitive_le 1 2 (|addr|)) //
    1036   |*: >tmp_addr_prf assumption
     1039      <addr_prf //
     1040  |4: >tmp_addr_prf assumption
    10371041  ]
    10381042qed.
     
    10411045  λglobals: list ident.
    10421046  λaddr.
    1043   λaddr_prf: 2 |addr|.
     1047  λaddr_prf: 2 = |addr|.
    10441048  λsrcrs: list register.
    10451049  λstart_lbl: label.
     
    10521056    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in
    10531057    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     1058    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    10541059    let f ≝ λtranslate_off. λsrcr.
    10551060      let 〈translates, off〉 ≝ translate_off in
     
    10581063          sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
    10591064        ];
    1060         translate_op2 globals Oaddp tmp_addr … addr [tmpr] ? ?;
     1065        translate_op2 globals Oaddp tmp_addr … addr [dummy; tmpr] ? ?;
    10611066        adds_graph rtl_params1 globals [
    10621067          sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
     
    10701075      add_translates rtl_params1 globals translates start_lbl dest_lbl def
    10711076  ].
    1072   [1: normalize //
     1077  [1: >tmp_addr_prf %
    10731078  |2: >tmp_addr_prf normalize
    1074       @(transitive_le 1 2 (|addr|)) //
    1075   |3: >tmp_addr_prf normalize
    1076       @(transitive_le 1 2 (|addr|)) //
    1077   |*: >tmp_addr_prf assumption
     1079      <addr_prf //
     1080  |3: >tmp_addr_prf <addr_prf //
     1081  |4: >tmp_addr_prf @addr_prf
    10781082  ]
    10791083qed.
Note: See TracChangeset for help on using the changeset viewer.