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