Commit 863176c3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Improve order: put prod/sum first.

parent e3e23ae9
......@@ -7,9 +7,9 @@ Fixpoint interp `{heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ :=
| TUnit => sem_ty_unit
| TBool => sem_ty_bool
| TInt => sem_ty_int
| TArr τ1 τ2 => τ1 ρ τ2 ρ
| TProd τ1 τ2 => τ1 ρ * τ2 ρ
| TSum τ1 τ2 => τ1 ρ + τ2 ρ
| TArr τ1 τ2 => τ1 ρ τ2 ρ
| TForall τ => X, τ (X :: ρ)
| TExist τ => X, τ (X :: ρ)
| TRef τ => ref ( τ ρ)
......@@ -99,15 +99,15 @@ Section fundamental.
- iApply sem_typed_unit.
- iApply sem_typed_bool.
- iApply sem_typed_int.
- iApply sem_typed_rec. iSpecialize ("IH" $! ρ).
by rewrite !interp_env_binder_insert.
- by iApply sem_typed_app.
- by iApply sem_typed_pair.
- by iApply sem_typed_fst.
- by iApply sem_typed_snd.
- by iApply sem_typed_injl.
- by iApply sem_typed_injr.
- by iApply sem_typed_case.
- iApply sem_typed_rec. iSpecialize ("IH" $! ρ).
by rewrite !interp_env_binder_insert.
- by iApply sem_typed_app.
- iApply sem_typed_tlam; iIntros (A). iSpecialize ("IH" $! (A :: ρ)).
by rewrite interp_env_ty_lift /=; last lia.
- rewrite interp_ty_subst /=; last lia.
......
......@@ -49,14 +49,14 @@ Section types.
Definition sem_ty_bool : sem_ty Σ := SemTy (λ w, b : bool, w = #b )%I.
Definition sem_ty_int : sem_ty Σ := SemTy (λ w, n : Z, w = #n )%I.
Definition sem_ty_arr (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
v, A1 v - WP App w v {{ A2 }})%I.
Definition sem_ty_prod (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
w1 w2, w = PairV w1 w2 A1 w1 A2 w2)%I.
Definition sem_ty_sum (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
( w1, w = InjLV w1 A1 w1) ( w2, w = InjRV w2 A2 w2))%I.
Definition sem_ty_arr (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
v, A1 v - WP App w v {{ A2 }})%I.
Definition sem_ty_forall (C : sem_ty Σ sem_ty Σ) : sem_ty Σ := SemTy (λ w,
A : sem_ty Σ, WP w #() {{ w, C A w }})%I.
Definition sem_ty_exist (C : sem_ty Σ sem_ty Σ) : sem_ty Σ := SemTy (λ w,
......@@ -76,9 +76,9 @@ Instance: Params (@sem_ty_ref) 2 := {}.
(* Nice notations *)
Notation "()" := sem_ty_unit : sem_ty_scope.
Infix "→" := sem_ty_arr : sem_ty_scope.
Infix "*" := sem_ty_prod : sem_ty_scope.
Infix "+" := sem_ty_sum : sem_ty_scope.
Infix "→" := sem_ty_arr : sem_ty_scope.
Notation "∀ A1 .. An , C" :=
(sem_ty_forall (λ A1, .. (sem_ty_forall (λ An, C%sem_ty)) ..)) : sem_ty_scope.
Notation "∃ A1 .. An , C" :=
......
From tutorial_popl20 Require Export sem_types.
From tutorial_popl20 Require Export sem_type_formers.
(* Typing for operators *)
Class SemTyUnboxed `{heapG Σ} (A : sem_ty Σ) :=
......@@ -126,29 +126,6 @@ Section typed_properties.
Lemma sem_typed_int Γ (n : Z) : Γ #n : sem_ty_int.
Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /sem_ty_car /=. eauto. Qed.
Lemma sem_typed_rec Γ f x e A1 A2 :
(binder_insert f (A1 A2)%sem_ty (binder_insert x A1 Γ) e : A2) -
Γ (rec: f x := e) : A1 A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH".
iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _).
iSpecialize ("H" $! (binder_insert f r (binder_insert x v vs)) with "[#]").
{ iApply (env_sem_typed_insert with "IH"). by iApply env_sem_typed_insert. }
destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
destruct (decide (x = f)) as [->|].
- by rewrite subst_subst delete_idemp insert_insert -subst_map_insert.
- rewrite subst_subst_ne // -subst_map_insert.
by rewrite -delete_insert_ne // -subst_map_insert.
Qed.
Lemma sem_typed_app Γ e1 e2 A1 A2 :
(Γ e1 : A1 A2) - (Γ e2 : A1) - Γ e1 e2 : A2.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w) "#HA1".
wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HA". by iApply "HA".
Qed.
Lemma sem_typed_pair Γ e1 e2 A1 A2 :
(Γ e1 : A1) - (Γ e2 : A2) - Γ (e1,e2) : A1 * A2.
Proof.
......@@ -194,6 +171,29 @@ Section typed_properties.
wp_apply (wp_wand with "(H2 [//])"); iIntros (v) "#HAB". by iApply "HAB".
Qed.
Lemma sem_typed_rec Γ f x e A1 A2 :
(binder_insert f (A1 A2)%sem_ty (binder_insert x A1 Γ) e : A2) -
Γ (rec: f x := e) : A1 A2.
Proof.
iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH".
iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _).
iSpecialize ("H" $! (binder_insert f r (binder_insert x v vs)) with "[#]").
{ iApply (env_sem_typed_insert with "IH"). by iApply env_sem_typed_insert. }
destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
destruct (decide (x = f)) as [->|].
- by rewrite subst_subst delete_idemp insert_insert -subst_map_insert.
- rewrite subst_subst_ne // -subst_map_insert.
by rewrite -delete_insert_ne // -subst_map_insert.
Qed.
Lemma sem_typed_app Γ e1 e2 A1 A2 :
(Γ e1 : A1 A2) - (Γ e2 : A1) - Γ e1 e2 : A2.
Proof.
iIntros "#H1 #H2" (vs) "!# #HΓ /=".
wp_apply (wp_wand with "(H2 [//])"); iIntros (w) "#HA1".
wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HA". by iApply "HA".
Qed.
Lemma sem_typed_tlam Γ e C : ( A, Γ e : C A) - Γ (Λ: e) : A, C A.
Proof.
iIntros "#H" (vs) "!# #HΓ /=". wp_pures.
......
......@@ -5,9 +5,9 @@ Inductive ty :=
| TUnit : ty
| TBool : ty
| TInt : ty
| TArr : ty ty ty
| TProd : ty ty ty
| TSum : ty ty ty
| TArr : ty ty ty
| TForall : ty ty
| TExist : ty ty
| TRef : ty ty.
......@@ -29,9 +29,9 @@ Fixpoint ty_lift (n : nat) (τ : ty) : ty :=
| TUnit => TUnit
| TBool => TBool
| TInt => TInt
| TArr τ1 τ2 => TArr (ty_lift n τ1) (ty_lift n τ2)
| TProd τ1 τ2 => TProd (ty_lift n τ1) (ty_lift n τ2)
| TSum τ1 τ2 => TSum (ty_lift n τ1) (ty_lift n τ2)
| TArr τ1 τ2 => TArr (ty_lift n τ1) (ty_lift n τ2)
| TForall τ => TForall (ty_lift (S n) τ)
| TExist τ => TExist (ty_lift (S n) τ)
| TRef τ => TRef (ty_lift n τ)
......@@ -44,9 +44,9 @@ Fixpoint ty_subst (x : nat) (σ : ty) (τ : ty) : ty :=
| TUnit => TUnit
| TBool => TBool
| TInt => TInt
| TArr τ1 τ2 => TArr (ty_subst x σ τ1) (ty_subst x σ τ2)
| TProd τ1 τ2 => TProd (ty_subst x σ τ1) (ty_subst x σ τ2)
| TSum τ1 τ2 => TSum (ty_subst x σ τ1) (ty_subst x σ τ2)
| TArr τ1 τ2 => TArr (ty_subst x σ τ1) (ty_subst x σ τ2)
| TForall τ => TForall (ty_subst (S x) (ty_lift 0 σ) τ)
| TExist τ => TExist (ty_subst (S x) (ty_lift 0 σ) τ)
| TRef τ => TRef (ty_subst x σ τ)
......
......@@ -41,13 +41,6 @@ Inductive typed (Γ : gmap string ty) : expr → ty → Prop :=
Γ # b : TBool
| Int_typed (i : Z) :
Γ # i : TInt
(** Functions *)
| 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 :
Γ e1 : TArr τ1 τ2 Γ e2 : τ1
Γ App e1 e2 : τ2
(** Products and sums *)
| Pair_typed e1 e2 τ1 τ2 :
Γ e1 : τ1 Γ e2 : τ2
......@@ -67,6 +60,13 @@ Inductive typed (Γ : gmap string ty) : expr → ty → Prop :=
| 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 :
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 :
Γ e1 : TArr τ1 τ2 Γ e2 : τ1
Γ App e1 e2 : τ2
(** Polymorphic functions and existentials *)
| TLam_typed e τ :
ty_lift 0 <$> Γ e : τ
......
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