lambda-nu.clf

id : type.
id/z : id.
id/s : id -o id.

answer : type.
yes : answer.
no : answer.

id/eq? : id -> id -> answer -> type.
id/eq/z/z : id/eq? id/z id/z yes.
id/eq/z/s : id/eq? id/z (id/s N) no.
id/eq/s/z : id/eq? (id/s N) id/z no.
id/eq/s/s : id/eq? M N B -o id/eq? (id/s M) (id/s N) B.

tm : type.
nm : type.

atm : nm -o tm.
nu : (nm -> tm) -o tm.
test : tm -o tm -o tm.

tt : tm.
ff : tm.
if : tm -o tm -o tm -o tm.

pair : tm -o tm -o tm.
spread : tm -o (tm -> tm -> tm) -o tm.

lam : (tm -> tm) -o tm.
ap : tm -o tm -o tm.


ty : type.
bool : ty.
name : ty.
arr : ty -o ty -o ty.
prod : ty -o ty -o ty.

of : tm -> ty -> type.
mobile : ty -> type.
local : nm -> type.

mobile/bool : mobile bool.

mobile/prod
  : mobile (prod S T)
  o- mobile S
  o- mobile T.

of/tt : of tt bool.
of/ff : of ff bool.

of/pair
  : of (pair M N) (prod S T)
  o- of M S
  o- of N T.

of/spread
  : of (spread M E) U
  o- of M (prod S T)
  o- Pi x. Pi y. of x S -> of y T -> of (E !x !y) U.

of/if
  : of (if M L R) S
  o- of M bool
  o- of L S
  o- of R S.

of/atm
  : of (atm A) name 
  o- local A.

of/lam 
  : of (lam E) (arr S T) 
  o- Pi x. of x S -> of (E !x) T.

of/ap 
  : of (ap M N) T 
  o- of M (arr S T) 
  o- of N S.

% Odersky's calculus is made type-safe by adding a mobility
% condition to the type of the fresh name generation.
of/nu
  : of (nu E) T
  o- mobile T
  o- Pi a. local a -> of (E !a) T.

of/test
  : of (test M N) bool
  o- of M name
  o- of N name.


is : nm -> id -> type.
count : id -> type.


dest : type.
eval : dest -> tm -> type.
retn : dest -> tm -> type.
push : dest -> (nm -> tm) -> type.

eval/atom : eval D (atm A) -o {retn D (atm A)}.
eval/tt : eval D tt -o {retn D tt}.
eval/ff : eval D ff -o {retn D ff}.
eval/lam : eval D (lam E) -o {retn D (lam E)}.
eval/pair : eval D (pair M N) -o {retn D (pair M N)}.

eval/if
  : eval D (if M L R) -o 
    { Exists d. eval d M 
    * (retn d tt -o {eval D L}) 
    & (retn d ff -o {eval D R})
    }.

eval/spread
  : eval D (spread M E) -o 
    { Exists d.
      eval d M
    * (retn d (pair M1 M2) -o {eval D (E !M1 !M2)})
    }.

eval/ap
  : eval D (ap M N) -o 
    { Exists d.
      eval d M
    * (retn d (lam E) -o {eval D (E !N)})
    }.

eval/nu
  : eval D (nu E) -o 
    { Exists d. Exists a. Pi i.
      count i -o 
      { !is a i
      * @count (id/s i)
      * eval d (E !a)
      * (retn d (F !a) -o {push d F * (retn d M -o {retn D M})})
      }
    }.

eval/test
  : eval D (test M N) -o 
    { Exists d1. Exists d2.
      eval d1 M 
    * eval d2 N 
    * ( retn d1 (atm A) 
      * retn d2 (atm B) 
      * is A I 
      * is B J
      -o (id/eq? I J yes -o {retn D tt})
       & (id/eq? I J no -o {retn D ff})
      )
    }.

push/atm : push D (\!a. atm a) -o {retn D (nu \!a. atm a)}.
push/nu : push D (\!a. nu \!b. atm b) -o {retn D (nu \!b. atm b)}.
push/tt : push D (\!a. tt) -o {retn D tt}.
push/ff : push D (\!a. ff) -o {retn D ff}.
push/lam : push D (\!a. lam (E !a)) -o {retn D (lam \!x. nu \!a. E !a !x)}.
push/pair : push D (\!a. pair (M !a) (N !a)) -o {retn D (pair (nu M) (nu N))}.

init : type = {@count id/z}.

evaluate : tm -> tm -> type.
evaluate/def : (Pi d. init -o eval d M -o {retn d N}) -o evaluate M N.

#query * 1 * 1
  evaluate 
    (if (nu \!a. nu \!b. test (atm a) (atm b)) ff tt)
    M.