% One possible answer to Homework 5.11
% Author: Frank Pfenning

linfun : (exp -> exp) -> type.		%name linfun F.
%mode linfun +E.

% linfun E
% is derivable if E is a linear, recursion-free function.

lf_id    : linfun ([x] x).
% no case for ([x] z)
lf_s     : linfun ([x] s (E x))
	    <- linfun ([x] E x).
lf_case1 : linfun ([x] case (E1 x) E2 ([y] E3 y))
	    <- linfun ([x] E1 x).
lf_case2 : linfun ([x] case E1 (E2 x) ([y] E3 x y))
	    <- linfun ([x] E2 x)
	    <- ({y:exp} linfun ([x] E3 x y)).
lf_pair1 : linfun ([x] pair (E1 x) E2)
	    <- linfun ([x] E1 x).
lf_pair2 : linfun ([x] pair E1 (E2 x))
	    <- linfun E2.
lf_fst   : linfun ([x] fst (E x))
	    <- linfun E.
lf_snd   : linfun ([x] snd (E x))
	    <- linfun E.
lf_lam   : linfun ([x] lam ([y] E x y))
	    <- ({y:exp} linfun ([x] E x y)).
lf_app1  : linfun ([x] app (E1 x) E2)
	    <- linfun E1.
lf_app2  : linfun ([x] app E1 (E2 x))
	    <- linfun E2.
lf_letv1 : linfun ([x] letv (E1 x) ([y] E2 y))
	    <- linfun ([x] E1 x).
lf_letv2 : linfun ([x] letv E1 (E2 x))
	    <- ({y:exp} linfun ([x] E2 x y)).
lf_letn1 : linfun ([x] letn (E1 x) ([y] E2 y))
	    <- linfun ([x] E1 x).
lf_letn2 : linfun ([x] letn E1 (E2 x))
	    <- ({y:exp} linfun ([x] E2 x y)).
% no case for ([x] fix ([y] E x y))

%terminates E (linfun E).
% %world (pi {y:exp} | pi {x:exp} {l:linear x}) (linfun E).

linear : exp -> type.			%name linear L.
%mode linear +E.

% linear E
%  is derivable if E is recursion-free and every abstraction
%  (introduced with case, lam, letv or letn) is linear.

l_z    : linear z.
l_s    : linear (s E)
	  <- linear E.
l_case : linear (case E1 E2 ([x] E3 x))
	  <- linear E1
	  <- linear E2
	  <- linfun ([x] E3 x)
	  <- ({x:exp} linear x -> linear (E3 x)).
l_pair : linear (pair E1 E2)
	  <- linear E1
	  <- linear E2.
l_fst  : linear (fst E)
	  <- linear E.
l_snd  : linear (snd E)
	  <- linear E.
l_lam  : linear (lam ([x] E x))
	  <- linfun ([x] E x)
	  <- ({x:exp} linear x -> linear (E x)).
l_app  : linear (app E1 E2)
	  <- linear E1
	  <- linear E2.
l_letv : linear (letv E1 ([x] E2 x))
	  <- linear E1
	  <- linfun ([x] E2 x)
	  <- ({x:exp} linear x -> linear (E2 x)).
l_letn : linear (letn E1 ([x] E2 x))
	  <- linear E1
	  <- linfun ([x] E2 x)
	  <- ({x:exp} linear x -> linear (E2 x)).

%terminates E (linear E).
% %world (pi {x:exp} {l:linear x}) (linear E).
% %covers linear +E.