Skip to content

Gate-1 repr grounding: ground modeled String to native Rust String in v1 emit #6983

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.

Sign up for GitHub

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

Merged
briansrls merged 3 commits into from
Jul 21, 2026
Merged

Gate-1 repr grounding: ground modeled String to native Rust String in v1 emit #6983

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c272e95
WIP: Gate-1 repr-mismatch lever (emit_representation_mismatch brick):…
briansrls Jul 21, 2026
4a13e13
repr_mismatch: update faithful-string witness for native-String groun…
briansrls Jul 21, 2026
ebef90b
WIP: Gate-1 CRITICAL PATH — repr grounding (reassigned from stalled b…
briansrls Jul 21, 2026
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
46 changes: 14 additions & 32 deletions src/v1/05_emit_rust.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -222,7 +222,7 @@ fn render_rust_type_without_applied_binding(n: Node, shared_types: Set<String>,
let tn = authored_name_at(source_indices: source_indices, node: n)
if type_node_has_unbound_type_variable(n: n, generic_param_names: emit_info.fn_generic_param_names, source_indices: source_indices) {
"_"
} else if tn == "String" && n.children |> count == 0 && corpus_repr_is_faithful(corpus_repr: corpus_repr) {
} else if is_host_text_carrier_type(n: n, source_indices: source_indices, corpus_repr: corpus_repr) {
rust_carrier_optional_wrap(n: n, rendered: render_rust_text_carrier(shared_types: shared_types))
} else {
render_node_type(n: n, target: Rust, shared_types: shared_types, source_indices: source_indices)
Expand All @@ -248,15 +248,11 @@ fn is_host_freemonoid_vec_alias(name: String, corpus_repr: RustCorpusRepr) -> Bo
corpus_repr_is_host(corpus_repr: corpus_repr) && name == "FreeMonoid"
}
fn render_rust_text_carrier(shared_types: Set<String>) -> String {
render_rust_shared_type_if_needed(type_name: "FreeMonoid", rendered: "FreeMonoid<Char>", shared_types: shared_types)
render_rust_shared_type_if_needed(type_name: "String", rendered: "String", shared_types: shared_types)
}

fn emit_rust_host_to_dag_string_via_seam(host_expr: String, corpus_repr: RustCorpusRepr) -> String {
if corpus_repr_is_faithful(corpus_repr: corpus_repr) {
concat("crate::v2_std_text::host_string_text_from_rust_host(", host_expr, ")")
} else {
host_expr
}
host_expr
}

fn emit_rust_map_literal_key(field_name: String, key_is_string: Bool, corpus_repr: RustCorpusRepr) -> String {
Expand Down Expand Up @@ -285,11 +281,7 @@ fn map_literal_key_is_string(map_type_node: Node, source_indices: Map<String, Ne
}

fn emit_rust_dag_string_to_host_via_seam(dag_expr: String, corpus_repr: RustCorpusRepr) -> String {
if corpus_repr_is_faithful(corpus_repr: corpus_repr) {
concat("crate::v2_std_text::host_string_text_to_rust_host(", dag_expr, ")")
} else {
dag_expr
}
dag_expr
}

fn rust_host_string_seam_fn_emit(name: String) -> String? {
Expand Down Expand Up @@ -408,17 +400,13 @@ fn rust_host_text_carrier_elem_name(n: Node, source_indices: Map<String, Newline
}

fn is_host_text_carrier_type(n: Node, source_indices: Map<String, NewlineIndex>, corpus_repr: RustCorpusRepr) -> Bool {
if !corpus_repr_is_host(corpus_repr: corpus_repr) {
false
let nm = authored_name_at(source_indices: source_indices, node: n)
if nm == "String" {
true
} else if nm == "FreeMonoid" || nm == "List" {
rust_host_text_carrier_elem_name(n: n, source_indices: source_indices) == "Char"
} else {
let nm = authored_name_at(source_indices: source_indices, node: n)
if nm == "String" {
true
} else if nm == "FreeMonoid" || nm == "List" {
rust_host_text_carrier_elem_name(n: n, source_indices: source_indices) == "Char"
} else {
false
}
false
}
}

Expand All @@ -432,19 +420,13 @@ fn rust_seed_host_freemonoid_empty(carrier_name: String, corpus_repr: RustCorpus
fn rust_named_type_base(name: String, corpus_repr: RustCorpusRepr) -> String {
if name == "Witness" || name == "witness" {
"Witness"
} else if name == "String" && corpus_repr_is_faithful(corpus_repr: corpus_repr) {
"FreeMonoid<Char>"
} else {
coerce_primitive_type(target: Rust, dag_name: name)
}
}

fn rust_applied_type_base(name: String, corpus_repr: RustCorpusRepr) -> String {
if name == "String" && corpus_repr_is_faithful(corpus_repr: corpus_repr) {
"FreeMonoid"
} else {
rust_named_type_base(name: name, corpus_repr: corpus_repr)
}
rust_named_type_base(name: name, corpus_repr: corpus_repr)
}

fn rust_normalize_witness_type_text(rendered: String) -> String {
Expand Down Expand Up @@ -613,7 +595,7 @@ fn render_rust_decl_type(n: Node, generic_param_names: List<String>, shared_type
let name = authored_name_at(source_indices: source_indices, node: n)
if n.connective == NoConnective && n.children |> count == 0 && (generic_param_names |> any(g => g == name)) {
to_pascal(name: name)
} else if n.connective == NoConnective && n.children |> count == 0 && applied_prop == none && name == "String" && corpus_repr_is_faithful(corpus_repr: corpus_repr) {
} else if n.connective == NoConnective && n.children |> count == 0 && applied_prop == none && is_host_text_carrier_type(n: n, source_indices: source_indices, corpus_repr: corpus_repr) {
rust_carrier_optional_wrap(n: n, rendered: render_rust_text_carrier(shared_types: shared_types))
} else if n.connective == NoConnective && n.children |> count == 0 && applied_prop == none && set_contains(shared_types, name) {
let rendered = rust_render_type_leaf_name(name: name, variant_to_enum: variant_to_enum)
Expand Down Expand Up @@ -705,7 +687,7 @@ fn render_rust_fn_sig_type(n: Node, generic_param_names: List<String>, shared_ty
return render_rust_decl_type(n: n, generic_param_names: generic_param_names, shared_types: shared_types, corpus_repr: corpus_repr, source_indices: source_indices, variant_to_enum: variant_to_enum, env: env)
}
let name = authored_name_at(source_indices: source_indices, node: n)
if n.connective == NoConnective && n.children |> count == 0 && name == "String" && corpus_repr_is_faithful(corpus_repr: corpus_repr) {
if n.connective == NoConnective && n.children |> count == 0 && is_host_text_carrier_type(n: n, source_indices: source_indices, corpus_repr: corpus_repr) {
rust_carrier_optional_wrap(n: n, rendered: render_rust_text_carrier(shared_types: shared_types))
} else if n.connective == NoConnective && n.children |> count == 0 && name != "" && name != "String" && !is_container_type(name: name) && rust_fn_sig_peel_closed_alias(env: env, n: n) && rust_fn_sig_preserves_authored_alias_leaf(name: name, corpus_repr: corpus_repr) {
render_rust_shared_type_with_optional(n: n, type_name: name, rendered: name, shared_types: shared_types)
Expand Down Expand Up @@ -767,7 +749,7 @@ fn render_rust_alias_rhs_type(n: Node, generic_param_names: List<String>, shared
match rust_seed_host_numeric_alias(name: name, corpus_repr: corpus_repr) {
Present { value: host } => host
Absent =>
if name == "String" && corpus_repr_is_faithful(corpus_repr: corpus_repr) {
if is_host_text_carrier_type(n: n, source_indices: source_indices, corpus_repr: corpus_repr) {
rust_carrier_optional_wrap(n: n, rendered: render_rust_text_carrier(shared_types: shared_types))
} else {
match rust_opaque_kernel_alias_carrier(name: name) {
Expand Down
95 changes: 33 additions & 62 deletions src/v1/stage0/src/v1_compiler_emit_rust.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -380,10 +380,11 @@ pub fn render_rust_type_without_applied_binding(
) {
"_".to_string()
} else {
if (((tn.clone() == "String".to_string())
&& ((n.children.clone().len() as i64) == 0))
&& corpus_repr_is_faithful(corpus_repr.clone()))
{
if is_host_text_carrier_type(
n.clone(),
source_indices.clone(),
corpus_repr.clone(),
) {
rust_carrier_optional_wrap(
n.clone(),
render_rust_text_carrier(shared_types.clone()),
Expand Down Expand Up @@ -434,8 +435,8 @@ pub fn is_host_freemonoid_vec_alias(name: String, corpus_repr: RustCorpusRepr) -

pub fn render_rust_text_carrier(shared_types: Rc<BTreeSet<String>>) -> String {
render_rust_shared_type_if_needed(
"FreeMonoid".to_string(),
"FreeMonoid<Char>".to_string(),
"String".to_string(),
"String".to_string(),
shared_types.clone(),
)
}
Expand All @@ -444,17 +445,7 @@ pub fn emit_rust_host_to_dag_string_via_seam(
host_expr: String,
corpus_repr: RustCorpusRepr,
) -> String {
if corpus_repr_is_faithful(corpus_repr.clone()) {
v1_rt::concat(
v1_rt::concat(
"crate::v2_std_text::host_string_text_from_rust_host(".to_string(),
host_expr.clone(),
),
")".to_string(),
)
} else {
host_expr.clone()
}
host_expr
}

pub fn emit_rust_map_literal_key(
Expand Down Expand Up @@ -500,17 +491,7 @@ pub fn emit_rust_dag_string_to_host_via_seam(
dag_expr: String,
corpus_repr: RustCorpusRepr,
) -> String {
if corpus_repr_is_faithful(corpus_repr.clone()) {
v1_rt::concat(
v1_rt::concat(
"crate::v2_std_text::host_string_text_to_rust_host(".to_string(),
dag_expr.clone(),
),
")".to_string(),
)
} else {
dag_expr.clone()
}
dag_expr
}

pub fn rust_host_string_seam_fn_emit(name: String) -> Option<String> {
Expand Down Expand Up @@ -641,21 +622,16 @@ pub fn is_host_text_carrier_type(
source_indices: Rc<HashMap<String, Rc<NewlineIndex>>>,
corpus_repr: RustCorpusRepr,
) -> bool {
if !corpus_repr_is_host(corpus_repr.clone()) {
false
} else {
{
let nm = authored_name_at(source_indices.clone(), n.clone());
if (nm.clone() == "String".to_string()) {
true
{
let nm = authored_name_at(source_indices.clone(), n.clone());
if (nm.clone() == "String".to_string()) {
true
} else {
if ((nm.clone() == "FreeMonoid".to_string()) || (nm.clone() == "List".to_string())) {
(rust_host_text_carrier_elem_name(n.clone(), source_indices.clone())
== "Char".to_string())
} else {
if ((nm.clone() == "FreeMonoid".to_string()) || (nm.clone() == "List".to_string()))
{
(rust_host_text_carrier_elem_name(n.clone(), source_indices.clone())
== "Char".to_string())
} else {
false
}
false
}
}
}
Expand All @@ -675,21 +651,12 @@ pub fn rust_named_type_base(name: String, corpus_repr: RustCorpusRepr) -> String
if ((name.clone() == "Witness".to_string()) || (name.clone() == "witness".to_string())) {
"Witness".to_string()
} else {
if ((name.clone() == "String".to_string()) && corpus_repr_is_faithful(corpus_repr.clone()))
{
"FreeMonoid<Char>".to_string()
} else {
coerce_primitive_type(RenderTarget::Rust, name.clone())
}
coerce_primitive_type(RenderTarget::Rust, name.clone())
}
}

pub fn rust_applied_type_base(name: String, corpus_repr: RustCorpusRepr) -> String {
if ((name.clone() == "String".to_string()) && corpus_repr_is_faithful(corpus_repr.clone())) {
"FreeMonoid".to_string()
} else {
rust_named_type_base(name.clone(), corpus_repr.clone())
}
rust_named_type_base(name.clone(), corpus_repr.clone())
}

pub fn rust_normalize_witness_type_text(rendered: String) -> String {
Expand Down Expand Up @@ -1215,11 +1182,14 @@ pub fn render_rust_decl_type(
{
to_pascal(name.clone())
} else {
if (((((n.connective.clone() == Connective::NoConnective)
if ((((n.connective.clone() == Connective::NoConnective)
&& ((n.children.clone().len() as i64) == 0))
&& (applied_prop.clone() == None))
&& (name.clone() == "String".to_string()))
&& corpus_repr_is_faithful(corpus_repr.clone()))
&& is_host_text_carrier_type(
n.clone(),
source_indices.clone(),
corpus_repr.clone(),
))
{
rust_carrier_optional_wrap(
n.clone(),
Expand Down Expand Up @@ -1502,10 +1472,9 @@ pub fn render_rust_fn_sig_type(
);
}
let name = authored_name_at(source_indices.clone(), n.clone());
if ((((n.connective.clone() == Connective::NoConnective)
if (((n.connective.clone() == Connective::NoConnective)
&& ((n.children.clone().len() as i64) == 0))
&& (name.clone() == "String".to_string()))
&& corpus_repr_is_faithful(corpus_repr.clone()))
&& is_host_text_carrier_type(n.clone(), source_indices.clone(), corpus_repr.clone()))
{
rust_carrier_optional_wrap(n.clone(), render_rust_text_carrier(shared_types.clone()))
} else {
Expand Down Expand Up @@ -1721,9 +1690,11 @@ pub fn render_rust_alias_rhs_type(
match rust_seed_host_numeric_alias(name.clone(), corpus_repr.clone()) {
Some(host) => host.clone(),
None => {
if ((name.clone() == "String".to_string())
&& corpus_repr_is_faithful(corpus_repr.clone()))
{
if is_host_text_carrier_type(
n.clone(),
source_indices.clone(),
corpus_repr.clone(),
) {
rust_carrier_optional_wrap(
n.clone(),
render_rust_text_carrier(shared_types.clone()),
Expand Down
36 changes: 16 additions & 20 deletions src/v1/tests/src/faithful_string_element_char_witness_test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,49 +7,45 @@ use v1_compiler::v1_compiler_emit_rust::{
use v1_compiler::v1_compiler_infer_emit_info::RustCorpusRepr;

#[test]
fn faithful_string_leaf_base_is_freemonoid_char() {
fn faithful_string_leaf_base_grounds_to_native_string() {
let leaf = rust_named_type_base("String".to_string(), RustCorpusRepr::FaithfulFreeMonoid);
assert_eq!(
leaf, "FreeMonoid<Char>",
"faithful String leaf must render the declared Char element (got {leaf:?})"
leaf, "String",
"faithful String leaf must ground to native String (Gate-1 text-carrier grounding), got {leaf:?}"
);
assert_ne!(
leaf, "FreeMonoid<Nat>",
"leaf must not bake the wrong Nat element"
leaf, "FreeMonoid<Char>",
"faithful String must not render FreeMonoid<Char> after grounding"
);
}

#[test]
fn faithful_string_text_carrier_is_freemonoid_char() {
fn faithful_string_text_carrier_grounds_to_native_string() {
let carrier = render_rust_text_carrier(Rc::new(BTreeSet::new()));
assert_eq!(carrier, "FreeMonoid<Char>");
assert_ne!(carrier, "FreeMonoid<Nat>");
assert_eq!(carrier, "String");
assert_ne!(carrier, "FreeMonoid<Char>");
}

#[test]
fn faithful_string_applied_base_is_bare_freemonoid() {
fn faithful_string_applied_base_grounds_to_native_string() {
let base = rust_applied_type_base("String".to_string(), RustCorpusRepr::FaithfulFreeMonoid);
assert_eq!(
base, "FreeMonoid",
"applied String base must be bare (element from the resolved child)"
base, "String",
"applied String base must ground to native String, got {base:?}"
);
assert!(
!base.contains('<'),
"applied base must hold no element literal (got {base:?})"
!base.contains("FreeMonoid"),
"applied base must not render FreeMonoid after grounding (got {base:?})"
);
}

#[test]
fn faithful_string_applied_single_application_not_doubled() {
fn faithful_string_applied_single_application_stays_string() {
let base = rust_applied_type_base("String".to_string(), RustCorpusRepr::FaithfulFreeMonoid);
let applied = format!("{base}<{}>", "Char");
assert_eq!(
applied, "FreeMonoid<Char>",
"applied String must be a single application"
);
assert_ne!(
applied, "FreeMonoid<Nat><Char>",
"applied String must not double-apply"
applied, "String<Char>",
"applied String after grounding is still the native carrier (got {applied:?})"
);
}

Expand Down
10 changes: 5 additions & 5 deletions src/v1/tests/src/map_literal_string_key_test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,17 +39,17 @@ fn non_string_key_is_left_as_literal() {
}

#[test]
fn faithful_repr_routes_owned_key_through_the_text_seam() {
// Under the faithful FreeMonoid repr the key still becomes an owned String first,
// then crosses the host->dag text seam (which consumes a `String`).
fn faithful_repr_grounds_string_key_to_owned_native_string() {
// Gate-1 text-carrier grounding: both corpus reprs emit native `String` keys
// (no host->dag text seam after FreeMonoid<Char> was dissolved).
let out = emit_rust_map_literal_key(
"alpha".to_string(),
true,
RustCorpusRepr::FaithfulFreeMonoid,
);
assert_eq!(
out, "crate::v2_std_text::host_string_text_from_rust_host(\"alpha\".to_string())",
"faithful repr must hand the seam an owned String"
out, "\"alpha\".to_string()",
"faithful repr must ground String keys to owned native String"
);
}

Expand Down
Loading