i : type.
o : type.
ilist:type
cont:type.

& : o -> o -> o.			%infix right 11 &
v : o -> o -> o.			%infix right 11 v
%=> : o -> o -> o.		%infix right 10  =>
%<= : o -> o -> o.		%infix right 10  <=
%not : o -> o.			%prefix 7 not
some : (i -> o) -> o.
all : (i -> o) -> o.
pi : (i -> o) -> o.

% numerals    nat < i.
0 : i.
s : i -> i.
% lists
nil : ilist
::   : i -> ilist ->ilist	%infix right 5  ::

%modes
prove(+Goal,+SuccessC,+FailureC,+SplitC)
split(+Formula,+Cont-Formulae)
update(+Cont,-UpdCont) 



demo 		: o  -> type.
prove 		: o -> o -> o -> cont-> type.
assume 	: o -> type.
chain  		: o -> o -> o -> o -> cont-> type.
split		: o -> cont -> o -> type.
update		: cont -> cont -> type.
atom : o -> type.		%name atom A1 A2 A3
apply : 	o -> covering ->o -> type.
mappred :  (i -> o) -> ilist -> o -> type.
covering : ilist -> type.


start 	: demo A <- prove A true false false.
ptrue   	: prove true true _ _.			%one answer
pand     	 : prove (A & B) S F C <- prove A (B & S) F C.
porl		 : prove (A v B ) S F C <- prove A S (B v F) C.
pinst	 	: prove (some A) S F C <- prove (A X) S F C.
pgen		: prove (pi A) S F C <- {a : i} prove (A a) S F C.
pcase		 : prove (all A) S F C 
			<-   split A C Gs
			<- {a : i}  prove Gs S F ((A a) & C).
patom    	 : prove A S F C <- assume B <- chain B A S F C.
pbtrack  	:  prove A S (F & false) C <- prove F S false C.
psplit  	:  prove A S false C
			<- update C NC
			<- prove C S false NC.

uaxiom 	 : chain A A S F C<- prove S true F C.
uandL   	 : chain (B1 & B2) A S F C <- chain B1 A S F C.
uandR   	 : chain (B1 & B2) A S F C <- chain B2 A S F C.
uall     	 : chain (all D) A S F C <- chain (D X) A S F C.
uimplies 	 : chain (B => A) A  S F C <- prove B S F C.

sp 		: split A C Gs
			<-covering Cov
			<- apply A Cov Gs.

up :		update C C.

aor	:	apply (A or B) Cov (CA v CB)
			<- apply A Cov CA
			<- apply B Cov CB.
aand	:	apply (A & B) Cov (CA & CB)
			<- apply A Cov CA
			<- apply B Cov CB.
aaatom	:apply A  Cov CA 
			<- atom A
			<- mappred A Cov CA.


mp_base: 	mappred P nil true.
mp_step:	mappred P C :: Cs (A C) & Gs 
			<- mappred P Cs Gs.

c1: 	cover (0 :: s(X) :: nil).
c2: 	cover (0 :: s(0) :: s(s(X)) :: nil).
c3: 	cover (0 :: s(0) :: s(s(0)) :: s(s(s(X))) :: nil).

%sample programs and queries

p : i > o.
p1 : i > o.
p2 : i > o.
q : i > o.

ap : atom ([x] p x).
ap1 : atom ([x] p1 x).
ap2 : atom ([x] p2 x).

1 : assume (p 0)
2 : assume (p s(X))
3 : assume (p1 0)
4 : assume (p1 s(0))
5 : assume (p1 s(s(X)))

% all ([x] p x)