% A strictly two-level lambda-a1v calculus based on lambda-a of
% Taha and Nielsen's `Environment Classifiers' (POPL03).
% The lambda-a1v calculus is introduced in our PEPM08 paper. The calculus
% permits writing code generators but specifically precludes writing generators
% of generators. For historical reasons, we call classifiers qualifiers here.
%
% Since our calculus (unlike the full lambda-a) is restricted, there
% is a temptation to `improve' the reduction and the typing rule
% for run. The original lambda-a defines a reduction:
%	run (alpha) <e>^alpha --> (alpha) e
% We may be tempted to replace this with the following
%       run (alpha) <e>^alpha --> e, provided e has no occurrence of alpha
% with the corresponding typing rule
%       G |- e : (alpha) <t>^alpha ==> G |- run e : t
% which implies that t does not have any occurrence of alpha.
% Incidentally, the lambda-i calculus in Walid's et al (ESOP04 paper)
% does have this simplified reduction rule for run.
% Alas, we cannot adopt it, because in our calculus, like in the original
% lambda-a (POPL03), classifiers may occur in terms. Furthermore,
% a term that contains a classifier will not necessarily have a type
% containing the classifier. Thus we would not be able to prove
% progress. Here is the counter-example:
%	run (alpha) <csp (((beta) 1) @q alpha)>^alpha
% The expression in brackets has the type int, but it does contain
% the occurrence of alpha and hence cannot be reduced according to the
% simplified rule for run. The original rule for run does apply, yielding
% (alpha) ((beta) 1 @q alpha) and then (alpha) 1.
%
% Our lambda-a1v paper however does exclude the above counter-example,
% using a special typing rule for CSP: we require that the CSP expression
% be typeable in the environment without alpha -- the classifier of the
% code expression in which CSP appears. The previous version of this
% file indeed tried to express such a typing rule. In that we succeeded:
% we had to introduce special `names' to `mark' places in the LF context.
% When typing CSP, we retrieve from the LF context the name of the 
% context that existed right before the classifier alpha was introduced.
% We then require the expression to lift to be typeable in that
% earlier context. Again, that worked: the examples exrun1 and exrun2
% below were rejected by the type-checker, and exrun3 was accepted -- 
% just as we wanted.
%
% That earlier approach did require asserting many facts that the context
% labels form an order. Alas, proving type preservation in that setting
% turned out too difficult: Our typing rules had to include a weakening
% rule of-w. Otherwise, we can't type, for example, (l [x] ll [alpha] x).
% Here x is bound at the environment without alpha and is used in the 
% weakened environment with alpha. The weakening rule `contaminates' 
% the preservation proof by essentially destroying canonical forms: 
% given an integer literal (N n), it's typing derivation is no longer 
% the single (of-: of (N n) int). Rather, it can include the arbitrarily
% long sequences of of-w: (of-w (of-: of (N n) int)), etc. The weakening
% rule also complicates the termination analysis by destroying
% simple structural recursion for derivations (we need to recur under of-w).
% Twelf's termination checker can't handle that. Even proving that 
% typechecking terminates becomes more involved, as we need to show 
% that our context labels form a (pre-order) and so there is a minimal 
% element or elements. Twelf's built-in termination checker cannot do 
% such an analysis automatically.
%
% In the present version of this development, we chose a syntactic
% restriction on CSP: see csp-ok. The restriction is imposed by the typing
% rule for CSP, of-csp. The example exrun3 no longer types. The loss of
% expressiveness does not seem to be too noticeable as all the examples
% from the PEPM08 paper can still be typed. Examples like exrun3 do
% seem quite atypical.


% we assume util.elf has been loaded ...

% Qualifiers and qualifier sequences
qual: type.			%name qual A.

	% qualifier sequences: named levels
quals: type.			%name quals A.
qt : quals.			% empty sequence
1q : qual -> quals.		% sequence of one qualifier
				% (longer sequences are not permitted here)

% Types

tp: type.			%name tp T.

int: tp.			% one single primitive type for now.
=>: tp -> tp -> tp.		%infix right 200 =>.
all: (qual -> tp) -> tp.	% (alpha)t
<: tp -> qual -> tp.		%infix left 250 <. % <t>^alpha

% The restriction of the calculus to two levels must be stated
% at the level of types. See the PEPM08 paper for the discussion why
% stating the restriction only at the level of terms is not enough:
% even if we disallow nested brackets, with the help of CSP of the type code,
% we gain as many staging levels as we wish.
% The restriction is specified by the following predicate.
flat: quals -> tp -> type.
%mode flat +A +T.
fint: flat A int.
f=>:  flat A T1 -> flat A T2 -> flat A (T1 => T2). %infix right 200 f=>.
fall: ({alpha} flat qt (T alpha)) -> flat qt (all T).
f>:   {AL} flat (1q AL) T -> flat qt (T < AL).     %infix left 250 f>.


% Expressions. All expressions are labeled with their levels
exp: quals -> type.		%name exp E.

n  : nat -> exp A.			%prefix 110 n.
l  : flat A T -> (exp A -> exp A) -> exp A.	% lambda (x:t) body
@  : exp A -> exp A -> exp A.		%infix left 100 @.
fix: flat A TV -> flat A TB -> exp A.   % fix f (x:tv):tb body
+: exp A -> exp A -> exp A.		%infix left 154 +.
ll : (qual -> exp qt) -> exp qt.        % qualifier lambda: qual intro
@q : exp qt -> qual -> exp qt.		%infix left 100 @q. % qualifier appl
>: {AL:qual} exp (1q AL) -> exp qt.	%infix right 150 >.
~: exp qt -> exp (1q AL).
csp: exp qt -> exp (1q AL).
run: exp qt -> exp qt.

% fix is an applicative fixpoint combinator, defined as a polymorphic constant:
%  fix TV TB 
% with the type ((TV -> TB) -> (TV -> TB)) -> (TV -> TB)

% We used to treat qualifier introductions (ll e) as values, similar
% to lambdas. That made the context for run quite complex. We go back
% to Walid03 approach and permit evaluations under qualifier introduction.
% We need that anyway for `run (a)e', to make sure e evaluates to <e>.

