Module MemChunkTree

Require Import
  Coqlib
  AST Maps.

Set Implicit Arguments.

Module MemChunkTree <: TREE with Definition elt := memory_chunk.

  Definition elt := memory_chunk.
  Lemma elt_eq: forall (a b: elt), {a = b} + {a <> b}.
Proof.
decide equality. Defined.
  
  Record _t (A:Type) : Type := T
  { i8s: option A
  ; i8u: option A
  ; i16s: option A
  ; i16u: option A
  ; i32: option A
  ; f32: option A
  ; f64: option A
  }.

  Definition t: Type -> Type := _t.
  Lemma eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
                forall (a b: t A), {a = b} + {a <> b}.
Proof.
repeat decide equality. Defined.
  Definition empty A : t A := T None None None None None None None.
  Definition get A k (m: t A) : option A :=
    match k with
      | Mint8signed => i8s
      | Mint8unsigned => i8u
      | Mint16signed => i16s
      | Mint16unsigned => i16u
      | Mint32 => i32
      | Mfloat32 => f32
      | Mfloat64 => f64
    end A m.
  Definition upd A (k: elt) (v: option A) (m: t A) : t A.
    destruct m as [a b c d e f g].
    exact
    match k with
      | Mint8signed => T v b c d e f g
      | Mint8unsigned => T a v c d e f g
      | Mint16signed => T a b v d e f g
      | Mint16unsigned => T a b c v e f g
      | Mint32 => T a b c d v f g
      | Mfloat32 => T a b c d e v g
      | Mfloat64 => T a b c d e f v
    end.
  Defined.
  Definition set A k v (m: t A) : t A := upd k (Some v) m.
  Definition remove A k m : t A := upd k None m.

  Lemma gempty: forall (A: Type) (i: elt), get i (empty A) = None.
Proof.
now destruct i. Qed.
  Lemma gss: forall (A: Type) (i: elt) (x: A) (m: t A), get i (set i x m) = Some x.
Proof.
now destruct m; destruct i. Qed.
  Lemma gso: forall (A: Type) (i j: elt) (x: A) (m: t A),
    i <> j -> get i (set j x m) = get i m.
Proof.
destruct m. destruct i; destruct j; auto; congruence. Qed.
  Lemma gsspec: forall (A: Type) (i j: elt) (x: A) (m: t A),
    get i (set j x m) = if elt_eq i j then Some x else get i m.
Proof.
destruct m. destruct i; destruct j; auto. Qed.
  Lemma gsident: forall (A: Type) (i: elt) (m: t A) (v: A),
    get i m = Some v -> set i v m = m.
Proof.
destruct m. destruct i; simpl; congruence. Qed.
  Lemma grs: forall (A: Type) (i: elt) (m: t A), get i (remove i m) = None.
Proof.
destruct m. destruct i; auto. Qed.
  Lemma gro: forall (A: Type) (i j: elt) (m: t A),
    i <> j -> get i (remove j m) = get i m.
Proof.
destruct m. destruct i; destruct j; auto; congruence. Qed.
  Lemma grspec: forall (A: Type) (i j: elt) (m: t A),
    get i (remove j m) = if elt_eq i j then None else get i m.
Proof.
destruct m. destruct i; destruct j; auto. Qed.

Extensional equality between trees.
  Definition opt_beq A (cmp: A -> A -> bool) : option A -> option A -> bool :=
    fun x y =>
      match x, y with
        | Some a, Some b => cmp a b
        | None, None => true
        | _, _ => false
      end.
  Definition beq A (cmp: A -> A -> bool) (m1 m2: t A) : bool.
    destruct m1 as [a1 b1 c1 d1 e1 f1 g1].
    destruct m2 as [a2 b2 c2 d2 e2 f2 g2].
    exact (opt_beq cmp a1 a2 &&
           opt_beq cmp b1 b2 &&
           opt_beq cmp c1 c2 &&
           opt_beq cmp d1 d2 &&
           opt_beq cmp e1 e2 &&
           opt_beq cmp f1 f2 &&
           opt_beq cmp g1 g2).
  Defined.   Lemma beq_correct:
    forall (A: Type) (P: A -> A -> Prop) (cmp: A -> A -> bool),
    (forall (x y: A), cmp x y = true -> P x y) ->
    forall (t1 t2: t A), beq cmp t1 t2 = true ->
    forall (x: elt),
    match get x t1, get x t2 with
    | None, None => True
    | Some y1, Some y2 => P y1 y2
    | _, _ => False
    end.
Proof.
    destruct t1. destruct t2.
    unfold beq. intros.
    repeat rewrite andb_true_iff in *. intuition.
    destruct x; simpl;
    repeat match goal with
      | |- context[match ?a with None => _ | Some _ => _ end] =>
        destruct a
    end; simpl in *; eauto; try congruence.
  Qed.

