(* Replace initialisation of global variables with equivalent Cminor code. *)

include "Cminor/syntax.ma".
include "common/Globalenvs.ma".

definition init_expr : init_data → option (memory_chunk × expr) ≝
λinit.
match init with
[ Init_int8 i          ⇒ Some ? 〈Mint8unsigned, Cst (Ointconst i)〉
| Init_int16 i         ⇒ Some ? 〈Mint16unsigned, Cst (Ointconst i)〉
| Init_int32 i         ⇒ Some ? 〈Mint32, Cst (Ointconst i)〉
| Init_float32 f       ⇒ Some ? 〈Mfloat32, Cst (Ofloatconst f)〉
| Init_float64 f       ⇒ Some ? 〈Mfloat64, Cst (Ofloatconst f)〉
| Init_space n         ⇒ None ?
| Init_null r          ⇒ Some ? 〈Mpointer r, Op1 (Optrofint r) (Cst (Ointconst zero))〉
| Init_addrof r id off ⇒ Some ? 〈Mpointer r, Cst (Oaddrsymbol id off)〉
].

(* Produces a few extra skips - hopefully the compiler will optimise these
   away. *)

definition init_datum : ident → init_data → int (*offset?*) → stmt ≝
λid,init,off.
match init_expr init with
[ None ⇒ St_skip
| Some x ⇒
    let 〈chunk, e〉 ≝ x in
    St_store chunk (Cst (Oaddrsymbol id off)) e
].

definition init_var : ident → list init_data → stmt ≝
λid,init.
\snd (foldr ??
  (λdatum,os.
   let 〈off,s〉 ≝ os in
     〈addition_n ? off (repr (size_init_data datum)), St_seq (init_datum id datum off) s〉)
  〈zero, St_skip〉 init).

definition init_vars : list (ident × (list init_data) × region × unit) → stmt ≝
λvars. foldr ??
  (λvar,s. St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst (\fst var))))) St_skip vars.

definition add_statement : ident → stmt →
                              list (ident × (fundef internal_function)) →
                              list (ident × (fundef internal_function)) ≝
λid,s.
  map ??
    (λidf.
      let 〈id',f'〉 ≝ idf in
      match ident_eq id id' with
      [ inl _ ⇒
          match f' with
          [ Internal f ⇒ 〈id, Internal ? (mk_internal_function
                                           (f_sig f)
                                           (f_params f)
                                           (f_vars f)
                                           (f_ptrs f)
                                           (f_stacksize f)
                                           (St_seq s (f_body f)))〉
          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
          ]
      | inr _ ⇒ 〈id',f'〉 ]).

definition empty_vars : list (ident × (list init_data) × region × unit) →
                        list (ident × (list init_data) × region × unit) ≝
map ?? (λv. 〈〈〈\fst (\fst (\fst v)),
               [Init_space (size_init_data_list (\snd (\fst (\fst v))))]〉,
              \snd (\fst v)〉,
              \snd v〉).

definition replace_init : Cminor_program → Cminor_program ≝
λp.
  mk_program ??
    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
    (prog_main ?? p)
    (empty_vars (prog_vars ?? p)).