Module Annotations

Require Import AST Values.
Import Coqlib Integers.

Inductive ablock: Type :=
| ABlocal (depth: nat) (varname: ident) (range: int * int)
| ABglobal (b: ident) (range: int * int).

Definition annotation: Type := (ident * list ablock)%type.

Definition pair_eq_dec {X Y: Type}
           (xdec: forall x x': X, { x = x' } + { x <> x' })
           (ydec: forall y y': Y, { y = y' } + { y <> y' })
           (a a' : X * Y): { a = a' } + { a <> a' } :=
  let '(x, y) := a in
  let '(x', y') := a' in
  match xdec x x' with
  | left EQx => match ydec y y' with
                | left EQy => left (f_equal2 pair EQx EQy)
                | right NEy => right (fun K : (x, y) = (x', y') => NEy (f_equal snd K))
                end
  | right NEx => right (fun K : (x, y) = (x', y') => NEx (f_equal fst K))
  end.

Definition range_eq_dec := pair_eq_dec Int.eq_dec Int.eq_dec.

Definition ablock_eq: forall (alpha beta: ablock), {alpha = beta} + {alpha <> beta}.

Definition range_leb (x x': int * int) : bool :=
    let '(a, b) := x in
    let '(a', b') := x' in
    match Z.compare (Int.unsigned a) (Int.unsigned a') with
    | Lt => false
    | Gt | Eq =>
           match Z.compare (Int.unsigned b) (Int.unsigned b') with
           | Lt | Eq => true
           | Gt => false
           end
    end.

Definition offset_ablock (alpha: ablock) (ofs: int) : ablock :=
  match alpha with
  | ABlocal depth varname (base, bound) => ABlocal depth varname (Int.add base ofs, Int.add bound ofs)
  | ABglobal id (base, bound) => ABglobal id (Int.add base ofs, Int.add bound ofs)
  end.

Definition offset_annotation (alpha: annotation) (ofs: int): annotation :=
  (fst alpha, List.map (fun a => offset_ablock a ofs) (snd alpha)).

Definition annot_sem (find_symbol: ident -> option block) (sps: list val) (alpha: list ablock) (a: val) :=
  alpha = nil \/
  (exists depth varname base bound, In (ABlocal depth varname (base, bound)) alpha /\
                               exists sp ofs, nth_error sps depth = Some sp /\
                                         a = Val.add sp (Vint ofs) /\
                                         Int.unsigned base <= Int.unsigned ofs <= Int.unsigned bound) \/
  (exists id base bound, In (ABglobal id (base, bound)) alpha /\
                    exists b ofs, find_symbol id = Some b /\
                             a = Vptr b ofs /\
                             Int.unsigned base <= Int.unsigned ofs <= Int.unsigned bound).

Lemma annot_sem_preserved:
  forall find_symbol1 find_symbol2 sps alpha a,
    (forall id, find_symbol1 id = find_symbol2 id) ->
    (annot_sem find_symbol1 sps alpha a <-> annot_sem find_symbol2 sps alpha a).