Changeset 1071 for src/RTL/RTLtoERTL.ma


Ignore:
Timestamp:
Jul 15, 2011, 2:40:40 PM (9 years ago)
Author:
mulligan
Message:

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r783 r1071  
    11include "RTL/RTL.ma".
    2 include "RTL/RTLTailcall.ma".
     2(* include "RTL/RTLTailcall.ma". *)
    33include "ERTL/ERTL.ma".
    4 include "utilities/RegisterSet.ma".
    54
    65definition change_exit_label ≝
     
    5251definition fresh_label ≝
    5352  λdef.
    54     match fresh LabelTag (ertl_if_luniverse def) with
    55     [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    56     | Error ⇒ None ?
    57     ].
     53    fresh LabelTag (ertl_if_luniverse def).
    5854   
    5955definition change_label ≝
     
    7672  | ertl_st_int r i _ ⇒ ertl_st_int r i l
    7773  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
    78   | ertl_st_opaccs opaccs d s1 s2 _ ⇒ ertl_st_opaccs opaccs d s1 s2 l
     74  | ertl_st_opaccs_a opaccs d s1 s2 _ ⇒ ertl_st_opaccs_a opaccs d s1 s2 l
     75  | ertl_st_opaccs_b opaccs d s1 s2 _ ⇒ ertl_st_opaccs_b opaccs d s1 s2 l
    7976  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
    8077  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
    8178  | ertl_st_clear_carry _ ⇒ ertl_st_clear_carry l
     79  | ertl_st_set_carry _ ⇒ ertl_st_set_carry l
    8280  | ertl_st_load d a1 a2 _ ⇒ ertl_st_load d a1 a2 l
    8381  | ertl_st_store a1 a2 s _ ⇒ ertl_st_store a1 a2 s l
    8482  | ertl_st_call_id f args _ ⇒ ertl_st_call_id f args l
    85   | ertl_st_cond_acc a i1 i2 ⇒ ertl_st_cond_acc a i1 i2
    86   | ertl_st_return a ⇒ ertl_st_return a
    87   ].
    88  
    89 let rec adds_graph (stmt_list: list ertl_statement) (start_lbl: label) (dest_lbl: label) (def: ertl_internal_function): option ertl_internal_function ≝
     83  | ertl_st_cond a i1 i2 ⇒ ertl_st_cond a i1 i2
     84  | ertl_st_return ⇒ ertl_st_return
     85  ].
     86 
     87let rec adds_graph
     88  (stmt_list: list ertl_statement) (start_lbl: label)
     89  (dest_lbl: label) (def: ertl_internal_function)
     90    on stmt_list ≝
    9091  match stmt_list with
    91   [ nil ⇒ Some ? def
    92   | cons hd tl
    93     match tl with
    94     [ nil ⇒ Some ? (add_graph start_lbl (change_label dest_lbl hd) def)
     92  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
     93  | cons stmt stmt_list
     94    match stmt_list with
     95    [ nil ⇒ add_graph start_lbl (change_label dest_lbl stmt) def
    9596    | _ ⇒
    96       let tmp_lbl ≝ fresh_label def in
    97       match tmp_lbl with
    98       [ Some tmp_lbl ⇒
    99         let stmt ≝ change_label tmp_lbl hd in
    100         let def ≝ add_graph start_lbl hd def in
    101           adds_graph tl tmp_lbl dest_lbl def
    102       | None ⇒ None ?
    103       ]
    104     ]
    105   ].
    106 
    107 let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function))
    108                        (start_lbl: label) (dest_lbl: label)
    109                        (def: ertl_internal_function): option ertl_internal_function ≝
     97      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
     98      let stmt ≝ change_label tmp_lbl stmt in
     99      let def ≝ add_graph start_lbl stmt def in
     100        adds_graph stmt_list tmp_lbl dest_lbl def
     101    ]
     102  ].
     103
     104let rec add_translates
     105  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
     106  (def: ertl_internal_function)
     107    on translate_list ≝
    110108  match translate_list with
    111   [ nil ⇒ Some ? def
    112   | cons hd tl
    113     match tl with
    114     [ nil ⇒ hd start_lbl dest_lbl def
     109  [ nil ⇒ add_graph start_lbl (ertl_st_skip dest_lbl) def
     110  | cons trans translate_list
     111    match translate_list with
     112    [ nil ⇒ trans start_lbl dest_lbl def
    115113    | _ ⇒
    116       let tmp_lbl ≝ fresh_label def in
    117       match tmp_lbl with
    118       [ Some tmp_lbl ⇒
    119         match hd start_lbl tmp_lbl def with
    120         [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def
    121         | None ⇒ None ?
    122         ]
    123       | None ⇒ None ?
    124       ]
    125     ]
    126   ].
    127  
    128 axiom fresh_reg: ertl_internal_function → ertl_internal_function × register.
    129 
    130 let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝
     114      let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
     115      let def ≝ trans start_lbl tmp_lbl def in
     116        add_translates translate_list tmp_lbl dest_lbl def
     117    ]
     118  ].
     119
     120axiom register_fresh: universe RegisterTag → register.
     121
     122definition fresh_reg: ertl_internal_function → ertl_internal_function × register ≝
     123  λdef.
     124    let r ≝ register_fresh (ertl_if_runiverse def) in
     125    let locals ≝ r :: ertl_if_locals def in
     126    let ertl_if_luniverse' ≝ ertl_if_luniverse def in
     127    let ertl_if_runiverse' ≝ ertl_if_runiverse def in
     128    let ertl_if_params' ≝ ertl_if_params def in
     129    let ertl_if_locals' ≝ locals in
     130    let ertl_if_stacksize' ≝ ertl_if_stacksize def in
     131    let ertl_if_graph' ≝ ertl_if_graph def in
     132    let ertl_if_entry' ≝ ertl_if_entry def in
     133    let ertl_if_exit' ≝ ertl_if_exit def in
     134      〈mk_ertl_internal_function
     135        ertl_if_luniverse' ertl_if_runiverse' ertl_if_params'
     136        ertl_if_locals' ertl_if_stacksize' ertl_if_graph'
     137        ertl_if_entry' ertl_if_exit', r〉.
     138
     139let rec fresh_regs
     140  (def: ertl_internal_function) (n: nat)
     141    on n ≝
    131142  match n with
    132143  [ O ⇒ 〈def, [ ]〉
     
    169180definition get_params_hdw ≝
    170181  λparams: list register.
    171   match length ? params with
    172   [ O ⇒ Some ? [ get_params_hdw_internal ]
     182  match params with
     183  [ nil ⇒ [get_params_hdw_internal]
    173184  | _ ⇒
    174     match zip ? ? params parameters with
    175     [ None ⇒ None ?
    176     | Some l ⇒ Some ? (save_hdws l)
    177     ]
     185    let l ≝ zip_pottier ? ? params parameters in
     186      save_hdws l
    178187  ].
    179188
     
    186195  let 〈def, addr2〉 ≝ fresh_reg def in
    187196  let 〈def, tmpr〉 ≝ fresh_reg def in
    188   let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
     197  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    189198  adds_graph [
    190199    ertl_st_frame_size addr1 start_lbl;
     
    199208  ] start_lbl dest_lbl def.
    200209 
    201 definition get_params_stack_internal ≝
    202   λi.
    203   λr.
    204     get_param_stack i r.
    205  
    206210definition get_params_stack ≝
    207211  λparams.
    208   match length ? params with
    209   [ O ⇒ [ get_params_hdw_internal ]
    210   | _ ⇒ mapi ? ? get_params_stack_internal params
     212  match params with
     213  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ]
     214  | _ ⇒
     215    let f ≝ λi. λr. get_param_stack i r in
     216      mapi ? ? f params
    211217  ].
    212218
     
    215221  let n ≝ min (length ? params) (length ? parameters) in
    216222  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    217   match get_params_hdw hdw_params with
    218   [ None ⇒ None ?
    219   | Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params))
    220   ].
     223  let hdw_params ≝ get_params_hdw hdw_params in
     224    hdw_params @ (get_params_stack stack_params).
    221225 
    222226definition add_prologue ≝
    223   λparams.
     227  λparams: list register.
    224228  λsral.
    225229  λsrah.
     
    227231  λdef.
    228232  let start_lbl ≝ ertl_if_entry def in
    229   let tmp_lbl ≝ fresh_label def in
    230   match tmp_lbl with
    231   [ None ⇒ None ?
    232   | Some tmp_lbl ⇒
    233     let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
    234     let params ≝
    235       match get_params params with
    236       [ Some params ⇒ params
    237       | None ⇒ [ ] (* dpm: is this ok? *)
    238       ] in
     233  let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in
     234  match lookup ? ? (ertl_if_graph def) start_lbl with
     235  [ None ⇒ ?
     236  | Some last_stmt ⇒
    239237    let def ≝
    240       add_translates (
    241         adds_graph [ ertl_st_new_frame start_lbl ] ::
    242         adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] ::
    243         save_hdws sregs @
    244         params) start_lbl tmp_lbl def in
    245     match def with
    246     [ Some def ⇒
    247       match last_stmt with
    248       [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def)
    249       | None ⇒ None ?
    250       ]
    251     | None ⇒ None ?
    252     ]
    253   ].
     238      add_translates
     239         ((adds_graph [
     240                     ertl_st_new_frame start_lbl
     241                   ]) ::
     242         (adds_graph [
     243                      ertl_st_pop sral start_lbl;
     244                      ertl_st_pop srah start_lbl
     245                   ]) ::
     246         (save_hdws sregs) @
     247         (get_params params))
     248        start_lbl tmp_lbl def
     249    in
     250      add_graph tmp_lbl last_stmt def
     251  ].
     252  cases not_implemented (* until Brian gives goahead for dep. types *)
     253qed.
     254
     255definition save_return ≝
     256  λret_regs.
     257  λstart_lbl: label.
     258  λdest_lbl: label.
     259  λdef: ertl_internal_function.
     260  let 〈def, tmpr〉 ≝ fresh_reg def in
     261  match reduce_strong ? RegisterSTS ret_regs with
     262  [ dp crl crl_proof ⇒
     263    let commonl ≝ \fst (\fst crl) in
     264    let commonr ≝ \fst (\snd crl) in
     265    let restl ≝ \snd (\fst crl) in
     266    let restr ≝ \snd (\snd crl) in
     267    let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in
     268    let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in
     269    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
     270    let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in
     271    let defaults ≝ map ? ? f_default restl in
     272      adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     273  ].
     274
     275let save_return ret_regs start_lbl dest_lbl def =
     276  let (def, tmpr) = fresh_reg def in
     277  let ((common1, rest1), (common2, _)) =
     278    MiscPottier.reduce I8051.sts ret_regs in
     279  let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in
     280  let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in
     281  let saves = List.map2 f_save common1 common2 in
     282  let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in
     283  let defaults = List.map f_default rest1 in
     284  adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
    254285 
    255286definition allocate_regs_internal ≝
Note: See TracChangeset for help on using the changeset viewer.