1 | :- module(validator, [spec_predicate/2, spec_predicate_recursive/4, spec_indirection/2, spec_connective/4, spec_basic/2, | |
2 | spec_exists/1, spec_exists/2, | |
3 | true/1, atom/2, | |
4 | valid/2, valid/3, | |
5 | evaluate_spec_match/4, | |
6 | list/4, compound/4, tuple/4, | |
7 | spec_and/4, and/4, or/4 | |
8 | ]). | |
9 | ||
10 | :- use_module(library(terms), [variant/2]). | |
11 | :- use_module(library(lists)). | |
12 | :- dynamic spec_indirection/2, spec_predicate/2, spec_predicate_recursive/4, spec_connective/4. | |
13 | :- multifile spec_indirection/2, spec_predicate/2, spec_predicate_recursive/4, spec_connective/4. | |
14 | ||
15 | ||
16 | :- use_module(plspec_logger,[log/3]). | |
17 | ||
18 | ||
19 | ||
20 | spec_basic(var, var). | |
21 | spec_basic(ground, ground). | |
22 | spec_basic(nonvar, nonvar). | |
23 | spec_basic(any, true). | |
24 | ||
25 | % Definition of spec predicates | |
26 | spec_predicate(atomic, atomic). | |
27 | spec_predicate(atom, atom). | |
28 | spec_predicate(atom(X), atom(X)). %for a concrete atom | |
29 | spec_predicate(integer, integer). | |
30 | spec_predicate(number, number). | |
31 | spec_predicate(float, float). | |
32 | ||
33 | spec_predicate_recursive(compound(X), compound(X), and, and_invariant). | |
34 | spec_predicate_recursive(list(X), list(X), and, and_invariant). | |
35 | spec_predicate_recursive(tuple(X), tuple(X), and, and_invariant). | |
36 | ||
37 | spec_indirection(int, integer). | |
38 | spec_indirection([X], list(X)). | |
39 | spec_indirection(same(X), atom(X)). | |
40 | ||
41 | spec_connective(and([H|T]), spec_and([H|T]), and, and_invariant). | |
42 | spec_connective(one_of(X), spec_and(X), or, or_invariant). | |
43 | ||
44 | %When does a predicate exists: | |
45 | spec_exists(X) :- spec_indirection(X, _), !. | |
46 | spec_exists(X) :- spec_basic(X, _), !. | |
47 | spec_exists(X) :- spec_predicate(X, _), !. | |
48 | spec_exists(X) :- spec_predicate_recursive(X, _, _, _), !. | |
49 | spec_exists(X) :- spec_connective(X, _, _, _), !. | |
50 | spec_exists(X, indirection(Y)) :- spec_indirection(X, Y), !. | |
51 | spec_exists(X, predicate(Y)) :- spec_predicate(X, Y), !. | |
52 | spec_exists(X, predicate_recursive(A,B,C)) :- spec_predicate_recursive(X, A, B, C), !. | |
53 | spec_exists(X, connective(A,B,C)) :- spec_connective(X, A, B, C), !. | |
54 | ||
55 | :- public true/1. | |
56 | true(_). | |
57 | :- public atom/2. | |
58 | atom(X, Y) :- atom(Y), X = Y. | |
59 | ||
60 | valid(Type, Spec, Val) :- | |
61 | ground(Spec), | |
62 | evaluate_spec_match(Spec, Type, Val, Success), | |
63 | Success == true, !. | |
64 | valid(Type, Spec, Val) :- | |
65 | \+ ground(Spec), | |
66 | evaluate_spec_match(Spec, Type, Val, Success), | |
67 | Success == true. | |
68 | ||
69 | valid(Spec, Val) :- | |
70 | ground(Spec), | |
71 | evaluate_spec_match(Spec, def, Val, Success), | |
72 | Success == true, !. | |
73 | valid(Spec, Val) :- | |
74 | \+ ground(Spec), | |
75 | evaluate_spec_match(Spec, any, Val, Success), | |
76 | Success == true. | |
77 | ||
78 | ||
79 | % checks, if the spec exists. If no, fail, if yes, call evaluate_spec_match_aux | |
80 | evaluate_spec_match(Spec, _Type, _, fail(spec_not_found(spec(Spec)))) :- | |
81 | nonvar(Spec), | |
82 | \+ spec_exists(Spec), !, | |
83 | log(warning,'spec ~w not found~n', [Spec]). | |
84 | ||
85 | evaluate_spec_match(Spec, Type, Val, Res) :- | |
86 | evaluate_spec_match_case(Spec, Type,Val, Res). | |
87 | ||
88 | %evaluate_spec_match_aux matches the value Val against the existing spec Spec. | |
89 | % There are different kinds of spec predicates: | |
90 | ||
91 | %spec was an alias for another spec | |
92 | evaluate_spec_match_aux(Spec, Type, Val, Res) :- | |
93 | spec_indirection(Spec, NewSpec), | |
94 | evaluate_spec_match(NewSpec, Type, Val, Res). | |
95 | ||
96 | % a basic spec %TODO: find better name | |
97 | evaluate_spec_match_case(Spec, def, Val, Res) :- | |
98 | spec_basic(Spec, Predicate), | |
99 | !, | |
100 | %% HACK: copy_term does weird things to co-routines | |
101 | copy_term(Val, Vali), | |
102 | (call(Predicate, Val) -> | |
103 | Res = true | |
104 | ; | |
105 | Res = fail(spec_not_matched(spec(Spec), value(Val))) | |
106 | ), | |
107 | (copy_term(Val, Valii), variant(Valii, Vali) -> | |
108 | true | |
109 | ; | |
110 | log(error,'implementation of spec ~w binds variables but should not~n', [Predicate]) | |
111 | ). | |
112 | ||
113 | % a normal spec predicate | |
114 | evaluate_spec_match_case(Spec, _Type, Val, Res) :- | |
115 | spec_predicate(Spec, Predicate), | |
116 | !, | |
117 | %% HACK: copy_term does weird things to co-routines | |
118 | copy_term(Val, Vali), | |
119 | (call(Predicate, Val) -> | |
120 | Res = true, | |
121 | (chec_variant(Val, Vali) -> | |
122 | true | |
123 | ; | |
124 | log( | |
125 | error, | |
126 | 'implementation of spec ~w binds variables but should not~n', | |
127 | [Predicate]) | |
128 | ) | |
129 | ; | |
130 | Res = fail(spec_not_matched(spec(Spec), value(Val))) | |
131 | ). | |
132 | ||
133 | % a recursive spec | |
134 | evaluate_spec_match_case(Spec, Type, Val, Res) :- | |
135 | spec_predicate_recursive(Spec, Predicate, MergePred, _MergePredInvariant), | |
136 | !, | |
137 | copy_term(Val, Vali), | |
138 | (call(Predicate, Val, NewSpecs, NewVals) -> | |
139 | call(MergePred, NewSpecs, Type, NewVals, Res), | |
140 | (chec_variant(Val, Vali) -> | |
141 | true | |
142 | ; | |
143 | log( | |
144 | error, | |
145 | 'implementation of spec ~w binds variables but should not~n', | |
146 | [Predicate] | |
147 | ) | |
148 | ) | |
149 | ; | |
150 | Res = fail(spec_not_matched(spec(Spec), value(Val))) | |
151 | ). | |
152 | % a connective spec | |
153 | evaluate_spec_match_case(Spec, Type, Val, Res) :- | |
154 | nonvar(Spec), | |
155 | spec_connective(Spec, Predicate, MergePred, _MergePredInvariant), | |
156 | !, | |
157 | copy_term(Val, Vali), | |
158 | (call(Predicate, Val, NewSpecs, NewVals) -> | |
159 | call(MergePred, NewSpecs, Type, NewVals, Res), | |
160 | (chec_variant(Val, Vali) -> | |
161 | true | |
162 | ; | |
163 | log( | |
164 | error, | |
165 | 'implementation of spec ~w binds variables but should not~n', | |
166 | [Predicate]) | |
167 | ) | |
168 | ; | |
169 | Res = fail(spec_not_matched(spec(Spec), value(Val))) | |
170 | ). | |
171 | %spec was an alias for another spec | |
172 | evaluate_spec_match_case(Spec, Type, Val, Res) :- | |
173 | spec_indirection(Spec, NewSpec), | |
174 | evaluate_spec_match(NewSpec, Type, Val, Res). | |
175 | ||
176 | ||
177 | :- if(current_prolog_flag(dialect,sicstus)). | |
178 | % in SICStus copy_term discards co-routines and variant does not examine co-routines or attributes | |
179 | chec_variant(Val,Vali) :- variant(Val,Vali). | |
180 | :- else. | |
181 | % for SWI copy_term copies co-routines and variant does examine them | |
182 | % for some reason this check was added in b7cb63b041fd25e91aa082e15e6450666b627035 | |
183 | % to allow plspec to attach co-routines to Val without raising the above error message | |
184 | % however, it does not seem to work with 7.2.2 | |
185 | chec_variant(Val,Vali) :- copy_term(Val, Valii), variant(Valii, Vali). | |
186 | :- endif. | |
187 | ||
188 | % built-in recursive specs | |
189 | list(Spec, Val, NewSpecs, NewVals) :- | |
190 | nonvar(Val), list1(Val, Spec, NewSpecs, NewVals). | |
191 | %% list1 only ensures that the value is a list. | |
192 | %% The type of its members is checked later on in a seperate step. | |
193 | %% list1 will return a spec for each member. | |
194 | %% If a tail is a variable, the bound value should be | |
195 | %% of the same type as the list itself. | |
196 | list1(L, Spec, [Spec|ST], [H|VT]) :- | |
197 | nonvar(L), L = [H|T], !, | |
198 | list1(T, Spec, ST, VT). | |
199 | list1(L, _, [], []) :- | |
200 | nonvar(L), L = [], !. | |
201 | list1(Var, Spec, [list(Spec)], [Var]) :- var(Var). | |
202 | ||
203 | :- public compound/4. | |
204 | compound(Spec, Val, NewSpecs, NewVars) :- | |
205 | compound(Val), | |
206 | Val =.. [Functor|NewVars], | |
207 | Functor \= '[|]', | |
208 | length(NewVars, Len), | |
209 | length(NewSpecs, Len), | |
210 | Spec =.. [Functor|NewSpecs]. | |
211 | ||
212 | :- public tuple/4. | |
213 | tuple(SpecList, VarList, SpecList, VarList) :- | |
214 | is_list(VarList). | |
215 | ||
216 | spec_and(SpecList, Var, SpecList, VarRepeated) :- | |
217 | SpecList \= [], | |
218 | %% this is actually repeat | |
219 | length(SpecList,L), | |
220 | length(VarRepeated,L), | |
221 | maplist(=(Var), VarRepeated). | |
222 | ||
223 | :- public and/4. | |
224 | and([], _, [], true). | |
225 | and([S|Specs], Type, [V|Vals], Res) :- | |
226 | evaluate_spec_match(S, Type, V, X), | |
227 | (X == true -> | |
228 | and(Specs, Type, Vals, Res) | |
229 | ; | |
230 | Res = fail(spec_not_matched(spec(S), value(V))) | |
231 | ). | |
232 | ||
233 | :- public or/4. | |
234 | or(Specs, Type, Vals, true) :- | |
235 | or2(Specs, Type, Vals). | |
236 | or(Specs, _, Vals, fail(spec_not_matched_merge(specs(or(Specs)), values(Vals)))). | |
237 | ||
238 | or2([HSpec|TSpec], Type, [HVal|TVal]) :- | |
239 | evaluate_spec_match(HSpec, Type, HVal, X), | |
240 | (X == true -> | |
241 | true | |
242 | ; | |
243 | or2(TSpec, Type, TVal) | |
244 | ). |