source: src/ERTL/Uses.ma @ 939

include "ERTL/ERTL.ma".
include "utilities/BitVectorTrieSet.ma".
include "ASM/Arithmetic.ma".
include "ASM/I8051.ma".
include "common/Registers.ma".

definition count ≝
  λr: register.
  λuses.
    let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
      insert ? 16 l uses.
      
definition examine_statement ≝
  λstatement: ertl_statement.
  λuses.
  match statement with
  [ ertl_st_skip _ ⇒ uses
  | ertl_st_comment _ _ ⇒ uses
  | ertl_st_cost _ _ ⇒ uses
  | ertl_st_hdw_to_hdw _ _ _ ⇒ uses
  | ertl_st_new_frame _ ⇒ uses
  | ertl_st_del_frame _ ⇒ uses
  | ertl_st_clear_carry _ ⇒ uses
  | ertl_st_call_id _ _ _ ⇒ uses
  | ertl_st_return _ ⇒ uses
  | ertl_st_get_hdw r _ _ ⇒ count (word_of_register r) uses
  | ertl_st_set_hdw _ r _ ⇒ count (word_of_register r) uses
  | ertl_st_frame_size ar _ ⇒
    match ar with [
      mk_abstract_register r ⇒
        (* dpm: shift the abstract registers above the physical registers *)
        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
          count offset uses
    ]
  | ertl_st_pop ar _ ⇒
    match ar with [
      mk_abstract_register r ⇒
        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
          count offset uses
    ]
  | ertl_st_push ar _ ⇒
    match ar with [
      mk_abstract_register r ⇒
        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
          count offset uses
    ]
  | ertl_st_int ar _ _ ⇒ 
    match ar with [
      mk_abstract_register r ⇒
        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
          count offset uses
    ]
  | ertl_st_addr_h ar _ _ ⇒
    match ar with [
      mk_abstract_register r ⇒
        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
          count offset uses
    ]
  | ertl_st_addr_l ar _ _ ⇒
    match ar with [
      mk_abstract_register r ⇒
        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
          count offset uses
    ]
  | ertl_st_cond_acc ar _ _ ⇒
    match ar with [
      mk_abstract_register r ⇒
        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
          count offset uses
    ]
  | ertl_st_move ar1 ar2 _ ⇒
    match ar1 with [
      mk_abstract_register r1 ⇒
      match ar2 with [
        mk_abstract_register r2 ⇒
          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
            count offset1 (count offset2 uses)
      ]
    ]
  | ertl_st_op1 op1 ar1 ar2 _ ⇒
    match ar1 with [
      mk_abstract_register r1 ⇒
      match ar2 with [
        mk_abstract_register r2 ⇒
          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
            count offset1 (count offset2 uses)
      ]
    ]
  | ertl_st_op2 op2 ar1 ar2 ar3 _ ⇒
    match ar1 with [
      mk_abstract_register r1 ⇒
      match ar2 with [
        mk_abstract_register r2 ⇒
        match ar3 with [
          mk_abstract_register r3 ⇒
          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
            count offset1 (count offset2 (count offset3 uses))
        ]
      ]
    ]
  | ertl_st_opaccs opaccs ar1 ar2 ar3 _ ⇒
    match ar1 with [
      mk_abstract_register r1 ⇒
      match ar2 with [
        mk_abstract_register r2 ⇒
        match ar3 with [
          mk_abstract_register r3 ⇒
          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
            count offset1 (count offset2 (count offset3 uses))
        ]
      ]
    ]
  | ertl_st_load ar1 ar2 ar3 _ ⇒
    match ar1 with [
      mk_abstract_register r1 ⇒
      match ar2 with [
        mk_abstract_register r2 ⇒
        match ar3 with [
          mk_abstract_register r3 ⇒
          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
            count offset1 (count offset2 (count offset3 uses))
        ]
      ]
    ]
  | ertl_st_store ar1 ar2 ar3 _ ⇒
    match ar1 with [
      mk_abstract_register r1 ⇒
      match ar2 with [
        mk_abstract_register r2 ⇒
        match ar3 with [
          mk_abstract_register r3 ⇒
          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
          let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
            count offset1 (count offset2 (count offset3 uses))
        ]
      ]
    ]
  ].
  [*: normalize
      @ le_S @ le_S @ le_S @ le_S @ le_S @ le_S
      @ le_S @ le_S @ le_S @ le_S @ le_S @ le_n ]
qed.

(*
definition examine_internal ≝
  λint_fun.
    let uses ≝ foldr ? ? examine_statement (Stub ? ?) (ERTL_IF_Graph int_fun) in
      lookup uses.
*)