Commit 74a31dc7 authored by Dan Frumin's avatar Dan Frumin
Browse files

Add typing for values.

parent aff91eaa
......@@ -88,6 +88,7 @@ Fixpoint fill_ctx_item (ctx : ctx_item) (e : expr) : expr :=
Definition ctx := list ctx_item.
(* TODO: consider using foldl here *)
Definition fill_ctx (K : ctx) (e : expr) : expr := foldr fill_ctx_item e K.
(** typed ctx *)
......@@ -283,15 +284,15 @@ Section bin_log_related_under_typed_ctx.
iAlways. iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_app with "[]").
iApply (IHK with "[Hrel]"); auto.
by iApply binary_fundamental.
by iApply fundamental.
+ iApply (bin_log_related_app _ _ _ _ _ _ τ2 with "[]").
by iApply binary_fundamental.
by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_pair with "[]").
iApply (IHK with "[Hrel]"); auto.
by iApply binary_fundamental.
by iApply fundamental.
+ iApply (bin_log_related_pair with "[]").
by iApply binary_fundamental.
by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply bin_log_related_fst.
iApply (IHK with "[Hrel]"); auto.
......@@ -303,36 +304,36 @@ Section bin_log_related_under_typed_ctx.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_case with "[] []").
iApply (IHK with "[Hrel]"); auto.
by iApply binary_fundamental.
by iApply binary_fundamental.
by iApply fundamental.
by iApply fundamental.
+ iApply (bin_log_related_case with "[] []").
by iApply binary_fundamental.
by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
by iApply binary_fundamental.
by iApply fundamental.
+ iApply (bin_log_related_case with "[] []").
by iApply binary_fundamental.
by iApply binary_fundamental.
by iApply fundamental.
by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []");
try by iApply binary_fundamental.
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []");
try by iApply binary_fundamental.
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_if with "[] []");
try by iApply binary_fundamental.
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_nat_binop with "[]");
try (by iApply binary_fundamental); eauto.
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_nat_binop with "[]");
try (by iApply binary_fundamental); eauto.
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_bool_binop with "[]");
try (by iApply binary_fundamental); eauto.
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_bool_binop with "[]");
try (by iApply binary_fundamental); eauto.
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_fold with "[]").
iApply (IHK with "[Hrel]"); auto.
......@@ -356,19 +357,19 @@ Section bin_log_related_under_typed_ctx.
+ iApply (bin_log_related_load with "[]").
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_store with "[]");
try by iApply binary_fundamental.
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_store with "[]");
try by iApply binary_fundamental.
try by iApply fundamental.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_CmpXchg with "[] []");
try (by iApply binary_fundamental); eauto.
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_CmpXchg with "[] []");
try (by iApply binary_fundamental); eauto.
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
+ iApply (bin_log_related_CmpXchg with "[] []");
try (by iApply binary_fundamental); eauto.
try (by iApply fundamental); eauto.
iApply (IHK with "[Hrel]"); auto.
Qed.
End bin_log_related_under_typed_ctx.
......@@ -470,44 +470,91 @@ Section fundamental.
asimpl. eauto.
Qed.
Theorem binary_fundamental Δ Γ e τ :
Γ e : τ ({Δ;Γ} e log e : τ)%I.
Theorem fundamental Δ Γ e τ :
Γ e : τ ({Δ;Γ} e log e : τ)%I
with fundamental_val Δ v τ :
v : τ (interp τ Δ v v).
Proof.
intros Ht. iInduction Ht as [] "IH" forall (Δ).
- by iApply bin_log_related_var.
- iApply bin_log_related_unit.
- by iApply bin_log_related_nat.
- by iApply bin_log_related_bool.
- by iApply (bin_log_related_nat_binop with "[]").
- by iApply (bin_log_related_bool_binop with "[]").
- by iApply bin_log_related_ref_binop.
- by iApply (bin_log_related_pair with "[]").
- by iApply bin_log_related_fst.
- by iApply bin_log_related_snd.
- by iApply bin_log_related_injl.
- by iApply bin_log_related_injr.
- by iApply (bin_log_related_case with "[] []").
- by iApply (bin_log_related_if with "[] []").
- iApply (bin_log_related_rec with "[]"); eauto.
- by iApply (bin_log_related_app with "[] []").
- iApply bin_log_related_tlam; eauto.
- by iApply bin_log_related_tapp'.
- by iApply bin_log_related_fold.
- by iApply bin_log_related_unfold.
- by iApply bin_log_related_pack'.
- iApply (bin_log_related_unpack with "[]"); eauto.
- by iApply bin_log_related_fork.
- by iApply bin_log_related_alloc.
- by iApply bin_log_related_load.
- by iApply (bin_log_related_store with "[]").
- by iApply (bin_log_related_CmpXchg with "[] []").
- intros Ht. destruct Ht.
+ by iApply bin_log_related_var.
+ iIntros (γ) "#H". simpl. rel_values.
iModIntro. by iApply fundamental_val.
+ iApply bin_log_related_unit.
+ by iApply bin_log_related_nat.
+ by iApply bin_log_related_bool.
+ iApply bin_log_related_nat_binop; first done;
by iApply fundamental.
+ iApply bin_log_related_bool_binop; first done;
by iApply fundamental.
+ iApply bin_log_related_ref_binop;
by iApply fundamental.
+ iApply bin_log_related_pair;
by iApply fundamental.
+ iApply bin_log_related_fst;
by iApply fundamental.
+ iApply bin_log_related_snd;
by iApply fundamental.
+ iApply bin_log_related_injl;
by iApply fundamental.
+ iApply bin_log_related_injr;
by iApply fundamental.
+ iApply bin_log_related_case;
by iApply fundamental.
+ iApply bin_log_related_if;
by iApply fundamental.
+ iApply bin_log_related_rec.
iAlways. by iApply fundamental.
+ iApply bin_log_related_app;
by iApply fundamental.
+ iApply bin_log_related_tlam.
iIntros (A). iAlways. by iApply fundamental.
+ iApply bin_log_related_tapp'; by iApply fundamental.
+ iApply bin_log_related_fold; by iApply fundamental.
+ iApply bin_log_related_unfold; by iApply fundamental.
+ iApply bin_log_related_pack'; by iApply fundamental.
+ iApply bin_log_related_unpack; try by iApply fundamental.
iIntros (A). by iApply fundamental.
+ iApply bin_log_related_fork; by iApply fundamental.
+ iApply bin_log_related_alloc; by iApply fundamental.
+ iApply bin_log_related_load; by iApply fundamental.
+ iApply bin_log_related_store; by iApply fundamental.
+ iApply bin_log_related_CmpXchg; eauto;
by iApply fundamental.
- intros Hv. destruct Hv; simpl.
+ iSplit; eauto.
+ iExists _; iSplit; eauto.
+ iExists _; iSplit; eauto.
+ iExists _,_,_,_.
repeat iSplit; eauto; by iApply fundamental_val.
+ iExists _,_. iLeft.
repeat iSplit; eauto; by iApply fundamental_val.
+ iExists _,_. iRight.
repeat iSplit; eauto; by iApply fundamental_val.
+ iLöb as "IH". iAlways.
iIntros (v1 v2) "#Hv".
pose (Γ := (<[f:=(τ1 τ2)%ty]> (<[x:=τ1]> )):stringmap type).
pose (γ := (binder_insert f ((rec: f x := e)%V,(rec: f x := e)%V)
(binder_insert x (v1, v2) )):stringmap (val*val)).
rel_pure_l. rel_pure_r.
iPoseProof (fundamental Δ Γ e τ2 $! γ with "[]") as "H"; eauto.
{ rewrite /γ /Γ. rewrite !binder_insert_fmap fmap_empty.
iApply (env_ltyped2_insert with "IH").
iApply (env_ltyped2_insert with "Hv").
iApply env_ltyped2_empty. }
rewrite /γ /=. rewrite !binder_insert_fmap !fmap_empty /=.
by rewrite !subst_map_binder_insert_2_empty.
+ iIntros (A). iAlways. iIntros (v1 v2) "_".
rel_pures_l. rel_pures_r.
iPoseProof (fundamental (A::Δ) e τ $! with "[]") as "H"; eauto.
{ rewrite fmap_empty. iApply env_ltyped2_empty. }
by rewrite !fmap_empty subst_map_empty.
Qed.
Theorem refines_typed τ Δ e :
e : τ
REL e << e : (interp τ Δ ).
Proof.
move=> /binary_fundamental Hty.
move=> /fundamental Hty.
iPoseProof (Hty Δ with "[]") as "H".
{ rewrite fmap_empty. iApply env_ltyped2_empty. }
by rewrite !fmap_empty !subst_map_empty.
......
......@@ -41,7 +41,7 @@ Theorem F_mu_ref_conc_typesfety e e' τ σ thp σ' :
Proof.
intros.
eapply (logrel_typesafety relocΣ); eauto.
intros. by apply binary_fundamental.
intros. by apply fundamental.
Qed.
Lemma logrel_simul Σ `{relocPreG Σ}
......
......@@ -72,6 +72,7 @@ Notation "'ref' τ" := (Tref τ%ty) (at level 10, τ at next level, right associ
(** * Typing judgements *)
Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
Reserved Notation "⊢ᵥ v : τ" (at level 20, v, τ at next level).
(* Shift all the indices in the context by one,
used when inserting a new type interpretation in Δ. *)
......@@ -100,60 +101,84 @@ Instance insert_binder (A : Type): Insert binder A (stringmap A) :=
binder_insert.
(** Typing itself *)
Inductive typed (Γ : stringmap type) : expr type Prop :=
| Var_typed x τ : Γ !! x = Some τ Γ Var x : τ
| Unit_typed : Γ #() : TUnit
| Nat_typed (n : nat) : Γ # n : TNat
| Bool_typed (b : bool) : Γ # b : TBool
| BinOp_typed_nat op e1 e2 τ :
Inductive typed : stringmap type expr type Prop :=
| Var_typed Γ x τ : Γ !! x = Some τ Γ Var x : τ
| Val_typed Γ v τ :
v : τ
Γ Val v : τ
| Unit_typed Γ : Γ #() : TUnit
| Nat_typed Γ (n : nat) : Γ # n : TNat
| Bool_typed Γ (b : bool) : Γ # b : TBool
| BinOp_typed_nat Γ op e1 e2 τ :
Γ e1 : TNat Γ e2 : TNat
binop_nat_res_type op = Some τ
Γ BinOp op e1 e2 : τ
| BinOp_typed_bool op e1 e2 τ :
| BinOp_typed_bool Γ op e1 e2 τ :
Γ e1 : TBool Γ e2 : TBool
binop_bool_res_type op = Some τ
Γ BinOp op e1 e2 : τ
| RefEq_typed e1 e2 τ :
| RefEq_typed Γ e1 e2 τ :
Γ e1 : Tref τ Γ e2 : Tref τ
Γ BinOp EqOp e1 e2 : TBool
| Pair_typed e1 e2 τ1 τ2 : Γ e1 : τ1 Γ e2 : τ2 Γ Pair e1 e2 : TProd τ1 τ2
| Fst_typed e τ1 τ2 : Γ e : TProd τ1 τ2 Γ Fst e : τ1
| Snd_typed e τ1 τ2 : Γ e : TProd τ1 τ2 Γ Snd e : τ2
| InjL_typed e τ1 τ2 : Γ e : τ1 Γ InjL e : TSum τ1 τ2
| InjR_typed e τ1 τ2 : Γ e : τ2 Γ InjR e : TSum τ1 τ2
| Case_typed e0 e1 e2 τ1 τ2 τ3 :
| Pair_typed Γ e1 e2 τ1 τ2 : Γ e1 : τ1 Γ e2 : τ2 Γ Pair e1 e2 : TProd τ1 τ2
| Fst_typed Γ e τ1 τ2 : Γ e : TProd τ1 τ2 Γ Fst e : τ1
| Snd_typed Γ e τ1 τ2 : Γ e : TProd τ1 τ2 Γ Snd e : τ2
| InjL_typed Γ e τ1 τ2 : Γ e : τ1 Γ InjL e : TSum τ1 τ2
| InjR_typed Γ e τ1 τ2 : Γ e : τ2 Γ InjR e : TSum τ1 τ2
| Case_typed Γ e0 e1 e2 τ1 τ2 τ3 :
Γ e0 : TSum τ1 τ2
Γ e1 : TArrow τ1 τ3
Γ e2 : TArrow τ2 τ3
Γ Case e0 e1 e2 : τ3
| If_typed e0 e1 e2 τ :
| If_typed Γ e0 e1 e2 τ :
Γ e0 : TBool Γ e1 : τ Γ e2 : τ Γ If e0 e1 e2 : τ
| Rec_typed f x e τ1 τ2 :
| Rec_typed Γ f x e τ1 τ2 :
<[f:=TArrow τ1 τ2]>(<[x:=τ1]>Γ) e : τ2
Γ Rec f x e : TArrow τ1 τ2
| App_typed e1 e2 τ1 τ2 :
| App_typed Γ e1 e2 τ1 τ2 :
Γ e1 : TArrow τ1 τ2 Γ e2 : τ1 Γ App e1 e2 : τ2
| TLam_typed e τ :
| TLam_typed Γ e τ :
Γ e : τ
Γ (Λ: e) : TForall τ
| TApp_typed e τ τ' : Γ e : TForall τ
| TApp_typed Γ e τ τ' : Γ e : TForall τ
Γ e #() : τ.[τ'/]
| TFold e τ : Γ e : τ.[TRec τ/] Γ e : TRec τ
| TUnfold e τ : Γ e : TRec τ Γ rec_unfold e : τ.[TRec τ/]
| TPack e τ τ' : Γ e : τ.[τ'/] Γ e : TExists τ
| TUnpack e1 x e2 τ τ2 :
| TFold Γ e τ : Γ e : τ.[TRec τ/] Γ e : TRec τ
| TUnfold Γ e τ : Γ e : TRec τ Γ rec_unfold e : τ.[TRec τ/]
| TPack Γ e τ τ' : Γ e : τ.[τ'/] Γ e : TExists τ
| TUnpack Γ e1 x e2 τ τ2 :
Γ e1 : TExists τ
<[x:=τ]>( Γ) e2 : (Autosubst_Classes.subst (ren (+1%nat)) τ2)
Γ (unpack: x := e1 in e2) : τ2
| TFork e : Γ e : TUnit Γ Fork e : TUnit
| TAlloc e τ : Γ e : τ Γ Alloc e : Tref τ
| TLoad e τ : Γ e : Tref τ Γ Load e : τ
| TStore e e' τ : Γ e : Tref τ Γ e' : τ Γ Store e e' : TUnit
| TCmpXchg e1 e2 e3 τ :
| TFork Γ e : Γ e : TUnit Γ Fork e : TUnit
| TAlloc Γ e τ : Γ e : τ Γ Alloc e : Tref τ
| TLoad Γ e τ : Γ e : Tref τ Γ Load e : τ
| TStore Γ e e' τ : Γ e : Tref τ Γ e' : τ Γ Store e e' : TUnit
| TCmpXchg Γ e1 e2 e3 τ :
EqType τ UnboxedType τ
Γ e1 : Tref τ Γ e2 : τ Γ e3 : τ
Γ CmpXchg e1 e2 e3 : TProd τ TBool
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).
with val_typed : val type Prop :=
| Unit_val_typed : #() : TUnit
| Nat_val_typed (n : nat) : #n : TNat
| Bool_val_typed (b : bool) : #b : TBool
| Pair_val_typed v1 v2 τ1 τ2 :
v1 : τ1
v2 : τ2
PairV v1 v2 : TProd τ1 τ2
| InjL_val_typed v τ1 τ2 :
v : τ1
InjLV v : TSum τ1 τ2
| InjR_val_typed v τ1 τ2 :
v : τ2
InjRV v : TSum τ1 τ2
| Rec_val_typed f x e τ1 τ2 :
<[f:=TArrow τ1 τ2]>(<[x:=τ1]>) e : τ2
RecV f x e : TArrow τ1 τ2
| TLam_val_typed e τ :
e : τ
(Λ: e) : TForall τ
where "Γ ⊢ₜ e : τ" := (typed Γ e τ)
and "⊢ᵥ e : τ" := (val_typed e τ).
Lemma binop_nat_typed_safe (op : bin_op) (n1 n2 : Z) τ :
binop_nat_res_type op = Some τ is_Some (bin_op_eval op #n1 #n2).
......
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