Module CstrC

Require String.
Require Import Itv.
Require Export LinTerm.
Require Import Debugging.
Require Export DomainInterfaces.

Open Scope option.

Module Type CstrSig <: CondSig QNum.

  Parameter t: Type.

  Parameter sat: t -> Mem.t QNum.t -> Prop.

  Parameter mayDependOn: t -> PVar.t -> Prop.
  Parameter sat_mdo: mdoExt mayDependOn sat Logic.eq.

  Definition Incl (c1: t) (c2: t): Prop
    := forall m, sat c1 m -> sat c2 m.
  Hint Unfold Incl: pedraQ.

  Parameter isIncl: t -> t -> bool.
  Parameter IsIncl_correct: forall c1 c2: t, If isIncl c1 c2 THEN Incl c1 c2.
  Hint Resolve IsIncl_correct: pedraQ.

  Parameter isContrad: t -> bool.
  Parameter IsContrad_correct: forall c: t, If isContrad c THEN forall m, ~(sat c m).
  Hint Resolve IsContrad_correct: pedraQ.

  Parameter top: t.
  Parameter top_correct: forall m, sat top m.

  Parameter add: t -> t -> t.
  Parameter Add_correct: forall (c1 c2: t) m,
    sat c1 m -> sat c2 m -> sat (add c1 c2) m.

  Parameter mul: QNum.t -> t -> t.
  Parameter mul_correct: forall n c m, sat c m -> sat (mul n c) m.

  Parameter merge: t -> t -> t.
  Parameter Merge_correct: forall c1 c2 m, sat c1 m -> sat c2 m -> sat (merge c1 c2) m.

  Parameter split: t -> option (t * t).
  Parameter split_correct: forall c, WHEN p <- split c THEN Incl c (fst p) /\ Incl c (snd p).

  Hint Resolve top_correct Add_correct mul_correct Merge_correct split_correct: pedraQ.

  Parameter isFree: PVar.t -> t -> bool.
  Parameter isFree_correct: forall (x: PVar.t) (c: t), (If (isFree x c) THEN ~(mayDependOn c x)).
  Hint Resolve isFree_correct:pedraQ.

  Parameter rename: PVar.t -> PVar.t -> t -> t.
  Parameter rename_correct: forall (x y:PVar.t) (l:t) m,
    (sat (rename x y l) m)=(sat l (Mem.assign x (m y) m)).

  Parameter pr: t -> String.string.

End CstrSig.

