Changeset 1331


Ignore:
Timestamp:
Oct 10, 2011, 10:21:35 AM (8 years ago)
Author:
mulligan
Message:

some changes, but i now have two contradictory proof obligations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1325 r1331  
    539539    translates @ tmp_destrs2'.
    540540
    541 (*
     541axiom foldi_strong:
     542  ∀a: Type[0].
     543  ∀b: Type[0].
     544  ∀the_list: list b.
     545  ∀f: ∀n: nat. n ≤ |the_list| → a → b → a.
     546  ∀seed: a.
     547    a.
     548 
    542549definition translate_mul ≝
    543550  λglobals: list ident.
     
    545552  λsrcrs1: list register.
    546553  λsrcrs2: list register.
     554  λregs_proof: |srcrs2| = |destrs|.
    547555  λstart_lbl: label.
    548556  λdest_lbl: label.
     
    550558  let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    551559  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    552   let 〈def, tmp_destrs〉 ≝ fresh_regs rtl_params0 globals def (|destrs|) in
    553   let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
    554   let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
    555   let insts_init ≝ [
    556     translate_move globals fresh_srcrs1 srcrs1;
    557     translate_move globals fresh_srcrs2 srcrs2;
    558     translate_cst globals (Ointconst I8 (zero …)) destrs
    559   ]
    560   in
    561   let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
    562   let insts_mul ≝ foldi … f [ ] srcrs2 in ?.
    563     add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
    564 *)
    565 
    566 axiom 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.
     560    match fresh_regs_strong rtl_params0 globals def (|destrs|) with
     561    [ dp def_tmp_destrs tmp_destrs_prf ⇒
     562      let def ≝ \fst def_tmp_destrs in
     563      let tmp_destrs ≝ \snd def_tmp_destrs in
     564      let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
     565      let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
     566      let insts_init ≝ [
     567        translate_move globals fresh_srcrs1 srcrs1;
     568        translate_move globals fresh_srcrs2 srcrs2;
     569        translate_cst globals (Ointconst I8 (zero …)) destrs
     570      ]
     571      in
     572        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
     575          add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def
     576    ].
     577  >tmp_destrs_prf
     578  <regs_proof
     579  assumption
     580qed.
    575581
    576582definition translate_divumodu8 ≝
     
    853859                                     but we need more dep. typ. in modu/divu
    854860                                     cases *)
    855   λsrcrs2_prf: 0 < |srcrs2|.
     861  λsrcrs2_prf: |srcrs2| = |destrs|.
    856862  λstart_lbl: label.
    857863  λdest_lbl: label.
     
    869875    translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
    870876  | Omul ⇒
    871     translate_mul globals destrs srcrs1 srcrs2 start_lbl dest_lbl def
     877    translate_mul globals destrs srcrs1 srcrs2 ? start_lbl dest_lbl def
    872878  | Odivu ⇒
    873879    match srcrs1 return λx. 0 < |x| → rtl_internal_function globals with
     
    959965  | _ ⇒ ? (* assert false, implemented in run time or float op *)
    960966  ].
    961   [ 2,6: normalize in nil_absrd;
     967  [ 3,7: normalize in nil_absrd;
    962968         cases(not_le_Sn_O 0)
    963969         #HYP cases(HYP nil_absrd)
    964   | 3,7,12,17,13,15,18,19,20,21,14,16:
     970  | 4,8,19,20,21,22,17,18,24:
     971         >srcrs2_prf
     972         assumption
     973  | 1,23:
    965974         assumption
    966975  | *:   cases not_implemented (* yes, really *)
Note: See TracChangeset for help on using the changeset viewer.