% Simply typed call-by-value lambda-calculus with constants
% and delimited continuations (shift/reset) and 
% Danvy/Filinski effect typing
%
% This is the intrinsic encoding, using GADTs native to Twelf.
% This file may be regarded as a translation of ShiftResetGenuine.hs, 
% with GADTs implementing parameterized monads. 
% Unlike the monadic encodings, we implement delimited continuations 
% `directly', in the `bubbling-up' style. Although the semantics is
% small step, we eschew explicit contexts (both object-level and meta-level:
% all world declarations below are empty).
%
% The main attractions are
%   - Twelf doing all type inference,
%   - subject reduction is more than trivial:
%     it is the very definition of eval,
%   - progress is just the totality of one-step reduction
% The intrinsic encoding is explained in
%	http://twelf.plparty.org/wiki/Intrinsic_encoding
% and has been independently pointed out by Chung-chieh Shan.
%
% Calculus:
% - Call-by-value lambda-calculus with shift/reset, integers, arithmetic,
%   conditional, fix-point
% - Type-and-effect typing, per Danvy/Filinski's 1989 technical report
% - No let-polymorphism
% - Small-step semantics with NO explicit contexts
% - Bubbling-up semantics of shift
%
% Formalization:
% - Higher-order abstract syntax
% - Includes both evaluation and type inference (`theory') and
%   the type soundness proofs (`meta-theory')
% - No explicit contexts (neither on the object level, nor on the
%   meta-level. All world declarations are empty)
% - Proved value/expression classification
% - Proved subject reduction: type preservation in one-step evaluation
%   and many-step evaluation. 
% - Proved progress: the one-step evaluation is total


% Types
pure: type. %name pure U.		% Pure types, types of values
tp  : type. %name tp T.			% General, effectful type

% An affectful type is a triple of pure types: et ui uo u
% Here, u is the type of the value produced by an expression;
% The evaluation of an expression may also change the answer type,
% from ui to uo.
et : pure -> pure -> pure -> tp.


int: pure.				% one single primitive type for now.
=> : pure -> tp -> pure.		%infix right 200 =>.

% Expressions and Values
%
% All values are typed, with a pure type. All expressions are typed,
% with the general type. All values are expressions.

% The definitions below specify not only the syntax of the language,
% but also its type system. Type inference is syntax-directed, and
% it is indeed tied to syntax. Type judgements are literally specified
% alongside the syntax.
% For the type system, we use Asai and Kameyama's APLAS07 paper (AK07):
% Fig 3 we only drop the `let' judgements: we don't have `let' in our
% calculus.
val : pure -> type.	     	    	%name val V.
exp : tp -> type.			%name exp E.
res : pure -> pure -> type.		%name res C. % contexts

	% All values are expressions, with any answer type
v : val U -> exp (et W W U).		%prefix 350 v.

	% primitive values: natural literals and the increment function
nat: type.				%name nat N.
0: nat.
1: nat -> nat.				%prefix 200 1.

n   : nat -> val int.			%prefix 400 n. % numeric literals
inc : val (int => et W W int).
dec : val (int => et W W int).


lam : (val A -> exp B) -> val (A => B).	% Abstractions are values
		% Type annotation is required to avoid
		% problems with the implicit variable W
l : (val A -> exp B) -> exp (et W W (A => B))
  = [body] v lam body.

fix : (exp (et WI WO A) -> exp (et WI WO A)) -> exp (et WI WO A).

	% Application. See rule 'app' in Fig 3 of AK07
@ : exp (et G D (S => et A B U)) -> 
    exp (et B G S) -> 
    exp (et A D U).			%infix left  300 @.

    	% See the rule 'if' in Fig 3 of AK07
ifz : exp (et S B int) -> exp (et A S U) -> exp (et A S U) -> exp (et A B U).

	% Delimited control

	% reset
? : exp (et S T S) -> exp (et W W T).

	% deru is used by the bubble-up semantics, internally
	% The user normally uses 'de' defined below
	% The typing rule is more general than the one in AK07
	% or in Danvy/Filinski.
	% This is because deru describes the current `bubble'
deru : (val U -> exp (et W AI AICurr)) -> % continuation being captured:
       (res U AI -> exp (et S AF S)) ->   % Body of shift
       exp (et W AF AICurr).

de : (res U W -> exp (et S AF S)) -> exp (et W AF U)
= [body] deru ([h] v h) body.	% How to use shift in user code

% Building contexts
ctx : (val U -> exp (et S A S)) -> res U A.

% We need a special operator to plug the continuation with a value
< : res U A -> exp (et WI WO U) -> exp (et WI WO A).
%infix left  300 <.

% A simple example of a program with shift/reset

% reset (shift k. 0)
ts2 = ? (de [k] (v n 0)).

% reset (shift k. k 0)
ts = ? (de [k] k < (v n 0)).

% reset (shift k. k (k 0))
ts = ? (de [k] k < (k < (v n 0))).

% ------------------------------------------------------------------------
% Dynamic semantics

% --------------------------------------------------
% Value classification

% Some expressions are values, some other are non-values

non-value: exp T -> type.
%mode non-value +E.
% The following simple rule would have sufficed.
% c-@: non-value (_ @ _).
% But the following more elaborate rules simplify the congruences.
c-@00: non-value ((v _) @ (v _)).
c-@1x: non-value (E1 @ _)
      <- non-value E1.
c-@01: non-value ((v _) @ E2)
      <- non-value E2.
c-@X:  non-value ((deru _ _) @ _).
c-@Y:  non-value ((v _) @ (deru _ _)).

% c-z: non-value (ifz _ _ _).
c-z0: non-value (ifz (v _) _ _).
c-z1: non-value (ifz E _ _)
      <- non-value E.
c-zX: non-value (ifz (deru _ _) _ _).
c-?0: non-value (? (v _)).
c-?X: non-value (? (deru _ _)).
c-?1: non-value (? E)
      <- non-value E.
c-<0: non-value (K < (v _)).
c-<X: non-value (K < (deru _ _)).
c-<1: non-value (K < E)
      <- non-value E.
c-f: non-value (fix _).
%worlds () (non-value _).
%terminates {E} (non-value E).


% The following constructively proves that each expression is
% either a value, deru,  or non-value.
% The following is purely automatic, and auxiliary
% relations vclassify-@ and vclassify-z are defined only because
% Twelf's output coverage checker can't deal with pattern-matching
% on output arguments <deep sigh>.

vhood: exp T -> type.
a-value     : vhood (v _).
a-deru      : vhood (deru _ _).
a-non-value : vhood E <- non-value E.

vclassify: {E:exp T} vhood E -> type.
%mode vclassify +E -P.
-: vclassify _ a-value.
-: vclassify _ a-deru.


vclassify-@: vhood E1 -> vhood E2 -> non-value (E1 @ E2) -> type.
%mode vclassify-@ +VE1 +VE2 -VE.
-: vclassify-@ a-value a-value c-@00.
-: vclassify-@ a-deru  _       c-@X.
-: vclassify-@ a-value a-deru  c-@Y.
-: vclassify-@ a-value (a-non-value V2) (c-@01 V2).
-: vclassify-@ (a-non-value V1) _ (c-@1x V1).
%worlds () (vclassify-@ _ _ _).
%total {} (vclassify-@ _ _ _).

-: vclassify (E1 @ E2) (a-non-value R)
   <- vclassify E1 PE1
   <- vclassify E2 PE2
   <- vclassify-@ PE1 PE2 R.

vclassify-z: vhood E -> {E1} {E2} non-value (ifz E E1 E2) -> type.
%mode vclassify-z +VE +E1 +E2 -PE.
-: vclassify-z a-value          _ _ c-z0.
-: vclassify-z a-deru           _ _ c-zX.
-: vclassify-z (a-non-value V1) _ _ (c-z1 V1).
%worlds () (vclassify-z _ _ _ _).
%total {} (vclassify-z _ _ _ _).

-: vclassify (ifz E E1 E2) (a-non-value R)
   <- vclassify E PE
   <- vclassify-z PE E1 E2 R.

vclassify-<: vhood E -> {K} non-value (K < E) -> type.
%mode vclassify-< +VE +C -PE.
-: vclassify-< a-value          _ c-<0.
-: vclassify-< a-deru           _ c-<X.
-: vclassify-< (a-non-value V1) _ (c-<1 V1).
%worlds () (vclassify-< _ _ _).
%total {} (vclassify-< _ _ _).

-: vclassify (K < E) (a-non-value R)
   <- vclassify E PE
   <- vclassify-< PE K R.

% This should be totally unnecessary. But it seems needed as a placeholder
% for an expression, so we can specify a particular expression
% in the definition of the family vclassify-?
reset-of: exp T -> type.
%mode reset-of +E1.
reset-of-: reset-of (? E).
%worlds () (reset-of _).

vclassify-?: reset-of ((? E):exp (et W W U)) -> vhood E -> 
	     non-value ((? E):exp (et W W U)) -> type.
%mode vclassify-? +ROF +VE -PE.
-: vclassify-? _ a-value          c-?0.
-: vclassify-? _ a-deru           c-?X.
-: vclassify-? _ (a-non-value V1) (c-?1 V1).
%worlds () (vclassify-? _ _ _).
%total {} (vclassify-? _ _ _).

-: vclassify ((? E):exp (et W W U)) (a-non-value R)
   <- vclassify E PE
   <- vclassify-? reset-of- PE R.

-: vclassify _ (a-non-value c-f).

%worlds () (vclassify _ _).
%total {E} (vclassify E _).

% --------------------------------------------------
% Small-step evaluation. Values are not in the domain of eval

eval : {E:exp T} non-value E  -> exp T -> type.
%mode eval +E1 +VC -E2.

ev-@: eval ((v lam EB) @ (v E)) c-@00 (EB E).	% beta-v

ev-i: eval (v inc @ (v n N)) _ (v n (1 N)).

ev-d0: eval (v dec @ (v n 0))     _ (v n 0).	% to keep dec total, we assume
ev-d+: eval (v dec @ (v n (1 N))) _ (v n N).	% that dec 0 is 0


ev-@1: eval (E1 @ E2) (c-@1x PE1-NV) (E1' @ E2)
       <- eval E1 PE1-NV E1'.
ev-@2: eval ((v E1) @ E2) (c-@01 PE2-NV) ((v E1) @ E2')
       <- eval E2 PE2-NV E2'.


ev-@X : eval ((deru C E) @ E2)   c-@X (deru ([x] ((C x) @ E2)) E).
ev-@Y : eval ((v E1) @ deru C E) c-@Y (deru ([x] ((v E1) @ (C x))) E).

ev-z0: eval (ifz (v n 0)     E1 E2) _ E1.
ev-z+: eval (ifz (v n (1 _)) E1 E2) _ E2.

ev-z1: eval (ifz E E1 E2) (c-z1 PE-NV) (ifz E' E1 E2)
       <- eval E PE-NV E'.
ev-zX: eval (ifz (deru C E) E1 E2) c-zX
            (deru ([x] ifz (C x) E1 E2) E).

ev-?0: eval (? (v V)) _ (v V).
ev-?1: eval (? E) (c-?1 PE) (? E')
       <- eval E PE E'.
ev-?X: eval (? (deru C E)) c-?X (? (E (ctx C))).

ev-<0: eval ((ctx C) < (v V)) _ (? (C V)).
ev-<1: eval (K < E) (c-<1 PE) (K < E')
       <- eval E PE E'.
ev-<X: eval (K < (deru C E)) _
            (deru ([x] (K < (C x))) E).
ev-f: eval (fix EB) _ (EB (fix EB)).
%worlds () (eval _ _ _).
%terminates {E} (eval E _ _).
%%covers eval +E1 +VC -E2. 
%total {E} (eval E _ _).

% Transitive closure of eval

eval*: exp T -> exp T -> type.
%mode eval* +E1 -E2.
-: eval* (v E) (v E).
-: eval* E ER <- vclassify E (a-non-value PNV) <- eval E PNV E' <- eval* E' ER.

% Evaluation tests

n0 = v n 0.
n1 = v n (1 0).
n2 = v n (1 1 0).
n3 = v n (1 1 1 0).
n4 = v n (1 1 1 1 0).
n5 = v n (1 1 1 1 1 0).
n6 = v n (1 1 1 1 1 1 0).
n7 = v n (1 1 1 1 1 1 1 0).


% The addition function

add = fix ([self] l [x] l [y]
        ifz (v x) (v y)
          (v inc @ (self @ (v dec @ v x) @ v y))).


% Nice to see all types inferred:
% add : {U1:pure} exp (et U1 U1 (int => et U1 U1 (int => et U1 U1 int)))
%    = [U1:pure]
%         fix
%            ([self:exp (et U1 U1 (int => et U1 U1 (int => et U1 U1 int)))]
%                l
%                   ([x:val int]
%                       l
%                          ([y:val int]
%                              ifz (v x) (v y)
%                                 (v inc @ (self @ (v dec @ v x) @ v y))))).

%query 1 2 eval* (add @ n2 @ n3) n5.

% The multiplication function

mul = fix ([self] l [x] l [y] 
        ifz (v x) n0
          (ifz (v dec @ v x) (v y)
            (add @ v y @ (self @ (v dec @ v x) @ v y)))).


%query 1 2 eval* (mul @ n2 @ n0) n0.
%query 1 2 eval* (mul @ n0 @ n3) n0.
%query 1 2 eval* (mul @ n2 @ n3) n6.

% The factorial function

fact = fix ([self] l [x] 
	       ifz (v x) n1
                (mul @ v x @ (self @ (v dec @ v x)))).

	            
%query 1 2 eval* (fact @ n3) n6.
%%query 1 2 eval* (fact @ n4) R.
% R = n (1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0).

% Delimited control tests
ts1 = ? n0.
ts2 = ? (de [f] (f < n0)).
ts3 = ? ((de [f] (f < (l [x] (v inc @ v x)))) @ n0).

%query 1 2 eval* ts1 n0.
%query 1 2 eval* ts2 n0.

%query 1 2 eval* ts3 n1.

% Danvy/Filinski's famous example
ts4 = ? (v inc @ 
    (? (v inc @ (v inc @ (de [f] (v inc @ (v inc @ (f < (f < n0))))))))).

%query 1 2 eval* ts4 n7.

% Checking CBV: the argument must be evaluated before the substitution
ts6' = (l [x] n1) @ (de [f] n0).
%%query 1 2 eval* t6' R.
%query 1 2 eval* (? ts6') n0.

% checking that our shift is shift indeed
ts01 = ? (de [f] (de [g] n0)).
%query 1 2 eval* ts01 n0.

ts02 = ? ((de [f] (v inc @ (v inc @ (f < (l [x] v inc @ v x))))) @ 
          (de [g] n1)).
% Nice to see the inferred types...
% ts02 : {U1:pure} exp (et U1 U1 int)
%    = [U1:pure]
%         ?
%            (de
%                ([f:res (int => et int int int) int]
%                    v inc @ (v inc @ (f < l ([x:val int] v inc @ v x))))
%                @ de ([g:res int int] n1)).
%query 1 2 eval* ts02 n3.


% This also shows the change in the answer-type...
ts03 = ? ((de [f] (f < (l [x] v inc @ v x))) @ 
          (de [g] (g < n1))).
%query 1 2 eval* ts03 n2.


ts04 = ? ((de [f] (f < (de [f] (l [x] v inc @ v x)))) @ 
          (de [g] (g < n0))).
%query 1 2 eval* ts04 (l [x] v inc @ v x).

ts05 = ? ((de [f] (f < (de [f] f < (l [x] v inc @ v x)))) @ 
          (de [g] (g < n0))).
%query 1 1 eval* ts05 n1.

% patent changing of the answer-type...
tc01 = (v inc @ (de [f] (l [x] (f < v x)))).
% Indeed, see the inferred type...
% tc01 : {U1:pure} {U2:pure} exp (et U1 (int => et U2 U2 U1) int)
%    = [U1:pure] [U2:pure] v inc @ de ([f:res int U1] l ([x:val int] f < v x)).
%query 1 2 eval* (? tc01) R.
% R = v lam ([v1:val int] ctx ([v2:val int] v inc @ v v2) < v v1).

ts8 = ? (v inc @ ((l [f] (v f @ n0)) @ 
         (de [k] v inc @ (k < (l [x] v inc @ v x))))).

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

ts10 = ? (v inc @ ((l [f] (v f @ n0)) @ 
          (de [k] v inc @ (k < (de [_] n0))))).
%query 1 2 eval* ts10 n0. % In CBN: (n 1 0).

% realistic example requiring answer-type polymorphism, which we don't have
tpoly = de [k] l [table] ((k < (v table @ n1)) @ v table).
%% tpoly1 = tpoly @ n2. % needs polymorphism
tpoly = de [k] l [table] (((k < (? (v table @ n1)))) @ 
              l [x] ? (v table @ v x)).
% tpoly1 = tpoly @ n2. % needs polymorphism
% tpoly2 = (? ((l [x] l [table] v x) @ (tpoly))) @ 
%          (l [v1] l [v2] add @ v v1 @ v v2).

% %query 1 2 eval* tpoly2 n3.

% A few examples demonstrating congruences, suggested by Ken

% tcong1 = fix @ ((l T1 [f] f) @ (l _ [self] n1)).
% %query 1 2 eval* tcong1 n1.

tcong2 = ? (fix [self] de [k] k < n1).
%query 1 2 eval* tcong2 n1.