EvalContML4_2.pl

% Dervation System EvalContML4
:- module('EvalContML4',[
  op(640,xfy,[$,$>]),
  op(700,xfy,=>),
  op(750,xfx,⇓),
  op(780,xfx,⊦),
  op(1200,xfx,--),
  v/1,k/1,e/1,'⊦'/2,'⇓'/2
]).

:- use_module(rtg).
term_expansion(A--B,B:-A).

% Syntax
syntax(integer). syntax(ε). syntax(k). syntax(maplist(_)).
int ::= integer. bool ::= true | false.
x ::= atom.
i ::= int.
b ::= bool.
e ::= i | b | x | e + e | e - e | e * e | e < e | if(e,e,e)
    | let(x=e ;e) | fun(x->e) | e $ e | letrec(x=(x->e); e)
    | [] | [e | e] | e$>{[]->e | [x|x]->e}
    | letcc(x; e) | {k}.
v ::= i | b | fun(ε,x->e) | rec(ε,x=(x->e)) | [] | [v|v] | {k}.
ε ::= [] | [x=v|ε].
op::= (+) | (-) | (*) | (<).
k1::= (ε⊦if(o,e,e))
    | ε⊦o+e | ε⊦o-e | ε⊦o*e | ε⊦o<e
    | v+o | v-o | v*o | v<o
    | ε⊦let(x=o;e)
    | ε⊦o$e
    | v$o
    | ε⊦[o|e]
    | [v|o]
    | ε⊦o$>{[]->e|[x|x]->e}.
k ::= maplist(k1).

% Derivation Rules:

_⊦[E|K] ⇓ _            :- writeln([E|K]),fail.                    % (E-Log)
_⊦[V|K] ⇓ V2           :- v(V),V => K ⇓ V2.                      % (E-V)
ℰ⊦[if(E1,E2,E3)|K]⇓V   :- ℰ⊦[E1,(ℰ⊦if(o,E2,E3))|K] ⇓ V.         % (E-If)
ℰ⊦[E|K] ⇓ V            :- E =..[Op,E1,E2],op(Op),E_ =..[Op,o,E2],
                           ℰ⊦[E1,(ℰ⊦ E_)|K] ⇓ V.                  % (E-BinOp)
ℰ⊦[X|K] ⇓ V2           :- member(X=V1,ℰ),V1 => K ⇓ V2.           % (E-Var)
ℰ⊦[let(X=E1;E2)|K]⇓V   :- ℰ⊦[E1,(ℰ⊦ let(X=o; E2))|K] ⇓ V.        % (E-Let)
ℰ⊦[fun(X->E)|K] ⇓ V    :- fun(ℰ,X->E) =>K ⇓ V.                   % (E-Fun)
ℰ⊦[E1 $ E2|K] ⇓ V      :- ℰ⊦[E1,(ℰ⊦o$ E2)|K] ⇓ V.                % (E-App)
ℰ⊦[letrec(X=(Y->E1);E2)|K]⇓V
                        :- [X=rec(ℰ,X=(Y->E1))|ℰ]⊦[E2|K] ⇓ V.     % (E-LetRec)
_⊦[[]|K] ⇓ V           :- [] => K ⇓ V.                            % (E-Nil)
ℰ⊦[[E1|E2]|K] ⇓ V      :- ℰ⊦[E1,(ℰ⊦[o|E2])|K] ⇓ V.               % (E-Cons)
ℰ⊦[E$>{[]->E2|[X|Y]->E3}|K]⇓V
                         :- ℰ⊦[E,ℰ⊦o$>{[]->E2|[X|Y]->E3}|K]⇓V.% (E-Match)
ℰ⊦[letcc(X; E)|K]⇓V     :- [X={K}|ℰ]⊦[E|K] ⇓ V.                  % (E-LetCc)
E => K ⇓ _                 :- writeln(E => K),fail.               % (C-Log)
V => [] ⇓ V                :- v(V).                               % (C-Ret)
V1 => [ℰ⊦ E1|K] ⇓ V2       :- E1=..[Op,o,E],op(Op),E2=..[Op,V1,o],
                               v(V1),ℰ⊦[E,E2|K] ⇓ V2.             % (C-EvalR)
