This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
vsc e5f4633c39 This commit was generated by cvs2svn to compensate for changes in r4,
which included commits to RCS files with non-trunk default branches.


git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@5 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
2001-04-09 19:54:03 +00:00

197 lines
5.3 KiB
Prolog

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% clp(q,r) version 1.3.2 %
% %
% (c) Copyright 1992,1993,1994,1995 %
% Austrian Research Institute for Artificial Intelligence (OFAI) %
% Schottengasse 3 %
% A-1010 Vienna, Austria %
% %
% File: expand.pl %
% Author: Christian Holzbaur christian@ai.univie.ac.at %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Perform theory-purification in the presence of
% interpreted terms.
%
:- module( expand, [expand/0, noexpand/0]).
:- dynamic expanding/0.
:- multifile
user:term_expansion/2,
user:goal_expansion/3.
:- dynamic
user:term_expansion/2,
user:goal_expansion/3.
user:term_expansion(A,B) :- % expands heads
expanding,
purify_head(A,B).
user:goal_expansion(G,M,E):- % expands bodies
M \== prolog, % quite common due to internal call_cleanups etc.
M \== expand, % this file may get loaded more than once
expanding,
purify(G,M,E).
noexpand :-
retractall(expanding).
expand :-
assert(expanding).
purify( Goal, Module, _) :- quoted( Goal, Module), !, fail.
purify( Goal, _, Expansion) :-
interpreted_relation( Goal, _Module),
!,
Expansion = {Goal}.
purify( X=Y, _Module, Expansion) :- !, % shortcut for =/2
( ( var(X) ; interpreted_term( X, Th) ),
( var(Y) ; interpreted_term( Y, Th) ),
nonvar( Th) ->
Expansion = {X=Y}
;
ra( X=Y, user, Pure, ThL, ThLTail),
ThL \== ThLTail,
ThLTail = [Pure],
l2conj( ThL, Expansion)
).
purify( Goal, _Module, Expansion) :-
nobuiltin( Goal),
ra( Goal, user, Pure, ThL, ThLTail),
ThL \== ThLTail, % ifunctors present ?
ThLTail = [Pure],
l2conj( ThL, Expansion).
nobuiltin( Goal) :-
predicate_property( Goal, built_in),
!,
fail.
nobuiltin( _).
quoted( {_}, _).
quoted( run(_,_), geler). % late goal of verify_attributes/3
quoted( resubmit_eq(_), nf). % some (all?) of its clients
quoted( resubmit_lt(_), nf).
quoted( resubmit_le(_), nf).
quoted( resubmit_ne(_), nf).
quoted( wait_linear_retry(_,_,_), nf).
quoted( fm_cp_filter(_,_,_), linear). % generator in findall/3
%
quoted( printf(_), _).
quoted( printf(_,_), _).
quoted( user_tout(_,_,_,_), _). % undef pred
%
% Identify the theory (module) involved.
%
interpreted_term( X, _) :- var(X), !, fail.
interpreted_term( X, linear) :- number(X).
interpreted_term( rat(_,_), linear). % rational constant
%
interpreted_term( #(_), linear). % Monash
interpreted_term( -(_), linear). % unary minus
interpreted_term( +(_), linear). % plus
interpreted_term( +(_,_), linear). % binary
interpreted_term( -(_,_), linear).
interpreted_term( *(_,_), linear).
interpreted_term( /(_,_), linear).
interpreted_term( pow(_,_), linear).
interpreted_term( exp(_,_), linear).
interpreted_term( ^(_,_), linear).
interpreted_term( sin(_), linear).
interpreted_term( cos(_), linear).
interpreted_term( tan(_), linear).
interpreted_term( min(_,_), linear).
interpreted_term( max(_,_), linear).
interpreted_term( abs(_), linear).
interpreted_relation( G, _) :- var(G), !, fail.
interpreted_relation( <(_,_), linear).
interpreted_relation( =<(_,_), linear).
interpreted_relation( <=(_,_), linear). % Monash
interpreted_relation( >(_,_), linear).
interpreted_relation( >=(_,_), linear).
interpreted_relation( =\=(_,_), linear).
interpreted_relation( =:=(_,_), linear).
% ----------------------------------------------------------------
%
% replace alien subterms by variables
% Special treatment for quote/1
%
%
%
ra( Term, _, Pure) --> {var(Term), !, Term = Pure}.
ra( Term, Th, Pure) -->
{
functor( Term, N, A),
functor( Pure, N, A)
},
ra( A, Term, Th, Pure).
ra( 0, _, _, _) --> !.
ra( N, Term, Th, Pure) -->
{
N1 is N-1,
arg( N, Term, Ta),
arg( N, Pure, Pa)
},
ra_one( Ta, Th, Pa),
ra( N1, Term, Th, Pure).
ra_one( Term, _, Pure) --> {var( Term), !, Pure=Term}.
ra_one( quote(Term), _, Pure) --> {!, Pure=Term}.
ra_one( Term, ParentTheory, Pure) -->
{
( interpreted_term( Term, Theory) ->
true
;
Theory=user
)
},
( { ParentTheory=Theory } ->
ra( Term, Theory, Pure)
;
ra_equate( Theory, Pure, ThPure),
ra( Term, Theory, ThPure)
).
ra_equate( user, A, B) --> !, { A=B }. % now
ra_equate( _Theory, A, B) --> [ {A=B} ]. % later
% ---------------------------------------------------------------------------
purify_head( Term, NewTerm) :-
( prolog:dcg_expansion( Term, []/*undef layout*/, Exp, _) ->
true
;
Term = Exp
),
( Exp = ?-(_) -> % don't touch these
fail
; Exp = :-(_) -> % expanded via goal_expansion
fail
; Exp = (H:-B) ->
ra( H, user, NewHead, Cl, []),
Cl = [_|_], % ifunctors in head ?
l2conj( Cl, Thc),
NewTerm = (NewHead:-Thc,B)
; % facts
ra( Exp, user, H, Cl, []),
Cl = [_|_], % ifunctors in head ?
l2conj( Cl, B),
NewTerm = (H:-B)
).
l2conj( [], true).
l2conj( [X|Xs], Conj) :-
( Xs = [], Conj = X
; Xs = [_|_], Conj = (X,Xc), l2conj( Xs, Xc)
).