Library ByteData

Require Import Coq.ZArith.ZArith.
Require Import FSets.FMaps.
Require Import FSets.FMapAVL.

Require Import Byte.
Require Import Fetch.

Open Local Scope N.

Module MN := FSets.FMapAVL.Make N_as_OT.

Definition Map_N_Byte : Type := MN.t Byte.

Definition find k (m: Map_N_Byte) := MN.find k m.

Definition update (p: N*Byte) (m: Map_N_Byte) := MN.add (fst p) (snd p) m.

Notation "k |-> v" := (pair k v) (at level 60).
Notation "[ ]" := (MN.empty Byte).
Notation "[ p1 , .. , pn ]" := (update p1 .. (update pn []) .. ).

Definition ByteData := N -> (@Fetch Byte).
Definition Disk := ByteData.

Bind Scope ByteData_scope with Disk.

Definition Disk_of_Map_N_Byte (map: Map_N_Byte) : Disk :=
  fun (key: N) => match (find key map) with
  | error => MissingAt key
  | value v => Found v
  end.

Coercion Disk_of_Map_N_Byte : Map_N_Byte >-> Disk.

Definition shift (bytes: ByteData) (shiftAmount index: N)
  : @Fetch Byte :=
  bytes (shiftAmount + index).