| 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 | :- multifile spec_indirection/2, spec_predicate/2, spec_predicate_recursive/4, spec_connective/4. | |
| 13 | :- dynamic 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 | true(_). | |
| 56 | ||
| 57 | atom(X, Y) :- atom(Y), X = Y. | |
| 58 | ||
| 59 | valid(Type, Spec, Val) :- | |
| 60 | ground(Spec), | |
| 61 | evaluate_spec_match(Spec, Type, Val, Success), | |
| 62 | Success == true, !. | |
| 63 | valid(Type, Spec, Val) :- | |
| 64 | \+ ground(Spec), | |
| 65 | evaluate_spec_match(Spec, Type, Val, Success), | |
| 66 | Success == true. | |
| 67 | ||
| 68 | valid(Spec, Val) :- | |
| 69 | ground(Spec), | |
| 70 | evaluate_spec_match(Spec, def, Val, Success), | |
| 71 | Success == true, !. | |
| 72 | valid(Spec, Val) :- | |
| 73 | \+ ground(Spec), | |
| 74 | evaluate_spec_match(Spec, any, Val, Success), | |
| 75 | Success == true. | |
| 76 | ||
| 77 | ||
| 78 | % checks, if the spec exists. If no, fail, if yes, call evaluate_spec_match_aux | |
| 79 | evaluate_spec_match(Spec, _Type, _, fail(spec_not_found(spec(Spec)))) :- | |
| 80 | nonvar(Spec), | |
| 81 | \+ spec_exists(Spec), !, | |
| 82 | log(warning,'spec ~w not found~n', [Spec]). | |
| 83 | ||
| 84 | evaluate_spec_match(Spec, Type, Val, Res) :- | |
| 85 | evaluate_spec_match_case(Spec, Type,Val, Res). | |
| 86 | ||
| 87 | %evaluate_spec_match_aux matches the value Val against the existing spec Spec. | |
| 88 | % There are different kinds of spec predicates: | |
| 89 | ||
| 90 | ||
| 91 | spec_basic_or_normal_pred(Spec,Predicate) :- spec_basic(Spec, Predicate). | |
| 92 | spec_basic_or_normal_pred(Spec,Predicate) :- spec_predicate(Spec, Predicate). | |
| 93 | ||
| 94 | spec_recursive_or_connective(Spec,Predicate,MergePred) :- | |
| 95 | spec_predicate_recursive(Spec, Predicate, MergePred, _MergePredInvariant). | |
| 96 | spec_recursive_or_connective(Spec,Predicate,MergePred) :- nonvar(Spec), | |
| 97 | spec_connective(Spec, Predicate, MergePred, _MergePredInvariant). | |
| 98 | ||
| 99 | ||
| 100 | % a basic spec %TODO: find better name | |
| 101 | evaluate_spec_match_case(Spec, def, Val, Res) :- | |
| 102 | spec_basic_or_normal_pred(Spec, Predicate), | |
| 103 | !, | |
| 104 | prepare_check_variant(Val, Vali), | |
| 105 | (call(Predicate, Val) -> | |
| 106 | Res = true, | |
| 107 | (check_variant(Val, Vali) -> | |
| 108 | true | |
| 109 | ; | |
| 110 | log(error,'implementation of spec ~w binds variables but should not~n', [Predicate]) | |
| 111 | ) | |
| 112 | ; | |
| 113 | Res = fail(spec_not_matched(spec(Spec), value(Val))) | |
| 114 | ). | |
| 115 | % a recursive or connective spec | |
| 116 | evaluate_spec_match_case(Spec, Type, Val, Res) :- | |
| 117 | spec_recursive_or_connective(Spec, Predicate, MergePred), | |
| 118 | !, | |
| 119 | prepare_check_variant(Val, Vali), | |
| 120 | (call(Predicate, Val, NewSpecs, NewVals) -> | |
| 121 | call(MergePred, NewSpecs, Type, NewVals, Res), | |
| 122 | (check_variant(Val, Vali) -> | |
| 123 | true | |
| 124 | ; | |
| 125 | log(error,'implementation of spec ~w binds variables but should not~n', [Predicate]) | |
| 126 | ) | |
| 127 | ; | |
| 128 | Res = fail(spec_not_matched(spec(Spec), value(Val))) | |
| 129 | ). | |
| 130 | %spec was an alias for another spec | |
| 131 | evaluate_spec_match_case(Spec, Type, Val, Res) :- | |
| 132 | spec_indirection(Spec, NewSpec), | |
| 133 | evaluate_spec_match(NewSpec, Type, Val, Res). | |
| 134 | ||
| 135 | ||
| 136 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
| 137 | :- if(environ(prob_safe_mode,false)). | |
| 138 | % checks disabled | |
| 139 | prepare_check_variant(_,nocheck). | |
| 140 | check_variant(_,_). | |
| 141 | :-else. | |
| 142 | prepare_check_variant(Val,Vars) :- term_variables(Val, Vars). | |
| 143 | check_variant(_,Vars) :- is_vars(Vars). % check if we have instantiated any variable | |
| 144 | is_vars([]). | |
| 145 | is_vars([H|T]) :- var(H), is_vars(T). | |
| 146 | % Note: the original implementation was using copy_term | |
| 147 | % in SICStus copy_term discards co-routines and variant does not examine co-routines or attributes | |
| 148 | % for SWI copy_term copies co-routines and variant does examine them | |
| 149 | % for some reason this check was added in b7cb63b041fd25e91aa082e15e6450666b627035 | |
| 150 | % to allow plspec to attach co-routines to Val without raising the above error message | |
| 151 | % however, it does not seem to work with 7.2.2 | |
| 152 | :- endif. | |
| 153 | ||
| 154 | % built-in recursive specs | |
| 155 | list(Spec, Val, NewSpecs, NewVals) :- | |
| 156 | nonvar(Val), list1(Val, Spec, NewSpecs, NewVals). | |
| 157 | %% list1 only ensures that the value is a list. | |
| 158 | %% The type of its members is checked later on in a seperate step. | |
| 159 | %% list1 will return a spec for each member. | |
| 160 | %% If a tail is a variable, the bound value should be | |
| 161 | %% of the same type as the list itself. | |
| 162 | list1(L, Spec, [Spec|ST], [H|VT]) :- | |
| 163 | nonvar(L), L = [H|T], !, | |
| 164 | list1(T, Spec, ST, VT). | |
| 165 | list1(L, _, [], []) :- | |
| 166 | nonvar(L), L = [], !. | |
| 167 | list1(Var, Spec, [list(Spec)], [Var]) :- var(Var). | |
| 168 | ||
| 169 | ||
| 170 | compound(Spec, Val, NewSpecs, NewVars) :- | |
| 171 | compound(Val), | |
| 172 | Val =.. [Functor|NewVars], | |
| 173 | Functor \= '[|]', | |
| 174 | length(NewVars, Len), | |
| 175 | length(NewSpecs, Len), | |
| 176 | Spec =.. [Functor|NewSpecs]. | |
| 177 | ||
| 178 | ||
| 179 | tuple(SpecList, VarList, SpecList, VarList) :- | |
| 180 | is_list(VarList). | |
| 181 | ||
| 182 | spec_and(SpecList, Var, SpecList, VarRepeated) :- | |
| 183 | SpecList \= [], | |
| 184 | %% this is actually repeat | |
| 185 | length(SpecList,L), | |
| 186 | length(VarRepeated,L), | |
| 187 | maplist(=(Var), VarRepeated). | |
| 188 | ||
| 189 | ||
| 190 | and([], _, [], true). | |
| 191 | and([S|Specs], Type, [V|Vals], Res) :- | |
| 192 | evaluate_spec_match(S, Type, V, X), | |
| 193 | (X == true -> | |
| 194 | and(Specs, Type, Vals, Res) | |
| 195 | ; | |
| 196 | Res = fail(spec_not_matched(spec(S), value(V))) | |
| 197 | ). | |
| 198 | ||
| 199 | ||
| 200 | or(Specs, Type, Vals, true) :- | |
| 201 | or2(Specs, Type, Vals). | |
| 202 | or(Specs, _, Vals, fail(spec_not_matched_merge(specs(or(Specs)), values(Vals)))). | |
| 203 | ||
| 204 | or2([HSpec|TSpec], Type, [HVal|TVal]) :- | |
| 205 | evaluate_spec_match(HSpec, Type, HVal, X), | |
| 206 | (X == true -> | |
| 207 | true | |
| 208 | ; | |
| 209 | or2(TSpec, Type, TVal) | |
| 210 | ). |