% Definition and examples of pattern-based focusing in Twelf.
% See accompanying paper, "Defunctionalizing focusing proofs".
% Noam Zeilberger, 2009

% NOTE: To load this code in Twelf CVS, auto-freezing must be turned off.
% (C-c < autoFreeze false)

%%%%%%%%%%%%
% RUN-TIME %
%%%%%%%%%%%%
% a tiny collection of integer operations, as logic programs...

i : type.     %mode i.
z : i.
s : i -> i.   %prefix 10 s.

i0 = z. i1 = s z. i2 = s s z. i3 = s s s z.

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

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

%%%%%%%%%%%%%%%%%%%
% TYPES/JUDGMENTS %
%%%%%%%%%%%%%%%%%%%

pos : type. neg : type. tp : type.
⁺ : pos -> tp.  %postfix 10 ⁺.
⁻ : neg -> tp.  %postfix 10 ⁻.

frm : type.
⋅ : frm.
, : frm -> frm -> frm.  %infix right 11 ,.
true : tp -> frm.       %postfix 9 true.
false : tp -> frm.      %postfix 9 false.

j : type.
# : j.
⊢ : frm -> j -> j.      %infix right 8 ⊢.
sub : frm -> type.
%abbrev val : tp -> type = [A] sub (A true).
%abbrev con : tp -> type = [A] sub (A false).
exp : j -> type.

% We assume a relation Δ ⊩ Δ' as a _dictionary_, defining different
% positive and negative types.  The actual dictionary entries will
% be provided later.
⊩ : frm -> frm -> type.  %mode ⊩ -XΔ1 +XΔ2.  %infix right 8 ⊩.

%%%%%%%%%
% TERMS %
%%%%%%%%%

% constructors for "terms in context"
λ⋅ : exp J -> exp (⋅ ⊢ J).
λ, : exp (XΔ₁ ⊢ XΔ₂ ⊢ J) -> exp (XΔ₁ , XΔ₂ ⊢ J).
λ : (sub XΔ -> exp J) -> exp (XΔ ⊢ J).
%prefix 9 λ⋅. %prefix 9 λ,. %prefix 9 λ.

% canonical constructors for positive values & negative continuations
v+ : XΔ ⊩ A ⁺ true -> sub XΔ -> val (A ⁺).
c- : XΔ ⊩ A ⁻ false -> sub XΔ -> con (A ⁻).

% canonical constructors for substitutions
nil : sub ⋅.
++ : sub XΔ₁ -> sub XΔ₂ -> sub (XΔ₁ , XΔ₂).   %infix right 11 ++.

