Module AssignD


Require Export ASCond.
Require Import Debugging.
Require Import Itv.

Require Import MSets.MSetPositive.
Require MSetDecide.
Module PositiveSetDecide := MSetDecide.Decide(PositiveSet).
Require MSetFacts.
Module Import PositiveSetFacts:=MSetFacts.Facts(PositiveSet).
Require Export Setoid.
Require Export Relation_Definitions.

Existing Instance PositiveSet.eq_equiv.

Module CoreAssign (N: NumSig) (Cond: ASCondSig N) (D: AbstractDomain N Cond) (R: HasRename N D).

  Import Cond.


  Definition encode (b:bool) (p:positive) :=
    if b
      then xI p
      else xO p.

  Definition decode (p:positive) :=
    match p with
      | xH => xH
      | xI p => p
      | xO p => p
    end.

  Lemma decode_encode_id b (p:positive) : decode (encode b p)=p.
Proof.
    unfold decode, encode; case b; simpl; auto.
  Qed.

  Hint Resolve decode_encode_id: vpl.

  Definition encodeE r x := encode (PositiveSet.mem x r) x.
  Definition encodeO r x := encode (negb (PositiveSet.mem x r)) x.


  Lemma encode_unalias: forall r x x0,
    (encodeO r x) <> (encodeE r x0).
Proof.
    unfold encodeO, encodeE; intros r x x0; case (PVar.eq_dec x0 x).
    - intros; subst; destruct (PositiveSet.mem x r); simpl; discriminate.
    - intros H1 H2; case H1; generalize H2; clear H1 H2.
    destruct (PositiveSet.mem x r); destruct (PositiveSet.mem x0 r); simpl; intro H; inversion H; auto.
  Qed.
  Hint Resolve encode_unalias: vpl.


  Definition decodeIn (r:PositiveSet.t) (aux m: Mem.t N.t) (p:positive) :=
    match p with
      | xH => (aux xH)
      | xI p => if PositiveSet.mem p r then m p else aux (xI p)
      | xO p => if PositiveSet.mem p r then aux (xO p) else m p
    end.

  Lemma decode_encodeE r aux m x: decodeIn r aux m (encodeE r x) = m x.
Proof.
    unfold decodeIn, encodeE, encode.
    elimtype (exists b, (PositiveSet.mem x r)=b); eauto.
    intro b; destruct b; intro H; rewrite H; simpl; rewrite H; simpl; auto.
  Qed.

  Hint Resolve decode_encodeE: vpl.
  Hint Rewrite decode_encodeE: vpl.

  Local Opaque PositiveSet.mem.

  Lemma decode_diff_encodeE r aux m x: x <> (encodeE r (decode x)) -> decodeIn r aux m x = aux x.
Proof.
    unfold decodeIn, encodeE, encode; destruct x as [p | p | ]; simpl;
      try (destruct (PositiveSet.mem p r); simpl; intuition).
    destruct (PositiveSet.mem 1 r); simpl; auto.
  Qed.

  Lemma decode_encodeO r aux m x: decodeIn r aux m (encodeO r x) = aux (encodeO r x).
Proof.
    unfold decodeIn, encodeO, encode.
    elimtype (exists b, (PositiveSet.mem x r)=b); eauto.
    intro b; destruct b; intro H; rewrite H; simpl; rewrite H; simpl; auto.
  Qed.

  Hint Rewrite decode_encodeO: vpl.

  Lemma decodeIn_simplify r aux1 m1 aux2 m2 x:
    (x=(encodeE r (decode x)) -> m1 (decode x) = m2 (decode x))
    ->(x<>(encodeE r (decode x)) -> aux1 x = aux2 x)
    -> decodeIn r aux1 m1 x = decodeIn r aux2 m2 x.
