/* This is an alternative to opsem.pl in the main set of code examples
  that allows more flexible queries.

  Compared to opsem.pl we have renamed all of the evals and do the following

eval(A,E,V) :- eval_const(A,E,V).
eval(A,E,V) :- eval_var(A,E,V).
% etc.

This allows the search engine to find more examples, and not run into
ambiguity when rule matching. For example:

?- eval([(x,2)], X, 2).
X = 2 ;
X = var(x) ;
X = app(fun(var(_G909), 2), true) ;
X = app(fun(var(_G909), var(x)), true) ;
X = app(fun(var(_G909), app(fun(var(_G930), 2), true)), true) ;
X = app(fun(var(_G909), app(fun(var(_G930), var(x)), true)), true) ;
% and so on…

or if I evaluate the if's first (i.e., reordering the defs below):

?- eval([(x,2)], X, 2).
X = 2 ;
X = var(x) ;
X = if(true, 2, _G908) ;
X = if(true, var(x), _G908) ;
X = if(true, if(true, 2, _G912), _G908) ;
X = if(true, if(true, var(x), _G912), _G908) ;
X = if(true, if(true, if(true, 2, _G916), _G912), _G908) ;
% ….

Try these queries with opsem.pl and see what happens. 
*/

/* Expressions E have the following syntax:

   var(X),
   plus(E1,E2),
   if(E1,E2,E3),
   let(var(X),E1,E2),
   fun(var(X),E),
   app(E1,E2)
   integers
   booleans

     where E1, E2, E3, and E are expressions, 
       and X is a variable name (e.g., an atom)
*/

/* You can swap the order of these to generate different (infinitely boring) programs */
eval(A,E,V) :- eval_constants(A,E,V).
eval(A,E,V) :- eval_variables(A,E,V).
eval(A,E,V) :- eval_add(A,E,V).
eval(A,E,V) :- eval_if_true(A,E,V).
eval(A,E,V) :- eval_if_false(A,E,V).
eval(A,E,V) :- eval_let(A,E,V).
eval(A,E,V) :- eval_fun_def(A,E,V).
eval(A,E,V) :- eval_fun_app(A,E,V).
eval(A,E,V) :- eval_fun_dynapp(A,E,V).

/* Constants */
eval_constants(_,true,true).
eval_constants(_,false,false).
eval_constants(_,N,N) :- integer(N).    % Question: what if I got rid of integer(N)?

/* Variable lookup */
eval_variables([(X,V)|_],var(X), V) :- !.  % Question: what property does this cut provide?
eval_variables([_|T], var(X), V) :- eval_variables(T, var(X), V).

/* Addition */
eval_add(A, plus(E1,E2), N) :- 
	eval(A, E1, N1), !,
	eval(A, E2, N2), !,
	eval_plus(N1,N2,N).   % Instead of "N is N1 + N2" to allow us to provide N and find N1 or N2

/* True branch */
eval_if_true(A, if(B, E1, _), V) :- 
	eval(A, B, true), !,
	eval(A, E1, V).

/* False branch */
eval_if_false(A, if(B, _, E2), V) :- 
	eval(A, B, false), !,
	eval(A, E2, V).

/* Let binding */
eval_let(A, let(var(X), E1, E2), V) :-
	eval(A, E1, V1), !,
	eval([(X,V1)|A], E2, V).

/* Function definition */
eval_fun_def(A, fun(var(X), E), closure(X,E,A)).

/* Function application */
eval_fun_app(A, app(FN, E2), V) :-
	eval(A, FN, closure(X,E,A0)), !,
	eval(A, E2, V2), !,
	append(A0,A,A1), !,
	eval([(X,V2)|A1], E, V).

/* Function application, dynamic scoping */
eval_fun_dynapp(A, dynapp(FN, E2), V) :-
	eval(A, FN, closure(X,E,_)), !,
	eval(A, E2, V2), !,
	eval([(X,V2)|A], E, V).

eval_plus(N1,N2,N) :-
	integer(N1), integer(N2), !,
	N is N1+N2.

eval_plus(N1,N2,N) :-
	integer(N), integer(N2), !,
	N1 is N-N2.

eval_plus(N1,N2,N) :-
	integer(N), integer(N1), !,
	N2 is N-N1.

/* Queries 
eval(A,3,2).				     % fails
eval(A,2,2).				     % succeeds
eval([(x,2)], let(var(y),var(x),var(y)), 2). % succeeds
eval([(x,V)], let(var(y),var(x),var(y)), 2). % succeeds, with V=2
eval([],plus(var(x),5),7). % fails
eval(A,plus(var(x),5),7). % fails: arguments insufficiently instantiated (why?)
eval([],if(true,let(var(x),2,var(x)),2),2).
eval([],app(app(fun(var(x),fun(var(y),plus(var(x),var(y)))),1),2),3). % eval to true 
eval([],let(var(x),app(fun(var(x),fun(var(y),plus(var(x),var(y)))),1),app(var(x),2)),3).
eval([],let(var(x),app(fun(var(x),fun(var(y),plus(var(x),var(y)))),1),dynapp(var(x),2)),V). % fails (dyn scoping)
*/