Repository navigation
Compile door refuses minimal modules with member_not_a_binder (blocks door-grain controls) #13654
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Closed
Closed
Changes from all commits
Commits
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| module v2.lens.common.record_field_carrier | ||
|
|
||
| import std.optional { Absent, Present } | ||
| import v2.std.node { Node } | ||
| import v2.extdeps.languages.dag { | ||
| namespace_graft_spine_chain_reaches_module_body, | ||
| parse_production_emitted_identity_optional | ||
| } | ||
|
|
||
| // THE CARRIER PREDICATE THE UNIT-MODELING AND LIFECYCLE-CARRIER LENSES SHARE. Both fold every | ||
| // TypeNode's Authored children through member_edge_type_node and refuse a child that is not a | ||
| // binder. A module shell, a marked module body, and a namespace-graft spine are TypeNode Conj | ||
| // containers whose Authored members are modules and declarations, not record fields; judging them | ||
| // as payloads is the member_not_a_binder door refusal on valid modules (compile_door_cause_ownership | ||
| // member_not_a_binder row). Production identity Present covers the shell and the marked body; | ||
| // the spine is the remaining unmarked single-Named-Conj chain that ends at that body | ||
| // (namespace_graft_spine_chain_reaches_module_body — shape alone would misread an inline nested | ||
| // record, so the body mark is the discriminator). | ||
|
|
||
| fn node_is_module_surface_or_namespace_container(node: Node) -> Bool { | ||
| match parse_production_emitted_identity_optional(node: node) { | ||
| Present { value: _ } => true | ||
| Absent => namespace_graft_spine_chain_reaches_module_body(node: node) | ||
| } | ||
| } | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
22 changes: 22 additions & 0 deletions
22
src/v2/test/lens_fact_density/surface_identity_atom_not_a_type_carrier_test.dag
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,22 @@ | ||
| module v2.test.lens_fact_density.surface_identity_atom_not_a_type_carrier | ||
|
|
||
| import std.occurrence_identity { OccurrenceSynthetic } | ||
| import v2.lens.fact_density { NotATypeCarrier, carrier_spec_fact } | ||
| import v2.std.node { Atom, Node, Symbol, TypeNode } | ||
|
|
||
| data surface_module_identity_atom: Node = Node { | ||
| kind: TypeNode { connective: Atom { identity: ^dag_surface_module } }, | ||
| children: [], | ||
| occurrence_id: OccurrenceSynthetic | ||
| } | ||
|
|
||
| data surface_body_identity_atom: Node = Node { | ||
| kind: TypeNode { connective: Atom { identity: ^namespace_graft_module_body } }, | ||
| children: [], | ||
| occurrence_id: OccurrenceSynthetic | ||
| } | ||
|
|
||
| test fn surface_identity_atoms_are_not_hollow_aliases() -> Bool { | ||
| (carrier_spec_fact(carrier: surface_module_identity_atom) == NotATypeCarrier) | ||
| && (carrier_spec_fact(carrier: surface_body_identity_atom) == NotATypeCarrier) | ||
| } |
159 changes: 159 additions & 0 deletions
159
src/v2/test/lens_unit_modeling/module_container_is_not_a_record_carrier_test.dag
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,159 @@ | ||
| module v2.test.lens_unit_modeling.module_container_is_not_a_record_carrier | ||
|
|
||
| import std.occurrence_identity { OccurrenceSynthetic } | ||
| import v2.compiler.compile { | ||
| CompileLensSubtree, | ||
| required_lenses_at_grain, | ||
| run_required_lens_gates_on_subtree | ||
| } | ||
| import v2.compiler.infer { InferredTree } | ||
| import v2.extdeps.languages.dag { | ||
| dag_grammar_atom, | ||
| dag_named_edge, | ||
| namespace_graft_namespace_body_node | ||
| } | ||
| import v2.lens.lifecycle_carrier { lifecycle_carrier_gate } | ||
| import v2.lens.unit_modeling { unit_modeling_gate } | ||
| import v2.std.diagnostic { Accepted, Rejected } | ||
| import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } | ||
| import v2.std.node { | ||
| Atom, | ||
| Authored, | ||
| Conj, | ||
| Edge, | ||
| Node, | ||
| Symbol, | ||
| TypeNode | ||
| } | ||
| import v2.test.lens_common.infer_fixture { | ||
| claim_inferred_facts, | ||
| claim_inferred_tree | ||
| } | ||
|
|
||
| data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly | ||
|
|
||
| data mc_source: Node = Node { | ||
| kind: TypeNode { connective: Conj }, | ||
| children: [], | ||
| occurrence_id: OccurrenceSynthetic | ||
| } | ||
|
|
||
| data mc_marked_body: Node = namespace_graft_namespace_body_node(edges: [], source: mc_source) | ||
|
|
||
| data mc_inner_segment: Node = Node { | ||
| kind: TypeNode { connective: Conj }, | ||
| children: [ | ||
| Edge { | ||
| label: Authored { name: ^x }, | ||
| target: mc_marked_body | ||
| } | ||
| ], | ||
| occurrence_id: OccurrenceSynthetic | ||
| } | ||
|
|
||
| data mc_spine: Node = Node { | ||
| kind: TypeNode { connective: Conj }, | ||
| children: [ | ||
| Edge { | ||
| label: Authored { name: ^extdeps }, | ||
| target: mc_inner_segment | ||
| } | ||
| ], | ||
| occurrence_id: OccurrenceSynthetic | ||
| } | ||
|
|
||
| data mc_module_shell: Node = Node { | ||
| kind: TypeNode { connective: Conj }, | ||
| children: [ | ||
| dag_named_edge( | ||
| name: ^grammar_production_identity_node_projection, | ||
| target: dag_grammar_atom(id: ^dag_surface_module) | ||
| ), | ||
| dag_named_edge( | ||
| name: ^grammar_production_captured_node_projection, | ||
| target: mc_spine | ||
| ) | ||
| ], | ||
| occurrence_id: OccurrenceSynthetic | ||
| } | ||
|
|
||
| fn mc_shell_tree() -> InferredTree { | ||
| claim_inferred_tree( | ||
| root: mc_module_shell, | ||
| facts: claim_inferred_facts( | ||
| type_symbol: ^mc_shell_type_sym, | ||
| algebra_symbol: ^mc_shell_algebra_sym, | ||
| descent_symbol: ^mc_shell_descent_sym | ||
| ) | ||
| ) | ||
| } | ||
|
|
||
| data mc_text_atom: Node = Node { | ||
| kind: TypeNode { connective: Atom { identity: ^Text } }, | ||
| children: [], | ||
| occurrence_id: OccurrenceSynthetic | ||
| } | ||
|
|
||
| data mc_malformed_field_root: Node = Node { | ||
| kind: TypeNode { connective: Conj }, | ||
| children: [ | ||
| Edge { | ||
| label: Authored { name: ^x }, | ||
| target: mc_text_atom | ||
| } | ||
| ], | ||
| occurrence_id: OccurrenceSynthetic | ||
| } | ||
|
|
||
| fn mc_malformed_field_tree() -> InferredTree { | ||
| claim_inferred_tree( | ||
| root: mc_malformed_field_root, | ||
| facts: claim_inferred_facts( | ||
| type_symbol: ^mc_malformed_type_sym, | ||
| algebra_symbol: ^mc_malformed_algebra_sym, | ||
| descent_symbol: ^mc_malformed_descent_sym | ||
| ) | ||
| ) | ||
| } | ||
|
|
||
| test fn a_module_shell_is_not_refused_as_member_not_a_binder() -> Bool { | ||
| match unit_modeling_gate(node: mc_module_shell) { | ||
| Accepted { value: _, diagnostics: _ } => | ||
| match lifecycle_carrier_gate(node: mc_module_shell) { | ||
| Accepted { value: _, diagnostics: _ } => true | ||
| Rejected { diagnostics: _ } => false | ||
| } | ||
| Rejected { diagnostics: _ } => false | ||
| } | ||
| } | ||
|
|
||
| test fn a_namespace_spine_is_not_refused_as_member_not_a_binder() -> Bool { | ||
| match unit_modeling_gate(node: mc_spine) { | ||
| Accepted { value: _, diagnostics: _ } => | ||
| match lifecycle_carrier_gate(node: mc_spine) { | ||
| Accepted { value: _, diagnostics: _ } => true | ||
| Rejected { diagnostics: _ } => false | ||
| } | ||
| Rejected { diagnostics: _ } => false | ||
| } | ||
| } | ||
|
|
||
| test fn a_grafted_module_tree_clears_the_subtree_roster_of_member_not_a_binder() -> Bool { | ||
| match run_required_lens_gates_on_subtree( | ||
| inferred: mc_shell_tree(), | ||
| lenses: required_lenses_at_grain(grain: CompileLensSubtree) | ||
| ) { | ||
| Accepted { value: _, diagnostics: _ } => true | ||
| Rejected { diagnostics: d } => d.head.reason != ^member_not_a_binder | ||
| } | ||
| } | ||
|
|
||
| test fn a_hand_built_field_is_still_member_not_a_binder_on_the_subtree_roster() -> Bool { | ||
| match run_required_lens_gates_on_subtree( | ||
| inferred: mc_malformed_field_tree(), | ||
| lenses: required_lenses_at_grain(grain: CompileLensSubtree) | ||
| ) { | ||
| Rejected { diagnostics: d } => d.head.reason == ^member_not_a_binder | ||
| Accepted { value: _, diagnostics: _ } => false | ||
| } | ||
| } |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For a graft with
dnamespace segments,run_required_lens_gates_on_subtreeinvokes both the unit-modeling and lifecycle-carrier gates at every segment, and each invocation reaches this branch;namespace_graft_spine_chain_reaches_module_bodythen recursively walks the remaining suffix throughnamespace_graft_spine_shaped_end. This makes compile-door validation Θ(d²), rather than the documented node-local linear traversal, and can cause excessive compile time or recursion depth for deeply qualified module paths. Preserve an O(1) marker on each segment or classify the spine once at root grain instead.Useful? React with 👍 / 👎.