Library BaseAsrtDef

Require Import include.
Require Import memory.
Require Import memdata.
Require Import Lists.ListSet.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Export inferules.
Notation "$ n" := (Int.repr n) (at level 41):int_scope.
Notation "V$ n" := (Vint32 (Int.repr n)) (at level 41):int_scope.
Notation "id +ᵢ n" := (Int.add id n)
  (at level 42, format "'[' id '/ ' '+ᵢ' '/ ' n ']'"):int_scope.
Notation "id -ᵢ n" := (Int.sub id n)
  (at level 42, format "'[' id '/ ' '-ᵢ' '/ ' n ']'"):int_scope.
Notation "n << m" := (Int.shl n m)
  (at level 42, format "'[' n '/ ' '<<' '/ ' m ']'"):int_scope.
Notation "n >>ᵢ m" := (Int.shru n m)
  (at level 42, format "'[' n '/ ' '>>ᵢ' '/ ' m ']'"):int_scope.
Notation "n & m" := (Int.and n m)
  (at level 42, format "'[' n '/ ' '&' '/ ' m ']'"):int_scope.
Open Scope int_scope.

Definition isptr v := v = Vnull \/ exists p, v = Vptr p.

Fixpoint Aarray´ (l:addrval) n t vl :=
  match vl, n with
    | nil,0 => Aemp
    | v :: vl´, S n´ =>
      let (b,i) := l in
      PV l @ t |-> v ** Aarray´ (b, (Int.add i (Int.repr (Z_of_nat (typelen t))))) n´ t vl´
    | _, _ => Afalse
  end.

Definition Aarray l t vl :=
  match t with
    | Tarray t´ n => Aarray´ l n t´ vl
    | _ => Afalse
  end.

Definition LAarray x t vl :=
  EX l, L& x @ t == l ** Aarray l t vl.

Definition GAarray x t vl :=
  EX l, G& x @ t == l ** Aarray l t vl.

Definition id_addrval (l:addrval) (id:var) (t:type) :=
  match t with
  | Tstruct s dcls => match field_offset id dcls with
                      | Some off => let (b,i):=l in
                                      Some (b, Int.add i off)
                      | None => None
                      end
  | _ => None
  end.

Fixpoint Aarray_rm (l:addrval) (n:nat) (t:type) (vl:list val) (m:nat) {struct vl}:=
  match l with
    | (b,i) =>
      match vl with
        | nil => Aemp
        | cons v vl´ => match n with
                          | 0 => Afalse
                          | S n´ =>
                            match m with
                              | 0 => Aarray´ (b, Int.add i (Int.repr (BinInt.Z.of_nat (typelen t)))) n´ t vl´
                              | S m´ => PV l @ t |-> v ** Aarray_rm (b, Int.add i (Int.repr (BinInt.Z.of_nat (typelen t)))) n´ t vl´ m´
                            end
                        end
      end
  end.

Fixpoint array_type_vallist_match (t:type) (vl:vallist) {struct vl}:=
  match vl with
  | nil => True
  | v::vl´ => rule_type_val_match t v = true /\ array_type_vallist_match t vl´
  end.

Fixpoint Astruct´ (l : addrval) dls vl {struct dls}:=
  match vl, dls with
    | nil,dnil => Aemp
    | v :: vl´, dcons id t dls´ =>
        match t with
        | Tarray t´ n => let (b,i):=l in Astruct´ (b, (Int.add i (Int.repr (Z_of_nat (typelen t))))) dls´ vl´
        | Tstruct _ _ => let (b,i):=l in Astruct´ (b, (Int.add i (Int.repr (Z_of_nat (typelen t))))) dls´ vl´
        | _ => let (b,i):=l in
               PV l @ t |-> v ** Astruct´ (b, (Int.add i (Int.repr (Z_of_nat (typelen t))))) dls´ vl´
        end
    | _, _ => Afalse
  end.

Definition Astruct l t vl :=
  match t with
    | Tstruct id dls => Astruct´ l dls vl
    | _ => Afalse
  end.

Fixpoint Astruct_rm (l:addrval) (dls:decllist) (vl:list val) (id:ident) {struct vl}:=
  match l with
    | (b,i) =>
      match vl with
        | nil => Aemp
        | cons v vl´ => match dls with
                      | dnil => Afalse
                      | dcons id´ t dls´ =>
                        if Zbool.Zeq_bool id id´
                        then
                          Astruct´ (b,Int.add i (Int.repr (BinInt.Z.of_nat (typelen t)))) dls´ vl´
                        else
                          match t with
                            | Tarray t´ n => Astruct_rm (b, Int.add i (Int.repr (BinInt.Z.of_nat (typelen t)))) dls´ vl´ id
                            | Tstruct _ _ => Astruct_rm (b, Int.add i (Int.repr (BinInt.Z.of_nat (typelen t)))) dls´ vl´ id
                            | _ => PV l @ t |-> v ** (Astruct_rm (b, Int.add i (Int.repr (BinInt.Z.of_nat (typelen t)))) dls´ vl´ id)
                          end
                    end
      end
  end.

