1 | :- module(plspec_core, | |
2 | %plspec predicates | |
3 | [enable_all_spec_checks/0, | |
4 | enable_spec_check/1, | |
5 | spec_pre/2, spec_post/3, spec_invariant/2, | |
6 | defspec/2, defspec_pred/2, | |
7 | defspec_pred_recursive/4, defspec_connective/4, | |
8 | %validator predicates: | |
9 | valid/2, | |
10 | %logger | |
11 | set_loglevel/1, log/3, | |
12 | %multifile: | |
13 | asserted_spec_pre/5, asserted_spec_invariant/3, | |
14 | asserted_spec_invariant/4, asserted_spec_post/7, | |
15 | check_predicate/1, | |
16 | ||
17 | set_error_handler/1 | |
18 | ]). | |
19 | :- use_module(plspec). | |
20 | :- use_module(validator). | |
21 | :- use_module(plspec_logger). | |
22 | ||
23 | expansion(Head, Body, PreSpecs, PreSpecTypes, | |
24 | InvariantSpecOrEmpty, InvSpecTypes, | |
25 | PrePostSpecs,PrePostSpecTypes, PostSpecs, PostSpecTypes, | |
26 | NewHead, NewBody) :- | |
27 | Head =.. [Functor|Args], | |
28 | length(Args, Lenny), | |
29 | %% newargs: only relevant if head implements pattern matching: | |
30 | % consider foo(foo). then the call 'foo(bar)' would not violate the spec but only fail | |
31 | % thus, we insert a fresh variable and check the unification with the argument term later on | |
32 | length(NewArgs, Lenny), | |
33 | NewHead =.. [Functor|NewArgs], | |
34 | NewBody = (% determine if at least one precondition is fulfilled | |
35 | (PreSpecs = [] -> | |
36 | true | |
37 | ; | |
38 | (plspec:plspec_some( | |
39 | spec_matches(NewArgs, true), | |
40 | PreSpecs, | |
41 | PreSpecTypes | |
42 | ) -> | |
43 | true | |
44 | ; | |
45 | plspec:error_not_matching_any_pre( | |
46 | Functor/Lenny, | |
47 | NewArgs, | |
48 | PreSpecs | |
49 | ) | |
50 | ) | |
51 | ), | |
52 | (InvariantSpecOrEmpty = [InvariantSpec] -> | |
53 | InvSpecTypes = [InvSpecType], | |
54 | lists:maplist( | |
55 | plspec:setup_uber_check(Functor/Lenny,InvSpecType), | |
56 | InvariantSpec, | |
57 | NewArgs | |
58 | ) | |
59 | ; | |
60 | true | |
61 | ), | |
62 | % gather all matching postconditions | |
63 | plspec:which_posts( | |
64 | PrePostSpecs, | |
65 | PrePostSpecTypes, | |
66 | PostSpecs, | |
67 | PostSpecTypes, | |
68 | Args, | |
69 | ValidPrePostSpecs, | |
70 | PostsToCheck, | |
71 | PostTypesToCheck), | |
72 | %% log(debug, 'These pre-post specs matched: ~w', [PrePostSpecs]), | |
73 | % unify with pattern matching of head | |
74 | NewArgs = Args, | |
75 | %% log(debug, 'Unified the arguments with ~w', [Args]), | |
76 | Body, | |
77 | lists:maplist( | |
78 | plspec:check_posts(Args), | |
79 | ValidPrePostSpecs, | |
80 | PostsToCheck, | |
81 | PostTypesToCheck | |
82 | ) | |
83 | ). | |
84 | ||
85 | :- load_files(library(system), [when(compile_time), imports([environ/2])]). | |
86 | :- if(environ(disable_plspec_runtime_checks, true)). | |
87 | should_expand(_A, _Module, _F, _Arity) :- fail. | |
88 | :- else. | |
89 | should_expand(A, Module, F, Arity) :- | |
90 | plspec:check_predicate(A), % check if the predicate is marked for expansion | |
91 | % true if enable_spec_check is executed | |
92 | functor(A,F,Arity), | |
93 | ( | |
94 | % TO DO: indexing occurs on :/2 !!!! | |
95 | plspec:asserted_spec_pre(F,Arity,Module, _, _) -> true | |
96 | ; plspec:asserted_spec_invariant(Module:F/Arity, _, _) -> true | |
97 | ; plspec:asserted_spec_post(F,Arity,Module, _, _, _, _) -> true | |
98 | ). | |
99 | :- endif. | |
100 | ||
101 | expandeur(':-'(A, B), Module, ':-'(NA, NB)) :- | |
102 | should_expand(A, Module, F, Arity), !, | |
103 | log(debug,'expansion of clause of ~w',[A]), | |
104 | findall( | |
105 | PreSpec, | |
106 | plspec:asserted_spec_pre(F,Arity,Module,PreSpec, _),PreSpecs), | |
107 | findall( | |
108 | InvSpec, | |
109 | plspec:asserted_spec_invariant(Module:F/Arity,InvSpec, _), | |
110 | InvariantSpecOrEmpty), | |
111 | findall( | |
112 | PreSpec2, | |
113 | plspec:asserted_spec_post(F,Arity,Module,PreSpec2,_,_,_),PrePostSpecs), | |
114 | findall( | |
115 | PostSpec, | |
116 | plspec:asserted_spec_post(F,Arity,Module,_,PostSpec,_,_),PostSpecs), | |
117 | findall( | |
118 | PreSpecType, | |
119 | plspec:asserted_spec_pre(F,Arity,Module,PreSpec, PreSpecType), | |
120 | PreSpecTypes), | |
121 | findall( | |
122 | InvSpecType, | |
123 | plspec:asserted_spec_invariant(Module:F/Arity,InvSpec, InvSpecType), | |
124 | InvSpecTypes), | |
125 | findall( | |
126 | PreSpec2Type, | |
127 | plspec:asserted_spec_post(F,Arity,Module,PreSpec2,_,PreSpec2Type,_), | |
128 | PrePostSpecTypes), | |
129 | findall( | |
130 | PostSpecType, | |
131 | plspec:asserted_spec_post(F,Arity,Module,_,PostSpec,_,PostSpecType), | |
132 | PostSpecTypes), | |
133 | expansion( | |
134 | A, | |
135 | B, | |
136 | PreSpecs, | |
137 | PreSpecTypes, | |
138 | InvariantSpecOrEmpty, | |
139 | InvSpecTypes, | |
140 | PrePostSpecs, | |
141 | PrePostSpecTypes, | |
142 | PostSpecs, | |
143 | PostSpecTypes, | |
144 | NA, | |
145 | NB | |
146 | ). | |
147 | ||
148 | do_expand( | |
149 | ':-'(spec_pre(Predicate/Arity, Spec)), | |
150 | Module, | |
151 | ':-'(spec_pre(Module:Predicate/Arity, Spec))). | |
152 | do_expand( | |
153 | ':-'(spec_invariant(Predicate/Arity, Spec)), | |
154 | Module, | |
155 | ':-'(spec_invariant(Module:Predicate/Arity, Spec))). | |
156 | do_expand( | |
157 | ':-'(spec_post(Predicate/Arity, SpecPre, SpecPost)), | |
158 | Module, | |
159 | ':-'(spec_post(Module:Predicate/Arity, SpecPre, SpecPost))). | |
160 | do_expand( | |
161 | ':-'(plspec:spec_pre(Predicate/Arity, Spec)), | |
162 | Module, | |
163 | ':-'(plspec:spec_pre(Module:Predicate/Arity, Spec))). | |
164 | do_expand( | |
165 | ':-'(plspec:spec_invariant(Predicate/Arity, Spec)), | |
166 | Module, | |
167 | ':-'(plspec:spec_invariant(Module:Predicate/Arity, Spec))). | |
168 | do_expand( | |
169 | ':-'(plspec:spec_post(Predicate/Arity, SpecPre, SpecPost)), | |
170 | Module, | |
171 | ':-'(plspec:spec_post(Module:Predicate/Arity, SpecPre, SpecPost))). | |
172 | do_expand(':-'(A, B), Module, ':-'(NA, NB)) :- !, | |
173 | %log(debug,'do_expand of ~w',[A]), | |
174 | expandeur(':-'(A, B), Module, ':-'(NA, NB)). | |
175 | do_expand(A, Module, ':-'(NA, NB)) :- | |
176 | %log(debug,'do_expand of ~w',[A]), | |
177 | expandeur(':-'(A, true), Module, ':-'(NA, NB)). | |
178 | do_expand(A, _Module, A). | |
179 | ||
180 | :- multifile user:term_expansion/2. | |
181 | user:term_expansion(A, B) :- | |
182 | log(debug,'term-expansion SWI of ~w', [A]), | |
183 | prolog_load_context(module, Module), | |
184 | do_expand(A, Module, B). | |
185 | ||
186 | :- multifile user:term_expansion/6. | |
187 | user:term_expansion(Term1, Layout1, Ids, Term2, Layout1, [plspec_token|Ids]) :- | |
188 | %log(debug,'term-expansion SICTUS of ~w', [Term1]), | |
189 | nonmember(plspec_token, Ids), | |
190 | prolog_load_context(module, Module), | |
191 | ? | do_expand(Term1, Module, Term2). |