Module AbIdealEnvProduct

Require Import AdomLib Util Coqlib.
Require Import AbIdealEnv IdealExpr.

Fixpoint process_msg_list {B iter_B:Type} `{ab_ideal_env B iter_B}
         (mchan:messages_chan) (ab:B * query_chan) (accu_mchan:messages_chan) :=
  match mchan with
    | nil => NotBot (fst ab, accu_mchan)
    | cons m mchanq =>
      do (ab', mchan') <- process_msg m ab;
      process_msg_list mchanq (ab', snd ab) (mchan'++accu_mchan)%list
  end.

Lemma process_msg_list_correct {A iter_A:Type} `{ab_ideal_env A iter_A}:
  forall (mchan:messages_chan) (ab:A * query_chan) (accu_mchan:messages_chan) ρ,
    ρ ∈ γ mchan -> ρ ∈ γ ab -> ρ ∈ γ accu_mchan ->
    ρ ∈ γ (process_msg_list mchan ab accu_mchan).

Instance ab_ideal_env_product {A iter_A B iter_B:Type}
         `(ab_ideal_env A iter_A)
         `(ab_ideal_env B iter_B) : ab_ideal_env (A*B) (iter_A*iter_B)%type :=
  {| id_init_iter a :=
       (id_init_iter (fmap fst a),
        id_init_iter (fmap snd a))
   ; id_top qchan :=
       do (a, mchana) <- id_top qchan;
       let qchana := enrich_query_chan a qchan in
       do (b, mchanb) <- id_top qchana;
       do (b, mchan) <- process_msg_list mchana (b, qchana) mchanb;
       ret ((a, b), mchan)
   ; id_leb x y :=
       let '((xa, xb), chan) := x in
       let '(ya, yb) := y in
       (id_leb (xa, chan) ya && id_leb (xb, chan) yb)%bool
   ; id_join x y qchan :=
       let '((xa, xb), xqchan) := x in
       let '((ya, yb), yqchan) := y in
       do (a, mchana) <- id_join (xa, xqchan) (ya, yqchan) qchan;
       let qchana := enrich_query_chan a qchan in
       do (b, mchanb) <- id_join (xb, xqchan) (yb, yqchan) qchana;
       do (b, mchan) <- process_msg_list mchana (b, qchana) mchanb;
       ret ((a, b), mchan)
   ; id_widen x y qchan :=
       let '(xa, xb) := x in
       let ayqchan := do (yab, yqchan) <- y; ret (fst yab, yqchan) in
       let '(ita, wa) := id_widen xa ayqchan qchan in
       let qchana :=
         do qchan <- qchan;
         do (a, _) <- wa;
         ret (enrich_query_chan a qchan)
       in
       let byqchan := do (yab, yqchan) <- y; ret (snd yab, yqchan) in
       let '(itb, wb) := id_widen xb byqchan qchana in
       ((ita, itb),
         do (a, mchana) <- wa;
         do (b, mchanb) <- wb;
         do qchana <- qchana;
         do (b, mchan) <- process_msg_list mchana (b, qchana) mchanb;
         ret ((a, b), mchan))
   ; assign v e ab qchan :=
       let '((a, b), abqchan) := ab in
       do (a, mchana) <- assign v e (a, abqchan) qchan;
       let qchana := enrich_query_chan a qchan in
       do (b, mchanb) <- assign v e (b, abqchan) qchana;
       do (b, mchan) <- process_msg_list mchana (b, qchana) mchanb;
       ret ((a, b), mchan)
   ; forget v ab qchan :=
       let '((a, b), abqchan) := ab in
       do (a, mchana) <- forget v (a, abqchan) qchan;
       let qchana := enrich_query_chan a qchan in
       do (b, mchanb) <- forget v (b, abqchan) qchana;
       do (b, mchan) <- process_msg_list mchana (b, qchana) mchanb;
       ret ((a, b), mchan)
   ; enrich_query_chan ab qchan :=
       let '(a, b) := ab in
       let qchan := enrich_query_chan a qchan in
       enrich_query_chan b qchan
   ; process_msg msg ab :=
       let '((a, b), abqchan) := ab in
       do (a, mchana) <- process_msg msg (a, abqchan);
       let qchana := enrich_query_chan a abqchan in
       do (b, mchan) <- process_msg_list mchana (b, qchana) nil;
       ret ((a, b), mchan)
  |}.

Section Reduce.

Context (A iter_A:Type) `{ab_ideal_env A iter_A}.

Definition reduced_product := { ab : A * query_chan | γ (fst ab) ⊆ γ (snd ab) }.

Instance reduced_gamma : gamma_op reduced_product (var -> ideal_num) :=
  fun ab => γ (proj1_sig ab).

Fixpoint filter_broadcasted (l:messages_chan) : messages_chan :=
  match l with
    | nil => nil
    | Broadcasted_msg m :: l => m :: filter_broadcasted l
    | _ :: l => filter_broadcasted l
  end.

Instance qchan_top : top_op query_chan :=
  let _ := tt in
  {| get_var_ty := fun v => ⊤;
     get_itv := fun e => ⊤;
     get_congr := fun e => ⊤;
     get_eq_expr := fun _ => None;
     linearize_expr := fun e => None |}.

Instance qchan_top_correct : top_op_correct query_chan (var -> ideal_num).

Program Definition reduce (ab:(A*messages_chan)+⊥): reduced_product+⊥ :=
  do ab <- ab;
  let '(ab, mchanab) := ab return _ in
  let c := enrich_query_chan ab top in
  do (ab, _) <- process_msg_list (filter_broadcasted mchanab) (ab, c) nil;
  let qchan := enrich_query_chan ab top in
  ret ((ab, qchan):reduced_product).

Lemma reduce_correct:
  forall (ab:(A*messages_chan)+⊥) (ρ:var->ideal_num), ρ ∈ γ ab -> ρ ∈ γ (reduce ab).

Program Instance ab_ideal_env_reduce: ab_ideal_env_nochan reduced_product iter_A :=
  {| idnc_top := reduce (id_top top)
   ; idnc_leb x y := id_leb x (fst y)
   ; idnc_join x y := reduce (id_join x y top)
   ; idnc_widen := {|
       init_iter x := id_init_iter (fmap (fst ∘ (@proj1_sig _ _)) x);
       widen x y :=
         let y := do y <- y; ret (proj1_sig y) in
         let '(it, w) := id_widen x y top return _ in
         (it, reduce w) |}
   ; idnc_assign v e ab := reduce (assign v e ab top)
   ; idnc_forget v ab := reduce (forget v ab top)
   ; idnc_assume c b ab := reduce (process_msg (Fact_msg c b) ab)
   ; idnc_get_query_chan ab := snd ab
  |}.

Program Instance reduced_ToString {T:ToString.ToString A} : ToString.ToString reduced_product :=
  fun x => T (fst x).

End Reduce.

Existing Instances reduced_ToString ab_ideal_env_reduce ab_ideal_env_product.