module lpbasic_absyn.
%  higher-order abstract syntax and execution of lpbasic

% A program will just be a stat

% type checking:
hastype (intexp N) integer.
hastype (intexp 1) boolean.		% overloading integers
hastype (intexp 0) boolean.
%hastype (var X) T :- bind X V, hastype V T.  % runtime typechecking
hastype (strexp S) ascii.
hastype (sumexp A B) integer :- hastype A integer, hastype B integer.
hastype (difexp A B) integer :- hastype A integer, hastype B integer.
hastype (multexp A B) integer :- hastype A integer, hastype B integer.
hastype (divexp A B) integer :- hastype A integer, hastype B integer.
hastype (andexp A B) boolean :- hastype A boolean, hastype B boolean.
hastype (orexp A B) boolean :- hastype A boolean, hastype B boolean.
hastype (notexp A) boolean :- hastype A boolean.
hastype (eqexp A B) boolean :- hastype A T, hastype B T.  % polymorphic =
hastype (ineqexp A B) boolean :- hastype A T, hastype B T.  % polymorphic =
welltyped (printst A) :- hastype A T.
welltyped (assignst S E) :- hastype S T, hastype E T.
welltyped (ifst C S) :- hastype C boolean, welltyped S.
welltyped (ifelsest C S1 S2) :- hastype C boolean, welltyped S1, welltyped S2.
welltyped (blockst nil).
welltyped (blockst [H|T]) :- welltyped H, welltyped (blockst T).
welltyped (whilest C L) :- hastype C boolean, welltyped L.
welltyped (letst E L) :- hastype E T,
	pi x\ (hastype x T => welltyped (L x)).
welltyped A :- print "Typechecking failed for ", printterm std_out A, !, fail.

copyexp (intexp N) (intexp N).
copyexp (strexp S) (strexp S).
copyexp (varexp V) (varexp V).
copyexp (sumexp A B) (sumexp C D) :- copyexp A C, copyexp B D.
copyexp (difexp A B) (difexp C D) :- copyexp A C, copyexp B D.
copyexp (multexp A B) (multexp C D) :- copyexp A C, copyexp B D.
copyexp (divexp A B) (divexp C D) :- copyexp A C, copyexp B D.
copyexp (andexp A B) (andexp C D) :- copyexp A C, copyexp B D.
copyexp (orexp A B) (orexp C D) :- copyexp A C, copyexp B D.
copyexp (eqexp A B) (eqexp C D) :- copyexp A C, copyexp B D.
copyexp (ineqexp A B) (ineqexp C D) :- copyexp A C, copyexp B D.
copyexp (notexp A) (notexp B) :- copyexp A B.
copyst (printst A) (printst B) :- copyexp A B.
copyst (assignst S A) (assignst T B) :-    % variable may be bound
       copyexp S T, copyexp A B.
copyst (ifst A S ) (ifst B T) :- copyexp A B, copyst S T.
copyst (ifelsest A S1 S2) (ifelsest B T1 T2) :-
	copyexp A B, copyst S1 T1, copyst S2 T2.
copyst (whilest A S) (whilest B T) :- copyexp A B, copyst S T.
copyst (letst A M) (letst B N) :- copyexp A B,
	pi x\ (copyexp x x => copyst (M x) (N x)).
copyst (blockst nil) (blockst nil).
copyst (blockst [H|T]) (blockst [L|M]) :- copyst H L, 
	copyst (blockst T) (blockst M).


% evaluation (into atoms)

lbeval (intexp N) (intexp N).
lbeval (strexp S) (strexp S).
lbeval (sumexp A B) (intexp N) :- lbeval A (intexp X), lbeval B (intexp Y), 
		N is (X + Y).
lbeval (difexp A B) (intexp N) :- lbeval A (intexp X), lbeval B (intexp Y), 
		N is (X - Y).
lbeval (multexp A B) (intexp N) :- lbeval A (intexp X), lbeval B (intexp Y), 
		N is (X * Y).
lbeval (divexp A B) (intexp N) :- lbeval A (intexp X), lbeval B (intexp Y), 
		N is (X div Y).
lbeval (andexp A B) (intexp N) :- lbeval A (intexp X), lbeval B (intexp Y), 
    ((X = 1, Y = 1, !, N = 1); N = 0).
lbeval (orexp A B) (intexp N) :- lbeval A (intexp X), lbeval B (intexp Y), 
    ((X = 0, Y = 0, !, N = 0); N = 1).		
lbeval (eqexp A B) (intexp N) :- lbeval A (intexp X), lbeval B (intexp X).
lbeval (ineqexp A B) (intexp N) :- lbeval A (intexp X), lbeval B (intexp Y),
    ((X < Y, !, N = 1); N = 0).
lbeval (notexp A) (intexp N) :- lbeval A (intexp X),
    ((X = 0, !, N = 1); N = 0).
lbeval V E :- bind V VV, lbeval VV E.  % V could be lambda-bound or free

% execution of a list of statements:

lbexecute nil :- print "\n".
lbexecute [(printst A)|Pg] :- lbeval A B, printit B, lbexecute Pg.
lbexecute [(assignst X Y)|Pg] :- lbeval Y E, 
     ((lbeval X E :- !) => lbexecute Pg).
lbexecute [(ifst A S)|Pg] :- lbeval A (intexp B),
  ((B = 1, lbexecute [S|Pg]); (B = 0, lbexecute Pg)).
lbexecute [(ifelsest A S T)|Pg] :- lbeval A (intexp B),
  ((B = 1, lbexecute [S|Pg]); (B = 0, lbexecute [T|Pg])).
lbexecute [(whilest A S)|Pg] :- lbeval A (intexp B),
  ((B = 1, lbexecute [S,(whilest A S)|Pg]); (B = 0, lbexecute Pg)).
lbexecute [(letst V S)|Pg] :-  pi x\ (bind x V => lbexecute [(S x)|Pg]).
lbexecute [(blockst B)|Pg] :- appendd B Pg BP, lbexecute BP.



% utilities:

printit (intexp N) :- printterm std_out N, print "\n".
printit (strexp S) :- print S, print "\n".
appendd nil L L.
appendd [A|B] C [A|D] :- appendd B C D.