% constructors for expressions
throw : con A -> val A -> exp #.
let : sub XΔ -> exp (XΔ ⊢ #) -> exp #.
abort : i -> exp #.

% Now we DEFUNCTIONALIZE the canonical representation of positive
% continuations & negative values...
cbody : con (A ⁺) -> XΔ ⊩ A ⁺ true -> exp (XΔ ⊢ #) -> type.
vbody : val (A ⁻) -> XΔ ⊩ A ⁻ false -> exp (XΔ ⊢ #) -> type.
%mode cbody +K +P -E.  %mode vbody +V +D -E.
% The following checks are trivial at this point, but we will continue
% to maintain them as invariants when we declare new constants.
%worlds () (cbody K P _). %total {K P} (cbody K P _). %unique cbody +K +P -E.
%worlds () (vbody V D _). %total {V D} (vbody V D _). %unique vbody +V +D -E.

% Positive values & negative continuations satisfy dual properties...
vfact : val (A ⁺) -> XΔ ⊩ A ⁺ true -> sub XΔ -> type.
cfact : con (A ⁻) -> XΔ ⊩ A ⁻ false -> sub XΔ -> type.
%mode vfact +V -P -Xσ.  %mode cfact +K -D -Xσ.
% Again these lemmas are trivial at this point, but we will maintain
% them whenever we add new constructors.
vfact/v+ : vfact (v+ P Xσ) P Xσ.
cfact/c- : cfact (c- D Xσ) D Xσ.
%worlds () (vfact V _ _). %total V (vfact V _ _). %unique vfact +V -P -Xσ.
%worlds () (cfact K _ _). %total K (cfact K _ _). %unique cfact +K -D -Xσ.

%%%%%%%%%%%%%%%%%%%%%%
% BIG-STEP SEMANTICS %
%%%%%%%%%%%%%%%%%%%%%%

load : sub XΔ -> exp (XΔ ⊢ J) -> exp J -> type.
%mode load +Xσ +T -T'.
ld/nil : load nil (λ⋅ T) T.
ld/++ : load (Xσ₁ ++ Xσ₂) (λ, T) T'' <- load Xσ₁ T T' <- load Xσ₂ T' T''.
ld/x : load Xσ (λ T*) (T* Xσ).

result : type.
halt : i -> result.
eval : exp # -> result -> type.
%mode eval +E -R.

ev/throw⁺ : eval (throw K V) R
   <- vfact V P Xσ
   <- cbody K P E
   <- eval (let Xσ E) R.
ev/throw⁻ : eval (throw K V) R
   <- cfact K D Xσ
   <- vbody V D E
   <- eval (let Xσ E) R.
ev/let :  eval (let Xσ E) R
   <- load Xσ E E'
   <- eval E' R.
ev/abort : eval (abort N) (halt N).

%worlds () (load _ _ _). %total (Sσ) (load Sσ _ _). %unique load +Sσ +T -T.
%worlds () (eval _ _). %covers eval +E -R.
% (TWELF NOTE: %covers does not quite guarantee type safety, because it does
% not check output-freeness.  Really we need the mythical %partial...)

%%%%%%%%%%%%%%%%%%%
% TYPE DICTIONARY %
%%%%%%%%%%%%%%%%%%%

% This concludes the generic description of focusing as a type
% system and operational semantics.  Now we present some specific
% patterns for specific types, which we'll use in some examples
% further below.

% some standard (polarized) propositional connectives
1 : pos.
  #* : ⋅ ⊩ 1 ⁺ true.
⊗ : pos -> pos -> pos.  %infix right 14 ⊗.
  #, : XΔ₁ ⊩ A ⁺ true -> XΔ₂ ⊩ B ⁺ true -> (XΔ₁ , XΔ₂) ⊩ A ⊗ B ⁺ true.  %infix right 11 #,.
0 : pos.
⊕ : pos -> pos -> pos.  %infix right 13 ⊕.
  #Inl : XΔ ⊩ A ⁺ true -> XΔ ⊩ A ⊕ B ⁺ true.
  #Inr : XΔ ⊩ B ⁺ true -> XΔ ⊩ A ⊕ B ⁺ true.
→ : pos -> neg -> neg.  %infix right 12 →.
  #; : XΔ₁ ⊩ A ⁺ true -> XΔ₂ ⊩ B ⁻ false -> (XΔ₁ , XΔ₂) ⊩ A → B ⁻ false.  %infix right 11 #;.
& : neg -> neg -> neg.  %infix right 13 &.
  #Fst : XΔ ⊩ A ⁻ false -> XΔ ⊩ A & B ⁻ false.
  #Snd : XΔ ⊩ B ⁻ false -> XΔ ⊩ A & B ⁻ false.
↓ : neg -> pos.
  _v : A ⁻ true ⊩ ↓ A ⁺ true.
↑ : pos -> neg.
  _k : A ⁺ false ⊩ ↑ A ⁻ false.

% recursive types
rec⁺ : (pos -> pos) -> pos.
  #Fold : XΔ ⊩ A (rec⁺ A) ⁺ true -> XΔ ⊩ rec⁺ A ⁺ true.
rec⁻ : (neg -> neg) -> neg.
  #Unfold : XΔ ⊩ A (rec⁻ A) ⁻ false -> XΔ ⊩ rec⁻ A ⁻ false.

% some derived types
bool = 1 ⊕ 1.
  #Tt : ⋅ ⊩ bool ⁺ true = #Inl #*.
  #Ff : ⋅ ⊩ bool ⁺ true = #Inr #*.
nat = rec⁺ [X] 1 ⊕ X.
  #Zz : ⋅ ⊩ nat ⁺ true = #Fold (#Inl #*).
  #Ss : XΔ ⊩ nat ⁺ true -> XΔ ⊩ nat ⁺ true = [p] #Fold (#Inr p).  %prefix 9 #Ss.
tree = [A] rec⁺ [X] A ⊕ (X ⊗ X).
  #Leaf : XΔ ⊩ A ⁺ true -> XΔ ⊩ (tree A) ⁺ true = [p] #Fold (#Inl p).
  #Node : XΔ₁ ⊩ (tree A) ⁺ true -> XΔ₂ ⊩ (tree A) ⁺ true -> XΔ₁ , XΔ₂ ⊩ (tree A) ⁺ true =
    [p₁] [p₂] #Fold (#Inr (p₁ #, p₂)).
stream = [A] rec⁻ [X] A & X.
  #Hd : XΔ ⊩ A ⁻ false -> XΔ ⊩ stream A ⁻ false = [p] #Unfold (#Fst p).
  #Tl : XΔ ⊩ stream A ⁻ false -> XΔ ⊩ stream A ⁻ false = [p] #Unfold (#Snd p).

% the type of "native integers", so to speak
int : pos.
  #I : i -> ⋅ ⊩ int ⁺ true.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% EXAMPLE 1 : native arithmetic %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% exit is the int-continuation that reads a native int and aborts with that int
exit : con (int ⁺).
exit/_ : cbody exit (#I N) (λ⋅ abort N).

% plus calculates the sum of two ints by performing a "system call"
plus : val (int → int → ↑ int ⁻).
plus/_ : vbody plus ((#I M) #; (#I N) #; _k) (λ, λ⋅ λ, λ⋅ λ [k] throw k (v+ (#I P) nil))
             <- add M N P.

% let's check that these definitions are exhaustive + non-redundant...
%total {K P} (cbody K P _). %unique cbody +K +P -E.
%total {V D} (vbody V D _). %unique vbody +V +D -E.

% Program to calculate "2 + 2" (yes, it's a bit funny syntax...)
%query 1 * eval (throw (c- ((#I i2) #; (#I i2) #; _k) (nil ++ nil ++ exit)) plus) R.

%%%%%%%%%%%%%%%%%%%
% SYNTACTIC SUGAR %
%%%%%%%%%%%%%%%%%%%

% First we'll define some sugar for building positive values, i.e.,
% by declaring new constructors and defining vfact clauses.

, : val (A ⁺) -> val (B ⁺) -> val (A ⊗ B ⁺). %infix none 9 ,.
,/_ : vfact (V1 , V2) (P1 #, P2) (Xσ₁ ++ Xσ₂)
   <- vfact V1 P1 Xσ₁
   <- vfact V2 P2 Xσ₂.

inl : val (A ⁺) -> val (A ⊕ B ⁺).
inr : val (B ⁺) -> val (A ⊕ B ⁺).
inl/_ : vfact (inl V) (#Inl P) Xσ
   <- vfact V P Xσ.
inr/_ : vfact (inr V) (#Inr P) Xσ
   <- vfact V P Xσ.

fold : val (A (rec⁺ A) ⁺) -> val (rec⁺ A ⁺).
fold/_ : vfact (fold V) (#Fold P) Xσ
   <- vfact V P Xσ.

_z : val (int ⁺) = v+ (#I z) nil.
_s : val (int ⁺) -> val (int ⁺).
_s/_ : vfact (_s V) (#I (s N)) nil
   <- vfact V (#I N) nil.

% Check that the vfact lemma really continues to hold...
%worlds () (vfact V _ _). %total V (vfact V _ _). %unique vfact +V -P -Xσ.

% some derived constructors
zz : val (nat ⁺) = fold (inl (v+ #* nil)).
ss : val (nat ⁺) -> val (nat ⁺) = [n] fold (inr n).  %prefix 9 ss.

% Next we introduce some syntactic sugar for building negative values
% and positive continuations, in defunctionalized style.

μ~ : (val (A ⁺) -> exp #) -> con (A ⁺).
μ~/_ : cbody (μ~ K) P (λ [σ] K (v+ P σ)).

μ : (con (A ⁻) -> exp #) -> val (A ⁻).
μ/_ : vbody (μ V) D (λ [σ] V (c- D σ)).

fn : (val (A ⁺) -> val (B ⁻)) -> val (A → B ⁻).
fn/_ : vbody (fn V) (P #; D) (λ, λ [σ₁] λ [σ₂] let σ₂ (E (v+ P σ₁)))
        <- {x} vbody (V x) D (E x).

@ : val (A → B ⁻) -> val (A ⁺) -> val (B ⁻).  %infix left 11 @.
@/_ : vbody (F @ V) D (λ [σ] let (Xσ₀ ++ σ) E) <- vfact V P Xσ₀ <- vbody F (P #; D) E.

% check the above definitions are exhaustive + non-redundant
%total {K P} (cbody K P _). %unique cbody +K +P -E.
%total {V D} (vbody V D _). %unique vbody +V +D -E.

% useful bit of syntactic sugar for plugging a value with a continuation
$ : val (↑ A ⁻) -> con (A ⁺) -> exp # = [v] [k] throw (c- _k k) v.   %infix none 10 $.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% EXAMPLE 2 : recursive function %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% plus calculates the sum of two nats, by standard recursion
plus* : val (nat → nat → ↑ nat ⁻).
plus*/z : vbody plus* (#Zz #; N #; _k) (λ, λ⋅ λ, λ [σ] λ [k]
                throw k (v+ N σ)).
plus*/s : vbody plus* ((#Ss M) #; N #; _k) (λ, λ [σ₁] λ, λ [σ₂] λ [k]
                plus* @ (v+ M σ₁) @ (v+ N σ₂) $ μ~ [x] throw k (ss x)).
%total {V D} (vbody V D _). %unique vbody +V +D -E.

% coercion from nats to ints (as a continuation transformer)
nat2int : con (int ⁺) -> con (nat ⁺).
nat2int/z : cbody (nat2int K) #Zz (λ⋅ throw K _z).
nat2int/s : cbody (nat2int K) (#Ss N) (λ [σ] throw (nat2int (μ~ [x] throw K (_s x))) (v+ N σ)).
%total {K P} (cbody K P _). %unique cbody +K +P -E.

%query 1 * eval (plus* @ (ss ss zz) @ (ss ss ss zz) $ nat2int exit) R.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% EXAMPLE 3 : embedding of call-by-value %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% types representing CBV values & terms
%abbrev vl : pos -> type = [A] val (A ⁺).
%abbrev tm : pos -> type = [A] val (↑ A ⁻).

% decompose the CBV function space
→v : pos -> pos -> pos = [A] [B] ↓ (A → ↑ B).  %infix right 12 →v.

% a few more combinators for building values/continuations.
split : (val (A ⁺) -> val (B ⁺) -> exp #) -> con (A ⊗ B ⁺).
split/_ : cbody (split E) (P1 #, P2) (λ, λ [σ₁] λ [σ₂] E (v+ P1 σ₁) (v+ P2 σ₂)).

case : con (A ⁺) -> con (B ⁺) -> con (A ⊕ B ⁺).
case/inl : cbody (case K1 K2) (#Inl P) E1 <- cbody K1 P E1.
case/inr : cbody (case K1 K2) (#Inr P) E2 <- cbody K2 P E2.

letcc : (con (A ⁺) -> exp #) -> val (↑ A ⁻).
letcc/_ : vbody (letcc E) _k (λ [k] E k).

force : (val (A ⁻) -> exp #) -> con (↓ A ⁺).
force/_ : cbody (force E) _v (λ [x] E x).

%total {K P} (cbody K P _). %unique cbody +K +P -E.
%total {V D} (vbody V D _). %unique vbody +V +D -E.

% Finally, we define an embedding of direct-style, CBV λ-calculus,
% as a collection of macros for building tms.

! : vl A -> tm A = [x] letcc [k] throw k x.  %prefix 9 !.
Pair : tm A -> tm B -> tm (A ⊗ B)
     = [e1] [e2] letcc [k] e1 $ μ~ [x1] e2 $ μ~ [x2] throw k (x1 , x2).
Fst : tm (A ⊗ B) -> tm A = [e] letcc [k] e $ split [x] [y] throw k x.
Snd : tm (A ⊗ B) -> tm B = [e] letcc [k] e $ split [x] [y] throw k y.
Inl : tm A -> tm (A ⊕ B) = [e] letcc [k] e $ μ~ [x] throw k (inl x).
Inr : tm B -> tm (A ⊕ B) = [e] letcc [k] e $ μ~ [x] throw k (inr x).
Case : tm (A ⊕ B) -> (vl A -> tm C) -> (vl B -> tm C) -> tm C
     = [e] [f] [g] letcc [k] e $ case (μ~ [x] f x $ k) (μ~ [y] g y $ k).
Fn : (vl A -> tm B) -> tm (A →v B) = [f] ! v+ _v (fn [x] letcc [k] f x $ k).
App : tm (A →v B) -> tm A -> tm B = [f] [e] letcc [k] f $ force [f₀] e $ μ~ [x] f₀ @ x $ k.
Z : tm nat = ! zz.
S : tm nat -> tm nat = [e] letcc [k] e $ μ~ [x] throw k (ss x).  %prefix 9 S.
Plus : tm nat -> tm nat -> tm nat
     = [e1] [e2] letcc [k] e1 $ μ~ [n1] e2 $ μ~ [n2] plus* @ n1 @ n2 $ k.
Abort : tm nat -> tm A = [e] letcc [k] e $ nat2int exit.

% For convenience, we define an LF type abbreviation, run E N,
% representing the fact that E terminates with result N.

%abbrev run : tm nat -> i -> type = [e] [n] eval (e $ nat2int exit) (halt n).

%query 1 * run (Plus (S S Z) (S S S Z)) N1.                     % N1 = s s s s s z
%query 1 * run (Plus (S S Z) (Abort (S Z))) N2.                 % N2 = s z
%query 1 * run (Plus (Abort Z) (Abort (S Z))) N3.               % N3 = z
%query 1 * run (App (Fn [x] Plus (! x) (S Z)) (S Z)) N4.        % N4 = s s z

% QED