Editing emacs buffer regions by Prolog scripts

Objective of this post to share ideas to apply Prolog to edit the emacs buffer regions. First,
I would like to explain an example case. As I posted I had written a “simple minded prolog-like prover”.

So far more than one hundred small valid formulae and also also about 20 invalid ones, it returns as expeced.

% ?- time(test_prove(valid_formula)).
%@ all(A,p==f(A))==(p==all(B,f(B)))
%@ Proved.
%@ p==all(A,f(A))->all(B,(f(B)->p))
%@ Proved.


%@ ** 91 formulae tested.

%@ % 487,006 inferences, 0.041 CPU in 0.106 seconds (38% CPU, 11995517 Lips)
%@ true.

% ?- time(test_prove(invalid_formula)).

%@ some(A,p(A))->all(A,p(A))
%@ NOT provable.
%@ all(A,some(B,p(A,B)))->some(B,all(A,p(A,B)))
%@ NOT provable.


%@ ** 19 formulae tested.
%@ % 14,070 inferences, 0.002 CPU in 0.002 seconds (91% CPU, 8653137 Lips)
%@ true.

However I have still no idea about “timeout” formulae.

timeout_formula(all(X, p(X))-> some(Y, (p(Y), p(f(Y))))

Now this is the place I used prolog to edit emacs buffer region.
I noticed that the above predicates valid_formula/invalid_formula
were redundant. In fact many redundant formulae like this.


So I wrote an emacs buffer handler in prolog

handle([free, variant])--> region, % get region in codes.
	split,			% split by `\n`
	remove([]),		% remove empty lines.
	maplist(pred(([X, Y-S]:- string_codes(S, X),	% parse each line as a term.
				 term_string(Y, S, [module(fol_prover)])))),
	peek(Terms, []),	% get current contents, and put [] as a inital value.
	add_non_variant(Terms),	% remove terms so that no variant pairs there.
	maplist(pred([_-S, [S,"\n"]])),	% put orginal terms with new line code at end.
	overwrite.  % replace the input region with the slimmed result.

% ?- add_non_variant([A-1, B-2, A-1], [], R).
%@ R = [A-1].
% ?- add_non_variant([f(A)-1, g(B)-2, f(A)-2], [], R).
%@ R = [g(B)-2, f(A)-1].

add_non_variant([], X, X).
add_non_variant([P|U], X, Y):-add_non_variant_one(P, X, Z),
	add_non_variant(U, Z, Y).
add_non_variant_one(A-B, X, Y):-
	(	member(C-_, X), variant(A, C) -> Y = X
	;	Y = [A-B|X]

For example, suppose the current region with


becomes this with variants formula removed.


The “handle” critically uses swi-prolog builtins term_string/3, and variant/2.

Now I am wondering how ones edit such region in a handy way. So far I never
heard about such use of prolog to edit emacs buffer. I believe there maybe
smarter ways to edit emacs buffer by prolog. However, as I have some experiences on this and still several basic questions I would like to ask emacs experts, I would like to share idea and experiences.

Hi there,

FWIW, with Sweep you can call Elisp functions (such as insert and delete-region and other buffer editing functions) from your SWI-Prolog code. See Sweep: SWI-Prolog Embedded in Emacs


EDIT: to be clear, Sweep also lets you invoke Prolog from Elisp (and vice versa, as mentioned above), so you can define an Emacs command which calls Prolog, which then calls Elisp to edit an Emacs buffer. Although TBH, for the purpose of editing Emacs buffers, I’d just stick to Elisp most probably :slight_smile:

I would like to try again later. In fact, once I tried but I failed for even simple
lisp function call from Prolog, despite reading reference. I installed and updates
sweep daily base via package manager of Emacs.

1 Like

I have tried an ad hoc idea. For given formula A,
run two processes (threads) in parallel, with iterated deepening method having the depth limit
in common, one is for A, the other is for negation of A. The output is (1) A is valid, (2) A is unsatisfiable, (3) A is invalid, or (4) A is NOT unsatisfiable. Note that A is invalid when A is not unsatisfiable. Although there is of course no guarantee in theory on FOL prover that this parallel processes terminate, this simple
“parallel prover” seems work on the “timeout” formula in a way of “conservative extension” of
the prolog-like prover.

 % ?- time(prove(all(X, p(X))-> some(Y, (p(Y) * p(f(Y)))))).
%@ valid
%@ % 1,181 inferences, 0.000 CPU in 0.000 seconds (93% CPU, 3393678 Lips)
%@ true.

% ?- time(prove(all(X, p(X))-> all(Y, (p(Y) * p(f(Y)))))).
%@ valid
%@ % 1,259 inferences, 0.000 CPU in 0.000 seconds (89% CPU, 3195431 Lips)
%@ true.

% ?- time(prove(all(X, p(X))-> -some(Y, (p(Y) * p(f(Y)))))).
%@ invalid
%@ % 1,274 inferences, 0.000 CPU in 0.000 seconds (95% CPU, 3241730 Lips)
%@ true.

I should be familiar with thread programming of swi-prolog, which seems fit what I have in mind
as parallelism but I am doing in the usual single thread.

EDIT I was confused with my scattered test formulae. The following
was really the timeout example. For human it should be obvious that
this is false, but my “simple-minded” prover continue endless search to find
refutation in iterated deepening search.

%@ 22 : all(A,p(A))->some(B,(p(B) * -p(f(B))))

like prolog goes into similar sittiuation for

?- p(A).
p(A):- p(f(A)).

In fact, I checked by hand that CNF of negation of formula 22 becomes similar to the above prolog clause

EDIT I “discovered” the formula by writing a simple emacs editing snipet
for numbering terms in the whole file on the current buffer. I am personally surprised
with how fast prolog works enough on emacs buffer despite of asynchronous communication in utf8 encoding.

It still sounds nice and like what I wish to have, but I have only lengthy concrete codes emacs-lisp and prolog codes to implements such communication between them, and more worse, details of which it is now difficult for me to remember. Fortunately, it still works as I expect, and here is a new simplified example “handle” on fill-paragraph which uses internally such mentioned basic codes. Of course such fill-paragraph must have been implemented in emacs-lisp, my interest is what kind of prolog codes for such fill-paragraph provided that the region is given as a list of character codes of text. The code below may have a careless bug, but I hope it shows some aspect of DCG-like approaches to edit
emacs region by prolog. I know there are many things for me to write what are behind this codes, but I have to say still they are poor and, worse, scattered in the pack library pac.

Listing of handle(fill, paragraph)
%!	handle([fill, paragraph])//2 is det.
%	Asssuming a global variable paragraph_width is set,
%	the region is filled so that the width of each line
%	fits the specified width.

% ?- nb_setval(paragraph_width, 3).

% for exampe, the region of this content
% a
%   b    c
% d e t

% ==>  is filled as this:
% a b
% c d
% e t

handle([fill, paragraph]) --> region,
	{	words(Words, [], X, []),
		maplist(string_codes, SWords, Words),
		(	nb_current(paragraph_width, Width)->true
		;	Width = 10
		fill_paragraph(Width, P, [], SWords) 
	maplist(insert(" ")),

% ?- fill_string_paragraph(5, "a  b  c  d", P).
%@ P = [["a", "b", "c"], ["d"]].
% ?- fill_string_paragraph(5, "a\t\t\r\n  b\n  c\n  d\n", P).
%@ P = [["a", "b", "c"], ["d"]].

fill_string_paragraph(K, X, P):- string_codes(X, Y),
	words(Words_in_codes, [], Y, []),
	maplist(string_codes, Words_in_string, Words_in_codes),
	fill_paragraph(K, P, [], Words_in_string).

% ?-words(X, [], `abc`, []), maplist(flip(string_codes), X, R).
% ?-words(X, [], `\t\t`,[]), maplist(flip(string_codes), X, R).
% ?-words(X, [], ` ab c\td \n`,[]), maplist(flip(string_codes), X, R).

words([X|Y], Z) --> wl("[^\s\t\n\r]+", X, []), !, words(Y, Z).
words(X, Y) --> wl("[\s\t\n\r]+"), !, words(X, Y).
words(X, X) --> [].

% ?- fill_paragraph(3, P, [], [a,a,a,a,a,a,a]).

fill_paragraph(_, P, P, []):-!.
fill_paragraph(W, P, Q, R):-
	fill_line(W, W, P, U, R, U),
	fill_paragraph(W, U, Q, U).

% ?- fill_line(5, 5, X, [], [a, a, a, a, a, a, a, a, a], R).
% ?- fill_line(5, 5, X, [], [a, a, a, a, a, a], R).
% ?- fill_line(1, 1, X, [], [a, a, a], R).
% ?- fill_line(10, 10,  X, [], [ab, cd, e, f, ghi, a, a, a, a], R).
% ?- fill_line(10, 10,  X, [], [ab], R).

fill_line(W, W, X, X, [], []):-!.
fill_line(_, _, [[]|X], X, [], []):-!.
fill_line(Width, K, X, Y, [Word|U], V):-
	insert_word_at_end(Width, K, K0, X, Z, Word),
	fill_line(Width, K0, Z, Y, U, V).

insert_word_at_end(Width, K, K0, X, Y, Word):-!,
	string_length(Word, A),
	compare(C, A, K),
	(	C = (=) ->
		X = [[Word]|Y],
		K0 = Width
	;	C = (<) ->
		X = [[Word|P]|X0],
		Y = [P|X0],
		K0 is K-(A + 1)
	;	Width =< A  ->
		X = [[]|[[Word]|Y]],
		K0 is Width
	;   X = [[],[Word|P] | Q],
		Y = [P|Q],
		K0 is Width -(A + 1)