I2 => [I1 + o|K] ⇓ V       :- I3 is I1 + I2,I3 => K ⇓ V.         % (C-Plus)
I2 => [I1 - o|K] ⇓ V       :- I3 is I1 - I2,I3 => K ⇓ V.         % (C-Minus)
I2 => [I1 * o|K] ⇓ V       :- I3 is I1 * I2,I3 => K ⇓ V.         % (C-Times)
I2 => [I1 < o|K] ⇓ V       :- I1 < I2,true => K ⇓ V.             % (C-Lt1)
I2 => [I1 < o|K] ⇓ V       :- I1 >= I2,false => K ⇓ V.           % (C-Lt2)
true=>[ℰ⊦if(o,E1,_)|K]⇓V   :- ℰ⊦[E1|K] ⇓ V.                      % (C-IfT)
false=>[ℰ⊦if(o,_,E2)|K]⇓V  :- ℰ⊦[E2|K] ⇓ V.                      % (C-IfF)
V1=>[ℰ⊦let(X=_;E)|K]⇓V2    :- v(V1),[X=V1|ℰ]⊦[E|K] ⇓ V2.         % (C-LetBody)
V1=>[ℰ⊦o$E|K] ⇓ V          :- v(V1),ℰ⊦[E,(V1 $ o)|K] ⇓ V.        % (C-EvalArg)
V1=>[fun(ℰ,X->E)$o|K]⇓V2   :- [X=V1|ℰ]⊦[E|K] ⇓ V2.               % (C-EvalFun)
V1=>[rec(ℰ,X=(Y->E))$o|K]⇓V:- [X=rec(ℰ,X=(Y->E)),Y=V1|ℰ]⊦[E|K]⇓V.% (C-EvalFunR)
V1=>[{K1}$o|_] ⇓ V2        :- V1=>K1 ⇓ V2.                        % (C-EvalFunC)
V1=>[ℰ⊦[o|E]|K] ⇓ V2       :- ℰ⊦[E,[V1|o]|K] ⇓ V2.               % (C-EvalConsR)
V2=>[[V1|o]|K] ⇓ V3        :- [V1|V2]=>K ⇓ V3.                    % (C-Cons)
[]=>[ℰ⊦o$>{[]->E1|[_|_]->_}|K]⇓V     :- ℰ⊦[E1|K]⇓V.              % (C-MatchNil)
[V1|V2]=>[ℰ⊦o$>{[]->_|[X|Y]->E}|K]⇓V :- [X=V1,Y=V2|ℰ]⊦[E|K]⇓V.   % (C-MatchCons)
run(E,EV) :- e(E),write(E),write(->),[]⊦[E] ⇓ V,writeln(V),!,V=EV.

:- begin_tests(run).
  test(i) :- run(1,1).
  test(b) :- run(true,true),run(false,false).
  test(x) :- run(let(x=1;x),1),run(let(abc=2;abc),2),run(let('ZZZ'=3;'ZZZ'),3).
  test(+) :- run(1+1,2).
  test(-) :- run(2-2,0).
  test(*) :- run(3*3,9).
  test(<) :- run(4<4,false).
  test(op):- run(1+2*3<1,false).
  test(if) :- run(if(true,1,2),1).
  test(if):- run(if(true,true,false),true).
  test(if):- run(if(1+2*3<1,true,false),false).
  test(let) :- run(let(z=1;z+1),2).
  test(fun) :- run(fun(z->z+1),fun([],z->z+1)). 
  test(app) :- run(fun(z->z+1) $ 3,4). 
  test(letrec) :- run(letrec(f=(z->z+1); f $ 2),3).
  test(list0) :- run([],[]).
  test(pair) :- run([1 | 2],[1|2]).
  test(list1) :- run([1],[1]).
  test(list2) :- run([1,2],[1,2]).
  test(match) :- run([]$>{[]->0 | [a|b]->a},0).
  test(match) :- run([1|2]$>{[]->0 | [a|b]->a},1).
  test(match) :- run([1|2]$>{[]->0 | [a|b]->a+b},3).
  test(letcc) :- run(letcc(k; k),{[]}).
  test(letcc) :- run(let(sm = fun(f -> (f $ 3) + (f $ 4)); letcc(k; (sm $ k))),3).
  test(letcc) :- run(2+letcc(k; 3),5).
  test(letcc) :- run(2+letcc(k; 1+(k $ 3)),5).
  test(letcc) :- run(letcc(k; 1+if(true,k$[10],2)),_).
  test(letcc) :- run(letcc(top;2+letcc(k;top $ k)),{[2 + o]}).
  test(letcc) :- run({[2 + o]},{[2 + o]}).
  test(letcc) :- run({[2 + o]}$3,5).
  test(letcc) :- run(letcc(top;let(x=1;x+2+letcc(k;top $ k))),{[3+ o]}).

