Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 47 additions & 1 deletion src/v2/std/qualified_name.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ import v2.std.diagnostic {
import std.algebra { Cons, Empty, FreeMonoid }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import std.disposition { Disposition, Scaffold, RealizationDispatch }
import v2.std.algebra { HeadAbsent, HeadFound, fold_list_right, is_empty, list_head, list_init, list_snoc_item }
import v2.std.algebra { HeadAbsent, HeadFound, fold_list_right, is_empty, is_prefix_of, list_head, list_init, list_snoc_item }
import v2.std.collection {
List
}
Expand Down Expand Up @@ -211,6 +211,52 @@ fn qualified_name_last_segment(qn: QualifiedName) -> Optional<Symbol> {
}
}

// STRICT DESCENT UNDER A NAMESPACE CONTAINER, as a RELATION and deliberately not as an enumeration.
//
// A module is a containment subtree and the path-module binding is derived at parse, so whether one
// qualified name lies beneath another is a fact about NAMES and is decided here, at the authority
// that owns QualifiedName -- not at a storage index, which would couple a naming question to one
// realization of where modules are kept.
//
// WHY A RELATION AND NOT A LIST OF MEMBERS. Every caller that could ask "which modules are under X"
// already holds the finite population -- the index is supplied to it, not discovered by it -- so the
// only fact missing at the namespace layer is the containment decision. Returning a sequence would
// hand every consumer a realization order for free, and index order is exactly the positional
// history a consumer must NOT reconstruct: ordering has to be grounded independently, by a
// row-owned ordinal or equivalent. A comment asking consumers to ignore an exported order is the
// defect restated, so no order is exported. The consumer folds its own population and applies its
// own ordering, and this answers member-or-not.
//
// SEGMENT-WISE, NOT TEXTUAL: `gunbc.rowing` is not under `gunbc.row`, because containment is a
// relation on SEGMENTS and a dotted string is a rendering of them.
//
// CONSUMPTION (DESIGN §3c), stated here rather than only in a pull request body, because a body is
// not in the tree a later reader greps. Consumed by execution in this change: this module's claim
// probes, which exercise the relation rather than assert that it exists. Beyond them this is a
// DECLARED FRONTIER, not a consumed declaration, and the honest state is named as such.
//
// Named later consumer: the failure-mode roster's membership, which today is a hand-authored tail
// listing what containment already knows -- which is why two lanes appending independent rows
// collide in one merge region.
//
// TRIGGER, named as the CAPABILITY and not as an artifact that would contribute to one: roster
// membership becomes DERIVED from the row-files, so no hand-authored tail must be edited to
// register a row. A batch split, a reformat, or any other rewrite of the tail satisfies none of
// it and does not retire this frontier. Ordering is deliberately NOT part of the trigger: the
// roster's order is load-bearing and must be grounded by the consuming projection, never taken
// from a sequence this relation refuses to export.
//
// STRICT: a name is a prefix of itself, and a container is not beneath itself. The neighbouring
// question -- whether a given module is present at all -- is exact-identity membership and is
// answered elsewhere; this is descent, and the two are disjoint rather than one refining the other.
fn qualified_name_is_strict_descendant(
container: QualifiedName,
candidate: QualifiedName
) -> Bool {
is_prefix_of(prefix: container, xs: candidate, eq: fn(a, b) { a == b })
&& candidate != container
}

fn qualified_name_snoc(qn: QualifiedName, segment: Symbol) -> QualifiedName {
list_snoc_item(xs: qn, item: segment)
}
Expand Down
52 changes: 52 additions & 0 deletions src/v2/test/claim/qualified_name_strict_descent_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
module v2.test.claim.qualified_name_strict_descent

import v2.std.logic { Bool }
import v2.std.collection { List }
import v2.std.text { String }
import v2.std.qualified_name {
QualifiedName,
qualified_name_from_string_segments,
qualified_name_is_strict_descendant
}
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

fn qn(segments: List<String>) -> QualifiedName {
qualified_name_from_string_segments(segments: segments)
}

fn container() -> QualifiedName {
qn(segments: ["gunbc", "row"])
}

test fn strict_descent_admits_a_child_and_refuses_a_sibling() -> Bool {
qualified_name_is_strict_descendant(container: container(), candidate: qn(segments: ["gunbc", "row", "first"]))
&& !qualified_name_is_strict_descendant(container: container(), candidate: qn(segments: ["gunbc", "other", "first"]))
}

// `row` is a textual prefix of `rowing`, and containment must refuse it: this is the control that
// separates a segment-wise relation from a string one, and it is the case a dotted-string
// implementation gets wrong while passing every other probe here.
test fn strict_descent_refuses_a_segment_that_merely_starts_with_the_container() -> Bool {
!qualified_name_is_strict_descendant(container: container(), candidate: qn(segments: ["gunbc", "rowing"]))
}

test fn strict_descent_refuses_the_container_itself() -> Bool {
!qualified_name_is_strict_descendant(container: container(), candidate: container())
}

test fn strict_descent_admits_a_deeper_descendant() -> Bool {
qualified_name_is_strict_descendant(
container: container(),
candidate: qn(segments: ["gunbc", "row", "first", "nested"])
)
}

// Descent is not symmetric: an ancestor is not beneath its own descendant.
test fn strict_descent_refuses_the_reverse_direction() -> Bool {
!qualified_name_is_strict_descendant(
container: qn(segments: ["gunbc", "row", "first"]),
candidate: container()
)
}
Loading