plspec

and_invariant(Specs, Vals, Location, R) :-
    (ground(Specs) ->
    and_invariant(Specs, Vals, Location, R, def)
    ;
    and_invariant(Specs, Vals, Location, R, any)
).

and_invariant([], [], _, true, _).

and_invariant([HSpec|TSpec], [HVal|TVal], Location, R, Type) :-
    setup_check(Location, ResElement,HSpec, HVal, Type),
    freeze(TVal, and_invariant(TSpec, TVal, Location, ResTail, Type)), % TODO: do we need this freeze?
    both_eventually_true(ResElement, ResTail, R).

asserted_spec_invariant(Pred, Spec) :-
    asserted_spec_invariant(Pred, _, Spec).

both_eventually_true(V1, V2, Res) :-
    when((nonvar(V1); nonvar(V2)),
    (V1 == true
    -> freeze(V2, Res = V2) %% look at the other co-routined variable
    ; nonvar(V1)
    -> Res = V1 %% since it is not true
    ; V2 == true
    -> freeze(V1, Res = V1)
    ; nonvar(V2) -> Res = V2)).

check_arity(_Pred, Spec, _SpecType, Arity) :-
    length(Spec, Arity).

check_arity(Pred, Spec, SpecType, Arity) :-
    \+ length(Spec, Arity),
    log(error,'~w of ~w does not match in length!',[SpecType, Pred]),
    fail.

check_ground(_Pred, Spec, _SpecType) :-
    ground(Spec).

check_ground(Pred, Spec, SpecType) :-
    \+ ground(Spec),
    log(info,'~w is not ground; got ~w in ~w. It is handled as a specific, but unknown spec.', [SpecType, Spec, Pred]).

check_posts([], [], [], _).

check_posts([Arg|ArgT], [Pre|PreT], [Post|PostT], PostType) :-
    evaluate_spec_match(Post, PostType, Arg, Res),!,
    (Res == true ->
    check_posts(ArgT, PreT, PostT, PostType)
    ;
    error_handler(X),
    call(
    X,
    fail(
    postcondition_violated(
    matched_pre(Pre),
    violated_post(Post),
    value(Arg)
)
)
)
).

defspec(SpecId, OtherSpec) :-
    (spec_exists(SpecId, Existing) ->
    %% we use variant in order to determine whether it is actually the same spec;
    % for example, consider defspec(foo(X,Y), bar(X,Y)), defspec(foo(X,Y), bar(Y,X)).
    % we do not want to unify X = Y but also notice these are not the same specs.
    log_spec_already_exists(SpecId, Existing, indirection(OtherSpec))
    ;
    assertz(spec_indirection(SpecId, OtherSpec)),
    log(info,'Spec ~w defined.',[SpecId])).

defspec_connective(SpecId, Predicate, MergePred, MergePredInvariant) :-
    (spec_exists(SpecId, Existing) ->
    log_spec_already_exists(
    SpecId,
    Existing,
    connective(Predicate, MergePred, MergePredInvariant)
    )
    ;
    assertz(
    spec_connective(
    SpecId,
    Predicate,
    MergePred,
    MergePredInvariant
    )
    ),
    log(info,'Connective spec ~w defined.')
).

defspec_pred(SpecId, Predicate) :-
    (spec_exists(SpecId, Existing) ->
    log_spec_already_exists(SpecId, Existing, predicate(Predicate))
    ;
    assertz(spec_predicate(SpecId, Predicate))).

defspec_pred_recursive(SpecId, Predicate, MergePred, MergePredInvariant) :-
    (spec_exists(SpecId, Existing) ->
    log_spec_already_exists(
    SpecId,
    Existing,
    predicate_recursive(Predicate, MergePred, MergePredInvariant)
    )
    ;
    assertz(
    spec_predicate_recursive(
    SpecId,
    Predicate,
    MergePred,
    MergePredInvariant)
    ),
    log(info, 'Recursive spec ~w defined.',[SpecId])
).

enable_all_spec_checks :-
    retractall(check_predicate(_)),
    assertz(check_predicate(_)).

enable_spec_check([H|T]) :- !,
    maplist(enable_spec_check, [H|T]).

