include "common/Values.ma".
include "joint/BEValues.ma".
include "common/Mem.ma".

(* Transform between lists of "back-end" (i.e., byte by byte) values and the
   front-end values.  Note that the memory_chunk arguments are mostly used to
   resolve the sizes; they are not strictly checked. *)

let rec make_parts (r:region) (n:nat) (H:le n (size_pointer r)) on n : list (part r) ≝
match n return λn.le n ? → ? with 
[ O ⇒ λ_. [ ]
| S m ⇒ λH'. mk_part r n H::(make_parts r m ?)
] H.
/2/
qed.

definition make_be_null : region → list beval ≝
λr. map ?? (λp. BVnull r p) (make_parts r (size_pointer r) ?).
//
qed.

let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝
match n return λn. BitVector (n*8) → ? with
[ O ⇒ λ_. [ ]
| S m ⇒ λv. let 〈h,t〉 ≝ split ??? v in h::(bytes_of_bitvector m t)
] v.

definition fe_to_be_values : memory_chunk → val → list beval ≝
λc,v. match v with
[ Vundef ⇒ make_list ? BVundef (size_chunk c)
| Vint sz i ⇒ map ?? (λb.BVByte b) (bytes_of_bitvector ? (i⌈bvint sz ↦ BitVector (size_intsize sz * 8)⌉))
| Vfloat _ ⇒ make_list ? BVundef (size_chunk c) (* unsupported *)
| Vptr ptr ⇒ bevals_of_pointer ptr
| Vnull r ⇒ make_be_null r
].
cases sz in i ⊢ %; //
qed.

let rec check_be_ptr ptr n t on t ≝
match t with
[ nil ⇒ eqb (size_pointer (ptype ptr)) n
| cons hd tl ⇒
    match hd with
    [ BVptr ptr' pt ⇒ eq_pointer ptr ptr' ∧ eqb (part_no ? pt) n ∧ check_be_ptr ptr (S n) tl
    | _ ⇒ false
    ]
].

let rec check_be_null r n t on t ≝
match t with
[ nil ⇒ eqb (size_pointer r) n
| cons hd tl ⇒
    match hd with
    [ BVnull r' pt ⇒ eq_region r r' ∧ eqb (part_no ? pt) n ∧ check_be_null r (S n) tl
    | _ ⇒ false
    ]
].

let rec build_integer (n:nat) (l:list beval) : option (BitVector (times n 8)) ≝
match n return λn. option (BitVector (n*8)) with
[ O ⇒ match l with [ nil ⇒ Some ? [[ ]] | cons _ _ ⇒ None ? ]
| S m ⇒
    match l with
    [ nil ⇒ None ?
    | cons h t ⇒
        match h with
        [ BVByte b ⇒
            option_map ?? (λtl. b @@ tl) (build_integer m t)
        | _ ⇒ None ?
        ]
    ]
].

definition build_integer_val : memory_chunk → list beval → val ≝
λc,l.
match c with
[ Mint8unsigned ⇒ option_map_def ?? (Vint I8) Vundef (build_integer 1 l)
| Mint8signed ⇒ option_map_def ?? (Vint I8) Vundef (build_integer 1 l)
| Mint16unsigned ⇒ option_map_def ?? (Vint I16) Vundef (build_integer 2 l)
| Mint16signed ⇒ option_map_def ?? (Vint I16) Vundef (build_integer 2 l)
| Mint32 ⇒ option_map_def ?? (Vint I32) Vundef (build_integer 4 l)
| _ ⇒ Vundef
].

definition be_to_fe_value : memory_chunk → list beval → val ≝
λc,l. match l with
[ nil ⇒ Vundef
| cons h t ⇒
    match h with
    [ BVundef ⇒ Vundef
    | BVByte b ⇒ build_integer_val c l
    | BVptr ptr pt ⇒ if eqb (part_no ? pt) O ∧ check_be_ptr ptr (S O) t then Vptr ptr else Vundef
    | BVnull r pt ⇒ if eqb (part_no ? pt) O ∧ check_be_null r (S O) t then Vnull r else Vundef
    ]
].