Ignore:
Timestamp:
Jul 8, 2011, 5:49:22 PM (9 years ago)
Author:
mulligan
Message:

more work, bug found, ridiculous map3 function with dep. types added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1060 r1061  
    9494  λA: Type[0].
    9595  λleft, right: list A.
    96   match left with
    97   [ nil ⇒
    98     match right with
    99     [ nil ⇒ None ?
    100     | _ ⇒ Some ? right
    101     ]
    102   | _ ⇒ Some ? left
    103   ].
     96  λprfl: 0 < |left|.
     97  λprfr: 0 < |right|.
     98  match left return λx. 0 < |x| → list A with
     99  [ nil ⇒ λnil_prf.
     100    match right return λx. 0 < |x| → list A with
     101    [ nil ⇒ λnil_nil_absrd. ?
     102    | _ ⇒ λnil_cons_prf. right
     103    ] prfr
     104  | _ ⇒ λcons_prf. right
     105  ] prfl.
     106  normalize in nil_prf;
     107  cases(not_le_Sn_O 0)
     108  #HYP
     109  cases(HYP nil_prf)
     110qed.
    104111
    105112definition complete_regs ≝
     
    475482      translate_move destrs srcrs start_lbl dest_lbl def
    476483  ].
     484 
     485definition translate_op ≝
     486  λop.
     487  λdestrs.
     488  λsrcrs1.
     489  λsrcrs2.
     490  λstart_lbl.
     491  λdest_lbl.
     492  λdef.
     493  λprf: |srcrs1| = |srcrs2|.
     494  match reduce_strong ? srcrs1 srcrs2 with
     495  [ dp reduced first_reduced_proof ⇒
     496    let srcrsl_common ≝ \fst (\fst reduced) in
     497    let srcrsr_common ≝ \fst (\snd reduced) in
     498    let srcrsl_rest ≝ \snd (\fst reduced) in
     499    let srcrsr_rest ≝ \snd (\snd reduced) in
     500    let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
     501    match reduce_strong ? destrs srcrsl_common with
     502    [ dp reduced second_reduced_proof ⇒
     503      let destrs_common ≝ \fst (\fst reduced) in
     504      let destrs_rest ≝ \snd (\fst reduced) in
     505      match reduce_strong ? destrs_rest srcrs_rest with
     506      [ dp reduced third_reduced_proof ⇒
     507        let destrs_cted ≝ \fst (\fst reduced) in
     508        let destrs_rest ≝ \snd (\fst reduced) in
     509        let srcrs_cted ≝ \fst (\snd reduced) in
     510        let 〈def, tmpr〉 ≝ fresh_reg def in
     511        let insts_init ≝ [
     512          rtl_st_clear_carry start_lbl;
     513          rtl_st_int tmpr (zero ?) start_lbl
     514        ] in
     515        let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in
     516        let insts_add ≝ map3 … f_add destrs_common srcrsl_common srcrsr_common ? ? in
     517        let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in
     518        let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in
     519        let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in
     520        let insts_rest ≝ map … f_rest destrs_rest in
     521          adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
     522      ]
     523    ]
     524  ].
     525  [ 1: @third_reduced_proof
     526  | 3: @first_reduced_proof
     527 
     528let translate_op op destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     529  let ((srcrs1_common, srcrs1_rest), (srcrs2_common, srcrs2_rest)) =
     530    MiscPottier.reduce srcrs1 srcrs2 in
     531  let srcrs_rest = choose_rest srcrs1_rest srcrs2_rest in
     532  let ((destrs_common, destrs_rest), _) =
     533    MiscPottier.reduce destrs srcrs1_common in
     534  let ((destrs_cted, destrs_rest), (srcrs_cted, _)) =
     535    MiscPottier.reduce destrs_rest srcrs_rest in
     536  let (def, tmpr) = fresh_reg def in
     537  let insts_init =
     538    [RTL.St_clear_carry start_lbl ;
     539     RTL.St_int (tmpr, 0, start_lbl)] in
     540  let f_add destr srcr1 srcr2 =
     541    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
     542  let insts_add =
     543    MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
     544  let f_add_cted destr srcr =
     545    RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
     546  let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
     547  let f_rest destr =
     548    RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
     549  let insts_rest = List.map f_rest destrs_rest in
     550  adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest)
     551    start_lbl dest_lbl def
    477552
    478553definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.