enable_spec_check(F/N) :-
    log(info, 'Spec check enabled for ~w/~w.',[F/N]),
    functor(X,F,N),
    assertz(check_predicate(X)).

enable_spec_check(X) :-
    log(error, 'Spec check cannot be enabled for ~w use Functor/Arity syntax!',[X]).

error_handler(plspec_default_error_handler).

error_not_matching_any_pre(Functor, Args, PreSpecs) :-
    error_handler(X),
    call(
    X,
    fail(
    prespec_violated(specs(PreSpecs), values(Args), location(Functor))
)
).

log_spec_already_exists(SpecId, ExistingDefinition, NewDefinition) :-
    (variant(spec(SpecId,ExistingDefinition),spec(SpecId,NewDefinition)) ->
    log(info,'spec is overwritten with itself, proceeding~n', [SpecId])
    ;
    log(warning,'spec ~w already exists, will not be redefined~n', [SpecId])).

named_spec(Name:Spec, Name, Spec).

or_invariant(NewSpecs, NewVals, Location, FutureRes) :-
    or_invariant(NewSpecs, NewVals, [], NewVals, or(NewSpecs), Location, FutureRes).

or_invariant([], [], Acc, OrigVals, OrigPattern, Location, UberVar) :-
    freeze(
    Acc,
    (Acc == fail ->
    (reason(OrigPattern, Location, OrigVals, Reason), UberVar = Reason)
    ;
    true
)
).

or_invariant([H|T], [V|VT], Prior, OrigVals, OrigPattern, Location, UberVar) :-
    setup_check(Location, ResOption, H, V),
    freeze(
    ResOption,
    (ResOption == true ->
    (UberVar = true, Current = true)
    ;
    freeze(
    Prior,
    (Prior == true -> true; Current = fail)
    )
    )
    ),
    or_invariant(T, VT, Current, OrigVals, OrigPattern, Location, UberVar).

plspec_default_error_handler(X) :-
    pretty_print_error(X), !,
    throw(plspec_error).

plspec_some(Goal, List, List2) :-
    plspec_some1(List, List2, Goal).

plspec_some1([],[], _) :- fail.

plspec_some1([H|_], [G|_], Goal) :-
    call(Goal,H,G),
    log(debug, 'Pre-Spec ~w matched!',[H]),
    !.

plspec_some1([_|T], [_|S], Goal) :-
    plspec_some1(T, S, Goal).

reason(T, Location, V, Reason) :-
    copy_term(Location, LocationWithoutAttributes, _Goals),
    Reason =
    fail(
    spec_violated(
    spec(T),
    value(V),
    location(LocationWithoutAttributes)
)
).

set_error_handler(Pred) :-
    retractall(error_handler(_)),
    assertz(error_handler(Pred)).

setup_check(Location,Res,Spec,Val,Type) :-
    setup_check_aux(Spec,Location,Val,Res,Type).

setup_check_aux(Spec, Location, Val, Res, def) :-
    spec_basic(Spec, Pred), !,
    freeze(Val, (call(Pred, Val) -> true ; reason(Spec, Location, Val, Res))).

setup_check_aux(Spec, Location, Val, Res, _) :-
    spec_predicate(Spec, Pred), !,
    freeze(Val, (call(Pred, Val) -> true ; reason(Spec, Location, Val, Res))).

setup_check_aux(Spec, Location, Val, Res, Type) :-
    spec_indirection(Spec, OtherSpec), !,
    setup_check_aux(OtherSpec, Location, Val, Res, Type).

setup_check_aux(Spec, Location, Val, Res, _Type) :-
    spec_predicate_recursive(Spec, Pred, _MergePred, MergePredInvariant),
    !,
    freeze(
    Val,
    (call(Pred, Val, NewSpecs, NewVals) ->
    call(MergePredInvariant, NewSpecs, NewVals, Location, Res)
    ;
    reason(Spec, Location, Val, Res)
)
).

setup_check_aux(Spec, Location, Val, Res, _Type) :-
    spec_connective(Spec, Pred, _MergePred, MergePredInvariant), !,
    freeze(
    Val,
    (call(Pred, Val, NewSpecs, NewVals) ->
    call(MergePredInvariant, NewSpecs, NewVals, Location, Res)
    ;
    reason(Spec, Location, Val, Res)
)
).