Proof.
    unfold decodeIn, encodeE, encodeO, encode; destruct x as [ p | p | ]; simpl;
      try (destruct (PositiveSet.mem p r); simpl; intros H H0; try (apply H0; intro; discriminate); intuition).
    case (PositiveSet.mem 1 r); simpl; intros H H0; try (apply H0; intro; discriminate); intuition.
  Qed.




  Fixpoint switch (m:PositiveSet.t) (i: positive) : PositiveSet.t :=
    match m with
      | PositiveSet.Leaf => PositiveSet.add i PositiveSet.Leaf
      | PositiveSet.Node l o r =>
        match i with
          | xH => PositiveSet.node l (negb o) r
          | xO p => PositiveSet.node (switch l p) o r
          | xI p => PositiveSet.node l o (switch r p)
        end
    end.

  Local Opaque PositiveSet.node.
  Local Transparent PositiveSet.mem.

  Lemma switch_out m: forall x y, y<>x -> PositiveSet.mem y (switch m x) = PositiveSet.mem y m.
Proof.
    induction m; simpl.
    + intros x y H. generalize (PositiveSet.add_spec PositiveSet.Leaf x y).
    unfold PositiveSet.In;
      destruct (PositiveSet.mem y (PositiveSet.add x PositiveSet.Leaf));
        destruct (PositiveSet.mem y PositiveSet.Leaf); intuition.
    + intro x; destruct x; simpl; intros y; rewrite PositiveSet.mem_node;
      destruct y; simpl; intuition.
  Qed.

  Lemma switch_in m: forall x, PositiveSet.mem x (switch m x) = negb (PositiveSet.mem x m).
Proof.
    induction m; simpl.
    + intros x; generalize (PositiveSet.add_spec PositiveSet.Leaf x x).
    unfold PositiveSet.In; simpl.
    cutrewrite (PositiveSet.mem x PositiveSet.Leaf = false); simpl.
    - destruct (PositiveSet.mem x (PositiveSet.add x PositiveSet.Leaf));
      intuition.
    - case x; simpl; auto.
    + intro x; destruct x; rewrite PositiveSet.mem_node; simpl; auto.
  Qed.
  Hint Rewrite switch_in: vpl.

  Local Opaque switch PositiveSet.mem.

  Lemma decode_sw_encodeE r aux m x:
    decodeIn (switch r x) aux m (encodeE r x) = aux (encodeE r x).
Proof.
    unfold decodeIn, encodeE, encode.
    elimtype (exists b, (PositiveSet.mem x r)=b); eauto.
    intro b; destruct b; intro H; rewrite H; simpl; rewrite switch_in; rewrite H; simpl; auto.
  Qed.

  Lemma decode_sw_encodeO r aux m x:
    decodeIn (switch r x) aux m (encodeO r x) = m x.
Proof.
    unfold decodeIn, encodeO, encode.
    elimtype (exists b, (PositiveSet.mem x r)=b); eauto.
    intro b; destruct b; intro H; rewrite H; simpl; rewrite switch_in; rewrite H; simpl; auto.
  Qed.
  Hint Rewrite decode_sw_encodeE decode_sw_encodeO: vpl.

  Lemma decode_sw_out r aux m x y:
    y <> (encodeE r x) -> y <> (encodeO r x) ->
    decodeIn (switch r x) aux m y =
    decodeIn r aux m y.
Proof.
    unfold decodeIn, encodeE, encodeO, encode.
    elimtype (exists b, (PositiveSet.mem x r)=b); eauto.
    intro b; destruct b; intro H; rewrite H; simpl;
      destruct y; intros H0 H1; try (rewrite switch_out); auto.
  Qed.


  Record assignDomain :=
    mk { pol: D.t ;
      renaming: PositiveSet.t
    }.

  Definition t:=assignDomain.

  Definition gamma (a:t) m := forall aux, D.gamma (pol a) (decodeIn (renaming a) aux m).


  Instance decodeIn_compat : Proper (PositiveSet.Equal ==>
    pointwise_relation PVar.t Logic.eq ==>
    pointwise_relation PVar.t Logic.eq ==>
    pointwise_relation PVar.t Logic.eq) decodeIn.
