Module AbTyps

Require Import ToString Coqlib Utf8 Maps ShareTree Sets Util.
Require Import AdomLib.
Require Import IdealExpr AbIdealEnv.

Module Dom := WPFun T.

Definition t := Dom.t ideal_num_ty.

Instance t_gamma: gamma_op t (var -> ideal_num) := Dom.gamma_tree _.

Instance eq_ty : EqDec ideal_num_ty.

Fixpoint traverse_expr (ab:t) (e:iexpr) : t+⊥ :=
  match e with
  | IEvar ty v =>
    match T.get v ab with
    | None => NotBot (T.set v ty ab)
    | Some ty' => if eq_ty ty ty' then NotBot ab else Bot
    end
  | IEconst _ | IEZitv _ => NotBot ab
  | IEunop _ e => traverse_expr ab e
  | IEbinop _ e1 e2 =>
    do ab <- traverse_expr ab e1;
    traverse_expr ab e2
  end.

Lemma traverse_expr_correct:
  ∀ e ab ρ n,
    ρ ∈ γ ab ->
    eval_iexpr ρ e n ->
    ρ ∈ γ (traverse_expr ab e).

Program Definition widen (a:t+⊥) (b:(t*query_chan)+⊥) (c:query_chan+⊥)
  : t+⊥ * (t*messages_chan)+⊥ :=
  match a, b return _ with
  | Bot, Bot => (Bot, Bot)
  | Bot, NotBot (r, _) | NotBot r, Bot => (NotBot r, NotBot (r, nil))
  | NotBot (a), NotBot (b, _) =>
    let r := Dom.joinwiden (flat_join_op eq_dec) _ (a:Dom.t ideal_num_ty) b in
    (NotBot r, NotBot (r, nil))
  end.

Definition assign x e (ab:t*query_chan) (c:query_chan) :=
  do ab <- traverse_expr (fst ab) e;
  ret (Dom.set ab x (Just (iexpr_ty e)), nil:messages_chan).

Definition forget x (ab:t*query_chan) (c:query_chan) :=
  NotBot (Dom.set (fst ab) x All, nil:messages_chan).

Definition process_msg m (ab:t*query_chan) :=
  match m with
  | Fact_msg e _ =>
    do ab <- traverse_expr (fst ab) e;
    ret (ab, m::nil)
  | _ => ret (fst ab, m::nil)
  end.

Program Instance abVarExpEq_env : ab_ideal_env t (t+⊥) :=
  {| id_leb a b := Dom.leb_tree (flat_leb_op eq_dec) _ (fst a) b;
     id_top c := NotBot (Dom.top_tree _, nil);
     id_join a b c := NotBot (Dom.joinwiden (flat_join_op eq_dec) _ (fst a) (fst b), nil);
     id_init_iter := id;
     id_widen := widen;
     assign := assign;
     forget := forget;
     enrich_query_chan ab c :=
       {| get_var_ty := fun x => Dom.get x ab;
          get_itv := c.(get_itv);
          get_congr := c.(get_congr);
          get_eq_expr := c.(get_eq_expr);
          linearize_expr := c.(linearize_expr) |};
     process_msg := process_msg
  |}.

Instance t_tostring : ToString t := fun _ => ""%string.