Module Encodable

Require Import ZArith.
Require Import Lattices.
Require Import CodeGen.
Require Import Concrete.
Require Import LibTactics.

Open Scope Z_scope.

The type L is encodable to integers if we have the following two-way mapping.

Class Encodable (L : Type) := {
  labToZ : L -> Z;
  ZToLab : Z -> L;
  ZToLab_labToZ_id : forall l, l = ZToLab (labToZ l)

The two-point lattice elements are encodable to integers.
Program Instance EncodableHL : Encodable Lab := {

  labToZ l :=
    match l with
      | L => boolToZ false
      | H => boolToZ true

  ;ZToLab z :=
    match z with
      | 0 => L
      | _ => H


Next Obligation.
destruct l; auto. Qed.

Connecting vectors of encodable labels to triples of concrete (integer) tags.
Section Encodable.

Context {T : Type}
        {ET : Encodable T}.

Lemma labToZ_inj: forall (l1 l2: T), labToZ l1 = labToZ l2 -> l1 = l2.
  rewrite (ZToLab_labToZ_id l1).
  rewrite (ZToLab_labToZ_id l2).
  apply f_equal; auto.

Import Vector.VectorNotations.
Local Open Scope nat_scope.

Definition nth_labToZ {n:nat} (vls: Vector.t T n) (m:nat) : Z :=
  match le_lt_dec n m with
  | left _ => dontCare
  | right p => labToZ (Vector.nth_order vls p)

Lemma of_nat_lt_proof_irrel:
  forall (m n: nat) (p q: m < n),
    Fin.of_nat_lt p = Fin.of_nat_lt q.
  induction m; intros.
    destruct n.
      false; omega.
    destruct n.
      false; omega.
      simpl; erewrite IHm; eauto.

Lemma nth_order_proof_irrel:
  forall (m n: nat) (v: Vector.t T n) (p q: m < n),
    Vector.nth_order v p = Vector.nth_order v q.
  unfold Vector.nth_order.
  erewrite of_nat_lt_proof_irrel; eauto.

Lemma nth_order_valid: forall (n:nat) (vls: Vector.t T n) m,
  forall (lt: m < n),
  nth_labToZ vls m = labToZ (Vector.nth_order vls lt).
  unfold nth_labToZ.
  destruct (le_lt_dec n m).
  false; omega.
  erewrite nth_order_proof_irrel; eauto.

Definition labsToZs {n:nat} (vls :Vector.t T n) : (Z * Z * Z) :=
(nth_labToZ vls 0,
 nth_labToZ vls 1,
 nth_labToZ vls 2).

End Encodable.