Proof.
    intros r1 r2 H1 aux1 aux2 H2 m1 m2 H3 x; subst.
    destruct x as [ p | p |]; simpl; try congruence;
        rewrite H1; case (PositiveSet.mem p r2); simpl; auto.
  Qed.

  Instance gamma_ext: Proper (Logic.eq ==> pointwise_relation PVar.t Logic.eq ==> iff) gamma.
Proof.
     eapply sat_compat_iff; unfold gamma.
     intros x y H m1 m2 H0 H1 aux. rewrite <- H. rewrite <- H0; auto.
  Qed.


  Definition top: t
    := {| pol := D.top ; renaming := PositiveSet.empty |}.

  Lemma top_correct: forall m, gamma top m.
    unfold gamma; simpl; auto with vpl.
  Qed.

  Definition bottom: t
    := {| pol := D.bottom ; renaming := PositiveSet.empty |}.

  Lemma bottom_correct m: gamma bottom m -> False.
    unfold gamma; simpl; intros.
    eapply D.bottom_correct.
    eapply (H m).
  Qed.
  Open Scope impure.
 
  Definition isBottom : t -> imp bool
    := fun p => D.isBottom (pol p).

  Lemma isBottom_correct : forall a, If isBottom a THEN forall m, gamma a m -> False.
Proof.
    unfold isBottom.
    VPLAsimplify.
    Grab Existential Variables.
    exact m.
  Qed.

  Definition assume (c:cond) (a: t) : imp t :=
  BIND res <- D.assume (map c (encodeE (renaming a))) (pol a) -;
  pure {| pol := res ;
          renaming := renaming a |}.

  Hint Unfold pointwise_relation.

  Lemma assume_correct (c:cond) (a:t): WHEN p <- assume c a THEN
    forall m, (sat c m) -> (gamma a m) -> gamma p m.
Proof.
    unfold gamma, assume; VPLAsimplify. simpl in * |- *.
    intros m H0 H1 aux; eapply H; auto.
    rewrite sat_map.
    erewrite (eval_pointwise_compat sat_mdo); eauto with vpl.
  Qed.
  Hint Resolve assume_correct: vpl.

  Definition assert (c:cond) (a: t) : imp bool := D.assert (map c (encodeE (renaming a))) (pol a).

  Lemma assert_correct (c:cond): forall (a:t), If assert c a THEN forall m, (gamma a m) -> (sat c m).
Proof.
    unfold gamma, assert. VPLAsimplify.
    intros m H0. generalize (H _ (H0 m)).
    rewrite sat_map.
    intros; erewrite (eval_pointwise_compat sat_mdo); eauto with vpl.
  Qed.
  Hint Resolve assert_correct: vpl.


  Definition project (a:t) (x:PVar.t) : imp t
    :=
     BIND res <- D.project (pol a) (encodeE (renaming a) x) -;
     pure {| pol := res ; renaming := (renaming a) |}.

  Lemma project_correct a x: WHEN p <- project a x THEN forall m v, gamma a m -> gamma p (Mem.assign x v m).