Applying a function to all data of a tree.
  Definition map A B (h: elt -> A -> B) (m: t A) : t B.
    destruct m as [a b c d e f g].
    exact
      (T (option_map (h Mint8signed) a)
         (option_map (h Mint8unsigned) b)
         (option_map (h Mint16signed) c)
         (option_map (h Mint16unsigned) d)
         (option_map (h Mint32) e)
         (option_map (h Mfloat32) f)
         (option_map (h Mfloat64) g)).
  Defined.   Lemma gmap: forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A),
    get i (map f m) = option_map (f i) (get i m).
Proof.
destruct m. now destruct i. Qed.

Same as map, but the function does not receive the elt argument.
  Definition map1 A B (h: A -> B) (m: t A) : t B.
    destruct m as [a b c d e f g].
    exact
      (T (option_map h a)
         (option_map h b)
         (option_map h c)
         (option_map h d)
         (option_map h e)
         (option_map h f)
         (option_map h g)).
  Defined.   Lemma gmap1: forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
    get i (map1 f m) = option_map f (get i m).
Proof.
destruct m. now destruct i. Qed.

Applying a function pairwise to all data of two trees.
  Definition combine A B (h: option A -> option A -> option B) (m1 m2: t A) : t B.
    destruct m1 as [a1 b1 c1 d1 e1 f1 g1].
    destruct m2 as [a2 b2 c2 d2 e2 f2 g2].
    exact
      (T (h a1 a2) (h b1 b2) (h c1 c2) (h d1 d2) (h e1 e2) (h f1 f2) (h g1 g2) ).
  Defined.   Lemma gcombine:
    forall (A B: Type) (f: option A -> option A -> option B),
    f None None = None ->
    forall (m1 m2: t A) (i: elt),
    get i (combine f m1 m2) = f (get i m1) (get i m2).
Proof.
now destruct m1; destruct m2; destruct i. Qed.
  Lemma combine_commut:
    forall (A B: Type) (f g: option A -> option A -> option B),
    (forall (i j: option A), f i j = g j i) ->
    forall (m1 m2: t A),
    combine f m1 m2 = combine g m2 m1.
Proof.
destruct m1; destruct m2. simpl. congruence. Qed.

Enumerating the bindings of a tree.
  Definition opt_list A (e: elt) (x: option A) : list (elt * A) :=
    match x with
      | None => nil
      | Some y => (e, y) :: nil
    end.
  Definition elements A (m: t A) : list (elt * A).
    destruct m as [a b c d e f g].
    exact (opt_list Mint8signed a
        ++ opt_list Mint8unsigned b
        ++ opt_list Mint16signed c
        ++ opt_list Mint16unsigned d
        ++ opt_list Mint32 e
        ++ opt_list Mfloat32 f
        ++ opt_list Mfloat64 g).
  Defined.   Lemma elements_correct:
    forall (A: Type) (m: t A) (i: elt) (v: A),
    get i m = Some v -> In (i, v) (elements m).
Proof.
destruct m. destruct i; simpl; intros; subst; simpl; auto;
                      repeat (apply in_app; first [now left|right; intuition]).
  Qed.
  Lemma elements_complete:
    forall (A: Type) (m: t A) (i: elt) (v: A),
    In (i, v) (elements m) -> get i m = Some v.
Proof.
    destruct m.
    repeat match goal with
             | H : option A |- _ => destruct H
           end; simpl; intuition;
    match goal with
      | H : _ = _ |- _ => injection H; intros; subst; clear H; auto
    end.
  Qed.
  Lemma ref A (dec: {A} + {~A}) : A <-> if dec then True else False.
Proof.
intuition. Qed.
  Lemma elements_keys_norepet:
    forall (A: Type) (m: t A),
    list_norepet (List.map (@fst elt A) (elements m)).
Proof.
    destruct m.
    repeat match goal with
             | H : option A |- _ => destruct H
           end; simpl; intuition;
    match goal with
      | |- list_norepet ?l =>
        rewrite (ref (list_norepet_dec elt_eq l)); simpl; auto
    end.
  Qed.

Folding a function over all bindings of a tree.
  Definition fold A B (f: B -> elt -> A -> B) (m: t A) (v: B) : B :=
    List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
  Lemma fold_spec:
    forall (A B: Type) (f: B -> elt -> A -> B) (v: B) (m: t A),
    fold f m v =
    List.fold_left (fun a p => f a (fst p) (snd p)) (elements m) v.
    auto.
  Qed.
End MemChunkTree.
Generated by coq2html