sem_typed.v 3.15 KB
Newer Older
1
From tutorial_popl20 Require Export sem_type_formers.
Robbert Krebbers's avatar
Robbert Krebbers committed
2

Amin Timany's avatar
Amin Timany committed
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(** * Here we define 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). *)
Robbert Krebbers's avatar
Robbert Krebbers committed
23
24
25
26
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 := {}.
Amin Timany's avatar
Amin Timany committed
27
28

(** The semantics typing judgment. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
31
32
33
34
35
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 100, e at next level, A at level 200).

Amin Timany's avatar
Amin Timany committed
36
37
38
(** A few useful lemmas about the semantic typing judgment. The first
few lemmas involving [Proper]ness are boilerplate required for supporting setoid
rewriting. *)
39
Section sem_typed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  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. Admitted.
  Global Instance env_sem_typed_proper :
    Proper (() ==> (=) ==> ()) (@env_sem_typed Σ _).
  Proof. intros ??????. subst. rewrite /env_sem_typed. Admitted.
  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.

  (* 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.

Amin Timany's avatar
Amin Timany committed
76
77
  Lemma env_sem_typed_empty vs : env_sem_typed  vs - vs = ∅⌝.
  Proof. by iIntros "?"; iApply big_sepM2_empty_r. Qed.
78
End sem_typed.