Module CstrImpl (L: LinSig QNum) <: CstrSig.

  Record tInd: Type := mk { coefs: L.t; typ: cmpT; cst: QNum.t }.
  Definition t := tInd.

  Definition sat (c: t) m: Prop
    := QNum.cmpDenote (typ c) (L.eval (coefs c) m) (cst c).

  Definition mayDependOn (c:t) (x: PVar.t) : Prop :=
    L.mayDependOn (coefs c) x.

  Lemma sat_mdo: mdoExt mayDependOn sat Logic.eq.

  Definition top := {| coefs:= L.nil; typ:= EqT; cst:=QNum.z |}.
  
  Lemma top_correct m: sat top m.
  Hint Resolve top_correct: pedraQ.

  Definition Incl (c1: t) (c2: t): Prop
    := forall m, sat c1 m -> sat c2 m.

  Definition isInclEq (c1 c2: t): bool :=
    match (typ c2) with
      | EqT =>
        if QNum.eqDec (cst c1) (cst c2) then true else false
      | LtT =>
        if QNum.ltLeDec (cst c1) (cst c2) then true else false
      | LeT =>
        if QNum.ltLeDec (cst c2) (cst c1) then false else true
    end.
  Extraction Inline isInclEq.
  
  Lemma isInclEq_correct c1 c2:
    (typ c1 = EqT) -> L.Eq (coefs c1) (coefs c2) ->
    If isInclEq c1 c2 THEN Incl c1 c2.
  Hint Local Resolve isInclEq_correct: pedraQ.
  
  Definition isInclLt (c1 c2: t): bool :=
    match (typ c2) with
      | LtT | LeT =>
        if QNum.ltLeDec (cst c2) (cst c1) then false else true
      | _ => false
    end.
  Extraction Inline isInclLt.

  Lemma isInclLt_correct c1 c2:
    (typ c1 = LtT) -> L.Eq (coefs c1) (coefs c2) ->
    If isInclLt c1 c2 THEN Incl c1 c2.
  Hint Local Resolve isInclLt_correct: pedraQ.

  Definition isInclLe (c1 c2: t): bool :=
    match (typ c2) with
      | LtT =>
        if QNum.ltLeDec (cst c1) (cst c2) then true else false
      | LeT =>
        if QNum.ltLeDec (cst c2) (cst c1) then false else true

      | _ => false
    end.
  Extraction Inline isInclLe.

  Lemma isInclLe_correct c1 c2:
    (typ c1 = LeT) -> L.Eq (coefs c1) (coefs c2) ->
    If isInclLe c1 c2 THEN Incl c1 c2.
  Hint Local Resolve isInclLe_correct: pedraQ.

  Definition isIncl (c1 c2: t): bool :=
    L.isEq (coefs c1) (coefs c2)
    &&& match typ c1 with
          | EqT => isInclEq c1 c2
          | LtT => isInclLt c1 c2
          | LeT => isInclLe c1 c2
        end.

  Ltac destructyp c H :=
    elimtype (exists x, (typ c)=x); eauto;
      let cmp:=fresh "cmp" in
        intros cmp H; rewrite !H in * |- *; destruct cmp; simpl.

  Lemma IsIncl_correct c1 c2: If isIncl c1 c2 THEN Incl c1 c2.
  Hint Resolve IsIncl_correct: pedraQ.
  Global Opaque isIncl.

  Definition isContrad (c: t): bool :=
    L.isEq (coefs c) L.nil
    &&& match typ c with
          | EqT => if QNum.eqDec QNum.z (cst c) then false else true
          | LtT => if QNum.ltLeDec QNum.z (cst c) then false else true
          | LeT => if QNum.ltLeDec (cst c) QNum.z then true else false
        end.
  
  Lemma IsContrad_correct c': If isContrad c' THEN forall m, ~(sat c' m).
  Hint Resolve IsContrad_correct: pedraQ.

  Definition cmpAdd: cmpT -> cmpT -> cmpT
    := fun t1 t2 =>
      match t1 with
        | EqT => t2
        | LtT => LtT
        | LeT =>
          match t2 with
            | EqT => LeT
            | LeT => LeT
            | LtT => LtT
          end
      end.

  Definition add (c1 c2: t): t :=
    mk (L.add (coefs c1) (coefs c2)) (cmpAdd (typ c1) (typ c2))
    (QNum.add (cst c1) (cst c2)).

  Lemma Add_correct: forall (c1 c2: t) m,
    sat c1 m -> sat c2 m -> sat (add c1 c2) m.

  Definition mulSimpl (c: t) n: t :=
    mk (L.mul n (coefs c)) (typ c) (QNum.mul n (cst c)).

  Lemma mulSimpl_correct: forall (c: t) n (hn: typ c = EqT \/ not (QNum.Le n QNum.z))
    m, sat c m -> sat (mulSimpl c n) m.
    intros c n hn x; unfold sat, mulSimpl; simpl;
      destruct hn as [hn | hn];
        [ rewrite hn; simpl; rewrite (L.Mul_correct n (coefs c) x); intro h; rewrite h; trivial
          | destruct (typ c); simpl; rewrite (L.Mul_correct n (coefs c) x)].
    - intro h; rewrite h; trivial.
    - apply QNum.MulLe1, QNum.LtLe, QNum.LtNotLe.
    assumption.
    - apply QNum.MulLt, QNum.LtNotLe.
    assumption.
  Qed.