% Testing uniqueness declarations

nat : type.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
pz : plus z Y Y.
ps : plus (s X) Y (s Z)
      <- plus X Y Z.
% p_z : plus X z X.

%mode plus +X +Y -Z.
%worlds () (plus X Y Z).
%unique plus +X +Y -1Z.

le : nat -> nat -> type.
le_refl : le X X.
le_s : le X (s Y) <- le X Y.
%mode le +X -Y.
%worlds () (le X Y).

pres : plus X1 X3 Y -> plus X2 X3 Y' -> le X1 X2 -> le Y Y' -> type.
pres_refl : pres S1 S2 le_refl le_refl.
pres_s : pres S1 (ps S2) (le_s L) (le_s L')
	  <- pres S1 S2 L L' .

%mode pres +S1 +S2 +L -L'.
%worlds () (pres S1 S2 L L').
%total L (pres S1 S2 L L').

exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

eq : exp -> exp -> type.

refl : eq E E.

copy : exp -> exp -> type.
clam : copy (lam [x] E x) (lam [x] F x)
	<- ({x:exp} copy x x -> copy (E x) (F x)).
capp : copy (app E1 E2) (app F1 F2)
	<- eq E1 E1'
	<- copy E1' F1
	<- copy E2 F2.

% %mode copy +E -1F.
%block cb : block {x:exp} {u:copy x x}.

%worlds (cb) (eq E F).
%worlds (cb) (copy E F).

% %block cb1 : block {x:exp} {u:copy x x} {u1:copy x x}.
% %worlds (cb | cb1) (copy E F).

% %block cb2 : block {x:exp} {u:copy x x} {u2:{E:exp} copy E x}.
% %worlds (cb | cb2) (copy E F).

% %block cb3 : block {x:exp} {u:{E:exp} copy (app x E) (app E E)}.
% %worlds (cb | cb3) (copy E F).

% %unique eq +E -F.
%unique eq +E -1F.
%unique copy +E -1F.

% Based on Carsten Schuermann's test for copy theorem
% Tests for uniqueness declarations, coverage failures -- Penny

exp : type.

0 : exp.
s : exp -> exp.
app : exp -> exp -> exp.
lam : (exp -> exp) -> exp.


exp' : type.

0' : exp'.
s' : exp' -> exp'.
app' : exp' -> exp' -> exp'.
lam' : (exp' -> exp') -> exp'.

cp : exp -> exp' -> type.
%mode cp +D -E.
cp_0 : cp 0 0'.
cp_s : cp (s N1) (s' N2) <- cp N1 N2.
cp_app : cp (app D1 D2) (app' E1 E2) 
         <- cp D1 E1
         <- cp D2 E2.
cp_lam : cp (lam ([x:exp] D x)) (lam' ([y:exp'] E y))
         <- ({x:exp} {y:exp'} cp x y -> cp (D x) (E y)). 

%block cp_hyp: block {x:exp} {y:exp'} {d:cp x y}.
%worlds (cp_hyp) (cp D E).
% unique cp +D -1E.
%total D (cp D E).

tp : type.

nat : tp.
arrow : tp -> tp -> tp.

of : exp -> tp -> type.
%mode of +E *T.

of_0 : of 0 nat.
of_s : of (s E) nat <- of E nat.
of_app : of (app E E1) T2 <- of E (arrow T1 T2) <- of E1 T1.
of_lam : of (lam E) (arrow T1 T2) 
	  <- ({x:exp} of x T1 -> of (E x) T2).
%block of_hyp: some {T1:tp} block {x:exp} {d:of x T1}.
%worlds (of_hyp) (of E T).
% % unique of +E -1T. fails, as it should.

tp' : type.

nat' : tp'.
arrow' : tp' -> tp' -> tp'.

of' : exp' -> tp' -> type.
%mode of' +E *T.

of'_0 : of' 0' nat'.
of'_s : of' (s' E) nat' <- of' E nat'.
of'_app : of' (app' E E1) T2 <- of' E (arrow' T1 T2) <- of' E1 T1.
of'_lam : of' (lam' E) (arrow' T1 T2) 
	  <- ({x:exp'} of' x T1 -> of' (E x) T2).
%block of'_hyp: some {T1:tp'} block {x:exp'} {d:of' x T1}.

tcp : tp -> tp' -> type.
%mode tcp +T1 -T2.
cp_nat : tcp nat nat'.
cp_arrow : tcp (arrow T1 T2) (arrow' T1' T2')
	    <- tcp T2 T2' <- tcp T1 T1'.
%worlds () (tcp T1 T2).
%unique tcp +T -1T'.
%total T1 (tcp T1 T2).

% tcp is total
tcpt : {T:tp} {T':tp'} tcp T T' -> type.
%mode tcpt +T -T' -D.
tcpt_nat : tcpt nat nat' cp_nat.
tcpt_arrow : tcpt (arrow T1 T2) (arrow' T1' T2') (cp_arrow D1 D2)
	      <- tcpt T2 T2' D2 <- tcpt T1 T1' D1.
%worlds () (tcpt T T' D).
%unique tcpt +T -1T' -1D.
%total T (tcpt T T' D).

% The output coverage failure example reformulated as input coverage failure.

% Uniqueness has been isolated to the family "same".

% The idea is to "tuple" the two recursive calls needed for the app case
% into one call to an auxiliary type family that returns matching type
% copies and typing derivations.

% All input coverage declarations succeed except for family "same".
% All termination declarations succeed.

% Input and output coverage and termination checking for preserv_aux
% succeed, but totality fails since "same" cannot be seen
% to be total without uniqueness information.

same : tcp T1 T1' -> tcp T1 T1'' 
       -> of' E' (arrow' T1'' T2') -> of' E' (arrow' T1' T2') -> type.
%mode same +CT +CT' +D -D'.

same_clause: {CT:tcp T1 T1'} {CT':tcp T1 T1'} same CT CT' D D.

%worlds () (same CT CT' D D').
%covers same +CT +CT' +D -D'. % fails in the absence of uniqueness knowledge
%terminates (CT) (same CT _ _ _). 
%total (CT) (same CT _ _ _).  % totality succeeds only because of uniqueness

preserv' : cp E E' -> of E T -> tcp T T' -> of' E' T' -> type.
%mode preserv' +C +D -CT -D'.
%block pres_hyp: some {T1:tp} {T1':tp'} {CT:tcp T1 T1'}
		  block {x:exp} {x':exp'} {c: cp x x'}
		  {d:of x T1} {d':of' x' T1'}
		  {p:preserv' c d CT d'}.
%worlds (pres_hyp) (preserv' C D CT D').

pres_0 : preserv' cp_0 of_0 cp_nat of'_0.
pres_s : preserv' (cp_s C) (of_s D) cp_nat (of'_s D') <- preserv' C D _ D'.

% type of first input is designed for easy termination checking
preserv_aux : cp (app E E1) (app' E' E1')
              -> of E (arrow T1 T2) -> of E1 T1 
              -> tcp T2 T2'
              -> tcp T1 T1' -> of' E' (arrow' T1' T2') -> of' E1' T1' -> type.
%mode preserv_aux +C +D +D1 -CT2 -CT1 -D' -D1'.

aux: preserv_aux (cp_app C1 C) D D1 CT2 CT1 D'' D1'
	    <- preserv' C1 D1 CT1 D1'
	    <- preserv' C D (cp_arrow CT1' CT2) D'
	    <- same CT1 CT1' D' D''.
%worlds () (preserv_aux _ _ _ _ _ _ _).

pres_app : preserv' (cp_app C1 C) (of_app D1 D) CT2 (of'_app D1' D')
	    <- preserv_aux (cp_app C1 C) D D1 CT2 CT1 D' D1'.
% The auxiliary predicate replaces the following, which causes
% failure of output freeness:
%	    <- preserv' C1 D1 CT1 D1'
%	    <- preserv' C D (cp_arrow CT1 CT2) D'.

pres_lam :  preserv' (cp_lam C) (of_lam D) (cp_arrow CT1 CT2) (of'_lam D')
	    <- tcpt T1 T1' CT1
	    <- ({x:exp} {x':exp'} {c: cp x x'} {d:of x T1}
		  {d':of' x' T1'}
		  {p:preserv' c d CT1 d'}
		  preserv' (C x x' c) (D x d) CT2  (D' x' d')).

%covers preserv_aux +C +D +D1 -CT -CT1 -D' -D1'.
%covers preserv' +C +D *CT *D'.
%terminates (C' C) (preserv_aux C _ _ _ _ _ _) (preserv' C' _ _ _).
% The following fails since "same" not seen to be total
% Succeeds with uniqueness contraction
%total (C' C) (preserv_aux C _ _ _ _ _ _) (preserv' C' _ _ _).

%{
% Input coverage "%covers preserv +C +D +CT *D'." fails
% since, in pres_lam, T1' in the hypothesis is not known to be
% uniquely determined by the input CT1:tcp T1 T1'.
% Hopefully the uniqueness of the type copy derivation is itself not required.

preserv : cp E E' -> of E T -> tcp T T' -> of' E' T' -> type.
%mode preserv +C +D +CT -D'.

pres_0 : preserv cp_0 of_0 cp_nat of'_0.
pres_s : preserv (cp_s C) (of_s D) cp_nat (of'_s D') <- preserv C D cp_nat D'.
pres_app : preserv (cp_app C1 C) (of_app D1 D) CT2 (of'_app D1' D')
	    <- tcpt T1 T1' CT1
	    <- preserv C1 D1 CT1 D1' <- preserv C D (cp_arrow CT1 CT2) D'.
pres_lam : preserv (cp_lam C) (of_lam D) (cp_arrow CT1 CT2) (of'_lam D')
	    <- ({x:exp} {x':exp'} {c: cp x x'} {d: of x T1} {d': of' x' T1'}
		  ({ct: tcp T1 T1'} preserv c d ct d')
		  -> preserv (C x x' c) (D x d) CT2  (D' x' d')).

%block pres_hyp: some {T1:tp} {T1':tp'} 
		  block {x:exp} {x':exp'} {c: cp x x'}
		  {d: of x T1} {d': of' x' T1'}
		  {p: {ct: tcp T1 T1'} preserv c d ct d'}.
%worlds (pres_hyp) (preserv C D CT D').
% %covers preserv +C +D +CT *D'. % current fails because we do not descend into blocks
% 
% %total C (preserv C D CT D').


% An artificial example where coverage fails because of missing 
% uniqueness information.  No context blocks are involved.
% This example requires uniqueness of proof terms.

nat: type.
0: nat.
s: nat -> nat.

eq: nat -> nat -> type.
%mode eq +N1 -N2.
eq0: eq 0 0.
eqs: eq N1 N2 -> eq (s N1) (s N2).
%worlds () (eq N1 N2).
%total N1 (eq N1 N2).
%unique eq *N1 +N2.
%unique eq +N1 +N2.
%unique eq +N1 -1N2.

b: nat -> type.
%mode b +A.
b0: b 0.
b1: b (s N1) <- eq N1 N2 <- b N1.
%worlds () (b N1).
%total N1 (b N1).

t: b N1 -> eq N1 N2 -> type.
%mode t +B +U.

t0: t b0 eq0.
t1:  t (b1 B U) (eqs U).
% t1:  t (b1 B U) (eqs U').

%worlds () (t B U).
% %covers t +B +U.  % currently fails because we do not have uniqueness of proof terms
}%