1 | :- module(plspec_checker, []). | |
2 | :- use_module(plspec). | |
3 | ||
4 | expansion(Head,Goal,PreSpecs,InvariantSpecOrEmpty,PrePostSpecs,PostSpecs,NewHead,NewBody) :- | |
5 | Head =.. [Functor|Args], | |
6 | length(Args, Lenny), | |
7 | %% newargs: only relevant if head implements pattern matching: | |
8 | % consider foo(foo). then the call 'foo(bar)' would not violate the spec but only fail | |
9 | % thus, we insert a fresh variable and check the unification with the argument term later on | |
10 | length(NewArgs, Lenny), | |
11 | NewHead =.. [Functor|NewArgs], | |
12 | NewBody = (% determine if at least one precondition is fulfilled | |
13 | (PreSpecs = [] -> true ; (plspec:plspec_some(spec_matches(NewArgs, true), PreSpecs) -> true ; plspec:error_not_matching_any_pre(Functor/Lenny, NewArgs, PreSpecs))), | |
14 | (InvariantSpecOrEmpty = [InvariantSpec] -> lists:maplist(plspec:setup_uber_check(Functor/Lenny),InvariantSpec,Args) ; true), | |
15 | % unify with pattern matching of head | |
16 | NewArgs = Args, | |
17 | % gather all matching postconditions | |
18 | plspec:which_posts(PrePostSpecs,PostSpecs,Args,ValidPrePostSpecs,PostsToCheck), | |
19 | Goal, | |
20 | lists:maplist(plspec:check_posts(Args),ValidPrePostSpecs,PostsToCheck)). | |
21 | ||
22 | should_expand(A, F, Module, Arity) :- | |
23 | functor(A,F,Arity), | |
24 | %trace, | |
25 | ? | (plspec:le_spec_pre(Module:F/Arity, _) ; plspec:le_spec_invariant(Module:F/Arity, _) ; plspec:le_spec_post(Module:F/Arity, _, _)), !, |
26 | plspec:check_predicate(F/Arity). | |
27 | ||
28 | expandeur(':-'(A, B), Module, ':-'(NA, NB)) :- | |
29 | should_expand(A, F, Module, Arity), !, | |
30 | findall(PreSpec, plspec:le_spec_pre(Module:F/Arity,PreSpec), PreSpecs), | |
31 | findall(InvSpec, plspec:le_spec_invariant(Module:F/Arity,InvSpec),InvariantSpecOrEmpty), | |
32 | findall(PreSpec2,plspec:le_spec_post(Module:F/Arity,PreSpec2,_),PrePostSpecs), | |
33 | findall(PostSpec,plspec:le_spec_post(Module:F/Arity,_,PostSpec),PostSpecs), | |
34 | expansion(A,B,PreSpecs,InvariantSpecOrEmpty,PrePostSpecs,PostSpecs,NA,NB). | |
35 | ||
36 | do_expand(':-'(spec_pre(Predicate/Arity, Spec)), Module, ':-'(spec_pre(Module:Predicate/Arity, Spec))). | |
37 | do_expand(':-'(spec_invariant(Predicate/Arity, Spec)), Module, ':-'(spec_invariant(Module:Predicate/Arity, Spec))). | |
38 | do_expand(':-'(spec_post(Predicate/Arity, SpecPre, SpecPost)), Module, ':-'(spec_post(Module:Predicate/Arity, SpecPre, SpecPost))). | |
39 | do_expand(':-'(plspec:spec_pre(Predicate/Arity, Spec)), Module, ':-'(plspec:spec_pre(Module:Predicate/Arity, Spec))). | |
40 | do_expand(':-'(plspec:spec_invariant(Predicate/Arity, Spec)), Module, ':-'(plspec:spec_invariant(Module:Predicate/Arity, Spec))). | |
41 | do_expand(':-'(plspec:spec_post(Predicate/Arity, SpecPre, SpecPost)), Module, ':-'(plspec:spec_post(Module:Predicate/Arity, SpecPre, SpecPost))). | |
42 | do_expand(':-'(A, B), Module, ':-'(NA, NB)) :- | |
43 | expandeur(':-'(A, B), Module, ':-'(NA, NB)). | |
44 | do_expand(A, Module, ':-'(NA, NB)) :- | |
45 | expandeur(':-'(A, true), Module, ':-'(NA, NB)). | |
46 | do_expand(A, _Module, A). | |
47 | ||
48 | ||
49 | :- multifile term_expansion/2. | |
50 | user:term_expansion(A, B) :- | |
51 | prolog_load_context(module, Module), | |
52 | do_expand(A, Module, B). | |
53 | ||
54 | :- multifile user:term_expansion/6. | |
55 | user:term_expansion(Term1, Layout1, Ids, Term2, Layout1, [plspec_token|Ids]) :- | |
56 | nonmember(plspec_token, Ids), | |
57 | prolog_load_context(module, Module), | |
58 | ? | do_expand(Term1, Module, Term2). |