Commit fd46e3a2 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Include a typing judgment for values so we can type check definitions.

parent 9a8ac3e6
......@@ -35,12 +35,11 @@ Section compatibility.
by iApply wp_value.
Qed.
Lemma Unit_sem_typed Γ : Γ #() : ().
Proof. iIntros (vs) "!# _ /=". by iApply wp_value. Qed.
Lemma Bool_sem_typed Γ (b : bool) : Γ #b : sem_ty_bool.
Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /sem_ty_car /=. eauto. Qed.
Lemma Int_sem_typed Γ (n : Z) : Γ #n : sem_ty_int.
Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /sem_ty_car /=. eauto. Qed.
Lemma Val_sem_typed Γ v A : ( v : A) - Γ v : A.
Proof.
iIntros "#Hv" (vs) "!# #HΓ /=".
iApply wp_value. iApply "Hv".
Qed.
Lemma Pair_sem_typed Γ e1 e2 A1 A2 :
(Γ e1 : A1) - (Γ e2 : A2) - Γ (e1,e2) : A1 * A2.
......@@ -209,4 +208,35 @@ Section compatibility.
iIntros "#H" (vs) "!# #HΓ /=".
wp_apply wp_fork; last done. by iApply (wp_wand with "(H [//])").
Qed.
Lemma UnitV_sem_typed : #() : ().
Proof. by iPureIntro. Qed.
Lemma BoolV_sem_typed (b : bool) : #b : sem_ty_bool.
Proof. by iExists b. Qed.
Lemma IntV_sem_typed (n : Z) : #n : sem_ty_int.
Proof. by iExists n. Qed.
Lemma PairV_sem_typed v1 v2 τ1 τ2 :
( v1 : τ1) - ( v2 : τ2) -
PairV v1 v2 : (τ1 * τ2).
Proof. iIntros "#H1 #H2". iExists v1, v2. auto. Qed.
Lemma InjLV_sem_typed v τ1 τ2 :
( v : τ1) -
InjLV v : (τ1 + τ2).
Proof. iIntros "H". iLeft. auto. Qed.
Lemma InjRV_sem_typed v τ1 τ2 :
( v : τ2) -
InjRV v : (τ1 + τ2).
Proof. iIntros "H". iRight. auto. Qed.
Lemma RecV_sem_typed f x e A B :
(binder_insert f (A B)%sem_ty (binder_insert x A ) e : B) -
RecV f x e : (A B).
Proof.
iIntros "#H". iLöb as "IH".
iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _).
rewrite -subst_map_binder_insert_2_empty. iApply "H".
iApply (env_sem_typed_insert with "IH").
iApply (env_sem_typed_insert with "[$]"). iApply env_sem_typed_empty.
Qed.
End compatibility.
......@@ -28,43 +28,69 @@ Section fundamental.
ty_bin_op op τ1 τ2 σ SemTyBinOp op ( τ1 ρ) ( τ2 ρ) ( σ ρ).
Proof. destruct 1; simpl; apply _. Qed.
Theorem fundamental Γ e τ ρ :
(Γ e : τ)
interp_env Γ ρ e : τ ρ.
Fixpoint fundamental Γ e τ ρ (Hty : Γ e : τ) : interp_env Γ ρ e : τ ρ
with fundamental_val v τ ρ (Hty : v : τ) : v : τ ρ.
Proof.
intros Htyped. iInduction Htyped as [] "IH" forall (ρ); simpl in *.
- iApply Var_sem_typed. by apply lookup_interp_env.
- iApply Unit_sem_typed.
- iApply Bool_sem_typed.
- iApply Int_sem_typed.
- by iApply Pair_sem_typed.
- by iApply Fst_sem_typed.
- by iApply Snd_sem_typed.
- by iApply InjL_sem_typed.
- by iApply InjR_sem_typed.
- by iApply Case_sem_typed.
- iApply Rec_sem_typed. iSpecialize ("IH" $! ρ).
by rewrite !interp_env_binder_insert.
- by iApply App_sem_typed.
- iApply TLam_sem_typed; iIntros (A). iSpecialize ("IH" $! (A :: ρ)).
by rewrite interp_env_ty_lift /=; last lia.
- rewrite interp_ty_subst /=; last lia.
iApply (TApp_sem_typed with "IH").
- iApply Pack_sem_typed. iSpecialize ("IH" $! ρ).
by rewrite interp_ty_subst; last lia.
- iApply (Unpack_sem_typed with "IH"); iIntros (A).
iSpecialize ("IH1" $! (A :: ρ)).
rewrite interp_env_binder_insert.
rewrite interp_env_ty_lift /=; last lia.
by rewrite interp_ty_lift /=; last lia.
- by iApply Alloc_sem_typed.
- by iApply Load_sem_typed.
- by iApply Store_sem_typed.
- by iApply FAA_sem_typed.
- by iApply CmpXchg_sem_typed.
- by iApply UnOp_sem_typed.
- by iApply BinOp_sem_typed.
- by iApply If_sem_typed.
- by iApply Fork_sem_typed.
Qed.
- destruct Hty; simpl.
+ iApply Var_sem_typed. by apply lookup_interp_env.
+ iApply Val_sem_typed; by iApply fundamental_val.
+ iApply Pair_sem_typed; by iApply fundamental.
+ iApply Fst_sem_typed; by iApply (fundamental _ _ (_ * _)%ty).
+ iApply Snd_sem_typed; by iApply (fundamental _ _ (_ * _)%ty).
+ iApply InjL_sem_typed; by iApply fundamental.
+ iApply InjR_sem_typed; by iApply fundamental.
+ iApply Case_sem_typed.
* by iApply (fundamental _ _ (_ + _)%ty).
* by iApply (fundamental _ _ (_ _)%ty).
* by iApply (fundamental _ _ (_ _)%ty).
+ iApply Rec_sem_typed.
change ( ?τ1 _ ?τ2 _)%sem_ty with ( τ1 τ2 ρ).
rewrite -!interp_env_binder_insert. by iApply fundamental.
+ iApply App_sem_typed.
* by iApply (fundamental _ _ (_ _)%ty).
* by iApply fundamental.
+ iApply TLam_sem_typed; iIntros (A).
rewrite -interp_env_ty_lift_0. by iApply fundamental.
+ rewrite interp_ty_subst_0.
iApply (TApp_sem_typed _ _ (λ A, _ (A :: _))).
by iApply (fundamental _ _ (∀: _)%ty).
+ iApply (Pack_sem_typed _ _ _ ( _ ρ)).
rewrite -interp_ty_subst_0. by iApply fundamental.
+ iApply (Unpack_sem_typed _ _ _ _ (λ A, _ (A :: _))).
* by iApply (fundamental _ _ (∃: _)%ty).
* iIntros (A).
rewrite -(interp_ty_lift_0 _ A ρ) -(interp_env_ty_lift_0 _ A ρ).
rewrite -interp_env_binder_insert.
by iApply fundamental.
+ iApply Alloc_sem_typed. by iApply fundamental.
+ iApply Load_sem_typed. by iApply (fundamental _ _ (ref _)%ty).
+ iApply Store_sem_typed.
* by iApply (fundamental _ _ (ref _)%ty).
* by iApply fundamental.
+ iApply FAA_sem_typed.
* by iApply (fundamental _ _ (ref TInt)%ty).
* by iApply (fundamental _ _ TInt).
+ iApply CmpXchg_sem_typed.
* by iApply (fundamental _ _ (ref _)%ty).
* by iApply fundamental.
* by iApply fundamental.
+ iApply UnOp_sem_typed. by iApply fundamental.
+ iApply BinOp_sem_typed; by iApply fundamental.
+ iApply If_sem_typed.
* by iApply (fundamental _ _ TBool).
* by iApply fundamental.
* by iApply fundamental.
+ iApply Fork_sem_typed. by iApply (fundamental _ _ TUnit).
- destruct Hty; simpl.
+ iApply UnitV_sem_typed.
+ iApply BoolV_sem_typed.
+ iApply IntV_sem_typed.
+ iApply PairV_sem_typed; by iApply fundamental_val.
+ iApply InjLV_sem_typed; by iApply fundamental_val.
+ iApply InjRV_sem_typed; by iApply fundamental_val.
+ iApply RecV_sem_typed.
change ( ?τ1 _ ?τ2 _)%sem_ty with ( τ1 τ2 ρ).
rewrite -(interp_env_empty ρ) -!interp_env_binder_insert.
by iApply fundamental.
Qed.
End fundamental.
......@@ -70,6 +70,8 @@ Section interp_properties.
- intros τ IH n ρ ?. f_equiv=> A /=. naive_solver auto with lia.
- intros τ IH n ρ ?. f_equiv=> A /=. naive_solver auto with lia.
Qed.
Lemma interp_ty_lift_0 τ A ρ : ty_lift 0 τ (A :: ρ) τ ρ.
Proof. apply interp_ty_lift; simpl; lia. Qed.
Lemma interp_env_ty_lift n Γ ρ :
n length ρ
......@@ -78,6 +80,9 @@ Section interp_properties.
intros. rewrite /interp_env -map_fmap_compose.
apply map_fmap_equiv_ext=> x A _ /=. by rewrite interp_ty_lift.
Qed.
Lemma interp_env_ty_lift_0 Γ A ρ :
interp_env (ty_lift 0 <$> Γ) (A :: ρ) interp_env Γ ρ.
Proof. apply interp_env_ty_lift; simpl; lia. Qed.
Lemma interp_ty_subst i τ τ' ρ :
i length ρ
......@@ -97,5 +102,7 @@ Section interp_properties.
- intros τ IH i τ' ρ ?. f_equiv=> A /=. rewrite IH /=; last lia.
by rewrite interp_ty_lift; last lia.
Qed.
Lemma interp_ty_subst_0 τ τ' ρ :
ty_subst 0 τ' τ ρ τ ( τ' ρ :: ρ).
Proof. apply interp_ty_subst; simpl; lia. Qed.
End interp_properties.
......@@ -33,6 +33,13 @@ Instance: Params (@sem_typed) 2 := {}.
Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
(at level 100, e at next level, A at level 200).
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 at next level, A at level 200).
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. *)
......@@ -62,6 +69,16 @@ Section sem_typed.
Global Instance sem_typed_persistent Γ e A : Persistent (Γ e : A).
Proof. rewrite /sem_typed /=. apply _. Qed.
Global Instance sem_val_typed_ne n v :
Proper (dist n ==> dist n) (@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
......@@ -78,6 +95,8 @@ Section sem_typed.
iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ").
Qed.
Lemma env_sem_typed_empty vs : env_sem_typed vs - vs = ∅⌝.
Lemma env_sem_typed_empty : env_sem_typed .
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.
......@@ -29,89 +29,111 @@ Existing Class ty_bin_op.
Existing Instances Ty_bin_op_eq Ty_bin_op_arith Ty_bin_op_compare Ty_bin_op_bool.
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
Inductive typed (Γ : gmap string ty) : expr ty Prop :=
Reserved Notation "⊢ᵥ v : τ" (at level 20, v, τ at next level).
Inductive typed : gmap string ty expr ty Prop :=
(** Variables *)
| Var_typed x τ :
| Var_typed Γ x τ :
Γ !! x = Some τ
Γ Var x : τ
(** Base tys *)
| Unit_typed :
Γ #() : TUnit
| Bool_typed (b : bool) :
Γ # b : TBool
| Int_typed (i : Z) :
Γ # i : TInt
(** Values *)
| Val_typed Γ v τ :
val_typed v τ
Γ v : τ
(** Products and sums *)
| Pair_typed e1 e2 τ1 τ2 :
| Pair_typed Γ e1 e2 τ1 τ2 :
Γ e1 : τ1 Γ e2 : τ2
Γ Pair e1 e2 : TProd τ1 τ2
| Fst_typed e τ1 τ2 :
| Fst_typed Γ e τ1 τ2 :
Γ e : TProd τ1 τ2
Γ Fst e : τ1
| Snd_typed e τ1 τ2 :
| Snd_typed Γ e τ1 τ2 :
Γ e : TProd τ1 τ2
Γ Snd e : τ2
| InjL_typed e τ1 τ2 :
| InjL_typed Γ e τ1 τ2 :
Γ e : τ1
Γ InjL e : TSum τ1 τ2
| InjR_typed e τ1 τ2 :
| InjR_typed Γ e τ1 τ2 :
Γ e : τ2
Γ InjR e : TSum τ1 τ2
| Case_typed e0 e1 e2 τ1 τ2 τ3 :
| Case_typed Γ e0 e1 e2 τ1 τ2 τ3 :
Γ e0 : TSum τ1 τ2 Γ e1 : TArr τ1 τ3 Γ e2 : TArr τ2 τ3
Γ Case e0 e1 e2 : τ3
(** Functions *)
| Rec_typed f x e τ1 τ2 :
| Rec_typed Γ f x e τ1 τ2 :
binder_insert f (TArr τ1 τ2) (binder_insert x τ1 Γ) e : τ2
Γ Rec f x e : TArr τ1 τ2
| App_typed e1 e2 τ1 τ2 :
| App_typed Γ e1 e2 τ1 τ2 :
Γ e1 : TArr τ1 τ2 Γ e2 : τ1
Γ App e1 e2 : τ2
(** Polymorphic functions and existentials *)
| TLam_typed e τ :
| TLam_typed Γ e τ :
ty_lift 0 <$> Γ e : τ
Γ (Λ: e) : TForall τ
| TApp_typed e τ τ' :
| TApp_typed Γ e τ τ' :
Γ e : TForall τ
Γ e <_> : ty_subst 0 τ' τ
| Pack_typed e τ τ' :
| Pack_typed Γ e τ τ' :
Γ e : ty_subst 0 τ' τ
Γ e : TExist τ
| Unpack_typed e1 x e2 τ τ2 :
| Unpack_typed Γ e1 x e2 τ τ2 :
Γ e1 : TExist τ
binder_insert x τ (ty_lift 0 <$> Γ) e2 : ty_lift 0 τ2
Γ (unpack: x := e1 in e2) : τ2
(** Heap operations *)
| Alloc_typed e τ :
| Alloc_typed Γ e τ :
Γ e : τ
Γ Alloc e : TRef τ
| Load_typed e τ :
| Load_typed Γ e τ :
Γ e : TRef τ
Γ Load e : τ
| Store_typed e1 e2 τ :
| Store_typed Γ e1 e2 τ :
Γ e1 : TRef τ Γ e2 : τ
Γ Store e1 e2 : TUnit
| FAA_typed e1 e2 :
| FAA_typed Γ e1 e2 :
Γ e1 : TRef TInt Γ e2 : TInt
Γ FAA e1 e2 : TInt
| CmpXchg_typed e1 e2 e3 τ :
| CmpXchg_typed Γ e1 e2 e3 τ :
ty_unboxed τ
Γ e1 : TRef τ Γ e2 : τ Γ e3 : τ
Γ CmpXchg e1 e2 e3 : TProd τ TBool
(** Operators *)
| UnOp_typed op e τ σ :
| UnOp_typed Γ op e τ σ :
Γ e : τ
ty_un_op op τ σ
Γ UnOp op e : σ
| BinOp_typed op e1 e2 τ1 τ2 σ :
| BinOp_typed Γ op e1 e2 τ1 τ2 σ :
Γ e1 : τ1 Γ e2 : τ2
ty_bin_op op τ1 τ2 σ
Γ BinOp op e1 e2 : σ
| If_typed e0 e1 e2 τ :
| If_typed Γ e0 e1 e2 τ :
Γ e0 : TBool Γ e1 : τ Γ e2 : τ
Γ If e0 e1 e2 : τ
(** Fork *)
| Fork_typed e :
| Fork_typed Γ e :
Γ e : TUnit
Γ Fork e : TUnit
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
with val_typed : val ty Prop :=
(** Base types *)
| UnitV_typed :
#() : TUnit
| BoolV_typed (b : bool) :
#b : TBool
| IntV_val_typed (i : Z) :
#i : TInt
(** Products and sums *)
| PairV_typed v1 v2 τ1 τ2 :
v1 : τ1 v2 : τ2
PairV v1 v2 : TProd τ1 τ2
| InjLV_typed v τ1 τ2 :
v : τ1
InjLV v : TSum τ1 τ2
| InjRV_typed v τ1 τ2 :
v : τ2
InjRV v : TSum τ1 τ2
(** Functions *)
| RecV_typed f x e τ1 τ2 :
binder_insert f (TArr τ1 τ2) (binder_insert x τ1 ) e : τ2
RecV f x e : TArr τ1 τ2
where "Γ ⊢ₜ e : τ" := (typed Γ e τ)
and "⊢ᵥ v : τ" := (val_typed v τ).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment