Module AbIdealEnv

Require Import Coqlib Utf8 Util TreeAl Hash FastArith.
Require Import ShareTree.
Require Import AdomLib.
Require Import ZCongruences_defs.
Require Import IdealExpr IdealIntervals.
Require Import LinearQuery.

Set Implicit Arguments.
Unset Elimination Schemes.

Record query_chan : Type :=
  { get_var_ty: var -> ideal_num_ty+⊤;
    get_itv: iexpr -> iitv+⊤+⊥;
    get_congr: iexpr -> zcongr+⊥;
    get_eq_expr: var -> option ite_iexpr;
    linearize_expr: iexpr -> option T_linear_expr }.

Record query_chan_gamma (chan:query_chan) (ρ:var->ideal_num) :=
  { get_var_ty_correct: ∀ v, ρ v ∈ γ (chan.(get_var_ty) v);
    get_itv_correct:
      ∀ e, eval_iexpr ρ e ⊆ γ (chan.(get_itv) e);
    get_congr_correct:
      ∀ e z, (eval_iexpr ρ e (INz z)) -> (z:Z) ∈ γ (chan.(get_congr) e);
    get_eq_expr_correct:
      ∀ x e, chan.(get_eq_expr) x = Some e ->
             eval_ite_iexpr ρ e (ρ x);
    linearize_expr_correct:
      ∀ e le, chan.(linearize_expr) e = Some le ->
      ∀ x, eval_iexpr ρ e x ->
           ∃ y, r_of_inum x = Some y /\ eval_T_linear_expr ρ le y
  }.
Instance query_chan_gamma' : gamma_op query_chan (var -> ideal_num)
  := query_chan_gamma.

Inductive message : Type :=
| Fact_msg : iexpr -> bool -> message
| Known_value_msg : var -> ideal_num -> message
| Itv_msg : var -> iitv -> message
| Linear_zero_msg : T_linear_expr -> message
| Congr_msg : var -> zcongr -> message
| Broadcasted_msg : message -> message.

Instance message_gamma : gamma_op message (var->ideal_num) :=
  fix message_gamma m ρ :=
    match m with
      | Fact_msg c b =>
        (INz (if b then F1 else F0)) ∈ eval_iexpr ρ c
      | Known_value_msg x v => ρ x = v
      | Itv_msg x i => ρ x ∈ γ i
      | Linear_zero_msg le => eval_T_linear_expr ρ le 0
      | Congr_msg x zc =>
        match ρ x with
          | INz v => (v:Z) ∈ γ zc
          | _ => False
        end
      | Broadcasted_msg m => message_gamma m ρ
    end.

Definition messages_chan := list message.
Instance messages_chan_gamma : gamma_op messages_chan (var -> ideal_num) :=
  fun ml ρ => List.Forall (fun m => ρ ∈ γ m) ml.

Class ab_ideal_env_nochan (t iter_t:Type) : Type := {
  idnc_top:> top_op (t+⊥);
  idnc_leb:> leb_op t;
  idnc_join:> join_op t (t+⊥);
  idnc_widen:> widen_op iter_t (t+⊥);

  idnc_assign: var -> iexpr -> t -> t+⊥;
  idnc_forget: var -> t -> t+⊥;
  idnc_assume: iexpr -> bool -> t -> t+⊥;
  idnc_get_query_chan: t -> query_chan;

  idnc_gamma:> gamma_op t (var -> ideal_num);
  idnc_gamma_iter:> gamma_op iter_t (var -> ideal_num);
  idnc_top_correct:> top_op_correct (t+⊥) (var -> ideal_num);
  idnc_leb_correct:> leb_op_correct t (var -> ideal_num);
  idnc_join_correct:> join_op_correct t (t+⊥) (var -> ideal_num);
  idnc_widen_correct:> widen_op_correct iter_t (t+⊥) (var -> ideal_num);
  idnc_assign_correct: ∀ x e ρ n ab,
    ρ ∈ γ ab ->
    n ∈ eval_iexpr ρ e ->
    (ρ+[x => n]) ∈ γ (idnc_assign x e ab);
  idnc_forget_correct: ∀ x ρ n ab,
    ρ ∈ γ ab ->
    (ρ+[x => n]) ∈ γ (idnc_forget x ab);
  idnc_assume_correct: ∀ c (b:bool) ρ ab,
    ρ ∈ γ ab ->
    (INz (if b then F1 else F0)) ∈ eval_iexpr ρ c ->
    ρ ∈ γ (idnc_assume c b ab);
  idnc_get_query_chan_correct: ∀ ab ρ,
    ρ ∈ γ ab ->
    ρ ∈ γ (idnc_get_query_chan ab)
}.

Class ab_ideal_env (t iter_t:Type) : Type := {
  id_top: query_chan -> (t * messages_chan)+⊥;
  id_leb: t * query_chan -> t -> bool;
  id_join: t * query_chan -> t * query_chan -> query_chan -> (t * messages_chan)+⊥;
  id_init_iter: t+⊥ -> iter_t;
  id_widen: iter_t -> (t * query_chan)+⊥ -> query_chan+⊥ -> iter_t * (t * messages_chan)+⊥;

  assign: var -> iexpr -> t * query_chan -> query_chan -> (t * messages_chan)+⊥;
  forget: var -> t * query_chan -> query_chan -> (t * messages_chan)+⊥;

  process_msg: message -> t * query_chan -> (t * messages_chan)+⊥;
  enrich_query_chan: t -> query_chan -> query_chan;

  id_gamma:> gamma_op t (var -> ideal_num);
  id_gamma_iter:> gamma_op iter_t (var -> ideal_num);
  id_top_correct: ∀ chan ρ, ρ ∈ γ chan -> ρ ∈ γ (id_top chan);
  id_leb_correct: ∀ ab1 ab2 ρ,
    id_leb ab1 ab2 = true ->
    ρ ∈ γ ab1 ->
    ρ ∈ γ ab2;
  id_join_correct: ∀ ab1 ab2 chan ρ,
    ρ ∈ γ ab1 \/ ρ ∈ γ ab2 -> ρ ∈ γ chan ->
    ρ ∈ γ (id_join ab1 ab2 chan);
  id_init_iter_sound: ∀ ab, γ ab ⊆ γ (id_init_iter ab);
  id_widen_incr: ∀ ab1 ab2 chan ρ,
    ρ ∈ γ ab1 -> ρ ∈ γ chan ->
    ρ ∈ γ (id_widen ab1 ab2 chan);

  assign_correct: ∀ x e ρ n ab chan,
    ρ ∈ γ ab -> (ρ+[x => n]) ∈ γ chan ->
    n ∈ eval_iexpr ρ e ->
    (ρ+[x => n]) ∈ γ (assign x e ab chan);
  forget_correct: ∀ x ρ n ab chan,
    ρ ∈ γ ab -> (ρ+[x => n]) ∈ γ chan ->
    (ρ+[x => n]) ∈ γ (forget x ab chan);

  process_msg_correct: ∀ m ρ ab,
    ρ ∈ γ ab -> ρ ∈ γ m ->
    ρ ∈ γ (process_msg m ab);
  enrich_query_chan_correct: ∀ ab chan ρ,
    ρ ∈ γ ab -> ρ ∈ γ chan ->
    ρ ∈ γ (enrich_query_chan ab chan)
}.