% Here, we permit arguments of lambda, fix and csp to be arbitrary
% expressions. Our evaluation rules make sure that lambda and fix
% are invoked with values only. As to CSP, we simply refuse to evaluate
% E in <csp(E)>. So, effectively we treat csp(E) as (csp (fun () -> E)) ()
% That seems to avoid many complications. 

	% Common blocks
%block bl-a    : block {a:qual}.
%block bl-e    : some {A:quals} block {e:exp A}.

% ------------------------------------ examples 
% the first running example
% let id x = x in (alpha)<fun x -> ~(id <x>)>
% later on, insert fix into id to simulate the effect in id

idp = ll [beta] l (beta f> fint) [x:exp qt] x.
exr1 
  = (l (fall [beta] beta f> fint  f=>  beta f> fint) [id:exp qt]
        (ll [alpha] alpha > l fint [x]
	~(id @q alpha @ alpha > x)))
    @ idp.

% The famous eta (specialized for int)
% (alpha)(fun f -> <fun x -> ~(f <x>)>)
% and its applications

eta = ll [alpha] l (alpha f> fint  f=>  alpha f> fint) [f: exp qt]
	           (alpha > l fint [x] ~(f @ alpha > x)).

etax1 = ll [alpha] alpha > l fint [y:exp (1q alpha)]
	 ~( eta @q alpha @ 
            (l (alpha f> fint) [q] (alpha > (~ q + y)))).

ex11 = ll [alpha] (alpha > l fint [y:exp (1q alpha)]
	 ~( alpha > (n 0) + y) ).

ex21 = ll [alpha] (alpha > l fint [y:exp (1q alpha)]
	 ~( (l (alpha f> fint) [q] (alpha > (~ q + y))) @ 
	    (alpha > n 0))).

% More examples, of code expression abstractions.

omega = fix fint fint @ 
          (l (fint f=> fint) [self:exp qt] l fint [x] self @ x) @ (n 0).

% .<fun x -> .~(let u = .<x>. in (.! .<fun y -> .<.~u>.>.) ()) >.;;

exrun = ll [alpha] alpha > l fint [x] 
         ~((l (alpha f> fint) [u]
	     ((run (ll [beta] beta >
			(l fint [y] csp u))) @q alpha)
	    @ n 0)
	@ alpha > x).

% the counter-example from the title comments
exrun1 = run (ll [alpha] alpha > csp ((ll [beta] (n 1 0)) @q alpha)).

exrun2 = run (ll [alpha] alpha > 
       csp ((run (ll [beta] beta > (n 1 0))) @q alpha)).

exrun3 = ll [gamma] run (ll [alpha] alpha > 
       	    	    csp ((run (ll [beta] beta > (n 1 0))) @q gamma)).


% ========================================================================
%			   Typechecking

of : exp A -> tp -> type.		%name of P.
%mode of +E -T.
%block bl-ofe : some {A:quals} {TV:tp} block {e:exp A} {tv:of e TV}.

% First, we define pure types (denoted u in the PEPM08 paper, Fig. 1)
puretp : tp -> type.
%mode puretp +T.
pt-i: puretp int.
pt-a: puretp (T1 => T2) <- puretp T2 <- puretp T1.
%worlds (bl-a | bl-ofe) (puretp _).
%terminates {T} (puretp T).

% Now, we define the syntactic restriction on CSP.
csp-ok: exp qt -> type.
%mode csp-ok +E.
csp-ok-i: csp-ok (n N).
csp-ok-l: csp-ok (l TV B) 
	  <- {e} csp-ok e -> csp-ok (B e).
csp-ok-f: csp-ok (fix _ _).
csp-ok-@: csp-ok (E1 @ E2)
	  <- csp-ok E2
	  <- csp-ok E1.
csp-ok-+: csp-ok (E1 + E2)
	  <- csp-ok E2
	  <- csp-ok E1.
% and that is it. We reject everything that includes qualifiers.
%block bl-csp-ok : block {e:exp qt} {ok:csp-ok e}.
%worlds (bl-a | bl-ofe | bl-csp-ok) (csp-ok _).
%terminates {E} (csp-ok E).

% of : exp A -> tp -> type.		%name of P.
% See the Fig 2. of the PEPM paper
of-i:  of (n N) int.

of-l:  of (l (_:flat A TV) EB) (TV => TB)
       <- ({e} of e TV -> of (EB e) TB).

of-fix: of (fix (_:flat A TV) (_:flat A TB)) 
           (((TV => TB) => (TV => TB)) => (TV => TB)).

of-+: of (E1 + E2) int
	<- of E2 int
	<- of E1 int.

of-@: of (E1 @ E2) T2 
	<- of E2 T1
	<- of E1 (T1 => T2).

of-L:  of (ll EP) (all TP) 
	<- {alpha:qual} of (EP alpha) (TP alpha).

of-@q: of (E @q AL) (TP AL)
	<- of E (all TP).

% Staging stuff. Some types are restricted to be pure
% For modality reasons, puretp must be the first argument of the family
% constructors (that is, appear the last as the <- puretp T) argument.
of-run: of (run E) (all [a] T)
	<- of E (all [a] (T < a))	% T does not depend on a
	<- puretp T.

