% Simple Twelf encoding, via defunctionalization, of the little language
% in Section 5 of "Focusing on Binding and Computation" [LICS 08].
% See paper "Defunctionalizing Focusing Proofs" [PSTT 09] for more discussion.
% Noam Zeilberger, 2009

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

%%%%%%%%%%%%
% RUN-TIME %
%%%%%%%%%%%%

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

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

%worlds () (add M _ _).
%total (M) (add M _ _).
%unique add +M +N -P.

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

%worlds () (mult M _ _).
%total (M) (mult M _ _).
%unique mult +M +N -P.

%%%%%%%%%%%%
%  SYNTAX  %
%%%%%%%%%%%%

binop : type.
apply : binop -> i -> i -> i -> type.
%mode apply +F +M1 +M2 -N.

%worlds () (apply F M1 M2 _).
% The totality/uniqueness check is trivial at this point, but we will
% maintain it as we declare new binops & add new apply clauses.
%total {F M1 M2} (apply F M1 M2 _).
%unique apply +F +M1 +M2 -N.

tm : type.

n : i -> tm.
let : tm -> (tm -> tm) -> tm.
@ : binop -> tm -> tm -> tm.

%%%%%%%%%%%%%
% SEMANTICS %
%%%%%%%%%%%%%

eval : tm -> i -> type.
%mode eval +E -N.

eval/n : eval (n N) N.
eval/let : eval (let E E*) N
        <- eval (E* E) N.
eval/@ : eval (@ F E1 E2) N
      <- eval E1 M1
      <- eval E2 M2
      <- apply F M1 M2 N.

%worlds () (eval E _).
%covers eval +E -N.
%unique eval +E -N.

%%%%%%%%%%%%
% EXAMPLES %
%%%%%%%%%%%%

plus : binop.
plus/_ : apply plus M N P <- add M N P.

times : binop.
times/_ : apply times M N P <- mult M N P.

%total (M1) (apply F M1 M2 _).
%unique apply +F +M1 +M2 -N.

%query 1 * eval (let (n (s s z)) [two]
		 let (n (s s s z)) [three]
		 @ plus two (@ times two three)) N.