eval(G, int(N), int(N)).

eval(G, cons(E1,E2), cons(V1,V2)) :- eval(G, E1, V1), eval(G, E2, V2).

eval(G, nil, nil).

eval(G, true, true).

eval(G, false, false).

eval(G, plus(E1,E2), int(V)) :-
   eval(G, E1, int(V1)), eval(G, E2, int(V2)), V is V1 + V2.

eval(G, minus(E1,E2), int(V)) :-
   eval(G, E1, int(V1)), eval(G, E2, int(V2)), V is V1 - V2.

eval(G, mult(E1,E2), int(V)) :-
   eval(G, E1, int(V1)), eval(G, E2, int(V2)), V is V1 * V2.

eval(G, blt(E1, E2), true) :-  eval(G, E1, int(V1)), eval(G, E2, int(V2)),
    V1 < V2.


eval(G, blt(E1, E2), false) :-
    eval(G, E1, int(V1)), eval(G, E2, int(V2)),
    V1 >= V2.

eval([{X,V}|_], X, V).

eval([{Y,_}|G], X, V) :- eval(G, X, V), X \= Y.

eval(G, match(E,[{P1,E1}| _]), V1) :-
    eval(G, E,V), match(G,V,P1,G1), eval(G1, E1, V1).

eval(G, match(E,[{P1,_}|L]), V1) :-
    eval(G, E, V), not_match(V,P1), eval(G,match(E,L),V1).

eval(G, fun(X,E), {fun(X,E),G}).

eval(G, app(E1, E2), V) :- eval(G, E1, {fun(X,E),G1}),
  eval(G, E2, V2), eval([{X,V2}|G1], E, V).

eval(G, let(X,E1,E2), V2) :- eval(G, E1, V1), eval([{X,V1}|G], E2, V2).

eval(G, letrec(X,E1,E2), V2) :- eval(G, E1, V1), 
   eval([{X,rec(X,V1)}|G], E2, V2).

eval(G, app(E1, E2), V) :- eval(G, E1, rec(Y,{fun(X,E),G1})),
  eval(G, E2, V2), eval([{X,V2},{Y,rec(Y,{fun(X,E),G1})}|G1], E, V).




match(G, V, var(X), [{X,V}|G]).

match(G, cons(V1,V2), cons(P1,P2), G2) :-
  match(G, V1, P1, G1), match(G1, V2, P2, G2).

match(G, true, true, G).

match(G, false, false, G).

match(G, nil, nil, G).

match(G, int(X), int(X), G).

not_match(V1,P1) :- match(G,V1,P1,G1),!,fail.
not_match(V1,P1).

ex1(letrec(g,
           fun(x,match(blt(x,int(1)),
               [{true,int(0)},
                {false,plus(x,app(g,minus(x,int(1))))}])),
           app(g, int(2)))).

ex2(letrec(append,
           fun(x,fun(y,
             match(x,
               [{nil,y},
                {cons(var(x1),var(tx)),
                 cons(x1,app(app(append,tx),y))}]))),
           app(app(append, cons(int(1),nil)),cons(int(2),nil)))).