Require Import Pip.Model.ADT.
Require Import List PeanoNat Lt Lia Coq.Logic.Classical_Prop Bool Coq.Program.Tactics.
Import List.ListNotations.

Fixpoint eqList {A : Type} (l1 l2 : list A) (eq : A → A → bool) : bool :=
 match l1, l2 with
 |nil,nil ⇒ true
 |a::l1' , b::l2' ⇒ if eq a b then eqList l1' l2' eq else false
 |_ , _ ⇒ false
end.

Definition beqPairs {A B: Type} (a : (A×B)) (b : (A×B)) (eqA : A → A → bool) (eqB : B → B → bool) :=
if (eqA (fst a) (fst b)) && (eqB (snd a) (snd b)) then true else false.

Fixpoint lookup {A B C: Type} (k : A) (i : B) (assoc : list ((A × B)*C)) (eqA : A → A → bool) (eqB : B → B → bool) :=
  match assoc with
    | nil ⇒ None
    | (a, b) :: assoc' ⇒ if beqPairs a (k,i) eqA eqB then Some b else lookup k i assoc' eqA eqB
  end.

Fixpoint removeDup {A B C: Type} (k : A) (i : B) (assoc : list ((A × B)*C) )(eqA : A → A → bool) (eqB : B → B → bool) :=
  match assoc with
    | nil ⇒ nil
    | (a, b) :: assoc' ⇒ if beqPairs a (k,i) eqA eqB then removeDup k i assoc' eqA eqB else (a, b) :: (removeDup k i assoc' eqA eqB)
  end.

Definition add {A B C: Type} (k : A) (i : B) (v : C) (assoc : list ((A × B)*C) ) (eqA : A → A → bool) (eqB : B → B → bool) :=
  (k,i,v) :: removeDup k i assoc eqA eqB.

Program Fixpoint getNextVaddrAux (indexList : list index) : bool × (list index) :=
match indexList with
| nil ⇒ (true, nil)
| h::t ⇒ if (fst (getNextVaddrAux t)) then
              if (Nat.eq_dec (h+1) tableSize) then
                (true, (Build_index 0 _)::(snd (getNextVaddrAux t)))
              else
                (false, (Build_index (h+1) _::(snd (getNextVaddrAux t))))
            else
                (false, (Build_index h _::(snd (getNextVaddrAux t))))
end.




Definition getNextVaddr (va : vaddr) : vaddr :=
CVaddr (snd (getNextVaddrAux va)).

Fixpoint getNthVAddrFromAux (start : vaddr) (range : nat) : vaddr :=
match range with
| 0 ⇒ start
| S n ⇒ getNthVAddrFromAux (getNextVaddr start) n
end.

Obligation Tactic := idtac.

Program Fixpoint firstVAddrGreaterThanSecondAux (firstIndexList secondIndexList : list index)
(HlenVAddr : length firstIndexList = length secondIndexList)
: bool :=
match (firstIndexList, secondIndexList) with
| (nil, nil) ⇒ true
| (hf::tf, hs::ts) ⇒ let hs_le_hf := Nat.leb hs hf in
                      if (hs_le_hf) then
                        true
                      else
                      let differentHeads := negb (Nat.eqb hf hs) in
                      if (differentHeads) then
                        false
                      else
                        firstVAddrGreaterThanSecondAux tf ts _
| (_,_) ⇒ False_rect _ _
end.





Obligation Tactic := program_simpl.