1/* Part of Extended Libraries for SWI-Prolog 2 3 Author: Edison Mera 4 E-mail: efmera@gmail.com 5 WWW: https://github.com/edisonm/xlibrary 6 Copyright (C): 2015, Process Design Center, Breda, The Netherlands. 7 All rights reserved. 8 9 Redistribution and use in source and binary forms, with or without 10 modification, are permitted provided that the following conditions 11 are met: 12 13 1. Redistributions of source code must retain the above copyright 14 notice, this list of conditions and the following disclaimer. 15 16 2. Redistributions in binary form must reproduce the above copyright 17 notice, this list of conditions and the following disclaimer in 18 the documentation and/or other materials provided with the 19 distribution. 20 21 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 22 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 23 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 24 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 25 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 26 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 27 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 28 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 29 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 30 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 31 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 32 POSSIBILITY OF SUCH DAMAGE. 33*/ 34 35:- module(abstract_slicer, 36 [ abstract_slice/3, 37 abstract_slice/4, 38 apply_mode/5, 39 slicer_abstraction/7 40 ]). 41 42:- use_module(library(apply)). 43:- use_module(library(lists)). 44:- use_module(library(option)). 45:- use_module(library(pure)). 46:- use_module(library(abstract_interpreter)). 47:- use_module(library(terms_share)). 48 49:- meta_predicate 50 abstract_slice(,,), 51 abstract_slice(,,,), 52 slicer_abstraction(,,,,, ,).
61abstract_slice(M:Head, Mode, OptL) :-
62 abstract_slice(M:Head, Mode, OptL, _).Example:
consider the next predicate:
popt('option'(A), []) :- member(A, [1,2,3]).
popt('option 1', Answer) :- append(_,_,Answer).
popt('option 2', Answer) :- member(Answer, [1,2,3]).
popt('option 3', []) :- member(_Answer, [1,2,3]).
If we just execute the predicate with Answer uninstatiated, we will get infinite solutions, but:
?- abstract_slice(popt(A,X),[+,?],[]). A = option(1) ; A = option(2) ; A = option(3) ; A = 'option 1' ; A = 'option 2' ; A = 'option 3'.
Will 'abstract' the execution of popt/2 to get all the matches of A, slicing out X
97abstract_slice(M:Head, Mode, OptL, State) :- 98 apply_mode(Head, Mask, Mode, Spec, RevS), 99 term_variables(RevS, VarsR), 100 option(eval_scope(Scope), OptL, body), 101 abstract_interpreter(M:Mask, slicer_abstraction(Spec, VarsR, Scope), OptL, State), 102 % In Mask the output arguments are variable, so the binding is performed 103 % after the abstract interpretation. This is a bit inefficient, but correct: 104 Head = Mask. 105 106apply_mode(Call, Mask, Mode, Spec, RevS) :- 107 functor(Call, F, A), 108 functor(Mask, F, A), 109 functor(Spec, F, A), 110 functor(RevS, F, A), 111 apply_mode_arg(1, Call, Mask, Mode, Spec, RevS). 112 113apply_mode_arg(N1, Call, Mask, Mode, Spec, RevS) :- 114 arg(N1, Call, Arg), !, 115 arg(N1, Mask, Var), 116 arg(N1, Mode, MSp), 117 arg(N1, Spec, ASp), 118 arg(N1, RevS, ARs), 119 ( MSp = - 120 ->ASp = Var, 121 ARs = - 122 ; ASp = +, 123 ARs = Arg, 124 Arg = Var 125 ), 126 succ(N1, N), 127 apply_mode_arg(N, Call, Mask, Mode, Spec, RevS). 128apply_mode_arg(_, _, _, _, _, _). 129 130chain_of_dependencies(Spec, VarsR, Goal, ContL) :- 131 \+ ground(Goal), 132 ( terms_share(Spec, VarsR, Goal) 133 ->true 134 ; select(Cont, ContL, ContL2), 135 terms_share(Cont, VarsR, Goal), 136 chain_of_dependencies(Spec, VarsR, Cont, ContL2) 137 ), 138 !. 139 140slicer_abstraction(Spec, VarsR, Scope, MGoal, Body) --> 141 {predicate_property(MGoal, interpreted)}, 142 !, 143 {strip_module(MGoal, M, Goal)}, 144 get_state(state(Loc1, EvalL, OnErr, CallL, Data, Cont, Result1)), 145 { \+ ground(Spec), 146 chain_of_dependencies(Spec, VarsR, Goal, Cont) 147 ->match_head_body(M:Goal, Body1, Loc), 148 ( Scope = body 149 ->( terms_share(Spec, VarsR, Goal) 150 ->Body = Body1 151 ; Body1 = CM:Body2, 152 Body = CM:once(Body2) 153 ) 154 ; terms_share(Spec, VarsR, Goal) 155 ->Body = Body1 156 ; Body = M:true 157 ) 158 ; % if no side effects, increase precision executing the body: 159 ( Scope = body_if_impure % This branch is not tested yet: --EM 160 ->( match_head_body(M:Goal, Body1, Loc), 161 is_pure_body(Body1, is_impure_or_requires_subst(EvalL)) 162 ->catch(call(Body1), _, true), % catch in case of not enough instantiation 163 Body = M:true 164 ; match_head_body(M:Goal, Body1, Loc), 165 ( is_pure_body(Body1, requires_subst(EvalL)) 166 ->Body = M:true 167 ; Body = Body1 168 ) 169 ) 170 ; ( Scope = body % check if the body trivially fails: 171 ->once(( match_head_body(M:Goal, Body1, Loc), 172 ( is_pure_body(Body1) 173 ->catch(call(Body1), _, true) 174 ; true 175 ) 176 )) 177 ; Loc = Loc1 178 ), 179 Body = M:true 180 ) 181 }, 182 { Scope = head 183 ->Result = bottom % Kludge to avoid cut remove solutions 184 ; Result = Result1 185 }, 186 put_state(state(Loc, EvalL, OnErr, CallL, Data, Cont, Result)). 187slicer_abstraction(_, _, _, MGoal, M:true) --> 188 get_state(state(Loc, _, OnError, CallL, _, _, _)), 189 { call(OnError, error(existence_error(evaluation_rule, MGoal), Loc)), 190 call(OnError, call_stack(CallL)), 191 strip_module(MGoal, M, _) 192 }, 193 bottom. 194 195is_impure_or_requires_subst(_, Pred) :- is_impure(Pred). 196is_impure_or_requires_subst(EvalL, Pred) :- requires_subst(EvalL, Pred). 197 198pattern_eval(H, I, _ +\ (I:H as _)). 199pattern_eval(H, I, _ +\ (I:H :- _)). 200pattern_eval(H, I, I:F/A) :- functor(H, F, A). 201 202requires_subst(EvalL, M:H) :- 203 predicate_property(M:H, implementation_module(I)), 204 pattern_eval(H, I, Pattern), 205 memberchk(Pattern, EvalL), 206 !. 207 208prologmessage(call_stack(CallL)) --> foldl(call_at, CallL). 209 210call_at(Call-Loc) --> 211 [" "], '$messages':swi_location(Loc), ["~q"-[Call], nl]
Abstract slicer
Implements the next abstract domain: find possible matches of output arguments of the given predicate.
*/