cgi.pl

    1:- module(cgi, []).    2:- use_module(pac(op)).    3:- use_module(pac(basic)).    4:- use_module(util(misc)).    5:- use_module(util(coalgebra)).    6:- use_module(util('fol-prover')).    7:- use_module(util(html)).    8:- use_module(util(latex)).    9:- use_module(util(math)).   10:- use_module(util(seqcal4)).   11:- use_module(util(npuzzle)).   12:- use_module(util(turing)).   13% :- use_module(util(matrix)).   % matrix_calc/3 unknown error: strange
   14:- qcompile(util(matrix)).   15:- use_module(util(langsem)).   16:- use_module(util(ptq)).   17:- use_module(util(models)).   18:- use_module(util(hmodel)).   19:- use_module(util(prooftree)).   20:- use_module(util(ifmap)).   21:- use_module(zdd(zdd)).   22:- use_module(zdd('zdd-plain')).   23:- use_module(pac('pac-listing')).   24
   25term_expansion --> pac:expand_pac.
   26
   27:- op(670, yfx, \).   28:- op(200, xfy, ^).   29
   30% :- use_module(util(zdd)).
   31% :- use_module(util('ptq-fragment')).
   32% :- use_module(util('emacs-handler')).
   33% :- use_module(util(interval)).
   34% :- use_module(gb('gb-top')).
   35
   36chat80(X, Y) :- ensure_loaded(lib('chat80-cgi')),
   37				chat80:cgi(X, Y).
   38show_env(X, Y):- getenv(X, Y).
   39
   40primrec_demo(X, Y):- primrecfast:eval_primrec_demo(X, Y).
   41
   42term_to_goal(X, such_that(V, Y), [], [], true):-
   43	term_to_goal(X, Y, V).
   44
   45setfont(X, Y):- flatten(["<font color=red size=6>", X, "</font>"], Y).
   46
   47		/**************************************
   48		*     First-order prover exercises    *
   49		**************************************/
   50
   51%;; (setq module-query  "qcompile(util(cgi)), module(cgi).")
   52% ?- qcompile(util(cgi)), module(cgi).
   53
   54web_proof_default_options([ clausal(false),
   55			    center([]),
   56			    initial_depth(300),
   57			    iteration_limit(5)]).

valid_tex(+X, -R) is det: Prove formula X, and unify R the result.

   62% ?- cgi:valid_test(a->a, R).
   63% ?- cgi:valid_test(a->(b->a), R).
   64valid_test(X, Result):- fol_prover:prove(X, Result).

valid_test_clausal(+P:pair, -R) is det: Prove clausal form P of FOL formulae P, and unify R with result.

   70% ?- cgi:valid_test_clausal(([[a,~b], [a,b], [~a,b], [~a,~b]], []), Result),
   71%	smash(Result).
   72% valid_test_clausal((X, Y), Result):-
   73% 	rename_vars((X, Y), (X0, Y0)),
   74% 	valid_test_clausal(Y0, X0, Result).
   75
   76
   77% ?- valid_test_clausal([], [[a],[a, -a]], Result).
   78% ?- leantap:apply_options([rm_tautology], [[a, -a]], X).
   79%
   80valid_test_clausal((X, Y), Result):-
   81	(	fol_prover:set_of_support_clausal(X, Y) ->
   82		Result = "Proved."
   83	;	Result = "NOT Provable."
   84	).
   85
   86% valid_test_clausal(X, [], Result):-!,
   87% 		leantap:apply_options(
   88% 		[	pure_literal_law,
   89% 			rm_tautology,
   90% 			cnf_normal,
   91% 			map_factoring,
   92% 			cnf_variant_normal
   93% 		 ],
   94% 		X, Y),
   95% 		fol_prover:linear_solve(Y, Result).
   96% valid_test_clausal(X, Cen, Result):-
   97% 	fol_prover:linear_solve_center(As, Ds, Result).
   98
   99
  100% ?- rename_vars([p(x,x), q(X, X)], R).
  101% ?- rename_vars([p(x,y,x), p(1,2), q(X, X)], R).
  102rename_vars(X, Y):- rename_vars(X, Y, [], _).
  103%
  104rename_vars(X, Y, A, B):-  % only u,v,w,z,y,z are Variables
  105	(	atom(X), u @=< X, X @=<z ->
  106			(	memberchk(X-Y, A) -> B = A
  107			; 	B = [X-Y|A]
  108			)
  109	;	is_list(X)	-> 	rename_vars_list(X, Y, A, B)
  110	;	compound(X)	->
  111		X =..[F|Xs],
  112		rename_vars_list(Xs, Ys, A, B),
  113		Y =..[F|Ys]
  114	;	Y = X,
  115		B = A
  116	).
  117%
  118rename_vars_list([], [], A, A).
  119rename_vars_list([X|Xs], [Y|Ys], A, B):-
  120	rename_vars(X, Y, A, C),
  121	rename_vars_list(Xs, Ys, C, B).

