% 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), length(Doomed, NDoomed),
    ExpectK is NOld - NDoomed,
    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.
complete(BaseFile, CandFile, ExcFile, LedgerOut) :-
    terms_of(BaseFile, Base),
    terms_of(CandFile, Cand),
    terms_of(ExcFile, Exc),
    ground_keys(Cand, CandKeys),
    ground_keys(Exc, ExcKeys),
    findall(T, ( member(T, Base), ground_key(T, K),
                 \+ memberchk(K, CandKeys), \+ memberchk(K, ExcKeys) ), Missing),
    length(Base, NB), length(Cand, NC),
    (  Missing == []
    -> ground_keys(Base, BaseKeys),
       findall(E, ( member(E, Exc), ground_key(E, K),
                    memberchk(K, BaseKeys), \+ memberchk(K, CandKeys) ), Kept),
       write_terms(LedgerOut, Kept),
       length(Kept, NK),
       format("kb-merge: complete -- baseline ~w, result ~w, ~w removal(s) recorded~n",
              [NB, NC, NK])
    ;  length(Missing, 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).

die(Msg) :- format("kb-merge: ~w~n", [Msg]), halt(2).
die_file(F) :- format("kb-merge: cannot read ~w~n", [F]), halt(2).