Fixpoint struct_type_vallist_match´ dls vl {struct vl}:=
  match vl, dls with
    | nil,dnil => True
    | v :: vl´, dcons id t dls´ =>
        match t with
        | Tarray t´ n => struct_type_vallist_match´ dls´ vl´
        | Tstruct id ds => struct_type_vallist_match´ dls´ vl´
        | _ => rule_type_val_match t v =true/\ struct_type_vallist_match´ dls´ vl´
        end
    | _, _ => False
  end.

Definition struct_type_vallist_match t vl :=
  match t with
    | Tstruct id dls => struct_type_vallist_match´ dls vl
    | _ => False
  end.


Fixpoint nth_val (n : nat) (vl : vallist) {struct vl}:=
  match vl with
    | nil => None
    | v::vl´ => match n with
                  | 0 => Some v
                  | S n´ => nth_val n´ vl´
                end
  end.

Fixpoint nth_id (n : nat) (decl : decllist){struct decl} :=
  match decl with
    | dnil => None
    | dcons id t decl´ => match n with
                  | 0 => Some id
                  | S n´ => nth_id n´ decl´
                end
  end.

Fixpoint nth_vallist (n : nat) (ll:list vallist) {struct ll} :=
  match ll with
    | nil => None
    | l::ll´ => match n with
                  | 0 => Some l
                  | S n´ => nth_vallist n´ ll´
                end
  end.

Fixpoint update_nth_val (n : nat) (vl : vallist) (v : val){struct vl} :=
  match vl with
    | nil => nil
    | v´::vl´ => match n with
                  | 0 => v::vl´
                  | S n´ => v´::(update_nth_val n´ vl´ v)
                end
  end.

Fixpoint id_nth´ id decl n:=
  match decl with
    | dnil => None
    | dcons id´ t decl´=> match Zbool.Zeq_bool id id´ with
                            | true => Some n
                            | false => id_nth´ id decl´ (S n)
                          end
  end.

Definition id_nth id decl := id_nth´ id decl 0.

Definition update_nth_val_op n vl v:=
  match NPeano.Nat.ltb n (length vl) with
    | false => None
    | true => Some (update_nth_val n vl v)
  end.

Fixpoint remove_nth_val (n : nat) (vl : vallist){struct vl} :=
  match vl with
    | nil => nil
    | v´::vl´ => match n with
                  | 0 => vl´
                  | S n´ => v´::(remove_nth_val n´ vl´)
                end
  end.

Definition remove_nth_val_op n vl :=
  match NPeano.Nat.ltb n (length vl) with
    | false => None
    | true => Some (remove_nth_val n vl)
  end.

Fixpoint remove_nth_vallist (n : nat) (vl : list vallist) {struct vl} :=
  match vl with
    | nil => nil
    | v´::vl´ => match n with
                  | 0 => vl´
                  | S n´ => v´::(remove_nth_vallist n´ vl´)
                end
  end.

Definition remove_nth_vallist_op n vl:=
  match NPeano.Nat.ltb n (length vl) with
    | false => None
    | true => Some (remove_nth_vallist n vl)
  end.

Definition node (v:val) (vl:vallist) (t:type) :=
  EX b, [| v= Vptr (b,Int.zero) /\ struct_type_vallist_match t vl |] ** Astruct (b,Int.zero) t vl.

Fixpoint sllseg (head tailnext : val) (l:list vallist) (t:type) (next: vallist -> option val):=
  match l with
    | nil => [| head = tailnext |]
    | vl::l´ => [| head <> Vnull |] ** EX vn, [|next vl = Some vn|] **
                node head vl t ** sllseg vn tailnext l´ t next
  end.

Definition sll head l t next := sllseg head Vnull l t next.

Fixpoint dllseg (head headprev tail tailnext : val) (l:list vallist)
         (t:type) (pre next: vallist -> option val):=
  match l with
    | nil => [| head = tailnext |] ** [| headprev = tail |]
    | vl::l´ => [| head <> Vnull |] ** EX vn,
                [|next vl = Some vn|] ** [|pre vl = Some headprev|] **
                node head vl t ** dllseg vn head tail tailnext l´ t pre next
  end.

Definition dll head tail l t pre n:= dllseg head Vnull tail Vnull l t pre n.

Fixpoint nth_val´ n vl :=
  match vl with
  | nil => Vundef
  | (v :: vl´)%list =>
    match n with
    | 0 => v
    | S n´ => nth_val´ n´ vl´
    end
  end.

Close Scope int_scope.