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/3, asserted_spec_invariant/3,
14 asserted_spec_invariant/4, asserted_spec_post/5,
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
86 should_expand(A, F, Module, Arity) :-
87 functor(A,F,Arity),
88 (
89 ? plspec:asserted_spec_pre(Module:F/Arity, _, _)
90 ;
91 plspec:asserted_spec_invariant(Module:F/Arity, _, _)
92 ;
93 plspec:asserted_spec_post(Module:F/Arity, _, _, _, _)
94 ),
95 !,
96 plspec:check_predicate(F/Arity).
97
98 expandeur(':-'(A, B), Module, ':-'(NA, NB)) :-
99 should_expand(A, F, Module, Arity), !,
100 findall(
101 PreSpec,
102 plspec:asserted_spec_pre(Module:F/Arity,PreSpec, _),PreSpecs),
103 findall(
104 InvSpec,
105 plspec:asserted_spec_invariant(Module:F/Arity,InvSpec, _),
106 InvariantSpecOrEmpty),
107 findall(
108 PreSpec2,
109 plspec:asserted_spec_post(Module:F/Arity,PreSpec2,_,_,_),PrePostSpecs),
110 findall(
111 PostSpec,
112 plspec:asserted_spec_post(Module:F/Arity,_,PostSpec,_,_),PostSpecs),
113 findall(
114 PreSpecType,
115 plspec:asserted_spec_pre(Module:F/Arity,PreSpec, PreSpecType),
116 PreSpecTypes),
117 findall(
118 InvSpecType,
119 plspec:asserted_spec_invariant(Module:F/Arity,InvSpec, InvSpecType),
120 InvSpecTypes),
121 findall(
122 PreSpec2Type,
123 plspec:asserted_spec_post(Module:F/Arity,PreSpec2,_,PreSpec2Type,_),
124 PrePostSpecTypes),
125 findall(
126 PostSpecType,
127 plspec:asserted_spec_post(Module:F/Arity,_,PostSpec,_,PostSpecType),
128 PostSpecTypes),
129 expansion(
130 A,
131 B,
132 PreSpecs,
133 PreSpecTypes,
134 InvariantSpecOrEmpty,
135 InvSpecTypes,
136 PrePostSpecs,
137 PrePostSpecTypes,
138 PostSpecs,
139 PostSpecTypes,
140 NA,
141 NB
142 ).
143
144 do_expand(
145 ':-'(spec_pre(Predicate/Arity, Spec)),
146 Module,
147 ':-'(spec_pre(Module:Predicate/Arity, Spec))).
148 do_expand(
149 ':-'(spec_invariant(Predicate/Arity, Spec)),
150 Module,
151 ':-'(spec_invariant(Module:Predicate/Arity, Spec))).
152 do_expand(
153 ':-'(spec_post(Predicate/Arity, SpecPre, SpecPost)),
154 Module,
155 ':-'(spec_post(Module:Predicate/Arity, SpecPre, SpecPost))).
156 do_expand(
157 ':-'(plspec:spec_pre(Predicate/Arity, Spec)),
158 Module,
159 ':-'(plspec:spec_pre(Module:Predicate/Arity, Spec))).
160 do_expand(
161 ':-'(plspec:spec_invariant(Predicate/Arity, Spec)),
162 Module,
163 ':-'(plspec:spec_invariant(Module:Predicate/Arity, Spec))).
164 do_expand(
165 ':-'(plspec:spec_post(Predicate/Arity, SpecPre, SpecPost)),
166 Module,
167 ':-'(plspec:spec_post(Module:Predicate/Arity, SpecPre, SpecPost))).
168 do_expand(':-'(A, B), Module, ':-'(NA, NB)) :- !,
169 log(debug,'do_expand of ~w',[A]),
170 expandeur(':-'(A, B), Module, ':-'(NA, NB)).
171 do_expand(A, Module, ':-'(NA, NB)) :-
172 log(debug,'do_expand of ~w',[A]),
173 expandeur(':-'(A, true), Module, ':-'(NA, NB)).
174 do_expand(A, _Module, A).
175
176 :- multifile term_expansion/2.
177 user:term_expansion(A, B) :-
178 log(debug,'term-expansion SWI of ~w', [A]),
179 prolog_load_context(module, Module),
180 do_expand(A, Module, B).
181
182 :- multifile user:term_expansion/6.
183 user:term_expansion(Term1, Layout1, Ids, Term2, Layout1, [plspec_token|Ids]) :-
184 log(debug,'term-expansion SICTUS of ~w', [Term1]),
185 nonmember(plspec_token, Ids),
186 prolog_load_context(module, Module),
187 ? do_expand(Term1, Module, Term2).