Lvc.Isa.Ops

Require Import Util EqDec DecSolve Val CSet Map Envs Option Get MapDefined SetOperations.
Require Import MoreList Option OptionR OptionMap ReplaceIf Filter.

Set Implicit Arguments.

Operations


Inductive op :=
  Con : val op
| Var : var op
| UnOp : unop op op
| BinOp : binop op op op.

Inductive isVar : op Prop :=
  IisVar v : isVar (Var v).

Instance isVar_dec e : Computable (isVar e).
Proof.
  destruct e; try dec_solve.
Defined.


Notation "'IsVar'" := (fun eB[isVar e]) (at level 0).
Notation "'NotVar'" := (fun eB[¬ isVar e]) (at level 0).

Definition getVar (e:op) :=
  match e with
  | Var yy
  | _default_var
  end.

Instance inst_eq_dec_op : EqDec op eq.
Proof.
  hnf; intros. change ({x = y} + {x y}).
  decide equality.
  - eapply inst_eq_dec_val.
  - eapply var_dec.
  - eapply inst_eq_dec_unop.
  - eapply inst_eq_dec_binop.
Defined.


Fixpoint op_eval (E:onv val) (e:op) : option val :=
  match e with
  | Con vSome v
  | Var xE x
  | UnOp o emdo v op_eval E e;
                 unop_eval o v
  | BinOp o mdo op_eval E ;
                      mdo op_eval E ;
                      binop_eval o
  end.

Inductive live_op_sound : op set var Prop :=
| ConLiveSound v lv : live_op_sound (Con v) lv
| VarLiveSound x lv : x lv live_op_sound (Var x) lv
| UnopLiveSound o e lv :
    live_op_sound e lv
     live_op_sound (UnOp o e) lv
| binopLiveSound o lv :
    live_op_sound lv
    live_op_sound lv
    live_op_sound (BinOp o ) lv.

Instance live_op_sound_Subset e
  : Proper (Subset impl) (live_op_sound e).
Proof.
  unfold Proper, respectful, impl; intros.
  general induction e; invt live_op_sound; eauto using live_op_sound.
Qed.


Instance live_op_sound_Equal e
  : Proper (Equal iff) (live_op_sound e).
Proof.
  unfold Proper, respectful, impl; split; intros.
  - eapply subset_equal in H. rewrite H in ; eauto.
  - symmetry in H. eapply subset_equal in H.
    rewrite H; eauto.
Qed.


Instance live_op_sound_dec e lv
  : Computable (live_op_sound e lv).
Proof.
  induction e as [c|v| |].
  - dec_solve.
  - decide (v lv); try dec_solve.
  - edestruct IHe; dec_solve.
  - edestruct , ; dec_solve.
Defined.


Lemma live_op_sound_incl
  : e lv lv', live_op_sound e lv' lv' lv live_op_sound e lv.
Proof.
  intros; general induction H; econstructor; eauto.
Qed.


Fixpoint freeVars (e:op) : set var :=
  match e with
  | Con _
  | Var v{v}
  | UnOp o efreeVars e
  | BinOp o freeVars freeVars
  end.

Lemma live_freeVars
  : e, live_op_sound e (freeVars e).
Proof.
  intros. general induction e; simpl; econstructor; eauto using live_op_sound_incl with cset.
Qed.


Lemma freeVars_live e lv
  : live_op_sound e lv freeVars e lv.
Proof.
  intros. general induction H; simpl; cset_tac; intuition.
Qed.


Lemma op_eval_live
  : e lv E E', live_op_sound e lv agree_on eq lv E E'
                 op_eval E e = op_eval E' e.
Proof.
  intros. general induction e; inv H; simpl; eauto.
  - erewrite IHe; eauto.
  - erewrite , ; eauto.
Qed.


Global Instance eval_op_ext
  : Proper (@feq _ _ eq eq eq) op_eval.
