%		Delimited continuations (shift) in CBN

% `Effect polymorphism'
% Regular, CBN functions, take arbitrary expressions as an argument.
% The type of the argument (annotation on the binder) is an arbitrary,
% possibly `effectful' type T. That type provides the _upper bound_
% on the `effectfulness' of the function argument: the function will
% accept any less effectful expression (for example, a pure one) but not
% a more effectful expression. See the TLCA07 paper for the definition of
% the order on effectful types (see also subtype predicate below).
% It follows then that a CBN function whose binder is annotated with a pure
% type U will not accept as an argument any expression that may possibly
% cause a control effect. That might be limiting at times. Therefore,
% we introduce a special category of `strict functions' (aka CBV functions).
% They can take only values as argument. We can write applications
% of such functions to any expression, no matter how effectful.
% That expression must first be evaluated before the application could
% proceed. In a sense, such strict functions are `effect-polymorphic'
% in that they can be applied to arguments with any effectfulness.

% Incidentally, the regular function application is such a `strict'
% function in its first argument.

% Hmm, a better idea occurred to me: instead of introducing a new type
% of expressions (strict functions) and new type of lambda (strict lambda),
% why not to introduce a new sort of applications, the one that is strict
% in both of its arguments? That turns out not too well: too many rules
% have to be introduced, one have to think of strict applications to be
% passed as arguments to CBN functions, etc.
%
% relationship with quotation and thunk translation? 

% Types

pure: type.                             %name pure U.
tp:   type.                             %name tp T.
cotp: type.                             %name cotp S.

int: pure.				% one single primitive type for now.
   % strict function (forces the evaluation of its argument)
*>: pure -> tp -> pure.                 %infix right 200 *>.
   % General, non-strict function: may evaluate its argument many times or
   % never
=>: tp -> tp -> pure.                   %infix right 200 =>.

pr: pure -> tp.                         %prefix      150 pr.
   % for shift, answer-types are always pure
=v: cotp -> pure -> tp.                 %infix right 130 =v.

% co-types are isomorphic to _purest_ functions,
% Indeed, the `hole' in a context is in the position where a value
% is demanded. The range of co-type is also pure because of # at the end.
=^: pure -> pure -> cotp.               %infix right 140 =^.

% ------------------------------------------------------------------------
% Expressions (see examples below)

exp: type.				%name exp E.
fn!: type.				%name fn! D. % strict functions
res: type.				%name res C. % coterms

	% primitive values: natural literals
nat: type.                              %name nat N.
0: nat.
1: nat -> nat.                          %prefix 200 1.
n: nat -> exp.				%prefix 150 n.

% expressions (terms)
		% first argument is the type of the bound variable
		% (doesn't have to be a pure type)
l  : tp -> (exp -> exp) -> exp.		% lambda (x) body
@  : exp -> exp -> exp.			%infix left 105 @.
!  : fn! -> exp.			%prefix 150 !.
xi : cotp -> (res -> exp) -> exp.	% shift f. e

% strict functions; increment is a built-in constant
inc : fn!.				% increment
l! : pure -> (exp -> exp) -> fn!.	% lambda (x) body, CBV

!l : pure -> (exp -> exp) -> exp = [t] [f] ! l! t f.
!inc = ! inc.

% co-terms
# : res.				% Top co-term
, : exp -> res -> res.          	%infix right 250 ,.
;!: res -> fn! -> res.          	%infix right 250 ;!.

% co-term application (aka, filling the hole)
< : res -> exp -> exp.			%infix left 100 <.

% Abbreviation for reset
?  : exp -> exp = [e] # < e.		%prefix 150 ?. % reset

		% The following `abstract term' isn't present in the
		% regular terms (at run-time). It is only used for
		% abstract interpretation.
		% The abstract value is the `value' in the sense it is
		% not inspectable and not traversable.
at: tp -> exp.				%prefix 110 at.
		% abstract co-term
ar: cotp -> res.			%prefix 110 ar.

		% introducing context for hypothetical reasoning:
		% special co-term to hold the hypothesis (aka, type)
cl: tp -> res.				%prefix 110 cl.
cl!: pure -> res.			%prefix 110 cl!.
ct: cotp -> res.			%prefix 110 ct.
cx: pure -> pure -> res.

% classification of expressions: values and non-values
val : exp -> type.
%mode val +E.
val-n: val (n N).
val-l: val (l _ E).			% non-strict functions are values
val-s: val (! D). 			% so are the strict functions
%worlds () (val _).
%terminates (E) (val E).

% Non-values  are used to `orient' the term equalities (which govern
% focusing and unfocusing)
nonval : exp -> type.
%mode nonval +E.
nval-@: nonval (E1 @ E2).
nval-<: nonval (C < E2).
nval-x: nonval (xi _ _).
%worlds () (nonval _).
%terminates (E) (nonval E).


