+++ /dev/null
-% Efforts toward literate tests with quads
-
-:- use_module(library(iso_ext)).
-:- use_module(library(pio)).
-:- use_module(library(lists)).
-:- use_module(library(dcgs)).
-:- use_module(library(format)).
-:- use_module(library(reif)).
-:- use_module(library(debug)).
-:- use_module(library(lambda)).
-:- use_module(library(error)).
-:- use_module(library(time)).
-
-:- use_module(testutils).
-:- use_module(special_functions).
-
-portray_term(Stream) :-
- read_term(Stream, Term, []),
- portray_clause(Term).
-
-?- check_module_quads(special_functions, _).
-% Checking 11 quads ..
-% CHECKING.. (?-A=0.6174468790806071,erf(A,A),B is-A,erf(B,B)).
-% CHECKING.. (?-try_falsify(odd_t(erf,real(A)))).
-% CHECKING.. (?-witness(odd_t(erf,real(A),false))).
-% CHECKING.. (?-witness((real(A),erf(A,B),erf(-A,C),abs(B+C)>0))).
-% CHECKING.. (?-length(A,B)).
-% CHECKING.. (?-real(A),erf(A,B),erfc(A,C),abs(B+C-1)>epsilon).
-% CHECKING.. (?-try_falsify(δ_inverses_t(40*epsilon,erf,inverf,interval(-2,2,A)))).
-% CHECKING.. (?-try_falsify(δ_inverses_t(40*epsilon,erfc,inverfc,interval(-2,2,A)))).
-% CHECKING.. (?-A=10,B is A+1,gamma(B,C),int_realfact(A,D)).
-% CHECKING.. (?-gamma_P_Q(1.2,2.3,A,B),abs(A+B-1)<epsilon).
-% CHECKING.. (?-A=1.5,B=0.7,invgammp(A,B,C),gamma_P_Q(A,C,D,E),abs(B-D)<epsilon).
- true.
-
-check_module_quads(Module, Quads) :-
- use_module(Module),
- read_quads(Module, Quads),
- zip(Qs, ADs, Quads),
- length(Qs, NQ),
- format("% Checking ~d quads ..~n", [NQ]),
- maplist(check_qu_ad, Qs, ADs).
-
-read_quads(Module, Quads) :-
- module_terms(Module, Terms),
- terms_quads(Terms, Quads).
-
-module_terms(Module, Terms) :-
- module_file(Module, File),
- setup_call_cleanup(
- open(File, read, Stream, [type(text)]),
- read_terms(Stream, Terms),
- close(Stream)
- ).
-
-module_file(Module, File) :- atom_concat(Module, '.pl', File).
-
-% Given a list of terms, filter out the predicate clauses.
-% TODO: Arg 1 is really a list of Term-VarNames _pairs_;
-% it would be very nice to find a less unsightly
-% name than 'TermVN' for these!
-terms_quads([Term|Terms], Quads) :-
- ( term_type(Term, clause) -> terms_quads(Terms, Quads)
- ; Quads = [Term|Quads_],
- terms_quads(Terms, Quads_)
- ).
-terms_quads([], []).
-
-term_type(Term-_, Type) :-
- ( Term = (?- _) -> Type = query
- ; Term = (_,_) -> Type = answer_description
- ; Term = (_;_) -> Type = answer_description
- ; Term == true -> Type = answer_description
- ; Term == false -> Type = answer_description
- ; Type = clause
- ).
-
-?- term_type(test("erf is odd",try_falsify(odd_t(erf,real(_L))))-_, Type).
- Type = clause.
-
-read_terms(Stream, Terms) :-
- read_terms_(Stream, [], Terms).
-read_terms_(Stream, Terms0, Terms) :-
- Options = [variable_names(VarNames)],
- read_term(Stream, Term, Options),
- ( Term = end_of_file -> reverse(Terms0, Terms)
- ; read_terms_(Stream, [Term-VarNames|Terms0], Terms)
- ).
-
-%% zip(+Xs, +Ys, ?XYs)
-%% zip(?Xs, ?Ys, +XYs)
-%
-% List XYs interleaves same-length lists Xs and Ys.
-zip([X|Xs], [Y|Ys], [X,Y|XYs]) :-
- zip(Xs, Ys, XYs).
-zip([], [], []).
-
-?- zip(Xs, Ys, XYs). % MGQ does not terminate
- error('$interrupt_thrown',repl/0).
-
-% The following suggested by Ulrich via Quad Works chat
-?- zip(Xs, Ys, XYs), false. % loops
-
-?- zip(X, [4,5,6], [1,4,2,5,3,6]).
- X = [1,2,3].
-
-?- zip([1,2,3], Y, [1,4,2,5,3,6]).
- Y = [4,5,6].
-
-?- zip([1,2,3], [4,5,6], Z).
- Z = [1,4,2,5,3,6].
-
-?- zip(Xs, Ys, [1,4,2,5,3,6]).
- Xs = [1,2,3], Ys = [4,5,6].
-
-% 3. Demonstrate checking 1 quad, the top two elements of a QAs list.
-check_qu_ad(Q-QVN, A-AVN) :-
- Q = ?-(G),
- phrase(portray_clause_(Q), LitQ), % NB: LitQ terminates w/ newline
- format("% CHECKING.. ",[]),
- ( A == true -> call(G)
- ; A == false -> ( call(G) -> false
- ; true
- )
- ; phrase(unconj(A), As) ->
- ( length(As, N),
- n_answers(N, A, AVN, ADs),
- n_answers(N, G, QVN, Answers),
- maplist(contains, ADs, Answers)
- )
- ; % Otherwise, we have the ',' case of a solitary answer
- call(G),
- call(A),
- QVN == AVN
- ),
- format("~s", [LitQ]).
-
-% Answer-description AD (qua set-of-bindings) contains Answer.
-contains(AD, Answer) :- append(Answer, _, AD).
-
-?- contains(['Xs'=[C],'L'=1,'_A'=C,'_B'=D], ['Xs'=[A],'L'=1]).
- C = A.
-
-?- check_qu_ad((?-length(_F,_G))-['Xs'=_F,'L'=_G],(_H=[],_I=0;_H=[_J],_I=1;_H=[_J,_K],_I=2;...)-['Xs'=_H,'L'=_I,'_A'=_J,'_B'=_K]).
-% CHECKING.. (?-length(A,B)).
- _F = [_A,_B], _G = 2, _H = [_J,_K], _I = 2.
-
-% Unravel the nested (;)/1 applications of multiple-AD structures.
-unconj(Conj) --> { Conj = (Elt;Conj_) },
- [Elt],
- unconj(Conj_).
-unconj(...) --> [].
-
-?- phrase(unconj((_H=[],_I=0;_H=[_J],_I=1;_H=[_J,_K],_I=2;...)), List).
- List = [(_H=[],_I=0),(_H=[_J],_I=1),(_H=[_J,_K],_I=2)].
-
-empty_anstack :-
- ( retract('$anstack'(_)), fail
- ; asserta('$anstack'([]))
- ).
-
-push(VN) :-
- retract('$anstack'(As)),
- asserta('$anstack'([VN|As])).
-
-backtrack(N) :-
- ( '$anstack'(Ans),
- length(Ans, N) -> true
- ; fail
- ).
-
-n_answers(N, G, VN, ADs) :-
- must_be(integer, N),
- ( N > 0 -> n_answers_(N, G, VN, ADs)
- ; domain_error(not_less_than_zero, N, n_answers/4)
- ).
-
-n_answers_(N, G, VN, ADs) :-
- empty_anstack,
- call(G), push(VN),
- backtrack(N),
- !,
- retract('$anstack'(As)),
- reverse(As, ADs).
-
-?- n_answers(3, length(Xs, L), ('Xs'=Xs,'Len'=L), ADs).
- Xs = [_A,_B], L = 2, ADs = [('Xs'=[],'Len'=0),('Xs'=[_C],'Len'=1),('Xs'=[_D,_E],'Len'=2)].
projects / scryer-prolog.git / commitdiff