rules.ott

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Entailment  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
Qs :: '' ::=


defn
QF1 ||- QF2 :: :: Qrules :: 'Q_' {{ com Concrete constraint entailment }}
by

(UCtx1, LCtx1) ||- (UCtx2, LCtx2)
q \notin Dup
------------------------------------------:: Linear
(UCtx1, LCtx1 \u q) ||- (UCtx2, LCtx2 \u q)

(UCtx1, LCtx1 \u q) ||- (UCtx2, LCtx2)
q \in Dup
------------------------------------------:: DupOne
(UCtx1, LCtx1 \u q) ||- (UCtx2, LCtx2 \u q)

(UCtx1, LCtx1) ||- (UCtx2, LCtx2)
q \notin LCtx2
q \in Dup
------------------------------------------:: DupNone
(UCtx1, LCtx1 \u q) ||- (UCtx2, LCtx2)

UCtx1 \subseteq UCtx2
---------------------------------------:: Ur
(UCtx1, emptyset) ||- (UCtx2, emptyset)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Entailment  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
Entail :: '' ::=

defn
QF |- CF :: :: Crules :: 'C_'  {{ com Generalised constraint entailment }}
by

Q1 ||- Q2 \\\\
Q2 |- C
--------- :: Dom
Q1 |- C

--------- :: Id
Q |- Q

Q1 |- C1
Q2 |- C2
-------------- :: Tensor
Q1*Q2 |- C1*C2

Q |- C1
Q |- C2
------------- :: With
Q |- C1 & C2

Q0*Q1 |- C
------------- :: Impl
pi. Q0 |- pi.(Q1 => C)

------------- :: Top
Q |- Top


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Typing rules  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
Ty :: '' ::=

defn
QF ; G |- e : t :: :: Ty :: 'E_' {{ com Expression typing }}
by

G1 = x :_1 forall as. Q1 =o u
--------------------------- :: Var
Q1[ts/as];G1+omega.G2 |- x : u[ts/as]

Q;G, x:_pi t1 |- e : t2
---------------------- :: Abs
Q;G |- \x.e : t1 ->_pi t2

Q1;G1 |- e1 : t1 ->_pi t
Q2; G2 |- e2 : t1
------------------------------ :: App
Q1*pi.Q2;G1+pi.G2 |- e1 e2 : t

Q ; G |- e : t[us/as]
------------------------- :: Pack
Q * Q1[us/as];G |- pack e : exists as. t o= Q1

Q1;G1 |- e1 : exists as. t1 o= Q
as fresh
Q2 * Q;G2,x:_1 t1 |- e2 : t
------------------------------------------------- :: Unpack
Q1 * Q2;G1 + G2 |- unpack x = e1 in e2 : t

Q1*Q;G1 |- e1 : t1
Q2;G2,x:_pi Q =o t1 |- e2 : t
--------------------------- :: Let
pi.Q1*Q2 ;pi.G1+G2 |- let_pi x = e1 in e2 : t

Q1*Q;G1 |- e1 : t1
as fresh
s = forall as.Q =o t1
Q2;G2,x:_pi forall as.Q =o t1 |- e2 : t
--------------------------- :: LetSig
pi.Q1 * Q2 ;pi.G1+G2 |- let_pi x : s = e1 in e2 : t

Q1;G1 |- e : T ts
Ki : forall as. usi ->_pisi T as
Q2; G2, < xi :_(pi.pii) ui[ts/as] > |- ei : t
------------------------- :: Case
pi.Q1*Q2;pi.G1+G2 |- case_pi e of { alts } : t

Q1;G |- e : t
Q ||- Q1
------------------------- :: Sub
Q;G |- e : t

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Constraint generation  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
Gen :: '' ::=

defn
G |-> e : t ~> CF :: :: Gen :: 'G_' {{ com Constraint generation }}
by

G1 = x :_1 forall as. Q =o u
------------------------------ :: Var
G1 + omega.G2 |-> x : u[ts/as] ~> Q[ts/as]

G, x:_pi t0 |-> e : t ~> C
------------------------------ :: Abs
G |-> \x. e : t0 ->_pi t ~> C

G1 |-> e1 : t2 ->_pi t ~> C1
G2 |-> e2 : t2 ~> C2
------------------------------ :: App
G1 + pi.G2 |-> e1 e2 : t ~> C1 * pi.C2

G |-> e : T ss ~> C
Ki : forall as. usi ->_pisi T as
D, <xi:_(pi.pii) ui[ss/as]> |-> ei : t ~> Ci
------------------------------ :: Case
pi.G + D |-> case_pi e of {alts} : t ~> pi.C * && Ci

G1 |-> e1 : exists as. t1 o= Q1 ~> C1
as fresh
G2, x:_1 t1 |-> e2 : t ~> C2
------------------------------ :: Unpack
G1+G2 |-> unpack x = e1 in e2 : t ~> C1 * 1.(Q1 => C2)

G |-> e : t[us/as] ~> C
------------------------------ :: Pack
G |-> pack e : exists as. t o= Q ~> C * Q[us/as]


G1 |-> e1 : t1 ~> C1
G2, x:_pi t1 |-> e2 : t ~> C2
------------------------------ :: Let
pi.G1+G2 |-> let_pi x = e1 in e2 : t ~> pi.C1 * C2

