1:- module(primrecfast, []). 2:- use_module(engine). 3% :- expects_dialect(pac). 4term_expansion --> pac:expand_pac. 5:- use_module(op). 6:- op(1200, xfy, :=). 7 8 9% ?- run_cfgi(`(peek([@query1, @defs]), maplist(herbrand), apply(primrecfast:eval_primrec_demo))`, [query1=`fact(3)`]). 10 11% ?- eval_primrec(f(4), [f(x):= if(x, x*f(x-1), 1)], V). 12% V = 24. 13 14eval_primrec_demo(Q, Def, V):- semicolon_to_list(Def, Def0), eval_primrec(Q, Def0, V). 15 16% semicolon_to_list --> eval([primrecfast:semicolon_to_list]). 17 18 19semicolon_to_list((X;Y),A1):-!,(semicolon_to_list(X,A2),semicolon_to_list(Y,A3)),append(A2,A3,A1) . 20semicolon_to_list(X,[X]):-! . 21 22 23eval_primrec(Q, Defs, V):- eval_primrec(Q, Defs, V, module_kleene). 24 25eval_primrec(Q, Defs, V, P):- 26 Ds = [('$VALUE'(0):= Q)| Defs], % to keep '$VALUE' as a predicate name. 27 maplist(primrec_horn, Ds, Es), 28 Hs=[ (-(X,Y,Z):- primrecfast: -(X,Y,Z)), % builtin 29 (*(X,Y,Z):- primrecfast: *(X,Y,Z)), % builtin 30 (+(X,Y,Z):- primrecfast: +(X,Y,Z)) % builtin 31 |Es], 32 maplist(retract_module(P), Hs), % clear conflicting predicates 33 maplist(P:assert, Hs), 34 call(P:'$VALUE'(_, V)). 35 36primrec_horn --> {b_setval(out_arg_last, true)}, 37 fresh_variables, 38% eval([primrecfast:code]), 39 primrecfast:code, 40 current(clause(X, Y)), 41 {reduce_horn_body(Y, Y0)}, 42 peek(X:- Y0). 43 44reduce_horn_body --> 45 reduce:reduce(primrecfast:horn, 46 subtree((:-) ; (,) ; (;) ; (->))). 47 48retract_module(P, A:-_):- !, retract_module_(P, A). 49retract_module(P, A):- retract_module_(P, A). 50 51retract_module_(P, A):- functor(A, F, N), functor(B, F, N), 52 retractall(P:).
compile_primrec_horn(test, 'testout.pl').
?- primrecfast:primrec_horn(a(X):= 2, Y).
Y = a(X, 2).
?- test_compile.61% symbols--> eval([primrecfast:symbols]). 62 63 64symbols(X,[X]):-var(X),! . 65symbols([],[]):-! . 66symbols(X,[X]):-atom(X),! . 67symbols(X,[]):-atomic(X),! . 68symbols(T,A1):-T=..[A2|As],!,(symbols(As,A3),maplist(symbols,A3,A4)),union(A4,A1) . 69 70 71test_compile:- compile_primrec_horn(lib('primrecfast-example'), 72 lib('primrecfast-example.out')). 73 74compile_primrec_horn --> translate_file(primrec_horn). 75 76fresh_variables(X, Y):- symbols(X, L), fresh_bind(\(L, X), \(_, Y)). 77 78read_terms(Ts) :- read(X), 79 ( X \== end_of_file -> Ts=[X|Ts0], read_terms(Ts0) 80 ; Ts=[] 81 ). 82 83:- meta_predicate translate_file(, , ). 84 85translate_file(A, X, Y):- 86 file(X, read, read_terms(X0)), 87 maplist(A, X0, Y0), 88 file(Y, write, maplist(write_fullstop, Y0)). 89 90write_fullstop(X):- numbervars(X, 0, _, [singletons(true)]), 91 print(X), write('.'), nl. 92 93%%%%%%%% simplifying horn clauses 94 95horn(X, Y):- var(X), !, Y=X. 96horn(X, Y):- listp(X), list_goal(X, Y). 97horn((X, Y), Y):- X==true. 98horn((X, Y), X):- Y==true. 99horn(clause(X, Y), X:-Y). 100horn(X:- Y, X):- Y==true. 101 102list_goal([], true). 103list_goal([X|Y], (X, Y0)):- list_goal(Y, Y0). 104 105subcode(X, Y):- nonvar(X), listp(Y). 106 107subcode0(X, Y):- nonvar(X), nonvar(Y). 108 109 110% % ?- eval(m(ap, [code], primrecfast), a, Y). 111% code(X, (true,X), [], [], true):- var(X); number(X). 112% code(if(C, T, E), ((C0, D), V), [C, rec(B, E, T)], [(C0, B), (D, V)], true). 113% code(rec(V, T, E), ((V==0 -> T0, R=R1; E0, R=R2), R), [T, E], [(T0, R1), (E0, R2)], true). 114% code(H:=Body, clause(H0, Body0), [head(H), Body], [(H0,V), (Body0, V)], true). 115% code(head(H), (H0, V), [], [], fun_rel(F, As, H0, V)):- H=..[F|As]. 116% code(T, Code, As, Bs, primrecfast:term_code(F, Bs, Code)):- T=..[F|As]. 117 118% code(X, (true,X)) :- var(X); number(X). 119% code(if(C, T, E), (T0, V=V0; E(C0, D), V)) :- 120% code(if(C, T, E), ((C0, D), V)) :- 121% code(C, rec(B, E, T)), 122% code((C0, B), (D, V)). 123% code(rec(V, T, E), ((V==0 -> T0, R=R1; E0, R=R2), R)):- 124% code(T, E), 125% code((T0, R1), (E0, R2)). 126% code(H:=Body, clause(H0, Body0)):- 127% code(head(H), Body), 128% code((H0,V), (Body0, V)). 129% code(head(H), (H0, V)):- 130% H=..[F|As], 131% fun_rel(F, As, H0, V). 132% code(T, Code):- T=..[F|As]. 133% maplist(code, As, Bs), 134% term_code(F, Bs, Code). 135 136% 137fun_rel(F, As, G, V):- nb_getval(out_arg_last, true) 138 -> append(As, [V], Bs), G=..[F|Bs] 139 ; G=..[F,V|As]. 140 141term_code(F, As, ((Hs, G), V)):- unzip(As, Gs, Vs), 142 period_to_comma(Gs, Hs), 143 fun_rel(F, Vs, G, V). 144 145period_to_comma([], true):-!. 146period_to_comma([X|Y], (X0, Y0)):-!, 147 period_to_comma(X, X0), 148 period_to_comma(Y, Y0). 149period_to_comma(X, X).
152+(X, Y, Z):- Z is X+Y. 153-(X, Y, Z):- X>=Y-> Z is X-Y; Z=0. 154*(X, Y, Z):- Z is X*Y. 155 156% +(X, Y, Z):- X is Y+Z. 157% -(X, Y, Z):- Y>=Z-> X is Y-Z; X=0. 158% *(X, Y, Z):- X is Y*Z. 159 160% ?- codes_with(user:eval, "user:append([a,b],[c,d])", X), smash(X). 161% :- meta_predicate codes_with(2, ?, ?). 162codes_with(A, X, Y) :- herbrand(X, X0), phrase(A, X0, X1), 163 numbervars(X1, 0, _, [singletons(true)]), 164 with_output_to(codes(Y), print(X1)). 165 166% %% å®ç¾©ä¾: 167% &(N, X) ::= if(N, X, 0). 168% or(N, X) ::= if(N, 1, X). 169 170% %% éä¹é¢æ° 171% fact(N) := rec(1, N * fact(N-1)). 172 173% %% ç´ æ°å¤å® 174% zero(N) := (N=0). 175% not(N) := zero(N). 176% prime(X) := &(X>1, not(has_factor(X, X))). 177% positive(N) := N>0. 178% has_factor(N, Y) := rec(0, &((N-1)>1, or(mod(Y, N-1)=0, has_factor(N-1, Y)))). 179 180% %% eval/2 181% % ?- eval_(3+3, X). 182% % X = 6 183% % ?- eval_(prime(5), X). 184% % X = 1 185 186% eval_(X, X):- var(X), !. 187% eval_(X, X):- integer(X), !, X>=0. 188% eval_(if(X, Y, Z), V):- eval_(X, V0), 189% (V0==0 -> eval_(Z, V); eval_(Y, V)). 190% eval_(X, V):- (X::= Body), eval_(Body, V). 191% eval_(T, V):- mapterm(primrecfast:eval_, T, T0), pr_apply(T0, V). 192 193% % pr_apply/2 194% pr_apply(X > Y, V):- !, X > Y -> V=1; V=0. 195% pr_apply(X = Y, V):- !, X==Y -> V=1; V=0. 196% pr_apply(X // Y, V):- !, V is X // Y. 197% pr_apply(X mod Y, V):- !, V is X mod Y. 198% pr_apply(X*Y, V):- !, V is X*Y. 199% pr_apply(X^Y, V):- !, V is X^Y. 200% pr_apply(X+Y, V):- !, V is X+Y. 201% pr_apply(X-Y, V):- !, X>Y -> V is X-Y; V=0. 202% pr_apply(X, Y):- :=(X, Body), !, pr_apply(X, Body, Y). 203% pr_apply(X, X). 204 205% % pr_apply/3 206% pr_apply(X, rec(A, B), V):- !, arg(1, X, N), (N==0 -> eval_(A, V); eval_(B, V)). 207% pr_apply(_, rec(N, A, B), V):- !, (N==0 -> eval_(A, V); eval_(B, V)). 208% pr_apply(_, Body, V):- eval_(Body, V). 209 210 211% subst_var(X, Y):- subst_var(X, Y, [], _). 212 213% subst_var(X, X, A, A):- (integer(X); var(X)), !. 214% subst_var(X, V, A, B):- atom(X), variable(X), !, assoc_var(X, V, A, B). 215% subst_var(X, Y, A, B):- X=..[X0|Xs], subst_var_list(Xs, Ys, A, B), 216% Y =..[X0|Ys]. 217 218% subst_var_list([], [], A, A). 219% subst_var_list([X|Xs], [Y|Ys], A, B):- subst_var(X, Y, A, A0), 220% subst_var_list(Xs, Ys, A0, B). 221 222% variable(X):- atom_codes(X, C), expr((code(lower), *code(digit)), C, []). 223 224%%%%%% sample translation %%%% 225% input (primitive recursive defition) 226% fact(n) := rec(n, 1, n * fact(n-1)). 227% zero(n) := rec(n, 1, 0). 228% not(n) := rec(n, 1, 0). 229% &(n, x) := rec(n, 0, not(zero(x))). 230% or(x, y) := not(&(not(x), not(y))). 231% positive(n) := rec(n, 0, 1). 232% (x > y) := positive(x - y). 233% (x=y) := &(zero(x-y), zero(y-x)). 234% mod_aux(m, r) := if(m-r>1, r+1, 0). 235% mod(x, m) := rec(x, 0, mod_aux(m, mod(x-1, m))). 236% prime(x) := &(x>1, not(has_a_factor(x, x))). 237% has_a_factor(n, y) := rec(n, 0, &((n-1) >1, or(mod(y,(n-1))=0, has_a_factor(n-1, y)))).
fact(B, C):-B==0->C=1; (-(B, 1, D), fact(D, E), *(B, E, F)), C=F.
zero(B, C):-B==0->C=1;C=0.
not(B, C):-B==0->C=1;C=0.
&(B, D, C):-B==0->C=0; (zero(D, E), not(E, F)), C=F.
or(B, C, G):-not(B, D), not(C, E), &(D, E, F), not(F, G).
positive(B, C):-B==0->C=0;C=1.
>(B, C, E):- -(B, C, D), positive(D, E).
=(B, C, H):- -(B, C, D), zero(D, F), -(C, B, E), zero(E, G), &(F, G, H).
mod_aux(B, C, F):- -(B, C, D), >(D, 1, E), (E==0->F=0;+(C, 1, G), F=G).
mod(B, E, C):-B==0->C=0; (-(B, 1, D), mod(D, E, F), mod_aux(E, F, G)), C=G.
prime(B, F):- >(B, 1, D), has_a_factor(B, B, C), not(C, E), &(D, E, F).
has_a_factor(B, E, C):-B==0->C=0; (-(B, 1, D), >(D, 1, Ko), -(B, 1, F), mod(E, F, G), =(G, 0, I), -(B, 1, H), has_a_factor(H, E, J), or(I, J, L), &(K, L, M)), C=M.prime(5, X).
X = 1