Require Import ZArith.
Require Import List.
Require Import util.
Require Import presburgerZ.
Require Import machine_int.
Import MachineInt.
Require Import machine_int_spec.
Require Import sum.
Require Import state.
Require Import mips.
Require Import mapstos.
Require Import mips_contrib.
Require Import mips_tactics.
Require Import Znumtheory.

Open Local Scope asm_heap_scope.
Open Local Scope mips_scope.
Open Local Scope Z_scope.

(* generic functions *)

Fixpoint not_in (A: Set) (elt: A) (l: list A) {struct l} : Prop :=
  match l with
    | nil => True
    | hd::tl => (elt <> hd) /\ (not_in A elt tl)
  end.
Implicit Arguments not_in.

Fixpoint is_set (A: Set) (l: list A) {struct l} : Prop :=
  match l with
    | nil => True
    | hd::tl => (not_in hd tl) /\ (is_set A tl)
  end.
Implicit Arguments is_set.

Fixpoint chg_elt (A:Set) (l: list A) (ne: A) (index: nat) {struct l}: list A :=
  match l with
    | nil => nil
    | hd::tl => match index with
                  | O => ne::tl
                  | S index' => hd::(chg_elt A tl ne index')
                end
  end.
Implicit Arguments chg_elt [A].

Lemma chg_elt_app: forall (A: Set) (l1 l2: list A) (elt: A) (index: nat),
  (length l1 <= index)%nat ->
  chg_elt (l1 ++ l2) elt index = l1 ++ (chg_elt l2 elt (index - (length l1))%nat).
  induction l1.
  simpl; intros.
  cutrewrite (index - 0 = index)%nat; try omega; auto.
  simpl; intros.
  destruct index.
  assert False; [omega | contradiction].
  rewrite IHl1; auto.
  omega.
Qed.

(**********************************************************)
(*  Signed multiprecision integer (2's complement vers.)  *)
(**********************************************************)

(* sign of a multiprecision integer (k is the index of the most significant work) *)
(* false -> positive 
   true -> negative *)

Fixpoint ssum_k_sign (l:nat) (k:nat) (lst:list (int l)) {struct lst} : bool :=
  match lst with
    | nil => false
    | hd::tl => 
      match k with
	| O => 
          if (Zlt_bool (s2Z hd) 0) then                    
            true
            else
              false
	| S k' => (ssum_k_sign l k' tl)
      end
  end.
Implicit Arguments ssum_k_sign.

Lemma ssum_k_sign_false: forall A nk,
  s2Z (nth nk A zero32) >= 0 ->
  ssum_k_sign nk A = false.
  induction A; auto.
  simpl; intros.    
  destruct nk.
  generalize (Zlt_cases (s2Z a) 0); intros.
  destruct (Zlt_bool (s2Z a) 0).
  assert (~ (s2Z a < 0)).
  generalize H.
  PresburgerZ_decision.
  tauto.
  auto.
  rewrite IHA; auto.
Qed.

Lemma ssum_k_sign_true: forall A nk,
  length A = S nk -> 
  s2Z (nth nk A zero32) < 0 ->
  ssum_k_sign nk A = true.
  induction A; simpl; intros.
  simpl in H; discriminate.
  destruct nk.
  generalize (Zlt_cases (s2Z a) 0); intros.
  destruct (Zlt_bool (s2Z a) 0).
  auto.
  ContradictionZ.
  apply IHA; auto.
Qed.    

(* transformation of a signed multiprecision to an unsigned *)

Fixpoint ssum_lst2sum_lst (l:nat) (k:nat) (lst:list (int l)) {struct lst} : list (int l) :=
  match lst with
    | nil => nil
    | hd::tl => 
      match k with
	| O => 
          if (Zlt_bool (s2Z hd) 0) then                    
            (int_cplt2 hd)::tl
            else
              lst
	| S k' => 
          hd::(ssum_lst2sum_lst l k' tl)
      end
  end.
Implicit Arguments ssum_lst2sum_lst.

Lemma ssum_lst2sum_lst_eq: forall A nk,
  s2Z (nth nk A zero32) >= 0 ->
  ssum_lst2sum_lst nk A = A.
  induction A; auto.
  simpl; intros.    
  destruct nk.
  generalize (Zlt_cases (s2Z a) 0); intros.
  destruct (Zlt_bool (s2Z a) 0).
  assert (~ (s2Z a < 0)).
  generalize H.
  PresburgerZ_decision.
  tauto.
  auto.
  rewrite IHA; auto.
Qed.

Lemma ssum_lst2sum_lst_chg_elt : forall A nk,
  s2Z (nth nk A zero32) < 0 ->
  ssum_lst2sum_lst nk A = (chg_elt A (int_cplt2 (nth nk A zero32)) nk).
  
  induction A; auto.
  simpl; intros.
  destruct nk.
  generalize (Zlt_cases (s2Z a) 0); intros.
  destruct (Zlt_bool (s2Z a) 0).
  auto.
  ContradictionZ.
  rewrite IHA; auto.
Qed.

(* value of a signed multiprecision integer composed (k is the index of the most significant word) *)

Definition ssum_k (l:nat) (k:nat) (lst:list (int l)) : Z :=
  if (ssum_k_sign k lst) then
    - (sum_k k (ssum_lst2sum_lst k lst))
    else
      (sum_k k lst).
Implicit Arguments ssum_k.

(* value of a signed multiprecision integer composed (k is the size in words of the integer) *)

Definition sSum l k (lst: list (int l)) : Z :=
  match k with
    O => 0
    | S k' => ssum_k k' lst
  end.
Implicit Arguments sSum.

(* return the negation of an integer *)

Fixpoint negsSum (l:nat) (k:nat) (lst:list (int l)) {struct lst} : list (int l) :=
  match lst with
    | nil => nil
    | hd::tl => 
      match k with
	| O => (int_cplt2 hd)::tl
      	| S k' => 
          hd::(negsSum l k' tl)
      end
  end.
Implicit Arguments negsSum.
  
Lemma negsSum_chg_elt : forall A nk,
  negsSum nk A = (chg_elt A (int_cplt2 (nth nk A zero32)) nk).
  induction A; auto.
  simpl; intros.
  destruct nk.
  auto.
  rewrite IHA; auto.
Qed.

(**************************************************************)
(*  Signed multiprecision integer (signed magnitude version)  *)
(**************************************************************)

(* in progress... *)