of->: of (AL > E) (T < AL)
	<- of E T
        <- puretp T.

of-~: of ((~ E):exp (1q AL)) T
	<- of (E:exp qt) (T < AL)
        <- puretp T.

of-csp: of ((csp E):exp (1q AL)) T
	<- csp-ok E			% restricting CSP expressions
	<- of E T
	<- puretp T.

%worlds (bl-a | bl-ofe) (of _ _).
%terminates {E} (of E _).
%covers of +E -T.	% All expression cases are covered
			% `of' is certainly not total.


% ---------------------------- typing of the examples

%query 1 2 of (l fint [x:exp qt] x) (int => int).

%query 1 2 of ((l fint [x:exp qt] x) @ n 0) int.

%query 1 2 of (ll [alpha] (alpha > n 0)) R. % (all ([a:qual] int < a)).

%query 1 2 of idp (all ([a:qual] int < a => int < a)).


%query 1 2 of (ll [a] (ll [b] n 0) @q a) (all ([a:qual] int)).


%query 1 2 of exr1 (all ([a:qual] (int => int) < a)).

%query 1 2 (of eta T).
%query 1 2 of eta (all ([a:qual] (int < a => int < a) => (int => int) < a)).


%query 1 2 of ex21 (all ([a:qual] (int => int) < a)).

%query 1 2 of (run ex21) (all [a] (int => int)).

%query 1 2 of etax1 T.
% T = all ([a:qual] (int => int => int) < a).

%query 1 2 of (run etax1) (all [a] (int => int => int)).

%query 1 2 of omega int.

% %query 1 2 of exrun R. With the pure restriction, no longer types!
% R = all ([a:qual] (int => int) < a).

%query 0 2 of exrun1 R. % No longer types
%query 0 2 of exrun2 R. % No longer types

%%% XXX The downside of our syntactic restriction is that exrun3 no longer
% types...
%%query 1 1 of exrun3 (all ([a:qual] all ([a1:qual] int))). % Does type
%query 0 1 of exrun3 (all ([a:qual] all ([a1:qual] int))).


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

% ----------------------------------------------------------------------
% Classification of expressions: values and pre-values
% Some expressions are classified as values or pre-values.

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

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

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

% Homomorphisms at any level (but in our calculus, only permitted at level 0)
val-L: val qt (ll  E)  <- {q:qual} val qt (E q).
val->: val qt (AL > E) <- val (1q AL) E.

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

% CSP at 0 level are always values -- so `<%omega>' halts, as does `run <fun
% () -> %omega>', but not `run <%omega>'.  In other words, this CSP does not
% evaluate the persisted expression to a value.  If that evaluation is desired,
% we can write `%e' as `~(let v = e in <%v>)'.  In the other direction, if we
% had chosen to make CSP evaluate the persisted expression, then where that
% evaluation is not desired, we would write `%e' as `(%(fun () -> e))()'.
val-csp0: val (1q AL) (csp E).

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


% pre-values: the smallest non-values, aka candidate redexes
% With one exception (pv-~), all pre-vals are at the 0 level
pre-val: {A} exp A -> type.
%mode pre-val +A +E.

pv-@: pre-val qt (E1 @ E2) <- val qt E2 <- val qt E1.
pv-+: pre-val qt (E1 + E2) <- val qt E2 <- val qt E1.
pv-q: pre-val qt (E1 @q AL) <- val qt E1.
pv-~: pre-val (1q AL) (~ E) <- val qt E.
pv-r: pre-val qt (run E) <- val qt E.


% testing of code values and non-values
%query 1 1 val qt (AL > (n 0)).
%query 0 1 val qt (AL > ~(AL > n 0)).
% %query 1 1 val qt (AL > BL > ~(BL > n 0)).
% %query 0 1 val qt (AL > BL > ~(~(AL > BL > n 0))).
% %query 1 1 val qt (CL > AL > BL > ~(~(AL > BL > n 0))).
% %query 1 1 val qt (AL > BL > ~(BL > ~(BL > n 0))).



% ----------------------------------------------------------------------
% 			Transitions

