miniml-lists.elf

% Jesper Louis Andersen
% Core Mini-ML + Lists definitions

% Syntax extensions

nil : exp.
cons : exp -> exp -> exp.
lcase : exp -> exp -> (exp -> exp -> exp) -> exp.

% Evaluation extensions

ev_nil : eval nil nil.
ev_cons : eval (cons HD TL) (cons V1 V2)
	   <- eval HD V1
	   <- eval TL V2.
ev_lcase_nil : eval (lcase E1 E2 E3) V
	       <- eval E1 nil
	       <- eval E2 V.
ev_lcase_cons : eval (lcase E1 E2 E3) V
		<- eval E1 (cons V1 V2)
		<- eval (E3 V1 V2) V.

%query 1 * D : eval (app (lam [x] s x) z) V.

% Value notions

val_nil : value nil.

val_cons : value (cons V1 V2)
	    <- value V1
	    <- value V2.

% Type extensions

list : tp -> tp.

of_nil : of nil (list T).

of_cons : of (cons HD TL) (list A)
	   <- of HD A
	   <- of TL (list A).

of_lcase : of (lcase E1 E2 E3) T
	    <- of E1 (list A)
	    <- of E2 T
	    <- {x : exp} {xs : exp} of x A -> of xs (list A) -> of (E3 x xs) T.

one = s z.
two = s one.
three = s two.
four  = s three.

list_one_two = (cons one (cons two nil)).
list_three_four = (cons three (cons four nil)).

append = fix [d] (lam [l1] (lam [l2]
			      lcase l1 l2 ([x : exp] [xs : exp]
					     cons x (app (app d xs) l2)))).

%query 1 5 D : of append T.
%query 1 5 D : eval (app (app append list_one_two) list_three_four) V.

% fun append l1 l2 =
%   case l1 of
%     nil => l2
%     cons x :: xs => cons x (append xs l2)

%% TODO - Queries as asked in the exercise.

%%query 1 5 D : of myexp T.