Proof.
  unfold Proper, respectful; intros; subst.
  general induction ; simpl; eauto.
  - erewrite ; eauto.
  - erewrite IHy0_1, IHy0_2; eauto.
Qed.


Lemma get_live_op_sound Y D n y
  : list_union (freeVars Y) D
     get Y n y
     live_op_sound y D.
Proof.
  intros. eapply live_op_sound_incl; [eapply live_freeVars |].
  rewrite H. eauto using get_list_union_map with cset.
Qed.


Definition var_to_op : x:var, op := Var.
Lemma var_to_op_correct : M x,
    op_eval M (var_to_op x) = M x.
Proof.
  reflexivity.
Qed.


Fixpoint rename_op (ϱ:env var) (s:op) : op :=
  match s with
  | Con vCon v
  | Var vVar (ϱ v)
  | UnOp o eUnOp o (rename_op ϱ e)
  | BinOp o BinOp o (rename_op ϱ ) (rename_op ϱ )
  end.

Lemma rename_op_comp e ϱ ϱ'
  : rename_op ϱ (rename_op ϱ' e) = rename_op (ϱ' ϱ) e.
Proof.
  unfold comp. general induction e; simpl; eauto.
  - f_equal; eauto.
  - f_equal; eauto.
Qed.


Lemma rename_op_ext
  : e (ϱ ϱ':env var), feq (R:=eq) ϱ ϱ' rename_op ϱ e = rename_op ϱ' e.
Proof.
  intros. general induction e; simpl; f_equal; eauto.
Qed.


Lemma rename_op_agree ϱ ϱ' e
  : agree_on eq (freeVars e) ϱ ϱ'
     rename_op ϱ e = rename_op ϱ' e.
Proof.
  intros; general induction e; simpl in *; f_equal;
    eauto 30 using agree_on_incl, incl_left, incl_right.
Qed.


Lemma rename_op_freeVars
  : e ϱ `{Proper _ (_eq _eq) ϱ},
    freeVars (rename_op ϱ e) lookup_set ϱ (freeVars e).
Proof.
  intros. general induction e; simpl; eauto using lookup_set_single_fact,
                                      lookup_set_union_incl, incl_union_lr; eauto.
Qed.


Lemma live_op_rename_sound e lv (ϱ:env var)
  : live_op_sound e lv
     live_op_sound (rename_op ϱ e) (lookup_set ϱ lv).
Proof.
  intros. general induction H; simpl; eauto using live_op_sound with cset.
Qed.


Fixpoint subst_op (ϱ:env op) (s:op) : op :=
  match s with
  | Con vCon v
  | Var v ⇒ (ϱ v)
  | UnOp o eUnOp o (subst_op ϱ e)
  | BinOp o BinOp o (subst_op ϱ ) (subst_op ϱ )
  end.

Lemma subst_op_comp e ϱ ϱ'
  : subst_op ϱ (subst_op ϱ' e) = subst_op (fun xsubst_op ϱ (ϱ' x)) e.
Proof.
  general induction e; simpl; eauto.
  - f_equal; eauto.
  - f_equal; eauto.
Qed.


Lemma subst_op_ext
  : e (ϱ ϱ':env op), feq (R:=eq) ϱ ϱ' subst_op ϱ e = subst_op ϱ' e.
Proof.
  intros. general induction e; simpl; eauto.
  - f_equal; eauto.
  - f_equal; eauto.
Qed.


Inductive alpha_op : env var env var op op Prop :=
| AlphaCon ϱ ϱ' v : alpha_op ϱ ϱ' (Con v) (Con v)
| AlphaVar ϱ ϱ' x y : ϱ x = y ϱ' y = x alpha_op ϱ ϱ' (Var x) (Var y)
| AlphaUnOp ϱ ϱ' o e e' :
    alpha_op ϱ ϱ' e e'
     alpha_op ϱ ϱ' (UnOp o e) (UnOp o e')
| AlphaBinOp ϱ ϱ' o :
    alpha_op ϱ ϱ'
    alpha_op ϱ ϱ'
    alpha_op ϱ ϱ' (BinOp o ) (BinOp o ).

Lemma alpha_op_rename_injective
  : e ϱ ϱ',
    inverse_on (freeVars e) ϱ ϱ'
     alpha_op ϱ ϱ' e (rename_op ϱ e).
Proof.
  intros. induction e; simpl; eauto using alpha_op.
  econstructor; eauto. eapply H; eauto. simpl; cset_tac; eauto.
  simpl in ×. econstructor.
  eapply . eapply inverse_on_incl; eauto. cset_tac; intuition.
  eapply . eapply inverse_on_incl; eauto. cset_tac; intuition.
Qed.


Lemma alpha_op_refl : e, alpha_op id id e e.
Proof.
  intros; induction e; eauto using alpha_op.
Qed.


Lemma alpha_op_sym : ϱ ϱ' e e', alpha_op ϱ ϱ' e e' alpha_op ϱ' ϱ e' e.
Proof.
  intros. general induction H; eauto using alpha_op.
Qed.


Lemma alpha_op_trans
  : ϱ1 ϱ1' ϱ2 ϱ2' s s' s'',
    alpha_op ϱ1 ϱ1' s s'
     alpha_op ϱ2 ϱ2' s' s''
     alpha_op (ϱ1 ϱ2) (ϱ2' ϱ1') s s''.
Proof.
  intros. general induction H.
  + inversion . subst ϱ0 s''. econstructor.
  + inversion . subst x ϱ0 s''. econstructor; unfold comp; congruence.
  + inversion . subst. econstructor; eauto.
  + inversion . subst. econstructor; eauto.
Qed.


Lemma alpha_op_inverse_on
  : ϱ ϱ' s t, alpha_op ϱ ϱ' s t inverse_on (freeVars s) ϱ ϱ'.
Proof.
  intros. general induction H.
  + isabsurd.
  + simpl. hnf; intros.
    eapply In_single in .
    rewrite at 1. rewrite H. eapply .
  + simpl; eauto.
  + simpl. eapply inverse_on_union; eauto.
Qed.


Lemma alpha_op_agree_on_morph
  : f g ϱ ϱ' s t,
    alpha_op ϱ ϱ' s t
     agree_on _eq (lookup_set ϱ (freeVars s)) g ϱ'
     agree_on _eq (freeVars s) f ϱ
     alpha_op f g s t.
Proof.
  intros. general induction H; simpl in *;
            eauto 20 using alpha_op, agree_on_incl, lookup_set_union_incl with cset.
  - econstructor.
    + rewrite ; eauto.
    + eapply . lset_tac.
Qed.


Lemma op_rename_renamedApart_all_alpha e e' ϱ ϱ'
  : alpha_op ϱ ϱ' e e'
     rename_op ϱ e = e'.
Proof.
  intros. general induction H; simpl; f_equal; eauto.
Qed.


Lemma alpha_op_morph
  : (ϱ1 ϱ1' ϱ2 ϱ2':env var) e e',
    @feq _ _ eq ϱ1 ϱ1'
     @feq _ _ eq ϱ2 ϱ2'
     alpha_op ϱ1 ϱ2 e e'
     alpha_op ϱ1' ϱ2' e e'.
Proof.
  intros. general induction ; eauto using alpha_op.
  econstructor.
  + rewrite ; eauto.
  + rewrite ; eauto.
Qed.


Inductive opLt : op op Prop :=
| OpLtCon c c'
  : _lt c c'
     opLt (Con c) (Con c')
| OpLtConVar c v
  : opLt (Con c) (Var v)
| OpLtConUnOp c o e
  : opLt (Con c) (UnOp o e)
| OpLtConBinop c o
  : opLt (Con c) (BinOp o )
| OpLtVar v v'
  : _lt v v'
     opLt (Var v) (Var v')
| OpLtVarUnOp v o e
  : opLt (Var v) (UnOp o e)
| OpLtVarBinop v o
  : opLt (Var v) (BinOp o )
| OpLtUnOpBinOp o e o'
  : opLt (UnOp o e) (BinOp o' )
| OpLtUnOp1 o o' e e'
  : _lt o o'
     opLt (UnOp o e) (UnOp o' e')
| OpLtUnOp2 o e e'
  : opLt e e'
     opLt (UnOp o e) (UnOp o e')
| OpLtBinOp1 o o'
  : _lt o o'
     opLt (BinOp o ) (BinOp o' )
| OpLtBinOp2 o
  : opLt
     opLt (BinOp o ) (BinOp o )
| OpLtBinOp3 o
  : opLt
     opLt (BinOp o ) (BinOp o ).

Lemma _lt_antirefl X `{OrderedType X} x
  : _lt x x False.
Proof.
  eapply lt_antirefl.
Qed.


Instance opLt_irr : Irreflexive opLt.
hnf; intros; unfold complement.
- induction x; inversion 1; subst; eauto.
Qed.

Instance opLt_trans : Transitive opLt.
hnf; intros.
general induction H; invt opLt; eauto using opLt.
- econstructor. eapply StrictOrder_Transitive. eapply H. eapply .
- econstructor. eapply StrictOrder_Transitive. eapply H. eapply .
- econstructor; eauto. eapply StrictOrder_Transitive. eapply H. eapply .
- econstructor; eauto. eapply StrictOrder_Transitive. eapply H. eapply .
Qed.

Notation "'Compare' x 'next' y" :=
  (match x with
   | Eqy
   | zz
   end) (at level 100).

Fixpoint op_cmp (e e':op) :=
  match e, e' with
  | Con c, Con c'_cmp c c'
  | Con _, _Lt
  | Var v, Var v'_cmp v v'
  | Var v, UnOp _ _Lt
  | Var v, BinOp _ _ _Lt
  | UnOp _ _, BinOp _ _ _Lt
  | UnOp o e, UnOp o' e'
    Compare _cmp o o' next
            Compare op_cmp e e' next Eq
  | BinOp o , BinOp o'
    Compare _cmp o o' next
            Compare op_cmp next
            Compare op_cmp next Eq
  | _, _Gt
  end.

Instance StrictOrder_opLt : OrderedType.StrictOrder opLt eq.
econstructor.
eapply opLt_trans.
intros. intro. eapply opLt_irr. rewrite in H.
eapply H.
Qed.

Instance OrderedType_op : OrderedType op :=
  { _eq := eq;
    _lt := opLt;
    _cmp := op_cmp}.
Proof.
  intros. revert y.
  induction x as [|v| |]; destruct y as [|v'| |];
    simpl; try now (econstructor; eauto using opLt).
- pose proof (_compare_spec v ).
  inv H.
  + econstructor. eauto using opLt.
  + econstructor. f_equal. eauto.
  + econstructor; eauto using opLt.
- pose proof (_compare_spec v v').
  inv H; (econstructor; eauto using opLt); f_equal; eauto.
- pose proof (_compare_spec u ).
  specialize (IHx y).
  inv H; try now (econstructor; eauto using opLt).
  eapply unop_eq_eq in ; subst.
  inv IHx; try now (econstructor; eauto using opLt).
- pose proof (_compare_spec b ).
  specialize ( ). specialize ( ).
  inv H; try now (econstructor; eauto using opLt).
  eapply binop_eq_eq in .
  inv .
  inv ; try now (econstructor; eauto using opLt).
  inv ; try now (econstructor; eauto using opLt).
Defined.


Lemma freeVars_renameOp ϱ e
  : freeVars (rename_op ϱ e) [=] lookup_set ϱ (freeVars e).
Proof.
  general induction e; simpl; try rewrite lookup_set_union; eauto.
  - rewrite , ; reflexivity.
Qed.


Definition op2bool (e:op) : option bool :=
  mdo r op_eval (fun _None) e; Some (val2bool r).

Lemma op_eval_mon (E E':onv val) e
  : agree_on (fstNoneOrR eq) (freeVars e) E E'
     fstNoneOrR eq (op_eval E e) (op_eval E' e).
Proof.
  intros. general induction e; simpl in *; eauto using fstNoneOrR.
  - exploit IHe as EQ; eauto. inv EQ; simpl; eauto using fstNoneOrR.
    reflexivity.
  - exploit as ; eauto with cset.
    inv ; simpl; eauto using fstNoneOrR.
    exploit as ; eauto with cset.
    inv ; simpl; eauto using fstNoneOrR.
    reflexivity.
Qed.


Lemma op_eval_op2bool_true V e v
  : op_eval V e = Some v val2bool v = true op2bool e Some false.
Proof.
  intros. unfold op2bool.
  exploit (@op_eval_mon (fun _None) V e).
  hnf; intros; eauto using fstNoneOrR.
  rewrite H in . inv ; simpl; congruence.
Qed.


Lemma op_eval_op2bool_false V e v
  : op_eval V e = Some v val2bool v = false op2bool e Some true.
Proof.
  intros. unfold op2bool.
  exploit (@op_eval_mon (fun _None) V e).
  hnf; intros; eauto using fstNoneOrR.
  rewrite H in . inv ; simpl; congruence.
Qed.


Lemma op2bool_val2bool E e b
  : op2bool e = Some b
     v, op_eval E e = Some v val2bool v = b.
Proof.
  intros. unfold op2bool in H. monad_inv H.
  eexists x; split; eauto.
  exploit (@op_eval_mon (fun _None) E e); eauto.
  hnf; intros; econstructor.
  inv H; congruence.
Qed.


Lemma op_eval_agree E E' e v
: agree_on eq (freeVars e) E E'
   op_eval E e = v
   op_eval E' e = v.
Proof.
  intros.
  erewrite op_eval_live; eauto.
  eauto using live_op_sound_incl, live_freeVars.
Qed.


Lemma omap_op_eval_agree E E' Y v
: agree_on eq (list_union (List.map freeVars Y)) E E'
   omap (op_eval E) Y = v
   omap (op_eval E') Y = v.
Proof.
  intros.
  erewrite omap_agree; eauto.
  intros. eapply op_eval_agree; eauto.
  eapply agree_on_incl; eauto.
  eapply incl_list_union; eauto using map_get_1.
Qed.


Lemma op_eval_live_agree E E' e lv v
: live_op_sound e lv
   agree_on eq lv E E'
   op_eval E e = v
   op_eval E' e = v.
Proof.
  intros. erewrite op_eval_live; eauto.
Qed.


Lemma omap_op_eval_live_agree E E' lv Y v
: ( n y, get Y n y live_op_sound y lv)
   agree_on eq lv E E'
   omap (op_eval E) Y = v
   omap (op_eval E') Y = v.
Proof.
  intros.
  erewrite omap_agree; eauto.
  intros. eapply op_eval_agree; eauto.
  eapply agree_on_incl; eauto using freeVars_live.
Qed.


Lemma omap_self_update E Z l
: omap (op_eval E) (List.map Var Z) = l
    E [Z <-- List.map Some l] [-] E.
Proof.
  general induction Z; simpl in × |- ×.
  - reflexivity.
  - monad_inv H; simpl.
    rewrite IHZ; eauto.
    hnf; intros; lud. congruence.
Qed.


Lemma omap_var_defined_on Za lv E
: of_list Za lv
   defined_on lv E
   l, omap (op_eval E) (List.map Var Za) = Some l.
Proof.
  intros. general induction Za; simpl.
  - eauto.
  - simpl in ×.
    edestruct .
    + instantiate (1:=a). cset_tac; intuition.
    + rewrite ; simpl. edestruct IHZa; eauto.
      cset_tac; intuition.
      rewrite ; simpl. eauto.
Qed.


Hint Extern 5 ⇒
match goal with
| [ LV : live_op_sound ?e ?lv, AG: agree_on eq ?lv ?E ?E',
     : op_eval ?E ?e = _, : op_eval ?E' ?e = _ |- _ ] ⇒
  rewrite (op_eval_live_agree LV AG ) in ; try solve [ exfalso; inv ];
    clear_trivial_eqs
end.

Lemma freeVars_live_list Y lv
  : ( (n : ) (y : op), get Y n y live_op_sound y lv)
     list_union (freeVars Y) lv.
Proof.
  intros H. eapply list_union_incl; intros; inv_get; eauto using freeVars_live with cset.
Qed.


Lemma freeVars_rename_op_list ϱ Y
  : list_union (List.map freeVars (List.map (rename_op ϱ) Y))[=]
               lookup_set ϱ (list_union (List.map freeVars Y)).
Proof.
  rewrite lookup_set_list_union; eauto using lookup_set_empty.
  repeat rewrite map_map. eapply fold_left_union_morphism; [|reflexivity].
  clear_all. general induction Y; simpl; eauto using AllInRel.PIR2, freeVars_renameOp.
Qed.


Lemma op_eval_var Y
  : ( (n : ) (y : op), get Y n y isVar y)
     { xl : list var | Y = Var xl }.
Proof.
  intros. general induction Y.
  - eexists nil; eauto.
  - exploit H; eauto using get.
    destruct a as [|v| |]; try now (exfalso; inv ).
    edestruct IHY; eauto using get; subst.
     (v::x); eauto.
Qed.


Lemma of_list_freeVars_vars xl
  : of_list xl [<=] list_union (freeVars Var xl).
Proof.
  general induction xl; simpl; eauto. rewrite list_union_start_swap.
  rewrite IHxl; eauto. cset_tac.
Qed.


Lemma omap_lookup_vars V xl vl
  : length xl = length vl
     NoDupA _eq xl
     omap (op_eval (V[xl <-- List.map Some vl])) (List.map Var xl) = Some vl.
Proof.
  intros. eapply length_length_eq in H.
  general induction H; simpl; eauto.
  lud; isabsurd; simpl.
  erewrite omap_op_eval_agree; try eapply IHlength_eq; eauto; simpl in *; intuition.
  instantiate (1:= V [x Some y]).
  eapply update_nodup_commute_eq; eauto; simpl; intuition.
Qed.


Lemma omap_replace_if V Y Y'
  : omap (op_eval V) (List.filter IsVar Y) =
      omap (op_eval V) Y' =
      omap
         (op_eval V)
         (replace_if NotVar Y Y') = merge_cond (IsVar Y) .
Proof.
  general induction Y; simpl; eauto.
  simpl in ×. cases in H; cases; isabsurd; simpl in ×.
  - monad_inv H. rewrite EQ. simpl. erewrite IHY; eauto. eauto.
  - destruct Y'; simpl in ×.
    + inv ; eauto.
    + monad_inv . rewrite EQ. simpl.
      erewrite IHY; eauto. simpl; eauto.
Qed.


Definition sid := fun xVar x.

Instance subst_op_Proper Z Y
  : Proper (_eq _eq) (subst_op (sid [Z <-- Y])).
Proof.
  hnf; intros. inv H. clear H.
  simpl. general induction y; simpl; eauto.
Qed.


Lemma eval_op_subst E y Y Z e
: length Z = length Y
   omap (op_eval E) Y = y
   op_eval (E [Z <-- List.map Some y]) e =
    op_eval E (subst_op (sid [Z <-- Y]) e).
Proof.
  intros.
  general induction e; simpl; eauto.
  - eapply length_length_eq in H.
    general induction H; simpl in × |- *; eauto.
    monad_inv . simpl.
    lud; eauto.
  - erewrite IHe; eauto.
  - erewrite ; eauto.
    erewrite ; eauto.
Qed.