Module

Baskerville.Explain

Package: purescript-baskerville-core
Repository: afcondon/purescript-baskerville

Reading the proof structure back out: the derivation DAG behind a claim, and the transitive closures a UI scrubs along.

Everything here exploits acyclicity-by-construction (premises point at strictly smaller ids): explain is a single backward scan over the feed prefix ending at the root — no recursion, no visited set beyond the growing needed-set.

#DerivationDag Source

type DerivationDag claim rule axiom = { edges :: Array Edge, nodes :: Array (Fact claim rule axiom), root :: FactId }

The proof behind one claim: every fact it transitively rests on (feed order — premises before conclusions), and the premise edges among them.

#Edge Source

type Edge = { from :: FactId, to :: FactId }

#explain Source

explain :: forall residue claim rule axiom. Ord claim => claim -> KB residue claim rule axiom -> Maybe (DerivationDag claim rule axiom)

#explainFact Source

explainFact :: forall residue claim rule axiom. KB residue claim rule axiom -> Fact claim rule axiom -> DerivationDag claim rule axiom

The DAG below a fact: scan the feed prefix backwards from the root; a fact is in the proof iff some already-needed fact cites it.

#supporters Source

supporters :: forall residue claim rule axiom. KB residue claim rule axiom -> Fact claim rule axiom -> Array (Fact claim rule axiom)

Direct premises of a fact, resolved.

#axiomsBehind Source

axiomsBehind :: forall residue claim rule axiom. Ord claim => claim -> KB residue claim rule axiom -> Array (Fact claim rule axiom)

The observation leaves a claim ultimately rests on.

#depthOf Source

depthOf :: forall residue claim rule axiom. KB residue claim rule axiom -> Map FactId Int

Longest premise chain below each fact (axioms at 0) — the cascade's stagger order. One forward scan; premises are always already depthed.

Modules: Baskerville.Conformance; Baskerville.Engine; Baskerville.Explain; Baskerville.Kernel; Baskerville.Rule