From exercises Require Export sem_typed.

(** Semantic operator typing *)
Class SemTyUnboxed `{!heapG Σ} (A : sem_ty Σ) :=
  sem_ty_unboxed v :
    A v -∗ ⌜ val_is_unboxed v ⌝.

Class SemTyUnOp `{!heapG Σ} (op : un_op) (A B : sem_ty Σ) :=
  sem_ty_un_op v :
    A v -∗ ∃ w, ⌜ un_op_eval op v = Some w ⌝ ∧ B w.

Class SemTyBinOp `{!heapG Σ} (op : bin_op) (A1 A2 B : sem_ty Σ) :=
  sem_ty_bin_op v1 v2 :
    A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∧ B w.

Section sem_operators.
  Context `{!heapG Σ}.
  Implicit Types A B : sem_ty Σ.

  (* Unboxed types *)
  Global Instance sem_ty_unit_unboxed : SemTyUnboxed ().
  Proof. by iIntros (v ->). Qed.
  Global Instance sem_ty_bool_unboxed : SemTyUnboxed sem_ty_bool.
  Proof. iIntros (v). by iDestruct 1 as (b) "->". Qed.
  Global Instance sem_ty_int_unboxed : SemTyUnboxed sem_ty_int.
  Proof. iIntros (v). by iDestruct 1 as (i) "->". Qed.
  Global Instance sem_ty_ref_unboxed A : SemTyUnboxed (ref A).
  Proof. iIntros (v). by iDestruct 1 as (i ->) "?". Qed.

  (* Operator typing *)
  Global Instance sem_ty_un_op_int op : SemTyUnOp op sem_ty_int sem_ty_int.
  Proof. iIntros (?). iDestruct 1 as (i) "->". destruct op; eauto. Qed.
  Global Instance sem_ty_un_op_bool : SemTyUnOp NegOp sem_ty_bool sem_ty_bool.
  Proof. iIntros (?). iDestruct 1 as (i) "->". eauto. Qed.

  Global Instance sem_ty_bin_op_eq A : SemTyUnboxed A → SemTyBinOp EqOp A A sem_ty_bool.
  Proof.
    iIntros (? v1 v2) "A1 _". rewrite /bin_op_eval /sem_ty_car /=.
    iDestruct (sem_ty_unboxed with "A1") as %Hunb.
    rewrite decide_True; last solve_vals_compare_safe.
    eauto.
  Qed.
  Global Instance sem_ty_bin_op_arith op :
    TCElemOf op [PlusOp; MinusOp; MultOp; QuotOp; RemOp;
                 AndOp; OrOp; XorOp; ShiftLOp; ShiftROp] →
    SemTyBinOp op sem_ty_int sem_ty_int sem_ty_int.
  Proof.
    iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->".
    repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
      rewrite /sem_ty_car /=; eauto.
  Qed.
  Global Instance sem_ty_bin_op_compare op :
    TCElemOf op [LeOp; LtOp] →
    SemTyBinOp op sem_ty_int sem_ty_int sem_ty_bool.
  Proof.
    iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->".
    repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
      rewrite /sem_ty_car /=; eauto.
  Qed.
  Global Instance sem_ty_bin_op_bool op :
    TCElemOf op [AndOp; OrOp; XorOp] →
    SemTyBinOp op sem_ty_bool sem_ty_bool sem_ty_bool.
  Proof.
    iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->".
    repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
      rewrite /sem_ty_car /=; eauto.
  Qed.
End sem_operators.