Proof.
    unfold project, gamma. VPLAsimplify. simpl in * |- *.
    intros m v H0 aux.
    eapply D.gamma_ext; [ eauto | idtac | idtac ].
    Focus 2.
    + eapply D.project_correct with (m:=decodeIn (renaming a) aux m) (v:=v);
      eauto.
    + intro x'; unfold Mem.assign at 2.
    case (PVar.eq_dec (encodeE (renaming a) x) x').
    - intro; subst. autorewrite with progvar vpl; auto.
    - intros; apply decodeIn_simplify; auto with vpl.
    intros; rewrite Mem.assign_out; auto.
    intro; subst x; intuition.
  Qed.



  Definition guassignAux x (c:cond) (a: t) : imp t :=
    let a:=trace DEBUG "guassign called" a in
    BIND tmp <- D.assume c (pol a) -;
    BIND aux <- D.project tmp (encodeE (renaming a) x) -;
    pure {| pol := aux ; renaming := switch (renaming a) x |}.

  Lemma guassignAux_correct x c a:
    let f:=(encodeE (renaming a)) in
    let c1:=(xmap c f (Mem.assign x (encodeO (renaming a) x) f)) in
    WHEN p <- guassignAux x c1 a THEN
        forall m v,
          xsat c m (Mem.assign x v m) ->
          gamma a m ->
            gamma p (Mem.assign x v m).
Proof.
    simpl; unfold guassignAux, trace; VPLAsimplify. simpl in * |- *. unfold gamma; intros m v Hxsat H1 aux.
    eapply D.gamma_ext; [ eauto | idtac | idtac ].
    Focus 2.
    + refine (H0 (decodeIn (renaming a) (Mem.assign (encodeO (renaming a) x) v aux) _) (aux (encodeE (renaming a) x)) _).
      eapply H; eauto.
    rewrite <- xsat_sat.
    rewrite xsat_xmap.
    erewrite (eval_pointwise_compat (xsat_old_mdo _)); eauto.
    erewrite (eval_pointwise_compat (xsat_new_mdo _)); eauto.
    - intros x'; simpl. autorewrite with vpl; auto.
    - intros x'. unfold Mem.assign at 2 3.
    case (PVar.eq_dec x x'); intros; autorewrite with progvar vpl; auto.
    + simpl; intro x'; unfold Mem.assign at 2.
    case (PVar.eq_dec (encodeE (renaming a) x) x').
    - intro; subst. autorewrite with vpl; auto.
    - intro H2. case (PVar.eq_dec x' (encodeO (renaming a) x)).
    * intros; subst; autorewrite with progvar vpl; auto.
    * intro H3; rewrite decode_sw_out; auto.
    apply decodeIn_simplify; auto with vpl.
    intros; rewrite Mem.assign_out; auto.
    intro; subst x; intuition.
    rewrite Mem.assign_out; auto.
  Qed.

  Definition guassign x (c:cond) (a: t) : imp t :=
    let f:=(encodeE (renaming a)) in
      let c1:=(xmap c f (Mem.assign x (encodeO (renaming a) x) f)) in
        guassignAux x c1 a.

  Local Hint Resolve guassignAux_correct: vpl.
  Opaque guassignAux.

  Lemma guassign_correct x c a:
    WHEN p <- guassign x c a THEN forall m v,
    xsat c m (Mem.assign x v m) ->
    gamma a m -> gamma p (Mem.assign x v m).
Proof.
    VPLAsimplify.
  Qed.

  Definition assign x te (a: t) : imp t :=
    let c:=(Atom Eq (Term.Var (encodeO (renaming a) x)) (Term.Old (Term.map te (encodeE (renaming a))))) in
      guassignAux x c a.

  Lemma assign_correct (x: PVar.t) (te: Term.t) (a:t): WHEN p <- assign x te a THEN
     forall m, gamma a m -> gamma p (Mem.assign x (Term.eval te m) m).
Proof.
    generalize (guassignAux_correct x (Atom Eq (Term.Var x) (Term.Old te)) a).
    simpl. VPLAsimplify.
    autorewrite with progvar in H.
    intros; eapply H; eauto with progvar.
  Qed.
  Hint Resolve guassign_correct assign_correct: vpl.


  Definition nop (x: PVar.t) a : imp t :=
    BIND res <- R.rename (encodeE (renaming a) x) (encodeO (renaming a) x) (pol a) -;
    pure {| pol := res ; renaming := switch (renaming a) x |}.
   
  Lemma nop_correct (x: PVar.t) (a:t):
    WHEN p <- nop x a THEN forall m, gamma a m -> gamma p m.
Proof.
    unfold nop, gamma; VPLAsimplify.
    intros; eapply R.rename_correct; eauto.
    autorewrite with vpl.
    eapply D.gamma_ext; [ eauto | idtac | eapply H with (aux:=Mem.assign (encodeO (renaming a) x) (m x) aux) ].
    intros x0.
    case (PVar.eq_dec (encodeE (renaming a) x) x0).
    - intros; subst; autorewrite with progvar vpl; auto.
    - intros. rewrite Mem.assign_out; auto.
      case (PVar.eq_dec (encodeO (renaming a) x) x0).
      + intros; subst; autorewrite with progvar vpl; auto.
      + intros. rewrite decode_sw_out; auto.
        intros; apply decodeIn_simplify; auto.
        intros; rewrite Mem.assign_out; auto.
  Qed.
  Local Hint Resolve nop_correct: vpl.

  Lemma nop_effect_1 (x: PVar.t) (a:t): WHEN p <- nop x a THEN PositiveSet.mem x (renaming p) = negb (PositiveSet.mem x (renaming a)).
Proof.
    unfold nop; xasimplify ltac:idtac.
    autorewrite with vpl.
    destruct (PositiveSet.mem x (renaming a)); simpl; intuition.
  Qed.

  Lemma nop_effect_2 (x y: PVar.t) (a:t): x <> y -> WHEN p <- nop x a THEN PositiveSet.mem y (renaming p) = (PositiveSet.mem y (renaming a)).
Proof.
    unfold nop; xasimplify ltac:idtac.
    intros; rewrite switch_out; intuition.
  Qed.

  Local Opaque nop.

  Definition switchAll (r:PositiveSet.t) (a:t) : imp t :=
    PositiveSet.fold (fun x0 k => bind k (nop x0))
                     r
                     (pure a).

  Lemma switchAll_correct r (a:t): WHEN p <- switchAll r a THEN forall m, gamma a m -> gamma p m.
Proof.
    unfold switchAll; rewrite PositiveSet.fold_spec.
    eapply wlp_forall; intro m.
    eapply wlp_forall; intro H.
    cut (WHEN p <- pure a THEN gamma p m).
    clear H.
    cut (forall x : PVar.t,
      PositiveSet.InL x (PositiveSet.elements r) ->
      PositiveSet.In x r).
    generalize (PositiveSet.elements_spec2w r).
    unfold PositiveSet.E.eq.
    generalize (PositiveSet.elements r).
    intros l H. generalize (pure a); clear a.
    induction H as [| a0 l H H0 IHl]; simpl.
    - auto.
    - intros. eapply IHl; eauto.
      VPLAsimplify.
    - intros; rewrite <- PositiveSet.elements_spec1; auto.
    - VPLAsimplify.
  Qed.

  Hint Rewrite SetoidList.InA_nil SetoidList.InA_cons: vplx.
  Hint Rewrite nop_effect_1: vplx.

  Lemma bool_eq_False b1 b2: (False <-> (b1=b2)) <-> b1 = negb b2.
Proof.
    case b1; case b2; simpl; intuition.
  Qed.

  Lemma negb_negb b : negb (negb b) = b.
Proof.
    case b; simpl; auto.
  Qed.

  Hint Rewrite bool_eq_False negb_negb: vplx.

  Lemma switchAll_effect r a x:
    WHEN p <- switchAll r a THEN
      (PositiveSet.In x r) <-> (PositiveSet.mem x (renaming p)) = negb (PositiveSet.mem x (renaming a)).
Proof.
    assert (WHEN p <- switchAll r a THEN
      PositiveSet.InL x (PositiveSet.elements r) <-> (PositiveSet.mem x (renaming p)) = negb (PositiveSet.mem x (renaming a))).
    unfold switchAll.
    rewrite PositiveSet.fold_spec.
    generalize (PositiveSet.elements_spec2w r).
    unfold PositiveSet.E.eq.
    generalize (PositiveSet.elements r).
    intros l H; generalize a; clear a.
    * induction H as [| x0 l H H0 IHl]; simpl; intro a.
    - VPLAsimplify. rewrite SetoidList.InA_nil, bool_eq_False, negb_negb. auto.
    - apply wlp_List_fold_left.
      VPLAsimplify.
      simpl in * |- *. intros H2; clear IHl.
      rewrite SetoidList.InA_cons.
      case (PVar.eq_dec x x0).
      + intro; subst.
        assert (X: (SetoidList.InA eq x0 l) <-> False).
        intuition.
        rewrite X in * |- *; clear X.
        rewrite bool_eq_False, negb_negb in H2.
        rewrite H2; clear H2; intuition.
        apply nop_effect_1; auto.
       + intros.
         rewrite H2; clear H2.
         generalize exta Hexta; clear exta Hexta H1 Hexta0.
         eapply wlp_monotone.
         eapply nop_effect_2; eauto.
         simpl. intros a1 H1 H2; rewrite H2; clear H2.
         intuition.
    * VPLAsimplify. simpl.
      intros a0; rewrite <- (PositiveSet.elements_spec1 r). auto.
  Qed.


  Lemma switchAll_effect_set r1 a:
       WHEN p <- (switchAll r1 a) THEN
         let r2:=(renaming a) in
         PositiveSet.Equal (renaming p) (PositiveSet.union (PositiveSet.diff r2 r1) (PositiveSet.diff r1 r2)).
Proof.
    unfold PositiveSet.Equal.
    apply wlp_forall. intros x.
    elimtype (exists r2, r2=(renaming a)); eauto.
    intros r2 H.
    eapply wlp_monotone.
    eapply switchAll_effect with (x:=x).
    simpl; intros p. generalize
      (PositiveSet.diff_spec r2 r1 x)
      (PositiveSet.diff_spec r1 r2 x)
      (PositiveSet.union_spec (PositiveSet.diff r2 r1) (PositiveSet.diff r1 r2) x).
    unfold PositiveSet.In; rewrite <- H; clear H.
    generalize (PositiveSet.mem x (renaming p)); intro b1.
    generalize (PositiveSet.mem x (PositiveSet.diff r2 r1)); intro b2.
    generalize (PositiveSet.mem x r2); intro b3.
    generalize (PositiveSet.mem x (PositiveSet.diff r1 r2)); intro b4.
    generalize (PositiveSet.mem x
      (PositiveSet.union (PositiveSet.diff r2 r1) (PositiveSet.diff r1 r2))); intro b5.
    generalize (PositiveSet.mem x r1); intro b6.
    generalize (PositiveSet.mem x r2); intro b7.
    destruct b1, b2, b3, b4, b5, b6; simpl; intuition.
  Qed.


  Lemma switchAll_prop1 r a:
      WHEN p <- switchAll (PositiveSet.diff (renaming a) r) a THEN
        PositiveSet.Equal (renaming p) (PositiveSet.inter (renaming a) r).
Proof.
    eapply wlp_monotone.
    eapply switchAll_effect_set.
    simpl.
    PositiveSetDecide.fsetdec.
  Qed.

  Lemma switchAll_prop2 r1 r2 a:
    WHEN p <- switchAll (PositiveSet.diff r2 r1) a THEN
      (PositiveSet.Equal (renaming a) (PositiveSet.inter r1 r2))
      -> (PositiveSet.Equal (renaming p) r2).
Proof.
    eapply wlp_monotone.
    eapply switchAll_effect_set.
    simpl.
    PositiveSetDecide.fsetdec.
  Qed.


  Definition isIncl (a1 a2:t): imp bool
    := let r1 := (PositiveSet.diff (renaming a1) (renaming a2)) in
       let r2 := (PositiveSet.diff (renaming a2) (renaming a1)) in
       BIND aux1 <- switchAll r1 a1 -;
       BIND aux2 <- switchAll r2 aux1 -;
        D.isIncl (pol aux2) (pol a2).

  Lemma isIncl_correct a1 a2: If isIncl a1 a2 THEN forall m, gamma a1 m -> gamma a2 m.
Proof.
    VPLAsimplify.
    intros m H0; assert (X: gamma exta0 m).
    - repeat (eapply switchAll_correct; eauto).
    - clear H0.
      unfold gamma.
      intros aux; generalize (X aux); clear X.
      cut (PositiveSet.Equal (renaming exta0) (renaming a2)).
      + intros X1 X2.
        rewrite <- X1; auto.
      + eapply switchAll_prop2; eauto.
        eapply switchAll_prop1; eauto.
  Qed.

  Definition join (a1 a2:t): imp t
    := let r1 := (PositiveSet.diff (renaming a1) (renaming a2)) in
        let r2 := (PositiveSet.diff (renaming a2) (renaming a1)) in
        BIND aux1 <- switchAll r1 a1 -;
        BIND aux2 <- switchAll r2 a2 -;
        BIND res <- D.join (pol aux1) (pol aux2) -;
        pure {| pol := res ; renaming := PositiveSet.inter (renaming a1) (renaming a2) |}.

  Lemma join_correct a1 a2: WHEN p <- join a1 a2 THEN forall m, gamma a1 m \/ gamma a2 m -> gamma p m.
Proof.
    unfold join; VPLAsimplify. simpl in * |- *.
    intros m H0 aux; simpl.
    case H0; clear H0; intro H0.
    * assert (H1: gamma exta m).
      eapply switchAll_correct; eauto.
      unfold gamma in H1.
      generalize (switchAll_prop1 (renaming a2) a1 _ Hexta).
      intro H2; rewrite <- H2; clear H2.
      eauto.
    * assert (H1: gamma exta0 m).
      eapply switchAll_correct; eauto.
      unfold gamma in H1.
      generalize (switchAll_prop1 (renaming a1) a2 _ Hexta0).
      intro X.
      eapply D.gamma_ext; [ eauto | idtac | eauto ].
      intros x; eapply decodeIn_compat; auto.
      rewrite X.
      PositiveSetDecide.fsetdec.
  Qed.


  Definition widen (a1 a2:t) : imp t :=
    let r1 := (PositiveSet.diff (renaming a1) (renaming a2)) in
    let r2 := (PositiveSet.diff (renaming a2) (renaming a1)) in
    BIND aux1 <- switchAll r1 a1 -;
    BIND aux2 <- switchAll r2 a2 -;
    BIND res <- D.widen (pol aux1) (pol aux2) -;
    pure {| pol := res ; renaming := PositiveSet.inter (renaming a1) (renaming a2) |}.

  Global Opaque assign join assume isIncl assert guassign project.
  Hint Resolve isIncl_correct top_correct join_correct bottom_correct project_correct
    assign_correct guassign_correct: vpl.


End CoreAssign.

Module Type CoreAssignSig (N: NumSig) (Cond: ASCondSig N) (D: AbstractDomain N Cond) (R: HasRename N D).

  Include CoreAssign N Cond D R.

End CoreAssignSig.


Module MakeAssign (N: NumSig) (Cond: ASCondSig N) (D: AbstractDomain N Cond) (R: HasRename N D) <: FullAbstractDomain N Cond
  := CoreAssign N Cond D R.

Module AssignLiftItv (N: NumSig) (Cond: ASCondSig N) (I: ItvSig N)
   (D: AbstractDomain N Cond) (R: HasRename N D) (DI: HasGetItv N Cond.Term I D)
   (CD: CoreAssignSig N Cond D R) <: HasGetItv N Cond.Term I CD.

  Import Cond DI.
  Import CD.

  Definition get_itv (te:Term.t) (a:t) := get_itv (Term.map te (encodeE (renaming a))) (pol a).

  Lemma get_itv_correct (te: Term.t) (a: t): WHEN i <- get_itv te a THEN
    forall m, gamma a m -> I.sat i (Term.eval te m).
Proof.
    unfold get_itv, gamma. VPLAsimplify. simpl.
 eliminate variable aux *) intros H m H0; generalize (H0 m); clear H0; intro H0.
    erewrite f_equal; eauto with vpl.
    erewrite Term.eval_map.
    apply (eval_pointwise_compat Term.eval_mdo); auto.
    intros x; autorewrite with vpl; auto.
  Qed.

End AssignLiftItv.

Module AssignSimplePrinting (N: NumSig) (Cond: ASCondSig N) (D: AbstractDomain N Cond) (R: HasRename N D) (DP: HasSimplePrinting N D)
   (Import CD: CoreAssignSig N Cond D R) <: HasSimplePrinting N CD.

  Definition pr (a:t) := DP.pr (pol a).

End AssignSimplePrinting.
Generated by coq2html