=================================================
=================== LANG0 =======================
=================================================

differences between lang0 and capability calculus:
 - major:
  - general "resources", not regions (no region annotations)
    (newrgn, freergn, region ops --> new, free, use)
  - static concepts only (omit r, heap, heap types)
  - omit recursion
 - minor (for neatness, conciseness):
  - limit (C,t1,...,tn) to (C,t)
  - limit <t1,...,tn> to <t1,t2>
  - split all[D].(C,t)->0 into pieces
  - omit int type, integer ops
  - require kind annotation on c
misc. notational differences

=================================================
================== SYNTAX =======================
=================================================

k = type | res | cap
b = A | t | c
t = A | A handle | all A:k.t | (c,t)->0 | <t1,t2> | _t
_t = all A<=c.t
c = A | {} | {A p} | c1+c2 | /c
p = ~ | +

d = . | d,A:k | d,A<=c
g = . | g,x:t

v = x | v[b:k]
h = \A:k.h | \(c,x:t).e | <v1,v2> | _h
_h = \A<=c.h
l = x=v | x=h | x=v.n | new A,x | free v | use v
e = let l in e | v1 v2 | halt

=================================================
================= SEMANTICS =====================
=================================================

d |- .

d |- d'
----------- (A not in Dom(d,d'))
d |- d',A:k

d |- d'
d,d' |- c:cap
------------- (A not in Dom(d,d'))
d |- d',A<=c

=================================================

d |- .

d |- g
d |- t:type
----------- (x not in Dom(g))
d |- g,x:t

=================================================

...,A:k,... |- A:k

...,A<=c,... |- A:cap

d |- A:res
------------------
d |- A handle:type

d |- t1:type
d |- t2:type
-----------------
d |- <t1,t2>:type

d,A:k |- t:type
------------------- (A not in Dom(d))
d |- all A:k.t:type

d |- c:cap
d,A<=c |- t:type
-------------------- (A not in Dom(d))
d |- all A<=c.t:type

d |- t:type
d |- c:cap
------------------
d |- (c,t)->0:type

d |- {}:cap

d |- A:res
--------------
d |- {A p}:cap

d |- c1:cap
d |- c2:cap
--------------
d |- c1+c2:cap

d |- c:cap
-----------
d |- /c:cap

=================================================

/* probably not necessary

d |- . = .

d |- d1 = d2
------------------- (A not in Dom(d,d1))
d | d1,A:k = d2,A:k

d |- d1 = d2
d,d1 |- c1 = c2:cap
---------------------------- (A not in Dom(d,d1))
d |- d1,A<=c1 = d1,A<=c2:cap

*/

=================================================

d |- b:k
------------
d |- b = b:k

d |- b2 = b1:k
--------------
d |- b1 = b2:k

d |- b1 = b2:k
d |- b2 = b3:k
--------------
d |- b1 = b3:k

d |- c1 = c1':k
d |- c2 = c2':k
---------------------- where k = cap
d |- c1+c2 = c1'+c2':k

d |- c1 = c1':cap
-------------------
d |- /c1 = /c1':cap

d |- c:k
--------------- where k = cap
d |- {}+c = c:k

d |- c1:k
d |- c2:k
-------------------- where k = cap
d |- c1+c2 = c2+c1:k

d |- c1:k
d |- c2:k
d |- c3:k
------------------------------ where k = cap
d |- (c1+c2)+c3 = c1+(c2+c3):k

d |- c:cap
-------------------
d |- /c = /c+/c:cap

d |- /{} = {}:cap

d |- A:res
---------------------
d |- /{A~} = {A+}:cap

d |- c:cap
-----------------
d |- //c = /c:cap

d |- c1:cap
d |- c2:cap
---------------------------
d |- /(c1+c2) = /c1+/c2:cap

=================================================

d |- c1 = c2:k
-------------- where k = cap
d |- c1 <= c2

d |- c1 <= c2
d |- c2 <= c3
-------------
d |- c1 <= c3

d |- c1 <= c1'
d |- c2 <= c2'
---------------------
d |- c1+c2 <= c1'+c2'

d |- c <= c'
--------------
d |- /c <= /c'

...,A<=c,... |- A<=c

d |- c:cap
------------
d |- c <= /c

d |- c:cap
------------ (optional)
d |- c <= {}

=================================================

d |- t1 = t1':type
d |- t2 = t2':type
-----------------------------
d |- <t1,t2> = <t1',t2'>:type

d,A:k |- t = t':type
-------------------------------- (A not in Dom(d))
d |- all A:k.t = all A:k.t':type

d |- c = c':cap
d,A<=c |- t = t':type
----------------------------------- (A not in Dom(d))
d |- all A<=c.t = all A<=c'.t':type

d |- t = t':type
d |- c = c':cap
-------------------------------
d |- (c,t)->0 = (c',t')->0:type

=================================================

d,A:k;g |- h:t
------------------------ (A not in Dom(d))
d;g |- \A:k.h: all A:k.t

d |- c:cap
d,A<=c;g |- h:t
-------------------------- (A not in Dom(d))
d;g |- \A<=c.h: all A<=c.t

d |- c:cap
d |- t:type
d;g,x:t;c |- e
--------------------------- (x not in Dom(g))
d;g |- \(c,x:t).e: (c,t)->0

d;g |- v1: t1
d;g |- v2: t2
-----------------------
d;g |- <v1,v2>: <t1,t2>

d;g |- h: t'
d |- t' = t:type
----------------
d;g |- h: t

=================================================

d;...,x:t,... |- x: t

d;g |- v: all A:k.t
d |- b:k
----------------------
d;g |- v[b:k]: [A<-b]t

d;g |- v: all A<=c'.t
d |- c <= c'
------------------------
d;g |- v[c:cap]: [A<-c]t

d;g |- v: t'
d |- t' = t:type
----------------
d;g |- v: t

=================================================

d;g |- v:t
-------------------------- (x not in Dom(g))
d;g;c |- x=v ==> d;g,x:t;c

d;g |- h:t
-------------------------- (x not in Dom(g))
d;g;c |- x=h ==> d;g,x:t;c

d;g |- v:<t_1,t_2>
------------------------------ (x not in Dom(g) and 1<=n<=2)
d;g;c |- x=v.n ==> d;g,x:t_n;c

d;g;c |- new A,x ==> d,A:res;g,x:A handle;c+{A~} (A not in Dom(d) and x not in Dom(g))

d;g |- v: A handle
d |- c = c'+{A~}:cap
--------------------------
d;g;c |- free v ==> d;g;c'

d;g |- v: A handle
d |- c <= c'+{A+}
------------------------
d;g;c |- use v ==> d;g;c

=================================================

d;g;c |- l ==> d';g';c'
d';g';c' |- e
-----------------------
d;g;c |- let l in e

d;g |- v1: (c',t)->0
d;g |- v2: t
d |- c <= c'
--------------------
d;g;c |- v1 v2

d |- c = {}:cap
---------------
d;g;c |- halt

=================================================
=================== LEMMAS ======================
=================================================

Language lemmas:
  - if |- d and d |- g and d;g |- v:t then d |- t:type
  - if |- d and d |- g and d;g |- h:t then d |- t:type