Changeset 1063


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

changes from today

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1062 r1063  
    1414 with precedence 10
    1515for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     16
     17definition ltb ≝
     18  λm, n: nat.
     19    leb (S m) n.
     20   
     21definition geb ≝
     22  λm, n: nat.
     23    ltb n m.
     24
     25definition gtb ≝
     26  λm, n: nat.
     27    leb n m.
     28
     29(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
     30let rec eq_nat (n: nat) (m: nat) on n: bool ≝
     31  match n with
     32  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
     33  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     34  ].
     35
     36let rec remove_n_first_internal
     37  (i: nat) (A: Type[0]) (l: list A) (n: nat)
     38    on l ≝
     39  match l with
     40  [ nil ⇒ [ ]
     41  | cons hd tl ⇒
     42    match eq_nat i n with
     43    [ true ⇒ l
     44    | _ ⇒ remove_n_first_internal (S i) A tl n
     45    ]
     46  ].
     47
     48definition remove_n_first ≝
     49  λA: Type[0].
     50  λn: nat.
     51  λl: list A.
     52    remove_n_first_internal 0 A l n.
     53   
     54let rec foldi_from_until_internal
     55  (A: Type[0]) (i: nat) (res: ?) (rem: list A) (m: nat) (f: nat → list A → A → list A)
     56    on rem ≝
     57  match rem with
     58  [ nil ⇒ res
     59  | cons e tl ⇒
     60    match geb i m with
     61    [ true ⇒ res
     62    | _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f
     63    ]
     64  ].
     65
     66definition foldi_from_until ≝
     67  λA: Type[0].
     68  λn: nat.
     69  λm: nat.
     70  λf: ?.
     71  λa: ?.
     72  λl: ?.
     73    foldi_from_until_internal A 0 a (remove_n_first A n l) m f.
     74
     75definition foldi_from ≝
     76  λA: Type[0].
     77  λn.
     78  λf.
     79  λa.
     80  λl.
     81    foldi_from_until A n (|l|) f a l.
     82
     83definition foldi_until ≝
     84  λA: Type[0].
     85  λm.
     86  λf.
     87  λa.
     88  λl.
     89    foldi_from_until A 0 m f a l.
     90
     91definition foldi ≝
     92  λA: Type[0].
     93  λf.
     94  λa.
     95  λl.
     96    foldi_from_until A 0 (|l|) f a l.
    1697
    1798definition hd ≝
     
    129210*)
    130211
    131 include "ASM/FoldStuff.ma".
    132 
    133212let rec reduce_strong
    134   (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left
    135   : Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |  ≝
    136   match left return λx. |x| = |right| → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    137   [ nil ⇒
    138     match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    139     [ nil ⇒ λnil_nil_prf. ?
    140     | cons hd tl ⇒ λnil_cons_absrd_prf. ?
    141     ]
     213  (A: Type[0]) (left: list A) (right: list A)
     214    on left : Σret: ((list A) × (list A)) × ((list A) × (list A)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
     215  match left with
     216  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
    142217  | cons hd tl ⇒
    143     match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    144     [ nil ⇒ λcons_nil_absrd_prf. ?
    145     | cons hd' tl' ⇒ λcons_cons_prf.
    146       let 〈commonl, commonr〉 ≝ eject … (reduce_strong A tl tl' ?) in ? (*
    147       [ dp clr their_proof ⇒ ? (*
    148         let 〈commonl, commonr〉 ≝ clr in ? *)
    149       ]*)
    150     ]
    151   ] prf.
    152   [ 5: normalize in cons_cons_prf;
    153        destruct(cons_cons_prf)
    154        assumption
    155   | 2: normalize in nil_cons_absrd_prf;
    156        destruct(nil_cons_absrd_prf)
    157   | 3: normalize in cons_nil_absrd_prf;
    158        destruct(cons_nil_absrd_prf)
    159   | 4:
     218    match right with
     219    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
     220    | cons hd' tl' ⇒
     221      let 〈cleft, cright〉 ≝ reduce_strong A tl tl' in
     222      let 〈commonl, restl〉 ≝ cleft in
     223      let 〈commonr, restr〉 ≝ cright in
     224        〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
     225    ]
     226  ].
     227  [ 1: normalize %
     228  | 2: normalize %
     229  | 3: normalize
     230       generalize in match (sig2 … (reduce_strong A tl tl1));
     231       >p2 >p3 >p4 normalize in ⊢ (% → ?)
     232       #HYP //
    160233  ]
    161234qed.
    162  
    163 axiom reduce_length:
    164   ∀A: Type[0].
    165   ∀left, right: list A.
    166   ∀prf: | left | = | right |.
    167     \fst (\fst (reduce A left right)) = \fst (\snd (reduce A left right)).
    168235   
    169236let rec map2_opt
     
    527594        ]
    528595    ].
    529    
    530 definition ltb ≝
    531   λm, n: nat.
    532     leb (S m) n.
    533    
    534 definition geb ≝
    535   λm, n: nat.
    536     ltb n m.
    537 
    538 definition gtb ≝
    539   λm, n: nat.
    540     leb n m.
    541    
    542 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
    543 let rec eq_nat (n: nat) (m: nat) on n: bool ≝
    544   match n with
    545   [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
    546   | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
    547   ].
    548596
    549597(* dpm: conflicts with library definitions
  • src/ASM/Vector.ma

    r998 r1063  
    8181    get_index_v A (S (n + m)) b n ?.
    8282  normalize
    83   //
     83  @le_S_S
     84  cases m //
    8485qed.
    8586
     
    179180  ] (? : S ? = S ?).
    180181  //
    181   [ destruct
    182   | lapply (injective_S … K)
    183     //
    184   ]
     182  lapply (injective_S … K)
     183  //
    185184qed.
    186185
     
    404403          ]
    405404    ].
    406   //
     405  /2/
    407406qed.
    408407
  • src/RTLabs/RTLAbstoRTL.ma

    r1062 r1063  
    7373  ].
    7474
     75axiom fresh_regs_length:
     76  ∀def: rtl_internal_function.
     77  ∀n: nat.
     78    |(\snd (fresh_regs def n))| = n.
     79   
    7580definition addr_regs ≝
    7681  λregs.
     
    487492  λsrcrs1.
    488493  λsrcrs2.
     494  λprf: |srcrs1| = |srcrs2|.
    489495  λstart_lbl.
    490496  λdest_lbl.
    491497  λdef.
    492   λprf: |srcrs1| = |srcrs2|.
    493498  match reduce_strong ? srcrs1 srcrs2 with
    494499  [ dp reduced first_reduced_proof ⇒
     
    586591  λdestrs: list register.
    587592  λtmp_destrs: list register.
     593  λdestrs_prf: |destrs| = |tmp_destrs|.
    588594  λsrcrs1: list register.
    589595  λdummy_lbl: label.
    590596  λi: nat.
    591   λtranslates.
    592   λsrcr2i.
    593   let 〈tmp_destrs1, tmp_destrs2〉 ≝ ? in ?.
    594 
    595 let translate_muli dummy tmpr destrs tmp_destrs srcrs1 dummy_lbl i translates
    596     srcr2i =
    597   let (tmp_destrs1, tmp_destrs2) = MiscPottier.split tmp_destrs i in
    598   translates @
    599     (match tmp_destrs2 with
    600       | [] -> []
    601       | tmp_destr2 :: tmp_destrs2 ->
    602         [adds_graph [RTL.St_clear_carry dummy_lbl ;
    603                      RTL.St_int (tmp_destr2, 0, dummy_lbl)] ;
    604          translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
    605          translate_cst (AST.Cst_int 0) tmp_destrs1 ;
    606          adds_graph [RTL.St_clear_carry dummy_lbl] ;
    607          translate_op I8051.Addc destrs destrs tmp_destrs])
     597  λi_prf.
     598  λtranslates: list ?.
     599  λsrcr2i: register.
     600  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
     601  let tmp_destrs2' ≝
     602    match tmp_destrs2 with
     603    [ nil ⇒ [ ]
     604    | cons tmp_destr2 tmp_destrs2 ⇒ [
     605        adds_graph [
     606          rtl_st_clear_carry dummy_lbl;
     607          rtl_st_int tmp_destr2 (zero ?) dummy_lbl
     608        ];
     609        translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
     610        translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
     611        adds_graph [
     612          rtl_st_clear_carry dummy_lbl
     613        ];
     614        translate_op Addc destrs destrs tmp_destrs destrs_prf
     615      ]
     616    ]
     617  in
     618    translates @ tmp_destrs2'.
     619
     620definition translate_mul ≝
     621  λdestrs: list register.
     622  λsrcrs1: list register.
     623  λsrcrs2: list register.
     624  λstart_lbl: label.
     625  λdest_lbl: label.
     626  λdef: rtl_internal_function.
     627  let 〈def, dummy〉 ≝ fresh_reg def in
     628  let 〈def, tmpr〉 ≝ fresh_reg def in
     629  let 〈def, tmp_destrs〉 ≝ fresh_regs def (|destrs|) in
     630  let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
     631  let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
     632  let insts_init ≝ [
     633    translate_move fresh_srcrs1 srcrs1;
     634    translate_move fresh_srcrs2 srcrs2;
     635    translate_cst (Ointconst I8 (zero ?)) destrs
     636  ]
     637  in
     638  let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
     639  let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
     640    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
     641
     642let translate_mul destrs srcrs1 srcrs2 start_lbl dest_lbl def =
     643  let (def, dummy) = fresh_reg def in
     644  let (def, tmpr) = fresh_reg def in
     645  let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
     646  let (def, fresh_srcrs1) = fresh_regs def (List.length srcrs1) in
     647  let (def, fresh_srcrs2) = fresh_regs def (List.length srcrs2) in
     648  let insts_init =
     649    [translate_move fresh_srcrs1 srcrs1 ;
     650     translate_move fresh_srcrs2 srcrs2 ;
     651     translate_cst (AST.Cst_int 0) destrs] in
     652  let f = λi. translate_muli dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl i ? in
     653  let insts_mul = MiscPottier.foldi f [] srcrs2 in
     654  add_translates (insts_init @ insts_mul) start_lbl dest_lbl def
    608655
    609656definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.