Changeset 1061


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

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

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1060 r1061  
    148148      destruct(cons_prf)
    149149      assumption
     150  ]
     151qed.
     152
     153let rec map3
     154  (A: Type[0]) (B: Type[0]) (C: Type[0]) (D: Type[0]) (f: A → B → C → D)
     155  (left: list A) (centre: list B) (right: list C)
     156  (prflc: |left| = |centre|) (prfcr: |centre| = |right|) on left ≝
     157  match left return λx. |x| = |centre| → list D with
     158  [ nil ⇒ λnil_prf.
     159    match centre return λx. |x| = |right| → list D with
     160    [ nil ⇒ λnil_nil_prf.
     161      match right return λx. |nil ?| = |x| → list D with
     162      [ nil        ⇒ λnil_nil_nil_prf. nil D
     163      | cons hd tl ⇒ λcons_nil_nil_absrd. ?
     164      ] nil_nil_prf
     165    | cons hd tl ⇒ λnil_cons_absrd. ?
     166    ] prfcr
     167  | cons hd tl ⇒ λcons_prf.
     168    match centre return λx. |x| = |right| → list D with
     169    [ nil ⇒ λcons_nil_absrd. ?
     170    | cons hd' tl' ⇒ λcons_cons_prf.
     171      match right return λx. |right| = |x| → |cons ? hd' tl'| = |x| → list D with
     172      [ nil ⇒ λrefl_prf. λcons_cons_nil_absrd. ?
     173      | cons hd'' tl'' ⇒ λrefl_prf. λcons_cons_cons_prf.
     174        (f hd hd' hd'') :: (map3 A B C D f tl tl' tl'' ? ?)
     175      ] (refl ? (|right|)) cons_cons_prf
     176    ] prfcr
     177  ] prflc.
     178  [ 1: normalize in cons_nil_nil_absrd;
     179       destruct(cons_nil_nil_absrd)
     180  | 2: generalize in match nil_cons_absrd;
     181       <prfcr <nil_prf #HYP
     182       normalize in HYP;
     183       destruct(HYP)
     184  | 3: generalize in match cons_nil_absrd;
     185       <prfcr <cons_prf #HYP
     186       normalize in HYP;
     187       destruct(HYP)
     188  | 4: normalize in cons_cons_nil_absrd;
     189       destruct(cons_cons_nil_absrd)
     190  | 5: normalize in cons_cons_cons_prf;
     191       destruct(cons_cons_cons_prf)
     192       assumption
     193  | 6: generalize in match cons_cons_cons_prf;
     194       <refl_prf <prfcr <cons_prf #HYP
     195       normalize in HYP;
     196       destruct(HYP)
     197       @sym_eq assumption
    150198  ]
    151199qed.
  • src/RTL/RTL.ma

    r1060 r1061  
    1414  | rtl_st_int: register → Byte → label → rtl_statement
    1515  | rtl_st_move: register → register → label → rtl_statement
    16   | rtl_st_opaccs: inter → register → register → register → register → label → rtl_statement
    17   | rtl_st_op1: intermediate_op1 → register → register → label → rtl_statement
    18   | rtl_st_op2: intermediate_op2 → register → register → register → label → rtl_statement
     16  | rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement
     17  | rtl_st_op1: Op1 → register → register → label → rtl_statement
     18  | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
    1919  | rtl_st_clear_carry: label → rtl_statement
    2020  | rtl_st_load: register → register → register → label → rtl_statement
  • 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.