% Demotion
% This function lowers the level of the expression, which is the essential
% operation in `run'. The non-trivial part is replacing (csp exp)
% with exp itself.
% The rest may seem trivial -- however, demoting under lambda requires
% a lot of hypothetical reasoning...
% Only level 1 values can be demoted (meaning, there cannot be any escapes)

demote-flat : flat (1q AL) T -> flat qt T -> type.
%mode demote-flat +F1 -F2.
dflat-i: demote-flat fint fint.
dflat-t: demote-flat (F1 f=> F2) (F1' f=> F2')
	 <- demote-flat F2 F2'
	 <- demote-flat F1 F1'.
%worlds (bl-a) (demote-flat _ _).
%total {F} (demote-flat F _).

demote : val (1q AL) E -> exp qt -> type.
%mode demote +V -E.
dn-n : demote (_:val _ (n N)) (n N).
dn-f : demote (_:val _ (fix TV TB)) (fix TV' TB')
        <- demote-flat TB TB'
        <- demote-flat TV TV'.
	% These are just homomorphisms
dn-@  : demote (val-@+ V1 V2) (E1' @ E2') 
	<- demote V2 E2'
	<- demote V1 E1'.
dn-+  : demote (val-++ V1 V2) (E1' + E2') 
	<- demote V2 E2'
	<- demote V1 E1'.
	% This is the one non-trivial thing
dn-c  : demote (_:val _ (csp E)) E.
	% This is too a homomorphism, but of higher-order expression
	% Lots of hypothetical reasoning...
dn-l : demote ((val-l+ D):val (1q AL) (l TV _)) (l TV' [x'] EB' x')
        <- demote-flat TV TV'
	<- {x:exp (1q AL)} {v:val (1q AL) x} {x':exp qt}
	   demote v x' -> 
	   demote (D x v) (EB' x'). 
%block bl-dn : some {AL:qual}
	       block
		  {x:exp (1q AL)} {v:val (1q AL) x} {x':exp qt}
	   	  {th:demote v x'}.
%worlds (bl-a | bl-dn) (demote _ _).
%covers demote +V -E.
%terminates {V} (demote V _).
% %total {V} (demote V _).


% Reduce a pre-value: one-step primitive evaluation
% Except for rx-~, all evaluation is at the level 0
ev-redex: pre-val A E -> exp A -> type.
%mode ev-redex +PV -E.
rx-@: ev-redex (pv-@ (_: val qt (l _ E1B)) (_:val qt E2)) (E1B E2).
rx-f: ev-redex (pv-@ (_: val qt (fix TV TB)) (_:val qt E2))
      (E2 @ (l TV [x] (fix TV TB @ E2 @ x))).
rx-+: ev-redex (pv-+ (_: val qt (n N1)) (_:val qt (n N2))) (n N)
	<- +nat N1 N2 N.
rx-q: ev-redex ((pv-q _):pre-val qt ((ll E1B) @q AL)) (E1B AL).
rx-~: ev-redex ((pv-~ _):pre-val (1q AL) (~ (AL > E))) E.

rx-r: ev-redex ((pv-r (val-L [a] (val-> (V a)))):
                 pre-val qt (run (ll [a] a > E a)))
               (ll [a] (R a))
      <- {a:qual} demote (V a) (R a).
%worlds (bl-a | bl-dn) (ev-redex _ _).
%terminates {} (ev-redex _ _).
% certainly ev-redex does not cover many things. It can get stuck.
%%covers ev-redex +PV -E.


% ----------------------------------------------------------------------
%		Focusing and full evaluation

% The motivation for the focusing function comes from the single-step
% congruent eval function.
% Let us consider the following eval function:
%    ev : exp A -> ev-result A -> type.
%    mode ev +E -R.
% where ev-result is the disjoint union
%    ev-result : quals -> type.
%    evr-value: val A E -> ev-result A.
%    evr-exp:   exp A -> ev-result A.
% That is, given an expression, ev checks if it is a value (and if so,
% returns the proof of that). If the argument is not a value, ev will
% try to reduce it a bit. Here's a sample clause for ev:
%    % E1 + E2 at a non-empty level
% -: ev (E1 + E2) (evr-value (val-++ PV1 PV2))
%	<- ev E1 (evr-value PV1) <- ev E2 (evr-value PV2).
%    % E1 + E2 at an empty-level, E1 and E2 are values
% -: ev (E1 + E2) (evr-exp R) 
%	<- ev E1 (evr-value PV1) <- ev E2 (evr-value PV2)
%	<- ev-redex (pv-+ PV1 PV2) R.
%    % congruences
% -: ev (E1 + E2) (evr-exp (E1' + E2)) <- ev E1 (evr-exp E1').
% -: ev (E1 + E2) (evr-exp (E1 + E2')) 
%	<- ev E1 (evr-value _) <- ev E2 (evr-exp E2').
%
% To turn ev into focusing, we merely need to return the prevalue
% rather than attempting to reduce it. Also, we CPS ev to make its continuation
% explicit. The continuation of redex is the context.



% unzipped expression:
% ouz A is the expression exp A with some identified
% sub-expression separated out. That separated-out piece must be a pre-value.
ouz: quals -> type.			%name ouz Z.
	% pre-value in the empty context
ouz-t: pre-val A E -> ouz A.
	% context does not cross any bindings
ouz-c: {B:quals} ouz B -> (exp B -> exp A) -> ouz A.
	% context crosses lambda
ouz-b:  flat A T -> ({x:exp A} val A x -> ouz A) -> ouz A.
	% context crosses the big lambda
ouz-a: ({AL:qual} ouz qt) -> ouz qt.

% The following union is the result of focusing
f-result: {A:quals} exp A -> type.
fr-val: val A E -> f-result A E.
fr-ouz: ouz A   -> f-result A E.

focus: {E:exp A} f-result A E -> type.  % forward declaration

%block bl-focusl : some {AL:qual} 
	block {x:exp (1q AL)} {v: val (1q AL) x}
	      {th:focus x (fr-val v)}.


% add more of the closed context to ouz
ouz-more: ouz B -> (exp B -> exp A) -> ouz A -> type.
%mode ouz-more +Z +C -ZR.
-: ouz-more ((ouz-t P):ouz B) C (ouz-c B (ouz-t P) C).
-: ouz-more (ouz-c B1 Z1 C1) C2 (ouz-c B1 Z1 ([e] C2 (C1 e))).
-: ouz-more ((ouz-b T P):ouz B) C (ouz-c B (ouz-b T P) C).
-: ouz-more ((ouz-a P):ouz qt) C (ouz-c qt (ouz-a P) C).
%worlds (bl-a | bl-focusl) (ouz-more _ _ _).
%total {Z} (ouz-more Z _ _).

% zip-up Z into the expression. This is the inverse of focusing
zip-up: ouz A -> exp A -> type.
%mode zip-up +Z -E.
-: zip-up (ouz-t (_:pre-val A E)) E.
-: zip-up (ouz-c B Z C) (C E') <- zip-up Z E'.
-: zip-up ((ouz-b T ([e] [v] Z e v)):ouz A) (l T E')
	<- {e:exp A} {v:val A e} zip-up (Z e v) (E' e).
-: zip-up (ouz-a ([q] Z q)) (ll E')
	<- {q:qual} zip-up (Z q) (E' q).
%worlds (bl-a | bl-ev) (zip-up _ _).
%total {Z} (zip-up Z _).

% evaluate the zipped-down expression
ev-ouz: ouz A -> exp A -> type.
%mode ev-ouz +Z -E.
-: ev-ouz (ouz-t PV) E <- ev-redex PV E.
-: ev-ouz (ouz-c B Z C) (C E') <- ev-ouz Z E'.
-: ev-ouz ((ouz-b T ([e] [v] Z e v)):ouz (1q AL)) (l T E')
	<- {e:exp (1q AL)} {v:val (1q AL) e} {e':exp qt}
	   {th:demote v e'} ev-ouz (Z e v) (E' e).
-: ev-ouz (ouz-a ([q] Z q)) (ll E')
	<- {q:qual} ev-ouz (Z q) (E' q).
%worlds (bl-a | bl-dn) (ev-ouz _ _).
%terminates {Z} (ev-ouz Z _).
% %covers ev-ouz +Z -E. We don't evaluate under lambda...

%%focus: exp A -> f-result A -> type.  % see the forward declaration above
%mode focus +E -FR.

-: focus ((n N):exp A) (fr-val (val-n:val A (n N))).

focus+: {E1:exp A} {E2:exp A} f-result A E1 -> f-result A E2
	-> f-result A (E1 + E2) -> type.
%mode focus+ +E1 +E2 +E1F +E2F -R.
-: focus+ E1 E2 (fr-val (V1:val (1q AL) _)) (fr-val (V2:val (1q AL) _))
	  (fr-val (val-++ V1 V2)).
-: focus+ E1 E2 (fr-ouz Z) _ (fr-ouz R) <- ouz-more Z ([e] (e + E2)) R.
-: focus+ E1 E2 (fr-val _) (fr-ouz Z) (fr-ouz R) 
	<- ouz-more Z ([e] (E1 + e)) R.
-: focus+ E1 E2 (fr-val (V1:val qt _)) (fr-val (V2:val qt _))
	  (fr-ouz (ouz-t (pv-+ V1 V2))).
%worlds (bl-a | bl-focusl) (focus+ _ _ _ _ _).
%total {F1 F2} (focus+ _ _ F1 F2 _).

-: focus (E1 + E2) R 
	<- focus E1 E1F <- focus E2 E2F 
	<- focus+ E1 E2 E1F E2F R.


focus@: {E1:exp A} {E2:exp A} f-result A E1 -> f-result A E2
	-> f-result A (E1 @ E2) -> type.
%mode focus@ +E1 +E2 +E1F +E2F -R.
-: focus@ E1 E2 (fr-val (V1:val (1q AL) _)) (fr-val (V2:val (1q AL) _))
	  (fr-val (val-@+ V1 V2)).
-: focus@ E1 E2 (fr-ouz Z) _ (fr-ouz R) <- ouz-more Z ([e] (e @ E2)) R.
-: focus@ E1 E2 (fr-val _) (fr-ouz Z) (fr-ouz R) 
	<- ouz-more Z ([e] (E1 @ e)) R.
-: focus@ E1 E2 (fr-val (V1:val qt _)) (fr-val (V2:val qt _))
	  (fr-ouz (ouz-t (pv-@ V1 V2))).
%worlds (bl-a | bl-focusl) (focus@ _ _ _ _ _).
%total {F1 F2} (focus@ _ _ F1 F2 _).

-: focus (E1 @ E2) R 
	<- focus E1 E1F <- focus E2 E2F 
	<- focus@ E1 E2 E1F E2F R.

-: focus ((l T E):exp qt) (fr-val (val-l0 : val qt (l T E))).

focusl+: {T:flat (1q AL) _}
	({x:exp (1q AL)} val (1q AL) x -> f-result (1q AL) (E x)) ->
	f-result (1q AL) (l T E) -> type.
%mode focusl+ +T +EF -EF'.
-: focusl+ T ([x] [v] (fr-val (V x v))) 
	   (fr-val ((val-l+ V):val _ (l T _))).
-: focusl+ T ([x] [v] (fr-ouz (Z x v))) (fr-ouz (ouz-b T Z)).
%worlds (bl-a | bl-focusl) (focusl+ _ _ _).
%total (C) (focusl+ _ C _).

-: focus ((l T E):exp (1q AL)) R
	<- ({x:exp (1q AL)} {v: val (1q AL) x} 
	    focus x (fr-val v) -> focus (E x) (EF x v))
	<- focusl+ T EF R.

focusL: ({q:qual} f-result qt (E q)) -> f-result qt (ll E) -> type.
%mode focusL +EF -EF'.
-: focusL ([q] (fr-val (V q))) (fr-val (val-L V)).
-: focusL ([q] (fr-ouz (Z q))) (fr-ouz (ouz-a Z)).
%worlds (bl-a | bl-focusl) (focusL _ _).
%total (C) (focusL C _).

-: focus ((ll E):exp qt) R
	<- ({q:qual} focus (E q) (EF q))
	<- focusL EF R.

focus@q: {AL:qual} f-result qt E -> f-result qt (E @q AL) -> type.
%mode focus@q +A +E1F -R.
-: focus@q BL (fr-val V1) (fr-ouz (ouz-t ((pv-q V1):pre-val qt (_ @q BL)))).
-: focus@q BL (fr-ouz Z) (fr-ouz R) <- ouz-more Z ([e] (e @q BL)) R.
%worlds (bl-a | bl-focusl) (focus@q _ _ _).
%total {F1} (focus@q _ F1 _).

-: focus (E1 @q AL) R 
	<- focus E1 E1F
	<- focus@q AL E1F R.

focus>: f-result (1q AL) E -> f-result qt (AL > E) -> type.
%mode focus> +E1F -R.
-: focus> (fr-val (V1:val (1q AL) _)) (fr-val ((val-> V1))).
-: focus> (fr-ouz Z) (fr-ouz R) <- ouz-more Z ([e] (AL > e)) R.
%worlds (bl-a | bl-focusl) (focus> _ _).
%total {F1} (focus> F1 _).

-: focus (AL > E) R
	<- focus E EF
	<- focus> EF R.


focus~: {BL:qual} f-result qt E -> f-result (1q BL) (~ E) -> type.
%mode focus~ +A +E1F -R.
-: focus~ BL (fr-val (V1:val qt _)) (fr-ouz (ouz-t (pv-~ V1))).
-: focus~ BL (fr-ouz Z) (fr-ouz R) <- ouz-more Z ([e] (~ e)) R.
%worlds (bl-a | bl-focusl) (focus~ _ _ _).
%total {F1} (focus~ _ F1 _).

-: focus ((~ E):exp (1q AL)) R
	<- focus E EF
	<- focus~ AL EF R.

-: focus ((fix TV TB):exp A) (fr-val (val-f : val A (fix TV TB))).

-: focus ((csp E):exp (1q AL))
	 (fr-val (val-csp0 : val (1q AL) (csp E))).

focusr: f-result qt E -> f-result qt (run E) -> type.
%mode focusr +E1F -R.
-: focusr (fr-val V) (fr-ouz (ouz-t (pv-r V))).
-: focusr (fr-ouz Z) (fr-ouz R) <- ouz-more Z ([e] (run e)) R.
%worlds (bl-a | bl-focusl) (focusr _ _).
%total (C) (focusr C _).

-: focus (run E) R
	<- focus E EF
	<- focusr EF R.

%worlds (bl-a | bl-focusl) (focus _ _).
%terminates {E} (focus E _).
%covers focus +E -EF.
%total {E} (focus E _).
	% Focus is total!

% Finally, the evaluation relation

eval: exp A -> exp A -> type.
%mode eval +E1 -E2.
-: eval E R 
	<- focus E (fr-ouz Z)
	<- ev-ouz Z R.

% The transitive reflexive closure, so we can evaluate programs

eval*: exp qt -> exp qt -> type.
%mode eval* +E1 -E2.
-: eval* E E <- val _ E.
-: eval* E R <- eval E ES <- eval* ES R.


% Sample evaluations

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

%query 1 2 eval* ((l fint [x] x + (n 1 0)) @ (n 1 1 0)) R.

%query 1 2 eval* ((ll [a] a > l fint [x] (x + ~ (a > n 0))) @q BL) R.

%query 1 2 focus ((l fint ([x] ~(AL > n 0))):exp (1q AL)) R.


%query 1 2 focus ((AL > l fint ([x] ~ (AL > x))):exp qt) R.

%query 1 2 eval* (AL > l fint ([x] ~ (AL > x))) 
       (AL > l fint ([e] e)).


% more focusing tests 
%query 1 2 focus (AL > (~ (AL > ((n 0):exp (1q AL))))) R.
% %query 1 2 focus (AL > (run (~ (AL > ((n 0):exp (1q AL)))))) R.

% Now try some of the tests under lambda, see `Sample tests of levels'