G1 |-> e1 : t1 ~> C1
Q_r * Q |- C1
G2, x:_pi Q =o t1 |-> e2 : t ~> C2
------------------------------ :: LetGen
pi.G1+G2 |-> let_pi x = e1 in e2 : t ~> pi.Q_r * C2

G1 |-> e1 : t1 ~> C1
as fresh
G2, x:_pi forall as. Q =o t1 |-> e2 : t ~> C2
------------------------------ :: LetSig
pi.G1+G2 |-> let_pi x : forall as. Q =o t1 = e1 in e2 : t ~> C2 * pi.(Q => C1)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Constraint solver  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
Solve :: '' ::=

defn
|-s CF_w ~> QF :: :: Solve :: 'S_' {{ com Constraint solving }}
by

---------------------------------------------- :: Atom
|-s pi.q ~> pi.q

|-s C1 ~> Q1  |-s C2 ~> Q2
--------------------------------------------------------------- :: With
|-s C1 & C2 ~> Q1 /\ Q2

|-s C1 ~> Q1  |-s C2 ~> Q2
------------------------------------------------------------- :: Tensor
|-s C1 * C2 ~> Q1 * Q2

|-s C ~> Q_i
|-d Q_i \d Q_b ~> Q_o
---------------------------------------------- :: Impl
|-s pi . (Q_b => C) ~> pi . Q_o

defn
|-d QF1 \d QF2 ~> QF3 :: :: CheckMult :: 'D_' {{ com Constraint bounding }}
by

q \notin Dup
q \notin LCtx_b
q \notin UCtx_b
q \notin Q_o
|-d Q_i \d (UCtx_b, LCtx_b) ~> Q_o * 1.q
------------------------------------ :: Linear
|-d Q_i \d (UCtx_b, LCtx_b \u q) ~> Q_o

q \in Dup
q \notin LCtx_b
q \notin UCtx_b
q \notin Q_o
|-d Q_i \d (UCtx_b, LCtx_b) ~> Q_o * many 1.q
------------------------------------ :: Dup
|-d Q_i \d (UCtx_b, LCtx_b \u q) ~> Q_o

q \notin LCtx_b
q \notin UCtx_b
q \notin Q_o
|-d Q_i \d (UCtx_b, LCtx_b) ~> Q_o * pi_1.q * .. * pi_n.q
------------------------------------ :: Ur
|-d Q_i \d (UCtx_b \u q, LCtx_b) ~> Q_o

defn
QF1 /\ QF2 = QF3 :: :: QInf :: 'Inf_' {{ com Constraint meet }}
by

------------------------------------------------------------------- :: Ur
(UCtx1, emptyset) /\ (UCtx2, emptyset) = (UCtx1 \u UCtx2, emptyset)

(UCtx1, LCtx1) /\ (UCtx2, LCtx2) = Q
------------------------------------------------------------------- :: Match
(UCtx1, LCtx1 \u q ) /\ (UCtx2, LCtx2 \u q) = Q * 1.q

(UCtx1, LCtx1) /\ (UCtx2, LCtx2) = Q
q \notin LCtx2
q \notin Dup
------------------------------------------------------------------- :: DiffL
(UCtx1, LCtx1 \u q ) /\ (UCtx2, LCtx2) = Q * omega.q

(UCtx1, LCtx1) /\ (UCtx2, LCtx2) = Q
q \notin LCtx1
q \notin Dup
------------------------------------------------------------------- :: DiffR
(UCtx1, LCtx1 ) /\ (UCtx2, LCtx2 \u q) = Q * omega.q

(UCtx1, LCtx1) /\ (UCtx2, LCtx2) = Q
q \notin LCtx2
q \in Dup
------------------------------------------------------------------- :: DiffDL
(UCtx1, LCtx1 \u q ) /\ (UCtx2, LCtx2) = Q * 1.q

(UCtx1, LCtx1) /\ (UCtx2, LCtx2) = Q
q \notin LCtx1
q \in Dup
------------------------------------------------------------------- :: DiffDR
(UCtx1, LCtx1 ) /\ (UCtx2, LCtx2 \u q) = Q * 1.q

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  Desugared expressions  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

defns
Core :: '' ::=

defn
G |- e : t :: :: Core :: 'L_' {{ com Core language }}
by

x :_1 forall as. u \in G
------------------------- :: Var
G |- x : u[ts/as]

G, x:_pi t1 |- e : t2
------------------------ :: Abs
G |- \x.e : t1 ->_pi t2

G1 |- e1 : t1 ->_pi t
G2 |- e1 : t1
------------------------- :: App
G1 + pi.G2 |- e1 e2 : t

G1 |- e1 : t1[us/as]
G2 |- e2 : t2[us/as]
------------------------------------------ :: Pack
G1+G2 |- pack (e1, e2) : exists as.t2 o- t1

G1 |- e1 : exists as. t2 o- t1
as fresh
G2,x:_1 t1,y:_1 t2 |- e2 : t
------------------------------------ :: Unpack
G1+G2 |- unpack (x,y) = e1 in e2 : t

G1 |- e1 : t1
G2, x:_pi s |- e2 : t
----------------------------------- :: Let
pi.G1 + G2 |- let_pi x : s = e1 in e2 : t

G1 |- e : T ts
Ki : forall as. usi ->_pisi T as
G2, < xi :_(pi.pii) ui[ts/as] > |- ei : t
------------------------------------------------ :: Case
pi.G1+G2 |- case_pi e of { alts } : t