(*
 * Copyright (c) 2017-present,
 * Programming Research Laboratory (ROPAS), Seoul National University, Korea
 * This software is distributed under the term of the BSD-3 clause license.
 *)
(** * Abstract Domain.  *)

Set Implicit Arguments.

Require Import Morphisms.
Require Import vgtac VocabA Syn DLat DUnit DStr DSum DMap DProd DPow
        DItv UserInputType.
Require DMem.
Require Import DomBasic DomArrayBlk.

(** ** Value domain *)

Module Val <: LAT := Prod4 Itv PowLoc ArrayBlk PowProc.

Definition itv_of_val : Val.t -> Itv.t := Val.fst.

Lemma itv_of_val_mor : Proper (Val.eq ==> Itv.eq) itv_of_val.
Proof. unfold itv_of_val; intros v1 v2 Hv. by apply Val.fst_mor. Qed.

Definition pow_loc_of_val : Val.t -> PowLoc.t := Val.snd.

Lemma pow_loc_of_val_mor : Proper (Val.eq ==> PowLoc.eq) pow_loc_of_val.
Proof. unfold pow_loc_of_val; intros v1 v2 Hv. by apply Val.snd_mor. Qed.

Definition array_of_val : Val.t -> ArrayBlk.t := Val.thrd.

Lemma array_of_val_mor : Proper (Val.eq ==> ArrayBlk.eq) array_of_val.
Proof. unfold array_of_val; intros v1 v2 Hv. by apply Val.thrd_mor. Qed.

Definition pow_proc_of_val : Val.t -> PowProc.t := Val.frth.

Lemma pow_proc_of_val_mor : Proper (Val.eq ==> PowProc.eq) pow_proc_of_val.
Proof. unfold pow_proc_of_val; intros v1 v2 Hv. by apply Val.frth_mor. Qed.

Definition powProc_of_val := pow_proc_of_val.

Definition val_of_itv (x : Itv.t) : Val.t :=
  (x, PowLoc.bot, ArrayBlk.bot, PowProc.bot).

Lemma val_of_itv_mor : Proper (Itv.eq ==> Val.eq) val_of_itv.
Proof.
intros i1 i2 Hi.
split; [split; [split|] |]; s
; by auto using Itv.eq_refl, PowLoc.eq_refl, ArrayBlk.eq_refl, PowProc.eq_refl.
Qed.

Definition val_of_pow_loc (x : PowLoc.t) : Val.t :=
  (Itv.bot, x, ArrayBlk.bot, PowProc.bot).

Lemma val_of_pow_loc_mor : Proper (PowLoc.eq ==> Val.eq) val_of_pow_loc.
Proof.
intros i1 i2 Hi.
split; [split; [split|] |]; s
; by auto using Itv.eq_refl, PowLoc.eq_refl, ArrayBlk.eq_refl, PowProc.eq_refl.
Qed.

Definition val_of_array (x : ArrayBlk.t) : Val.t :=
  (Itv.bot, PowLoc.bot, x, PowProc.bot).

Lemma val_of_array_mor : Proper (ArrayBlk.eq ==> Val.eq) val_of_array.
Proof.
intros i1 i2 Hi.
split; [split; [split|] |]; s
; by auto using Itv.eq_refl, PowLoc.eq_refl, ArrayBlk.eq_refl, PowProc.eq_refl.
Qed.

Definition val_of_pow_proc (x : PowProc.t) : Val.t :=
  (Itv.bot, PowLoc.bot, ArrayBlk.bot, x).

Lemma val_of_pow_proc_mor : Proper (PowProc.eq ==> Val.eq) val_of_pow_proc.
Proof.
intros i1 i2 Hi.
split; [split; [split|] |]; s
; by auto using Itv.eq_refl, PowLoc.eq_refl, ArrayBlk.eq_refl, PowProc.eq_refl.
Qed.

Coercion val_of_itv : Itv.t >-> Val.t.
Coercion val_of_pow_loc : PowLoc.t >-> Val.t.
Coercion val_of_array : ArrayBlk.t >-> Val.t.
Coercion val_of_pow_proc : PowProc.t >-> Val.t.

Definition modify_itv (x : Val.t) (i : Itv.t) : Val.t :=
  (i, pow_loc_of_val x, array_of_val x, pow_proc_of_val x).

Lemma modify_itv_mor : Proper (Val.eq ==> Itv.eq ==> Val.eq) modify_itv.
Proof.
unfold modify_itv; intros [[[x1 y1] z1] a1] [[[x2 y2] z2] a2] [[[H1 H2] H3] H4] i1 i2 Hi.
split; [split; [split|]|]; assumption.
Qed.

Definition modify_pow_loc (x : Val.t) (l : PowLoc.t) : Val.t :=
  (itv_of_val x, l, array_of_val x, pow_proc_of_val x).

Lemma modify_pow_loc_mor : Proper (Val.eq ==> PowLoc.eq ==> Val.eq) modify_pow_loc.
Proof.
unfold modify_pow_loc; intros [[[x1 y1] z1] a1] [[[x2 y2] z2] a2] [[[H1 H2] H3] H4] i1 i2 Hi.
split; [split; [split|]|]; assumption.
Qed.

Definition modify_array (x : Val.t) (a : ArrayBlk.t) : Val.t :=
  (itv_of_val x, pow_loc_of_val x, a, pow_proc_of_val x).

Lemma modify_array_mor : Proper (Val.eq ==> ArrayBlk.eq ==> Val.eq) modify_array.
Proof.
unfold modify_array; intros [[[x1 y1] z1] a1] [[[x2 y2] z2] a2] [[[H1 H2] H3] H4] i1 i2 Hi.
split; [split; [split|]|]; assumption.
Qed.

Definition modify_pow_proc (x : Val.t) (p : PowProc.t) : Val.t :=
  (itv_of_val x, pow_loc_of_val x, array_of_val x, p).

Lemma modify_pow_proc_mor : Proper (Val.eq ==> PowProc.eq ==> Val.eq) modify_pow_proc.
Proof.
unfold modify_pow_proc; intros [[[x1 y1] z1] a1] [[[x2 y2] z2] a2] [[[H1 H2] H3] H4] i1 i2 Hi.
split; [split; [split|]|]; assumption.
Qed.