%query 1 2 focus ((AL > (l fint [x] (~ (AL > n 0)))):exp qt) R .
%query 1 2 focus ((AL > (l fint [x] (~ (AL > x)))):exp qt) R .

%{
%query 1 2 focus ((AL > (l fint [x] (BL > (l fint [y] (~ (BL > n 0)))))):exp qt)
	R.

%query 1 2 focus ((AL >
	  (l int [x] (BL > (l int [y] ~ (~ (AL > BL > n 0)))))):exp qt)
	R.
}%

% Now try some of the tests under lambda, and qualifier introduction.

%query 1 2 focus (ll [bl] (bl > (l fint [y] n 0)))
	(fr-val R).

%query 1 2 focus (ll [bl] (bl > (l fint [y] ~ (bl > n 0))))
	R.


% Now try to run our examples

%query 1 2 eval* idp idp.
%query 1 2 eval* exr1 
	(ll ([a:qual] a > l fint ([e:exp (1q a)] e))).


%query 1 2 eval* (ll ([a:qual] l (a f> fint) ([x1:exp qt] x1)) @q AL
                             @ AL > (n 0)) (AL > (n 0)).


%query 1 2 eval* 
          (AL
             > l fint
                  ([x:exp (1q AL)]
                      ~
                         (ll ([a:qual] l (a f> fint) ([x1:exp qt] x1)) @q AL
                             @ AL > x))) R.


