Set Implicit Arguments.
Require Import MyTactics.
Require Import Layers.
Require Import Types.
Require Import TypeContexts.
Require Import FocusPaths.
Require Import TypeEquality.
Require Import MoreTypeEquality.
Require Import Store.
Require Import Programs.
Require Import ValueLists.
Require Import Coercions.
Require Import Environments.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import Subtyping.
Require Import Resources.
Require Import ResourcesContinued.
Require Import Erasure.
Require Import AntiFrameSwitch.
The typing judgement.
Inductive jv :
resource ->
menv ->
env ->
value ->
ty ->
Prop :=
|
JVVar:
forall R M E x m T,
jenv M x m ->
nonzero m ->
jenv E x T ->
wf T ->
jv R M E (
VVar x)
T
|
JVAbs:
forall R M E t T1 T2,
jt R (
M;;
MOne) (
E;;
T1)
t T2 ->
wf T1 ->
jv R M E (
VAbs t) (
TyArrow T1 T2)
|
JVPair:
forall R1 R2 R M1 M2 M E v1 v2 layer1 layer2 T1 T2,
star R1 R2 R ->
star M1 M2 M ->
jv R1 M1 E v1 T1 ->
jv R2 M2 E v2 T2 ->
jv R M E (
VPair layer1 layer2 v1 v2) (
TyPair layer1 layer2 T1 T2)
|
JVUnit:
forall R M E layer,
jv R M E (
VUnit layer) (
TyUnit layer)
|
JVTyAbs:
forall R M E v T,
jv R M (
E!)
v T ->
jv R M E (
VTyAbs v) (
TyForall T)
|
JVPack:
forall R M E v U T,
jv R M E v (
subst_ty U 0
T) ->
wf T ->
wf U ->
jv R M E (
VPack v) (
TyExists T)
|
JVCoApp:
forall R M E c v T U,
jv R M E v T ->
jco nil c (
T -->
U) ->
cwf c ->
jv R M E (
VCoApp c v)
U
|
JVBang:
forall R M E v T,
jv (
neutral R) (
neutral M)
E v T ->
jv R M E (
VBang v) (
TyBang T)
|
JVAtRegion:
forall R M E v r,
r <
reglimit R ->
region_map R r (
erase_value v) ->
closed_value v ->
jv R M E (
VInhabitant v) (
TyAt (
TyRegion r))
|
JVRegionCap:
forall rk R1 R M E r R2 vs T,
The region r must exist.
r <
reglimit R ->
The list vs must contain all inhabitants of the region. This ensures
that R2, which is large enough to typecheck vs, is large enough to
typecheck all inhabitants.
(
forall rv,
region_map R r rv ->
some (
fun v =>
erase_value v =
rv)
vs) ->
Conversely, every element of vs must be an inhabitant of the region.
This should be required, at least, for singleton regions, where vs
is a singleton list, and we wish to guarantee that its unique element
is indeed an inhabitant of the region. Here, we require it for group
regions as well.
(
forall v,
member v vs ->
region_map R r (
erase_value v)) ->
The resource R is split between a residue R1 and a part R2 that
serves to typecheck the inhabitants.
star R1 R2 R ->
Every inhabitant must have type T.
ji R2 vs T ->
The residue R1 must guarantee the ownership of the region r. If
there is more, it is ignored: this is again an affine typing rule.
permission_map R1 r =
Some tt ->
If this a singleton region, then vs should be a singleton list.
(
rk =
Singleton ->
count vs = 1) ->
That's it!
jv R M E (
VRegionCap vs) (
TyRegionCap rk (
TyRegion r)
T)
|
JVRegionCapPunched:
forall R1 R M E r1 r2 R2 w vs T,
The regions r1 and r2 must exist.
r1 <
reglimit R ->
r2 <
reglimit R ->
The list VCons w vs must contain all inhabitants of the region r1.
(
forall rv,
region_map R r1 rv ->
some (
fun v =>
erase_value v =
rv) (
VCons w vs)) ->
Conversely, every element of VCons w vs must be an inhabitant of r1.
(
forall v,
member v (
VCons w vs) ->
region_map R r1 (
erase_value v)) ->
The resource R is split between a residue R1 and a part R2 that
serves to typecheck the inhabitants.
star R1 R2 R ->
Every inhabitant must have type T. This does not include w.
ji R2 vs T ->
The value w must be an inhabitant of region r2.
region_map R r2 (
erase_value w) ->
closed_value w ->
The residue R1 must guarantee the ownership of the region r1.
permission_map R1 r1 =
Some tt ->
That's it!
jv R M E (
VRegionCapPunched vs) (
TyRegionCapPunched (
TyRegion r1)
T (
TyRegion r2))
|
JVLoc:
forall R1 R2 R M E l v T,
The location l must exist.
l <
reflimit R ->
The resource R is split between a part R1 that represents the
ownership of the reference and a part R2 that serves to typecheck
the content of the reference.
star R1 R2 R ->
The value must have type T.
jv R2 nil nil v T ->
R1 must guarantee the ownership of the region r. Furthermore,
the erasure of the value v must coincide with the contents of the
reference.
location_map R1 l =
Some (
erase_value v) ->
That's it!
jv R M E (
VLoc l v) (
TyRef T)
|
JVEq:
forall R M E v T1 T2,
jv R M E v T1 ->
tyeq T1 T2 ->
wf T2 ->
jv R M E v T2
with ji :
resource ->
values ->
ty ->
Prop :=
|
JINil:
forall R T,
wf T ->
ji R VNil T
|
JICons:
forall R1 R2 R v vs T,
jv R1 nil nil v T ->
ji R2 vs T ->
star R1 R2 R ->
ji R (
VCons v vs)
T
with jt :
resource ->
menv ->
env ->
term ->
ty ->
Prop :=
|
JTVal:
forall R M E v T,
jv R M E v T ->
jt R M E (
TVal v)
T
|
JTApp:
forall R1 R2 R M1 M2 M E v t T1 T2,
star R1 R2 R ->
star M1 M2 M ->
jv R1 M1 E v (
TyArrow T1 T2) ->
jt R2 M2 E t T1 ->
jt R M E (
TApp v t)
T2
|
JTMixPair:
forall R1 R2 R M1 M2 M E t1 v2 T1 T2,
star R1 R2 R ->
star M1 M2 M ->
jt R1 M1 E t1 T1 ->
jv R2 M2 E v2 T2 ->
jt R M E (
TMixPair t1 v2) (
TyMixPair T1 T2)
|
JTTyAbs:
forall R M E t T,
anti_frame_disabled ->
jt R M (
E!)
t T ->
jt R M E (
TTyAbs t) (
TyForall T)
|
JTCoApp:
forall R M E c t T U,
jt R M E t T ->
jco nil c (
T -->
U) ->
cwf c ->
jt R M E (
TCoApp c t)
U
|
JTLetUnpack:
forall R1 R2 R M1 M2 M E v t T1 T2,
star R1 R2 R ->
star M1 M2 M ->
jv R1 M1 E v (
TyExists T1) ->
jt R2 (
M2;;
MOne) (
E!;;
T1)
t (
lift_ty 0
T2) ->
jt R M E (
TLetUnpack v t)
T2
|
JTLetBang:
forall R1 R2 R M1 M2 M E v t T1 T2,
star R1 R2 R ->
star M1 M2 M ->
jv R1 M1 E v (
TyBang T1) ->
jt R2 (
M2;;
MInfinity) (
E;;
T1)
t T2 ->
jt R M E (
TLetBang v t)
T2
|
JTLetPair:
forall R1 R2 R M1 M2 M E v t layer1 layer2 T1 T2 U,
star R1 R2 R ->
star M1 M2 M ->
jv R1 M1 E v (
TyPair layer1 layer2 T1 T2) ->
jt R2 (
M2;;
MOne;;
MOne) (
E;;
T1;;
T2)
t U ->
jt R M E (
TLetPair layer1 layer2 v t)
U
|
JTPrimApp:
forall R M E p v T1 T2,
jv R M E v T1 ->
jp p T1 T2 ->
jt R M E (
TPrimApp p v)
T2
|
JTHide:
forall R1 R2 R M E v t T1 T2 U,
anti_frame_enabled ->
jv R1 M E v T1 ->
jt R2 (
nil;;
MOne) (
nil;;
TyTensor T1 U)
t (
TyCompos T2 U) ->
star R1 R2 R ->
wf T1 ->
wf T2 ->
wf U ->
jt R M E (
THide v t)
T2
|
JTEq:
forall R M E t T1 T2,
jt R M E t T1 ->
tyeq T1 T2 ->
wf T2 ->
jt R M E t T2
with jp :
primitive ->
ty ->
ty ->
Prop :=
|
JPDefocusDuplicable:
forall rk sigma T TC pi,
jpath pi TC ->
wf sigma ->
wf T ->
jp (
PDefocusDuplicable pi)
(
TyMixPair (
fill TC (
TyAt sigma)) (
TyRegionCap rk sigma (
TyBang T)))
(
TyMixPair (
fill TC (
TyBang T)) (
TyRegionCap rk sigma (
TyBang T)))
|
JPFocus:
forall T TC pi,
jpath pi TC ->
wf T ->
jp
(
PFocus pi)
(
fill TC T)
(
TyExists (
TyMixPair (
fill (
lift_ty_ctx 0
TC) (
TyAt (
TyVar 0)))
(
TyRegionCap Singleton (
TyVar 0) (
lift_ty 0
T))))
|
JPNewGroup:
forall T,
wf T ->
jp PNewGroup
TyPhyUnit
(
TyExists (
TyMixPair TyPhyUnit (
TyRegionCap Group (
TyVar 0)
T)))
|
JPAdopt:
forall sigma T,
wf sigma ->
wf T ->
jp PAdopt
(
TyMixPair T (
TyRegionCap Group sigma T))
(
TyMixPair (
TyAt sigma) (
TyRegionCap Group sigma T))
|
JPFocusGroup:
forall rho T,
wf rho ->
wf T ->
jp PFocusGroup
(
TyMixPair (
TyAt rho)
(
TyRegionCap Group rho T))
(
TyExists (
TyMixPair (
TyAt (
TyVar 0))
(
TyLogPair (
TyRegionCap Singleton (
TyVar 0) (
lift_ty 0
T))
(
TyRegionCapPunched (
lift_ty 0
rho) (
lift_ty 0
T) (
TyVar 0)))))
|
JPNewAffine:
forall T,
wf T ->
jp PNewAffine T (
TyRef T)
|
JPReadAffine:
forall T,
wf T ->
jp PReadAffine (
TyRef (
TyBang T)) (
TyPhyPair (
TyBang T) (
TyRef (
TyBang T)))
|
JPWriteAffine:
forall T1 T2,
wf T1 ->
wf T2 ->
jp PWriteAffine (
TyPhyPair (
TyRef T1)
T2) (
TyRef T2)
|
JPNewCap:
forall T,
wf T ->
jp PNewCap
T
(
TyExists (
TyMixPair (
TyAt (
TyVar 0)) (
TyRegionCap Singleton (
TyVar 0) (
TyRef (
lift_ty 0
T)))))
|
JPReadCap:
forall sigma T,
wf sigma ->
wf T ->
jp PReadCap
(
TyMixPair (
TyAt sigma) (
TyRegionCap Singleton sigma (
TyRef (
TyBang T))))
(
TyMixPair (
TyBang T) (
TyRegionCap Singleton sigma (
TyRef (
TyBang T))))
|
JPWriteCap:
forall sigma T1 T2,
wf sigma ->
wf T1 ->
wf T2 ->
jp PWriteCap
(
TyMixPair (
TyPhyPair (
TyAt sigma)
T2) (
TyRegionCap Singleton sigma (
TyRef T1)))
(
TyMixPair TyPhyUnit (
TyRegionCap Singleton sigma (
TyRef T2)))
.
Hint Constructors jv ji jt jp.
Construct an appropriate mutual induction scheme.
Scheme jvit_ind_v :=
Induction for jv Sort Prop
with jvit_ind_i :=
Induction for ji Sort Prop
with jvit_ind_t :=
Induction for jt Sort Prop.
Combined Scheme jvit_ind from jvit_ind_v,
jvit_ind_i,
jvit_ind_t.
A typing judgement for stores.
Definition jsto (
R :
resource) (
s :
store) :
Prop :=
let (
limit,
m) :=
erase_store s in
limit =
reflimit R /\
forall l,
l <
limit ->
m l =
location_map R l.
A typing judgement for configurations.
At the toplevel of a configuration, we allow any number of active hide
constructs. In other words, we consider that the configuration has type T
is the term has type composs T Us for some list of hidden invariants Us.
We make T a parameter of the jconf judgement, and following the above
comment, consider that the configuration has type T if the term t has
type composs T Us for some Us. However, there is not much to be gained
by making T a parameter of the judgement. The only apparent gain is a
slightly more precise subject reduction statement for configurations, which
states that reduction of configurations preserves T. One could also choose
not to make T a parameter of this judgement. One would then allow t to
have an arbitrary type.
Inductive jconf (
s :
store) (
t :
term) (
T :
ty) :
Prop :=
|
JConfCons:
forall R Us,
jsto R s ->
jt R nil nil t (
composs T Us) ->
wfs Us ->
jconf s t T.
Hint Constructors jconf.
The tactic jveq_forward equality looks for a typing judgement among the
current hypotheses and modifies it by applying JVEq. The type equality
is proved via the tactic equality.
Ltac jveq_forward equality :=
let U :=
fresh "
U"
in
evar (
U :
ty);
match goal with j:
jv ?
R ?
M ?
E ?
v ?
T |-
_ =>
assert (
jv R M E v U);
unfold U in *;
clear U; [
eapply JVEq; [
eexact j |
instantiate;
equality |
wf ] |
clear j ]
end.
The tactic jveq equality modifies the goal by applying JVEq. The type
equality is first reversed, then proved via the tactic equality.
Ltac jveq equality :=
eapply JVEq; [
idtac |
eapply tyeq_symmetric;
equality |
wf ].