web_proof(+X:options, -V) is det: Prove formula in X, and unify V with the rusult.

  125web_proof(Options, V):- web_proof_default_options(D),
  126	completing_options(D, Options, Options0),
  127	memberchk(input(X), Options0),
  128	once(fol:old_prove(X, S, Options0)),
  129	(	memberchk(clausal(true), Options0)
  130	->  	(	integer(S),
  131			number_codes(S, S0),
  132			R = ["depth of search = ", S0, "\n<br/>"]
  133		;	R = S
  134		),
  135		memberchk(trace(Trace), Options0),
  136		maplist(copy_term, Trace, Trace0),
  137		maplist(rename_variable, Trace0),
  138		insert("\n<br/>", Trace0, Trace1),
  139		V0 = [R|Trace1]
  140	;	(	integer(S),
  141			V0 = 'proved.'
  142		;	V0 = 'no proof found.'
  143		)
  144	),
  145	smash_codes(V0, V).
  146
  147% ?-  cgi:rename_variable(f(A,B,C,A)).
  148rename_variable(T):- term_variables(T, Vs),
  149	( Vs == []
  150	->	Zip = []
  151	;	length(Vs, N),
  152		numlist(1, N, Ns),
  153		maplist(pred([I, V, I-V]), Ns, Vs, Zip)
  154	),
  155	maplist(pred([I - Name]:- fol:number_to_var_name(I, Name)), Zip).
  156
  157% ?- cgi_dnf(a, Dnf).
  158% ?- cgi_dnf(a+b, X).
  159% ?- cgi_dnf(-(a+b), X).
  160cgi_dnf(Boole, Z):- ltr, zmod:dnf(Boole, X), sets(X, Z).
  161
  162%?- cgi:demo_sed((@(s/"e"/"x"), "ea"), R).
  163%?- cgi:demo_sed((w("e")/"x", "ea"), R).
  164
  165demo_sed((Exp, String), Val):- string_codes(String, Codes),
  166	once(let_sed(G, Exp)),
  167	once(call(G,  Codes, Out)),
  168	string_codes(Val, Out).
  169
  170% ?- cgi_matrix([x, "1", "2"], R).
  171% ?- cgi_matrix(["x+y", "1", "2"], R).
  172cgi_matrix([E|Ms], A):-
  173	term_string(E0, E),
  174	maplist(parse_matrix, Ms, Ns),
  175	matrix_calc(Ns, E0, A).
  176%
  177parse_matrix(S, M):-
  178	split_string(S, "\n", "\s\n\t", U),
  179	remove([], U, V),
  180	maplist(parse_raw, V, M).
  181%
  182parse_raw(S, R):- split_string_by_word(S, "\s\s", U),
  183	maplist(pred(["",0] & ['', 0] & ([X,Y]:- term_string(Y, X))), U, V),
  184	maplist(pred([X, Y]:- Y is X), V, R).
  185%
  186matrix_html -->
  187	maplist(maplist(cgi_tag(td))),
  188	maplist(cgi_tag(tr)),
  189	insert("\n"),
  190	cgi_tag(table),
  191	cgi_tag(html),
  192	term_smash0.
  193
  194%.
  195cgi_tag(T, X, ["<", T, ">", X, "</", T, ">"]).
  196
  197% rational_codes(rdiv(X,Y), X/Y):-!.
  198% rational_codes(X, X).
  199
  200% javascript ããã®ä½¿ãæ¹
  201% act(`cgi:csv_demo`, `[@columns, @csv]`, `columns;csv`,
  202%      `ãããæ¼ãã¨æå®ãããã«ã©ã ãããä¸ã«è¡¨ç¤ºããã`,
  203%      CGI, setInnerHTML, `div`);
  204csv_demo --> peek([E, X], X),
  205	{herbrand(E, IndexList)},
  206	csv:columns(IndexList, `,`, `<br>`),
  207	smash.
  208
  209%- cgi:matrix_rule([1, set::pow([1,2])], y, R).
  210matrix_rule(L,x(N),A1):-!,
  211	nth1(N,L,A2),
  212	matrix_rule(L, A2, A1).
  213matrix_rule([A|A1], x, A2):-!,
  214	matrix_rule([A|A1],A,A3),
  215	matrix_rule([A|A1],A3,A2).
  216matrix_rule([A1,A|A2],y,A3):-!,
  217	matrix_rule([A1,A|A2],A,A4),
  218	matrix_rule([A1,A|A2],A4,A3).
  219matrix_rule([A1,A2,A|A3],z,A4):-!,
  220	matrix_rule([A1,A2,A|A3],A,A5),
  221	matrix_rule([A1,A2,A|A3],A5,A4)