%query 1 2 eval* (exr1 @q BL) 
	(BL > l fint ([e:exp (1q BL)] e)).	% <fun x -> x>


%query 1 2 eval* exr1 R. 
% R = ll ([a:qual] a > l fint ([e:exp (1q a)] e)).

%query 1 2 eval* (run exr1) (ll [a] (l fint ([x':exp qt] x'))).


%query 1 2 eval* (ex11 @q BL) 
	(BL > l fint ([e:exp (1q BL)] (n 0) + e)).	% <fun x -> 0+x>

%query 1 2 eval* (ex21 @q BL)
	(BL > l fint ([e:exp (1q BL)] (n 0) + e)).	% <fun x -> 0+x>

%query 1 2 eval* (run ex21) (ll [a] (l fint ([x':exp qt] (n 0) + x'))).

% The famous eta.
% (alpha)(fun f -> <fun x -> ~(f <x>)>)

%query 1 2 eval* (etax1 @q BL)		% <fun x y -> x + y>
   (BL > l fint ([e:exp (1q BL)] l fint ([e1:exp (1q BL)] e1 + e))).


% .<fun x -> .~(let u = .<x>. in (.! .<fun y -> .<.~u>.>.) ()) >.;;
%query 1 2 eval* ((run exrun) @q BL) (l fint ([x':exp qt] x')). % fun x -> x

       % The following do run, although ill-typed
%query 1 2 eval* exrun1 (ll [a] n 1 0).
%query 1 2 eval* exrun2 (ll ([a:qual] n 1 0)).
%query 1 2 eval* exrun3 (ll ([a:qual] ll ([a1:qual] n 1 0))).

% ========================================================================
%			Type preservation

% We define a family isomorphic to csp-ok but different. The point is
% to avoid strengthening: csp-ok may occur in (of E T) -- see of-csp --
% but csp-ok1 cannot.

csp-ok1: exp qt -> type.
%mode csp-ok1 +E.
csp-ok1-i: csp-ok1 (n N).
csp-ok1-l: csp-ok1 (l TV B) 
	  <- {e} csp-ok1 e -> csp-ok1 (B e).
csp-ok1-f: csp-ok1 (fix _ _).
csp-ok1-@: csp-ok1 (E1 @ E2)
	  <- csp-ok1 E2
	  <- csp-ok1 E1.
csp-ok1-+: csp-ok1 (E1 + E2)
	  <- csp-ok1 E2
	  <- csp-ok1 E1.
%block bl-csp-ok1 : block {e:exp qt} {ok1:csp-ok1 e}.
%worlds (bl-a | bl-csp-ok1) (csp-ok1 _).
%terminates {E} (csp-ok1 E).

% The following marks the typing derivation of an expression that
% is the result of a demotion. Demotion is not subjective; we need
% that fact to prove the strengthening lemmas below.
demotedof: exp qt -> tp -> type.
%mode demotedof +E -T.
dof-: of E T -> csp-ok1 E -> demotedof E T.


% Stating the proposition that demotion is type-preserving
%   Forward family and block declaration
tp-dem: demote (_:val (1q AL) E) E' -> of E T -> demotedof E' T -> type.
%mode tp-dem +DJ +P1 -P2.
%block bl-tp-dm : some {AL:qual} {TV:tp}
                  block
		  {x: exp (1q AL)} {v: val (1q AL) x} {x':exp qt}
                  {dth: demote v x'}
	          {oth:  of x TV}
	          {oth': of x' TV}
	          {x'-ok1: csp-ok1 x'}
	          {t:tp-dem dth oth (dof- oth' x'-ok1)}.


% Strengthening Lemma: asserting that (of (E:exp qt) T)
% cannot depend on any hypothesis of the type exp (1q AL)
% and (of (_:exp (1q AL)) T) -- provided that E is the result of a demotion.
% The following is the constructive proof.
strength-tp-dem : csp-ok1 E ->
		  ({x:exp (1q AL)} of x TV -> of E T) -> 
		  of E T -> type.
%mode strength-tp-dem +CS +H -P.
-: strength-tp-dem _ ([x] [t] P) P.  % for P that is patently independent
-: strength-tp-dem (csp-ok1-@ C1 C2) ([x] [t] (of-@ (P1 x t) (P2 x t)))
   		   (of-@ P1' P2')
   <- strength-tp-dem C1 P1 P1'
   <- strength-tp-dem C2 P2 P2'.
-: strength-tp-dem (csp-ok1-+ C1 C2) ([x] [t] (of-+ (P1 x t) (P2 x t)))
   		   (of-+ P1' P2')
   <- strength-tp-dem C1 P1 P1'
   <- strength-tp-dem C2 P2 P2'.
-: strength-tp-dem (csp-ok1-l C) ([x] [t] ((of-l (P x t)):of _ (T1 => T2)))
   		   (of-l P')
   <- {x':exp qt} {ok:csp-ok1 x'} {t':of x' T1}
      strength-tp-dem (C x' ok) ([x] [t] P x t x' t') (P' x' t').
%block strength-tp-dem-bl :
       some {T:tp}
       block {x':exp qt} {ok:csp-ok1 x'} {t':of x' T}.
%worlds (bl-a | bl-tp-dm | strength-tp-dem-bl) (strength-tp-dem _ _ _).
%terminates {P} (strength-tp-dem _ P _).
%total {P} (strength-tp-dem _ P _).

% Flat types that have been demoted are pure
% Although we ended up not using this lemma, it is still nice.
dflat-pure: demote-flat FT1 (FT2:flat qt T) -> puretp T -> type.
%mode dflat-pure +DF -PT.
-: dflat-pure dflat-i pt-i.
-: dflat-pure (dflat-t D1 D2) (pt-a PT1 PT2)
   <- dflat-pure D2 PT2
   <- dflat-pure D1 PT1.
%worlds (bl-a) (dflat-pure _ _).
%total {DF} (dflat-pure DF _).

% Another strengthening lemma: csp-ok1 E judgments cannot depend
% on hypotheses {x:exp (1q AL)}.
strength-csp-ok1 : ({x:exp (1q AL)} csp-ok1 E) -> csp-ok1 E -> type.
%mode strength-csp-ok1 +H -C.
-: strength-csp-ok1 ([x] C) C.
-: strength-csp-ok1 ([x] (csp-ok1-@ (C1 x) (C2 x))) (csp-ok1-@ C1' C2')
   <- strength-csp-ok1 C2 C2'
   <- strength-csp-ok1 C1 C1'.
-: strength-csp-ok1 ([x] (csp-ok1-+ (C1 x) (C2 x))) (csp-ok1-+ C1' C2')
   <- strength-csp-ok1 C2 C2'
   <- strength-csp-ok1 C1 C1'.
-: strength-csp-ok1 ([x] (csp-ok1-l (C x))) (csp-ok1-l C')
   <- {x':exp qt} {c:csp-ok1 x'}
      strength-csp-ok1 ([x] (C x x' c)) (C' x' c).
%worlds (bl-a | bl-tp-dm | bl-csp-ok1) (strength-csp-ok1 _ _).
%total {H} (strength-csp-ok1 H _).

% We state that csp-ok and csp-ok1 are isomorphic families.
% We only need one direction however: given csp-ok, we can always obtain
% csp-ok1.
csp-ok-ok1: csp-ok E -> csp-ok1 E -> type.
%mode csp-ok-ok1 +C1 -C2.
-: csp-ok-ok1 csp-ok-i csp-ok1-i.
-: csp-ok-ok1 csp-ok-f csp-ok1-f.
-: csp-ok-ok1 (csp-ok-l C) (csp-ok1-l C1)
     <- {e} {c:csp-ok e} {c1:csp-ok1 e} 
        csp-ok-ok1 c c1 -> csp-ok-ok1 (C e c) (C1 e c1).
-: csp-ok-ok1 (csp-ok-@ C1 C2) (csp-ok1-@ C1' C2')
     <- csp-ok-ok1 C2 C2'
     <- csp-ok-ok1 C1 C1'.
-: csp-ok-ok1 (csp-ok-+ C1 C2) (csp-ok1-+ C1' C2')
     <- csp-ok-ok1 C2 C2'
     <- csp-ok-ok1 C1 C1'.
%block bl-csp-ok-ok1 : 
       block {e:exp qt} {c:csp-ok e} {c1:csp-ok1 e} {t:csp-ok-ok1 c c1}.
%worlds (bl-a | bl-tp-dm | bl-csp-ok-ok1) (csp-ok-ok1 _ _).
%terminates {C} (csp-ok-ok1 C _).
%total {C} (csp-ok-ok1 C _).


% After all these lemmas, we now prove that demotion is type-preserving
% tp-dem: demote (_:val (1q AL) E) E' -> of E T -> demotedof E' T -> type.

-: tp-dem dn-n _ (dof- of-i csp-ok1-i).
-: tp-dem (dn-f _ _) _ (dof- of-fix csp-ok1-f).
-: tp-dem (dn-@ DV1 DV2) (of-@ P1 P2) 
   	  (dof- (of-@ P1' P2') (csp-ok1-@ CSP-ok1 CSP-ok2))
     <- tp-dem DV1 P1 (dof- P1' CSP-ok1)
     <- tp-dem DV2 P2 (dof- P2' CSP-ok2).
-: tp-dem (dn-+ DV1 DV2) (of-+ P1 P2) 
   	  (dof- (of-+ P1' P2') (csp-ok1-+ CSP-ok1 CSP-ok2))
     <- tp-dem DV1 P1 (dof- P1' CSP-ok1)
     <- tp-dem DV2 P2 (dof- P2' CSP-ok2).
-: tp-dem dn-c (of-csp _ P CSP-ok) (dof- P CSP-ok1)
     <- csp-ok-ok1 CSP-ok CSP-ok1.
-: tp-dem (dn-l DJ DFTV) ((of-l P1):of (_:exp (1q AL)) _)
          (dof- R CSP-okl)
     <- ({x: exp (1q AL)} {v: val (1q AL) x} {x':exp qt}
         {dth: demote v x'}
	 {oth:  of x TV}
	 {oth': of x' TV}
	 {x'-ok1: csp-ok1 x'}
	 tp-dem dth oth (dof- oth' x'-ok1) ->
         tp-dem (DJ x v x' dth) (P1 x oth) 
	  (dof- (P2 x' oth' x oth) (CSP-ok x x' x'-ok1)))
     <- strength-csp-ok1 
         ([x:exp (1q AL)] (csp-ok1-l [x'] [ok'] CSP-ok x x' ok')) CSP-okl
     <- strength-tp-dem 
        CSP-okl 
	([x] [oth] (of-l [x'] [oth'] P2 x' oth' x oth)) R.
%worlds (bl-a | bl-tp-dm) (tp-dem _ _ _).
%covers tp-dem +DJ +P1 -P2.
%terminates {D} (tp-dem D _ _).
%total {D} (tp-dem D _ _).


% Lemma: typing a pre-value 
ofpv : pre-val A E -> tp -> type.	%name of P.
%mode ofpv +E -T.
ofpv- : ofpv (_:pre-val A E) T <- of E T.

% reducing a redex is type-preserving
tp-redex : ev-redex PV E -> ofpv PV T -> of E T -> type.
%mode tp-redex +RJ +P1 -P2.
-: tp-redex rx-@ (ofpv- (of-@ (of-l PB) (PE2:of E T2))) (PB E PE2).
-: tp-redex rx-f (ofpv- (of-@ of-fix PE2)) 
       (of-@ PE2 (of-l [x][tx] (of-@ (of-@ of-fix PE2) tx))).
-: tp-redex (rx-+ _) (ofpv- _) of-i.
-: tp-redex rx-q 
            (ofpv- ((of-@q (of-L [a] PB a)):of (_ @q AL) _))
	    (PB AL).
-: tp-redex rx-~ (ofpv- (of-~ PT (of-> _ PE))) PE.
-: tp-redex (rx-r TDEM)
            (ofpv- (of-run _ (of-L [a] (of-> _ (PE a)))))
            (of-L [a] (R a))
   <- {a} tp-dem (TDEM a) (PE a) (dof- (R a) _).
%worlds (bl-a) (tp-redex _ _ _).
%covers tp-redex +RJ +P1 -P2.
%terminates {R P} (tp-redex R P _).
%total {P} (tp-redex P _ _).

%.