Changeset 1047 for src/RTLabs


Ignore:
Timestamp:
Jun 29, 2011, 5:38:27 PM (8 years ago)
Author:
mulligan
Message:

more work from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1046 r1047  
    3030    ].
    3131
    32 axiom fresh_reg: rtl_internal_function → rtl_internal_function × register.
    33 
     32axiom register_fresh: universe RegisterTag → register.
     33
     34definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝
     35  λdef.
     36    let r ≝ register_fresh (rtl_if_runiverse def) in
     37    let locals ≝ r :: rtl_if_locals def in
     38    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
     39    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
     40    let rtl_if_sig' ≝ rtl_if_sig def in
     41    let rtl_if_result' ≝ rtl_if_result def in
     42    let rtl_if_params' ≝ rtl_if_params def in
     43    let rtl_if_locals' ≝ locals in
     44    let rtl_if_stacksize' ≝ rtl_if_stacksize def in
     45    let rtl_if_graph' ≝ rtl_if_graph def in
     46    let rtl_if_entry' ≝ rtl_if_entry def in
     47    let rtl_if_exit' ≝ rtl_if_exit def in
     48      〈mk_rtl_internal_function
     49        rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig' rtl_if_result'
     50        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
     51        rtl_if_entry' rtl_if_exit', r〉.
     52       
    3453let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
    3554  match n with
     
    4968    | nil          ⇒ None (register × register)
    5069    ]
    51   | nil ⇒ None (register × register)
    52   ].
     70  | nil ⇒ None (register × register) (* registers are not an address *)
     71  ].
     72
     73let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
     74  match n with
     75  [ O ⇒ [ ]
     76  | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
     77  ].
     78
     79definition choose_rest ≝
     80  λA: Type[0].
     81  λleft, right: list A.
     82  match left with
     83  [ nil ⇒
     84    match right with
     85    [ nil ⇒ None ?
     86    | _ ⇒ Some ? right
     87    ]
     88  | _ ⇒ Some ? left
     89  ].
     90
     91definition complete_regs ≝
     92  λdef.
     93  λsrcrs1.
     94  λsrcrs2.
     95  let nb_added ≝ abs ((length ? srcrs1) - (length ? srcrs2)) in
     96  let 〈def, added_regs〉 ≝ fresh_regs def nb_added in
     97    if gtb nb_added 0 then
     98      〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
     99    else
     100      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
     101
     102definition size_of_sig_type ≝
     103  λsig.
     104  match sig with
     105  [ ASTint isize sign ⇒
     106    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
     107      Some ? (isize' ÷ (nat_of_bitvector ? int_size))
     108  | ASTfloat _ ⇒ None ?
     109  | ASToffset ⇒ Some ? (nat_of_bitvector ? int_size)
     110  | ASTptr rgn ⇒ Some ? (nat_of_bitvector ? ptr_size)
     111  ].
     112
     113definition concrete_size ≝ .
     114
     115definition concrete_offset ≝ .
    53116
    54117inductive register_type: Type[0] ≝
     
    246309  [ cast_int i ⇒
    247310    match destrs with
    248     [ nil ⇒ None ?
     311    [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
    249312    | cons hd tl ⇒
    250313      match tl with
     
    253316      ]
    254317    ]
    255   | cast_addr_symbol id ⇒
     318  | cast_addrsymbol id ⇒
    256319    match destrs with
    257320    [ nil ⇒ None ?
     
    263326      ]
    264327    ]
    265   | cast_stack_offset off ⇒
     328  | cast_offset off ⇒
    266329    match destrs with
    267330    [ nil ⇒ None ?
     
    280343      ]
    281344    ]
    282   | cast_float f ⇒ None ?
     345  | cast_stack ⇒ ?
     346  | cast_sizeof size ⇒ ?
     347  (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *)
    283348  ].
    284349
Note: See TracChangeset for help on using the changeset viewer.