Module MemcpyTypes

Require Import AST.
Require Import Coqlib.
Require Import OptionMonad.

Inductive memcpy_typ: Set :=
  | SZ1: memcpy_typ | SZ2: memcpy_typ
  | SZ4: memcpy_typ | SZ8: memcpy_typ.

Local Open Scope Z_scope.

Definition Z_to_memcpy_typ (n: Z) :=
  match n with
  | 1 => Some SZ1
  | 2 => Some SZ2
  | 4 => Some SZ4
  | 8 => Some SZ8
  | _ => None
  end.

Definition memcpy_typ_to_Z (m: memcpy_typ) :=
  match m with
  | SZ1 => 1
  | SZ2 => 2
  | SZ4 => 4
  | SZ8 => 8
  end.

Lemma memcpy_typ_Z: forall n x,
  Z_to_memcpy_typ n = Some x <-> memcpy_typ_to_Z x = n.