theorem
CC.typed_env_lookup_var
{a✝ : Sig}
{Γ : Ctx a✝}
{env : TypeEnv a✝}
{store : Memory}
{x : BVar a✝ Kind.var}
{T : Ty TySort.capt a✝}
(hts : EnvTyping Γ env store)
(hx : Γ.LookupVar x T)
:
Ty.capt_val_denot env T store (Exp.var (Var.free (env.lookup_var x)))
theorem
CC.shape_denot_with_var_reachability
{s : Sig}
{Γ : Ctx s}
{env : TypeEnv s}
{m : Memory}
{x : BVar s Kind.var}
{C : CaptureSet s}
{S : Ty TySort.shape s}
(hts : EnvTyping Γ env m)
(hd : Ty.shape_val_denot env S (CaptureSet.denot env C m) m (Exp.var (Var.free (env.lookup_var x))))
:
Ty.shape_val_denot env S (reachability_of_loc m.heap (env.lookup_var x)) m (Exp.var (Var.free (env.lookup_var x)))
theorem
CC.sem_typ_var
{a✝ : Sig}
{x : BVar a✝ Kind.var}
{Γ : Ctx a✝}
{S : Ty TySort.shape a✝}
{C : CaptureSet a✝}
(hx : Γ.LookupVar x (Ty.capt C S))
:
theorem
CC.sem_typ_abs
{s : Sig}
{T1 : Ty TySort.capt s}
{e : Exp (s,x)}
{Γ : Ctx s}
{T2 : Ty TySort.exi (s,x)}
{Cf : CaptureSet s}
(hclosed_abs : (Exp.abs Cf T1 e).IsClosed)
(ht : Cf.rename Rename.succ ∪ CaptureSet.var (Var.bound BVar.here) # Γ,x:T1 ⊨ e : T2)
:
theorem
CC.sem_typ_pack
{s : Sig}
{T : Ty TySort.capt (s,C)}
{cs : CaptureSet s}
{x : Var Kind.var s}
{Γ : Ctx s}
(hclosed_e : (Exp.pack cs x).IsClosed)
(ht : CaptureSet.var x # Γ ⊨ Exp.var x : (T.subst (Subst.openCVar cs)).typ)
:
theorem
CC.abs_val_denot_inv
{a✝ : Sig}
{env : TypeEnv a✝}
{T1 : Ty TySort.capt a✝}
{T2 : Ty TySort.exi (a✝,x)}
{store : Memory}
{x : Var Kind.var ∅}
{A : CapabilitySet}
(hv : Ty.shape_val_denot env (T1.arrow T2) A store (Exp.var x))
:
∃ (fx : ℕ),
x = Var.free fx ∧ ∃ (cs : CaptureSet ∅) (T0 : Ty TySort.capt ∅) (e0 : Exp (∅,x)) (hval : (Exp.abs cs T0 e0).IsSimpleVal) (R :
CapabilitySet),
store.heap fx = some (Cell.val { unwrap := Exp.abs cs T0 e0, isVal := hval, reachability := R }) ∧ expand_captures store.heap cs ⊆ A ∧ ∀ (arg : ℕ) (m' : Memory),
m'.subsumes store →
Ty.capt_val_denot env T1 m' (Exp.var (Var.free arg)) →
Ty.exi_exp_denot (env.extend_var arg) T2
(expand_captures store.heap cs ∪ reachability_of_loc m'.heap arg) m'
(e0.subst (Subst.openVar (Var.free arg)))
theorem
CC.tabs_val_denot_inv
{a✝ : Sig}
{env : TypeEnv a✝}
{S : Ty TySort.shape a✝}
{T : Ty TySort.exi (a✝,X)}
{store : Memory}
{x : Var Kind.var ∅}
{A : CapabilitySet}
(hv : Ty.shape_val_denot env (S.poly T) A store (Exp.var x))
:
∃ (fx : ℕ),
x = Var.free fx ∧ ∃ (cs : CaptureSet ∅) (S0 : Ty TySort.shape ∅) (e0 : Exp (∅,X)) (hval : (Exp.tabs cs S0 e0).IsSimpleVal) (R :
CapabilitySet),
store.heap fx = some (Cell.val { unwrap := Exp.tabs cs S0 e0, isVal := hval, reachability := R }) ∧ expand_captures store.heap cs ⊆ A ∧ ∀ (m' : Memory) (denot : PreDenot),
m'.subsumes store →
denot.is_proper →
denot.ImplyAfter m' (Ty.shape_val_denot env S) →
Ty.exi_exp_denot (env.extend_tvar denot) T (expand_captures store.heap cs) m'
(e0.subst (Subst.openTVar Ty.top))
theorem
CC.cabs_val_denot_inv
{a✝ : Sig}
{env : TypeEnv a✝}
{B : CaptureBound a✝}
{T : Ty TySort.exi (a✝,C)}
{store : Memory}
{x : Var Kind.var ∅}
{A : CapabilitySet}
(hv : Ty.shape_val_denot env (Ty.cpoly B T) A store (Exp.var x))
:
∃ (fx : ℕ),
x = Var.free fx ∧ ∃ (cs : CaptureSet ∅) (B0 : CaptureBound ∅) (e0 : Exp (∅,C)) (hval : (Exp.cabs cs B0 e0).IsSimpleVal) (R :
CapabilitySet),
store.heap fx = some (Cell.val { unwrap := Exp.cabs cs B0 e0, isVal := hval, reachability := R }) ∧ expand_captures store.heap cs ⊆ A ∧ ∀ (m' : Memory) (CS : CaptureSet ∅),
CS.WfInHeap m'.heap →
m'.subsumes store →
(CaptureSet.denot TypeEnv.empty CS m').BoundedBy (CaptureBound.denot env B m') →
Ty.exi_exp_denot (env.extend_cvar CS) T (expand_captures store.heap cs) m'
(e0.subst (Subst.openCVar CS))
theorem
CC.cap_val_denot_inv
{a✝ : Sig}
{env : TypeEnv a✝}
{store : Memory}
{x : Var Kind.var ∅}
{A : CapabilitySet}
(hv : Ty.shape_val_denot env Ty.cap A store (Exp.var x))
:
theorem
CC.unit_val_denot_inv
{a✝ : Sig}
{env : TypeEnv a✝}
{A : CapabilitySet}
{store : Memory}
{x : Var Kind.var ∅}
(hv : Ty.shape_val_denot env Ty.unit A store (Exp.var x))
:
theorem
CC.cell_val_denot_inv
{a✝ : Sig}
{env : TypeEnv a✝}
{store : Memory}
{x : Var Kind.var ∅}
{A : CapabilitySet}
(hv : Ty.shape_val_denot env Ty.cell A store (Exp.var x))
:
theorem
CC.bool_val_denot_inv
{a✝ : Sig}
{env : TypeEnv a✝}
{A : CapabilitySet}
{store : Memory}
{x : Var Kind.var ∅}
(hv : Ty.shape_val_denot env Ty.bool A store (Exp.var x))
:
theorem
CC.var_exp_denot_inv
{a✝ : Sig}
{env : TypeEnv a✝}
{T : Ty TySort.exi a✝}
{store : Memory}
{x : Var Kind.var ∅}
{A : CapabilitySet}
(hv : Ty.exi_exp_denot env T A store (Exp.var x))
:
Ty.exi_val_denot env T store (Exp.var x)
theorem
CC.closed_captureset_subst_denot
{s : Sig}
{env : TypeEnv s}
{D : CaptureSet s}
(hD_closed : D.IsClosed)
:
For closed capture sets, the denotation is preserved under substitution with from_TypeEnv, provided the environment satisfies the cvar invariant.
theorem
CC.sem_typ_tapp
{s : Sig}
{Γ : Ctx s}
{x : BVar s Kind.var}
{S : Ty TySort.shape s}
{T : Ty TySort.exi (s,X)}
(hx :
CaptureSet.var (Var.bound x) # Γ ⊨ Exp.var (Var.bound x) : (Ty.capt (CaptureSet.var (Var.bound x)) (S.poly T)).typ)
:
theorem
CC.sem_typ_capp
{s : Sig}
{Γ : Ctx s}
{x : BVar s Kind.var}
{T : Ty TySort.exi (s,C)}
{D : CaptureSet s}
(hD_closed : D.IsClosed)
(hx :
CaptureSet.var (Var.bound x) # Γ ⊨ Exp.var (Var.bound x) : (Ty.capt (CaptureSet.var (Var.bound x)) (Ty.cpoly (CaptureBound.bound D) T)).typ)
:
theorem
CC.sem_typ_app
{s : Sig}
{Γ : Ctx s}
{T1 : Ty TySort.capt s}
{T2 : Ty TySort.exi (s,x)}
{x y : BVar s Kind.var}
(hx :
CaptureSet.var (Var.bound x) # Γ ⊨ Exp.var (Var.bound x) : (Ty.capt (CaptureSet.var (Var.bound x)) (T1.arrow T2)).typ)
(hy : CaptureSet.var (Var.bound y) # Γ ⊨ Exp.var (Var.bound y) : T1.typ)
:
CaptureSet.var (Var.bound x) ∪ CaptureSet.var (Var.bound y) # Γ ⊨ Exp.app (Var.bound x) (Var.bound y) : T2.subst (Subst.openVar (Var.bound y))
theorem
CC.sem_typ_invoke
{s : Sig}
{Γ : Ctx s}
{x y : BVar s Kind.var}
(hx : CaptureSet.var (Var.bound x) # Γ ⊨ Exp.var (Var.bound x) : (Ty.capt (CaptureSet.var (Var.bound x)) Ty.cap).typ)
(hy : CaptureSet.var (Var.bound y) # Γ ⊨ Exp.var (Var.bound y) : (Ty.capt (CaptureSet.var (Var.bound y)) Ty.unit).typ)
:
theorem
CC.sem_typ_cond
{s : Sig}
{C1 C2 C3 : CaptureSet s}
{Γ : Ctx s}
{x : Var Kind.var s}
{e2 e3 : Exp s}
{T : Ty TySort.exi s}
{Cb : CaptureSet s}
(hclosed_C1 : C1.IsClosed)
(hclosed_C2 : C2.IsClosed)
(hclosed_C3 : C3.IsClosed)
(_hclosed_guard : x.IsClosed)
(_hclosed_then : e2.IsClosed)
(_hclosed_else : e3.IsClosed)
(ht1 : C1 # Γ ⊨ Exp.var x : (Ty.capt Cb Ty.bool).typ)
(ht2 : C2 # Γ ⊨ e2 : T)
(ht3 : C3 # Γ ⊨ e3 : T)
:
theorem
CC.sem_typ_letin
{s : Sig}
{C : CaptureSet s}
{Γ : Ctx s}
{e1 : Exp s}
{T : Ty TySort.capt s}
{e2 : Exp (s,,Kind.var)}
{U : Ty TySort.exi s}
(hclosed_C : C.IsClosed)
(_hclosed_e : (e1.letin e2).IsClosed)
(ht1 : C # Γ ⊨ e1 : T.typ)
(ht2 : C.rename Rename.succ # Γ,x:T ⊨ e2 : U.rename Rename.succ)
:
theorem
CC.sem_sc_trans
{a✝ : Sig}
{Γ : Ctx a✝}
{C1 C2 C3 : CaptureSet a✝}
(hsub1 : SemSubcapt Γ C1 C2)
(hsub2 : SemSubcapt Γ C2 C3)
:
SemSubcapt Γ C1 C3
theorem
CC.sem_sc_elem
{s : Sig}
{Γ : Ctx s}
{C1 C2 : CaptureSet s}
(hmem : C1 ⊆ C2)
:
SemSubcapt Γ C1 C2
theorem
CC.sem_sc_union
{s : Sig}
{Γ : Ctx s}
{C1 C2 C3 : CaptureSet s}
(hsub1 : SemSubcapt Γ C1 C3)
(hsub2 : SemSubcapt Γ C2 C3)
:
SemSubcapt Γ (C1.union C2) C3
theorem
CC.typed_env_lookup_cvar_aux
{a✝ : Sig}
{Γ : Ctx a✝}
{env : TypeEnv a✝}
{m : Memory}
{c : BVar a✝ Kind.cvar}
{cb : CaptureBound a✝}
(hts : EnvTyping Γ env m)
(hc : Γ.LookupCVar c cb)
:
((env.lookup_cvar c).ground_denot m).BoundedBy (CaptureBound.denot env cb m)
theorem
CC.typed_env_lookup_cvar
{a✝ : Sig}
{Γ : Ctx a✝}
{env : TypeEnv a✝}
{m : Memory}
{c : BVar a✝ Kind.cvar}
{C : CaptureSet a✝}
(hts : EnvTyping Γ env m)
(hc : Γ.LookupCVar c (CaptureBound.bound C))
:
theorem
CC.sem_sc_var
{s : Sig}
{Γ : Ctx s}
{x : BVar s Kind.var}
{C : CaptureSet s}
{S : Ty TySort.shape s}
(hlookup : Γ.LookupVar x (Ty.capt C S))
:
SemSubcapt Γ (CaptureSet.var (Var.bound x)) C
theorem
CC.sem_sc_cvar
{s : Sig}
{Γ : Ctx s}
{c : BVar s Kind.cvar}
{C : CaptureSet s}
(hlookup : Γ.LookupCVar c (CaptureBound.bound C))
:
SemSubcapt Γ (CaptureSet.cvar c) C
theorem
CC.fundamental_subcapt
{a✝ : Sig}
{Γ : Ctx a✝}
{C1 C2 : CaptureSet a✝}
(hsub : Subcapt Γ C1 C2)
:
SemSubcapt Γ C1 C2
theorem
CC.env_typing_lookup_tvar
{s : Sig}
{Γ : Ctx s}
{X : BVar s Kind.tvar}
{S : Ty TySort.shape s}
{env : TypeEnv s}
{m : Memory}
(hlookup : Γ.LookupTVar X S)
(htyping : EnvTyping Γ env m)
:
(env.lookup_tvar X).ImplyAfter m (Ty.shape_val_denot env S)
theorem
CC.sem_subtyp_tvar
{s : Sig}
{Γ : Ctx s}
{X : BVar s Kind.tvar}
{S : Ty TySort.shape s}
(hlookup : Γ.LookupTVar X S)
:
theorem
CC.pre_denot_imply_after_monotonic
{pd1 pd2 : PreDenot}
{H m : Memory}
(himply : pd1.ImplyAfter H pd2)
(hsub : m.subsumes H)
:
pd1.ImplyAfter m pd2
theorem
CC.sem_subtyp_arrow
{s : Sig}
{Γ : Ctx s}
{T1 T2 : Ty TySort.capt s}
{U1 U2 : Ty TySort.exi (s,x)}
(harg : SemSubtyp Γ T2 T1)
(hres : SemSubtyp (Γ,x:T2) U1 U2)
:
Equations
- CC.SemSubbound Γ B1 B2 = ∀ (env : CC.TypeEnv s) (m : CC.Memory), CC.EnvTyping Γ env m → CC.CaptureBound.denot env B1 m ⊆ CC.CaptureBound.denot env B2 m
Instances For
theorem
CC.fundamental_subbound
{a✝ : Sig}
{Γ : Ctx a✝}
{B1 B2 : CaptureBound a✝}
(hsub : Subbound Γ B1 B2)
:
SemSubbound Γ B1 B2
theorem
CC.sem_subtyp_cpoly
{s : Sig}
{Γ : Ctx s}
{cb1 cb2 : CaptureBound s}
{T1 T2 : Ty TySort.exi (s,C)}
(hB : SemSubbound Γ cb1 cb2)
(hT : SemSubtyp (Γ,C<:cb1) T1 T2)
(hclosed_cb1 : cb1.IsClosed)
:
theorem
CC.sem_subtyp_capt
{s : Sig}
{Γ : Ctx s}
{C1 C2 : CaptureSet s}
{S1 S2 : Ty TySort.shape s}
(hC : SemSubcapt Γ C1 C2)
(hS : SemSubtyp Γ S1 S2)
(hclosed_C2 : C2.IsClosed)
:
theorem
CC.sem_subtyp_exi
{s : Sig}
{Γ : Ctx s}
{T1 T2 : Ty TySort.capt (s,C)}
(hT : SemSubtyp (Γ,C<:CaptureBound.unbound) T1 T2)
:
theorem
CC.sem_subtyp_typ
{s : Sig}
{Γ : Ctx s}
{T1 T2 : Ty TySort.capt s}
(hT : SemSubtyp Γ T1 T2)
:
theorem
CC.sem_subtyp_poly
{s : Sig}
{Γ : Ctx s}
{S1 S2 : Ty TySort.shape s}
{T1 T2 : Ty TySort.exi (s,X)}
(hS : SemSubtyp Γ S2 S1)
(hT : SemSubtyp (Γ,X<:S2) T1 T2)
:
theorem
CC.sem_typ_unpack
{s : Sig}
{C : CaptureSet s}
{Γ : Ctx s}
{t : Exp s}
{T : Ty TySort.capt (s,C)}
{u : Exp (s,C,x)}
{U : Ty TySort.exi s}
(hclosed_C : C.IsClosed)
(ht : C # Γ ⊨ t : T.exi)
(hu :
(C.rename Rename.succ).rename Rename.succ # Γ,C<:CaptureBound.unbound,x:T ⊨ u : (U.rename Rename.succ).rename Rename.succ)
:
theorem
CC.fundamental
{a✝ : Sig}
{C : CaptureSet a✝}
{Γ : Ctx a✝}
{e : Exp a✝}
{T : Ty TySort.exi a✝}
(ht : C # Γ ⊢ e : T)
:
The fundamental theorem of semantic type soundness.