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):-
   65	(	fol_prover:prove(X) ->
   66		Result = "Proved."
   67	;	Result = "NOT provable."
   68	).

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

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

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

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