% one-step reduction of non-values.
eval : exp -> exp -> type.
%mode eval +E1 -E2.

% general function: beta and application ctx accumulation
-: eval (C < l _ E1 @ E2) (C < E1 E2).
-: eval (C < E1 @ E2) ((E2 , C) < E1) <- nonval E1.

% strict functions
-: eval (C < ! inc @ (n N)) (C < n (1 N)).
-: eval (C < ! (l! _ E1) @ E2) (C < E1 E2) <- val E2.
-: eval (C < ! D @ E) ((C ;! D) < E) <- nonval E. % ctx accumulation

% reset, multiple context congruence
-: eval (# < E) E <- val E.
-: eval (C1 < (C2 < E)) (C1 < R) <- eval (C2 < E) R.

% shift
-: eval (C < xi _ E) (# < (E C)).

% ctx unwinding
-: eval ((E2 , C) < E1) (C < (E1 @ E2))    <- val E1.
-: eval ((C ;! D1) < E2) (C < (! D1 @ E2)) <- val E2.
%worlds () (eval _ _).
%terminates (E1) (eval E1 _).
% %covers eval +E1 -E2. None of the values are in the domain of eval...


% transitive reflexive closure of eval
eval* : exp -> exp -> type.
%mode eval* +E1 -E2.

-: eval* E E <- val E.
%% shift outside reset is not an error. Rather, it behaves as a (co)value.
% -: eval* (xi S E) (xi S E).
-: eval* E1 E2 <- eval E1 E1' <- eval* E1' E2.

% tests

t1 = ? (n 0).
t2 = ? (xi S [f] (f < (n 0))).
t3  = ? ((xi S [f] (f < (l T [x] x))) @ (n 0)).
t3' = ? ((xi S [f] (f < (!l T [x] (!inc @ x)))) @ (n 0)).

% Danvy/Filinski's famous example
t4 = ? (!inc @ (? (!inc @ (!inc @ 
	 (xi S [f] (!inc @ (!inc @ (f < (f < n 0))))))))).

%query 1 2 eval* t1 R.
%query 1 2 eval* t2 R.
%query 1 2 eval* t3 (n 0).
%query 1 2 eval* t3' (n 1 0).

%query 1 2 eval* t4 R.
%query 1 2 eval* t4 (n 1 1 1 1 1 1 1 0).


% CBN vs strict functions
t6  = (l T [x] n 1 0) @ (xi S [f] (f < (n 0))).
%query 1 2 eval* (? t6) (n 1 0).           % CBN application: no effect
t6' = (!l T [x] n 1 0) @ (xi S [f] (n 0)). % CBV application: effect
%%query 1 2 eval* t6' R.
%query 1 2 eval* (? t6') (n 0).

	% applying an effectful term
t7 = ((l T [x] (xi S1 [_] x)) @ (xi S2 [f] (f < (n 1 0)))).
%%query 1 2 eval* t7 R.
%query 1 2 eval* (? t7) (n 1 0).

% checking that our shift is shift indeed
ts01 = ? (xi S1 [f] (xi S2 [g] (n 0))).
%query 1 2 eval* ts01 (n 0).

ts02 = ? ((xi S1 [f] (f < !inc)) @ (xi S2 [g] (n 0))).
%query 1 2 eval* ts02 (n 0).


% This also shows the change in the answer-type...
ts03 = ? ((xi S1 [f] (f < !inc)) @ (xi S2 [g] (g < n 0))).
%query 1 2 eval* ts03 (n 1 0).

ts04 = ? ((xi S1 [f] (f < (xi S3 [f] !inc))) @ (xi S2 [g] (g < n 0))).
%query 1 2 eval* ts04 !inc.

% Check that we can pass an effectful term, which gets evaluated `inside'
ts05 = ? ((xi S1 [f] (f < (xi S3 [f] f < !inc))) @ (xi S2 [g] (g < n 0))).
%query 1 2 eval* ts05 (n 1 0).


% patent changing of the asnwer-type...
tc01 = ? (!inc @ (xi S1 [f] (l T [x] (f < x)))).
%query 1 2 eval* tc01 R.
% R = l T1 ([x:exp] # ;! inc < x).

% % (display (reset
% %            (let ((x (shift f (cons 'a (f '())))))
% %              (shift g x))))

% more examples

t8 = ? (!inc @ ((!l T [f] (f @ n 0)) @ (xi S [k] !inc @ (k < !inc)))).

% %define ti = R %solve _ : (eval t8 R).
% %define ti = R %solve _ : (eval ti R).
%query 1 2 eval* t8 (n 1 1 1 0).

t9 = ? ((l T1 [x] (!inc @ x)) @ 
	((l T2 [f] (f @ n 0)) @ (xi S [k] !inc @ (k < !inc)))).
%query 1 2 eval* t9 (n 1 1 1 0).

% t10' = ? (!inc @ (xi S [k] (k < (xi S2 [_] n 0)))).
% %define ti = R %solve _ : (eval t10' R).
% %define ti = R %solve _ : (eval ti R).

% Passing an effectful term to a captured continuation
t10 = ? (!inc @ ((!l T [f] (f @ n 0)) @ 
	(xi S [k] !inc @ (k < (xi S2 [_] n 0))))).
%query 1 2 eval* t10 (n 1 0).


% ------------------------------------------------------------------------
%			Typing

% The deterministic predicate that decides subtyping. 
%   subtype T1 T2 asserts that T1 <= T2.
% Note that we don't explicitly assert T <= T for arbitrary T, since this
% is derivable from the rules below. There is no need to add more
% `choice points'.
subtype : tp -> tp -> type.
%mode subtype +T1 +T2.

% the following two declarations are for the sake of running %queries.
%deterministic subtype.
%tabled subtype.

% Primitive terms are the subtypes of themselves
-: subtype (pr int) (pr int).
% A pure type can always be converted to an impure one:
% a term that has no effect can be over-approximated to have (any)
% effect at all. In other words, U can be generalized to (U =^ T) =v T
% which is essentially the consequence that 'x' can be generalized to
% shift k. k x
% The following rule is a bit more general
-: subtype (pr U1) ((UA2 =^ UR1) =v UR2) 
	<- subtype (pr U1) (pr UA2)
	<- subtype (pr UR1) (pr UR2).
% standard co-variance/contra-variance
-: subtype (pr U1 *> T1) (pr U2 *> T2)
	<- subtype T1 T2
	<- subtype (pr U2) (pr U1).
-: subtype (pr TA1 => T1) (pr TA2 => T2)
	<- subtype T1 T2
	<- subtype TA2 TA1.
% Given a function h == (l (U => T) [f] (f e)), where f is a general
% function that takes a pure argument, we can apply h
% to f' of the type U *> T instead. Indeed, the argument of f must be
% a non-effectful term, so (brushing aside non-termination), it doesn't
% matter if we evaluate the argument (as a strict function would require)
% or not. For a strongly-normalizing calculus, we can indeed brush aside
% the termination concerns.
-: subtype (pr U1 *> T1) (pr (pr U2) => T2)
        <- subtype (pr U1 *> T1) (pr U2 *> T2).
% subtyping of impure terms. The over-arching idea: if a function
% or a continuation are prepared to deal with the type T2, one can always
% pass a `smaller' type T1.
% The reason for T2 <= T1 below: (U2 =^ T2) is what the body
% of the shift assumed of its context. The shift that assumes the worst
% of the context (the context is exceptional: has the bigger type)
% is always substitutable for the more optimistic shift.
-: subtype ((UA1 =^ U1) =v UR1) ((UA2 =^ U2) =v UR2)
	<- subtype (pr UR1) (pr UR2)
	<- subtype (pr UA1) (pr UA2)
	<- subtype (pr U2) (pr U1).
%worlds () (subtype _ _).
%covers subtype +T1 -T2.
%%terminates {T2} (subtype _ T2).

% Just treating =^ just as a regular arrow...
subcotype : cotp -> cotp -> type.
%mode subcotype +T1 +T2.
-: subcotype (U1A =^ U1R) (U2A =^ U2R)
	<- subtype (pr U1R) (pr U2R)
	<- subtype (pr U2A) (pr U1A).
%worlds () (subcotype _ _).
%covers subcotype +T1 +T2.


% One-step type-checking relation: one-step abstract interpretation.
% Our goal is to progressively reduce a term to an abstract term.
%
% The drawback of this approach is the difficulty of proving type preservation.
% I don't think Twelf can see the canonical forms of a given type.
% So, preservation should be formulated as follows then:
% if we have a redex (e.g., (l _ E1) E2) which has the type T,
% then as we replace (l _ E1) and E2 with abstract terms at of some types
% and do teval, we obtain the abstract term of the type T.

% Note, (at T) is not in the domain of teval1. So (at T) is a 
% `value' for the type-checker.
teval1 : exp -> exp -> type.
%mode teval1 +E1 -E2.

% abstraction of numbers
-: teval1 (n _) (at pr int).

% strict functions
-: teval1 (! inc) (at pr int *> pr int).
-: teval1 (! l! U E) (cl! U < (E  at pr U)). % introduce the hypothesis U

% general lambdas
-: teval1 (l TA E) (cl TA < (E  at TA)).

% applications
-: teval1 ((at pr U1 *> T1) @ (at pr U2)) (at T1)
	<- subtype (pr U2) (pr U1).
-: teval1 ((at pr TA => T1) @ (at TA2)) (at T1)
	<- subtype TA2 TA.

% effectful term in a partial context
-: teval1 ((at pr U1 *> T1) @ (at U2A =^ U2R =v UR))
	  ((cx U2R UR) < ((at pr U1 *> T1) @ (at pr U2A))).
-: teval1 ((at U1A =^ U1R =v UR) @ (at T2))
	  ((cx U1R UR) < ((at pr U1A) @ (at T2))).


% congruences. teval1 is somewhat like CBV: needs to `evaluate' both of 
% arguments of the application...
-: teval1 ((at T) @ E2) ((at T) @ E2') <- teval1 E2 E2'.
-: teval1 (E1 @ E2) (E1' @ E2) <- teval1 E1 E1'.

% reset
-: teval1 (? (at pr U)) (at pr U).
-: teval1 (? (at U1 =^ U2 =v UR)) (at pr UR)
   <- subtype (pr U1) (pr U2).
	% ((at pr U2 *> pr UR) @ (? (at T))).
	% or (pr U =^ UR) < ? (at T)

% contexts, hypotheses elimination
-: teval1 (cl! U < at T) (at pr U *> T).
-: teval1 (cl TA < at T) (at pr TA => T).
-: teval1 (ct S  < at pr U) (at S =v U).

% Type-checking partial co-term. 
-: teval1 ((cx UA UR) < at pr U) (at (U =^ UA) =v UR).
% The following is the most complex rule. The effectful term appears
% in the context that already has an effect, U1R
-: teval1 ((cx U1A U1R) < at S2 =v U2F) (at S2 =v U1R)
   <- subtype (pr U2F) (pr U1A).

% context application rule, =^E
-: teval1 (ar (UA =^ UR) < at pr U2) (at pr UR)
	<- subtype (pr U2) (pr UA).

-: teval1 (ar S1 < at (S2 =v UR)) (at pr UR)
	<- subcotype S1 S2.

% congruences
-: teval1 ((E1  , C) < at T) (C < (at T) @ E1).
-: teval1 ((C ;! D1) < at T) (C < ! D1 @ (at T)).

-: teval1 (C < E) (C < E') <- teval1 E E'.


% shift
-: teval1 (xi S E) (ct S < ? (E (ar S))). % introduce co-hyp S

%worlds () (teval1 _ _).
% %terminates (E1) (teval1 E1 _).
% %covers teval1 +E1 -E2. % Only teval (at T) X should be uncovered.



% We can do something like the following. Alas, that means we need a lot
% of pattern-mathing on the result of teval -- which is greatly-inconvenient
% in Twelf (need to define a new type family for each such pattern-match).
% So, we use the equivalent of one-step reduction instead.
% -: teval (n _) (pr int).
% teval-app : tp -> tp -> tp -> type.
% %mode teval-app +T1 +T2 -T3.
% -: teval-app (pr U1 *> T1) (pr U1) T1. % generally, subtype...
%
%
% -: teval (E1 @ E2) T 
% 	<- teval E1 T1
% 	<- teval E2 T2
% 	<- teval-app T1 T2 T.


% transitive reflexive closure of teval1: the typechecking relation
teval : exp -> tp -> type.
%mode teval +E1 -T.

-: teval (at T) T.
-: teval E T <- teval1 E E' <- teval E' T.

% tests

%query 1 2 teval t1 (pr int).

%query 1 2 teval (! inc @ n 0) (pr int).

%query 1 2 teval ((!l int [x] ! inc @ x)) (pr int *> (pr int)).
%query 1 2 teval ((!l int [x] ! inc @ x) @ n 0) (pr int).

 % pure and impure solutions possible
%query 2 2 teval (l TF [f] l TX [x] f @ x) R.

%query 2 2 teval ((l TF [f] l TX [x] f @ x) @ (!l int [x] ! inc @ x)) R.


%query 2 2 teval ((l TF [f] l TX [x] f @ x) @ (!l int [x] ! inc @ x) @ n 0)
	R.
%query 1 1 teval ((l TF [f] l TX [x] f @ x) @ (!l int [x] ! inc @ x) @ n 0)
	(pr int).


%query 1 2 teval t2 (pr int).

int=>int = (pr int) => (pr int).
int*>int = int *> (pr int).


%query 1 2 teval (? ((xi (int=>int =^ U) [f] (f < (l (pr int) [x] x))))) R.

% t3  = ? ((xi S [f] (f < (l T [x] x))) @ (n 0)).
%query 1 1 teval (? ((xi (int=>int =^ U) [f] (f < (l (pr int) [x] x))) @ 
	(n 0))) (pr int).

% t3' = ? ((xi S [f] (f < (!l T [x] (!inc @ x)))) @ (n 0)).
%query 1 1 teval (? ((xi (U2 =^ U) [f] (f < (!l T [x] (!inc @ x)))) @ 
	(n 0))) (pr int).

%query 1 2 teval t4 (pr int).


% tests for subtyping
%query 0 2 teval ((l (pr int) [x] x) @ (xi S [_] (n 0))) R. % ill-typed

%query 1 2 teval ((l (S1 =v U) [x] x) @ (xi S [_] (n 0))) 
	(int =^ int =v int). 

%query 1 2 teval ((!l int [x] x) @ (xi S [_] (n 0))) R.


% patent changing of the answer-type...
% tc01 = ? (!inc @ (xi S1 [f] (l T [x] (f < x)))).
%query 1 2 eval* (? (!inc @ (xi S1 [f] (l T [x] (f < x))))) R.
%query 2 2 teval (? (!inc @ (xi S1 [f] (l T [x] (f < x))))) R.
% eval: R = l T ([x:exp] # ;! inc < x)
% teval:
% R = pr (pr int) => (pr int);
% T = pr int;
% S1 = int =^ int.
% also: accepting an effectful term
% R = pr (int =^ int =v U1) => (pr U1);
% T = int =^ int =v U1;
% S1 = int =^ int.


% checking that our shift is shift indeed
% ts01 = ? (xi S1 [f] (xi S2 [g] (n 0))).
%query 1 1 teval ts01 (pr int).


% ts02 = ? ((xi S1 [f] (f < !inc)) @ (xi S2 [g] (n 0))).
% Some type annotations are needed: subtyping makes life complex...
%query 1 1 teval (? ((xi (int*>int =^ U) [f] (f < !inc)) @ 
	             (xi S2 [g] (n 0)))) (pr int).

% This also shows the change in the answer-type...
% ts03 = ? ((xi S1 [f] (f < !inc)) @ (xi S2 [g] (g < n 0))).
%query 1 1 teval (? ((xi (int*>int =^ U) [f] (f < !inc)) @ 
	             (xi S2 [g] (g < n 0))))
	(pr int).


% ts04 = ? ((xi S1 [f] (f < (xi S3 [f] !inc))) @ (xi S2 [g] (g < n 0))).
% %query 1 2 eval* ts04 !inc.

%query 1 1 teval 
       ((xi (int*>int =^ int) [f] (f < (xi (int*>int =^ U2) [f] !inc))) @ 
         (n 0)) 
       (int =^ int =v int *> (pr int)).

% ts04 does typecheck...
%query 1 1 teval 
       ((xi (int*>int =^ int) [f] (f < (xi (int*>int =^ int) [f] !inc))) @ 
         (xi (int =^ U3) [g] (g < n 0))) 
       (int =^ int =v int *> (pr int)).

% Check that we can pass an effectful term, which gets evaluated `inside'
% ts05 = ? ((xi S1 [f] (f < (xi S3 [f] f < !inc))) @ (xi S2 [g] (g < n 0))).
%query 1 2 teval 
       ((xi (int*>int =^ U) [f] (f < (xi S3 [f] f < !inc))) @ 
        (xi S2 [g] (g < n 0)))
       (int =^ int =v int).


% teval
%    (!l UA ([x:exp] xi (UA =^ UR) ([f:res] (f < x) @ x))
%        @ xi (e =^ U2) ([f:res] c forall1 /tt (f < c c1))) R.
%query 1 1 teval 
       ((!l int [x] xi S ([f:res] (f < x) @ x))
        @ xi S2 [f] (!l (int*>int *> pr int) [x] (f < n 0))
       )
       R.

% CBN and strict functions
%query 1 2 teval t6 (pr int).

%query 1 2 teval t6' R. 
% one solution, effectful type
% R = int =^ U1 =v int.
%query 1 2 teval (? t6') (pr int). % still several solutions, all ints

	% applying an effectful term
%query 1 1 teval t7 (S1 =v int).
%query 1 1 teval (? t7) (pr int).


% more examples

% t8 = ? (!inc @ ((!l T [f] (f @ n 0)) @ (xi S [k] !inc @ (k < !inc)))).
%query 1 1 teval (? (!inc @ ((!l T [f] (f @ n 0)) @ 
		             (xi (int*>int =^ U) [k] !inc @ (k < !inc)))))
	(pr int).

% t9 = ? ((l T1 [x] (!inc @ x)) @ 
% 	((l T2 [f] (f @ n 0)) @ (xi S [k] !inc @ (k < !inc)))).
%query 1 1 teval (? ((l T1 [x] (!inc @ x)) @ 
 	             ((l ((int*>int =^ int) =v int) [f] (f @ n 0)) @ 
		       (xi (int*>int =^ int) [k] !inc @ (k < !inc)))))
	(pr int).

% passing an effectful term to continuation...
% t10 = ? (!inc @ ((!l T [f] (f @ n 0)) @ 
% 	(xi S [k] !inc @ (k < (xi S2 [_] n 0))))).
%query 1 1 teval 
    (xi (U1 =^ int) [k] !inc @ (k < (xi S2 [_] n 0)))
    (int =^ int =v int).

%query 1 1 teval 
	((!l T [f] (f @ n 0)) @
          (xi (int*>int =^ int) [k] !inc @ (k < (xi S2 [_] n 0))))
    (int =^ int =v int).

%query 1 1 teval (? (!inc @ ((!l T [f] (f @ n 0)) @ 
		    (xi (int*>int =^ int) [k] 
			!inc @ (k < (xi S2 [_] n 0))))))
	(pr int).