setup_check_aux(
    Spec,
    Location,
    _,
    fail(spec_not_found(spec(Spec), location(Location))),_).

setup_uber_check(Location,any,Spec,Val) :-
    log(debug,'setup_uber_check'),
    setup_check(Location,Res,Spec,Val,any),
    freeze(Res, ((Res == true) -> true ; error_handler(X), call(X, Res))).

setup_uber_check(Location,def,Spec,Val) :-
    log(debug,'setup_uber_check'),
    setup_check(Location,Res,Spec,Val,def),
    freeze(Res, ((Res == true) -> true ; error_handler(X), call(X, Res))).

spec_invariant(Pred, InvariantSpec) :-
    check_ground(Pred, InvariantSpec, 'invariant specs'),
    Pred = _:_/Arity,
    check_arity(Pred, InvariantSpec, 'An invariant spec', Arity),
    (ground(InvariantSpec) ->
    (maplist(plspec:named_spec, InvariantSpec, Names, Specs) ->
    assertz(asserted_spec_invariant(Pred, Names, Specs, def))
    ;
    assertz(asserted_spec_invariant(Pred, InvariantSpec, def)))
    ;
    (maplist(plspec:named_spec, InvariantSpec, Names, Specs) ->
    assertz(asserted_spec_invariant(Pred, Names, Specs, any))
    ;
    assertz(asserted_spec_invariant(Pred, InvariantSpec, any)))),
    log(debug,'Assertedc spec invariant for ~w.',[Pred]).

spec_matches([], true, [], _).

spec_matches([Arg|ArgsT], Res, [Spec|SpecT], Type) :-
    evaluate_spec_match(Spec, Type, Arg, R),
    (R == true ->
    spec_matches(ArgsT, Res, SpecT, Type)
    ;
    Res = spec_not_matched(Spec, Arg, in(R))).

spec_post(Pred,PreSpec,PostSpec) :-
    check_ground(Pred, PreSpec, 'post-specs'),
    check_ground(Pred, PostSpec, 'post-specs'),
    Pred = Module:F/Arity,
    check_arity(Pred, PreSpec, 'A post spec (precondition)', Arity),
    check_arity(Pred, PostSpec, 'A post spec (postcondition)', Arity),
    (ground(PreSpec) ->
    (ground(PostSpec) ->
    assertz(asserted_spec_post(F,Arity,Module,PreSpec,PostSpec,def,def))
    ;
    assertz(asserted_spec_post(F,Arity,Module,PreSpec,PostSpec,def,any)))
    ;
    (ground(PostSpec) ->
    assertz(asserted_spec_post(F,Arity,Module,PreSpec,PostSpec,any,def))
    ;
    assertz(asserted_spec_post(F,Arity,Module,PreSpec,PostSpec,any,any)))),
    log(debug,'Asserted spec post for ~w.',[Pred]).

spec_pre(Pred,PreSpec) :-
    check_ground(Pred, PreSpec, 'pre specs'),
    Pred = Module:Functor/Arity,
    check_arity(Pred, PreSpec, 'A pre spec', Arity),
    (ground(PreSpec) ->
    assertz(asserted_spec_pre(Functor,Arity,Module,PreSpec,def))
    ;
    assertz(asserted_spec_pre(Functor,Arity,Module,PreSpec,any))),
    log(debug,'Asserted spec pre for ~w.',[Pred]).

which_posts([],[],[],[],_,[],[],[]) :- !.

which_posts([Pre|PresBefore], [PreType|PreTypes],
    [Post|Posts], [PostType|PostTypes], Args,
    [Pre|PresAfter], [Post|PostAfter], [PostType|PostTypesAfter]) :-
    maplist(valid(PreType),Pre,Args),!,
    which_posts(
    PresBefore,
    PreTypes,
    Posts,
    PostTypes,
    Args,
    PresAfter,
    PostAfter,
    PostTypesAfter).

which_posts([_|Pres],[_|PreTypes],[_|Posts],[_|PostTypes],Args,PreT,T,Z) :-
    which_posts(Pres,PreTypes,Posts,PostTypes,Args,PreT,T,Z).