1% ----------------------------------------------------------------------
2% BEGIN LICENSE BLOCK
3% Version: CMPL 1.1
4%
5% The contents of this file are subject to the Cisco-style Mozilla Public
6% License Version 1.1 (the "License"); you may not use this file except
7% in compliance with the License.  You may obtain a copy of the License
8% at www.eclipse-clp.org/license.
9%
10% Software distributed under the License is distributed on an "AS IS"
11% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied.  See
12% the License for the specific language governing rights and limitations
13% under the License.
14%
15% The Original Code is  The ECLiPSe Constraint Logic Programming System.
16% The Initial Developer of the Original Code is  Cisco Systems, Inc.
17% Portions created by the Initial Developer are
18% Copyright (C) 1989-2006 Cisco Systems, Inc.  All Rights Reserved.
19%
20% Contributor(s): ECRC GmbH
21%
22% END LICENSE BLOCK
23%
24% System:	ECLiPSe Constraint Logic Programming System
25% Version:	$Id: peval.pl,v 1.1 2008/06/30 17:43:48 jschimpf Exp $
26% ----------------------------------------------------------------------
27
28/*
29Partial evaluator for pure Prolog plus ineq, ~=, cut and not. No other
30builtins. Uses no cut execution rules, but uses auxiliary predicate
31creation to preserve correctness. Needs directives `unfold(G)'. No
32folding or generalisation is done.
33*/
34
35pe(InFile,OutFile) :-
36   erase_all(program), readprog(InFile), setval(newname,0),
37   unfold_loop, writeto(OutFile), show_program, written, !.
38
39unfold_loop :-
40   recorded(program,F/A/L), splitlist(L,L1,(H:-T),L2),
41   splitconj(T,T1,G,T2), want_to_unfold(G), !, unfold(G,U),
42   (cutcalls(U) -> acc(H,T1,G,T2,N),
43                   append(L1,[(H:-T1,N)],L2), append(L2,T2,L3)
44                 ; expand(H,T1,G=U,T2,X),
45                   append(L1,X,L1U), append(L1U,L2,L3)),
46   erase(program,F/A/_), record(program,F/A/L3),
47   unfold_loop.
48unfold_loop.
49
50acc(H,T1,G,T2,N) :-
51   cj(G,T2,GT2), newpred(N,GT2,H+T1), cj(T1,GT2,X), addclause((N:-X)).
52
53newpred(N,R,V) :- varset(R,S), intersect(S,V,S1), newpred1(N,S1).
54
55newpred1(N,S) :-
56   getval(newname,I), atom_string(aux,Aux), term_string(I,Istr),
57   append_strings(Aux,Istr,Nstr), atom_string(Name,Nstr),
58   N=..[Name|S], incval(newname).
59
60varset(T,S) :- varset(T,Z-Z,S-[]), !.
61
62varset(T,Si,So) :- var(T), not vdmember(T,Si), !, dappend(Si,[T|Z]-Z,So).
63varset(T,Si,Si) :- var(T), !.
64varset(T,Si,So) :- T=..[_|L], varsetl(L,Si,So).
65
66varsetl([],Si,Si).
67varsetl([H|T],Si,So) :- varset(H,Si,St), varsetl(T,St,So).
68
69vdmember(V,A-B) :- A==B, !, fail.
70vdmember(V,[A|B]-C) :- V==A; vdmember(V,B-C).
71
72dappend(A-B,B-C,A-C).
73
74intersect([],_,[]) :- !.
75intersect([A|B],V,[A|C]) :- occurs(A,V), !, intersect(B,V,C).
76intersect([_|B],V,C) :- intersect(B,V,C).
77
78splitlist([A|B],[A|C],D,E) :- splitlist(B,C,D,E).
79splitlist([A|B],[],A,B).
80
81splitconj(((A,B),C),D,E,F) :- !, splitconj((A,B,C),D,E,F).
82splitconj((A,B),AC,D,E) :- splitconj(B,C,D,E), cj(A,C,AC).
83splitconj((A,B),true,A,B) :- !.
84splitconj(A,true,A,true).
85
86want_to_unfold(G) :- unfold(G).
87
88unfold(A,[A]) :- builtin(A), !, A.
89unfold(A,L) :- functor(A,P,Q), recorded(program,P/Q/AL), !,
90               matches(AL,A,L1), L=L1.
91unfold(_,[]).
92
93matches(L,G,L1) :- matches1(L,G,L2), final_cut(L2,L1).
94
95matches1([],_,[]) :- !.
96matches1([(A:-B)|C],D,E) :- not unify(A,D), !, matches1(C,D,E).
97matches1([(A:-!)|C],D,[(A:-true)]) :- instance(D,A), !.
98matches1([(A:-!,B)|C],D,[(A:-B)]) :- instance(D,A), !.
99matches1([(A:-B)|C],D,[(A:-B)|E]) :- matches1(C,D,E).
100
101final_cut([],[]) :- !.
102final_cut([(A:-!)],[(A:-true)]) :- !.
103final_cut([(A:-!,B)],[(A:-B)]) :- !.
104final_cut([A|L],[A|L1]) :- final_cut(L,L1).
105
106cutcalls(L) :- not not (member((_:-T),L), hascuts(T)).
107
108hascuts((A,B)) :- !, (hascuts(A); hascuts(B)).
109hascuts(!).
110
111suspendable(!) :- !.
112suspendable(ineq(V,A,B)) :- !, not unfold_ineq(V,A,B).
113suspendable(A~=B) :- !, not unfold_ineq([],A,B).
114suspendable((not G)) :- !.
115suspendable(F) :- not unfold(F).
116
117unfold_ineq(V,A,B) :- A==B.
118unfold_ineq(V,A,B) :- copy_term(V,V1), not (A=B, variant(V,V1)).
119
120builtin(ineq(_,_,_)).
121builtin(_ ~= _).
122
123readprog(F) :-
124   clear_declarations, open(F,read,input_file), open(temp,write,decs_file),
125   readclauses(prog_mode), close(input_file), close(decs_file),
126   compile(temp).
127
128readclauses(prog_mode) :- read(input_file,X), X\==end_of_file, !,
129                          clause_process(X,Mode), readclauses(Mode).
130readclauses(decs_mode) :- read(input_file,X), X\==end_of_file, !,
131                          write(decs_file,X), writeln(decs_file,"."),
132                          readclauses(decs_mode).
133readclauses(_).
134
135clear_declarations :-
136   open(temp,write,decs_file), writeln(decs_file,"open(dummy)."),
137   close(decs_file), compile(temp).
138
139clause_process(declarations,decs_mode) :- !.
140clause_process((P:-T),prog_mode) :- !, addclause((P:-T)),
141                                       program_clause(P,T).
142clause_process(X,prog_mode) :- addclause((X:-true)),
143                               program_clause(X,true).
144
145program_clause(H,T) :- functor(H,F,A), recorded(program,F/A/L),
146                       member((X:-T),L), unify(H,X).
147
148show_program :- recorded(program,_/_/P), wrn(""), member(C,P),
149                writeclau(C), fail.
150show_program.
151
152writeto(F) :- open(F,write,file), set_stream(result,file).
153
154written :- set_stream(result,output), close(file).
155
156res(F) :- writeto(F), show_program, written.
157
158writeclau(C) :- writeclau1(C), fail.
159writeclau(_).
160
161writeclau1((H:-true)) :- !,
162   writeclau1(H).
163writeclau1((H:-T)) :- !,
164   clarify((H:-T)), wr(H), wrn(" :-"), writebody(T), wrn(".").
165writeclau1(H) :-
166   clarify(H), wr(H), wrn(".").
167
168writebody(((A,B),C)) :- !, writebody((A,B,C)).
169writebody((A,B)) :- !, writebody(A), wrn(","), writebody(B).
170writebody((A;B)) :- !, wr("("), writebody(A), wrn(";"), writebody(B), wr(")").
171writebody(call(A)) :- !, writebody(A).
172writebody(A) :- wr("   "), wr(A).
173
174wr(X) :- write(result,X).
175wrn(X) :- writeln(result,X).
176wrc(X) :- not not (clarify(X), wr(X)).
177wrnc(X) :- not not (clarify(X), wrn(X)).
178
179clarify(T) :- clarify1(65,_,T).
180
181clarify1(Ni,Ni,_) :- Ni>89, !.
182clarify1(Ni,No,T) :- var(T), !, No is Ni+1, char_int(X,Ni), atom_string(T,X).
183clarify1(Ni,No,T) :- T=..[_|L], clarify1l(Ni,No,L).
184
185clarify1l(Ni,Ni,[]) :- !.
186clarify1l(Ni,No,[H|T]) :- clarify1(Ni,Nt,H), clarify1l(Nt,No,T).
187
188expand(_,_,_=[],_,[]).
189expand(H,T1,G=[(G1:-T)|L],T2,[(Hc:-A)|B]) :-
190   copy_term((H,T1,G,T2),(Hc,T1c,Gc,T2c)), G1=Gc,
191   cj(T1c,T,T3), cj(T3,T2c,A), expand(H,T1,G=L,T2,B).
192
193cj(true,X,X) :- !.
194cj(X,true,X) :- !.
195cj(X,Y,(X,Y)).
196
197unify(A,B) :- var(A), !, unify1(A,B).
198unify(A,B) :- var(B), !, unify2(B,A).
199unify(A,B) :- A=..[F|LA], B=..[F|LB], unifyl(LA,LB).
200
201unify1(A,B) :- var(B), !, A=B.
202unify1(A,B) :- occurs(A,B), !, fail.
203unify1(A,A).
204
205unify2(A,B) :- occurs(A,B), !, fail.
206unify2(A,A).
207
208unifyl([],[]) :- !.
209unifyl([A|LA],[B|LB]) :- unify(A,B), unifyl(LA,LB).
210
211addclause((H:-T)) :- functor(H,F,A), erase_program(F/A/L),
212                     append(L,[(H:-T)],L1), record(program,F/A/L1).
213
214erase_program(F/A/L) :- erase(program,F/A/L), !.
215erase_program(F/A/[]).
216
217?- set_stream(result,output), set_flag(gc,on), set_flag(gc_interval,500000).
218