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