% lambda-circle with shift/reset

% The calculus is a simple, 1-level version of lambda-circle --
% or a run-and-CSP-free version of our lambda-am1.
% However, it has shift/reset.
% We use lambda-circle rather than lambda-box, because in lambda-box
% all staged code must be closed: one can't have a boxed expression with
% a free variable. So, eta is not expressible in lambda-box.

% lambda-circle reference:
%      Rowan Davies. A temporal-logic approach to
%      binding-time analysis. In the Symposium on Logic in
%      Computer Science (LICS '96), pages 184-195, New
%      Brunswick, 1996. IEEE Computer Society Press.

% The calculus is designed so that we could write Gibonacci,
% staged Gibonacci, and let-insertion


% Primitive types: one so far, integer.
% A term N of type nat is a nonnegative integer.
%   Constructors: 0, 1.

nat: type.                              %name nat N.
0: nat.
1: nat -> nat.                          %prefix 200 1.

% implementation of the addition of two naturals
plus : nat -> nat -> nat -> type.
%mode plus +N1 +N2 -N3.
-: plus 0 N N.
-: plus (1 N1) N2 (1 N3) <- plus N1 N2 N3.
%worlds () (plus _ _ _).
%total {N} (plus N _ _).

% predecessor
% We make the predecessor total by setting pred 0 to 0
pred : nat -> nat -> type.
%mode pred +N1 -N2.
-: pred 0 0.
-: pred (1 N) N.
%worlds () (pred _ _).
%total {} (pred _ _).

% Staging levels
qual: type.			%name qual A.
q0 : qual.				% Level 0: present stage
q1 : qual.				% Level 1: code, future stage


% Types
% We have two types for code: <t> (written as & t below) and
% <t/t> (written as && (t / t) below). The former describes the code
% whose evaluation has no observable control effect. The latter describes
% the code with a control effect; the second type is the answer type.
% Discriminating pure code from effectful code lets us avoid selecting
% the answer type for each bracket.
% There is no subtyping for these code types, for simplicity.
% If a function demands an argument of the type <t1/t2>
% but only the value v of the type <t1> is available, the programmer
% must write the explicit conversion. Likewise, we have the type
% of pure functions U1 => U2 and general functions U1 *> U2 / UA. 
% Here, UA is the answer-type for function's body.
% Again, sometimes the programmer must write a coercion (which happens
% in the case of passing a function to a higher-order function).
% The coercion is expressible in the language, usually via a conditional
% statement with one ineffective branch. This is similar to Haskell's
% False guard trick...

tp: type.				%name tp U.


tpp: type.				%name tpp T. % a pair of types
/ : tp -> tp -> tpp.                    %infix none 250 /.

int: tp.				% one single primitive type for now.
	% function types
=> : tp -> tp -> tp.			%infix right 200 =>. % pure function
*> : tp -> tpp -> tp.			%infix right 200 *>. % impure
	% code types
&  : tp -> tp.				%prefix 230 &. % circle tp, pure
&& : tpp -> tp.				%prefix 230 &&. % circle tp, impure

	% pair types
*: tp -> tp -> tp.			%infix none 225 *.


% Since we don't allow CSP, we can state the restriction to one
% level in syntax


% Expressions. All expressions are labeled with their levels
% We minimize the number of binding constructs to only one:
% lambda. We fix as a constant, and the body of shift supposed to
% be a function, or something that evaluates to a function.
% fix is an applicative fixpoint combinator, defined as a _polymorphic_ 
% constant, with the type forall TV. (TV -> TV) -> TV.
% Here TV is generally a pure or impure arrow type.
% We do not have the explicit polymorphism. Rather, polymorphism is
% `baked' into the type system. The constant fix has a special type
% fix. When the type checker sees the application (fix @ E),
% it chooses TV based on the type of E (which must be an arrow type).
%
% The body of shift, aka `de', is supposed to be a function.
% Since we use shift-expansion-style of semantics here, the real
% shift form is called deru. The user-visible form `de' is the particular
% case, defined as an abbreviation below.
%
% The point of pairs is to introduce a limited form of polymorphism:
% polymorphism over the result type and the corresponding answer-type.
% The price to pay is that polymorphic constants fix, fst and snd are
% not first-class. They can't be passed as arguments. They can be wrapped
% into lambdas (eta-expanded). But they become monomorphic then.
% This situation is not quite different from Hindley-Milner functions,
% were polymorphic functions are not first-class either.
% Come to think of it, the point of ifz is exactly the same: polymorphism
% over that type w (the result type in Church-encoding).

exp: qual -> type.		%name exp E.

n  : nat -> exp A.			%prefix 170 n.
l  : tp -> (exp A -> exp A) -> exp A.	% lambda (x:t) body
@  : exp A -> exp A -> exp A.		%infix left 154 @.
fix: exp A.			% fix f (x:tv) body
+  : exp A -> exp A -> exp A.		%infix left 100 +.
dec: exp A -> exp A.			% Decrement
ifz: exp A -> exp A -> exp A -> exp A.	% if zero
^: exp q1 -> exp q0.			%prefix 170 ^. % aka next
~: exp q0 -> exp q1.			%prefix 150 ~. % aka prev

deru : tp -> (exp A -> exp A) -> exp A -> exp A.	% shift f. e
?  : exp A -> exp A .			%prefix 150 ?. % reset

de : tp -> exp A -> exp A =		% body must be a function
   [cotp] [body] deru cotp ([h] h) body.

cons: exp A -> exp A -> exp A.		% standard pair stuff
fst : exp A.				% constants
snd : exp A.

% abstract expressions: used in the type checking
apure : tp -> exp A.			% the type of 1 or <1>
a2    : tp -> tp -> exp A.		% The type of (shift f 1) or <shift f 1>
a21   : tp -> tp -> tp -> exp q1.	% Two answer-types
a11   : tp -> tp -> exp q1.		% pure level-1 expression with 
                                        % an effectful escape

al    : tp -> exp A -> exp A.		% lambda-abstraction
ar    : tp -> exp A -> exp A -> exp A.	% shift-abstraction

% Abbreviations
n0 = n 0.
n1 = n 1 0.
n2 = n 1 1 0.
n3 = n 1 1 1 0.
n4 = n 1 1 1 1 0.
n5 = n 1 1 1 1 1 0.
n6 = n 1 1 1 1 1 1 0.
n7 = n 1 1 1 1 1 1 1 0.
n8 = n 1 1 1 1 1 1 1 1 0.

% other useful abbreviations
int=>int = int => int.
int=>int=>int = int => int=>int.
&int = & int.				% int code


% ========================================================================
% examples

% The Gibonacci function
% All type annotations could be replaced by logic variables; they
% will be inferred

gib = l int [x:exp q0] l int [y] 
    fix @ l int=>int [self] l int [k]
     (ifz k x 
       (ifz (dec k) y
         (self @ dec (dec k) + self @ dec k))).


% Staged Gibonacci

gibs = l &int [x:exp q0] l &int [y] 
    fix @ l TS [self] l int [k]
     (ifz k x 
       (ifz (dec k) y
         (^ (~ (self @ dec (dec k)) + ~ (self @ dec k))))).

gibs3 = ^ (l int [x] l int [y] ~ (gibs @ ^ x @ ^ y @ n3)).


% ========================================================================
% 			Dynamic Semantics

% ----------------------------------------------------------------------
% Some expressions are classified as values.

val: {A} exp A -> type.			%name val V.
%mode val +A +E.
%block bl-ev    : block {e:exp q1} {v:val q1 e}.

val-n: val _ (n _).			% Literals are values at each level
val-f: val _ fix.			% A constant: trivially a value
val-F: val _ fst.			% A constant: trivially a value
val-S: val _ snd.			% A constant: trivially a value

% values at the empty level
val-l0: val q0 (l _ _).

val-c:  val A (cons E1 E2)		% A pair of values is a value, at 
	<- val A E1			% every level.
	<- val A E2.

% Homomorphisms at any level (but in our calculus, only permitted at level 0)
val-^: val q0 (^ E) <- val q1 E.

% Values at the non-empty level: basically, the absence of 0-level escapes
	% homomorphisms...
val-l+: val q1 (l _ E) 
	<- {x:exp q1} val q1 x -> val q1 (E x).
val-@+: val q1 (E1 @ E2) 
	<- val q1 E2
	<- val q1 E1.
val-++: val q1 (E1 + E2) 
	<- val q1 E2
	<- val q1 E1.

val-d+: val q1 (dec E) 
	<- val q1 E.
val-i+: val q1 (ifz E1 E2 E3) 
	<- val q1 E3
	<- val q1 E2
	<- val q1 E1.

val-?+: val q1 (? E) 
	<- val q1 E.

val-r+: val q1 (deru _ ([h] h) E) 
	<- val q1 E.

%worlds (bl-ev) (val _ _).
%terminates {E} (val _ E).

% ----------------------------------------------------------------------
% 			Transitions
% The function eval is only defined on non-values.
%
% The transitions below fall into several groups:
%  - `semantic' transitions, e.g. the beta-v reduction or the addition of
%    two literal numbers: see ev-@ or ev-+
%  - congruences at level 0 (for actual evaluation) or polymorphic
%    congruences:
%    ev-@1 and ev-@2 (suffix 1 means left-argument congruence, suffix 2
%    stands for the right-argument congruence, if such exists)
%  - congruences at level 1 (used for processing of embedded escapes)
%    For operations like dec or +, level 1 and level 0 congruences are
%    the same and can be stated level-polymorphically. However,
%    lambda has the congruence only at level 1 (see ev-l3) because
%    the lambda form is a value at level 0.
%    The last two arguments of `if' have congruences only at level 1.
%    The names of these congruence rules have suffixes 3, 4, or 5.
%  - shift-expansion congruences. Shift is implemented in the `expansion'
%    style, in the manner of lambda-mu calculus.
%    Shift congruences at level 0 have names ending with X, Y or Z;
%    Shift congruences at level 1 (expansion of shift within an escape)
%    have names ending with U, V, W.

eval : {A} exp A -> exp A -> type.
%mode eval +A +E1 -E2.

% congruences

% 2-arg conruences
cong2 : (exp A -> exp A -> exp A) -> exp A -> exp A -> exp A -> type.
%mode cong2 +Form +EArg1 +Earg2 -ER.

cg2-1 : cong2 F (E1:exp A) E2 (F E1' E2)
     <- eval A E1 E1'.
cg2-2 : cong2 F (E1:exp A) E2 (F E1 E2')
     <- val A E1
     <- eval A E2 E2'.
cg2-X : cong2 F ((deru S C E):exp q0) E2 (deru S ([x] (F (C x) E2)) E).
cg2-Y : cong2 F (E1:exp q0) (deru S C E) (deru S ([x] (F E1 (C x))) E)
     <- val q0 E1.
cg2-U : cong2 F ((~ (deru S C E)):exp q1) E2 
                (~ (deru S ([x] ^ (F (~ (C x)) E2)) E)).
cg2-V : cong2 F (E1:exp q1) (~ (deru S C E))
                (~ (deru S ([x] ^ (F E1 (~ (C x)))) E))
     <- val q1 E1.

% lambda introduces reset, implicitly...
% Thus lambda stops the expansion of shift within an escape
ev-lU : eval q1 (l TV [x] (~ (deru S (C x) (E x)))) 
                (l TV [x] (~ (? (deru S (C x) (E x))))).

ev-l3 : eval q1 (l TV E) (l TV E')
      <- {x:exp q1} val q1 x -> eval q1 (E x) (E' x).


ev-@ : eval q0 ((l _ E1B) @ E2) (E1B E2)
     <- val q0 E2.

ev-@C: eval A (E1 @ E2) ER
     <- cong2 ([e1] [e2] e1 @ e2) E1 E2 ER.

% these are delta-rules for constants

ev-f : eval q0 (fix @ (l TV E)) (E (fix @ (l TV E))).

ev-F : eval q0 (fst @ (cons E1 E2)) E1
	<- val q0 E1
	<- val q0 E2.
ev-S : eval q0 (snd @ (cons E1 E2)) E2
	<- val q0 E1
	<- val q0 E2.

ev-+ : eval q0 ((n N1) + (n N2)) (n N)
	<- plus N1 N2 N.

ev-+C: eval A (E1 + E2) ER
     <- cong2 ([e1] [e2] e1 + e2) E1 E2 ER.

% cons only has congruences
ev-cC: eval A (cons E1 E2) ER
     <- cong2 cons E1 E2 ER.


ev-d : eval q0 (dec (n N1)) (n N)
	<- pred N1 N.

ev-d1 : eval A (dec E) (dec E')
	<- eval A E E'.

ev-dX : eval q0 (dec (deru S C E)) (deru S ([x] dec (C x)) E).
ev-dU : eval q1 (dec (~ (deru S C E))) (~ (deru S ([x] ^ (dec (~ (C x)))) E)).


ev-iz: eval q0 (ifz (n 0) E1 E2) E1.	% ifz delta rules
ev-ip: eval q0 (ifz (n (1 N)) E1 E2) E2.

ev-i1 : eval A (ifz E1 E2 E3) (ifz E1' E2 E3)
	<- eval A E1 E1'.
ev-i4 : eval q1 (ifz E1 E2 E3) (ifz E1 E2' E3)
        <- val q1 E1
	<- eval q1 E2 E2'.
ev-i5 : eval q1 (ifz E1 E2 E3) (ifz E1 E2 E3')
        <- val q1 E1
        <- val q1 E2
	<- eval q1 E3 E3'.

ev-iX : eval q0 (ifz (deru S C E) E2 E3) (deru S ([x] (ifz (C x) E2 E3)) E).

ev-iU : eval q1 (ifz (~ (deru S C E)) E2 E3) 
                (~ (deru S ([x] ^ (ifz (~ (C x)) E2 E3)) E)).
ev-iV : eval q1 (ifz E1 (~ (deru S C E)) E3)
                (~ (deru S ([x] ^ (ifz E1 (~ (C x)) E3)) E))
        <- val q1 E1.
ev-iW : eval q1 (ifz E1 E2 (~ (deru S C E)))
                (~ (deru S ([x] ^ (ifz E1 E2 (~ (C x)))) E))
        <- val q1 E1
        <- val q1 E2.


ev-~ : eval q1 (~ ^ E) E <- val q1 E.	% splicing

ev-~1 : eval q1 (~ E) (~ E')
      <- eval q0 E E'.

ev-^1 : eval q0 (^ E) (^ E')
      <- eval q1 E E'.

ev-^X : eval q0 (^ (~ (deru S C E))) (deru S ([x] (^ (~ (C x)))) E).


% reset rules
ev-?v : eval q0 (? E) E 
      <- val q0 E.
ev-?r : eval q0 (? (deru U C E)) (? (E @ (l U [x] ? (C x)))).


ev-?1 : eval A (? E) (? E')
      <- eval A E E'.
ev-?U : eval q1 (? (~ (deru S C E))) (~ (deru S ([x] ^ (? (~ (C x)))) E)).


% shift only has congruences
ev-r3 : eval q1 (deru S C E) (deru S C E')
      <- eval q1 E E'.

%worlds (bl-ev) (eval _ _ _) (cong2 _ _ _ _).
%%terminates {E} (eval _ E _).
% certainly eval does not cover many things. It does not
% cover any values and it does not cover the naked shift. And it can get stuck.
%%covers eval +A +E1 -E2.


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

-: eval* E E <- val q0 E.
-: eval* E1 E2 <- eval q0 E1 E1' <- eval* E1' E2.


% ------------------------------------------------------------------------
% Running sample code

%query 1 2 eval* (gib @ n1 @ n1 @ n1) n1.

%query 1 2 eval* (gib @ n1 @ n1 @ n3) n3.
% %query 1 2 eval* (gib @ n1 @ n1 @ n4) n5.
% %query 1 2 eval* (gib @ n1 @ n1 @ n5) n8. % takes a bit of time

%query 1 2 eval* (gibs @ ^ n2 @ ^ n3 @ n3) R.
% R = ^ (n3 + (n2 + n3)).

%query 1 2 eval* gibs3
  (^ l int ([e:exp q1] l int ([e1:exp q1] e1 + (e + e1)))).


% tests of shift
ts1 = ? n0.
ts2 = ? (de S (l T [f] (f @ n0))).
ts3 = ? ((de S (l T1 [f] (f @ (l T [x] (x + n1))))) @ (n 0)).

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

%query 1 2 eval* ts3 n1.

% Danvy/Filinski's famous example
ts4 = ? (n1 + (? (n1 + (de S (l T [f] (n1 + (n1 + (f @ (f @ n0)))))) + n1))).

%query 1 2 eval* ts4 n7.

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

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

ts02 = ? ((de S1 (l _ [f] (n2 + (f @ (l T [x] x + n1))))) @ 
          (de S2 (l _ [g] n1))).
%query 1 2 eval* ts02 n3.


% This also shows the change in the answer-type...
ts03 = ? ((de S1 (l _ [f] (f @ (l T [x] x + n1)))) @ 
          (de S2 (l _ [g] (g @ n1)))).
%query 1 2 eval* ts03 n2.


ts04 = ? ((de S1 (l _ [f] (f @ (de S3 (l _ [f] (l T [x] x + n1)))))) @ 
          (de S2 (l _ [g] (g @ n0)))).
%query 1 2 eval* ts04 (l T [x] x + n1).

ts05 = ? ((de S1 (l _ [f] (f @ (de S3 (l _ [f] f @ (l T [x] x + n1)))))) @ 
          (de S2 (l _ [g] (g @ n0)))).
%query 1 2 eval* ts05 n1.

% patent changing of the answer-type...
tc01 = ? (n1 + (de S1 (l _ [f] (l T [x] (f @ x))))).
%query 1 2 eval* tc01 R.
% R = l U1 ([x:exp q0] l U2 ([x1:exp q0] ? (n1 + x1)) @ x).

ts8 = ? (n1 + ((l T [f] (f @ n0)) @ 
         (de S (l _ [k] (k @ (l T [x] x + n1)) + n1)))).

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

ts10 = ? (n1 + ((l T [f] (f @ n0)) @ 
          (de S (l _ [k] n1 + (k @ (de S2 (l _ [_] n0))))))).
%query 1 2 eval* ts10 n0. % In CBN: (n 1 0).

% shift across stages

tss1 = ? ^ (dec ~(de S (l _ [f] f))).
tss2 = tss1 @ ^ n2.

%query 1 2 eval* tss1 R.
% R = l U1 ([x:exp q0] ? ^ (~ ^ dec (~ x))).

%query 1 2 eval* tss2 (^ dec n2).

tss3 =  ^ (l int [x] dec ~(de S (l T [f] ^((~ (f @ ^ x)) + (~ (f @ ^ x)))))).
%query 1 2 eval* tss3 R.
% R = ^ l int ([e:exp q1] dec e + dec e).

% realistic example requiring answer-type polymorphism
tpoly = de SL (l _ [k:exp q0] l T [table] (k @ (table @ n1) @ table)).
tpoly1 = tpoly @ n2.
tpoly2 = (? ((l T1 [v] l T2 [table] v) @ (tpoly1))) @ 
         (l T3 [v1] l T4 [v2] v1 + 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 @ (de S (l T [k] k @ (l T2 [self] n1))).
%query 1 2 eval* tcong2 n1.

% pairs

tpair1 = ? (fst @ (cons (de S (l _ [k] k @ n1)) (de S (l _ [k] k @ n2)))).
%query 1 2 eval* tpair1 n1.
tpair2 = ? (snd @ (cons (de S (l _ [k] k @ n1)) (de S (l _ [k] k @ n2)))).
%query 1 2 eval* tpair2 n2.


% ------------------------------------------------------------------------
% Type system

% `Unify' the two types and reconcile their effects
ajoin : exp A -> exp A -> exp A -> type.
%mode ajoin +E1 +E2 -E3.

aj-00: ajoin (apure U) (apure U)     (apure U).
aj-01: ajoin (apure U) (a2 U UA)     (a2 U UA).
aj-02: ajoin (apure U) (a21 U UA UF) (a21 U UA UF).
aj-03: ajoin (apure U) (a11 U UF)    (a11 U UF).

aj-10: ajoin (a2 U UA) (apure U)     (a2 U UA).
aj-11: ajoin (a2 U UA) (a2 U UA)     (a2 U UA).
aj-12: ajoin (a2 U UA) (a21 U UA UF) (a21 U UA UF).
aj-13: ajoin (a2 U UA) (a11 U UF)    (a21 U UA UF).

aj-20: ajoin (a21 U UA UF) (apure U)     (a21 U UA UF).
aj-21: ajoin (a21 U UA UF) (a2 U UA)     (a21 U UA UF).
aj-22: ajoin (a21 U UA UF) (a21 U UA UF) (a21 U UA UF).
aj-23: ajoin (a21 U UA UF) (a11 U UF)    (a21 U UA UF).

aj-30: ajoin (a11 U UF) (apure U)     (a11 U UF).
aj-31: ajoin (a11 U UF) (a2 U UA)     (a21 U UA UF).
aj-32: ajoin (a11 U UF) (a21 U UA UF) (a21 U UA UF).
aj-33: ajoin (a11 U UF) (a11 U UF)    (a11 U UF).

%worlds () (ajoin _ _ _).
%terminates {} (ajoin _ _ _).

% `Transfer' effects from the type T1 to the type T2.
% That is, make type T2 at least as effectful as T1, with the same answer
% types
amove-effects: exp A -> exp A -> exp A -> type.
%mode amove-effects +E1 +E2 -E3.

am-00: amove-effects (apure _) E E.

am-10: amove-effects (a2 _ UA) (apure U2)     (a2 U2 UA).
am-11: amove-effects (a2 _ UA) (a2 U2 UA)     (a2 U2 UA).
am-12: amove-effects (a2 _ UA) (a21 U2 UA UF) (a21 U2 UA UF).
am-13: amove-effects (a2 _ UA) (a11 U2 UF)    (a21 U2 UA UF).

am-20: amove-effects (a21 _ UA UF) (apure U2)     (a21 U2 UA UF).
am-21: amove-effects (a21 _ UA UF) (a2 U2 UA)     (a21 U2 UA UF).
am-22: amove-effects (a21 _ UA UF) (a21 U2 UA UF) (a21 U2 UA UF).
am-23: amove-effects (a21 _ UA UF) (a11 U2 UF)    (a21 U2 UA UF).

am-20: amove-effects (a11 _ UF) (apure U2)     (a11 U2 UF).
am-21: amove-effects (a11 _ UF) (a2 U2 UA)     (a21 U2 UA UF).
am-22: amove-effects (a11 _ UF) (a21 U2 UA UF) (a21 U2 UA UF).
am-23: amove-effects (a11 _ UF) (a11 U2 UF)    (a11 U2 UF).

%worlds () (amove-effects _ _ _).
%terminates {} (amove-effects _ _ _).

% Determine the base type, sans any effects
base-type: exp A -> tp -> type.
%mode base-type +E -U.
-: base-type (apure U) U.
-: base-type (a2 U _)  U.
-: base-type (a21 U _ _) U.
-: base-type (a11 U _) U.
%worlds () (base-type _ _).
%terminates {} (base-type _ _).


% Abstract values (which are types....)
avalue : exp A -> type.
%mode avalue +E.
-: avalue (apure U).
-: avalue (a2 U1 U2).
-: avalue (a11 U1 U2).
-: avalue (a21 U1 U2 U3).
-: avalue fix.				% polymorphic constants
-: avalue fst.
-: avalue snd.
%worlds () (avalue _).
%terminates {} (avalue _).


% One-step type-checking evaluator. It reduces terms to abstract terms,
% one step at a time. Like eval, teval is not defined on abstract
% values.

teval: exp A -> exp A -> type.
%mode teval +E -T.

tv-n: teval (n _) (apure int).

tv-d0: teval (dec (apure int)) (apure int).
tv-d1: teval (dec (a2 int U)) (a2 int U).
tv-d2: teval (dec (a21 int U1 U2)) (a21 int U1 U2).
tv-d3: teval (dec (a11 int U2)) (a11 int U2).

tv-dX: teval (dec E) (dec E')
       <- teval E E'.

% addition takes a while: all combinations of differently effectful
% operands
tv-+0: teval (E1 + E2) EJ
	<- ajoin E1 E2 EJ
	<- ajoin (apure int) EJ _.

tv-+X: teval (E1 + E2) (E1' + E2)
       <- teval E1 E1'.
tv-+Y: teval (E1 + E2) (E1 + E2')
       <- avalue E1
       <- teval E2 E2'.

% pairs
tv-c0: teval (cons E1 E2) ER
       <- base-type E1 U1 
       <- base-type E2 U2
       <- amove-effects E1 (apure (U1 * U2)) ER1
       <- amove-effects E2 ER1 ER.

tv-cX: teval (cons E1 E2) (cons E1' E2)
       <- teval E1 E1'.
tv-cY: teval (cons E1 E2) (cons E1 E2')
       <- avalue E1
       <- teval E2 E2'.


% conditional
tv-i0: teval (ifz E E1 E2) R
	 <- ajoin (apure int) E _
	 <- ajoin E1 E2 EJ
	 <- amove-effects E EJ R.

tv-iX: teval (ifz E E1 E2) (ifz E' E1 E2)
	 <- teval E E'.
tv-iY: teval (ifz E E1 E2) (ifz E E1' E2)
	 <- avalue E
	 <- teval E1 E1'.
tv-iZ: teval (ifz E E1 E2) (ifz E E1 E2')
	 <- avalue E
	 <- avalue E1
	 <- teval E2 E2'.

% application is very extensive

% A helper function: application judggement at base types
teval-apply-aux: {A:qual} tp -> tp -> exp A -> type.
%mode teval-apply-aux +A +T1 +T2 -E.
ta-pure: teval-apply-aux A (U => U1) U (apure U1).
ta-eff : teval-apply-aux A (U *> U1 / U2) U (a2 U1 U2).
%worlds () (teval-apply-aux _ _ _ _).
%terminates {} (teval-apply-aux _ _ _ _).

tv-@: teval ((E1 @ E2):exp A) ER
	<- base-type E1 UOP
	<- base-type E2 UARG
	<- teval-apply-aux A UOP UARG ER1
	<- amove-effects E1 ER1 ER2
	<- amove-effects E2 ER2 ER.


% The rules for polymorhic constants
tv-@f: teval (fix @ E) ER
       <- base-type E (TV => TV)	% TV is an arrow type
       <- amove-effects E (apure TV) ER.

tv-@F: teval (fst @ E) ER
       <- base-type E (U1 * U2)
       <- amove-effects E (apure U1) ER.

tv-@S: teval (snd @ E) ER
       <- base-type E (U1 * U2)
       <- amove-effects E (apure U2) ER.


tv-@X: teval (E1 @ E2) (E1' @ E2)
       <- teval E1 E1'.
tv-@Y: teval (E1 @ E2) (E1 @ E2')
       <- avalue E1
       <- teval E2 E2'.

% abstraction
% The type of lambda is always pure, even at level 1 and even
% if the body may contain escapes with shift

tv-l:  teval (l U E) (al U (E (apure U))).

tv-l0: teval (al U (apure UR)) (apure (U => UR)).
tv-l1: teval (al U (a2 UR UA)) (apure (U *> UR / UA)).

% Level-0 effects can't propagate out of the body of level-1 lambda
tv-l2: teval (al U (a21 UR UA (&& UR / UA))) (apure (U *> UR / UA)).
tv-l3: teval (al U (a11 UR (& UR)))          (apure (U => UR)).

tv-lX: teval (al T E) (al T E')
      <- teval E E'.


% control
tv-?0: teval (? (apure U)) (apure U).
tv-?1: teval (? (a2 U U))  (apure U).
tv-?2: teval (? (a21 U U U2))  (a11 U U2).
tv-?2: teval (? (a11 U U2))  (a11 U U2).

tv-?X: teval (? E) (? E')
      <- teval E E'.


tv-r:  teval (deru U C E) (ar U (C (apure U)) E).

% Just like in lambda, the effects of escapes in the body of shift
% cannot cross the body of shift. The binder for shift's variable
% stops the effects.
% Although in the form (de S E), E may be an arbitrary expression
% yielding a function, we restrict it to be a pure expression. Most
% of the times is just lambda-expression anyways. That does not limit
% expressiveness in any way.

tv-r01: teval (ar U EC (apure ((U => UA) => UA))) ER
	<- amove-effects (a2 int UA) EC ER. % int is chosen arbitrary, it
                                            % is disregarded by amove-effects

tv-r02: teval (ar U EC (apure ((U => UA) *> UA / UA))) ER
	<- amove-effects (a2 int UA) EC ER.

tv-rX: teval (ar U EC E) (ar U EC' E)
      <- teval EC EC'.
tv-rY: teval (ar U EC E) (ar U EC E')
       <- avalue EC 
       <- teval E E'.


% staging
tv-^0: teval (^ (apure U)) (apure (& U)).
tv-^1: teval (^ (a2 U1 U2)) (apure (&& U1 / U2)).
tv-^2: teval (^ (a21 U1 U2 UF)) (a2 (&& U1 / U2) UF).
tv-^3: teval (^ (a11 U1 UF)) (a2 (& U1) UF).

tv-^X: teval (^ E) (^ E')
      <- teval E E'.

tv-~0: teval (~ (apure (& U))) (apure U).
tv-~1: teval (~ (apure (&& U1 / U2))) (a2 U1 U2).
tv-~2: teval (~ (a2 (& U) UF)) (a11 U UF).
tv-~3: teval (~ (a2 (&& U1 / U2) UF)) (a21 U1 U2 UF).

tv-~X: teval (~ E) (~ E')
      <- teval E E'.

%worlds () (teval _ _).
%terminates {E} (teval E _).
%%covers teval +E -T.	% abstract values should not be covered!


% Transitive closure of teval

teval*: exp A -> exp A -> type.
%mode teval* +E -T.
-: teval* E E  <- avalue E.
-: teval* E E' <- teval E E1 <- teval* E1 E'.
%worlds () (teval* _ _).


% Type checking sample expressions

%query 1 2 teval* (^ (l int [x] dec x + n1)) (apure (& (int => int))).

%query 1 2 teval* 
    (fix @ l int=>int [self] l int [k]
      (self @ dec (dec k) + self @ dec k))
    (apure (int => int)).

% There are effectful and effect-free code types
%query 2 2 teval* 
    (fix @ l T [self] l int [k]
      (^ (~ (self @ dec (dec k)) + ~ (self @ dec k))))
    R.

%query 1 1 teval* (l int [x:exp q0] l int [y] 
    fix @ l int=>int [self] l int [k]
     (ifz k x 
       (ifz (dec k) y n0)))
  (apure (int => int => int => int)).

%query 1 1 teval* gib (apure (int => int => int => int)).
gibs = [TS] l &int [x:exp q0] l &int [y] 
    fix @ l TS [self] l int [k]
     (ifz k x 
       (ifz (dec k) y
         (^ (~ (self @ dec (dec k)) + ~ (self @ dec k))))).
%query 1 1 teval* (gibs TS) R.
%query 1 1 teval* (gibs TS)
       (apure (&int => &int => int => &int)).

gibs3 = ^ (l int [x] l int [y] ~ (gibs TS @ ^ x @ ^ y @ n3)).
%query 1 1 teval* gibs3 R.
% R = apure (& (int => int => int)).

%query 1 2 teval* ts1 (apure int).
%query 1 2 teval* ts2 (apure int).
%query 1 2 teval* ts3 (apure int).
%query 1 2 teval* ts4 (apure int).	% Danvy/Filinski's test

%query 1 2 teval* ts6' (a2 int int).
%query 1 2 teval* ts01 (apure int).
%query 1 2 teval* ts02 (apure int).
%query 1 2 teval* ts03 (apure int).

% shift across stages

%query 0 2 teval* tss1 R.	% requires change in the answer-type
%query 1 2 teval* (? ^ (dec ~(de S (l T [f] f @ ^ n2)))) (apure (& int)).
%query 1 2 teval* tss3 (apure (& (int => int))).

% Both => and *> arrows are inferred
%query 2 2 teval* tpoly R.
% R = a2 U1 ((int => U1) => U2).
% R = a2 U1 ((int => U1) *> U3 / U4).

%query 1 1 teval* tpoly1 R.
% a2 U1 ((int => int => U1) => U2).

%query 1 2 teval* tpoly2 (apure int).

%query 1 2 teval* tcong1 (apure int).
%query 1 2 teval* tcong2 (apure int).
 
% pairs
%query 1 2 teval* tpair1 (apure int).
%query 1 2 teval* tpair2 (apure int).

% Examples from the paper

% Section on delimited continuations and staging

paper_ex1 = (? ((l TR [r] l TS [_] r) @
	        ^ (~ (de S1 (l TK1 [k] l TV [v] k @ v @ v)) +
	          ~ (de S1 (l TK1 [k] l TV [v] k @ v @ v))))) @
	    ^(n1 + n4).
%query 1 2 teval* paper_ex1 (apure &int).
%query 1 1 eval* paper_ex1 (^ (n1 + n4 + (n1 + n4))).

paper_ex2 = (? ((l TR [r] l TS [_] r) @
	        ^ (~ (de S1 (l TK1 [k] l TV [v] 
		         ^((l TV1 [t] ~(k @ ^ t @ ^ t)) @ ~ v))) +
	           ~ (de S1 (l TK1 [k] l TV [v] k @ v @ v))))) @
	    ^(n1 + n4).
%query 1 2 teval* paper_ex2 (apure &int).
%query 1 1 eval* paper_ex2 (^ (l U1 ([e:exp q1] e + e) @ (n1 + n4))).

% paper_ex1 with a binding. The binding `cuts' the mutation and makes the
% state inaccessible. The example becomes stuck and won't type either.
paper_ex3 = (? ((l TR [r] l TS [_] r) @
	        ^ (l TX [x]
		   ~ (de S1 (l TK1 [k] l TV [v] k @ v @ v)) +
	           ~ (de S1 (l TK1 [k] l TV [v] k @ v @ v))))) @
	    ^(n1 + n4).
%query 0 2 teval* paper_ex3 R.
%query 0 1 eval* paper_ex3 R.


% ------------------------------------------------------------------------
% Staged Gibonacci with memoization and let insertion
% Please see fib.ml

% compare two integers, return 0 if they are equal. Otherwise, return non-zero.

int-compare = [A] fix @
	      l int=>int=>int [self:exp A] 
	      l int [i1] l int [i2]
	      (ifz i1 i2 (ifz i2 i1 (self @ (dec i1) @ (dec i2)))).

%query 1 2 eval* (int-compare q0 @ n1 @ n2) n1.
%query 1 2 eval* (int-compare q0 @ n2 @ n1) n1.
%query 1 2 eval* (int-compare q0 @ n2 @ n2) n0.

%query 1 2 teval* (int-compare q0) (apure (int => int=>int)).


% Memoization table, with int keys and values of the type TV
% It is a function of the signature

memo-sig = [TV] int => (int * (int => TV)).

% memo key reduces to
% It returns (0, fun _ => omega) if the value is not found
% It returns (1, fun _ => v) if the value is found.

omega = [TV] fix @ l TV [self:exp q0] self.

%query 1 2 teval* (omega TV) (apure TV).

memo-empty = [TV] l int [key] (cons n0 (l int [_] omega TV)).

%query 1 2 teval* (memo-empty int) R.
% R = apure (int => int * (int => int)).

memo-ext = [TV]
  l (memo-sig TV) [memo]
  l int [key0:exp q0]
  l TV [val0]
  l int [key]
  (ifz (int-compare q0 @ key @ key0) (cons n1 (l int [_] val0)) (memo @ key)).

%query 1 1 teval* (memo-ext int) R.
% R = apure (memo-sig int => int => int => int => int * (int => int)).

top-fn = [TV] [body]
 (? ( (l TV [v]  l (memo-sig TV) [table] v) @ body)) @ (memo-empty TV).

%query 1 1 teval* (top-fn int n1) (apure int).

let = [A] [T] [e:exp A] [body] (l T body) @ e.

% Memoizing fixpoint combinator, unstaged
fix-memo = l TIF [f]
  (f @
    % memo
     (fix @ l TF [memo] l int [x]
       % do lookup x first
       let q0 TL 
        (de TL (l TSL [k] l (memo-sig int) [table] (k @ (table @ x) @ table)))
	([r]
	 ifz (fst @ r)
            % value not found
	    (let q0 int
	       (f @ memo @ x)	% compute the needed value
               ([v] 
	         % extend the table
	        de int (l TSE [k] l (memo-sig int) [table] k @ v @ 
                             (memo-ext int @ table @ x @ v))))
	    % value found
	    (snd @ r @ n0)))).

% Just to see the inferred types for the binders
%query 1 1 teval* 
 (l TIF [f]
  (f @
    % memo
     (fix @ l TF [memo] l int [x]
       % do lookup x first
       let q0 TL 
        (de TL (l TSL [k] l (memo-sig int) [table] (k @ (table @ x) @ table)))
	([r]
	 ifz (fst @ r)
            % value not found
	    (let q0 int
	       (f @ memo @ x)	% compute the needed value
               ([v] 
	         % extend the table
	        de int (l TSE [k] l (memo-sig int) [table] k @ v @ 
                             (memo-ext int @ table @ x @ v))))
	    % value found
	    (snd @ r @ n0)))
     )) R.



% Old comments, kept for record

% % The following is a simplified version of the above

% %query 1 1 teval* 
% ((de SL [k] l T [table] (k @ (table @ n1) @ table)) @
%  (l int [v] ifz n0 v (a2 int UA)) @
%  (l int [x] (l int [v] 
% 	   % extend the table
% 	   de (int / UA) [k] l T1 [table] n1) @
% 	 % compute the needed value
% 	 n1))
% R.

% %{
% That type-checks, but demonstrates the problem:
% The second shift has the answer-type T1 -> int.
% the function (l int [x] ...) that contains this shift has the type
% int *> int / (T1 => int).
% Therefore, the type T in the first shift contains the type
%   int *> int / (T1 => int)
% as the argument type. But type T is the part of the answer type of the
% first shift. The attempt to unify these types leads to occurs check.
% From another angle: both T1 and T must be the types of the same memoization
% table.

% The situation does not arize in OCaml because types do not contain
% the answer-types (and (T1 => int) shows up in the answer-type).

% R =
%    a2 U1
%       ((int => (int *> int / (T1 => int)) => (int *> int / (T1 => int)) => U1)
%           => U2);
% T1 = T1;
% UA = T1 => int;
% T = int => (int *> int / (T1 => int)) => (int *> int / (T1 => int)) => U1;
% SL =
%    ((int *> int / (T1 => int)) => (int *> int / (T1 => int)) => U1)
%       / ((int => (int *> int / (T1 => int)) => (int *> int / (T1 => int)) => U1)
%             => U2).
% }%

% Type checking the memoizing combinator
%query 1 1 teval* fix-memo R.
% R = apure (((int *> int / (memo-sig int => U1)) => int => int) => int => int).

% The Gibonacci function with memoization

gib-memo = l int [x:exp q0] l int [y] 
    fix-memo @ l int=>int [self] l int [k]
     (ifz k x 
       (ifz (dec k) y
         (self @ dec (dec k) + self @ dec k))).

%query 1 1 eval* (top-fn int (gib-memo @ n1 @ n1 @ n3)) n3.
% the following takes a while
%%query 1 1 eval* (top-fn int (gib-memo @ n1 @ n1 @ n4)) n5.
%%query 1 1 eval* (top-fn int (gib-memo @ n1 @ n1 @ n5)) n8.

%query 1 1 teval* gib-memo (apure (int => int => int => int)).


% Staged memoizing fixpoint combinator
fix-memo-staged = l TIF [f]
  (f @
    % memo
     (fix @ l TF [memo] l int [x]
       % do lookup x first; the same as in the unstaged case
       let q0 TL 
        (de TL (l TSL [k] l (memo-sig &int) [table] (k @ (table @ x) @ table)))
	([r]
	 ifz (fst @ r)
            % value not found
	    (let q0 &int
	       (f @ memo @ x)	% compute the needed value
               ([v] 
	         % extend the table
	        de &int (l TSE [k] l (memo-sig &int) [table] 
	        % let-insertion
                ^ (let q1 int (~ v)
		    [t] ~ (k @ (^ t) @ (memo-ext &int @ table @ x @ (^ t)))))))
	    % value found
	    (snd @ r @ n0)))).

%query 1 1 teval*
 (l TIF [f]
  (f @
    % memo
     (fix @ l TF [memo] l int [x]
       % do lookup x first; the same as in the unstaged case
       let q0 TL 
        (de TL (l TSL [k] l (memo-sig &int) [table] (k @ (table @ x) @ table)))
	([r]
	 ifz (fst @ r)
            % value not found
	    (let q0 &int
	       (f @ memo @ x)	% compute the needed value
               ([v] 
	         % extend the table
	        de &int (l TSE [k] l (memo-sig &int) [table] 
	        % let-insertion
                ^ (let q1 int (~ v)
		    [t] ~ (k @ (^ t) @ (memo-ext &int @ table @ x @ (^ t)))))))
	    % value found
	    (snd @ r @ n0)))
     )) R.

% R = apure
%    (((int *> &int / (memo-sig &int => & U1)) => int => &int) => int => &int);
% TSE = & int => (int => int * (int => &int)) => & U1;
% TSL = int * (int => &int) => memo-sig &int => & U1;
% TL = int * (int => &int);
% TF = int *> &int / (memo-sig &int => & U1);
% TIF = (int *> &int / (memo-sig &int => & U1)) => int => &int.



% The staged Gibonacci function with memoization

gibs-memo = l &int [x:exp q0] l &int [y] 
    fix-memo-staged @ l (int => &int) [self] l int [k]
     (ifz k x 
       (ifz (dec k) y
         (^ (~ (self @ dec (dec k)) + ~ (self @ dec k))))).

%query 1 1 teval* gibs-memo (apure (&int => &int => int => &int)).


gibs3-memo = ^ (l int [x] l int [y] 
  ~ (top-fn &int (gibs-memo @ ^ x @ ^ y @ n3))).

gibs4-memo = ^ (l int [x] l int [y] 
  ~ (top-fn &int (gibs-memo @ ^ x @ ^ y @ n4))).


%query 1 1 teval* gibs3-memo R.
% R = apure (& (int => int => int)).

%query 1 1 eval* gibs3-memo
   (^
      l int
         ([e:exp q1]
             l int
                ([e1:exp q1]
                    l int
                       ([e2:exp q1]
                           l int
                              ([e3:exp q1]
                                  l int ([e4:exp q1] e2 + e4) @ (e3 + e2)) @ e)
                       @ e1))).

% I took the result produced by gibs3-memo, and removed the quotation mark:
% and replaced q1 with q0:
gibs3-memo-unquoted =
      l int
         ([e:exp q0]
             l int
                ([e1:exp q0]
                    l int
                       ([e2:exp q0]
                           l int
                              ([e3:exp q0]
                                  l int ([e4:exp q0] e2 + e4) @ (e3 + e2)) @ e)
                       @ e1)).

%query 1 2 teval* gibs3-memo-unquoted (apure (int => int => int)).
%query 1 1 eval* (gibs3-memo-unquoted @ n1 @ n2) n5. % x + 2y = 1 + 2*2


%%query 1 1 eval* gibs4-memo R.
%{ takes a while to compute
R =
   ^
      l int
         ([e:exp q1]
             l int
                ([e1:exp q1]
                    l int
                       ([e2:exp q1]
                           l int
                              ([e3:exp q1]
                                  l int
                                     ([e4:exp q1]
                                         l int ([e5:exp q1] e4 + e5) @ 
                                                         (e3 + e4))
                                     @ (e2 + e3))
                              @ e1)
                       @ e)).

}%

% Here is the unsafe example gibs3-memo-bad, from the end of fib.ml
% It is like gibs3-memo, only gibs-memo is placed inside a binding form

% Twelf still has a few bugs when it comes to implicit parameters
% and abbreviations.
% The following is the same as fix-memo-staged but with all type
% variables explicit.
fix-memo-staged = [TF] [TL] [TSL] [TSE] l (TF => int => &int) [f]
  (f @
    % memo
     (fix @ l TF [memo] l int [x]
       % do lookup x first; the same as in the unstaged case
       let q0 TL 
        (de TL (l TSL [k] l (memo-sig &int) [table] (k @ (table @ x) @ table)))
	([r]
	 ifz (fst @ r)
            % value not found
	    (let q0 &int
	       (f @ memo @ x)	% compute the needed value
               ([v] 
	         % extend the table
	        de &int (l TSE [k] l (memo-sig &int) [table] 
	        % let-insertion
                ^ (let q1 int (~ v)
		    [t] ~ (k @ (^ t) @ (memo-ext &int @ table @ x @ (^ t)))))))
	    % value found
	    (snd @ r @ n0)))).

gibs-memo = [TF] [TL] [TSL] [TSE] l &int [x:exp q0] l &int [y] 
    fix-memo-staged TF TL TSL TSE @ l (int => &int) [self] l int [k]
     (ifz k x 
       (ifz (dec k) y
         (^ (~ (self @ dec (dec k)) + ~ (self @ dec k))))).

gibs3-memo-bad = ^ (l int [x] l int [y] 
  ~ (top-fn &int 
     ( ^(let q1 int (y + n1)
           [z] ~(gibs-memo TF TL TSL TSE @ ^ x @ ^ z @ n3))))).

% It does not run, nor does it type check.
%query 0 1 eval* gibs3-memo-bad R.
%query 0 1 teval* gibs3-memo-bad R. % takes a while



% if- and assertion-insertion

% the generator in a direct style
gen = l T1 [suba]
    ^(l int=>int [arr] l int [i]
       (n1 + n2)			% simulating complex expression
       + ~(suba @ ^ arr @ ^ i)).

%query 1 1 teval* gen R.
% R = apure ((& int=>int => & int => & int) => & (int=>int => int => int)).

suba = l (& int=>int) [arr] l &int [i]
    (de S (l T [k] 
     ^(ifz (~ i) (fix @ l TO [self] self)  % omega emulates assertion failure
        ~(k @ ^( (~ arr) @ (~ i)))))).

%query 1 1 teval* suba R.
% R = apure (& int=>int => &int *> (& int) / (& U1)).

% It type-checks!
%query 1 1 teval* (gen @ suba) 
 (apure (& (int=>int => int => int))).

% And runs. if- is inserted at the front!
%query 1 1 eval* (gen @ suba) R.
%{
R = ^ l int=>int
         ([e:exp q1]
             l int
                ([e1:exp q1]
                 ifz e1 (fix @ l U1 ([self:exp q1] self)) (n1 + n2 + e @ e1))).
}%