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.
<snip>
%@ ** 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.
<snip>
%@ ** 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.
valid_formula(A->A).
valid_formula(B->B).
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.
reverse,
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
valid_formula(A->A).
valid_formula(B->B).
valid_formula(C->C).
becomes this with variants formula removed.
valid_formula(A->A).
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.
