% encoding of higher-order focusing
% a.k.a., lambda calculus with pattern-matching in CPS
% copyright Noam Zeilberger (2009)

%%%% "built-in" arithmetic
nat : type.       %mode nat.
z : nat.
s : nat -> nat.	  %prefix 10 s.

add : nat -> nat -> nat -> type.
%mode add +M +N -P.
add/z : add z N N.
add/s : add (s M) N (s P) <- add M N P.
%worlds () (add M _ _).
%total (M) (add M N P).

%%%% types
tp : type.
int  : tp.					% primitive nats
+ : tp -> tp -> tp. %infix right 11 +.		% binary sums
void : tp.					% void
*    : tp -> tp -> tp. %infix right 12 *.	% binary products
unit : tp.					% unit
neg  : tp -> tp.				% continuations
rec  : (tp -> tp) -> tp.			% recursive types

% some derived types
arrow = [A] [B] neg (A * neg B).		% CBV-CPS functions
Nat = rec [X] unit + X.				% nat datatype
List = [A] rec [X] unit + A * X.		% lists
Lam = rec [X] arrow X X.			% Lam = Lam -> Lam

%%%% contexts (as join lists)
ctx : type.
emp : ctx.
join : ctx -> ctx -> ctx.
fhyp : tp -> ctx.

%%%% patterns
pat : ctx -> tp -> type.
%mode pat -Delta +A.

num : nat -> pat emp int.
inl : pat Delta A -> pat Delta (A + B).
inr : pat Delta B -> pat Delta (A + B).
u   : pat emp unit.
pair : pat Delta1 A -> pat Delta2 B -> pat (join Delta1 Delta2) (A * B).
fold : pat Delta (A (rec A)) -> pat Delta (rec A).
wild : pat (fhyp A) (neg A).

% some derived patterns
zz : pat emp Nat = fold (inl u).
ss : pat Delta Nat -> pat Delta Nat = [p] fold (inr p).  %prefix 9 ss.

nil : pat emp (List A) = fold (inl u).
cons : pat Delta1 A -> pat Delta2 (List A) -> pat (join Delta1 Delta2) (List A) =
	[p1] [p2] fold (inr (pair p1 p2)).

%%%% judgments

true : tp -> type.  %prefix 9 true.
all : ctx -> type.  %prefix 9 all.
false : tp -> type. %prefix 9 false.
%mode false +A.

lctx : type.
@ : lctx.
,, : lctx -> ctx -> lctx.  %infix left 9 ,,.
# : lctx -> type.  %prefix 9 #.

%%%% terms

% values
val : pat Delta A -> all Delta -> true A.

% substitutions
semp : all emp.
sjoin : all Delta1 -> all Delta2 -> all (join Delta1 Delta2).
scon : false A -> all (fhyp A).

% closed expressions
throw : false A -> true A -> # @.              % throw K V
let : all Delta -> # (@ ,, Delta) -> # @.      % let Sigma in E
abort : nat -> # @.

% expressions in context

bemp : # Gamma -> # (Gamma ,, emp).
bjoin : # (Gamma ,, Delta2 ,, Delta1) -> # (Gamma ,, (join Delta1 Delta2)).
bvar : (false A -> # Gamma) -> # (Gamma ,, fhyp A).
ball : (all Delta -> # Gamma) -> # (Gamma ,, Delta).
%prefix 9 bemp. %prefix 9 bjoin. %prefix 9 bvar. %prefix 9 ball.

%%%% defunctionalized continuations: declaration + definition

% the "apply" function
body : false A -> pat Delta A -> # (Gamma ,, Delta) -> type.
%mode body +Phi +P -E.

% some useful continuations

ignore : false A.
ignore/p : body ignore P (ball [_] abort z).

exit : false int.
exit/n : body exit (num N) (bemp (abort N)).

% plus defined via built-in addition
plus : false int -> false (int * int).
plus/mn : body (plus K) (pair (num M) (num N))
	  (bjoin bemp bemp 
		    throw K (val (num P) semp))
	     <- add M N P.

% plus' defined via explicit recursion
succ : false Nat -> false Nat.
succ/n : body (succ K) N (ball [sigma] throw K (val (ss N) sigma)).

plus' : false Nat -> false (Nat * Nat).
plus'/zn : body (plus' K) (pair zz N) (bjoin bemp ball [sigma]
		throw K (val N sigma)).
plus'/sn : body (plus' K) (pair (ss M) N) (ball [sigma]
	        throw (plus' (succ K)) (val (pair M N) sigma)).

% conversion function Nat -> int

add1 : false int -> false int.
add1/n : body (add1 K) (num N) (bemp throw K (val (num (s N)) semp)).

N2n : false int -> false Nat.
N2n/zz : body (N2n K) zz (bemp throw K (val (num z) semp)).
N2n/ss : body (N2n K) (ss N) (ball [sigma] throw (N2n (add1 K)) (val N sigma)).

% silliness

lambda : (false Lam -> false Lam) -> false (Lam * neg Lam).
lambda/f : body (lambda F) (pair (fold wild) wild)
	    (bjoin bvar [x] bvar [k]
	       throw (F k) (val (fold wild) (scon x))).

Lambda : (false Lam -> false Lam) -> true Lam =
   [f] val (fold wild) (scon (lambda f)).

selfapp : false Lam -> false Lam.
selfapp/k : body (selfapp K) (fold wild)
	    (bvar [k] 
	       throw k (val (pair (fold wild) wild) (sjoin (scon k) (scon K)))).

omega : # @ = throw (selfapp ignore) (Lambda selfapp).

%terminates P (body _ P _).
%worlds () (body _ P _).
%total P (body K P _).

%%%% big-step semantics

result : type.
halt : nat -> result.
diverge : result.

load : all Delta -> # (Gamma ,, Delta) -> # Gamma -> type.
%mode load +Sigma +E -E'.

ld/emp : load Delta (bemp E) E.
ld/con : load (scon K) (bvar E*) (E* K).
ld/join : load (sjoin S1 S2) (bjoin E) E''
	  <- load S1 E E'
	  <- load S2 E' E''.
ld/all : load S (ball E) (E S).
%worlds () (load _ _ _).
%total (Sigma) (load Sigma _ _).

% really this should be a coinductive relation
eval : # @ -> result -> type.
%mode eval +E -R.

ev/load : eval (let Sigma E) R
       <- load Sigma E E'
       <- eval E' R.
ev/throw : eval (throw K (val P Sigma)) R
       <- body K P E
       <- eval (let Sigma E) R.
ev/abort : eval (abort N) (halt N).

%worlds () (eval _ _).
%covers eval +E -R.

% 2 + 2 = 4 with built-in nats
%query 1 *
  eval (throw (plus exit) (val (pair (num (s s z)) (num (s s z))) (sjoin semp semp))) E.


% 2 + 3 = 5 with datatype Nat
%query 1 *
  eval (throw (plus' (N2n exit)) (val (pair (ss ss zz) (ss ss ss zz)) (sjoin semp semp))) E.

% uncomment for never-ending fun!
% %query 1 *
% eval omega diverge.