Changeset 1285


Ignore:
Timestamp:
Oct 3, 2011, 3:08:21 PM (8 years ago)
Author:
mulligan
Message:

more implementation on maps, final push to get rtl abs to rtl working

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1283 r1285  
    216216    ] start_lbl dest_lbl def.
    217217
    218 (*
    219 definition translate_cast_signed
    220   λglobals.
     218definition translate_cast_signed:
     219    ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals
     220  λglobals: list ident.
    221221  λdestrs.
    222222  λsrcr.
     
    229229  let 〈def, dummy〉 ≝ fresh_reg … def in
    230230  let insts ≝ [
    231     rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
    232     rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
    233     rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
    234     rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
    235     rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
    236   ] in
     231    sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
     232    sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
     233    sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
     234    sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
     235    sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
     236  ]
     237  in
    237238  let srcrs ≝ make … tmpr (length … destrs) in
    238     add_translates [
    239       adds_graph insts;
    240       translate_move destrs srcrs
     239    add_translates rtl_params1 globals [
     240      adds_graph rtl_params1 globals insts;
     241      translate_move globals destrs srcrs
    241242    ] start_lbl dest_lbl def.
    242243
    243244definition translate_cast ≝
    244   λsrc_size.
    245   λsrc_sign.
    246   λdest_size.
    247   λdestrs.
    248   λsrcrs.
     245  λglobals: list ident.
     246  λsrc_size: nat.
     247  λsrc_sign: signedness.
     248  λdest_size: nat.
     249  λdestrs: list register.
     250  λsrcrs: list register.
    249251  match |srcrs| return λx. |srcrs| = x → ? with
    250   [ O ⇒ λzero_prf. adds_graph [ ]
     252  [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
    251253  | S n' ⇒ λsucc_prf.
    252254    if ltb dest_size src_size then
    253       translate_move destrs srcrs
     255      translate_move globals destrs srcrs
    254256    else
    255257      match reduce_strong register register destrs srcrs with
     
    259261        let restl ≝ \snd (\fst crl) in
    260262        let restr ≝ \snd (\snd crl) in
    261         let insts_common ≝ translate_move commonl commonr in
     263        let insts_common ≝ translate_move globals commonl commonr in
    262264        let sign_reg ≝ last_safe ? srcrs ? in
    263265        let insts_sign ≝
    264266          match src_sign with
    265           [ Unsigned ⇒ translate_cast_unsigned restl
    266           | Signed ⇒ translate_cast_signed restl sign_reg
     267          [ Unsigned ⇒ translate_cast_unsigned globals restl
     268          | Signed ⇒ translate_cast_signed globals restl sign_reg
    267269          ]
    268270        in
    269           add_translates [ insts_common; insts_sign ]
     271          add_translates rtl_params1 globals [ insts_common; insts_sign ]
    270272      ]
    271273  ] (refl ? (|srcrs|)).
     
    274276
    275277definition translate_negint ≝
    276   λdestrs.
    277   λsrcrs.
    278   λstart_lbl.
    279   λdest_lbl.
    280   λdef.
    281   λprf: | destrs | = | srcrs |. (* assert in caml code *)
    282   let 〈def, tmpr〉 ≝ fresh_reg def in
    283   let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
    284   let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
     278  λglobals: list ident.
     279  λdestrs: list register.
     280  λsrcrs: list register.
     281  λstart_lbl: label.
     282  λdest_lbl: label.
     283  λdef: rtl_internal_function globals.
     284  λprf: |destrs| = |srcrs|. (* assert in caml code *)
     285  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     286  let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
     287  let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
    285288  let insts_init ≝ [
    286     rtl_st_set_carry start_lbl;
    287     rtl_st_int tmpr (zero ?) start_lbl
     289    sequential … (SET_CARRY …);
     290    sequential … (INT rtl_params_ globals tmpr (zero ?))
    288291  ] in
    289   let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
     292  let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
    290293  let insts_add ≝ map … f_add destrs in
    291     adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
    292 
    293 definition translate_notbool ≝
    294   λdestrs.
    295   λsrcrs.
    296   λstart_lbl.
    297   λdest_lbl.
    298   λdef.
     294    adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
     295
     296definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     297  λglobals: list ident.
     298  λdestrs: list register.
     299  λsrcrs: list register.
     300  λstart_lbl: label.
     301  λdest_lbl: label.
     302  λdef: rtl_internal_function globals.
    299303  match destrs with
    300   [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     304  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
    301305  | cons destr destrs ⇒
    302     let 〈def, tmpr〉 ≝ fresh_reg def in
    303     let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
    304     let save_srcrs ≝ translate_move tmp_srcrs srcrs in
    305     let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
     306    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     307    let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
     308    let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
     309    let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
    306310    let f ≝ λtmp_srcr. [
    307       rtl_st_clear_carry start_lbl;
    308       rtl_st_int tmpr (zero ?) start_lbl;
    309       rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
    310       rtl_st_int tmpr (zero ?) start_lbl;
    311       rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
    312       rtl_st_op2 Xor destr destr tmpr start_lbl
     311      sequential … (CLEAR_CARRY rtl_params_ globals);
     312      sequential … (INT rtl_params_ globals tmpr (zero ?));
     313      sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
     314      sequential … (INT rtl_params_ globals tmpr (zero ?));
     315      sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
     316      sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
    313317    ] in
    314     let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
    315     let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
    316       add_translates [
    317         save_srcrs; adds_graph insts; epilogue
     318    let insts ≝ init_destr :: (flatten (map … f tmp_srcrs)) in
     319    let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
     320      add_translates rtl_params1 globals [
     321        save_srcrs; adds_graph rtl_params1 globals insts; epilogue
    318322      ] start_lbl dest_lbl def
    319323  ].
     324
     325(*
    320326
    321327(* TODO: examine this properly.  This is a change from the O'caml code due
  • src/utilities/adt/table_adt.ma

    r1274 r1285  
    1313  | empty: table dom_type rng_type
    1414  | node : nat → dom_type → rng_type → table dom_type rng_type → table dom_type rng_type → table dom_type rng_type.
    15  
    16 definition tbl_empty ≝ empty.
    17 
    18 definition tbl_size ≝
     15
     16definition tbl_height ≝
    1917  λdom_type : Type[0].
    2018  λrng_type : Type[0].
     
    2523  ].
    2624
     25let rec tbl_size
     26  (dom_type : Type[0]) (rng_type : Type[0]) (the_table: table dom_type rng_type)
     27    on the_table: nat ≝
     28  match the_table with
     29  [ empty ⇒ 0
     30  | node sz key val l r ⇒ S (tbl_size … l) + (tbl_size … r)
     31  ].
     32 
     33definition tbl_empty ≝
     34  λdom_type: Type[0].
     35  λrng_type: Type[0].
     36    empty dom_type rng_type.
     37
     38definition tbl_is_empty ≝
     39  λdom_type: Type[0].
     40  λrng_type: Type[0].
     41  λthe_table: table dom_type rng_type.
     42  match the_table with
     43  [ empty ⇒ true
     44  | _     ⇒ false
     45  ].
     46
     47definition tbl_is_empty_p ≝
     48  λdom_type: Type[0].
     49  λrng_type: Type[0].
     50  λthe_table: table dom_type rng_type.
     51  match the_table with
     52  [ empty ⇒ True
     53  | _     ⇒ False
     54  ].
     55
    2756let rec tbl_to_list
    2857  (dom_type: Type[0]) (rng_type: Type[0]) (the_table: table dom_type rng_type)
     
    3261  | node sz key val l r ⇒ 〈key, val〉 :: tbl_to_list … l @ tbl_to_list … r
    3362  ].
    34  
    35 axiom tbl_insert : ∀key_type, rng_type. key_type → rng_type → table key_type rng_type → table key_type rng_type.
    36 
    37 axiom tbl_merge:
    38   ∀key_type, rng_type.
    39     (key_type → key_type → order) → table key_type rng_type → table key_type rng_type → table key_type rng_type.
    40 
    41 axiom tbl_remove : ∀key_type, rng_type. key_type → table key_type rng_type → table key_type rng_type.
     63
     64let rec tbl_min_binding
     65  (key_type: Type[0]) (rng_type: Type[0]) (the_table: table key_type rng_type)
     66    (proof: ¬ (tbl_is_empty_p … the_table))
     67      on the_table: key_type × rng_type ≝
     68  match the_table return λx. ¬ (tbl_is_empty_p … x) → key_type × rng_type with
     69  [ empty               ⇒ λabsurd. ?
     70  | node sz key val l r ⇒ λproof.
     71    match l return λx. x = l → key_type × rng_type with
     72    [ empty ⇒ λproof. 〈key, val〉
     73    | _     ⇒ λproof. tbl_min_binding key_type rng_type l ?
     74    ] (refl … l)
     75  ] proof.
     76  [1: normalize in absurd;
     77      elim absurd;
     78      #ABSURD
     79      @⊥ @ABSURD @I
     80  |2: <proof
     81      normalize
     82      /2/
     83  ]
     84qed.
     85
     86definition tbl_create ≝
     87  λkey_type: Type[0].
     88  λrng_type: Type[0].
     89  λleft    : table key_type rng_type.
     90  λkey     : key_type.
     91  λval     : rng_type.
     92  λright   : table key_type rng_type.
     93  let hl ≝ tbl_height … left in
     94  let hr ≝ tbl_height … right in
     95  let height ≝ if gtb hl hr then hl + 1 else hr + 1 in
     96    node key_type rng_type height key val left right.
     97     
     98let rec tbl_balance
     99  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
     100    (left: table key_type rng_type) (key: key_type) (val: rng_type)
     101      (right: table key_type rng_type) (left_proof: ¬ (tbl_is_empty_p … left))
     102        (right_proof: ¬ (tbl_is_empty_p … right))
     103          on left: table key_type rng_type ≝
     104  match gtb (tbl_height … left) ((tbl_height … right) + 2) with
     105  [ true  ⇒
     106    match left return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
     107    [ empty              ⇒ λabsurd. ?
     108    | node _ lv ld ll lr ⇒ λnon_empty_proof.
     109      if gtb (tbl_height … ll) (tbl_height … lr) then
     110        tbl_create … ll lv ld (tbl_create … lr key val right)
     111      else
     112        match lr return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
     113        [ empty ⇒ λabsurd. ?
     114        | node _ lrv lrd lrl lrr ⇒ λ
     115            tbl_create … (tbl_create … ll lv ld lrl) lrv lrd (tbl_create … lrr key val right)
     116        ]
     117    ] left_proof
     118  | false ⇒ ?
     119  ].
     120  [1: normalize in absurd;
     121      elim absurd
     122      #ABSURD
     123      @⊥ @ABSURD @I
     124  |*: cases daemon
     125  ]
     126qed.
     127 
     128let rec tbl_remove_min_binding
     129  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
     130    (the_table: table key_type rng_type) (proof: ¬ (tbl_is_empty_p … the_table))
     131      on the_table: table key_type rng_type ≝
     132  match the_table return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
     133  [ empty               ⇒ λabsurd. ?
     134  | node sz key val l r ⇒ λproof.
     135    match l return λx. x = l → table key_type rng_type with
     136    [ empty ⇒ λproof. r
     137    | _     ⇒ λproof. tbl_balance … ord (tbl_remove_min_binding … ord l ?) key val r
     138    ] (refl … l)
     139  ] proof.
     140  [1: normalize in absurd;
     141      elim absurd;
     142      #ABSURD
     143      @⊥ @ABSURD @I
     144  |2: <proof
     145      normalize
     146      @nmk //
     147  ]
     148qed.
     149   
     150let rec tbl_insert
     151  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
     152    (key: key_type) (val: rng_type) (the_table: table key_type rng_type)
     153      on the_table: table key_type rng_type ≝
     154  match the_table with
     155  [ empty                 ⇒ node … 1 key val (empty …) (empty …)
     156  | node sz key' val' l r ⇒
     157    match ord key key' with
     158    [ order_lt ⇒ tbl_balance … ord (tbl_insert … ord key val l) key' val' r
     159    | order_eq ⇒ node … sz key val l r
     160    | order_gt ⇒ tbl_balance … ord l key' val' (tbl_insert … ord key val r)
     161    ]
     162  ].
     163 
     164let rec tbl_merge
     165  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
     166    (left: table dom_type rng_type) (right: table dom_type rng_type)
     167      on left: table dom_type rng_type ≝
     168  match left with
     169  [ empty ⇒ right
     170  | _     ⇒
     171    match right return λx. x = right → table dom_type rng_type with
     172    [ empty               ⇒ λid_proof. left
     173    | node sz key val l r ⇒ λid_proof.
     174      let 〈x, d〉 ≝ tbl_min_binding dom_type rng_type right ? in
     175        tbl_balance … ord left x d (tbl_remove_min_binding … ord right ?)
     176    ] (refl … right)
     177  ].
     178  <id_proof
     179  normalize /2/
     180qed.
     181
     182let rec tbl_remove
     183  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
     184    (key: key_type) (the_table: table key_type rng_type)
     185      on the_table: table key_type rng_type ≝
     186  match the_table with
     187  [ empty                 ⇒ empty …
     188  | node sz key' val' l r ⇒
     189    match ord key key' with
     190    [ order_lt ⇒ tbl_balance … ord (tbl_remove … ord key l) key' val' r
     191    | order_eq ⇒ tbl_merge … ord l r
     192    | order_gt ⇒ tbl_balance … ord l key' val' (tbl_remove … ord key r)
     193    ]
     194  ].
    42195 
    43196let rec tbl_find
     
    87240  | node sz key val l r ⇒ f val ∨ tbl_exists … f l ∨ tbl_exists … f r
    88241  ].
    89  
    90 axiom tbl_equal  : ∀key_type, rng_type. table key_type rng_type
    91                     → table key_type rng_type → bool.
     242     
     243axiom tbl_equal:
     244  ∀key_type, rng_type.
     245    (key_type → key_type → order) → (rng_type → rng_type → order) →
     246      table key_type rng_type → table key_type rng_type → bool.
    92247
    93248let rec tbl_mapi
     
    117272  | node sz key val l r ⇒ tbl_fold … f r (f key val (tbl_fold … f l seed))
    118273  ].
    119 
    120 definition tbl_is_empty ≝
    121   λkey_type : Type[0].
    122   λrng_type : Type[0].
    123   λtable    : table key_type rng_type.
    124     tbl_size … table = 0.
    125274
    126275definition tbl_singleton ≝
     
    129278  λkey      : key_type.
    130279  λrng      : rng_type.
    131     tbl_insert … key rng (tbl_empty …).
     280    node key_type rng_type 1 key rng (empty …) (empty …).
    132281
    133282definition tbl_from_list ≝
    134283  λkey_type : Type[0].
    135284  λrng_type : Type[0].
     285  λord      : key_type → key_type → order.
    136286  λthe_list : list (key_type × rng_type).
    137287    foldr … (λkey_rng.
    138288      let 〈key, rng〉 ≝ key_rng in
    139         tbl_insert … key rng) (tbl_empty …) the_list.
     289        tbl_insert … ord key rng) (tbl_empty …) the_list.
    140290
    141291definition tbl_filter ≝
    142292  λdom_type : Type[0].
    143293  λrng_type : Type[0].
     294  λord      : dom_type → dom_type → order.
    144295  λf        : rng_type → bool.
    145296  λthe_table: table dom_type rng_type.
    146297  let as_list  ≝ tbl_to_list … the_table in
    147298  let filtered ≝ filter … (λx. f (\snd x)) as_list in
    148     tbl_from_list … filtered.
    149 
     299    tbl_from_list … ord filtered.
     300
Note: See TracChangeset for help on using the changeset viewer.