b3a41bca57
WIP: cases 23-24 added; 24 (improvise-yea8) still fails. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
391 lines
15 KiB
Prolog
391 lines
15 KiB
Prolog
% Reads the knowledge base and a delta as DATA -- never consults either -- and
|
|
% writes their merge in canonical form. See context/code/kb-tool.md for why.
|
|
|
|
% No initialization/1: scripts/kb supplies a goal that turns a throw into
|
|
% exit 2 and a failure into exit 1. Measured on trealla 3.10.3, `-g main,halt`
|
|
% exits 0 for BOTH -- silently reporting a crash as a clean run.
|
|
main :-
|
|
current_prolog_flag(argv, Argv),
|
|
( Argv = [ModeStr, KbFile, DeltaFile, OutFile], mode_atom(ModeStr, Mode)
|
|
-> run(Mode, KbFile, DeltaFile, OutFile)
|
|
; Argv = [CountStr, KbFile], CountStr == "count"
|
|
-> count_only(KbFile)
|
|
; Argv = [CS, BaseFile, CandFile, ExcFile, LedgerOut], CS == "complete"
|
|
-> complete(BaseFile, CandFile, ExcFile, LedgerOut)
|
|
; die('usage: kb-merge.pl <add|replace|remove> <kb> <delta> <out> | count <kb> | complete <baseline> <candidate> <removed> <ledger-out>')
|
|
).
|
|
|
|
% argv arrives as strings; every later comparison is on an atom.
|
|
mode_atom(S, add) :- S == "add", !.
|
|
mode_atom(S, replace) :- S == "replace", !.
|
|
mode_atom(S, remove) :- S == "remove", !.
|
|
|
|
run(remove, KbFile, DeltaFile, OutFile) :-
|
|
!,
|
|
terms_of(KbFile, Old),
|
|
terms_of(DeltaFile, Doomed),
|
|
check_callable(Doomed),
|
|
functional_preds(Old, Funcs),
|
|
check_self_consistent(Funcs, Doomed),
|
|
absent(Funcs, Old, Doomed, Missing),
|
|
( Missing == []
|
|
-> true
|
|
; format("kb-merge: REFUSED -- no such clause to remove:~n", []),
|
|
forall(member(K, Missing), format(" ~q~n", [K])),
|
|
halt(2)
|
|
),
|
|
foldl_remove(Funcs, Doomed, Old, Kept),
|
|
length(Old, NOld),
|
|
findall(x, ( member(O, Old), clause_key(Funcs, O, KO),
|
|
member(T, Doomed), clause_key(Funcs, T, KT), same_key(KO, KT) ), Hits),
|
|
length(Hits, NHits),
|
|
ExpectK is NOld - NHits,
|
|
check_total(Kept, ExpectK),
|
|
write_terms(OutFile, Kept),
|
|
verify(OutFile, Kept),
|
|
length(Old, NO), length(Kept, NK),
|
|
Gone is NO - NK,
|
|
format("kb-merge: ~w before, ~w removed, ~w after~n", [NO, Gone, NK]).
|
|
run(Mode, KbFile, DeltaFile, OutFile) :-
|
|
terms_of(KbFile, Old),
|
|
terms_of(DeltaFile, New),
|
|
check_callable(New),
|
|
functional_preds(Old, Funcs),
|
|
check_self_consistent(Funcs, New),
|
|
conflicts(Funcs, Old, New, Clashes),
|
|
gate(Mode, Clashes),
|
|
check_rule_replace(Funcs, Mode, Old, New),
|
|
foldl_merge(Funcs, New, Mode, Old, Merged),
|
|
expected_total(Funcs, Mode, Old, New, Expect),
|
|
check_total(Merged, Expect),
|
|
write_terms(OutFile, Merged),
|
|
verify(OutFile, Merged),
|
|
length(Old, NO), length(New, NN), length(Merged, NM),
|
|
format("kb-merge: ~w before, ~w in delta, ~w after~n", [NO, NN, NM]).
|
|
|
|
% A term can parse and still not be a clause: `42.` reads fine, is not
|
|
% callable, and reached the knowledge base as a fact whose head is a number.
|
|
% Nothing downstream objected -- kb_consistent has no opinion about stray terms.
|
|
check_callable([]).
|
|
check_callable([T|Ts]) :-
|
|
( bad_shape(T, Why)
|
|
-> format("kb-merge: REFUSED -- ~w: ~q~n", [Why, T]),
|
|
halt(2)
|
|
; check_callable(Ts)
|
|
).
|
|
|
|
% A DIRECTIVE is callable, so a callable test alone lets one through -- and the
|
|
% candidate is validated by consulting it, so `:- halt(0).` exits the check
|
|
% with success before kb_consistent runs and the gate passes by never running.
|
|
bad_shape(T, 'a directive, which would run when the result is checked') :-
|
|
nonvar(T), T = (:- _), !.
|
|
bad_shape(T, 'a query') :-
|
|
nonvar(T), T = (?- _), !.
|
|
bad_shape(T, 'not a clause') :-
|
|
clause_head(T, H), \+ callable(H).
|
|
bad_shape(T, 'part of the gate that validates this write') :-
|
|
\+ gate_writes_allowed,
|
|
clause_pred(T, P),
|
|
gate_predicate(P).
|
|
|
|
% Removing kb_consistent made the check pass by not existing; REPLACING it with
|
|
% a fact that is trivially true passes forever after. A write that can disarm
|
|
% its own validation is refused unless KB_ALLOW_GATE says otherwise, which makes
|
|
% an intentional change to the checker a deliberate, greppable act.
|
|
% Hand-maintained, and that is its weakness: a new gate predicate is unprotected
|
|
% until it is named here.
|
|
gate_predicate(kb_consistent/0).
|
|
gate_predicate(kb_report/0).
|
|
gate_predicate(kb_error/1).
|
|
gate_predicate(functional/1).
|
|
gate_predicate(kb_sentinel/1).
|
|
gate_predicate(known_crate/1).
|
|
gate_predicate(kb_external_check/1).
|
|
|
|
gate_writes_allowed :-
|
|
catch(getenv('KB_ALLOW_GATE', V), _, fail),
|
|
V \== '',
|
|
V \== '0'.
|
|
|
|
clause_head((H :- _), H) :- !.
|
|
clause_head(H, H).
|
|
|
|
% Which leading arguments identify a clause. Anything not listed keys on the
|
|
% WHOLE head, so a multi-valued relation -- a crate depends on several crates --
|
|
% can hold many clauses and only an exact repeat is a duplicate.
|
|
% This cannot be read off the KB's own functional/1: that check keys an arity-3
|
|
% predicate on its FIRST argument, which is right for crate/3 and wrong for
|
|
% decision/3, where one ticket carries several decisions under different names.
|
|
% Hand-maintained, like gate_predicate/1, but the default is the safe direction.
|
|
% A RULE keys on the whole clause, because two clauses with the same head shape
|
|
% and different bodies is ordinary Prolog -- keying a rule on its head alone
|
|
% made the second refuse as a duplicate, or worse, silently replace the first.
|
|
clause_key(Funcs, (H :- B), K) :-
|
|
!,
|
|
( clause_pred((H :- B), P), key_arity(P, _)
|
|
-> head_key(Funcs, H, K)
|
|
; K = (H :- B)
|
|
).
|
|
clause_key(Funcs, H, K) :- head_key(Funcs, H, K).
|
|
|
|
key_arity(doctrine/2, 1).
|
|
key_arity(invariant/2, 1).
|
|
key_arity(decision/3, 2).
|
|
key_arity(work_done/3, 2).
|
|
key_arity(work_followup/3, 2).
|
|
key_arity(crate/3, 1).
|
|
key_arity(location/3, 2).
|
|
key_arity(groom_check/2, 1).
|
|
key_arity(kb_issue_found/2, 1).
|
|
key_arity(wasm_runtime_hazard/3, 2).
|
|
|
|
head_key(_, H, K) :-
|
|
functor(H, F, A),
|
|
( key_arity(F/A, N), H =.. [F|Args], length(Front, N), append(Front, _, Args)
|
|
-> K =.. [F|Front]
|
|
; K = H
|
|
).
|
|
|
|
functional_preds(_, []).
|
|
|
|
clause_pred((H :- _), F/A) :- !, functor(H, F, A).
|
|
clause_pred(H, F/A) :- functor(H, F, A).
|
|
|
|
% Keys were only checked against the EXISTING file, so two clauses sharing a
|
|
% previously-unused key clashed with nothing and the merge silently dropped the
|
|
% first -- add discarding part of its own payload, visible only as a delta count
|
|
% that did not match the clauses added.
|
|
check_self_consistent(Funcs, New) :-
|
|
findall(C, ( member(T, New), clause_key(Funcs, T, K), canon_key(K, C) ), Ks),
|
|
msort(Ks, Sorted),
|
|
adjacent_dups(Sorted, Dups0),
|
|
sort(Dups0, Dups),
|
|
( Dups == []
|
|
-> true
|
|
; format("kb-merge: REFUSED -- the delta names one key twice:~n", []),
|
|
forall(member(K, Dups), format(" ~q~n", [K])),
|
|
halt(2)
|
|
).
|
|
|
|
adjacent_dups([], []).
|
|
adjacent_dups([_], []).
|
|
adjacent_dups([A, B|T], Out) :-
|
|
( A == B
|
|
-> Out = [A|Rest]
|
|
; Out = Rest
|
|
),
|
|
adjacent_dups([B|T], Rest).
|
|
|
|
% The tool printed "N in delta" beside a total that did not account for N,
|
|
% twice, and nothing compared them. This checks the arithmetic the report
|
|
% already shows, which catches a dropped clause without knowing about keys.
|
|
check_total(Result, Expect) :-
|
|
length(Result, Got),
|
|
( Got =:= Expect
|
|
-> true
|
|
; format("kb-merge: REFUSED -- would write ~w clauses, expected ~w; a clause was dropped~n",
|
|
[Got, Expect]),
|
|
halt(2)
|
|
).
|
|
|
|
expected_total(_, add, Old, New, Expect) :-
|
|
length(Old, NO), length(New, NN), Expect is NO + NN.
|
|
expected_total(Funcs, replace, Old, New, Expect) :-
|
|
length(Old, NO),
|
|
findall(x, ( member(T, New), clause_key(Funcs, T, K),
|
|
\+ ( member(O, Old), clause_key(Funcs, O, K2), same_key(K, K2) ) ), Fresh),
|
|
length(Fresh, NF),
|
|
Expect is NO + NF.
|
|
|
|
conflicts(Funcs, Old, New, Clashes) :-
|
|
findall(K,
|
|
( member(T, New), clause_key(Funcs, T, K),
|
|
member(O, Old), clause_key(Funcs, O, K2), same_key(K, K2) ),
|
|
Clashes).
|
|
|
|
% A rule keys on its whole clause, so an EDITED rule matches nothing and
|
|
% `replace` silently becomes `add` -- both arms then live, and the stale one
|
|
% goes on firing beside the new one. check_total cannot see it: NO + NF is
|
|
% correct arithmetic for an add. So replace refuses a rule it cannot find and
|
|
% names the route, which is rm then add (improvise-dj1l, review of PR #69).
|
|
check_rule_replace(Funcs, replace, Old, New) :-
|
|
!,
|
|
findall(T,
|
|
( member(T, New), T = (_ :- _),
|
|
clause_key(Funcs, T, K),
|
|
\+ ( member(O, Old), clause_key(Funcs, O, K2), same_key(K, K2) ) ),
|
|
Fresh),
|
|
( Fresh == []
|
|
-> true
|
|
; format("kb-merge: REFUSED -- replace cannot find these rules, so it would ADD them rather than replace anything:~n", []),
|
|
forall(member(T, Fresh), format(" ~q~n", [T])),
|
|
die('a rule is keyed on its whole clause, so an edited body is a NEW clause: kb rm the old one, then kb add')
|
|
).
|
|
check_rule_replace(_, _, _, _).
|
|
|
|
gate(add, []) :- !.
|
|
gate(add, Clashes) :-
|
|
!,
|
|
format("kb-merge: REFUSED -- ~w clause(s) already present:~n", [Clashes]),
|
|
forall(member(K, Clashes), format(" ~q~n", [K])),
|
|
die('use replace to overwrite an existing clause').
|
|
gate(replace, _).
|
|
gate(M, _) :- die(M).
|
|
|
|
foldl_merge(_, [], _, Acc, Acc).
|
|
foldl_merge(Funcs, [T|Ts], Mode, Acc0, Acc) :-
|
|
clause_key(Funcs, T, K),
|
|
exclude(has_key(Funcs, K), Acc0, Acc1),
|
|
clause_pred(T, P),
|
|
insert_after_last(Acc1, P, T, Acc2),
|
|
foldl_merge(Funcs, Ts, Mode, Acc2, Acc).
|
|
|
|
% Key matching is VARIANT equality, never unification. Unifying a key against a
|
|
% clause both matched too much -- a non-ground key probe(X) matched probe(a),
|
|
% destroying it -- and MUTATED the incoming clause, because the unification
|
|
% bound X to a, so the rule written was not the rule supplied. The round-trip
|
|
% check cannot see that: it compares the file against an intended list already
|
|
% corrupted by the same unification.
|
|
has_key(Funcs, K, T) :- clause_key(Funcs, T, K2), same_key(K, K2).
|
|
|
|
same_key(K1, K2) :- canon_key(K1, C1), canon_key(K2, C2), C1 == C2.
|
|
|
|
canon_key(K, C) :- copy_term(K, C), numbervars(C, 0, _).
|
|
|
|
% A remove that matches nothing is refused rather than silently doing nothing:
|
|
% a typo'd key would otherwise report success and leave the clause in place.
|
|
absent(Funcs, Old, Doomed, Missing) :-
|
|
findall(K,
|
|
( member(T, Doomed), clause_key(Funcs, T, K),
|
|
\+ ( member(O, Old), clause_key(Funcs, O, K2), same_key(K, K2) ) ),
|
|
Missing).
|
|
|
|
foldl_remove(_, [], Acc, Acc).
|
|
foldl_remove(Funcs, [T|Ts], Acc0, Acc) :-
|
|
clause_key(Funcs, T, K),
|
|
exclude(has_key(Funcs, K), Acc0, Acc1),
|
|
foldl_remove(Funcs, Ts, Acc1, Acc).
|
|
|
|
% Keeps each predicate a contiguous block: a new clause lands after the last
|
|
% one of its own predicate, or at the end when the predicate is new.
|
|
insert_after_last([], _, T, [T]).
|
|
insert_after_last([H|Rest], P, T, Out) :-
|
|
( clause_pred(H, P), \+ ( member(X, Rest), clause_pred(X, P) )
|
|
-> Out = [H, T|Rest]
|
|
; Out = [H|Tail], insert_after_last(Rest, P, T, Tail)
|
|
).
|
|
|
|
terms_of(File, Terms) :-
|
|
catch(open(File, read, S), _, die_file(File)),
|
|
read_all(S, Terms),
|
|
close(S).
|
|
|
|
% An uncaught syntax error drops trealla into its REPL, which waits on stdin --
|
|
% so a malformed delta HANGS with a terminal and exits 0 without one, reading
|
|
% as acceptance. Catching it is what makes the refusal a refusal.
|
|
read_all(S, Terms) :-
|
|
catch(read_term(S, T, []), E, parse_died(E)),
|
|
( T == end_of_file
|
|
-> Terms = []
|
|
; Terms = [T|Rest], read_all(S, Rest)
|
|
).
|
|
|
|
parse_died(E) :-
|
|
format("kb-merge: REFUSED -- does not parse: ~w~n", [E]),
|
|
halt(2).
|
|
|
|
write_terms(File, Terms) :-
|
|
open(File, write, S),
|
|
forall(member(T, Terms), portray_clause(S, T)),
|
|
close(S).
|
|
|
|
% The guard that matters: read the file back and require it to be exactly what
|
|
% was intended. A serializer bug is the wipe-the-KB failure with a new owner.
|
|
verify(File, Intended) :-
|
|
terms_of(File, Written),
|
|
canon(Written, CW),
|
|
canon(Intended, CI),
|
|
( CW == CI
|
|
-> true
|
|
; length(Written, NW), length(Intended, NI),
|
|
format("kb-merge: ROUND-TRIP FAILED -- wrote ~w terms, meant ~w~n", [NW, NI]),
|
|
die('output does not read back as the intended clauses')
|
|
).
|
|
|
|
% Reading a term back yields FRESH variables, so == compares variable identity
|
|
% rather than clause content. numbervars over a copy gives variant equality.
|
|
canon(Terms, Canon) :- copy_term(Terms, Canon), numbervars(Canon, 0, _).
|
|
|
|
count_only(KbFile) :-
|
|
terms_of(KbFile, Terms),
|
|
forall(member(P, [doctrine/2, invariant/2, decision/3, work_done/3]),
|
|
( findall(x, ( member(T, Terms), clause_pred(T, P) ), L),
|
|
length(L, N),
|
|
P = F/A,
|
|
format("~w/~w=~w~n", [F, A, N]) )),
|
|
length(Terms, Total),
|
|
format("total=~w~n", [Total]).
|
|
|
|
% Consistency is not completeness: a kb that lost 276 clauses still passed
|
|
% kb_consistent. Why by key and against HEAD: context/code/kb-tool.md.
|
|
% Keys are counted, not collected: a merge can commit two clauses under one
|
|
% key, and a set of keys cannot see one of them go (improvise-ih3k).
|
|
complete(BaseFile, CandFile, ExcFile, LedgerOut) :-
|
|
terms_of(BaseFile, Base),
|
|
terms_of(CandFile, Cand),
|
|
terms_of(ExcFile, Exc),
|
|
key_counts(Base, BaseCounts),
|
|
key_counts(Cand, CandCounts),
|
|
ground_keys(Exc, ExcKeys),
|
|
findall(K-D, ( member(K-NBK, BaseCounts), count_of(K, CandCounts, NCK),
|
|
D is NBK - NCK, D > 0 ), Short),
|
|
findall(K-D, ( member(K-D, Short), \+ memberchk(K, ExcKeys) ), Unexcused),
|
|
findall(T, ( member(K-_, Unexcused), lost_under(K, Base, Cand, T) ), Missing),
|
|
length(Base, NB), length(Cand, NC),
|
|
( Unexcused == []
|
|
-> findall(E, ( member(E, Exc), ground_key(E, K), memberchk(K-_, Short) ), Kept),
|
|
write_terms(LedgerOut, Kept),
|
|
length(Kept, NK),
|
|
format("kb-merge: complete -- baseline ~w, result ~w, ~w removal(s) recorded~n",
|
|
[NB, NC, NK])
|
|
; foldl(add_deficit, Unexcused, 0, NM),
|
|
format("kb-merge: REFUSED -- the baseline has ~w clauses and the result ~w; ~w of the baseline's are missing and no kb rm recorded their removal:~n",
|
|
[NB, NC, NM]),
|
|
forall(( nth1(I, Missing, T), I =< 10 ), format(" ~q~n", [T])),
|
|
( NM > 10 -> Rest is NM - 10, format(" ... and ~w more~n", [Rest]) ; true ),
|
|
halt(2)
|
|
).
|
|
|
|
ground_key(T, C) :- clause_key([], T, K), canon_key(K, C).
|
|
|
|
ground_keys(Terms, Sorted) :-
|
|
findall(C, ( member(T, Terms), ground_key(T, C) ), Cs),
|
|
sort(Cs, Sorted).
|
|
|
|
key_counts(Terms, Counts) :-
|
|
findall(C, ( member(T, Terms), ground_key(T, C) ), Cs),
|
|
msort(Cs, Sorted),
|
|
run_lengths(Sorted, Counts).
|
|
|
|
run_lengths([], []).
|
|
run_lengths([K|T], [K-N|Rest]) :-
|
|
same_run(K, T, 1, N, After),
|
|
run_lengths(After, Rest).
|
|
|
|
same_run(K, [X|T], N0, N, After) :- X == K, !, N1 is N0 + 1, same_run(K, T, N1, N, After).
|
|
same_run(_, After, N, N, After).
|
|
|
|
count_of(K, Counts, N) :- ( memberchk(K-N0, Counts) -> N = N0 ; N = 0 ).
|
|
|
|
add_deficit(_-D, N0, N) :- N is N0 + D.
|
|
|
|
% What to name for a short key: the baseline's clauses under it that the
|
|
% result holds no variant of, or the first one when every text survives.
|
|
lost_under(K, Base, Cand, T) :-
|
|
findall(B, ( member(B, Base), ground_key(B, KB), KB == K ), Under),
|
|
findall(B, ( member(B, Under), \+ ( member(C, Cand), same_key(B, C) ) ), Gone),
|
|
( Gone == [] -> Under = [T|_] ; member(T, Gone) ).
|
|
|
|
die(Msg) :- format("kb-merge: ~w~n", [Msg]), halt(2).
|
|
die_file(F) :- format("kb-merge: cannot read ~w~n", [F]), halt(2).
|