source: src/RTLabs/RTLAbstoRTL.ma @ 789

include "RTLabs/syntax.ma".
include "RTL/RTL.ma".
include "common/AssocList.ma".
include "common/Graphs.ma".

definition add_graph ≝
  λlbl: label.
  λstmt.
  λdef.
  let f_labgen' ≝ f_labgen def in
  let f_reggen' ≝ f_reggen def in
  let f_sig' ≝ f_sig def in
  let f_result' ≝ f_result def in
  let f_params' ≝ f_params def in
  let f_locals' ≝ f_locals def in
  let f_ptrs' ≝ f_ptrs def in
  let f_stacksize' ≝ f_stacksize def in
  let f_graph' ≝ add ? ? (f_graph def) lbl stmt in
  let f_entry' ≝ f_entry def in
  let f_exit' ≝ f_exit def in
    mk_internal_function
      f_labgen' f_reggen' f_sig' f_result'
      f_params' f_locals' f_ptrs' f_stacksize'
      f_graph' f_entry' f_exit'.
      
definition fresh_label ≝
  λdef.
    match fresh LabelTag (f_labgen def) with
    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
    | Error ⇒ None ?
    ].

axiom fresh_reg: internal_function → internal_function × register.

let rec fresh_regs (def: internal_function) (n: nat) on n ≝
  match n with
  [ O   ⇒ 〈def, [ ]〉
  | S n ⇒
    let 〈def, res〉 ≝ fresh_regs def n in
    let 〈def, r〉 ≝ fresh_reg def in
      〈def, r :: res〉
  ].

definition addr_regs ≝
  λregs.
  match regs with
  [ cons hd tl ⇒
    match tl with
    [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
    | nil          ⇒ None (register × register)
    ]
  | nil ⇒ None (register × register)
  ].

inductive register_type: Type[0] ≝
  | register_int: register → register_type
  | register_ptr: register → register → register_type.

definition local_env ≝ assoc_list register register_type.

definition initialize_local_env_internal ≝
  λeq.
  λruniverse.
  λptrs.
  λlenv.
  λr.
    let fresh ≝ snd ? ? (fresh_reg runiverse) in
    let rt ≝
      match member ? eq r ptrs with
      [ true  ⇒ register_ptr r fresh
      | false ⇒ register_int r
      ]
    in
    assoc_list_add ? ? 〈r, rt〉 lenv.

definition initialize_local_env ≝
  λruniverse.
  λptrs.
  λregisters.
    foldl ? ? (initialize_local_env_internal (eq_identifier RegisterTag) runiverse ptrs) [ ] registers.

definition filter_and_to_list_local_env_internal ≝
  λlenv.
  λl.
  λr.
  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
  [ Some entry ⇒
    match entry with
    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
    | register_int r ⇒ (l @ [ r ])
    ]
  | None       ⇒ [ ] (* dpm: should this be none? *)
  ].

definition filter_and_to_list_local_env ≝
  λlenv.
  λregisters.
    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.

definition list_of_register_type ≝
  λrt.
  match rt with
  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
  | register_int r ⇒ [ r ]
  ].

definition find_and_list ≝
  λr.
  λlenv.
  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
  [ None      ⇒ [ ] (* dpm: should this be none? *)
  | Some lkup ⇒ list_of_register_type lkup
  ].

definition find_and_list_args ≝
  λargs.
  λlenv.
    map ? ? (λr. find_and_list r lenv) args.

definition find_and_addr ≝
  λr.
  λlenv.
  match find_and_list r lenv with
  [ cons hd tl ⇒
    match tl with
    [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
    | nil          ⇒ None ?
    ]
  | nil ⇒ None ? (* dpm: was assert false *)
  ].

definition rtl_args ≝
  λregs_list.
  λlenv.
    flatten ? (find_and_list_args regs_list lenv).

definition change_label ≝
  λlbl.
  λstmt.
  match stmt with
  [ rtl_st_skip _ ⇒ rtl_st_skip lbl
  | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
  | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
  | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
  | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl
  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
  | rtl_st_clear_carry _ ⇒ rtl_st_clear_carry lbl
  | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
  | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
  | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
  | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
  | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
  | rtl_st_return r ⇒ rtl_st_return r
  | _ ⇒ ?
  ].

let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) def ≝
  match stmt_list with
  [ nil ⇒ def
  | cons hd tl ⇒
    match tl with
    [ nil ⇒ add_graph start_lbl (change_lbl dest_lbl stmt) def
    | cons hd' tl' ⇒ ?
    ]
  ].

let rec adds_graph stmt_list start_lbl dest_lbl def = match stmt_list with
  | [] -> def
  | [stmt] ->
    add_graph start_lbl (change_label dest_lbl stmt) def
  | stmt :: stmt_list ->
    let tmp_lbl = fresh_label def in
    let stmt = change_label tmp_lbl stmt in
    let def = add_graph start_lbl stmt def in
    adds_graph stmt_list tmp_lbl dest_lbl def