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

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

(* XXX having to specify the return type in the match is annoying. *)
definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝
λinit.
match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst I8 i)))
| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst I16 i)))
| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst I32 i)))
| Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
| Init_space n         ⇒ None ?
| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst I8 (zero ?)))))
| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
].

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

definition init_datum : ident → region → init_data → nat (*offset*) → stmt ≝
λid,r,init,off.
match init_expr init with
[ None ⇒ St_skip
| Some x ⇒
    match x with [ dp chunk e ⇒
      St_store ? r chunk (Cst ? (Oaddrsymbol id off)) e
    ]
].

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

definition init_vars : list (ident × region × (list init_data)) → stmt ≝
λvars. foldr ??
  (λvar,s. St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd 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_return f)
                                           (f_params f)
                                           (f_vars f)
                                           (f_stacksize f)
                                           (St_seq s (f_body f)))〉
          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
          ]
      | inr _ ⇒ 〈id',f'〉 ]).

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

definition replace_init : Cminor_program → Cminor_noinit_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)).