%%%% Logical programming - Prolog %%%%
thing : type.
witch : thing -> type.
burns : thing -> type.
female : thing -> type.
wooden : thing -> type.
float : thing -> type.
sameweight : thing -> thing -> type.
duck : thing.

% term : a -> a
% a -> a : type
% wooden duck <- float duck <- female duck.
% female duck.

witch_is_burning_female : witch X <- burns X <- female X.
wood_burns : burns X <- wooden X.
float_is_wooden : wooden X <- float X.
sameweight_as_duck_floats : float X <- sameweight duck X.

girl : thing. 
girl_is_female : female girl. % by observation
girl_has_weight_of_duck : sameweight duck girl. % by experiment

%solve _ : witch girl. 

%witch_is_burning_female
%  girl_is_female
%    (wood_burns
%     (float_is_wooden 
%       (sameweight_as_duck_floats girl_has_weight_of_duck))).

%%%% After Monty Python (Sir Bedevere)


%%%% Natural numbers %%%%
nat : type. %name nat N.

z   : nat.
s   : nat -> nat.

0 = z.
1 = s 0.
2 = s 1.
3 = s 2.
4 = s 3.
5 = s 4.
6 = s 5.
7 = s 6.
8 = s 7.
9 = s 8.
% ... another job for Sisyphos.

leq : nat -> nat -> type. %name leq L.
%mode leq +N +M.

leq/z : leq z N.
leq/s : leq (s N) (s M) <- leq N M.

%solve solution : leq 4 N.
%solve solution : leq N 3.
%solve _ : {N} leq 4 N.

% worlds () (leq _ _).
%terminates M (leq N M).

%%%% Lists %%%%
list : type. %name nat L.

cons : nat -> list -> list.
nil : list.

l = cons 2 (cons 4 (cons 5 nil)).

%%%% Sized lists %%%%
nlist : nat -> type.

ncons : {n:nat} nat -> nlist n -> nlist (s n).
nnil : nlist z.

ex = nnil : nlist z.
ex = ncons z 2 nnil : nlist 1.

nl = ncons 2 2 (ncons 1 4 (ncons 0 5 nnil)).

% merge : {n:nat} nlist n -> nlist n -> nlist n.


%%%% Implicit sized lists %%%%
inlist : nat -> type.

incons : nat -> inlist N -> inlist (s N).
innil : inlist z.

nl = incons 2 (incons 4 (incons 5 innil)).

inlength : {l:inlist N} nat.
%abbrev inlength = [l : inlist N] N.

ex = inlength nl.

%%%% Church numerals %%%%
cnat : type.

cnat : {a:type} (a -> a) -> (a -> a).


%%%% Untyped lambda terms %%%%
tm : type.

var : nat -> tm. 
lam : tm -> tm. % De Bruijn
app : tm -> tm -> tm.

ex = (app (lam (var 1)) (var 2)).

%%%% Typed lambda terms %%%%
ty : type.

j : ty.
=> : ty -> ty -> ty.   %infix right 7 =>.

ex = (j => j => j).

tm : ty -> type.

ex : tm j.

var : {a:ty} nat -> tm a.
lam : {a:ty} {b:ty} tm b -> tm (a => b).
app : {a:ty} {b:ty} tm (a => b) -> tm a -> tm b.

ex = (lam (j => j) j (var j 0)).

ex = (app (j => j) j (lam (j => j) j (var j 0)) (lam j j (var j 0))).

% mit impliziten Argumenten

tm : ty -> type.

var : nat -> tm A.
lam : tm B -> tm (A => B).
app : tm (A => B) -> tm A -> tm B.

ex = (app (lam  (var 0)) (lam (var 0))).
ex = (app (var 0) (var 0)).

%%%% Typed lambda terms with context %%%%

% ...

%%%% Higher order abstract syntax %%%%

tm : ty -> type.

app : tm (A => B) -> tm A -> tm B.
lam : (tm A -> tm B) -> tm (A => B).

ex = lam ([x] x).

ex = (app (lam [x] x) (lam [x] x)).
% -> (lam [x] x)

%%%% Reductions %%%%

reduces : tm A -> tm A -> type.

reduces/beta : reduces (app (lam [x] (T x)) S) (T S).

%solve _ : reduces ex (lam [x] x).
%solve _ : reduces ex R.

ex2 = (lam [x] (app (lam [y] x) (lam [z] z))).
%solve _ : reduces ex2 R.

%%%% Normalisation %%%%

normalises : tm A -> tm A -> type.

norm/red : normalises T T' <- reduces T T'.
norm/lam : normalises (lam [x] (T x)) (lam [x] (T' x))
	    <- {x} normalises (T x) (T' x).
norm/app1 : normalises (app T S) (app T' S) <- normalises T T'.
norm/app2 : normalises (app T S) (app T S') <- normalises S S'.
norm/trans : normalises A B -> normalises B C -> normalises A C. 
norm/refl : normalises T T.

%solve _ : normalises ex2 R.

%%%% System F %%%%
ty : type.

all : (ty -> ty) -> ty.
=> : ty -> ty -> ty.   %infix right 7 =>.

tm : ty -> type.

app : tm (A => B) -> tm A -> tm B.
lam : (tm A -> tm B) -> tm (A => B).
tlam : ({a:ty} tm (([x] (F x)) a)) -> tm (all F).
tapp : tm (all F) -> {a:ty} tm (F a).

reduces : tm A -> tm A -> type.

reduces/beta : reduces (app (lam [x] (T x)) S) (T S).
reduces/tbeta : reduces (tapp (tlam T) A) (T A).
reduces/lam : reduces (lam [x] (T x)) (lam [x] (T' x))
	    <- {x} reduces (T x) (T' x).
reduces/tlam : reduces (tlam T) (tlam T')
	    <- {a:ty} reduces (T a) (T' a).
reduces/app1 : reduces (app T S) (app T' S) <- reduces T T'.
reduces/app2 : reduces (app T S) (app T S') <- reduces S S'.
reduces/tapp : reduces (tapp T A) (tapp T' A) 
	     <- reduces T T'.

normalises : tm A -> tm A -> type.
norm/trans : normalises B C -> reduces A B -> normalises A C. 
norm/refl : normalises T T.

ex = (app (tapp (tlam [a] (lam [x:tm a] x)) (A => A)) (lam [y] y)).

%solve _ : normalises ex R.

closed : tm A -> type.
linear : tm A -> type.

%mode reduces +N -M.
%%% worlds () (reduces _ _).
%terminates N (reduces N M).

%mode normalises +N -M.
%%% worlds () (normalises _ _).
%terminates N (normalises N M).