25:- use_module(library(lists)). 26
30
31progol_engine(aleph).
32
33
34:- multifile legitimate_literal/1. 35
36set_def(refinethreadvar, refineop,
37 'Description',
38 templatevar, 'thread',
39 show).
40
41set_def(refinelitgen, refineop,
42 'Description',
43 [modes, user], modes,
44 show).
45
46lith(Head) :-
47 progol_engine(Engine),
48 lith(Engine, Head).
49
50litb(Lit) :-
51 progol_engine(Engine),
52 litb(Engine, Lit).
53
54
55thread_type(Type) :-
56 setting(refinethreadvar, Type).
57
58lith(aleph, Head) :-
59 '$aleph_global'(modeh, modeh(_, Head)).
60
61litb(aleph, Lit) :-
62 '$aleph_global'(modeb, modeb(_, Lit)).
63
64refine(A, B) :-
65 setting(construct_bottom, saturation)
66 -> refine_bot(A, B)
67 ; refine_lazy(A, B).
68
69refine_lazy(nil, Clause) :-
70 lith(HeadTemplate),
71 functor(HeadTemplate, Name, Arity),
72 functor(Head, Name, Arity),
73 Clause = (Head).
74
75refine_lazy((Head:-Body), (Head:-Body2)):- !,
76 generate_lit(Lit),
77 copy_term(Body, Body1),
78 append_thread(Lit, Body1, Body2),
79 connect_thread((Head:-Body2)).
80
81refine_lazy(Head, Clause) :- !,
82 refine_lazy((Head:-true), Clause).
83
84
85generate_lit(Lit) :-
86 setting(refinelitgen, user)
87 -> legitimate_literal(Lit)
88 ; generate_lit_modes(Lit).
89
90generate_lit_modes(Lit) :-
91 find_mode(modeb, Name/Arity, Mode),
92 functor(Lit, Name, Arity),
93 split_args(Lit, Mode, _Inputs, _Outputs, Constants),
94 generate_constants(Lit, Constants).
95
96generate_constants(Lit, []).
97generate_constants(Lit, [Type/Place|Z]) :-
98 arg(Lit, Place, ConArg),
99 call(Type,ConArg),
100 generate_constants(Lit, Z).
101
102
103subset([], []).
104subset([X|L], [X|S]) :- subset(L, S).
105subset(L, [_|S]) :- subset(L, S).
106
107unordered_subset(Set, SubSet):-
108 length(Set, LSet),
109 between(0,LSet, LSubSet),
110 length(NSubSet, LSubSet),
113 subset(NSubSet,Set),
114 permutation(NSubSet, SubSet).
115
116refine_bot(nil, Clause) :-
117 bottom(BottomClause),
118 BottomClause = (Head:-Body),
119 has_pieces(Body, BottomClauseList),
120 unordered_subset(BottomClauseList, SelectedLits),
121 has_pieces(Body2, SelectedLits),
122 Clause = (Head :- Body2),
123 connect_thread(Clause).
124
125
127argp(Term, InputPlaces, OutputPlaces) :-
128 split_args(Term, _Mode, Inputs, Outputs, _Constants),
129 thread_type(Type),
130 member(InputPlaces/Type, Inputs),
131 member(OutputPlaces/Type, Outputs).
132
133inout_lit(Term, Input, Output) :-
134 functor(Term, _, Arity),
135 once(argp(Term, [InArg], [OutArg])),
136 arg(InArg, Term, Input),
137 arg(OutArg, Term, Output).
138
139inout_thread(','(A, B), Input, Output) :-
140 inout_lit(A, Input, FirstOut),
141 inout_thread(B, FirstOut, Output), !.
142
143inout_thread(Atom, Input, Output) :- inout_lit(Atom, Input, Output), !.
144
147has_pieces(','(A, R), [A|Z]) :- Z \== [], has_pieces(R, Z), !.
148has_pieces(A, [A]) :- A \== true, !.
149has_pieces(true, []) :- !.
150
153concat_thread([A], A) :- !.
154concat_thread([A|Z], ','(A, Z1)) :-
155 concat_thread(Z, Z1),
156 inout_lit(A, _, Out),
157 inout_thread(Z1, Out, _).
158
160count_literals(Lits, Count) :-
161 has_pieces(Lits, LitList),
162 length(LitList, Count).
163
166connect_thread((Head:-Body)) :-
167 inout_lit(Head, Input, Output),
168 inout_thread(Body, Input, Output), !.
169
172append_thread(Lit, Body, BodyWith) :-
173 has_pieces(Body, Atoms),
174 append(Atoms, [Lit], Atoms2),
175 concat_thread(Atoms2, BodyWith), !