sem_typed.v 3.98 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From exercises Require Export sem_type_formers.
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92

(** * The semantic typing judgment *)

(** We define the judgment [Γ ⊨ e : A] for semantic typing of the expression [e]
at semantic type [A], assuming that free variables in [e] belong to the semantic
types described by [Γ]. This notion is defined as follows:

- We define the semantic typing relation [env_sem_typed] for typing contexts:
  An environments (mappings from free variables to values) [vs] is in the
  semantic type for a typing context [Γ], [env_sem_typed Γ vs], if for any free
  variable [x], [vs(x)] is in the semantic type [Γ(x)].
- The semantic typing judgment [Γ ⊨ e : A] holds if for any environment [vs]
  such that [env_sem_typed Γ vs] we have that [subst_map vs e] is an expression
  in the semantics of type [A], i.e., [WP subst_map vs e {{ A }}] holds. *)

(** The semantic type for the typing context (environment). *)
Definition env_sem_typed `{!heapG Σ} (Γ : gmap string (sem_ty Σ))
    (vs : gmap string val) : iProp Σ :=
  ([ map] i  A;v  Γ; vs, sem_ty_car A v)%I.
Instance: Params (@env_sem_typed) 2 := {}.

(** The semantics typing judgment. *)
Definition sem_typed `{!heapG Σ}
    (Γ : gmap string (sem_ty Σ)) (e : expr) (A : sem_ty Σ) : iProp Σ :=
  tc_opaque (  vs,
    env_sem_typed Γ vs - WP subst_map vs e {{ A }})%I.
Instance: Params (@sem_typed) 2 := {}.
Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
  (at level 74, e, A at next level) : bi_scope.

Definition sem_val_typed `{!heapG Σ} (v : val) (A : sem_ty Σ) : iProp Σ :=
  tc_opaque (A v).
Instance: Params (@sem_val_typed) 3 := {}.
Notation "⊨ᵥ v : A" := (sem_val_typed v A)
  (at level 20, v, A at next level) : bi_scope.
Arguments sem_val_typed : simpl never.

(** A few useful lemmas about the semantic typing judgment. The first
few lemmas involving [Proper]ness are boilerplate required for supporting setoid
rewriting. *)
Section sem_typed.
  Context `{!heapG Σ}.
  Implicit Types A B : sem_ty Σ.
  Implicit Types C : sem_ty Σ  sem_ty Σ.

  Global Instance env_sem_typed_ne n :
    Proper (dist n ==> (=) ==> dist n) (@env_sem_typed Σ _).
  Proof.
    intros Γ1 Γ2 HΓ ρ ? <-.
    apply big_sepM2_ne_2=> // k A1 v1 A2 v2 _ _ HA _ _ /discrete_iff / leibniz_equiv_iff ->.
    by apply HA.
  Qed.
  Global Instance env_sem_typed_proper :
    Proper (() ==> (=) ==> ()) (@env_sem_typed Σ _).
  Proof. intros Γ1 Γ2 HΓ ρ ? <-. apply equiv_dist=> n. f_equiv. by rewrite HΓ. Qed.

  Global Instance sem_typed_ne n :
    Proper (dist n ==> (=) ==> dist n ==> dist n) (@sem_typed Σ _).
  Proof. solve_proper. Qed.
  Global Instance sem_typed_proper :
    Proper (() ==> (=) ==> () ==> ()) (@sem_typed Σ _).
  Proof. solve_proper. Qed.

  Global Instance sem_typed_persistent Γ e A : Persistent (Γ  e : A).
  Proof. rewrite /sem_typed /=. apply _. Qed.

  Global Instance sem_val_typed_ne v : NonExpansive (@sem_val_typed Σ _ v).
  Proof. solve_proper. Qed.
  Global Instance sem_val_typed_proper v :
    Proper (() ==> ()) (@sem_val_typed Σ _ v).
  Proof. solve_proper. Qed.

  Global Instance sem_val_typed_persistent v A : Persistent ( v : A).
  Proof. rewrite /sem_val_typed /=. apply _. Qed.

  (* Environments *)
  Lemma env_sem_typed_lookup Γ vs x A :
    Γ !! x = Some A 
    env_sem_typed Γ vs -  v,  vs !! x = Some v   A v.
  Proof.
    iIntros (HΓx) "HΓ". rewrite /env_sem_typed.
    by iApply (big_sepM2_lookup_1 with "HΓ").
  Qed.
  Lemma env_sem_typed_insert Γ vs x A v :
    A v - env_sem_typed Γ vs -
    env_sem_typed (binder_insert x A Γ) (binder_insert x v vs).
  Proof.
    destruct x as [|x]=> /=; first by auto. rewrite /env_sem_typed.
    iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ").
  Qed.

93
  Lemma env_sem_typed_empty :  env_sem_typed  .
94
95
96
97
  Proof. iIntros "". by rewrite /env_sem_typed. Qed.
  Lemma env_sem_typed_empty_l_inv vs : env_sem_typed  vs - vs = ∅⌝.
  Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed.
End sem_typed.