sem_operators.v 2.71 KB
Newer Older
1
From solutions Require Export sem_typed.
2

Robbert Krebbers's avatar
Robbert Krebbers committed
3
(** Semantic operator typing *)
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Class SemTyUnboxed `{!heapG Σ} (A : sem_ty Σ) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
  sem_ty_unboxed v :
    A v -  val_is_unboxed v .
7

Robbert Krebbers's avatar
Robbert Krebbers committed
8
Class SemTyUnOp `{!heapG Σ} (op : un_op) (A B : sem_ty Σ) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
  sem_ty_un_op v :
    A v -  w,  un_op_eval op v = Some w   B w.
11

Robbert Krebbers's avatar
Robbert Krebbers committed
12
Class SemTyBinOp `{!heapG Σ} (op : bin_op) (A1 A2 B : sem_ty Σ) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
  sem_ty_bin_op v1 v2 :
    A1 v1 - A2 v2 -  w,  bin_op_eval op v1 v2 = Some w   B w.
15
16

Section sem_operators.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  Context `{!heapG Σ}.
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
  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.