:- end_tests(run).
% :- run_tests. :- halt.

:- begin_tests(k).
  test(if) :- k([[x=1,y=2]⊦if(o,x,y)]).
  test(+) :- k([[x=1]⊦o+ x]).
  test(-) :- k([[x=1]⊦o- x]).
  test(*) :- k([[x=1]⊦o* x]).
  test(<) :- k([[x=1]⊦o< x]).
  test(+) :- k([3 + o]).
  test(-) :- k([3 - o]).
  test(*) :- k([3 * o]).
  test(<) :- k([3 < o]).
  test(let) :- k([[x=1]⊦ let(z=o; z+1)]).
  test(app) :- k([[x=1]⊦ o $ x]). 
  test(app) :- k([1 $ o]). 
  test(pair) :- k([[x=1]⊦[o| 2]]).
  test(list2) :- k([[2|o]]).
  test(match) :- k([[x=1]⊦o$>{[]->0 | [a|b]->a}]).
:- end_tests(k).
:- begin_tests(e).
  test(i) :- e(1).
  test(b) :- e(true),e(false).
  test(x) :- e(x),e(abc),e('ZZZ').
  test(+) :- e(1+1).
  test(-) :- e(2-2).
  test(*) :- e(3*3).
  test(<) :- e(4<4).
  test(if) :- e(if(true,1,2)).
  test(let) :- e(let(z=1;z+1)).
  test(fun) :- e(fun(z->z+1)). 
  test(app) :- e(fun(z->z+1) $ 3). 
  test(letrec) :- e(letrec(f=(z->z+1); f $ 2)).
  test(list0) :- e([]).
  test(pair) :- e([1 | 2]).
  test(list1) :- e([1]).
  test(list2) :- e([1,2]).
  test(match) :- e([]$>{[]->0 | [a|b]->a}).
  test(letcc) :- e(letcc(x; 1+2)).
:- end_tests(e).
:- begin_tests(syntax).
  test(syntax) :- writeln(ε;((a⊦a),a)).
:- end_tests(syntax).
:- begin_tests(v).
  test(i) :- v(1),v(true),v(false).
  test(fun) :- v(fun([x=2],x->1)).
  test(rec) :- v(rec([x=2],z=(y->1))).
  test(list) :- v([]).
  test(list) :- v([1]).
  test(list) :- v([1,2]).
  test(list) :- v([1|2]).
  test(k) :- v({[]}).
  test(k_if) :- v({[[x=1,y=2]⊦if(o,x,y)]}).
  test('k +') :- v({[[x=1]⊦o+ x]}).
  test('k -') :- v({[[x=1]⊦o- x]}).
  test('k *') :- v({[[x=1]⊦o* x]}).
  test('k <') :- v({[[x=1]⊦o< x]}).
  test('k +') :- v({[3 + o]}).
  test('k -') :- v({[3 - o]}).
  test('k *') :- v({[3 * o]}).
  test('k <') :- v({[3 < o]}).
  test(k_let) :- v({[[x=1]⊦ let(z=o; z+1)]}).
  test(k_app) :- v({[[x=1]⊦ o $ x]}).
  test(k_app) :- v({[1 $ o]}).
  test(k_pair) :- v({[[x=1]⊦[o| 2]]}).
  test(k_list2) :- v({[[2|o]]}).
  test(k_match) :- v({[[x=1]⊦o$>{[]->0 | [a|b]->a}]}).
:- end_tests(v).
:- run_tests.
:- halt.