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).